Debug/CBMC: Interpret debug-assertions as proof obligations

Previously, runtime assertions via debug_assert_xxx and CBMC
assertions via cassert(...) were separate.

This commit modifies the implementation of the debug assertion
macros so that when CBMC is used, debug assertions are intepreted
as proof obligations.

This removes some redundancy and non-uniformity in the code,
and also reduces the likelihood that debug assertions and CBMC
contracts get out of sync. In some case, this actually happened,
and the commit fixes this. The commit also adds further bounds
assertions in alignment with pre/post conditions.

A slight nuisance is that the debug assertions cannot flatten
nested structures like polyvec for the bounds check, running
into issue diffblue/cbmc#8570. We
work around this by introducing a new `xxx_2d` (for 2-dimensional)
macro which takes two dimensions and uses a two-step array
access, circumventing the above CBMC issue.

Signed-off-by: Hanno Becker <[email protected]>

Author: hanno-becker

Diff for: examples/monolithic_build/mlkem_native_monobuild.c

@@ -373,6 +373,11 @@
 #undef debug_assert
 #endif
 
+/* mlkem/debug/debug.h */
+#if defined(debug_assert)
+#undef debug_assert
+#endif
+
 /* mlkem/debug/debug.h */
 #if defined(debug_assert_abs_bound)
 #undef debug_assert_abs_bound
@@ -383,6 +388,31 @@
 #undef debug_assert_abs_bound
 #endif
 
+/* mlkem/debug/debug.h */
+#if defined(debug_assert_abs_bound)
+#undef debug_assert_abs_bound
+#endif
+
+/* mlkem/debug/debug.h */
+#if defined(debug_assert_abs_bound_2d)
+#undef debug_assert_abs_bound_2d
+#endif
+
+/* mlkem/debug/debug.h */
+#if defined(debug_assert_abs_bound_2d)
+#undef debug_assert_abs_bound_2d
+#endif
+
+/* mlkem/debug/debug.h */
+#if defined(debug_assert_abs_bound_2d)
+#undef debug_assert_abs_bound_2d
+#endif
+
+/* mlkem/debug/debug.h */
+#if defined(debug_assert_bound)
+#undef debug_assert_bound
+#endif
+
 /* mlkem/debug/debug.h */
 #if defined(debug_assert_bound)
 #undef debug_assert_bound
@@ -393,6 +423,21 @@
 #undef debug_assert_bound
 #endif
 
+/* mlkem/debug/debug.h */
+#if defined(debug_assert_bound_2d)
+#undef debug_assert_bound_2d
+#endif
+
+/* mlkem/debug/debug.h */
+#if defined(debug_assert_bound_2d)
+#undef debug_assert_bound_2d
+#endif
+
+/* mlkem/debug/debug.h */
+#if defined(debug_assert_bound_2d)
+#undef debug_assert_bound_2d
+#endif
+
 /* mlkem/debug/debug.h */
 #if defined(mlkem_debug_assert)
 #undef mlkem_debug_assert

Diff for: mlkem/cbmc.h

@@ -119,13 +119,13 @@
   {                                                                    \
     unsigned qvar;                                                     \
     ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                    \
-        (((value_lb) <= (array_var[(qvar)])) &&                        \
-        ((array_var[(qvar)]) < (value_ub)))                            \
+        (((value_lb) <= ((array_var)[(qvar)])) &&		       \
+         (((array_var)[(qvar)]) < (value_ub)))			       \
   }
 
 #define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \
   array_bound_core(CBMC_CONCAT(_cbmc_idx, __LINE__), (qvar_lb),      \
-                   (qvar_ub), (array_var), (value_lb), (value_ub))
+      (qvar_ub), (array_var), (value_lb), (value_ub))
 /* clang-format on */
 
 /* Wrapper around array_bound operating on absolute values.

Diff for: mlkem/debug/debug.h

@@ -50,24 +50,17 @@ void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr,
  *
  * val: Value that's asserted to be non-zero
  */
-#define debug_assert(val)                          \
-  do                                               \
-  {                                                \
-    mlkem_debug_assert(__FILE__, __LINE__, (val)); \
-  } while (0)
+#define debug_assert(val) mlkem_debug_assert(__FILE__, __LINE__, (val))
 
 /* Check bounds in array of int16_t's
  * ptr: Base of int16_t array; will be explicitly cast to int16_t*,
  *      so you may pass a byte-compatible type such as poly or polyvec.
  * len: Number of int16_t in array
  * value_lb: Inclusive lower value bound
  * value_ub: Exclusive upper value bound */
-#define debug_assert_bound(ptr, len, value_lb, value_ub)                 \
-  do                                                                     \
-  {                                                                      \
-    mlkem_debug_check_bounds(__FILE__, __LINE__, (const int16_t *)(ptr), \
-                             (len), (value_lb)-1, (value_ub));           \
-  } while (0)
+#define debug_assert_bound(ptr, len, value_lb, value_ub)                      \
+  mlkem_debug_check_bounds(__FILE__, __LINE__, (const int16_t *)(ptr), (len), \
+                           (value_lb)-1, (value_ub))
 
 /* Check absolute bounds in array of int16_t's
  * ptr: Base of array, expression of type int16_t*
@@ -76,6 +69,38 @@ void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr,
 #define debug_assert_abs_bound(ptr, len, value_abs_bd) \
   debug_assert_bound((ptr), (len), (-(value_abs_bd) + 1), (value_abs_bd))
 
+/* Version of bounds assertions for 2-dimensional arrays */
+#define debug_assert_bound_2d(ptr, len0, len1, value_lb, value_ub) \
+  debug_assert_bound((ptr), ((len0) * (len1)), (value_lb), (value_ub))
+
+#define debug_assert_abs_bound_2d(ptr, len0, len1, value_abs_bd) \
+  debug_assert_abs_bound((ptr), ((len0) * (len1)), (value_abs_bd))
+
+/* When running CBMC, convert debug assertions into proof obligations */
+#elif defined(CBMC)
+
+#include "../cbmc.h"
+
+#define debug_assert(val) cassert(val)
+
+#define debug_assert_bound(ptr, len, value_lb, value_ub) \
+  cassert(array_bound(((int16_t *)(ptr)), 0, (len), (value_lb), (value_ub)))
+
+#define debug_assert_abs_bound(ptr, len, value_abs_bd) \
+  cassert(array_abs_bound(((int16_t *)(ptr)), 0, (len), (value_abs_bd)))
+
+/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
+ * just use a single flattened array_bound(...) here. */
+#define debug_assert_bound_2d(ptr, N, M, value_lb, value_ub)           \
+  cassert(forall(kN, 0, (M),                                           \
+                 array_bound(&((int16_t(*)[(N)])(ptr))[kN][0], 0, (N), \
+                             (value_lb), (value_ub))))
+
+#define debug_assert_abs_bound_2d(ptr, N, M, value_abs_bd)                 \
+  cassert(forall(kN, 0, (M),                                               \
+                 array_abs_bound(&((int16_t(*)[(N)])(ptr))[kN][0], 0, (N), \
+                                 (value_abs_bd))))
+
 #else /* MLKEM_DEBUG */
 
 #define debug_assert(val) \
@@ -91,6 +116,17 @@ void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr,
   {                                                    \
   } while (0)
 
+#define debug_assert_bound_2d(ptr, len0, len1, value_lb, value_ub) \
+  do                                                               \
+  {                                                                \
+  } while (0)
+
+#define debug_assert_abs_bound_2d(ptr, len0, len1, value_abs_bd) \
+  do                                                             \
+  {                                                              \
+  } while (0)
+
+
 #endif /* MLKEM_DEBUG */
 
 #endif /* MLKEM_DEBUG_H */

Diff for: mlkem/indcpa.c

@@ -51,7 +51,7 @@
 static void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk,
                     const uint8_t seed[MLKEM_SYMBYTES])
 {
-  debug_assert_abs_bound(pk, MLKEM_K * MLKEM_N, MLKEM_Q);
+  debug_assert_bound_2d(pk, MLKEM_N, MLKEM_K, 0, MLKEM_Q);
   polyvec_tobytes(r, pk);
   memcpy(r + MLKEM_POLYVECBYTES, seed, MLKEM_SYMBYTES);
 }
@@ -91,7 +91,7 @@ static void unpack_pk(polyvec *pk, uint8_t seed[MLKEM_SYMBYTES],
  **************************************************/
 static void pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], polyvec *sk)
 {
-  debug_assert_abs_bound(sk, MLKEM_K * MLKEM_N, MLKEM_Q);
+  debug_assert_bound_2d(sk, MLKEM_N, MLKEM_K, 0, MLKEM_Q);
   polyvec_tobytes(r, sk);
 }
 
@@ -354,7 +354,7 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed)
     i++;
   }
 
-  cassert(i == MLKEM_K * MLKEM_K);
+  debug_assert(i == MLKEM_K * MLKEM_K);
 
   /*
    * The public matrix is generated in NTT domain. If the native backend

Diff for: mlkem/poly.c

@@ -20,6 +20,8 @@ MLKEM_NATIVE_INTERNAL_API
 void poly_compress_du(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DU], const poly *a)
 {
   unsigned j;
+  debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
+
 #if (MLKEM_POLYCOMPRESSEDBYTES_DU == 352)
   for (j = 0; j < MLKEM_N / 8; j++)
   __loop__(invariant(j >= 0 && j <= MLKEM_N / 8))
@@ -139,6 +141,8 @@ void poly_decompress_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU])
 #else
 #error "MLKEM_POLYCOMPRESSEDBYTES_DU needs to be in {320,352}"
 #endif
+
+  debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q);
 }
 
 MLKEM_NATIVE_INTERNAL_API
@@ -260,7 +264,6 @@ void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a)
   unsigned i;
   debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
 
-
   for (i = 0; i < MLKEM_N / 2; i++)
   __loop__(invariant(i >= 0 && i <= MLKEM_N / 2))
   {
@@ -489,7 +492,7 @@ void poly_tomont(poly *r)
   for (i = 0; i < MLKEM_N; i++)
   __loop__(
     invariant(i >= 0 && i <= MLKEM_N)
-    invariant(array_abs_bound(r->coeffs ,0, i, MLKEM_Q)))
+    invariant(array_abs_bound(r->coeffs, 0, i, MLKEM_Q)))
   {
     r->coeffs[i] = fqmul(r->coeffs[i], f);
   }
@@ -566,11 +569,20 @@ void poly_mulcache_compute(poly_mulcache *x, const poly *a)
 {
   unsigned i;
   for (i = 0; i < MLKEM_N / 4; i++)
-  __loop__(invariant(i >= 0 && i <= MLKEM_N / 4))
+  __loop__(
+    invariant(i >= 0 && i <= MLKEM_N / 4)
+    invariant(array_abs_bound(x->coeffs, 0, 2 * i, MLKEM_Q)))
   {
     x->coeffs[2 * i + 0] = fqmul(a->coeffs[4 * i + 1], zetas[64 + i]);
     x->coeffs[2 * i + 1] = fqmul(a->coeffs[4 * i + 3], -zetas[64 + i]);
   }
+
+  /*
+   * This bound is true for the C implementation, but not needed
+   * in the higher level bounds reasoning. It is thus omitted
+   * them from the spec to not unnecessarily constrain native
+   * implementations, but checked here nonetheless.
+   */
   debug_assert_abs_bound(x, MLKEM_N / 2, MLKEM_Q);
 }
 #else  /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */

Diff for: mlkem/poly.h

@@ -307,17 +307,17 @@ __contract__(
  ************************************************************/
 static INLINE uint16_t scalar_signed_to_unsigned_q(int16_t c)
 __contract__(
-  requires(c >= -(MLKEM_Q - 1) && c <= (MLKEM_Q - 1))
-  ensures(return_value >= 0 && return_value <= (MLKEM_Q - 1))
+  requires(c > -MLKEM_Q && c < MLKEM_Q)
+  ensures(return_value >= 0 && return_value < MLKEM_Q)
   ensures(return_value == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q)))
 {
+  debug_assert_abs_bound(&c, 1, MLKEM_Q);
+
   /* Add Q if c is negative, but in constant time */
   c = ct_sel_int16(c + MLKEM_Q, c, ct_cmask_neg_i16(c));
 
-  cassert(c >= 0);
-  cassert(c < MLKEM_Q);
-
   /* and therefore cast to uint16_t is safe. */
+  debug_assert_bound(&c, 1, 0, MLKEM_Q);
   return (uint16_t)c;
 }
 

Diff for: mlkem/polyvec.c

@@ -15,7 +15,7 @@ void polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU],
                          const polyvec *a)
 {
   unsigned i;
-  debug_assert_bound(a, MLKEM_K * MLKEM_N, 0, MLKEM_Q);
+  debug_assert_bound_2d(a, MLKEM_N, MLKEM_K, 0, MLKEM_Q);
 
   for (i = 0; i < MLKEM_K; i++)
   {
@@ -33,13 +33,15 @@ void polyvec_decompress_du(polyvec *r,
     poly_decompress_du(&r->vec[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU);
   }
 
-  debug_assert_bound(r, MLKEM_K * MLKEM_N, 0, MLKEM_Q);
+  debug_assert_bound_2d(r, MLKEM_N, MLKEM_K, 0, MLKEM_Q);
 }
 
 MLKEM_NATIVE_INTERNAL_API
 void polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const polyvec *a)
 {
   unsigned i;
+  debug_assert_bound_2d(a, MLKEM_N, MLKEM_K, 0, MLKEM_Q);
+
   for (i = 0; i < MLKEM_K; i++)
   {
     poly_tobytes(r + i * MLKEM_POLYBYTES, &a->vec[i]);
@@ -54,6 +56,8 @@ void polyvec_frombytes(polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES])
   {
     poly_frombytes(&r->vec[i], a + i * MLKEM_POLYBYTES);
   }
+
+  debug_assert_bound_2d(r, MLKEM_N, MLKEM_K, 0, UINT12_LIMIT);
 }
 
 MLKEM_NATIVE_INTERNAL_API
@@ -64,6 +68,8 @@ void polyvec_ntt(polyvec *r)
   {
     poly_ntt(&r->vec[i]);
   }
+
+  debug_assert_abs_bound_2d(r, MLKEM_N, MLKEM_K, NTT_BOUND);
 }
 
 MLKEM_NATIVE_INTERNAL_API
@@ -74,6 +80,8 @@ void polyvec_invntt_tomont(polyvec *r)
   {
     poly_invntt_tomont(&r->vec[i]);
   }
+
+  debug_assert_abs_bound_2d(r, MLKEM_N, MLKEM_K, INVNTT_BOUND);
 }
 
 #if !defined(MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED)
@@ -84,27 +92,22 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
 {
   unsigned i;
   poly t;
-
-  debug_assert_bound(a, MLKEM_K * MLKEM_N, 0, UINT12_LIMIT);
-  debug_assert_abs_bound(b, MLKEM_K * MLKEM_N, NTT_BOUND);
-  debug_assert_abs_bound(b_cache, MLKEM_K * (MLKEM_N / 2), MLKEM_Q);
+  debug_assert_bound_2d(a, MLKEM_N, MLKEM_K, 0, UINT12_LIMIT);
 
   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, &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.
+   * This bound is true for the C implementation, but not needed
+   * in the higher level bounds reasoning. It is thus omitted
+   * them from the spec to not unnecessarily constrain native
+   * implementations, but checked here nonetheless.
    */
-  cassert(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_K * 2 * MLKEM_Q));
-  /* TODO: Integrate CBMC assertion into debug_asserts if CBMC is set */
   debug_assert_abs_bound(r, MLKEM_N, MLKEM_K * 2 * MLKEM_Q);
 }
 #else  /* !MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */
@@ -113,8 +116,7 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
                                            const polyvec *b,
                                            const polyvec_mulcache *b_cache)
 {
-  debug_assert_bound(a, MLKEM_K * MLKEM_N, 0, UINT12_LIMIT);
-  debug_assert_abs_bound(b, MLKEM_K * MLKEM_N, NTT_BOUND);
+  debug_assert_bound_2d(a, MLKEM_N, MLKEM_K, 0, UINT12_LIMIT);
   /* Omitting bounds assertion for cache since native implementations may
    * decide not to use a mulcache. Note that the C backend implementation
    * of poly_basemul_montgomery_cached() does still include the check. */
@@ -148,6 +150,8 @@ void polyvec_reduce(polyvec *r)
   {
     poly_reduce(&r->vec[i]);
   }
+
+  debug_assert_bound_2d(r, MLKEM_N, MLKEM_K, 0, MLKEM_Q);
 }
 
 MLKEM_NATIVE_INTERNAL_API
@@ -168,4 +172,6 @@ void polyvec_tomont(polyvec *r)
   {
     poly_tomont(&r->vec[i]);
   }
+
+  debug_assert_abs_bound_2d(r, MLKEM_N, MLKEM_K, MLKEM_Q);
 }