From 169eace292de13e790c22a334cd76228df2cc3a9 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 30 Dec 2025 19:38:48 +0800 Subject: [PATCH 1/2] sign stack usage: compute z incrementally This commit reduces the stack usage of signing by computing z = y + s1*cp incrementally (one polynomial at a time) allowing to eliminate the polyvecl z (at to cost of a single poly z). The computation of z is moved into a separate function (compute_pack_z) to vastly speed up the CBMC proofs. De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM. Practically, the same buffer was used early in the function too. Here we instead introduce a new polyvecl buffer tmp, but that can be placed in a union together with w1. Unfortuantely, with the current struct workaround for diffblue/cbmc#8813, this results in an increase in stack space by L KB. This gets eliminated when MLD_CONFIG_REDUCE_RAM is set. Hoisted out from https://github.com/pq-code-package/mldsa-native/pull/791 Signed-off-by: Matthias J. Kannwischer --- mldsa/mldsa_native.S | 8 +- mldsa/mldsa_native.c | 8 +- mldsa/src/packing.c | 17 +- mldsa/src/packing.h | 41 +++-- mldsa/src/polyvec.c | 101 ----------- mldsa/src/polyvec.h | 115 ------------- mldsa/src/sign.c | 161 +++++++++++++----- .../attempt_signature_generation/Makefile | 8 +- .../Makefile | 26 ++- .../compute_pack_z/compute_pack_z_harness.c | 20 +++ .../cbmc/{pack_sig => pack_sig_c_h}/Makefile | 10 +- .../pack_sig_c_h_harness.c} | 3 +- .../{polyvecl_pack_z => pack_sig_z}/Makefile | 14 +- .../pack_sig_z_harness.c} | 9 +- proofs/cbmc/polyvecl_add/Makefile | 55 ------ .../cbmc/polyvecl_add/polyvecl_add_harness.c | 10 -- proofs/cbmc/polyvecl_invntt_tomont/Makefile | 55 ------ .../polyvecl_invntt_tomont_harness.c | 12 -- .../polyvecl_pack_z/polyvecl_pack_z_harness.c | 11 -- ...lyvecl_pointwise_poly_montgomery_harness.c | 11 -- proofs/cbmc/polyvecl_reduce/Makefile | 55 ------ 21 files changed, 225 insertions(+), 525 deletions(-) rename proofs/cbmc/{polyvecl_pointwise_poly_montgomery => compute_pack_z}/Makefile (72%) create mode 100644 proofs/cbmc/compute_pack_z/compute_pack_z_harness.c rename proofs/cbmc/{pack_sig => pack_sig_c_h}/Makefile (90%) rename proofs/cbmc/{pack_sig/pack_sig_harness.c => pack_sig_c_h/pack_sig_c_h_harness.c} (80%) rename proofs/cbmc/{polyvecl_pack_z => pack_sig_z}/Makefile (87%) rename proofs/cbmc/{polyvecl_reduce/polyvecl_reduce_harness.c => pack_sig_z/pack_sig_z_harness.c} (57%) delete mode 100644 proofs/cbmc/polyvecl_add/Makefile delete mode 100644 proofs/cbmc/polyvecl_add/polyvecl_add_harness.c delete mode 100644 proofs/cbmc/polyvecl_invntt_tomont/Makefile delete mode 100644 proofs/cbmc/polyvecl_invntt_tomont/polyvecl_invntt_tomont_harness.c delete mode 100644 proofs/cbmc/polyvecl_pack_z/polyvecl_pack_z_harness.c delete mode 100644 proofs/cbmc/polyvecl_pointwise_poly_montgomery/polyvecl_pointwise_poly_montgomery_harness.c delete mode 100644 proofs/cbmc/polyvecl_reduce/Makefile diff --git a/mldsa/mldsa_native.S b/mldsa/mldsa_native.S index 54e55c931..f4e08ebb3 100644 --- a/mldsa/mldsa_native.S +++ b/mldsa/mldsa_native.S @@ -223,7 +223,8 @@ /* mldsa/src/packing.h */ #undef MLD_PACKING_H #undef mld_pack_pk -#undef mld_pack_sig +#undef mld_pack_sig_c_h +#undef mld_pack_sig_z #undef mld_pack_sk #undef mld_unpack_pk #undef mld_unpack_sig @@ -298,15 +299,10 @@ #undef mld_polyveck_unpack_t0 #undef mld_polyveck_use_hint #undef mld_polyvecl -#undef mld_polyvecl_add #undef mld_polyvecl_chknorm -#undef mld_polyvecl_invntt_tomont #undef mld_polyvecl_ntt #undef mld_polyvecl_pack_eta -#undef mld_polyvecl_pack_z #undef mld_polyvecl_pointwise_acc_montgomery -#undef mld_polyvecl_pointwise_poly_montgomery -#undef mld_polyvecl_reduce #undef mld_polyvecl_uniform_gamma1 #undef mld_polyvecl_unpack_eta #undef mld_polyvecl_unpack_z diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 8047ff46e..0ba9bd82a 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -219,7 +219,8 @@ /* mldsa/src/packing.h */ #undef MLD_PACKING_H #undef mld_pack_pk -#undef mld_pack_sig +#undef mld_pack_sig_c_h +#undef mld_pack_sig_z #undef mld_pack_sk #undef mld_unpack_pk #undef mld_unpack_sig @@ -294,15 +295,10 @@ #undef mld_polyveck_unpack_t0 #undef mld_polyveck_use_hint #undef mld_polyvecl -#undef mld_polyvecl_add #undef mld_polyvecl_chknorm -#undef mld_polyvecl_invntt_tomont #undef mld_polyvecl_ntt #undef mld_polyvecl_pack_eta -#undef mld_polyvecl_pack_z #undef mld_polyvecl_pointwise_acc_montgomery -#undef mld_polyvecl_pointwise_poly_montgomery -#undef mld_polyvecl_reduce #undef mld_polyvecl_uniform_gamma1 #undef mld_polyvecl_unpack_eta #undef mld_polyvecl_unpack_z diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c index ab08fb6ea..26da27385 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -99,16 +99,16 @@ void mld_unpack_sk(uint8_t rho[MLDSA_SEEDBYTES], uint8_t tr[MLDSA_TRBYTES], } MLD_INTERNAL_API -void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES], - const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyvecl *z, - const mld_polyveck *h, const unsigned int number_of_hints) +void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES], + const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h, + const unsigned int number_of_hints) { unsigned int i, j, k; mld_memcpy(sig, c, MLDSA_CTILDEBYTES); sig += MLDSA_CTILDEBYTES; - mld_polyvecl_pack_z(sig, z); + /* skip z component - packed via mld_pack_sig_z */ sig += MLDSA_L * MLDSA_POLYZ_PACKEDBYTES; /* Encode hints h */ @@ -168,6 +168,15 @@ void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES], } } +MLD_INTERNAL_API +void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi, + unsigned i) +{ + sig += MLDSA_CTILDEBYTES; + sig += i * MLDSA_POLYZ_PACKEDBYTES; + mld_polyz_pack(sig, zi); +} + /************************************************* * Name: mld_unpack_hints * diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h index 1fdec836d..e00366889 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -69,16 +69,16 @@ __contract__( ); -#define mld_pack_sig MLD_NAMESPACE_KL(pack_sig) +#define mld_pack_sig_c_h MLD_NAMESPACE_KL(pack_sig_c_h) /************************************************* - * Name: mld_pack_sig + * Name: mld_pack_sig_c_h * - * Description: Bit-pack signature sig = (c, z, h). + * Description: Bit-pack c and h component of sig = (c, z, h). + * The z component is packed separately using mld_pack_sig_z. * * Arguments: - uint8_t sig[]: output byte array * - const uint8_t *c: pointer to challenge hash length * MLDSA_SEEDBYTES - * - const mld_polyvecl *z: pointer to vector z * - const mld_polyveck *h: pointer to hint vector h * - const unsigned int number_of_hints: total * hints in *h @@ -88,22 +88,43 @@ __contract__( * proof of type safety. **************************************************/ MLD_INTERNAL_API -void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES], - const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyvecl *z, - const mld_polyveck *h, const unsigned int number_of_hints) +void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES], + const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h, + const unsigned int number_of_hints) __contract__( requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) requires(memory_no_alias(c, MLDSA_CTILDEBYTES)) - requires(memory_no_alias(z, sizeof(mld_polyvecl))) requires(memory_no_alias(h, sizeof(mld_polyveck))) - requires(forall(k0, 0, MLDSA_L, - array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) requires(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) requires(number_of_hints <= MLDSA_OMEGA) assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) ); +#define mld_pack_sig_z MLD_NAMESPACE_KL(pack_sig_z) +/************************************************* + * Name: mld_pack_sig_z + * + * Description: Bit-pack single polynomial of z component of sig = (c, z, h). + * The c and h components are packed separately using + * mld_pack_sig_c_h. + * + * Arguments: - uint8_t sig[]: output byte array + * - const mld_poly *zi: pointer to a single polynomial in z + * - const unsigned int i: index of zi in vector z + * + **************************************************/ +MLD_INTERNAL_API +void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi, + unsigned i) +__contract__( + requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) + requires(memory_no_alias(zi, sizeof(mld_poly))) + requires(i < MLDSA_L) + requires(array_bound(zi->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) + assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) +); + #define mld_unpack_pk MLD_NAMESPACE_KL(unpack_pk) /************************************************* * Name: mld_unpack_pk diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index f6cc08386..5c3a08ab3 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -290,50 +290,6 @@ void mld_polyvecl_uniform_gamma1(mld_polyvecl *v, MLDSA_GAMMA1 + 1); } -MLD_INTERNAL_API -void mld_polyvecl_reduce(mld_polyvecl *v) -{ - unsigned int i; - mld_assert_bound_2d(v->vec, MLDSA_L, MLDSA_N, INT32_MIN, - MLD_REDUCE32_DOMAIN_MAX); - - for (i = 0; i < MLDSA_L; ++i) - __loop__( - assigns(i, memory_slice(v, sizeof(mld_polyvecl))) - invariant(i <= MLDSA_L) - invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) - invariant(forall(k2, 0, i, - array_bound(v->vec[k2].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX)))) - { - mld_poly_reduce(&v->vec[i]); - } - - mld_assert_bound_2d(v->vec, MLDSA_L, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, - MLD_REDUCE32_RANGE_MAX); -} - -/* Reference: We use destructive version (output=first input) to avoid - * reasoning about aliasing in the CBMC specification */ -MLD_INTERNAL_API -void mld_polyvecl_add(mld_polyvecl *u, const mld_polyvecl *v) -{ - unsigned int i; - - for (i = 0; i < MLDSA_L; ++i) - __loop__( - assigns(i, memory_slice(u, sizeof(mld_polyvecl))) - invariant(i <= MLDSA_L) - invariant(forall(k0, i, MLDSA_L, - forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1]))) - invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) - ) - { - mld_poly_add(&u->vec[i], &v->vec[i]); - } - mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, INT32_MIN, - MLD_REDUCE32_DOMAIN_MAX); -} - MLD_INTERNAL_API void mld_polyvecl_ntt(mld_polyvecl *v) { @@ -353,46 +309,6 @@ void mld_polyvecl_ntt(mld_polyvecl *v) mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND); } -MLD_INTERNAL_API -void mld_polyvecl_invntt_tomont(mld_polyvecl *v) -{ - unsigned int i; - mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLDSA_Q); - - for (i = 0; i < MLDSA_L; ++i) - __loop__( - assigns(i, memory_slice(v, sizeof(mld_polyvecl))) - invariant(i <= MLDSA_L) - invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) - invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_INTT_BOUND)))) - { - mld_poly_invntt_tomont(&v->vec[i]); - } - - mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_INTT_BOUND); -} - -MLD_INTERNAL_API -void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a, - const mld_polyvecl *v) -{ - unsigned int i; - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); - mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND); - - for (i = 0; i < MLDSA_L; ++i) - __loop__( - assigns(i, memory_slice(r, sizeof(mld_polyvecl))) - invariant(i <= MLDSA_L) - invariant(forall(k2, 0, i, array_abs_bound(r->vec[k2].coeffs, 0, MLDSA_N, MLDSA_Q))) - ) - { - mld_poly_pointwise_montgomery(&r->vec[i], a, &v->vec[i]); - } - - mld_assert_abs_bound_2d(r->vec, MLDSA_L, MLDSA_N, MLDSA_Q); -} - MLD_STATIC_TESTABLE void mld_polyvecl_pointwise_acc_montgomery_c( mld_poly *w, const mld_polyvecl *u, const mld_polyvecl *v) __contract__( @@ -858,23 +774,6 @@ void mld_polyvecl_pack_eta(uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES], } } -MLD_INTERNAL_API -void mld_polyvecl_pack_z(uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES], - const mld_polyvecl *p) -{ - unsigned int i; - mld_assert_bound_2d(p->vec, MLDSA_L, MLDSA_N, -(MLDSA_GAMMA1 - 1), - MLDSA_GAMMA1 + 1); - for (i = 0; i < MLDSA_L; ++i) - __loop__( - assigns(i, memory_slice(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) - invariant(i <= MLDSA_L) - ) - { - mld_polyz_pack(&r[i * MLDSA_POLYZ_PACKEDBYTES], &p->vec[i]); - } -} - MLD_INTERNAL_API void mld_polyveck_pack_t0(uint8_t r[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES], const mld_polyveck *p) diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index 71e902e90..ee97508b7 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -53,53 +53,6 @@ __contract__( array_bound(v->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ); -#define mld_polyvecl_reduce MLD_NAMESPACE_KL(polyvecl_reduce) -/************************************************* - * Name: mld_polyvecl_reduce - * - * Description: Inplace reduction of all coefficients of all polynomial in a - * vector of length MLDSA_L to - * representative in - *[-MLD_REDUCE32_RANGE_MAX,MLD_REDUCE32_RANGE_MAX]. - * - * Arguments: - mld_poly *v: pointer to input/output vector - **************************************************/ -MLD_INTERNAL_API -void mld_polyvecl_reduce(mld_polyvecl *v) -__contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) - requires(forall(k0, 0, MLDSA_L, - array_bound(v->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) - assigns(memory_slice(v, sizeof(mld_polyvecl))) - ensures(forall(k1, 0, MLDSA_L, - array_bound(v->vec[k1].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))) -); - -#define mld_polyvecl_add MLD_NAMESPACE_KL(polyvecl_add) -/************************************************* - * Name: mld_polyvecl_add - * - * Description: Add vectors of polynomials of length MLDSA_L. - * No modular reduction is performed. - * - * Arguments: - mld_polyveck *u: pointer to input-output vector of polynomials - * to be added to - * - const mld_polyveck *v: pointer to second input vector of - * polynomials - **************************************************/ -MLD_INTERNAL_API -void mld_polyvecl_add(mld_polyvecl *u, const mld_polyvecl *v) -__contract__( - requires(memory_no_alias(u, sizeof(mld_polyvecl))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) - requires(forall(p0, 0, MLDSA_L, array_abs_bound(u->vec[p0].coeffs, 0 , MLDSA_N, MLD_INTT_BOUND))) - requires(forall(p1, 0, MLDSA_L, - array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - assigns(memory_slice(u, sizeof(mld_polyvecl))) - ensures(forall(q2, 0, MLDSA_L, - array_bound(u->vec[q2].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX))) -); - #define mld_polyvecl_ntt MLD_NAMESPACE_KL(polyvecl_ntt) /************************************************* * Name: mld_polyvecl_ntt @@ -118,52 +71,6 @@ __contract__( ensures(forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ); -#define mld_polyvecl_invntt_tomont MLD_NAMESPACE_KL(polyvecl_invntt_tomont) -/************************************************* - * Name: mld_polyvecl_invntt_tomont - * - * Description: Inplace inverse NTT and multiplication by 2^{32}. - * Input coefficients need to be less than MLDSA_Q in absolute - * value and output coefficients are bounded by - * MLD_INTT_BOUND. - * - * Arguments: - mld_polyvecl *v: pointer to input/output vector - **************************************************/ -MLD_INTERNAL_API -void mld_polyvecl_invntt_tomont(mld_polyvecl *v) -__contract__( - requires(memory_no_alias(v, sizeof(mld_polyvecl))) - requires(forall(k0, 0, MLDSA_L, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyvecl))) - ensures(forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0 , MLDSA_N, MLD_INTT_BOUND))) -); - -#define mld_polyvecl_pointwise_poly_montgomery \ - MLD_NAMESPACE_KL(polyvecl_pointwise_poly_montgomery) -/************************************************* - * Name: mld_polyvecl_pointwise_poly_montgomery - * - * Description: Pointwise multiplication of a polynomial vector of length - * MLDSA_L by a single polynomial in NTT domain and multiplication - * of the resulting polynomial vector by 2^{-32}. - * - * Arguments: - mld_polyvecl *r: pointer to output vector - * - mld_poly *a: pointer to input polynomial - * - mld_polyvecl *v: pointer to input vector - **************************************************/ -MLD_INTERNAL_API -void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a, - const mld_polyvecl *v) -__contract__( - requires(memory_no_alias(r, sizeof(mld_polyvecl))) - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(v, sizeof(mld_polyvecl))) - requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) - requires(forall(k0, 0, MLDSA_L, array_abs_bound(v->vec[k0].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) - assigns(memory_slice(r, sizeof(mld_polyvecl))) - ensures(forall(k1, 0, MLDSA_L, array_abs_bound(r->vec[k1].coeffs, 0, MLDSA_N, MLDSA_Q))) -); - #define mld_polyvecl_pointwise_acc_montgomery \ MLD_NAMESPACE_KL(polyvecl_pointwise_acc_montgomery) /************************************************* @@ -626,28 +533,6 @@ __contract__( assigns(memory_slice(r, MLDSA_L * MLDSA_POLYETA_PACKEDBYTES)) ); -#define mld_polyvecl_pack_z MLD_NAMESPACE_KL(polyvecl_pack_z) -/************************************************* - * Name: mld_polyvecl_pack_z - * - * Description: Bit-pack polynomial vector with coefficients in - * [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1]. - * - * Arguments: - uint8_t *r: pointer to output byte array with - * MLDSA_L * MLDSA_POLYZ_PACKEDBYTES bytes - * - const mld_polyvecl *p: pointer to input polynomial vector - **************************************************/ -MLD_INTERNAL_API -void mld_polyvecl_pack_z(uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES], - const mld_polyvecl *p) -__contract__( - requires(memory_no_alias(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) - requires(memory_no_alias(p, sizeof(mld_polyvecl))) - requires(forall(k1, 0, MLDSA_L, - array_bound(p->vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - assigns(memory_slice(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) -); - #define mld_polyveck_pack_t0 MLD_NAMESPACE_KL(polyveck_pack_t0) /************************************************* * Name: mld_polyveck_pack_t0 diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index d3457ea6e..a65b5d0c8 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -47,6 +47,7 @@ #define mld_validate_hash_length MLD_ADD_PARAM_SET(mld_validate_hash_length) #define mld_get_hash_oid MLD_ADD_PARAM_SET(mld_get_hash_oid) #define mld_H MLD_ADD_PARAM_SET(mld_H) +#define mld_compute_pack_z MLD_ADD_PARAM_SET(mld_compute_pack_z) #define mld_attempt_signature_generation \ MLD_ADD_PARAM_SET(mld_attempt_signature_generation) #define mld_compute_t0_t1_tr_from_sk_components \ @@ -432,15 +433,93 @@ __contract__( mld_zeroize(&state, sizeof(state)); } -/* Reference: The reference implementation does not explicitly */ -/* check the maximum nonce value, but instead loops indefinitely */ -/* (even when the nonce would overflow). Internally, */ -/* sampling of y uses (nonceL), (nonceL+1), ... (nonce*L+L-1). */ -/* Hence, there are no overflows if nonce < (UINT16_MAX - L)/L. */ -/* Explicitly checking for this explicitly allows us to prove */ -/* type-safety. Note that FIPS204 explicitly allows an upper- */ -/* bound this loop of 814 (< (UINT16_MAX - L)/L) - see */ -/* @[FIPS204, Appendix C]. */ +/************************************************* + * Name: mld_compute_pack_z + * + * Description: Computes z = y + s1*c, checks that z has coefficients smaller + * than MLDSA_GAMMA1 - MLDSA_BETA, and packs z into the + * signature buffer. + * + * Arguments: - uint8_t *sig: output signature + * - const mld_poly *cp: challenge polynomial + * - const polyvecl *s1: secret vector s1 + * - const polyvecl *y: masking vector y + * + * Returns: - 0: Success (z has coefficients smaller than + * MLDSA_GAMMA1 - MLDSA_BETA,) + * - MLD_ERR_FAIL: z rejected (norm check failed) + * - MLD_ERR_OUT_OF_MEMORY: If MLD_CONFIG_CUSTOM_ALLOC_FREE is + * used and an allocation via MLD_CUSTOM_ALLOC returned NULL. + * + * Reference: This function is inlined into crypto_sign_signature in the + * reference implementation. + **************************************************/ +MLD_MUST_CHECK_RETURN_VALUE +static int mld_compute_pack_z(uint8_t sig[MLDSA_CRYPTO_BYTES], + const mld_poly *cp, const mld_polyvecl *s1, + const mld_polyvecl *y, mld_poly *z) +__contract__( + requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) + requires(memory_no_alias(cp, sizeof(mld_poly))) + requires(memory_no_alias(s1, sizeof(mld_polyvecl))) + requires(memory_no_alias(y, sizeof(mld_polyvecl))) + requires(memory_no_alias(z, sizeof(mld_poly))) + requires(array_abs_bound(cp->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) + requires(forall(k0, 0, MLDSA_L, + array_bound(y->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) + requires(forall(k1, 0, MLDSA_L, array_abs_bound(s1->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns(memory_slice(z, sizeof(mld_poly))) + ensures(return_value == 0 || return_value == MLD_ERR_FAIL || + return_value == MLD_ERR_OUT_OF_MEMORY) +) +{ + unsigned int i; + uint32_t z_invalid; + for (i = 0; i < MLDSA_L; i++) + __loop__( + assigns(i, memory_slice(z, sizeof(mld_poly)), memory_slice(sig, MLDSA_CRYPTO_BYTES)) + invariant(i <= MLDSA_L) + ) + { + mld_poly_pointwise_montgomery(z, cp, &s1->vec[i]); + mld_poly_invntt_tomont(z); + mld_poly_add(z, &y->vec[i]); + mld_poly_reduce(z); + + z_invalid = mld_poly_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA); + /* Constant time: It is fine (and prohibitively expensive to avoid) + * to leak the result of the norm check and which polynomial in z caused a + * rejection. It would even be okay to leak which coefficient led to + * rejection as the candidate signature will be discarded anyway. + * See Section 5.5 of @[Round3_Spec]. */ + MLD_CT_TESTING_DECLASSIFY(&z_invalid, sizeof(uint32_t)); + if (z_invalid) + { + return MLD_ERR_FAIL; /* reject */ + } + /* 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_z() */ + mld_assert_abs_bound(z, MLDSA_N, (MLDSA_GAMMA1 - MLDSA_BETA)); + + /* After the norm check, the distribution of each coefficient of z is + * independent of the secret key and it can, hence, be considered + * public. It is, hence, okay to immediately pack it into the user-provided + * signature buffer. */ + mld_pack_sig_z(sig, z, i); + } + return 0; +} + +/* Reference: The reference implementation does not explicitly check the + * maximum nonce value, but instead loops indefinitely (even when the nonce + * would overflow). Internally, sampling of y uses + * (nonceL), (nonceL+1), ... (nonce*L+L-1). + * Hence, there are no overflows if nonce < (UINT16_MAX - L)/L. + * Explicitly checking for this explicitly allows us to prove type-safety. + * Note that FIPS204 explicitly allows an upper-bound this loop of + * 814 (< (UINT16_MAX - L)/L) - see @[FIPS204, Appendix C]. */ #define MLD_NONCE_UB ((UINT16_MAX - MLDSA_L) / MLDSA_L) /************************************************* @@ -493,7 +572,7 @@ __contract__( ) { unsigned int n; - uint32_t z_invalid, w0_invalid, h_invalid; + uint32_t w0_invalid, h_invalid; int ret; /* TODO: Remove the following workaround for * https://github.com/diffblue/cbmc/issues/8813 */ @@ -506,29 +585,43 @@ __contract__( mld_polyvecl *y; mld_polyveck *h; + /* TODO: Remove the following workaround for + * https://github.com/diffblue/cbmc/issues/8813 */ + typedef MLK_UNION_OR_STRUCT + { + mld_polyveck w1; + mld_polyvecl tmp; + } + w1tmp_u; + mld_polyveck *w1; + mld_polyvecl *tmp; + MLD_ALLOC(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES); MLD_ALLOC(yh, yh_u, 1); - MLD_ALLOC(z, mld_polyvecl, 1); - MLD_ALLOC(w1, mld_polyveck, 1); + MLD_ALLOC(z, mld_poly, 1); + MLD_ALLOC(w1tmp, w1tmp_u, 1); MLD_ALLOC(w0, mld_polyveck, 1); MLD_ALLOC(cp, mld_poly, 1); + MLD_ALLOC(t, mld_poly, 1); - if (challenge_bytes == NULL || yh == NULL || z == NULL || w1 == NULL || - w0 == NULL || cp == NULL) + if (challenge_bytes == NULL || yh == NULL || z == NULL || w1tmp == NULL || + w0 == NULL || cp == NULL || t == NULL) { ret = MLD_ERR_OUT_OF_MEMORY; goto cleanup; } y = &yh->y; h = &yh->h; + w1 = &w1tmp->w1; + tmp = &w1tmp->tmp; /* Sample intermediate vector y */ mld_polyvecl_uniform_gamma1(y, rhoprime, nonce); /* Matrix-vector multiplication */ - *z = *y; - mld_polyvecl_ntt(z); - mld_polyvec_matrix_pointwise_montgomery(w0, mat, z); + *tmp = *y; + mld_polyvecl_ntt(tmp); + mld_polyvec_matrix_pointwise_montgomery(w0, mat, tmp); mld_polyveck_reduce(w0); mld_polyveck_invntt_tomont(w0); @@ -548,30 +641,12 @@ __contract__( mld_poly_ntt(cp); /* Compute z, reject if it reveals secret */ - mld_polyvecl_pointwise_poly_montgomery(z, cp, s1); - mld_polyvecl_invntt_tomont(z); - mld_polyvecl_add(z, y); - mld_polyvecl_reduce(z); - - z_invalid = mld_polyvecl_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA); - /* Constant time: It is fine (and prohibitively expensive to avoid) - * leaking the result of the norm check. In case of rejection it - * would even be okay to leak which coefficient led to rejection - * as the candidate signature will be discarded anyway. - * See Section 5.5 of @[Round3_Spec]. */ - MLD_CT_TESTING_DECLASSIFY(&z_invalid, sizeof(uint32_t)); - if (z_invalid) + ret = mld_compute_pack_z(sig, cp, s1, y, t); + if (ret) { - ret = MLD_ERR_FAIL; /* reject */ goto cleanup; } - /* 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() */ - 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 */ mld_polyveck_pointwise_poly_montgomery(h, cp, s2); @@ -622,20 +697,19 @@ __contract__( } /* All is well - write signature */ + mld_pack_sig_c_h(sig, challenge_bytes, h, n); /* Constant time: At this point it is clear that the signature is valid - it * can, hence, be considered public. */ - MLD_CT_TESTING_DECLASSIFY(h, sizeof(*h)); - MLD_CT_TESTING_DECLASSIFY(z, sizeof(*z)); - mld_pack_sig(sig, challenge_bytes, z, h, n); - + MLD_CT_TESTING_DECLASSIFY(sig, MLDSA_CRYPTO_BYTES); ret = 0; /* success */ cleanup: /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + MLD_FREE(t, mld_poly, 1); MLD_FREE(cp, mld_poly, 1); MLD_FREE(w0, mld_polyveck, 1); - MLD_FREE(w1, mld_polyveck, 1); - MLD_FREE(z, mld_polyvecl, 1); + MLD_FREE(w1tmp, w1tmp_u, 1); + MLD_FREE(z, mld_poly, 1); MLD_FREE(yh, yh_u, 1); MLD_FREE(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES); @@ -1390,6 +1464,7 @@ int crypto_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], #undef mld_validate_hash_length #undef mld_get_hash_oid #undef mld_H +#undef mld_compute_pack_z #undef mld_attempt_signature_generation #undef mld_compute_t0_t1_tr_from_sk_components #undef MLD_NONCE_UB diff --git a/proofs/cbmc/attempt_signature_generation/Makefile b/proofs/cbmc/attempt_signature_generation/Makefile index dc518af3d..f7a494d1a 100644 --- a/proofs/cbmc/attempt_signature_generation/Makefile +++ b/proofs/cbmc/attempt_signature_generation/Makefile @@ -31,18 +31,14 @@ USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1 \ mld_H \ $(MLD_NAMESPACE)poly_challenge \ $(MLD_NAMESPACE)poly_ntt \ - $(MLD_NAMESPACE)polyvecl_pointwise_poly_montgomery \ - $(MLD_NAMESPACE)polyvecl_invntt_tomont \ - $(MLD_NAMESPACE)polyvecl_add \ - $(MLD_NAMESPACE)polyvecl_reduce \ - $(MLD_NAMESPACE)polyvecl_chknorm \ $(MLD_NAMESPACE)polyveck_pointwise_poly_montgomery \ $(MLD_NAMESPACE)polyveck_sub \ $(MLD_NAMESPACE)polyveck_reduce \ $(MLD_NAMESPACE)polyveck_chknorm \ $(MLD_NAMESPACE)polyveck_add \ $(MLD_NAMESPACE)polyveck_make_hint \ - $(MLD_NAMESPACE)pack_sig + $(MLD_NAMESPACE)pack_sig_c_h \ + mld_compute_pack_z USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on diff --git a/proofs/cbmc/polyvecl_pointwise_poly_montgomery/Makefile b/proofs/cbmc/compute_pack_z/Makefile similarity index 72% rename from proofs/cbmc/polyvecl_pointwise_poly_montgomery/Makefile rename to proofs/cbmc/compute_pack_z/Makefile index 08673b1b7..3e9166327 100644 --- a/proofs/cbmc/polyvecl_pointwise_poly_montgomery/Makefile +++ b/proofs/cbmc/compute_pack_z/Makefile @@ -4,30 +4,40 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = polyvecl_pointwise_poly_montgomery_harness +HARNESS_FILE = compute_pack_z_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = polyvecl_pointwise_poly_montgomery +PROOF_UID = mld_compute_pack_z DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += +UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c + +CHECK_FUNCTION_CONTRACTS=mld_compute_pack_z +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery \ + $(MLD_NAMESPACE)poly_invntt_tomont \ + $(MLD_NAMESPACE)poly_add \ + $(MLD_NAMESPACE)poly_reduce \ + $(MLD_NAMESPACE)poly_chknorm \ + $(MLD_NAMESPACE)pack_sig_z +USE_FUNCTION_CONTRACTS+=mld_zeroize -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_poly_montgomery -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 --slice-formula +CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3 +CBMCFLAGS += --slice-formula +CBMCFLAGS += --no-array-field-sensitivity -FUNCTION_NAME = polyvecl_pointwise_poly_montgomery +FUNCTION_NAME = mld_compute_pack_z # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will @@ -36,7 +46,7 @@ FUNCTION_NAME = polyvecl_pointwise_poly_montgomery # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 9 +CBMC_OBJECT_BITS = 12 # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file diff --git a/proofs/cbmc/compute_pack_z/compute_pack_z_harness.c b/proofs/cbmc/compute_pack_z/compute_pack_z_harness.c new file mode 100644 index 000000000..6200e76cd --- /dev/null +++ b/proofs/cbmc/compute_pack_z/compute_pack_z_harness.c @@ -0,0 +1,20 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "sign.h" + +int mld_compute_pack_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *cp, + const mld_polyvecl *s1, const mld_polyvecl *y, + mld_poly *t); + +void harness(void) +{ + uint8_t *sig; + mld_poly *cp; + mld_polyvecl *s1; + mld_polyvecl *y; + mld_poly *t; + + int r; + r = mld_compute_pack_z(sig, cp, s1, y, t); +} diff --git a/proofs/cbmc/pack_sig/Makefile b/proofs/cbmc/pack_sig_c_h/Makefile similarity index 90% rename from proofs/cbmc/pack_sig/Makefile rename to proofs/cbmc/pack_sig_c_h/Makefile index b50425d16..0c0a7e762 100644 --- a/proofs/cbmc/pack_sig/Makefile +++ b/proofs/cbmc/pack_sig_c_h/Makefile @@ -4,11 +4,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = pack_sig_harness +HARNESS_FILE = pack_sig_c_h_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = pack_sig +PROOF_UID = pack_sig_c_h DEFINES += INCLUDES += @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sig -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pack_z +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sig_c_h +USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS+=--slice-formula -FUNCTION_NAME = pack_sig +FUNCTION_NAME = pack_sig_c_h # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will diff --git a/proofs/cbmc/pack_sig/pack_sig_harness.c b/proofs/cbmc/pack_sig_c_h/pack_sig_c_h_harness.c similarity index 80% rename from proofs/cbmc/pack_sig/pack_sig_harness.c rename to proofs/cbmc/pack_sig_c_h/pack_sig_c_h_harness.c index 40d7aecf7..fa7df3565 100644 --- a/proofs/cbmc/pack_sig/pack_sig_harness.c +++ b/proofs/cbmc/pack_sig_c_h/pack_sig_c_h_harness.c @@ -8,7 +8,6 @@ void harness(void) { uint8_t *a, *b; mld_polyveck *h; - mld_polyvecl *z; unsigned int nh; - mld_pack_sig(a, b, z, h, nh); + mld_pack_sig_c_h(a, b, h, nh); } diff --git a/proofs/cbmc/polyvecl_pack_z/Makefile b/proofs/cbmc/pack_sig_z/Makefile similarity index 87% rename from proofs/cbmc/polyvecl_pack_z/Makefile rename to proofs/cbmc/pack_sig_z/Makefile index 5658b041e..5e2866615 100644 --- a/proofs/cbmc/polyvecl_pack_z/Makefile +++ b/proofs/cbmc/pack_sig_z/Makefile @@ -4,11 +4,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = polyvecl_pack_z_harness +HARNESS_FILE = pack_sig_z_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = polyvecl_pack_z +PROOF_UID = pack_sig_z DEFINES += INCLUDES += @@ -16,9 +16,9 @@ INCLUDES += REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pack_z +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sig_z USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_pack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -26,9 +26,9 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -CBMCFLAGS += --slice-formula +CBMCFLAGS+=--slice-formula -FUNCTION_NAME = polyvecl_pack_z +FUNCTION_NAME = pack_sig_z # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will @@ -37,7 +37,7 @@ FUNCTION_NAME = polyvecl_pack_z # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 8 +CBMC_OBJECT_BITS = 9 # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file diff --git a/proofs/cbmc/polyvecl_reduce/polyvecl_reduce_harness.c b/proofs/cbmc/pack_sig_z/pack_sig_z_harness.c similarity index 57% rename from proofs/cbmc/polyvecl_reduce/polyvecl_reduce_harness.c rename to proofs/cbmc/pack_sig_z/pack_sig_z_harness.c index 2306f8ddd..585b5811d 100644 --- a/proofs/cbmc/polyvecl_reduce/polyvecl_reduce_harness.c +++ b/proofs/cbmc/pack_sig_z/pack_sig_z_harness.c @@ -1,10 +1,13 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -#include "polyvec.h" +#include "packing.h" + void harness(void) { - mld_polyvecl *a; - mld_polyvecl_reduce(a); + uint8_t *a; + mld_poly *zi; + unsigned i; + mld_pack_sig_z(a, zi, i); } diff --git a/proofs/cbmc/polyvecl_add/Makefile b/proofs/cbmc/polyvecl_add/Makefile deleted file mode 100644 index 38de96cdd..000000000 --- a/proofs/cbmc/polyvecl_add/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = polyvecl_add_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = polyvecl_add - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c - -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_add -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_add -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula - -FUNCTION_NAME = polyvecl_add - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 10 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/polyvecl_add/polyvecl_add_harness.c b/proofs/cbmc/polyvecl_add/polyvecl_add_harness.c deleted file mode 100644 index 83de2c6cb..000000000 --- a/proofs/cbmc/polyvecl_add/polyvecl_add_harness.c +++ /dev/null @@ -1,10 +0,0 @@ -// Copyright (c) The mldsa-native project authors -// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -#include "polyvec.h" - -void harness(void) -{ - mld_polyvecl *r, *b; - mld_polyvecl_add(r, b); -} diff --git a/proofs/cbmc/polyvecl_invntt_tomont/Makefile b/proofs/cbmc/polyvecl_invntt_tomont/Makefile deleted file mode 100644 index f33d63781..000000000 --- a/proofs/cbmc/polyvecl_invntt_tomont/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = polyvecl_invntt_tomont_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = polyvecl_invntt_tomont - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c - -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_invntt_tomont -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_invntt_tomont -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 - -FUNCTION_NAME = polyvecl_invntt_tomont - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 8 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/polyvecl_invntt_tomont/polyvecl_invntt_tomont_harness.c b/proofs/cbmc/polyvecl_invntt_tomont/polyvecl_invntt_tomont_harness.c deleted file mode 100644 index 3aac3f02c..000000000 --- a/proofs/cbmc/polyvecl_invntt_tomont/polyvecl_invntt_tomont_harness.c +++ /dev/null @@ -1,12 +0,0 @@ -// Copyright (c) The mldsa-native project authors -// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -#include -#include "params.h" -#include "polyvec.h" - -void harness(void) -{ - mld_polyvecl *v; - mld_polyvecl_invntt_tomont(v); -} diff --git a/proofs/cbmc/polyvecl_pack_z/polyvecl_pack_z_harness.c b/proofs/cbmc/polyvecl_pack_z/polyvecl_pack_z_harness.c deleted file mode 100644 index f07a0b8f1..000000000 --- a/proofs/cbmc/polyvecl_pack_z/polyvecl_pack_z_harness.c +++ /dev/null @@ -1,11 +0,0 @@ -// Copyright (c) The mldsa-native project authors -// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -#include "polyvec.h" - -void harness(void) -{ - mld_polyvecl *a; - uint8_t *b; - mld_polyvecl_pack_z(b, a); -} diff --git a/proofs/cbmc/polyvecl_pointwise_poly_montgomery/polyvecl_pointwise_poly_montgomery_harness.c b/proofs/cbmc/polyvecl_pointwise_poly_montgomery/polyvecl_pointwise_poly_montgomery_harness.c deleted file mode 100644 index 23323057b..000000000 --- a/proofs/cbmc/polyvecl_pointwise_poly_montgomery/polyvecl_pointwise_poly_montgomery_harness.c +++ /dev/null @@ -1,11 +0,0 @@ -// Copyright (c) The mldsa-native project authors -// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -#include "polyvec.h" - -void harness(void) -{ - mld_polyvecl *a, *b; - mld_poly *c; - mld_polyvecl_pointwise_poly_montgomery(a, c, b); -} diff --git a/proofs/cbmc/polyvecl_reduce/Makefile b/proofs/cbmc/polyvecl_reduce/Makefile deleted file mode 100644 index c665a453e..000000000 --- a/proofs/cbmc/polyvecl_reduce/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = polyvecl_reduce_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = polyvecl_reduce - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c - -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_reduce -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_reduce -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 - -FUNCTION_NAME = polyvecl_reduce - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 8 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common From d28fb9f14958bafca4b15cd6722462e5306e6343 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 31 Dec 2025 12:46:03 +0800 Subject: [PATCH 2/2] CBMC: Correct called contracts in verify_pre_hash_internal For some reason the previous (unrelated) commit caused the verify_pre_hash_internal proof to fail due to extra functions in USE_FUNCTION_CONTRACTS. This commit removes the extra functions. Signed-off-by: Matthias J. Kannwischer --- .../cbmc/crypto_sign_verify_pre_hash_internal/Makefile | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile b/proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile index 99300ac4a..0798452be 100644 --- a/proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile +++ b/proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile @@ -20,14 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_internal -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal \ - $(MLD_NAMESPACE)unpack_pk \ - $(MLD_NAMESPACE)unpack_sig \ - $(MLD_NAMESPACE)polyvec_matrix_expand \ - $(MLD_NAMESPACE)polyvecl_invntt_tomont \ - $(MLD_NAMESPACE)polyveck_invntt_tomont \ - $(MLD_NAMESPACE)polyveck_sub \ - $(MLD_NAMESPACE)polyveck_use_hint +USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on