Improve speed of proof of matvec_mul()

Adjust modelling of arrays in CBMC for proof of this function, as recommended by CBMC team (CBMC Issue 8505). Signed-off-by: Rod Chapman <[email protected]>
pq-code-package · Nov 14, 2024 · 73abc1a · 73abc1a
1 parent 6aa6118
commit 73abc1a
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 8 deletions.
diff --git a/cbmc/proofs/matvec_mul/Makefile b/cbmc/proofs/matvec_mul/Makefile
@@ -13,19 +13,18 @@ DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
-UNWINDSET += matvec_mul.0:4 # Maximum value of MLKEM_K
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c
 
 CHECK_FUNCTION_CONTRACTS=matvec_mul
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_mulcache_compute $(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
+CBMCFLAGS=--smt2 --no-array-field-sensitivity --arrays-uf-always --slice-formula
 
 FUNCTION_NAME = $(MLKEM_NAMESPACE)matvec_mul
 
@@ -36,7 +35,7 @@ FUNCTION_NAME = $(MLKEM_NAMESPACE)matvec_mul
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 10
+CBMC_OBJECT_BITS = 8
 
 # 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

diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c
@@ -220,7 +220,7 @@ void gen_matrix_entry(poly *entry,
   while (ctr < MLKEM_N)  // clang-format off
     ASSIGNS(ctr, state, OBJECT_UPTO(entry, sizeof(poly)), OBJECT_WHOLE(buf))
     INVARIANT(0 <= ctr && ctr <= MLKEM_N)
-    INVARIANT(ctr > 0 ==> ARRAY_BOUND(entry->coeffs, 0, ctr - 1, 
+    INVARIANT(ctr > 0 ==> ARRAY_BOUND(entry->coeffs, 0, ctr - 1,
                                           0, (MLKEM_Q - 1)))  // clang-format on
     {
       shake128_squeezeblocks(buf, 1, &state);
@@ -342,9 +342,12 @@ void matvec_mul(polyvec *out, const polyvec a[MLKEM_K], const polyvec *v,
   ASSIGNS(OBJECT_WHOLE(out))
 // clang-format on
 {
-  for (int i = 0; i < MLKEM_K; i++) {
-    polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a[i], v, vc);
-  }
+  for (int i = 0; i < MLKEM_K; i++)  // clang-format off
+    ASSIGNS(i, OBJECT_WHOLE(out))
+    INVARIANT(i >= 0 && i <= MLKEM_K)  // clang-format on
+    {
+      polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a[i], v, vc);
+    }
 }
 
 /*************************************************