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

willieyz · 2025-08-07T11:48:27Z

Resolves Add debug assertions for reduce.c and polyvec.c #216
All implementations of functions in poly.c, polyvec.c have bounds assertions
for inputs and outputs added that match the CBMC specifications.
As for mlkem-native, if CBMC is enabled, the bounds assertions
are interpreted as CBMC proof obligations.

- This commit is ported from mlkem PR #214 - All implementations of functions in poly.c have bounds assertions for inputs and outputs added that match the CBMC specifications. Signed-off-by: willieyz <[email protected]>

mkannwischer

Thanks @willieyz. This is a nice addition!
There are still quite a few things that could be improved.

mkannwischer · 2025-08-13T05:39:13Z

mldsa/polyvec.c

@@ -384,11 +421,15 @@ void mld_polyveck_sub(mld_polyveck *u, const mld_polyveck *v)
  {
    mld_poly_sub(&u->vec[i], &v->vec[i]);
  }
+
+  mld_assert_bound_2d(u->vec, MLDSA_K, MLDSA_N, (int64_t)INT32_MIN,


This cast should not be needed.

mkannwischer · 2025-08-13T05:39:39Z

mldsa/polyvec.c

 }

 void mld_polyvecl_reduce(mld_polyvecl *v)
 {
  unsigned int i;
+  mld_assert_bound_2d(v->vec, MLDSA_L, MLDSA_N, (int64_t)INT32_MIN,


This cast should not be needed.

mkannwischer · 2025-08-13T05:42:50Z

mldsa/poly.c

@@ -74,6 +74,8 @@ void mld_poly_add(mld_poly *r, const mld_poly *b)
 void mld_poly_sub(mld_poly *r, const mld_poly *b)


Did you miss mld_poly_add or was that intentionally skipped?

@mkannwischer , I leave this intentionally, because there is no any array_bound or array_abs_bound post-condition in the contract of mld_poly_add.
It do have some post-condition, but none of those are array_bound and array_abs_bound.
or should I add assertion for it according to those?

mkannwischer · 2025-08-13T05:47:07Z

mldsa/poly.c

@@ -379,6 +393,8 @@ void mld_poly_uniform(mld_poly *a, const uint8_t seed[MLDSA_SEEDBYTES + 2])

  /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */
  mld_zeroize(buf, sizeof(buf));
+
+  mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);


Can we have all assertions before the zeroize call please? Just to be consistent with mlkem-native that zeroize is the last step in the function.

Fixed, Thank you for your reviewing!

mkannwischer · 2025-08-13T05:51:17Z

mldsa/poly.c

@@ -84,6 +86,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, (int64_t)INT32_MIN, REDUCE32_DOMAIN_MAX);


This cast should not be needed

mkannwischer · 2025-08-13T05:57:07Z

mldsa/polyvec.c

 }

 void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
                                           const mld_polyvecl *v)
 {
  unsigned int i, j;
+  mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);


isn't this missing a pre-condition on v?

Yes, sorry about the miss..
I had fixed it now, thank you for your reviewing!

mkannwischer · 2025-08-13T06:00:11Z

mldsa/polyvec.c

@@ -372,6 +407,8 @@ void mld_polyveck_add(mld_polyveck *u, const mld_polyveck *v)
 void mld_polyveck_sub(mld_polyveck *u, const mld_polyveck *v)


mld_polyveck_add can have a post-condition in the contract - just like mld_polyvecl_add. That should be added and also be asserted.

Added, thank you for your reviewing!

mkannwischer · 2025-08-13T06:01:21Z

mldsa/polyvec.c

@@ -431,12 +477,15 @@ void mld_polyveck_invntt_tomont(mld_polyveck *v)
  {
    mld_poly_invntt_tomont(&v->vec[i]);
  }
+
+  mld_assert_abs_bound_2d(v->vec, MLDSA_K, MLDSA_N, MLD_NTT_BOUND);


This should be INTT_BOUND.

mkannwischer · 2025-08-13T06:09:32Z

mldsa/poly.c

Can the assertion for mld_poly_reduce now be added?

mkannwischer · 2025-08-13T06:12:14Z

mldsa/poly.c

@@ -141,6 +146,9 @@ void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a,
 {


mld_poly_invntt_tomont should have an MLD_INTT_BOUND output bound.

Signed-off-by: willieyz <[email protected]>

- This commit is ported from mlkem PR #214 - All implementations of functions in polyvec.c have bounds assertions for inputs and outputs added that match the CBMC specifications. Signed-off-by: willieyz <[email protected]>

…test error Signed-off-by: willieyz <[email protected]>

Signed-off-by: willieyz <[email protected]>

willieyz force-pushed the cbmc-bound-assertions branch 7 times, most recently from 6ed6054 to 407a414 Compare August 8, 2025 02:39

Debug: Add bounds assertions in poly.c

6738b4b

- This commit is ported from mlkem PR #214 - All implementations of functions in poly.c have bounds assertions for inputs and outputs added that match the CBMC specifications. Signed-off-by: willieyz <[email protected]>

willieyz force-pushed the cbmc-bound-assertions branch from 407a414 to a4cfae5 Compare August 8, 2025 04:02

willieyz changed the title ~~Debug: Add bounds assertions macros (port mlkem-native #214)~~ Debug: Add bounds assertions macros (port PR#214) Aug 8, 2025

willieyz changed the title ~~Debug: Add bounds assertions macros (port PR#214)~~ Add debug assertions for reduce.c and polyvec.c #216 Aug 8, 2025

willieyz force-pushed the cbmc-bound-assertions branch 5 times, most recently from b99b71f to 1a95672 Compare August 11, 2025 08:53

willieyz marked this pull request as ready for review August 11, 2025 09:19

willieyz requested a review from a team as a code owner August 11, 2025 09:19

mkannwischer requested changes Aug 13, 2025

View reviewed changes

willieyz marked this pull request as draft August 13, 2025 08:57

willieyz force-pushed the cbmc-bound-assertions branch 2 times, most recently from 8b12dbf to 7e05da5 Compare August 15, 2025 01:41

willieyz added 2 commits August 15, 2025 10:02

fix: fix the overflow problem for the exclusive lower bound

fc904dd

Signed-off-by: willieyz <[email protected]>

Debug: Add bounds assertions in polyvec.c

ca96114

- This commit is ported from mlkem PR #214 - All implementations of functions in polyvec.c have bounds assertions for inputs and outputs added that match the CBMC specifications. Signed-off-by: willieyz <[email protected]>

willieyz force-pushed the cbmc-bound-assertions branch from 7e05da5 to d36b82b Compare August 15, 2025 02:03

fix: change the MLD_INTT_BOUND to (3 * MLDSA_Q / 4), fix the debug …

2ed2e64

…test error Signed-off-by: willieyz <[email protected]>

willieyz force-pushed the cbmc-bound-assertions branch from d36b82b to 2ed2e64 Compare August 21, 2025 05:25

wip: test with 0.8 Q

f3858ea

Signed-off-by: willieyz <[email protected]>

willieyz force-pushed the cbmc-bound-assertions branch from 494c599 to f3858ea Compare August 22, 2025 07:10

wip: test with 0.9Q

d795846

Signed-off-by: willieyz <[email protected]>

wip: test with Q

f6884fb

Signed-off-by: willieyz <[email protected]>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

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

Uh oh!

willieyz commented Aug 7, 2025 •

edited

Loading

Uh oh!

mkannwischer left a comment

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

willieyz Aug 13, 2025

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

willieyz Aug 13, 2025 •

edited

Loading

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

willieyz Aug 13, 2025

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

willieyz Aug 13, 2025

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

mkannwischer Aug 13, 2025

Uh oh!

Uh oh!

		@@ -74,6 +74,8 @@ void mld_poly_add(mld_poly r, const mld_poly b)
		void mld_poly_sub(mld_poly r, const mld_poly b)

		@@ -372,6 +407,8 @@ void mld_polyveck_add(mld_polyveck u, const mld_polyveck v)
		void mld_polyveck_sub(mld_polyveck u, const mld_polyveck v)

		@@ -141,6 +146,9 @@ void mld_poly_pointwise_montgomery(mld_poly c, const mld_poly a,
		{

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

Are you sure you want to change the base?

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

Uh oh!

Conversation

willieyz commented Aug 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

willieyz Aug 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

willieyz commented Aug 7, 2025 •

edited

Loading

willieyz Aug 13, 2025 •

edited

Loading