Simplify polymat_permite_bitrev_to_customer() (native version)

The code structure now mimics the data structure to make proof tractable.

Also updates Makefile for this proof in line with the similar function
in mldsa-native.

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

mlkem/src/indcpa.c

@@ -188,21 +188,30 @@ __contract__(
   requires(memory_no_alias(a, sizeof(mlk_polymat)))
   requires(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
     array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
-  assigns(object_whole(a))
+  assigns(memory_slice(a, sizeof(mlk_polymat)))
   ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
     array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
 {
 #if defined(MLK_USE_NATIVE_NTT_CUSTOM_ORDER)
-  unsigned i;
-  for (i = 0; i < MLKEM_K * MLKEM_K; i++)
+  unsigned i, j;
+  for (i = 0; i < MLKEM_K; i++)
   __loop__(
-     assigns(i, object_whole(a))
-     invariant(i <= MLKEM_K * MLKEM_K)
-     invariant(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
-       array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
+    assigns(i, j, memory_slice(a, sizeof(mlk_polymat)))
+    invariant(i <= MLKEM_K)
+    invariant(forall(x2, 0, MLKEM_K, forall(y2, 0, MLKEM_K,
+      array_bound(a->vec[x2].vec[y2].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
   {
-    mlk_poly_permute_bitrev_to_custom(
-        a->vec[i / MLKEM_K].vec[i % MLKEM_K].coeffs);
+    for (j = 0; j < MLKEM_K; j++)
+    __loop__(
+      assigns(j, memory_slice(a, sizeof(mlk_polymat)))
+      invariant(i <= MLKEM_K)
+      invariant(j <= MLKEM_K)
+      invariant(forall(x3, 0, MLKEM_K, forall(y3, 0, MLKEM_K,
+        array_bound(a->vec[x3].vec[y3].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
+    )
+    {
+      mlk_poly_permute_bitrev_to_custom(a->vec[i].vec[j].coeffs);
+    }
   }
 #else  /* MLK_USE_NATIVE_NTT_CUSTOM_ORDER */
   /* Nothing to do */

proofs/cbmc/polymat_permute_bitrev_to_custom_native/Makefile

@@ -26,7 +26,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
+CBMCFLAGS=--smt2 --slice-formula --no-array-field-sensitivity
 
 FUNCTION_NAME = mlk_polymat_permute_bitrev_to_custom_native
 
@@ -35,7 +35,7 @@ FUNCTION_NAME = mlk_polymat_permute_bitrev_to_custom_native
 # restrict the number of EXPENSIVE CBMC jobs running at once. See the
 # documentation in Makefile.common under the "Job Pools" heading for details.
 # EXPENSIVE = true
-CBMC_OBJECT_BITS = 10
+CBMC_OBJECT_BITS = 12
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file