From 73abc1a5ff5aa74ea844abb92cb06f4abd1a1125 Mon Sep 17 00:00:00 2001
From: Rod Chapman <rodchap@amazon.com>
Date: Thu, 14 Nov 2024 17:23:15 +0000
Subject: [PATCH] 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 <rodchap@amazon.com>
---
 cbmc/proofs/matvec_mul/Makefile |  7 +++----
 mlkem/indcpa.c                  | 11 +++++++----
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/cbmc/proofs/matvec_mul/Makefile b/cbmc/proofs/matvec_mul/Makefile
index 48c3d6d1d..24b282a6c 100644
--- 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
index 042b25324..27ae39475 100644
--- 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);
+    }
 }
 
 /*************************************************