CBMC: Add spec + proof for polyvec_basemul_acc_montgomery_cached

The proof is less trivial than the ones before since one has to use
the output bounds of the lower level functions to show that the
accumulation loop does not overflow.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

cbmc/proofs/polyvec_basemul_acc_montgomery_cached/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = polyvec_basemul_acc_montgomery_cached_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = polyvec_basemul_acc_montgomery_cached
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += $(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached.0:4 # Largest value of MLKEM_K
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_basemul_montgomery_cached $(MLKEM_NAMESPACE)poly_add
+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
+
+FUNCTION_NAME = polyvec_basemul_acc_montgomery_cached
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# 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
+
+# This function is large enough to need...
+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
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

cbmc/proofs/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c

@@ -0,0 +1,30 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0 AND Apache-2.0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file polyvec_basemul_acc_montgomery_cached_harness.c
+ * @brief Implements the proof harness for basemul_cached function.
+ */
+#include "polyvec.h"
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+  poly r;
+  polyvec a, b;
+  polyvec_mulcache b_cached;
+
+  polyvec_basemul_acc_montgomery_cached(&r, &a, &b, &b_cached);
+}

mlkem/polyvec.c

@@ -226,18 +226,35 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
   POLYVEC_BOUND(b, NTT_BOUND);
   POLYVEC_BOUND(b_cache, MLKEM_Q);
 
-  unsigned int i;
+  int i;
   poly t;
 
   poly_basemul_montgomery_cached(r, &a->vec[0], &b->vec[0], &b_cache->vec[0]);
-  for (i = 1; i < MLKEM_K; i++) {
-    poly_basemul_montgomery_cached(&t, &a->vec[i], &b->vec[i],
-                                   &b_cache->vec[i]);
-    poly_add(r, r, &t);
-    // abs bounds: < (i+1) * 3/2 * q
-  }
 
-  // abs bounds: < MLKEM_K * 3/2 * q <= 4 * 3/2 * q = 19974
+  for (i = 1; i < MLKEM_K; i++)
+      // clang-format off
+    ASSIGNS(i, t, OBJECT_WHOLE(r))
+    INVARIANT(i >= 1 && i <= MLKEM_K)
+    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs,
+                              i * (-3 * HALF_Q + 1), i * (3 * HALF_Q - 1)))
+    DECREASES(MLKEM_K - i)
+    // clang-format on
+    {
+      poly_basemul_montgomery_cached(&t, &a->vec[i], &b->vec[i],
+                                     &b_cache->vec[i]);
+      poly_add(r, r, &t);
+      // abs bounds: < (i+1) * 3/2 * q
+    }
+
+  // Those bounds are true for the C implementation, but not needed
+  // in the higher level bounds reasoning. It is thus best to omit
+  // them from the spec to not unnecessarily constraint native implementations.
+  ASSERT(
+      ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs,
+                      MLKEM_K * (-3 * HALF_Q + 1), MLKEM_K * (3 * HALF_Q - 1)),
+      "polyvec_basemul_acc_montgomery_cached output bounds");
+  // TODO: Integrate CBMC assertin into POLY_BOUND if CBMC is set
+  POLY_BOUND(r, MLKEM_K * 3 * HALF_Q);
 }
 #else  /* !MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */
 void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,

mlkem/polyvec.h

@@ -40,9 +40,37 @@ void polyvec_basemul_acc_montgomery(poly *r, const polyvec *a,
 // REF-CHANGE: This function does not exist in the reference implementation
 #define polyvec_basemul_acc_montgomery_cached \
   MLKEM_NAMESPACE(polyvec_basemul_acc_montgomery_cached)
+/*************************************************
+ * Name:        polyvec_basemul_acc_montgomery_cached
+ *
+ * Description: Scalar product of two vectors of polynomials in NTT domain,
+ *              using mulcache for second operand.
+ *
+ *              Bounds:
+ *              - a is assumed to be coefficient-wise < q in absolute value.
+ *              - No bounds guarantees for the coefficients in the result.
+ *
+ * Arguments:   - poly *r: pointer to output polynomial
+ *              - const polyvec *a: pointer to first input polynomial vector
+ *              - const polyvec *b: pointer to second input polynomial vector
+ *              - const polyvec_mulcache *b_cache: pointer to mulcache
+ *                  for second input polynomial vector. Can be computed
+ *                  via polyvec_mulcache_compute().
+ **************************************************/
 void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
                                            const polyvec *b,
-                                           const polyvec_mulcache *b_cache);
+                                           const polyvec_mulcache *b_cache)
+    // clang-format off
+REQUIRES(r != NULL && a != NULL && b != NULL && b_cache != NULL)
+REQUIRES(IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(a, sizeof(polyvec)) && IS_FRESH(b, sizeof(polyvec)))
+REQUIRES(IS_FRESH(b_cache, sizeof(polyvec_mulcache)))
+// Input is coefficient-wise < q in absolute value
+REQUIRES(FORALL(int, k1, 0, MLKEM_K - 1,
+ ARRAY_IN_BOUNDS(int, k2, 0, MLKEM_N - 1,
+   a->vec[k1].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1))))
+ASSIGNS(OBJECT_WHOLE(r));
+// clang-format on
 
 // REF-CHANGE: This function does not exist in the reference implementation
 #define polyvec_mulcache_compute MLKEM_NAMESPACE(polyvec_mulcache_compute)