diff --git a/README.md b/README.md index 3677ba128..2a3e03978 100644 --- a/README.md +++ b/README.md @@ -158,7 +158,7 @@ Yes. mldsa-native supports all three ML-DSA security levels (ML-DSA-44, ML-DSA-6 Yes. mldsa-native provides a compile-time option `MLD_CONFIG_REDUCE_RAM` that reduces RAM usage. This trades memory for performance: - **Memory savings**: 12 KB (ML-DSA-44), 25 KB (ML-DSA-65), 49 KB (ML-DSA-87) for each of key generation, signing, and verification. - For signing, additional 4 KB (ML-DSA-44), 5 KB (ML-DSA-65), and 7 KB (ML-DSA-87) are saved. + For signing, additional 8 KB (ML-DSA-44), 10 KB (ML-DSA-65), and 14 KB (ML-DSA-87) are saved. - **Performance cost**: Matrix generation is no longer batched, resulting in slower signing and verification To enable this mode, define `MLD_CONFIG_REDUCE_RAM` in [mldsa_native_config.h](mldsa/mldsa_native_config.h) or pass `-DMLD_CONFIG_REDUCE_RAM` as a compiler flag. diff --git a/mldsa/mldsa_native.S b/mldsa/mldsa_native.S index 8428fc58a..af5df31a4 100644 --- a/mldsa/mldsa_native.S +++ b/mldsa/mldsa_native.S @@ -222,6 +222,7 @@ #undef MLD_PACKING_H #undef mld_pack_pk #undef mld_pack_sig +#undef mld_pack_sig_z #undef mld_pack_sk #undef mld_unpack_pk #undef mld_unpack_sig @@ -296,15 +297,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 9396a7efd..90cbfe27d 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -218,6 +218,7 @@ #undef MLD_PACKING_H #undef mld_pack_pk #undef mld_pack_sig +#undef mld_pack_sig_z #undef mld_pack_sk #undef mld_unpack_pk #undef mld_unpack_sig @@ -292,15 +293,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..5af0c8e08 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -100,15 +100,15 @@ 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) + 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..5518bf688 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -73,12 +73,12 @@ __contract__( /************************************************* * Name: mld_pack_sig * - * 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 @@ -89,21 +89,41 @@ __contract__( **************************************************/ 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) + 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. + * + * 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 95f7677f6..fb5ea5e73 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -264,50 +264,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) { @@ -327,46 +283,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__( @@ -832,23 +748,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 ef5ea6bea..9fa75ff61 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -486,7 +486,7 @@ __contract__( return_value == MLD_ERR_OUT_OF_MEMORY) ) { - unsigned int n; + unsigned int n, i; uint32_t z_invalid, w0_invalid, h_invalid; int ret; /* TODO: Remove the following workaround for @@ -500,14 +500,25 @@ __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); - if (challenge_bytes == NULL || yh == NULL || z == NULL || w1 == NULL || + if (challenge_bytes == NULL || yh == NULL || z == NULL || w1tmp == NULL || w0 == NULL || cp == NULL) { ret = MLD_ERR_OUT_OF_MEMORY; @@ -515,14 +526,16 @@ __contract__( } 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); @@ -542,30 +555,35 @@ __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) + 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)) { - ret = MLD_ERR_FAIL; /* reject */ - goto cleanup; + 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) + * 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_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_z() */ + mld_assert_abs_bound(z, MLDSA_N, (MLDSA_GAMMA1 - MLDSA_BETA)); + mld_pack_sig_z(sig, z, i); } - /* 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); @@ -616,20 +634,18 @@ __contract__( } /* All is well - write signature */ + mld_pack_sig(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(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); diff --git a/proofs/cbmc/attempt_signature_generation/Makefile b/proofs/cbmc/attempt_signature_generation/Makefile index dc518af3d..a1682f63c 100644 --- a/proofs/cbmc/attempt_signature_generation/Makefile +++ b/proofs/cbmc/attempt_signature_generation/Makefile @@ -31,17 +31,18 @@ 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)poly_pointwise_montgomery \ + $(MLD_NAMESPACE)poly_invntt_tomont \ + $(MLD_NAMESPACE)poly_add \ + $(MLD_NAMESPACE)poly_reduce \ + $(MLD_NAMESPACE)poly_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_z \ $(MLD_NAMESPACE)pack_sig USE_FUNCTION_CONTRACTS+=mld_zeroize 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 diff --git a/proofs/cbmc/pack_sig/Makefile b/proofs/cbmc/pack_sig/Makefile index b50425d16..abee66a67 100644 --- a/proofs/cbmc/pack_sig/Makefile +++ b/proofs/cbmc/pack_sig/Makefile @@ -19,7 +19,7 @@ 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 +USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/pack_sig/pack_sig_harness.c b/proofs/cbmc/pack_sig/pack_sig_harness.c index 40d7aecf7..f6c93774a 100644 --- a/proofs/cbmc/pack_sig/pack_sig_harness.c +++ b/proofs/cbmc/pack_sig/pack_sig_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(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_pack_z/polyvecl_pack_z_harness.c b/proofs/cbmc/pack_sig_z/pack_sig_z_harness.c similarity index 57% rename from proofs/cbmc/polyvecl_pack_z/polyvecl_pack_z_harness.c rename to proofs/cbmc/pack_sig_z/pack_sig_z_harness.c index f07a0b8f1..585b5811d 100644 --- a/proofs/cbmc/polyvecl_pack_z/polyvecl_pack_z_harness.c +++ b/proofs/cbmc/pack_sig_z/pack_sig_z_harness.c @@ -1,11 +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; - uint8_t *b; - mld_polyvecl_pack_z(b, 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_pointwise_poly_montgomery/Makefile b/proofs/cbmc/polyvecl_pointwise_poly_montgomery/Makefile deleted file mode 100644 index 08673b1b7..000000000 --- a/proofs/cbmc/polyvecl_pointwise_poly_montgomery/Makefile +++ /dev/null @@ -1,54 +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_pointwise_poly_montgomery_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 - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c - -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 - -FUNCTION_NAME = polyvecl_pointwise_poly_montgomery - -# 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 = 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 -# ("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_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 diff --git a/proofs/cbmc/polyvecl_reduce/polyvecl_reduce_harness.c b/proofs/cbmc/polyvecl_reduce/polyvecl_reduce_harness.c deleted file mode 100644 index 2306f8ddd..000000000 --- a/proofs/cbmc/polyvecl_reduce/polyvecl_reduce_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 *a; - mld_polyvecl_reduce(a); -}