Improve CBMC proof for forward NTT

cbmc/proofs/ntt_butterfly_block_at/Makefile

@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
 
 CHECK_FUNCTION_CONTRACTS=ntt_butterfly_block_at
-USE_FUNCTION_CONTRACTS= ntt_butterfly_block
+USE_FUNCTION_CONTRACTS= $(MLKEM_NAMESPACE)fqmul #ntt_butterfly_block
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

cbmc/proofs/ntt_butterfly_block_at/ntt_butterfly_block_at_harness.c

@@ -10,8 +10,7 @@
  * @brief Implements the proof harness for ntt_butterfly_block_at function.
  */
 #include <stdint.h>
-void ntt_butterfly_block_at(int16_t *p, int16_t root, int sz, int base,
-                            int stride, int bound);
+void ntt_butterfly_block_at(int16_t *r, int16_t root, int start, int len, int bound);
 
 /**
  * @brief Starting point for formal analysis
@@ -20,5 +19,5 @@ void ntt_butterfly_block_at(int16_t *p, int16_t root, int sz, int base,
 void harness(void) {
   int16_t *r, root;
   int sz, base, stride, bound;
-  ntt_butterfly_block_at(r, root, sz, base, stride, bound);
+  ntt_butterfly_block_at(r, root, base, stride, bound);
 }

mlkem/cbmc.h

@@ -4,6 +4,8 @@
 // Basic replacements for __CPROVER_XXX contracts
 ///////////////////////////////////////////////////
 
+#include "common.h"
+
 #ifndef CBMC
 
 #define STATIC_TESTABLE static
@@ -126,4 +128,11 @@
   }
 // clang-format on
 
+// Helper macros to make NTT contracts and invariants more readable
+// TODO: Consolidate this with the macros in cbmc.h
+#define SCALAR_ABS_BOUND(a, k) (-(k) <= (a) && (a) <= (k))
+#define ARRAY_ABS_BOUND(arr, lb, ub, k)                              \
+  ARRAY_IN_BOUNDS(int, MLKEM_CONCAT(i, __LINE__), (lb), (ub), (arr), \
+                  (-(k) + 1), ((k) - 1))
+
 #endif

mlkem/ntt.c

@@ -74,82 +74,49 @@ const int16_t zetas[128] = {
  **************************************************/
 #if !defined(MLKEM_USE_NATIVE_NTT)
 
-// Helper macros to make NTT contracts and invariants more readable
-// TODO: Consolidate this with the macros in cbmc.h
-#define SCALAR_IN_BOUNDS(a, lb, ub) ((lb) <= (a) && (a) <= (ub))
-#define SCALAR_Q_BOUND(a, k) \
-  SCALAR_IN_BOUNDS((a), (-(k) * MLKEM_Q + 1), ((k) * MLKEM_Q - 1))
-#define ARRAY_Q_BOUND(arr, lb, ub, k)                                \
-  ARRAY_IN_BOUNDS(int, MLKEM_CONCAT(i, __LINE__), (lb), (ub), (arr), \
-                  (-(k) * MLKEM_Q + 1), ((k) * MLKEM_Q - 1))
-
 // Compute a block CT butterflies with a fixed twiddle factor
-STATIC_TESTABLE  // clang-format off
-void ntt_butterfly_block(int16_t *r, int16_t root, int stride, int bound)
-  REQUIRES(1 <= stride && stride <= 128)
-  REQUIRES(1 <= bound && bound <= 7)
-  REQUIRES(IS_FRESH(r, 4 * stride))
-  REQUIRES(SCALAR_IN_BOUNDS(root, -HALF_Q + 1, HALF_Q - 1))
-  REQUIRES(ARRAY_Q_BOUND(r, 0, (2 * stride - 1), bound))
-  ASSIGNS(OBJECT_UPTO(r, sizeof(int16_t) * 2 * stride))
-  ENSURES(ARRAY_Q_BOUND(r, 0, (2 * stride - 1), bound+1))
+STATIC_TESTABLE
 // clang-format off
+void ntt_butterfly_block_at(int16_t *r, int16_t root, int start, int len, int bound)
+  REQUIRES(0 <= start && start < MLKEM_N && 1 <= len && len <= MLKEM_N / 2 && start + 2 * len <= MLKEM_N)
+  REQUIRES(0 <= bound && bound < INT16_MAX - MLKEM_Q)
+  REQUIRES(IS_FRESH(r, sizeof(int16_t) * MLKEM_N))
+  REQUIRES(SCALAR_ABS_BOUND(root, HALF_Q - 1))
+  REQUIRES(ARRAY_ABS_BOUND(r, 0, start - 1, bound + MLKEM_Q))
+  REQUIRES(ARRAY_ABS_BOUND(r, start, MLKEM_N - 1, bound))
+  ASSIGNS(OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N))
+  ENSURES(ARRAY_ABS_BOUND(r, 0, start + 2*len - 1, bound + MLKEM_Q))
+  ENSURES(ARRAY_ABS_BOUND(r, start + 2 * len, MLKEM_N - 1, bound))
+// clang-format on
 {
-  // Used for the specification only
-  ((void) bound);
+  // Parameter only used in the CBMC specification
+  ((void)bound);
   // clang-format off
-  for (int j = 0; j < stride; j++)
-    ASSIGNS(j, OBJECT_UPTO(r, sizeof(int16_t) * 2 * stride))
-    INVARIANT(0 <= j && j <= stride)
-    INVARIANT(ARRAY_Q_BOUND(r, 0,          j-1,            bound+1))
-    INVARIANT(ARRAY_Q_BOUND(r, stride,     stride + j - 1, bound+1))
-    INVARIANT(ARRAY_Q_BOUND(r, j,          stride - 1,     bound))
-    INVARIANT(ARRAY_Q_BOUND(r, stride + j, 2*stride - 1,   bound))
+  for (int j = start; j < start + len; j++)
+    ASSIGNS(j, OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N))
+    INVARIANT(start <= j && j <= start + len)
+    INVARIANT(ARRAY_ABS_BOUND(r, 0,           j - 1,           bound + MLKEM_Q))
+    INVARIANT(ARRAY_ABS_BOUND(r, j,           start + len - 1, bound))
+    INVARIANT(ARRAY_ABS_BOUND(r, start + len, j + len - 1,     bound + MLKEM_Q))
+    INVARIANT(ARRAY_ABS_BOUND(r, j + len,     MLKEM_N - 1,     bound))
     // clang-format on
     {
       int16_t t;
-      t = fqmul(r[j + stride], root);
-      r[j + stride] = r[j] - t;
+      t = fqmul(r[j + len], root);
+      r[j + len] = r[j] - t;
       r[j] = r[j] + t;
     }
 }
 
-// Framed version of ntt_bufferly_block
-//
-// TODO: This only exists because inlining ntt_butterfly_block() leads to
-// much longer proof times (in fact, I have not witnessed it finishing so far).
-// Even this proof, while seemingly a trivial framing, takes longer than all
-// of the 'actual' NTT proof.
+// Compute one layer of forward NTT
 STATIC_TESTABLE
-// clang-format off
-void ntt_butterfly_block_at(int16_t *p, int16_t root, int sz, int base, int stride, int bound)
-  REQUIRES(2 <= sz && sz <= 256 && (sz & 1) == 0)
-  REQUIRES(0 <= base && base < sz && 1 <= stride && stride <= sz / 2 && base + 2 * stride <= sz)
-  REQUIRES((stride & (stride - 1)) == 0)
-  REQUIRES((base & (stride - 1)) == 0)
-  REQUIRES(1 <= bound && bound <= 7)
-  REQUIRES(IS_FRESH(p, sizeof(int16_t) * sz))
-  REQUIRES(SCALAR_IN_BOUNDS(root, -HALF_Q + 1, HALF_Q - 1))
-  REQUIRES(ARRAY_Q_BOUND(p, 0, base - 1, bound + 1))
-  REQUIRES(ARRAY_Q_BOUND(p, base, sz - 1, bound))
-  ASSIGNS(OBJECT_UPTO(p, sizeof(int16_t) * sz))
-  ENSURES(ARRAY_Q_BOUND(p, 0, base + 2*stride - 1, bound + 1))
-  ENSURES(ARRAY_Q_BOUND(p, base + 2 * stride, sz - 1, bound))
-// clang-format on
-{
-  // Parameter only used in the CBMC specification
-  ((void)sz);
-  ntt_butterfly_block(p + base, root, stride, bound);
-}
-
-STATIC_TESTABLE
-// clang-format off
 void ntt_layer(poly *p, int layer)
+// clang-format off
   REQUIRES(IS_FRESH(p, sizeof(poly)))
   REQUIRES(1 <= layer && layer <= 7)
-  REQUIRES(ARRAY_Q_BOUND(p->coeffs, 0, MLKEM_N - 1, layer))
+  REQUIRES(ARRAY_ABS_BOUND(p->coeffs, 0, MLKEM_N - 1, layer * MLKEM_Q))
   ASSIGNS(OBJECT_UPTO(p, sizeof(poly)))
-  ENSURES(ARRAY_Q_BOUND(p->coeffs, 0, MLKEM_N - 1, layer + 1))
+  ENSURES(ARRAY_ABS_BOUND(p->coeffs, 0, MLKEM_N - 1, (layer + 1) * MLKEM_Q))
 // clang-format on
 {
   int16_t *r = p->coeffs;
@@ -160,12 +127,12 @@ void ntt_layer(poly *p, int layer)
     ASSIGNS(i, OBJECT_UPTO(r, sizeof(poly)))
     INVARIANT(1 <= layer && layer <= 7)
     INVARIANT(0 <= i && i <= blocks)
-    INVARIANT(ARRAY_Q_BOUND(r, 2 * i * len, MLKEM_N - 1, layer))
-    INVARIANT(ARRAY_Q_BOUND(r, 0, 2 * i * len - 1, layer + 1))
+    INVARIANT(ARRAY_ABS_BOUND(r, 2 * i * len, MLKEM_N - 1, layer * MLKEM_Q))
+    INVARIANT(ARRAY_ABS_BOUND(r, 0, 2 * i * len - 1, layer * MLKEM_Q + MLKEM_Q))
   // clang-format off
   {
     int16_t zeta = zetas[blocks + i];
-    ntt_butterfly_block_at(r, zeta, MLKEM_N, 2 * i * len, len, layer);
+    ntt_butterfly_block_at(r, zeta, 2 * i * len, len, layer * MLKEM_Q);
   }
 }
 
@@ -188,7 +155,7 @@ void poly_ntt(poly *p) {
   for (int layer = 1; layer < 8; layer++)
     ASSIGNS(layer, OBJECT_UPTO(p, sizeof(poly)))
     INVARIANT(1 <= layer && layer <= 8)
-    INVARIANT(ARRAY_Q_BOUND(p->coeffs, 0, MLKEM_N - 1, layer))
+    INVARIANT(ARRAY_ABS_BOUND(p->coeffs, 0, MLKEM_N - 1, layer * MLKEM_Q))
     // clang-format on
     {
       ntt_layer(p, layer);