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]>

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

@@ -6,6 +6,7 @@
 #include <string.h>
 
 #include "common.h"
+#include "debug.h"
 #include "poly.h"
 #include "polyvec.h"
 
@@ -270,20 +271,20 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
     }
 
     /* 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));
+    mld_assert(j == MLDSA_L);
+    mld_assert(t >= -(int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1));
+    mld_assert(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);
+    mld_assert(t >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX);
+    mld_assert(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);
+    mld_assert(r > -MLDSA_Q);
+    mld_assert(r < MLDSA_Q);
     w->coeffs[i] = r;
   }
 }

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 */