Skip to content

Consistently use mld_assert instead of cassert #365

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
+13 −31
Open

Consistently use mld_assert instead of cassert #365

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
21001e3
Consistently use mld_assert instead of cassert
mkannwischer Jul 15, 2025
4b6feba
Remove unnecessary weak spec for mld_montgomery_reduce()
hanno-becker Jul 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions mldsa/fips202/fips202.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,6 @@ __contract__(
{
s[i] = 0;
}

cassert(forall(k, 0, MLD_KECCAK_LANES, s[k] == 0));
}

/*************************************************
Expand Down
14 changes: 0 additions & 14 deletions mldsa/polyvec.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
}
Expand Down
4 changes: 3 additions & 1 deletion mldsa/reduce.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
*/
#include <stdint.h>

#include "debug.h"
#include "reduce.h"

/*************************************************
Expand Down Expand Up @@ -65,7 +66,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;
}

Expand Down
8 changes: 2 additions & 6 deletions mldsa/reduce.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,12 +48,8 @@
**************************************************/
int32_t mld_montgomery_reduce(int64_t a)
__contract__(
requires(a >= -MONTGOMERY_REDUCE_DOMAIN_MAX && a <= MONTGOMERY_REDUCE_DOMAIN_MAX)
ensures(return_value >= INT32_MIN && return_value < REDUCE32_DOMAIN_MAX)

/* Special case - for stronger input bounds, we can ensure stronger bounds on the output */
ensures((a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX) ==>
(return_value > -MLDSA_Q && return_value < MLDSA_Q))
requires(a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX)
ensures(return_value > -MLDSA_Q && return_value < MLDSA_Q)
);

#define mld_reduce32 MLD_NAMESPACE(reduce32)
Expand Down
11 changes: 6 additions & 5 deletions mldsa/rounding.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
*/
#include <stdint.h>

#include "debug.h"
#include "rounding.h"


Expand All @@ -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);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here

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

Expand Down
5 changes: 2 additions & 3 deletions mldsa/sign.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
#include <string.h>

#include "cbmc.h"
#include "debug.h"
#include "fips202/fips202.h"
#include "packing.h"
#include "poly.h"
Expand Down Expand Up @@ -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 */
Expand Down