Consistently use mld_assert instead of cassert

cassert turns into a CBMC proof assertion inside of CBMC proofs, but it
turns into a no-op otherwise.
mld_assert behaves the save inside of CBMC proofs, but also turns into a
run-time assertion in debug builds.

Signed-off-by: Matthias J. Kannwischer <[email protected]>
Signed-off-by: Hanno Becker <[email protected]>

Author: mkannwischer

mldsa/fips202/fips202.c

@@ -93,8 +93,6 @@ __contract__(
   {
     s[i] = 0;
   }
-
-  cassert(forall(k, 0, MLD_KECCAK_LANES, s[k] == 0));
 }
 
 /*************************************************

mldsa/polyvec.c

@@ -269,21 +269,7 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
       t += (int64_t)u->vec[j].coeffs[i] * v->vec[j].coeffs[i];
     }
 
-    /* Substitute j == MLSDA_L into the loop invariant to get... */
-    cassert(j == MLDSA_L);
-    cassert(t >= -(int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1));
-    cassert(t <= (int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1));
-
-    /* ...and therefore... */
-    cassert(t >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX);
-    cassert(t < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX);
-
-    /* ...which meets the "strong" case of mld_montgomery_reduce() */
     r = mld_montgomery_reduce(t);
-
-    /* ...and therefore we can assert a stronger bound on r */
-    cassert(r > -MLDSA_Q);
-    cassert(r < MLDSA_Q);
     w->coeffs[i] = r;
   }
 }

mldsa/reduce.c

@@ -65,7 +65,8 @@ int32_t mld_reduce32(int32_t a)
 
   t = (a + (1 << 22)) >> 23;
   t = a - t * MLDSA_Q;
-  cassert((t - a) % MLDSA_Q == 0);
+
+  mld_assert((t - a) % MLDSA_Q == 0);
   return t;
 }
 

mldsa/rounding.c

@@ -4,6 +4,7 @@
  */
 #include <stdint.h>
 
+#include "debug.h"
 #include "rounding.h"
 
 
@@ -17,20 +18,20 @@ void mld_decompose(int32_t *a0, int32_t *a1, int32_t a)
 {
   *a1 = (a + 127) >> 7;
   /* We know a >= 0 and a < MLDSA_Q, so... */
-  cassert(*a1 >= 0 && *a1 <= 65472);
+  mld_assert(*a1 >= 0 && *a1 <= 65472);
 
 #if MLDSA_MODE == 2
   *a1 = (*a1 * 11275 + (1 << 23)) >> 24;
-  cassert(*a1 >= 0 && *a1 <= 44);
+  mld_assert(*a1 >= 0 && *a1 <= 44);
 
   *a1 ^= ((43 - *a1) >> 31) & *a1;
-  cassert(*a1 >= 0 && *a1 <= 43);
+  mld_assert(*a1 >= 0 && *a1 <= 43);
 #else /* MLDSA_MODE == 2 */
   *a1 = (*a1 * 1025 + (1 << 21)) >> 22;
-  cassert(*a1 >= 0 && *a1 <= 16);
+  mld_assert(*a1 >= 0 && *a1 <= 16);
 
   *a1 &= 15;
-  cassert(*a1 >= 0 && *a1 <= 15);
+  mld_assert(*a1 >= 0 && *a1 <= 15);
 
 #endif /* MLDSA_MODE != 2 */
 

mldsa/sign.c

@@ -6,6 +6,7 @@
 #include <string.h>
 
 #include "cbmc.h"
+#include "debug.h"
 #include "fips202/fips202.h"
 #include "packing.h"
 #include "poly.h"
@@ -252,9 +253,7 @@ __contract__(
   /* If z is valid, then its coefficients are bounded by  */
   /* MLDSA_GAMMA1 - MLDSA_BETA. This will be needed below */
   /* to prove the pre-condition of pack_sig()             */
-  cassert(forall(k1, 0, MLDSA_L,
-                 array_abs_bound(z.vec[k1].coeffs, 0, MLDSA_N,
-                                 (MLDSA_GAMMA1 - MLDSA_BETA))));
+  mld_assert_abs_bound_2d(z.vec, MLDSA_L, MLDSA_N, (MLDSA_GAMMA1 - MLDSA_BETA));
 
   /* Check that subtracting cs2 does not change high bits of w and low bits
    * do not reveal secret information */