Skip to content

Add debug assertions for reduce.c and polyvec.c #416

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 6 commits into
base: main
Choose a base branch
from
Open

Add debug assertions for reduce.c and polyvec.c #416

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
5969e6e
Debug: Add bounds assertions in poly.c
willieyz Aug 7, 2025
40c070d
fix: fix the overflow problem for the exclusive lower bound
willieyz Aug 7, 2025
d19414d
Debug: Add bounds assertions in polyvec.c
willieyz Sep 22, 2025
5b04600
Change MLD_INTT_BOUND to (MLDSA_Q * 3 / 4)
willieyz Sep 22, 2025
9661916
wip: test with ((MLDSA_Q - 83787) + 1) as MLD_INTT_BOUND
willieyz Sep 22, 2025
932b260
wip: test with MLDSA_Q as MLD_INTT_BOUND
willieyz Sep 22, 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
17 changes: 9 additions & 8 deletions mldsa/debug.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@

#if defined(MLDSA_DEBUG)

#include <inttypes.h>
#include <stdio.h>
#include <stdlib.h>
#include "debug.h"
Expand All @@ -27,8 +28,8 @@ void mld_debug_check_assert(const char *file, int line, const int val)
}

void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
unsigned len, int lower_bound_exclusive,
int upper_bound_exclusive)
unsigned len, int64_t lower_bound_exclusive,
int64_t upper_bound_exclusive)
{
int err = 0;
unsigned i;
Expand All @@ -37,12 +38,12 @@ void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
int32_t val = ptr[i];
if (!(val > lower_bound_exclusive && val < upper_bound_exclusive))
{
fprintf(
stderr,
MLD_DEBUG_ERROR_HEADER
"Bounds assertion failed: Index %u, value %d out of bounds (%d,%d)\n",
file, line, i, (int)val, lower_bound_exclusive,
upper_bound_exclusive);
fprintf(stderr,
MLD_DEBUG_ERROR_HEADER
"Bounds assertion failed: Index %u, value %d out of bounds "
"(%" PRId64 ",%" PRId64 ")\n",
file, line, i, (int)val, lower_bound_exclusive,
upper_bound_exclusive);
err = 1;
}
}
Expand Down
11 changes: 6 additions & 5 deletions mldsa/debug.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,8 @@ void mld_debug_check_assert(const char *file, int line, const int val);
**************************************************/
#define mld_debug_check_bounds MLD_NAMESPACE(mldsa_debug_check_bounds)
void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
unsigned len, int lower_bound_exclusive,
int upper_bound_exclusive);
unsigned len, int64_t lower_bound_exclusive,
int64_t upper_bound_exclusive);

/* Check assertion, calling exit() upon failure
*
Expand All @@ -60,14 +60,15 @@ void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
* value_ub: Exclusive upper value bound */
#define mld_assert_bound(ptr, len, value_lb, value_ub) \
mld_debug_check_bounds(__FILE__, __LINE__, (const int32_t *)(ptr), (len), \
(value_lb) - 1, (value_ub))
((int64_t)(value_lb)) - 1, (value_ub))

/* Check absolute bounds in array of int32_t's
* ptr: Base of array, expression of type int32_t*
* len: Number of int32_t in array
* value_abs_bd: Exclusive absolute upper bound */
#define mld_assert_abs_bound(ptr, len, value_abs_bd) \
mld_assert_bound((ptr), (len), (-(value_abs_bd) + 1), (value_abs_bd))
#define mld_assert_abs_bound(ptr, len, value_abs_bd) \
mld_assert_bound((ptr), (len), (-((int64_t)(value_abs_bd)) + 1), \
(value_abs_bd))

/* Version of bounds assertions for 2-dimensional arrays */
#define mld_assert_bound_2d(ptr, len0, len1, value_lb, value_ub) \
Expand Down
2 changes: 1 addition & 1 deletion mldsa/ntt.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
/* Absolute exclusive upper bound for the output of the forward NTT */
#define MLD_NTT_BOUND (9 * MLDSA_Q)
/* Absolute exclusive upper bound for the output of the inverse NTT*/
#define MLD_INTT_BOUND 4211139
#define MLD_INTT_BOUND MLDSA_Q

#define mld_ntt MLD_NAMESPACE(ntt)
/*************************************************
Expand Down
45 changes: 39 additions & 6 deletions mldsa/poly.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,7 @@
void mld_poly_reduce(mld_poly *a)
{
unsigned int i;
/* TODO: Introduce the following after using inclusive lower bounds in
* the underlying debug function mld_debug_check_bounds(). */
/* mld_assert_bound(a->coeffs, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX); */
mld_assert_bound(a->coeffs, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX);

for (i = 0; i < MLDSA_N; ++i)
__loop__(
Expand Down Expand Up @@ -74,6 +72,8 @@ void mld_poly_add(mld_poly *r, const mld_poly *b)
void mld_poly_sub(mld_poly *r, const mld_poly *b)
{
unsigned int i;
mld_assert_abs_bound(b->coeffs, MLDSA_N, MLDSA_Q);
mld_assert_abs_bound(r->coeffs, MLDSA_N, MLDSA_Q);

for (i = 0; i < MLDSA_N; ++i)
__loop__(
Expand All @@ -84,6 +84,8 @@ void mld_poly_sub(mld_poly *r, const mld_poly *b)
{
r->coeffs[i] = r->coeffs[i] - b->coeffs[i];
}

mld_assert_bound(r->coeffs, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX);
}

void mld_poly_shiftl(mld_poly *a)
Expand All @@ -102,6 +104,7 @@ void mld_poly_shiftl(mld_poly *a)
*/
a->coeffs[i] *= (1 << MLDSA_D);
}
mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
}

#if !defined(MLD_USE_NATIVE_NTT)
Expand Down Expand Up @@ -132,7 +135,7 @@ void mld_poly_invntt_tomont(mld_poly *a)
{
mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
mld_intt_native(a->coeffs);
mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND);
}
#endif /* MLD_USE_NATIVE_INTT */

Expand All @@ -141,6 +144,9 @@ void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a,
{
unsigned int i;

mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
mld_assert_abs_bound(b->coeffs, MLDSA_N, MLD_NTT_BOUND);

for (i = 0; i < MLDSA_N; ++i)
__loop__(
invariant(i <= MLDSA_N)
Expand All @@ -149,6 +155,8 @@ void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a,
{
c->coeffs[i] = mld_montgomery_reduce((int64_t)a->coeffs[i] * b->coeffs[i]);
}

mld_assert_abs_bound(c->coeffs, MLDSA_N, MLDSA_Q);
}

void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a)
Expand Down Expand Up @@ -210,6 +218,7 @@ unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0,
}

mld_assert(s <= MLDSA_N);
mld_assert_bound(h->coeffs, MLDSA_N, 0, 2);
return s;
}

Expand Down Expand Up @@ -306,6 +315,7 @@ __contract__(
{
unsigned int ctr, pos;
uint32_t t;
mld_assert_bound(a, offset, 0, MLDSA_Q);

/* TODO: CBMC proof based on mld_rej_uniform_native */
#if defined(MLD_USE_NATIVE_REJ_UNIFORM)
Expand Down Expand Up @@ -341,6 +351,8 @@ __contract__(
}
}

mld_assert_bound(a, ctr, 0, MLDSA_Q);

return ctr;
}

Expand Down Expand Up @@ -376,6 +388,7 @@ void mld_poly_uniform(mld_poly *a, const uint8_t seed[MLDSA_SEEDBYTES + 2])
ctr = mld_rej_uniform(a->coeffs, MLDSA_N, ctr, buf, buflen);
}
mld_xof128_release(&state);
mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);

/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
mld_zeroize(buf, sizeof(buf));
Expand Down Expand Up @@ -435,6 +448,11 @@ void mld_poly_uniform_4x(mld_poly *vec0, mld_poly *vec1, mld_poly *vec2,
}
mld_xof128_x4_release(&state);

mld_assert_bound(vec0->coeffs, MLDSA_N, 0, MLDSA_Q);
mld_assert_bound(vec1->coeffs, MLDSA_N, 0, MLDSA_Q);
mld_assert_bound(vec2->coeffs, MLDSA_N, 0, MLDSA_Q);
mld_assert_bound(vec3->coeffs, MLDSA_N, 0, MLDSA_Q);

/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
mld_zeroize(buf, sizeof(buf));
}
Expand Down Expand Up @@ -496,6 +514,7 @@ __contract__(
unsigned int ctr, pos;
int t_valid;
uint32_t t0, t1;
mld_assert_abs_bound(a, offset, MLDSA_ETA + 1);

/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */
#if MLDSA_ETA == 2 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2)
Expand Down Expand Up @@ -573,6 +592,8 @@ __contract__(
#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */
}

mld_assert_abs_bound(a, ctr, MLDSA_ETA + 1);

return ctr;
}

Expand Down Expand Up @@ -649,6 +670,11 @@ void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,

mld_xof256_x4_release(&state);

mld_assert_abs_bound(r0->coeffs, MLDSA_N, MLDSA_ETA + 1);
mld_assert_abs_bound(r1->coeffs, MLDSA_N, MLDSA_ETA + 1);
mld_assert_abs_bound(r2->coeffs, MLDSA_N, MLDSA_ETA + 1);
mld_assert_abs_bound(r3->coeffs, MLDSA_N, MLDSA_ETA + 1);

/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
mld_zeroize(buf, sizeof(buf));
mld_zeroize(extseed, sizeof(extseed));
Expand Down Expand Up @@ -676,6 +702,8 @@ void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES],

mld_xof256_release(&state);

mld_assert_bound(a->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);

/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
mld_zeroize(buf, sizeof(buf));
mld_zeroize(extseed, sizeof(extseed));
Expand Down Expand Up @@ -719,6 +747,11 @@ void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
mld_polyz_unpack(r3, buf[3]);
mld_xof256_x4_release(&state);

mld_assert_bound(r0->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);
mld_assert_bound(r1->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);
mld_assert_bound(r2->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);
mld_assert_bound(r3->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);

/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
mld_zeroize(buf, sizeof(buf));
mld_zeroize(extseed, sizeof(extseed));
Expand Down Expand Up @@ -796,11 +829,11 @@ void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES])
signs >>= 1;
}

mld_assert_bound(c->coeffs, MLDSA_N, -1, 2);

/* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
mld_zeroize(buf, sizeof(buf));
mld_zeroize(&signs, sizeof(signs));

mld_assert_bound(c->coeffs, MLDSA_N, -1, 2);
}

void mld_polyeta_pack(uint8_t *r, const mld_poly *a)
Expand Down
Loading
Loading