From edfd1119e5d85753e7fb7691c703615e3139ec87 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Wed, 3 Sep 2025 17:17:57 -0700 Subject: [PATCH 1/2] Split files into level-specific and level-generic Signed-off-by: Jake Massimo --- mldsa/poly.c | 646 ------------------------------------------------ mldsa/poly_k.c | 659 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 659 insertions(+), 646 deletions(-) create mode 100644 mldsa/poly_k.c diff --git a/mldsa/poly.c b/mldsa/poly.c index 90092a8f..d8f8934f 100644 --- a/mldsa/poly.c +++ b/mldsa/poly.c @@ -172,65 +172,6 @@ void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a) mld_assert_bound(a1->coeffs, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1); } -void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) -{ - unsigned int i; - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - - for (i = 0; i < MLDSA_N; ++i) - __loop__( - assigns(i, memory_slice(a0, sizeof(mld_poly)), memory_slice(a1, sizeof(mld_poly))) - invariant(i <= MLDSA_N) - invariant(array_bound(a1->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) - invariant(array_abs_bound(a0->coeffs, 0, i, MLDSA_GAMMA2+1)) - ) - { - mld_decompose(&a0->coeffs[i], &a1->coeffs[i], a->coeffs[i]); - } - - mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2 + 1); - mld_assert_bound(a1->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); -} - -unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, - const mld_poly *a1) -{ - unsigned int i, s = 0; - - for (i = 0; i < MLDSA_N; ++i) - __loop__( - invariant(i <= MLDSA_N) - invariant(s <= i) - invariant(array_bound(h->coeffs, 0, i, 0, 2)) - ) - { - const unsigned int hint_bit = mld_make_hint(a0->coeffs[i], a1->coeffs[i]); - h->coeffs[i] = hint_bit; - s += hint_bit; - } - - mld_assert(s <= MLDSA_N); - return s; -} - -void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) -{ - unsigned int i; - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - - for (i = 0; i < MLDSA_N; ++i) - __loop__( - invariant(i <= MLDSA_N) - invariant(array_bound(b->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) - ) - { - b->coeffs[i] = mld_use_hint(a->coeffs[i], h->coeffs[i]); - } - - mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); -} - /* Reference: explicitly checks the bound B to be <= (MLDSA_Q - 1) / 8). * This is unnecessary as it's always a compile-time constant. * We instead model it as a precondition. @@ -439,457 +380,6 @@ void mld_poly_uniform_4x(mld_poly *vec0, mld_poly *vec1, mld_poly *vec2, mld_zeroize(buf, sizeof(buf)); } -/************************************************* - * Name: mld_rej_eta - * - * Description: Sample uniformly random coefficients in [-MLDSA_ETA, MLDSA_ETA] - *by performing rejection sampling on array of random bytes. - * - * Arguments: - int32_t *a: pointer to output array (allocated) - * - unsigned int target: requested number of coefficients to - *sample - * - unsigned int offset: number of coefficients already sampled - * - const uint8_t *buf: array of random bytes to sample from - * - unsigned int buflen: length of array of random bytes - * - * Returns number of sampled coefficients. Can be smaller than target if not - *enough random bytes were given. - **************************************************/ - -/* Reference: `mld_rej_eta()` in the reference implementation [@REF]. - * - Our signature differs from the reference implementation - * in that it adds the offset and always expects the base of the - * target buffer. This avoids shifting the buffer base in the - * caller, which appears tricky to reason about. */ -#if MLDSA_ETA == 2 -/* - * Sampling 256 coefficients mod 15 using rejection sampling from 4 bits. - * Expected number of required bytes: (256 * (16/15))/2 = 136.5 bytes. - * We sample 1 block (=136 bytes) of SHAKE256_RATE output initially. - * Sampling 2 blocks initially results in slightly worse performance. - */ -#define POLY_UNIFORM_ETA_NBLOCKS 1 -#elif MLDSA_ETA == 4 -/* - * Sampling 256 coefficients mod 9 using rejection sampling from 4 bits. - * Expected number of required bytes: (256 * (16/9))/2 = 227.5 bytes. - * We sample 2 blocks (=272 bytes) of SHAKE256_RATE output initially. - */ -#define POLY_UNIFORM_ETA_NBLOCKS 2 -#else /* MLDSA_ETA == 4 */ -#error "Invalid value of MLDSA_ETA" -#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ -static unsigned int mld_rej_eta(int32_t *a, unsigned int target, - unsigned int offset, const uint8_t *buf, - unsigned int buflen) -__contract__( - requires(offset <= target && target <= MLDSA_N) - requires(buflen <= (POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) - requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) - assigns(memory_slice(a, sizeof(int32_t) * target)) - ensures(offset <= return_value && return_value <= target) - ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) -) -{ - unsigned int ctr, pos; - int t_valid; - uint32_t t0, t1; - -/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */ -#if MLDSA_ETA == 2 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) - if (offset == 0) - { - int ret = mld_rej_uniform_eta2_native(a, target, buf, buflen); - if (ret != -1) - { - unsigned res = (unsigned)ret; - mld_assert_abs_bound(a, res, MLDSA_ETA + 1); - return res; - } - } -/* TODO: CBMC proof based on mld_rej_uniform_eta4_native */ -#elif MLDSA_ETA == 4 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) - if (offset == 0) - { - int ret = mld_rej_uniform_eta4_native(a, target, buf, buflen); - if (ret != -1) - { - unsigned res = (unsigned)ret; - mld_assert_abs_bound(a, res, MLDSA_ETA + 1); - return res; - } - } -#endif /* !(MLDSA_ETA == 2 && MLD_USE_NATIVE_REJ_UNIFORM_ETA2) && MLDSA_ETA == \ - 4 && MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */ - - ctr = offset; - pos = 0; - while (ctr < target && pos < buflen) - __loop__( - invariant(offset <= ctr && ctr <= target && pos <= buflen) - invariant(array_abs_bound(a, 0, ctr, MLDSA_ETA + 1)) - ) - { - t0 = buf[pos] & 0x0F; - t1 = buf[pos++] >> 4; - - /* Constant time: The inputs and outputs to the rejection sampling are - * secret. However, it is fine to leak which coefficients have been - * rejected. For constant-time testing, we declassify the result of - * the comparison. - */ -#if MLDSA_ETA == 2 - t_valid = t0 < 15; - MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); - if (t_valid) /* t0 < 15 */ - { - t0 = t0 - (205 * t0 >> 10) * 5; - a[ctr++] = 2 - (int32_t)t0; - } - t_valid = t1 < 15; - MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); - if (t_valid && ctr < target) /* t1 < 15 */ - { - t1 = t1 - (205 * t1 >> 10) * 5; - a[ctr++] = 2 - (int32_t)t1; - } -#elif MLDSA_ETA == 4 - t_valid = t0 < 9; - MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); - if (t_valid) /* t0 < 9 */ - { - a[ctr++] = 4 - (int32_t)t0; - } - t_valid = t1 < 9; /* t1 < 9 */ - MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); - if (t_valid && ctr < target) - { - a[ctr++] = 4 - (int32_t)t1; - } -#else /* MLDSA_ETA == 4 */ -#error "Invalid value of MLDSA_ETA" -#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ - } - - return ctr; -} - -void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, - mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES], - uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, - uint8_t nonce3) -{ - /* Temporary buffers for XOF output before rejection sampling */ - MLD_ALIGN uint8_t - buf[4][MLD_ALIGN_UP(POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)]; - - MLD_ALIGN uint8_t extseed[4][MLD_ALIGN_UP(MLDSA_CRHBYTES + 2)]; - - /* Tracks the number of coefficients we have already sampled */ - unsigned ctr[4]; - mld_xof256_x4_ctx state; - unsigned buflen; - - memcpy(extseed[0], seed, MLDSA_CRHBYTES); - memcpy(extseed[1], seed, MLDSA_CRHBYTES); - memcpy(extseed[2], seed, MLDSA_CRHBYTES); - memcpy(extseed[3], seed, MLDSA_CRHBYTES); - extseed[0][MLDSA_CRHBYTES] = nonce0; - extseed[1][MLDSA_CRHBYTES] = nonce1; - extseed[2][MLDSA_CRHBYTES] = nonce2; - extseed[3][MLDSA_CRHBYTES] = nonce3; - extseed[0][MLDSA_CRHBYTES + 1] = 0; - extseed[1][MLDSA_CRHBYTES + 1] = 0; - extseed[2][MLDSA_CRHBYTES + 1] = 0; - extseed[3][MLDSA_CRHBYTES + 1] = 0; - - mld_xof256_x4_init(&state); - mld_xof256_x4_absorb(&state, extseed, MLDSA_CRHBYTES + 2); - - /* - * Initially, squeeze heuristic number of POLY_UNIFORM_ETA_NBLOCKS. - * This should generate the coefficients with high probability. - */ - mld_xof256_x4_squeezeblocks(buf, POLY_UNIFORM_ETA_NBLOCKS, &state); - buflen = POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES; - - ctr[0] = mld_rej_eta(r0->coeffs, MLDSA_N, 0, buf[0], buflen); - ctr[1] = mld_rej_eta(r1->coeffs, MLDSA_N, 0, buf[1], buflen); - ctr[2] = mld_rej_eta(r2->coeffs, MLDSA_N, 0, buf[2], buflen); - ctr[3] = mld_rej_eta(r3->coeffs, MLDSA_N, 0, buf[3], buflen); - - /* - * So long as not all entries have been generated, squeeze - * one more block a time until we're done. - */ - buflen = STREAM256_BLOCKBYTES; - while (ctr[0] < MLDSA_N || ctr[1] < MLDSA_N || ctr[2] < MLDSA_N || - ctr[3] < MLDSA_N) - __loop__( - assigns(ctr, state, memory_slice(r0, sizeof(mld_poly)), - memory_slice(r1, sizeof(mld_poly)), memory_slice(r2, sizeof(mld_poly)), - memory_slice(r3, sizeof(mld_poly)), object_whole(buf[0]), - object_whole(buf[1]), object_whole(buf[2]), - object_whole(buf[3])) - invariant(ctr[0] <= MLDSA_N && ctr[1] <= MLDSA_N) - invariant(ctr[2] <= MLDSA_N && ctr[3] <= MLDSA_N) - invariant(array_abs_bound(r0->coeffs, 0, ctr[0], MLDSA_ETA + 1)) - invariant(array_abs_bound(r1->coeffs, 0, ctr[1], MLDSA_ETA + 1)) - invariant(array_abs_bound(r2->coeffs, 0, ctr[2], MLDSA_ETA + 1)) - invariant(array_abs_bound(r3->coeffs, 0, ctr[3], MLDSA_ETA + 1))) - { - mld_xof256_x4_squeezeblocks(buf, 1, &state); - ctr[0] = mld_rej_eta(r0->coeffs, MLDSA_N, ctr[0], buf[0], buflen); - ctr[1] = mld_rej_eta(r1->coeffs, MLDSA_N, ctr[1], buf[1], buflen); - ctr[2] = mld_rej_eta(r2->coeffs, MLDSA_N, ctr[2], buf[2], buflen); - ctr[3] = mld_rej_eta(r3->coeffs, MLDSA_N, ctr[3], buf[3], buflen); - } - - mld_xof256_x4_release(&state); - - /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */ - mld_zeroize(buf, sizeof(buf)); - mld_zeroize(extseed, sizeof(extseed)); -} - - -#define POLY_UNIFORM_GAMMA1_NBLOCKS \ - ((MLDSA_POLYZ_PACKEDBYTES + STREAM256_BLOCKBYTES - 1) / STREAM256_BLOCKBYTES) -void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES], - uint16_t nonce) -{ - MLD_ALIGN uint8_t buf[POLY_UNIFORM_GAMMA1_NBLOCKS * STREAM256_BLOCKBYTES]; - MLD_ALIGN uint8_t extseed[MLDSA_CRHBYTES + 2]; - mld_xof256_ctx state; - - memcpy(extseed, seed, MLDSA_CRHBYTES); - extseed[MLDSA_CRHBYTES] = nonce & 0xFF; - extseed[MLDSA_CRHBYTES + 1] = nonce >> 8; - - mld_xof256_init(&state); - mld_xof256_absorb(&state, extseed, MLDSA_CRHBYTES + 2); - - mld_xof256_squeezeblocks(buf, POLY_UNIFORM_GAMMA1_NBLOCKS, &state); - mld_polyz_unpack(a, buf); - - mld_xof256_release(&state); - - /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */ - mld_zeroize(buf, sizeof(buf)); - mld_zeroize(extseed, sizeof(extseed)); -} - -void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, - mld_poly *r3, - const uint8_t seed[MLDSA_CRHBYTES], - uint16_t nonce0, uint16_t nonce1, - uint16_t nonce2, uint16_t nonce3) -{ - /* Temporary buffers for XOF output before rejection sampling */ - MLD_ALIGN uint8_t - buf[4][MLD_ALIGN_UP(POLY_UNIFORM_GAMMA1_NBLOCKS * STREAM256_BLOCKBYTES)]; - - MLD_ALIGN uint8_t extseed[4][MLD_ALIGN_UP(MLDSA_CRHBYTES + 2)]; - - /* Tracks the number of coefficients we have already sampled */ - mld_xof256_x4_ctx state; - - memcpy(extseed[0], seed, MLDSA_CRHBYTES); - memcpy(extseed[1], seed, MLDSA_CRHBYTES); - memcpy(extseed[2], seed, MLDSA_CRHBYTES); - memcpy(extseed[3], seed, MLDSA_CRHBYTES); - extseed[0][MLDSA_CRHBYTES] = nonce0 & 0xFF; - extseed[1][MLDSA_CRHBYTES] = nonce1 & 0xFF; - extseed[2][MLDSA_CRHBYTES] = nonce2 & 0xFF; - extseed[3][MLDSA_CRHBYTES] = nonce3 & 0xFF; - extseed[0][MLDSA_CRHBYTES + 1] = nonce0 >> 8; - extseed[1][MLDSA_CRHBYTES + 1] = nonce1 >> 8; - extseed[2][MLDSA_CRHBYTES + 1] = nonce2 >> 8; - extseed[3][MLDSA_CRHBYTES + 1] = nonce3 >> 8; - - mld_xof256_x4_init(&state); - mld_xof256_x4_absorb(&state, extseed, MLDSA_CRHBYTES + 2); - mld_xof256_x4_squeezeblocks(buf, POLY_UNIFORM_GAMMA1_NBLOCKS, &state); - - mld_polyz_unpack(r0, buf[0]); - mld_polyz_unpack(r1, buf[1]); - mld_polyz_unpack(r2, buf[2]); - mld_polyz_unpack(r3, buf[3]); - mld_xof256_x4_release(&state); - - /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */ - mld_zeroize(buf, sizeof(buf)); - mld_zeroize(extseed, sizeof(extseed)); -} - - -void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES]) -{ - unsigned int i, j, pos; - uint64_t signs; - uint64_t offset; - MLD_ALIGN uint8_t buf[SHAKE256_RATE]; - keccak_state state; - - shake256_init(&state); - shake256_absorb(&state, seed, MLDSA_CTILDEBYTES); - shake256_finalize(&state); - shake256_squeezeblocks(buf, 1, &state); - - /* Convert the first 8 bytes of buf[] into an unsigned 64-bit value. */ - /* Each bit of that dictates the sign of the resulting challenge value */ - signs = 0; - for (i = 0; i < 8; ++i) - __loop__( - assigns(i, signs) - invariant(i <= 8) - ) - { - signs |= (uint64_t)buf[i] << 8 * i; - } - pos = 8; - - memset(c, 0, sizeof(mld_poly)); - - for (i = MLDSA_N - MLDSA_TAU; i < MLDSA_N; ++i) - __loop__( - assigns(i, j, object_whole(buf), state, pos, memory_slice(c, sizeof(mld_poly)), signs) - invariant(i >= MLDSA_N - MLDSA_TAU) - invariant(i <= MLDSA_N) - invariant(pos >= 1) - invariant(pos <= SHAKE256_RATE) - invariant((&state)->pos <= SHAKE256_RATE) - invariant(array_bound(c->coeffs, 0, MLDSA_N, -1, 2)) - ) - { - do - __loop__( - assigns(j, object_whole(buf), state, pos) - invariant((&state)->pos <= SHAKE256_RATE) - ) - { - if (pos >= SHAKE256_RATE) - { - shake256_squeezeblocks(buf, 1, &state); - pos = 0; - } - j = buf[pos++]; - } while (j > i); - - c->coeffs[i] = c->coeffs[j]; - - /* Reference: Compute coefficent value here in two steps to */ - /* mixinf unsigned and signed arithmetic with implicit */ - /* conversions, and so that CBMC can keep track of ranges */ - /* to complete type-safety proof here. */ - - /* The least-significant bit of signs tells us if we want -1 or +1 */ - offset = 2 * (signs & 1); - - /* offset has value 0 or 2 here, so (1 - (int32_t) offset) has - * value -1 or +1 */ - c->coeffs[j] = 1 - (int32_t)offset; - - /* Move to the next bit of signs for next time */ - signs >>= 1; - } - - /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */ - mld_zeroize(buf, sizeof(buf)); - mld_zeroize(&signs, sizeof(signs)); - - mld_assert_bound(c->coeffs, MLDSA_N, -1, 2); -} - -void mld_polyeta_pack(uint8_t *r, const mld_poly *a) -{ - unsigned int i; - uint8_t t[8]; - - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_ETA + 1); - -#if MLDSA_ETA == 2 - for (i = 0; i < MLDSA_N / 8; ++i) - __loop__( - invariant(i <= MLDSA_N/8)) - { - t[0] = MLDSA_ETA - a->coeffs[8 * i + 0]; - t[1] = MLDSA_ETA - a->coeffs[8 * i + 1]; - t[2] = MLDSA_ETA - a->coeffs[8 * i + 2]; - t[3] = MLDSA_ETA - a->coeffs[8 * i + 3]; - t[4] = MLDSA_ETA - a->coeffs[8 * i + 4]; - t[5] = MLDSA_ETA - a->coeffs[8 * i + 5]; - t[6] = MLDSA_ETA - a->coeffs[8 * i + 6]; - t[7] = MLDSA_ETA - a->coeffs[8 * i + 7]; - - r[3 * i + 0] = ((t[0] >> 0) | (t[1] << 3) | (t[2] << 6)) & 0xFF; - r[3 * i + 1] = - ((t[2] >> 2) | (t[3] << 1) | (t[4] << 4) | (t[5] << 7)) & 0xFF; - r[3 * i + 2] = ((t[5] >> 1) | (t[6] << 2) | (t[7] << 5)) & 0xFF; - } -#elif MLDSA_ETA == 4 - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2)) - { - t[0] = MLDSA_ETA - a->coeffs[2 * i + 0]; - t[1] = MLDSA_ETA - a->coeffs[2 * i + 1]; - r[i] = t[0] | (t[1] << 4); - } -#else /* MLDSA_ETA == 4 */ -#error "Invalid value of MLDSA_ETA" -#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ -} - -void mld_polyeta_unpack(mld_poly *r, const uint8_t *a) -{ - unsigned int i; - -#if MLDSA_ETA == 2 - for (i = 0; i < MLDSA_N / 8; ++i) - __loop__( - invariant(i <= MLDSA_N/8) - invariant(array_bound(r->coeffs, 0, i*8, -5, MLDSA_ETA + 1))) - { - r->coeffs[8 * i + 0] = (a[3 * i + 0] >> 0) & 7; - r->coeffs[8 * i + 1] = (a[3 * i + 0] >> 3) & 7; - r->coeffs[8 * i + 2] = ((a[3 * i + 0] >> 6) | (a[3 * i + 1] << 2)) & 7; - r->coeffs[8 * i + 3] = (a[3 * i + 1] >> 1) & 7; - r->coeffs[8 * i + 4] = (a[3 * i + 1] >> 4) & 7; - r->coeffs[8 * i + 5] = ((a[3 * i + 1] >> 7) | (a[3 * i + 2] << 1)) & 7; - r->coeffs[8 * i + 6] = (a[3 * i + 2] >> 2) & 7; - r->coeffs[8 * i + 7] = (a[3 * i + 2] >> 5) & 7; - - r->coeffs[8 * i + 0] = MLDSA_ETA - r->coeffs[8 * i + 0]; - r->coeffs[8 * i + 1] = MLDSA_ETA - r->coeffs[8 * i + 1]; - r->coeffs[8 * i + 2] = MLDSA_ETA - r->coeffs[8 * i + 2]; - r->coeffs[8 * i + 3] = MLDSA_ETA - r->coeffs[8 * i + 3]; - r->coeffs[8 * i + 4] = MLDSA_ETA - r->coeffs[8 * i + 4]; - r->coeffs[8 * i + 5] = MLDSA_ETA - r->coeffs[8 * i + 5]; - r->coeffs[8 * i + 6] = MLDSA_ETA - r->coeffs[8 * i + 6]; - r->coeffs[8 * i + 7] = MLDSA_ETA - r->coeffs[8 * i + 7]; - } -#elif MLDSA_ETA == 4 - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2) - invariant(array_bound(r->coeffs, 0, i*2, -11, MLDSA_ETA + 1))) - { - r->coeffs[2 * i + 0] = a[i] & 0x0F; - r->coeffs[2 * i + 1] = a[i] >> 4; - r->coeffs[2 * i + 0] = MLDSA_ETA - r->coeffs[2 * i + 0]; - r->coeffs[2 * i + 1] = MLDSA_ETA - r->coeffs[2 * i + 1]; - } -#else /* MLDSA_ETA == 4 */ -#error "Invalid value of MLDSA_ETA" -#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ - - mld_assert_bound(r->coeffs, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, - MLDSA_ETA + 1); -} - void mld_polyt1_pack(uint8_t *r, const mld_poly *a) { unsigned int i; @@ -1034,139 +524,3 @@ void mld_polyt0_unpack(mld_poly *r, const uint8_t *a) mld_assert_bound(r->coeffs, MLDSA_N, -(1 << (MLDSA_D - 1)) + 1, (1 << (MLDSA_D - 1)) + 1); } - -void mld_polyz_pack(uint8_t *r, const mld_poly *a) -{ - unsigned int i; - uint32_t t[4]; - - mld_assert_bound(a->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - -#if MLDSA_MODE == 2 - for (i = 0; i < MLDSA_N / 4; ++i) - __loop__( - invariant(i <= MLDSA_N/4)) - { - t[0] = MLDSA_GAMMA1 - a->coeffs[4 * i + 0]; - t[1] = MLDSA_GAMMA1 - a->coeffs[4 * i + 1]; - t[2] = MLDSA_GAMMA1 - a->coeffs[4 * i + 2]; - t[3] = MLDSA_GAMMA1 - a->coeffs[4 * i + 3]; - - r[9 * i + 0] = (t[0]) & 0xFF; - r[9 * i + 1] = (t[0] >> 8) & 0xFF; - r[9 * i + 2] = (t[0] >> 16) & 0xFF; - r[9 * i + 2] |= (t[1] << 2) & 0xFF; - r[9 * i + 3] = (t[1] >> 6) & 0xFF; - r[9 * i + 4] = (t[1] >> 14) & 0xFF; - r[9 * i + 4] |= (t[2] << 4) & 0xFF; - r[9 * i + 5] = (t[2] >> 4) & 0xFF; - r[9 * i + 6] = (t[2] >> 12) & 0xFF; - r[9 * i + 6] |= (t[3] << 6) & 0xFF; - r[9 * i + 7] = (t[3] >> 2) & 0xFF; - r[9 * i + 8] = (t[3] >> 10) & 0xFF; - } -#else /* MLDSA_MODE == 2 */ - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2)) - { - t[0] = MLDSA_GAMMA1 - a->coeffs[2 * i + 0]; - t[1] = MLDSA_GAMMA1 - a->coeffs[2 * i + 1]; - - r[5 * i + 0] = (t[0]) & 0xFF; - r[5 * i + 1] = (t[0] >> 8) & 0xFF; - r[5 * i + 2] = (t[0] >> 16) & 0xFF; - r[5 * i + 2] |= (t[1] << 4) & 0xFF; - r[5 * i + 3] = (t[1] >> 4) & 0xFF; - r[5 * i + 4] = (t[1] >> 12) & 0xFF; - } -#endif /* MLDSA_MODE != 2 */ -} - -void mld_polyz_unpack(mld_poly *r, const uint8_t *a) -{ - unsigned int i; - -#if MLDSA_MODE == 2 - for (i = 0; i < MLDSA_N / 4; ++i) - __loop__( - invariant(i <= MLDSA_N/4) - invariant(array_bound(r->coeffs, 0, i*4, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - { - r->coeffs[4 * i + 0] = a[9 * i + 0]; - r->coeffs[4 * i + 0] |= (uint32_t)a[9 * i + 1] << 8; - r->coeffs[4 * i + 0] |= (uint32_t)a[9 * i + 2] << 16; - r->coeffs[4 * i + 0] &= 0x3FFFF; - - r->coeffs[4 * i + 1] = a[9 * i + 2] >> 2; - r->coeffs[4 * i + 1] |= (uint32_t)a[9 * i + 3] << 6; - r->coeffs[4 * i + 1] |= (uint32_t)a[9 * i + 4] << 14; - r->coeffs[4 * i + 1] &= 0x3FFFF; - - r->coeffs[4 * i + 2] = a[9 * i + 4] >> 4; - r->coeffs[4 * i + 2] |= (uint32_t)a[9 * i + 5] << 4; - r->coeffs[4 * i + 2] |= (uint32_t)a[9 * i + 6] << 12; - r->coeffs[4 * i + 2] &= 0x3FFFF; - - r->coeffs[4 * i + 3] = a[9 * i + 6] >> 6; - r->coeffs[4 * i + 3] |= (uint32_t)a[9 * i + 7] << 2; - r->coeffs[4 * i + 3] |= (uint32_t)a[9 * i + 8] << 10; - r->coeffs[4 * i + 3] &= 0x3FFFF; - - r->coeffs[4 * i + 0] = MLDSA_GAMMA1 - r->coeffs[4 * i + 0]; - r->coeffs[4 * i + 1] = MLDSA_GAMMA1 - r->coeffs[4 * i + 1]; - r->coeffs[4 * i + 2] = MLDSA_GAMMA1 - r->coeffs[4 * i + 2]; - r->coeffs[4 * i + 3] = MLDSA_GAMMA1 - r->coeffs[4 * i + 3]; - } -#else /* MLDSA_MODE == 2 */ - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2) - invariant(array_bound(r->coeffs, 0, i*2, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - { - r->coeffs[2 * i + 0] = a[5 * i + 0]; - r->coeffs[2 * i + 0] |= (uint32_t)a[5 * i + 1] << 8; - r->coeffs[2 * i + 0] |= (uint32_t)a[5 * i + 2] << 16; - r->coeffs[2 * i + 0] &= 0xFFFFF; - - r->coeffs[2 * i + 1] = a[5 * i + 2] >> 4; - r->coeffs[2 * i + 1] |= (uint32_t)a[5 * i + 3] << 4; - r->coeffs[2 * i + 1] |= (uint32_t)a[5 * i + 4] << 12; - /* r->coeffs[2*i+1] &= 0xFFFFF; */ /* No effect, since we're anyway at 20 - bits */ - - r->coeffs[2 * i + 0] = MLDSA_GAMMA1 - r->coeffs[2 * i + 0]; - r->coeffs[2 * i + 1] = MLDSA_GAMMA1 - r->coeffs[2 * i + 1]; - } -#endif /* MLDSA_MODE != 2 */ - - mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); -} - -void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) -{ - unsigned int i; - - mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); - -#if MLDSA_MODE == 2 - for (i = 0; i < MLDSA_N / 4; ++i) - __loop__( - invariant(i <= MLDSA_N/4)) - { - r[3 * i + 0] = (a->coeffs[4 * i + 0]) & 0xFF; - r[3 * i + 0] |= (a->coeffs[4 * i + 1] << 6) & 0xFF; - r[3 * i + 1] = (a->coeffs[4 * i + 1] >> 2) & 0xFF; - r[3 * i + 1] |= (a->coeffs[4 * i + 2] << 4) & 0xFF; - r[3 * i + 2] = (a->coeffs[4 * i + 2] >> 4) & 0xFF; - r[3 * i + 2] |= (a->coeffs[4 * i + 3] << 2) & 0xFF; - } -#else /* MLDSA_MODE == 2 */ - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2)) - { - r[i] = a->coeffs[2 * i + 0] | (a->coeffs[2 * i + 1] << 4); - } -#endif /* MLDSA_MODE != 2 */ -} diff --git a/mldsa/poly_k.c b/mldsa/poly_k.c new file mode 100644 index 00000000..1b8cb204 --- /dev/null +++ b/mldsa/poly_k.c @@ -0,0 +1,659 @@ +/* + * Copyright (c) The mldsa-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ +#include +#include + +#include "ct.h" +#include "debug.h" +#include "fips202/fips202x4.h" +#include "ntt.h" +#include "poly.h" +#include "reduce.h" +#include "rounding.h" +#include "symmetric.h" + +void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) +{ + unsigned int i; + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + + for (i = 0; i < MLDSA_N; ++i) + __loop__( + assigns(i, memory_slice(a0, sizeof(mld_poly)), memory_slice(a1, sizeof(mld_poly))) + invariant(i <= MLDSA_N) + invariant(array_bound(a1->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + invariant(array_abs_bound(a0->coeffs, 0, i, MLDSA_GAMMA2+1)) + ) + { + mld_decompose(&a0->coeffs[i], &a1->coeffs[i], a->coeffs[i]); + } + + mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2 + 1); + mld_assert_bound(a1->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); +} + +unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, + const mld_poly *a1) +{ + unsigned int i, s = 0; + + for (i = 0; i < MLDSA_N; ++i) + __loop__( + invariant(i <= MLDSA_N) + invariant(s <= i) + invariant(array_bound(h->coeffs, 0, i, 0, 2)) + ) + { + const unsigned int hint_bit = mld_make_hint(a0->coeffs[i], a1->coeffs[i]); + h->coeffs[i] = hint_bit; + s += hint_bit; + } + + mld_assert(s <= MLDSA_N); + return s; +} + +void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) +{ + unsigned int i; + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); + + for (i = 0; i < MLDSA_N; ++i) + __loop__( + invariant(i <= MLDSA_N) + invariant(array_bound(b->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ) + { + b->coeffs[i] = mld_use_hint(a->coeffs[i], h->coeffs[i]); + } + + mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); +} + +/************************************************* + * Name: mld_rej_eta + * + * Description: Sample uniformly random coefficients in [-MLDSA_ETA, MLDSA_ETA] + *by performing rejection sampling on array of random bytes. + * + * Arguments: - int32_t *a: pointer to output array (allocated) + * - unsigned int target: requested number of coefficients to + *sample + * - unsigned int offset: number of coefficients already sampled + * - const uint8_t *buf: array of random bytes to sample from + * - unsigned int buflen: length of array of random bytes + * + * Returns number of sampled coefficients. Can be smaller than target if not + *enough random bytes were given. + **************************************************/ + +/* Reference: `mld_rej_eta()` in the reference implementation [@REF]. + * - Our signature differs from the reference implementation + * in that it adds the offset and always expects the base of the + * target buffer. This avoids shifting the buffer base in the + * caller, which appears tricky to reason about. */ +#if MLDSA_ETA == 2 +/* + * Sampling 256 coefficients mod 15 using rejection sampling from 4 bits. + * Expected number of required bytes: (256 * (16/15))/2 = 136.5 bytes. + * We sample 1 block (=136 bytes) of SHAKE256_RATE output initially. + * Sampling 2 blocks initially results in slightly worse performance. + */ +#define POLY_UNIFORM_ETA_NBLOCKS 1 +#elif MLDSA_ETA == 4 +/* + * Sampling 256 coefficients mod 9 using rejection sampling from 4 bits. + * Expected number of required bytes: (256 * (16/9))/2 = 227.5 bytes. + * We sample 2 blocks (=272 bytes) of SHAKE256_RATE output initially. + */ +#define POLY_UNIFORM_ETA_NBLOCKS 2 +#else /* MLDSA_ETA == 4 */ +#error "Invalid value of MLDSA_ETA" +#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ +static unsigned int mld_rej_eta(int32_t *a, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen) +__contract__( + requires(offset <= target && target <= MLDSA_N) + requires(buflen <= (POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)) + requires(memory_no_alias(a, sizeof(int32_t) * target)) + requires(memory_no_alias(buf, buflen)) + requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) + assigns(memory_slice(a, sizeof(int32_t) * target)) + ensures(offset <= return_value && return_value <= target) + ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) +) +{ + unsigned int ctr, pos; + int t_valid; + uint32_t t0, t1; + +/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */ +#if MLDSA_ETA == 2 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) + if (offset == 0) + { + int ret = mld_rej_uniform_eta2_native(a, target, buf, buflen); + if (ret != -1) + { + unsigned res = (unsigned)ret; + mld_assert_abs_bound(a, res, MLDSA_ETA + 1); + return res; + } + } +/* TODO: CBMC proof based on mld_rej_uniform_eta4_native */ +#elif MLDSA_ETA == 4 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) + if (offset == 0) + { + int ret = mld_rej_uniform_eta4_native(a, target, buf, buflen); + if (ret != -1) + { + unsigned res = (unsigned)ret; + mld_assert_abs_bound(a, res, MLDSA_ETA + 1); + return res; + } + } +#endif /* !(MLDSA_ETA == 2 && MLD_USE_NATIVE_REJ_UNIFORM_ETA2) && MLDSA_ETA == \ + 4 && MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */ + + ctr = offset; + pos = 0; + while (ctr < target && pos < buflen) + __loop__( + invariant(offset <= ctr && ctr <= target && pos <= buflen) + invariant(array_abs_bound(a, 0, ctr, MLDSA_ETA + 1)) + ) + { + t0 = buf[pos] & 0x0F; + t1 = buf[pos++] >> 4; + + /* Constant time: The inputs and outputs to the rejection sampling are + * secret. However, it is fine to leak which coefficients have been + * rejected. For constant-time testing, we declassify the result of + * the comparison. + */ +#if MLDSA_ETA == 2 + t_valid = t0 < 15; + MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); + if (t_valid) /* t0 < 15 */ + { + t0 = t0 - (205 * t0 >> 10) * 5; + a[ctr++] = 2 - (int32_t)t0; + } + t_valid = t1 < 15; + MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); + if (t_valid && ctr < target) /* t1 < 15 */ + { + t1 = t1 - (205 * t1 >> 10) * 5; + a[ctr++] = 2 - (int32_t)t1; + } +#elif MLDSA_ETA == 4 + t_valid = t0 < 9; + MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); + if (t_valid) /* t0 < 9 */ + { + a[ctr++] = 4 - (int32_t)t0; + } + t_valid = t1 < 9; /* t1 < 9 */ + MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); + if (t_valid && ctr < target) + { + a[ctr++] = 4 - (int32_t)t1; + } +#else /* MLDSA_ETA == 4 */ +#error "Invalid value of MLDSA_ETA" +#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ + } + + return ctr; +} +void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, + mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES], + uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, + uint8_t nonce3) +{ + /* Temporary buffers for XOF output before rejection sampling */ + MLD_ALIGN uint8_t + buf[4][MLD_ALIGN_UP(POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)]; + + MLD_ALIGN uint8_t extseed[4][MLD_ALIGN_UP(MLDSA_CRHBYTES + 2)]; + + /* Tracks the number of coefficients we have already sampled */ + unsigned ctr[4]; + mld_xof256_x4_ctx state; + unsigned buflen; + + memcpy(extseed[0], seed, MLDSA_CRHBYTES); + memcpy(extseed[1], seed, MLDSA_CRHBYTES); + memcpy(extseed[2], seed, MLDSA_CRHBYTES); + memcpy(extseed[3], seed, MLDSA_CRHBYTES); + extseed[0][MLDSA_CRHBYTES] = nonce0; + extseed[1][MLDSA_CRHBYTES] = nonce1; + extseed[2][MLDSA_CRHBYTES] = nonce2; + extseed[3][MLDSA_CRHBYTES] = nonce3; + extseed[0][MLDSA_CRHBYTES + 1] = 0; + extseed[1][MLDSA_CRHBYTES + 1] = 0; + extseed[2][MLDSA_CRHBYTES + 1] = 0; + extseed[3][MLDSA_CRHBYTES + 1] = 0; + + mld_xof256_x4_init(&state); + mld_xof256_x4_absorb(&state, extseed, MLDSA_CRHBYTES + 2); + + /* + * Initially, squeeze heuristic number of POLY_UNIFORM_ETA_NBLOCKS. + * This should generate the coefficients with high probability. + */ + mld_xof256_x4_squeezeblocks(buf, POLY_UNIFORM_ETA_NBLOCKS, &state); + buflen = POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES; + + ctr[0] = mld_rej_eta(r0->coeffs, MLDSA_N, 0, buf[0], buflen); + ctr[1] = mld_rej_eta(r1->coeffs, MLDSA_N, 0, buf[1], buflen); + ctr[2] = mld_rej_eta(r2->coeffs, MLDSA_N, 0, buf[2], buflen); + ctr[3] = mld_rej_eta(r3->coeffs, MLDSA_N, 0, buf[3], buflen); + + /* + * So long as not all entries have been generated, squeeze + * one more block a time until we're done. + */ + buflen = STREAM256_BLOCKBYTES; + while (ctr[0] < MLDSA_N || ctr[1] < MLDSA_N || ctr[2] < MLDSA_N || + ctr[3] < MLDSA_N) + __loop__( + assigns(ctr, state, memory_slice(r0, sizeof(mld_poly)), + memory_slice(r1, sizeof(mld_poly)), memory_slice(r2, sizeof(mld_poly)), + memory_slice(r3, sizeof(mld_poly)), object_whole(buf[0]), + object_whole(buf[1]), object_whole(buf[2]), + object_whole(buf[3])) + invariant(ctr[0] <= MLDSA_N && ctr[1] <= MLDSA_N) + invariant(ctr[2] <= MLDSA_N && ctr[3] <= MLDSA_N) + invariant(array_abs_bound(r0->coeffs, 0, ctr[0], MLDSA_ETA + 1)) + invariant(array_abs_bound(r1->coeffs, 0, ctr[1], MLDSA_ETA + 1)) + invariant(array_abs_bound(r2->coeffs, 0, ctr[2], MLDSA_ETA + 1)) + invariant(array_abs_bound(r3->coeffs, 0, ctr[3], MLDSA_ETA + 1))) + { + mld_xof256_x4_squeezeblocks(buf, 1, &state); + ctr[0] = mld_rej_eta(r0->coeffs, MLDSA_N, ctr[0], buf[0], buflen); + ctr[1] = mld_rej_eta(r1->coeffs, MLDSA_N, ctr[1], buf[1], buflen); + ctr[2] = mld_rej_eta(r2->coeffs, MLDSA_N, ctr[2], buf[2], buflen); + ctr[3] = mld_rej_eta(r3->coeffs, MLDSA_N, ctr[3], buf[3], buflen); + } + + mld_xof256_x4_release(&state); + + /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */ + mld_zeroize(buf, sizeof(buf)); + mld_zeroize(extseed, sizeof(extseed)); +} + + +#define POLY_UNIFORM_GAMMA1_NBLOCKS \ + ((MLDSA_POLYZ_PACKEDBYTES + STREAM256_BLOCKBYTES - 1) / STREAM256_BLOCKBYTES) +void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES], + uint16_t nonce) +{ + MLD_ALIGN uint8_t buf[POLY_UNIFORM_GAMMA1_NBLOCKS * STREAM256_BLOCKBYTES]; + MLD_ALIGN uint8_t extseed[MLDSA_CRHBYTES + 2]; + mld_xof256_ctx state; + + memcpy(extseed, seed, MLDSA_CRHBYTES); + extseed[MLDSA_CRHBYTES] = nonce & 0xFF; + extseed[MLDSA_CRHBYTES + 1] = nonce >> 8; + + mld_xof256_init(&state); + mld_xof256_absorb(&state, extseed, MLDSA_CRHBYTES + 2); + + mld_xof256_squeezeblocks(buf, POLY_UNIFORM_GAMMA1_NBLOCKS, &state); + mld_polyz_unpack(a, buf); + + mld_xof256_release(&state); + + /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */ + mld_zeroize(buf, sizeof(buf)); + mld_zeroize(extseed, sizeof(extseed)); +} + +void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, + mld_poly *r3, + const uint8_t seed[MLDSA_CRHBYTES], + uint16_t nonce0, uint16_t nonce1, + uint16_t nonce2, uint16_t nonce3) +{ + /* Temporary buffers for XOF output before rejection sampling */ + MLD_ALIGN uint8_t + buf[4][MLD_ALIGN_UP(POLY_UNIFORM_GAMMA1_NBLOCKS * STREAM256_BLOCKBYTES)]; + + MLD_ALIGN uint8_t extseed[4][MLD_ALIGN_UP(MLDSA_CRHBYTES + 2)]; + + /* Tracks the number of coefficients we have already sampled */ + mld_xof256_x4_ctx state; + + memcpy(extseed[0], seed, MLDSA_CRHBYTES); + memcpy(extseed[1], seed, MLDSA_CRHBYTES); + memcpy(extseed[2], seed, MLDSA_CRHBYTES); + memcpy(extseed[3], seed, MLDSA_CRHBYTES); + extseed[0][MLDSA_CRHBYTES] = nonce0 & 0xFF; + extseed[1][MLDSA_CRHBYTES] = nonce1 & 0xFF; + extseed[2][MLDSA_CRHBYTES] = nonce2 & 0xFF; + extseed[3][MLDSA_CRHBYTES] = nonce3 & 0xFF; + extseed[0][MLDSA_CRHBYTES + 1] = nonce0 >> 8; + extseed[1][MLDSA_CRHBYTES + 1] = nonce1 >> 8; + extseed[2][MLDSA_CRHBYTES + 1] = nonce2 >> 8; + extseed[3][MLDSA_CRHBYTES + 1] = nonce3 >> 8; + + mld_xof256_x4_init(&state); + mld_xof256_x4_absorb(&state, extseed, MLDSA_CRHBYTES + 2); + mld_xof256_x4_squeezeblocks(buf, POLY_UNIFORM_GAMMA1_NBLOCKS, &state); + + mld_polyz_unpack(r0, buf[0]); + mld_polyz_unpack(r1, buf[1]); + mld_polyz_unpack(r2, buf[2]); + mld_polyz_unpack(r3, buf[3]); + mld_xof256_x4_release(&state); + + /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */ + mld_zeroize(buf, sizeof(buf)); + mld_zeroize(extseed, sizeof(extseed)); +} + +void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES]) +{ + unsigned int i, j, pos; + uint64_t signs; + uint64_t offset; + MLD_ALIGN uint8_t buf[SHAKE256_RATE]; + keccak_state state; + + shake256_init(&state); + shake256_absorb(&state, seed, MLDSA_CTILDEBYTES); + shake256_finalize(&state); + shake256_squeezeblocks(buf, 1, &state); + + /* Convert the first 8 bytes of buf[] into an unsigned 64-bit value. */ + /* Each bit of that dictates the sign of the resulting challenge value */ + signs = 0; + for (i = 0; i < 8; ++i) + __loop__( + assigns(i, signs) + invariant(i <= 8) + ) + { + signs |= (uint64_t)buf[i] << 8 * i; + } + pos = 8; + + memset(c, 0, sizeof(mld_poly)); + + for (i = MLDSA_N - MLDSA_TAU; i < MLDSA_N; ++i) + __loop__( + assigns(i, j, object_whole(buf), state, pos, memory_slice(c, sizeof(mld_poly)), signs) + invariant(i >= MLDSA_N - MLDSA_TAU) + invariant(i <= MLDSA_N) + invariant(pos >= 1) + invariant(pos <= SHAKE256_RATE) + invariant((&state)->pos <= SHAKE256_RATE) + invariant(array_bound(c->coeffs, 0, MLDSA_N, -1, 2)) + ) + { + do + __loop__( + assigns(j, object_whole(buf), state, pos) + invariant((&state)->pos <= SHAKE256_RATE) + ) + { + if (pos >= SHAKE256_RATE) + { + shake256_squeezeblocks(buf, 1, &state); + pos = 0; + } + j = buf[pos++]; + } while (j > i); + + c->coeffs[i] = c->coeffs[j]; + + /* Reference: Compute coefficent value here in two steps to */ + /* mixinf unsigned and signed arithmetic with implicit */ + /* conversions, and so that CBMC can keep track of ranges */ + /* to complete type-safety proof here. */ + + /* The least-significant bit of signs tells us if we want -1 or +1 */ + offset = 2 * (signs & 1); + + /* offset has value 0 or 2 here, so (1 - (int32_t) offset) has + * value -1 or +1 */ + c->coeffs[j] = 1 - (int32_t)offset; + + /* Move to the next bit of signs for next time */ + signs >>= 1; + } + + /* FIPS 204. Section 3.6.3 Destruction of intermediate values. */ + mld_zeroize(buf, sizeof(buf)); + mld_zeroize(&signs, sizeof(signs)); + + mld_assert_bound(c->coeffs, MLDSA_N, -1, 2); +} + +void mld_polyeta_pack(uint8_t *r, const mld_poly *a) +{ + unsigned int i; + uint8_t t[8]; + + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_ETA + 1); + +#if MLDSA_ETA == 2 + for (i = 0; i < MLDSA_N / 8; ++i) + __loop__( + invariant(i <= MLDSA_N/8)) + { + t[0] = MLDSA_ETA - a->coeffs[8 * i + 0]; + t[1] = MLDSA_ETA - a->coeffs[8 * i + 1]; + t[2] = MLDSA_ETA - a->coeffs[8 * i + 2]; + t[3] = MLDSA_ETA - a->coeffs[8 * i + 3]; + t[4] = MLDSA_ETA - a->coeffs[8 * i + 4]; + t[5] = MLDSA_ETA - a->coeffs[8 * i + 5]; + t[6] = MLDSA_ETA - a->coeffs[8 * i + 6]; + t[7] = MLDSA_ETA - a->coeffs[8 * i + 7]; + + r[3 * i + 0] = ((t[0] >> 0) | (t[1] << 3) | (t[2] << 6)) & 0xFF; + r[3 * i + 1] = + ((t[2] >> 2) | (t[3] << 1) | (t[4] << 4) | (t[5] << 7)) & 0xFF; + r[3 * i + 2] = ((t[5] >> 1) | (t[6] << 2) | (t[7] << 5)) & 0xFF; + } +#elif MLDSA_ETA == 4 + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2)) + { + t[0] = MLDSA_ETA - a->coeffs[2 * i + 0]; + t[1] = MLDSA_ETA - a->coeffs[2 * i + 1]; + r[i] = t[0] | (t[1] << 4); + } +#else /* MLDSA_ETA == 4 */ +#error "Invalid value of MLDSA_ETA" +#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ +} + +void mld_polyeta_unpack(mld_poly *r, const uint8_t *a) +{ + unsigned int i; + +#if MLDSA_ETA == 2 + for (i = 0; i < MLDSA_N / 8; ++i) + __loop__( + invariant(i <= MLDSA_N/8) + invariant(array_bound(r->coeffs, 0, i*8, -5, MLDSA_ETA + 1))) + { + r->coeffs[8 * i + 0] = (a[3 * i + 0] >> 0) & 7; + r->coeffs[8 * i + 1] = (a[3 * i + 0] >> 3) & 7; + r->coeffs[8 * i + 2] = ((a[3 * i + 0] >> 6) | (a[3 * i + 1] << 2)) & 7; + r->coeffs[8 * i + 3] = (a[3 * i + 1] >> 1) & 7; + r->coeffs[8 * i + 4] = (a[3 * i + 1] >> 4) & 7; + r->coeffs[8 * i + 5] = ((a[3 * i + 1] >> 7) | (a[3 * i + 2] << 1)) & 7; + r->coeffs[8 * i + 6] = (a[3 * i + 2] >> 2) & 7; + r->coeffs[8 * i + 7] = (a[3 * i + 2] >> 5) & 7; + + r->coeffs[8 * i + 0] = MLDSA_ETA - r->coeffs[8 * i + 0]; + r->coeffs[8 * i + 1] = MLDSA_ETA - r->coeffs[8 * i + 1]; + r->coeffs[8 * i + 2] = MLDSA_ETA - r->coeffs[8 * i + 2]; + r->coeffs[8 * i + 3] = MLDSA_ETA - r->coeffs[8 * i + 3]; + r->coeffs[8 * i + 4] = MLDSA_ETA - r->coeffs[8 * i + 4]; + r->coeffs[8 * i + 5] = MLDSA_ETA - r->coeffs[8 * i + 5]; + r->coeffs[8 * i + 6] = MLDSA_ETA - r->coeffs[8 * i + 6]; + r->coeffs[8 * i + 7] = MLDSA_ETA - r->coeffs[8 * i + 7]; + } +#elif MLDSA_ETA == 4 + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2) + invariant(array_bound(r->coeffs, 0, i*2, -11, MLDSA_ETA + 1))) + { + r->coeffs[2 * i + 0] = a[i] & 0x0F; + r->coeffs[2 * i + 1] = a[i] >> 4; + r->coeffs[2 * i + 0] = MLDSA_ETA - r->coeffs[2 * i + 0]; + r->coeffs[2 * i + 1] = MLDSA_ETA - r->coeffs[2 * i + 1]; + } +#else /* MLDSA_ETA == 4 */ +#error "Invalid value of MLDSA_ETA" +#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ + + mld_assert_bound(r->coeffs, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, + MLDSA_ETA + 1); +} +void mld_polyz_pack(uint8_t *r, const mld_poly *a) +{ + unsigned int i; + uint32_t t[4]; + + mld_assert_bound(a->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + +#if MLDSA_MODE == 2 + for (i = 0; i < MLDSA_N / 4; ++i) + __loop__( + invariant(i <= MLDSA_N/4)) + { + t[0] = MLDSA_GAMMA1 - a->coeffs[4 * i + 0]; + t[1] = MLDSA_GAMMA1 - a->coeffs[4 * i + 1]; + t[2] = MLDSA_GAMMA1 - a->coeffs[4 * i + 2]; + t[3] = MLDSA_GAMMA1 - a->coeffs[4 * i + 3]; + + r[9 * i + 0] = (t[0]) & 0xFF; + r[9 * i + 1] = (t[0] >> 8) & 0xFF; + r[9 * i + 2] = (t[0] >> 16) & 0xFF; + r[9 * i + 2] |= (t[1] << 2) & 0xFF; + r[9 * i + 3] = (t[1] >> 6) & 0xFF; + r[9 * i + 4] = (t[1] >> 14) & 0xFF; + r[9 * i + 4] |= (t[2] << 4) & 0xFF; + r[9 * i + 5] = (t[2] >> 4) & 0xFF; + r[9 * i + 6] = (t[2] >> 12) & 0xFF; + r[9 * i + 6] |= (t[3] << 6) & 0xFF; + r[9 * i + 7] = (t[3] >> 2) & 0xFF; + r[9 * i + 8] = (t[3] >> 10) & 0xFF; + } +#else /* MLDSA_MODE == 2 */ + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2)) + { + t[0] = MLDSA_GAMMA1 - a->coeffs[2 * i + 0]; + t[1] = MLDSA_GAMMA1 - a->coeffs[2 * i + 1]; + + r[5 * i + 0] = (t[0]) & 0xFF; + r[5 * i + 1] = (t[0] >> 8) & 0xFF; + r[5 * i + 2] = (t[0] >> 16) & 0xFF; + r[5 * i + 2] |= (t[1] << 4) & 0xFF; + r[5 * i + 3] = (t[1] >> 4) & 0xFF; + r[5 * i + 4] = (t[1] >> 12) & 0xFF; + } +#endif /* MLDSA_MODE != 2 */ +} + + +void mld_polyz_unpack(mld_poly *r, const uint8_t *a) +{ + unsigned int i; + +#if MLDSA_MODE == 2 + for (i = 0; i < MLDSA_N / 4; ++i) + __loop__( + invariant(i <= MLDSA_N/4) + invariant(array_bound(r->coeffs, 0, i*4, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) + { + r->coeffs[4 * i + 0] = a[9 * i + 0]; + r->coeffs[4 * i + 0] |= (uint32_t)a[9 * i + 1] << 8; + r->coeffs[4 * i + 0] |= (uint32_t)a[9 * i + 2] << 16; + r->coeffs[4 * i + 0] &= 0x3FFFF; + + r->coeffs[4 * i + 1] = a[9 * i + 2] >> 2; + r->coeffs[4 * i + 1] |= (uint32_t)a[9 * i + 3] << 6; + r->coeffs[4 * i + 1] |= (uint32_t)a[9 * i + 4] << 14; + r->coeffs[4 * i + 1] &= 0x3FFFF; + + r->coeffs[4 * i + 2] = a[9 * i + 4] >> 4; + r->coeffs[4 * i + 2] |= (uint32_t)a[9 * i + 5] << 4; + r->coeffs[4 * i + 2] |= (uint32_t)a[9 * i + 6] << 12; + r->coeffs[4 * i + 2] &= 0x3FFFF; + + r->coeffs[4 * i + 3] = a[9 * i + 6] >> 6; + r->coeffs[4 * i + 3] |= (uint32_t)a[9 * i + 7] << 2; + r->coeffs[4 * i + 3] |= (uint32_t)a[9 * i + 8] << 10; + r->coeffs[4 * i + 3] &= 0x3FFFF; + + r->coeffs[4 * i + 0] = MLDSA_GAMMA1 - r->coeffs[4 * i + 0]; + r->coeffs[4 * i + 1] = MLDSA_GAMMA1 - r->coeffs[4 * i + 1]; + r->coeffs[4 * i + 2] = MLDSA_GAMMA1 - r->coeffs[4 * i + 2]; + r->coeffs[4 * i + 3] = MLDSA_GAMMA1 - r->coeffs[4 * i + 3]; + } +#else /* MLDSA_MODE == 2 */ + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2) + invariant(array_bound(r->coeffs, 0, i*2, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) + { + r->coeffs[2 * i + 0] = a[5 * i + 0]; + r->coeffs[2 * i + 0] |= (uint32_t)a[5 * i + 1] << 8; + r->coeffs[2 * i + 0] |= (uint32_t)a[5 * i + 2] << 16; + r->coeffs[2 * i + 0] &= 0xFFFFF; + + r->coeffs[2 * i + 1] = a[5 * i + 2] >> 4; + r->coeffs[2 * i + 1] |= (uint32_t)a[5 * i + 3] << 4; + r->coeffs[2 * i + 1] |= (uint32_t)a[5 * i + 4] << 12; + /* r->coeffs[2*i+1] &= 0xFFFFF; */ /* No effect, since we're anyway at 20 + bits */ + + r->coeffs[2 * i + 0] = MLDSA_GAMMA1 - r->coeffs[2 * i + 0]; + r->coeffs[2 * i + 1] = MLDSA_GAMMA1 - r->coeffs[2 * i + 1]; + } +#endif /* MLDSA_MODE != 2 */ + + mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); +} + +void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) +{ + unsigned int i; + + mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); + +#if MLDSA_MODE == 2 + for (i = 0; i < MLDSA_N / 4; ++i) + __loop__( + invariant(i <= MLDSA_N/4)) + { + r[3 * i + 0] = (a->coeffs[4 * i + 0]) & 0xFF; + r[3 * i + 0] |= (a->coeffs[4 * i + 1] << 6) & 0xFF; + r[3 * i + 1] = (a->coeffs[4 * i + 1] >> 2) & 0xFF; + r[3 * i + 1] |= (a->coeffs[4 * i + 2] << 4) & 0xFF; + r[3 * i + 2] = (a->coeffs[4 * i + 2] >> 4) & 0xFF; + r[3 * i + 2] |= (a->coeffs[4 * i + 3] << 2) & 0xFF; + } +#else /* MLDSA_MODE == 2 */ + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2)) + { + r[i] = a->coeffs[2 * i + 0] | (a->coeffs[2 * i + 1] << 4); + } +#endif /* MLDSA_MODE != 2 */ +} From 8790846644055a5f3ebba5fa8f5fe9ec6fb61a1f Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Wed, 3 Sep 2025 17:45:30 -0700 Subject: [PATCH 2/2] Fix CBMC proofs Signed-off-by: Jake Massimo --- proofs/cbmc/poly_challenge/Makefile | 2 +- proofs/cbmc/poly_decompose/Makefile | 2 +- proofs/cbmc/poly_make_hint/Makefile | 2 +- proofs/cbmc/poly_uniform_eta_4x/Makefile | 2 +- proofs/cbmc/poly_uniform_gamma1/Makefile | 2 +- proofs/cbmc/poly_uniform_gamma1_4x/Makefile | 2 +- proofs/cbmc/poly_use_hint/Makefile | 2 +- proofs/cbmc/polyeta_pack/Makefile | 2 +- proofs/cbmc/polyeta_unpack/Makefile | 2 +- proofs/cbmc/polyw1_pack/Makefile | 2 +- proofs/cbmc/polyz_pack/Makefile | 2 +- proofs/cbmc/polyz_unpack/Makefile | 2 +- proofs/cbmc/rej_eta/Makefile | 2 +- 13 files changed, 13 insertions(+), 13 deletions(-) diff --git a/proofs/cbmc/poly_challenge/Makefile b/proofs/cbmc/poly_challenge/Makefile index 9c9edd0d..9c7e01f0 100644 --- a/proofs/cbmc/poly_challenge/Makefile +++ b/proofs/cbmc/poly_challenge/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_challenge USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_finalize $(FIPS202_NAMESPACE)shake256_squeezeblocks diff --git a/proofs/cbmc/poly_decompose/Makefile b/proofs/cbmc/poly_decompose/Makefile index 5b50ef87..75288e18 100644 --- a/proofs/cbmc/poly_decompose/Makefile +++ b/proofs/cbmc/poly_decompose/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_decompose USE_FUNCTION_CONTRACTS=mld_decompose diff --git a/proofs/cbmc/poly_make_hint/Makefile b/proofs/cbmc/poly_make_hint/Makefile index 22386569..6e754705 100644 --- a/proofs/cbmc/poly_make_hint/Makefile +++ b/proofs/cbmc/poly_make_hint/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_make_hint USE_FUNCTION_CONTRACTS=mld_make_hint diff --git a/proofs/cbmc/poly_uniform_eta_4x/Makefile b/proofs/cbmc/poly_uniform_eta_4x/Makefile index c36e03f6..f33bc8ed 100644 --- a/proofs/cbmc/poly_uniform_eta_4x/Makefile +++ b/proofs/cbmc/poly_uniform_eta_4x/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202x4.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c $(SRCDIR)/mldsa/fips202/fips202x4.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta_4x USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256x4_absorb_once $(FIPS202_NAMESPACE)shake256x4_squeezeblocks mld_rej_eta diff --git a/proofs/cbmc/poly_uniform_gamma1/Makefile b/proofs/cbmc/poly_uniform_gamma1/Makefile index 66ca915e..cdda7a86 100644 --- a/proofs/cbmc/poly_uniform_gamma1/Makefile +++ b/proofs/cbmc/poly_uniform_gamma1/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c $(SRCDIR)/mldsa/fips202/fips202.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_gamma1 USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_finalize $(FIPS202_NAMESPACE)shake256_squeezeblocks $(MLD_NAMESPACE)polyz_unpack diff --git a/proofs/cbmc/poly_uniform_gamma1_4x/Makefile b/proofs/cbmc/poly_uniform_gamma1_4x/Makefile index e3e497bf..1215b248 100644 --- a/proofs/cbmc/poly_uniform_gamma1_4x/Makefile +++ b/proofs/cbmc/poly_uniform_gamma1_4x/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202x4.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c $(SRCDIR)/mldsa/fips202/fips202x4.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_gamma1_4x USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256x4_absorb_once $(FIPS202_NAMESPACE)shake256x4_squeezeblocks $(MLD_NAMESPACE)polyz_unpack diff --git a/proofs/cbmc/poly_use_hint/Makefile b/proofs/cbmc/poly_use_hint/Makefile index 883fefa4..d3cb890d 100644 --- a/proofs/cbmc/poly_use_hint/Makefile +++ b/proofs/cbmc/poly_use_hint/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_use_hint USE_FUNCTION_CONTRACTS=mld_use_hint diff --git a/proofs/cbmc/polyeta_pack/Makefile b/proofs/cbmc/polyeta_pack/Makefile index e0341e2a..b0ff55e6 100644 --- a/proofs/cbmc/polyeta_pack/Makefile +++ b/proofs/cbmc/polyeta_pack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_pack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/polyeta_unpack/Makefile b/proofs/cbmc/polyeta_unpack/Makefile index 1ed697af..999a87a1 100644 --- a/proofs/cbmc/polyeta_unpack/Makefile +++ b/proofs/cbmc/polyeta_unpack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_unpack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/polyw1_pack/Makefile b/proofs/cbmc/polyw1_pack/Makefile index 807daf60..c3447922 100644 --- a/proofs/cbmc/polyw1_pack/Makefile +++ b/proofs/cbmc/polyw1_pack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyw1_pack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/polyz_pack/Makefile b/proofs/cbmc/polyz_pack/Makefile index ef47c44d..1b212868 100644 --- a/proofs/cbmc/polyz_pack/Makefile +++ b/proofs/cbmc/polyz_pack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_pack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/polyz_unpack/Makefile b/proofs/cbmc/polyz_unpack/Makefile index be3e4aa0..e3073cb4 100644 --- a/proofs/cbmc/polyz_unpack/Makefile +++ b/proofs/cbmc/polyz_unpack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_unpack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/rej_eta/Makefile b/proofs/cbmc/rej_eta/Makefile index eaadab2b..c40db0b5 100644 --- a/proofs/cbmc/rej_eta/Makefile +++ b/proofs/cbmc/rej_eta/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_k.c CHECK_FUNCTION_CONTRACTS=mld_rej_eta USE_FUNCTION_CONTRACTS=