diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index 09f3ab00b..f3e89c245 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -164,126 +164,146 @@ void mld_poly_shiftl(mld_poly *a) } #endif /* !MLD_CONFIG_NO_VERIFY_API */ -static MLD_INLINE int32_t mld_fqmul(int32_t a, int32_t b) +/* + * Montgomery multiplication with precomputed twist + * + * b_twisted is the precomputed b * MLDSA_Q^{-1} mod 2^32 (signed canonical). + */ +static MLD_INLINE int32_t mld_fqmul(int32_t a, int32_t b, int32_t b_twisted) __contract__( requires(b > -MLDSA_Q_HALF && b < MLDSA_Q_HALF) ensures(return_value > -MLDSA_Q && return_value < MLDSA_Q) ) { - /* Bounds: We argue in mld_montgomery_reduce() that the reult - * of Montgomery reduction is < MLDSA_Q if the input is smaller - * than 2^31 * MLDSA_Q in absolute value. Indeed, we have: - * - * |a * b| = |a| * |b| - * < 2^31 * MLDSA_Q_HALF - * < 2^31 * MLDSA_Q - */ - return mld_montgomery_reduce((int64_t)a * (int64_t)b); + /* High 32 bits of the signed product a * b. */ + const int32_t prod_hi = (int32_t)(((int64_t)a * b) >> 32); + /* Low 32 bits of a * b_twisted (== a * b * q^{-1} mod 2^32), taken in + * unsigned 64-bit then narrowed; the explicit `& UINT32_MAX` is a no-op + * for the value, but silences CBMC's unsigned-conversion overflow check + * on the implicit uint64_t->uint32_t narrowing. */ + const uint32_t prod_lo_t_u = + (uint32_t)(((uint64_t)mld_cast_int32_to_uint32(a) * + mld_cast_int32_to_uint32(b_twisted)) & + UINT32_MAX); + const int32_t prod_lo_t = mld_cast_uint32_to_int32(prod_lo_t_u); + /* High 32 bits of prod_lo_t * Q. */ + const int32_t correction = (int32_t)(((int64_t)prod_lo_t * MLDSA_Q) >> 32); + return prod_hi - correction; } -/* mld_ntt_butterfly_block() - * - * Computes a block CT butterflies with a fixed twiddle factor, - * using Montgomery multiplication. +/* Cooley-Tukey butterfly */ +static MLD_INLINE void mld_ct_butterfly(int32_t r[MLDSA_N], unsigned i, + unsigned j, int32_t z, int32_t zt) +{ + const int32_t t = mld_fqmul(r[j], z, zt); + r[j] = r[i] - t; + r[i] = r[i] + t; +} + +/* Gentleman-Sande butterfly * - * Parameters: - * - r: Pointer to base of polynomial (_not_ the base of butterfly block) - * - zeta: Twiddle factor to use for the butterfly. This must be in - * Montgomery form and signed canonical. - * - start: Offset to the beginning of the butterfly block - * - len: Index difference between coefficients subject to a butterfly - * - bound: Ghost variable describing coefficient bound: Prior to `start`, - * coefficients must be bound by `bound + MLDSA_Q`. Post `start`, - * they must be bound by `bound`. - * When this function returns, output coefficients in the index range - * [start, start+2*len) have bound bumped to `bound + MLDSA_Q`. - * Example: - * - start=8, len=4 - * This would compute the following four butterflies - * 8 -- 12 - * 9 -- 13 - * 10 -- 14 - * 11 -- 15 - * - start=4, len=2 - * This would compute the following two butterflies - * 4 -- 6 - * 5 -- 7 - */ + * The twiddles `z`, `zt` are implicitly negated: we compute `b - a` instead + * of `a - b`, which is equivalent to multiplying by `-z`. Callers therefore + * pass the un-negated zetas straight from `mld_zetas`. */ +static MLD_INLINE void mld_gs_butterfly(int32_t r[MLDSA_N], unsigned i, + unsigned j, int32_t z, int32_t zt) +{ + const int32_t a = r[i]; + const int32_t b = r[j]; + r[i] = a + b; + r[j] = mld_fqmul(b - a, z, zt); +} -/* Reference: Embedded in `ntt()` in the reference implementation @[REF]. */ -static MLD_INLINE void mld_ntt_butterfly_block(int32_t r[MLDSA_N], - const int32_t zeta, - const unsigned start, - const unsigned len, - const unsigned bound) +/* + * Two merged forward-NTT layers, applied to one outer block. + */ +static MLD_INLINE void mld_ntt_2_layers_block( + int32_t r[MLDSA_N], unsigned start, unsigned len, int32_t z0, int32_t z0t, + int32_t z1, int32_t z1t, int32_t z2, int32_t z2t, const int32_t bound) __contract__( - requires(start < MLDSA_N) - requires(1 <= len && len <= MLDSA_N / 2 && start + 2 * len <= MLDSA_N) - requires(0 <= bound && bound < INT32_MAX - MLDSA_Q) - requires(-MLDSA_Q_HALF < zeta && zeta < MLDSA_Q_HALF) requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(array_abs_bound(r, 0, start, bound + MLDSA_Q)) + requires(0 < bound && bound < INT32_MAX - 2 * MLDSA_Q) + requires(1 <= len && len <= MLDSA_N / 4) + requires(start <= MLDSA_N - 4 * len) + requires(z0 > -MLDSA_Q_HALF && z0 < MLDSA_Q_HALF) + requires(z1 > -MLDSA_Q_HALF && z1 < MLDSA_Q_HALF) + requires(z2 > -MLDSA_Q_HALF && z2 < MLDSA_Q_HALF) requires(array_abs_bound(r, start, MLDSA_N, bound)) - assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) - ensures(array_abs_bound(r, 0, start + 2*len, bound + MLDSA_Q)) - ensures(array_abs_bound(r, start + 2 * len, MLDSA_N, bound))) + requires(array_abs_bound(r, 0, start, bound + 2 * MLDSA_Q)) + assigns(memory_slice(r, sizeof(uint32_t) * MLDSA_N)) + ensures(array_abs_bound(r, start + 4 * len, MLDSA_N, bound)) + ensures(array_abs_bound(r, 0, start + 4 * len, bound + 2 * MLDSA_Q)) +) { - /* `bound` is a ghost variable only needed in the CBMC specification */ - unsigned j; + unsigned j = 0; + /* `bound` is a ghost variable referenced only in the CBMC contract. */ ((void)bound); - for (j = start; j < start + len; j++) + for (j = 0; j < len; j++) __loop__( - invariant(start <= j && j <= start + len) - /* - * Coefficients are updated in strided pairs, so the bounds for the - * intermediate states alternate twice between the old and new bound - */ - invariant(array_abs_bound(r, 0, j, bound + MLDSA_Q)) - invariant(array_abs_bound(r, j, start + len, bound)) - invariant(array_abs_bound(r, start + len, j + len, bound + MLDSA_Q)) - invariant(array_abs_bound(r, j + len, MLDSA_N, bound)) - decreases(start + len - j)) + assigns(j, memory_slice(r, sizeof(uint32_t) * MLDSA_N)) + invariant(j <= len) + /* Static bounds */ + invariant(array_abs_bound(r, 0, start, bound + 2 * MLDSA_Q)) + invariant(array_abs_bound(r, start + 4 * len, MLDSA_N, bound)) + /* Dynamic bounds */ + invariant(array_abs_bound(r, start + 0 * len, start + 0 * len + j, bound + 2 * MLDSA_Q)) + invariant(array_abs_bound(r, start + 1 * len, start + 1 * len + j, bound + 2 * MLDSA_Q)) + invariant(array_abs_bound(r, start + 2 * len, start + 2 * len + j, bound + 2 * MLDSA_Q)) + invariant(array_abs_bound(r, start + 3 * len, start + 3 * len + j, bound + 2 * MLDSA_Q)) + invariant(array_abs_bound(r, start + 0 * len + j, start + 1 * len, bound)) + invariant(array_abs_bound(r, start + 1 * len + j, start + 2 * len, bound)) + invariant(array_abs_bound(r, start + 2 * len + j, start + 3 * len, bound)) + invariant(array_abs_bound(r, start + 3 * len + j, start + 4 * len, bound)) + decreases(len - j)) { - int32_t t; - t = mld_fqmul(r[j + len], zeta); - r[j + len] = r[j] - t; - r[j] = r[j] + t; + const unsigned i0 = start + j; + const unsigned i1 = i0 + 1 * len; + const unsigned i2 = i0 + 2 * len; + const unsigned i3 = i0 + 3 * len; + + mld_ct_butterfly(r, i0, i2, z0, z0t); + mld_ct_butterfly(r, i1, i3, z0, z0t); + mld_ct_butterfly(r, i0, i1, z1, z1t); + mld_ct_butterfly(r, i2, i3, z2, z2t); } } -/* mld_ntt_layer() - * - * Compute one layer of forward NTT - * - * Parameters: - * - r: Pointer to base of polynomial - * - layer: Indicates which layer is being applied. +/* + * Two merged forward-NTT layers. */ - -/* Reference: Embedded in `ntt()` in the reference implementation @[REF]. */ -static MLD_INLINE void mld_ntt_layer(int32_t r[MLDSA_N], const unsigned layer) +static MLD_INLINE void mld_ntt_2_layers(int32_t r[MLDSA_N], + const unsigned layer) __contract__( requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(1 <= layer && layer <= 8) + requires(layer == 1 || layer == 3 || layer == 5 || layer == 7) requires(array_abs_bound(r, 0, MLDSA_N, layer * MLDSA_Q)) assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) - ensures(array_abs_bound(r, 0, MLDSA_N, (layer + 1) * MLDSA_Q))) + ensures(array_abs_bound(r, 0, MLDSA_N, (layer + 2) * MLDSA_Q))) { - unsigned start, k, len; - /* Twiddle factors for layer n are at indices 2^(n-1)..2^n-1. */ + const unsigned len_outer = (unsigned)MLDSA_N >> layer; + const unsigned len = len_outer >> 1; + unsigned start, k; k = 1u << (layer - 1); - len = (unsigned)MLDSA_N >> layer; - for (start = 0; start < MLDSA_N; start += 2 * len) + for (start = 0; start < MLDSA_N; start += 2 * len_outer) __loop__( - invariant(start < MLDSA_N + 2 * len) - invariant(k <= MLDSA_N) - invariant(2 * len * k == start + MLDSA_N) - invariant(array_abs_bound(r, 0, start, layer * MLDSA_Q + MLDSA_Q)) + invariant(start <= MLDSA_N) + invariant((1u << (layer - 1)) <= k && k <= (1u << layer)) + invariant(2 * len_outer * k == start + MLDSA_N) + invariant(array_abs_bound(r, 0, start, (layer + 2) * MLDSA_Q)) invariant(array_abs_bound(r, start, MLDSA_N, layer * MLDSA_Q)) decreases(MLDSA_N - start)) { - int32_t zeta = mld_zetas[k++]; - mld_ntt_butterfly_block(r, zeta, start, len, layer * MLDSA_Q); + const int32_t z0 = mld_zetas[k][0]; + const int32_t z1 = mld_zetas[2 * k][0]; + const int32_t z2 = mld_zetas[2 * k + 1][0]; + + const int32_t z0t = mld_zetas[k][1]; + const int32_t z1t = mld_zetas[2 * k][1]; + const int32_t z2t = mld_zetas[2 * k + 1][1]; + + k++; + mld_ntt_2_layers_block(r, start, len, z0, z0t, z1, z1t, z2, z2t, + (int32_t)(layer * MLDSA_Q)); } } @@ -295,22 +315,15 @@ __contract__( ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) ) { - unsigned int layer; int32_t *r; - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); r = a->coeffs; - for (layer = 1; layer < 9; layer++) - __loop__( - invariant(1 <= layer && layer <= 9) - invariant(array_abs_bound(r, 0, MLDSA_N, layer * MLDSA_Q)) - decreases(9 - layer) - ) - { - mld_ntt_layer(r, layer); - } + mld_ntt_2_layers(r, 1); + mld_ntt_2_layers(r, 3); + mld_ntt_2_layers(r, 5); + mld_ntt_2_layers(r, 7); mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); } @@ -348,49 +361,105 @@ __contract__( { /* check-magic: 41978 == pow(2,64-8,MLDSA_Q) */ const int32_t f = 41978; - /* Bounds: MLD_INTT_BOUND is MLDSA_Q, so the bounds reasoning is just - * a special case of that in mld_fqmul(). */ - return mld_montgomery_reduce((int64_t)a * f); + /* check-magic: + -8395782 == signed_mod(41978 * pow(MLDSA_Q, -1, 2^32), 2^32) */ + const int32_t f_twisted = -8395782; + /* Bounds: MLD_INTT_BOUND is MLDSA_Q, so the bound follows directly from + * the postcondition of mld_fqmul(). */ + return mld_fqmul(a, f, f_twisted); } -/* Reference: Embedded into `invntt_tomont()` in the reference implementation - * @[REF] */ -static MLD_INLINE void mld_invntt_layer(int32_t r[MLDSA_N], unsigned layer) +/* + * Two merged inverse-NTT layers, applied to one outer block. + */ +static MLD_INLINE void mld_invntt_2_layers_block( + int32_t r[MLDSA_N], unsigned start, unsigned len, int32_t z0, int32_t z0t, + int32_t z1, int32_t z1t, int32_t z2, int32_t z2t, const int32_t bound) __contract__( requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) - requires(1 <= layer && layer <= 8) - requires(array_abs_bound(r, 0, MLDSA_N, (MLDSA_N >> layer) * MLDSA_Q)) + requires(MLDSA_Q <= bound && bound <= INT32_MAX / 4) + requires(1 <= len && len <= MLDSA_N / 4) + requires(start <= MLDSA_N - 4 * len) + requires(z0 > -MLDSA_Q_HALF && z0 < MLDSA_Q_HALF) + requires(z1 > -MLDSA_Q_HALF && z1 < MLDSA_Q_HALF) + requires(z2 > -MLDSA_Q_HALF && z2 < MLDSA_Q_HALF) + requires(array_abs_bound(r, start, MLDSA_N, bound)) + requires(array_abs_bound(r, 0, start, 4 * bound)) + assigns(memory_slice(r, sizeof(uint32_t) * MLDSA_N)) + ensures(array_abs_bound(r, start + 4 * len, MLDSA_N, bound)) + ensures(array_abs_bound(r, 0, start + 4 * len, 4 * bound)) +) +{ + unsigned j = 0; + /* `bound` is a ghost variable referenced only in the CBMC contract. */ + ((void)bound); + for (j = 0; j < len; j++) + __loop__( + assigns(j, memory_slice(r, sizeof(uint32_t) * MLDSA_N)) + invariant(j <= len) + /* Static bounds */ + invariant(array_abs_bound(r, 0, start, 4 * bound)) + invariant(array_abs_bound(r, start + 4 * len, MLDSA_N, bound)) + /* Dynamic bounds */ + invariant(array_abs_bound(r, start + 0 * len, start + 0 * len + j, 4 * bound)) + invariant(array_abs_bound(r, start + 1 * len, start + 1 * len + j, 4 * bound)) + invariant(array_abs_bound(r, start + 2 * len, start + 2 * len + j, 4 * bound)) + invariant(array_abs_bound(r, start + 3 * len, start + 3 * len + j, 4 * bound)) + invariant(array_abs_bound(r, start + 0 * len + j, start + 1 * len, bound)) + invariant(array_abs_bound(r, start + 1 * len + j, start + 2 * len, bound)) + invariant(array_abs_bound(r, start + 2 * len + j, start + 3 * len, bound)) + invariant(array_abs_bound(r, start + 3 * len + j, start + 4 * len, bound)) + decreases(len - j)) + { + const unsigned i0 = start + j; + const unsigned i1 = i0 + 1 * len; + const unsigned i2 = i0 + 2 * len; + const unsigned i3 = i0 + 3 * len; + + mld_gs_butterfly(r, i0, i1, z1, z1t); + mld_gs_butterfly(r, i2, i3, z2, z2t); + mld_gs_butterfly(r, i0, i2, z0, z0t); + mld_gs_butterfly(r, i1, i3, z0, z0t); + } +} + +/* + * Two merged inverse-NTT layers. + */ +static MLD_INLINE void mld_invntt_2_layers(int32_t r[MLDSA_N], + const unsigned layer) +__contract__( + requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(layer == 2 || layer == 4 || layer == 6 || layer == 8) + requires(array_abs_bound(r, 0, MLDSA_N, ((unsigned)MLDSA_N >> layer) * MLDSA_Q)) assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) - ensures(array_abs_bound(r, 0, MLDSA_N, (MLDSA_N >> (layer - 1)) * MLDSA_Q))) + ensures(array_abs_bound(r, 0, MLDSA_N, ((unsigned)MLDSA_N >> (layer - 2)) * MLDSA_Q))) { - unsigned start, k, len; - len = (unsigned)MLDSA_N >> layer; - k = (1u << layer) - 1; - for (start = 0; start < MLDSA_N; start += 2 * len) + const unsigned len = (unsigned)MLDSA_N >> layer; + const unsigned len_outer = len << 1; + const int32_t bound = (int32_t)(((unsigned)MLDSA_N >> layer) * MLDSA_Q); + unsigned start, k; + k = (1u << (layer - 1)) - 1u; + for (start = 0; start < MLDSA_N; start += 2 * len_outer) __loop__( - invariant(start <= MLDSA_N && k <= 255) - invariant(2 * len * k + start == 2 * MLDSA_N - 2 * len) - invariant(array_abs_bound(r, 0, start, (MLDSA_N >> (layer - 1)) * MLDSA_Q)) - invariant(array_abs_bound(r, start, MLDSA_N, (MLDSA_N >> layer) * MLDSA_Q)) + invariant(start <= MLDSA_N) + invariant(k < (1u << (layer - 1))) + invariant(2 * len_outer * k + 2 * len_outer == 2 * MLDSA_N - start) + invariant(array_abs_bound(r, 0, start, 4 * bound)) + invariant(array_abs_bound(r, start, MLDSA_N, bound)) decreases(MLDSA_N - start)) { - unsigned j; - int32_t zeta = -mld_zetas[k--]; - - for (j = start; j < start + len; j++) - __loop__( - invariant(start <= j && j <= start + len) - invariant(array_abs_bound(r, 0, start, (MLDSA_N >> (layer - 1)) * MLDSA_Q)) - invariant(array_abs_bound(r, start, j, (MLDSA_N >> (layer - 1)) * MLDSA_Q)) - invariant(array_abs_bound(r, j, start + len, (MLDSA_N >> layer) * MLDSA_Q)) - invariant(array_abs_bound(r, start + len, MLDSA_N, (MLDSA_N >> layer) * MLDSA_Q)) - decreases(start + len - j)) - { - int32_t t = r[j]; - r[j] = t + r[j + len]; - r[j + len] = t - r[j + len]; - r[j + len] = mld_fqmul(r[j + len], zeta); - } + /* Zetas are passed un-negated; `mld_gs_butterfly` absorbs the negation. */ + const int32_t z0 = mld_zetas[k][0]; + const int32_t z1 = mld_zetas[2 * k + 1][0]; + const int32_t z2 = mld_zetas[2 * k][0]; + + const int32_t z0t = mld_zetas[k][1]; + const int32_t z1t = mld_zetas[2 * k + 1][1]; + const int32_t z2t = mld_zetas[2 * k][1]; + + k--; + mld_invntt_2_layers_block(r, start, len, z0, z0t, z1, z1t, z2, z2t, bound); } } @@ -402,22 +471,16 @@ __contract__( ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_INTT_BOUND)) ) { - unsigned int layer, j; + unsigned int j; int32_t *r; mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q); r = a->coeffs; - for (layer = 8; layer >= 1; layer--) - __loop__( - invariant(layer <= 8) - /* Absolute bounds increase from 1Q before layer 8 */ - /* up to 256Q after layer 1 */ - invariant(array_abs_bound(r, 0, MLDSA_N, (MLDSA_N >> layer) * MLDSA_Q)) - decreases(layer)) - { - mld_invntt_layer(r, layer); - } + mld_invntt_2_layers(r, 8); + mld_invntt_2_layers(r, 6); + mld_invntt_2_layers(r, 4); + mld_invntt_2_layers(r, 2); /* Coefficient bounds are now at 256Q. We now scale by mont / 256, * i.e., compute the Montgomery multiplication by mont^2 / 256. diff --git a/mldsa/src/zetas.inc b/mldsa/src/zetas.inc index fa3034440..1ad058440 100644 --- a/mldsa/src/zetas.inc +++ b/mldsa/src/zetas.inc @@ -12,44 +12,263 @@ /* * Table of zeta values used in the reference NTT and inverse NTT. - * See autogen for details. + * Each row is (zeta_mont, zeta_twisted); see autogen for details. */ -static const int32_t mld_zetas[MLDSA_N] = { - 0, 25847, -2608894, -518909, 237124, -777960, -876248, - 466468, 1826347, 2353451, -359251, -2091905, 3119733, -2884855, - 3111497, 2680103, 2725464, 1024112, -1079900, 3585928, -549488, - -1119584, 2619752, -2108549, -2118186, -3859737, -1399561, -3277672, - 1757237, -19422, 4010497, 280005, 2706023, 95776, 3077325, - 3530437, -1661693, -3592148, -2537516, 3915439, -3861115, -3043716, - 3574422, -2867647, 3539968, -300467, 2348700, -539299, -1699267, - -1643818, 3505694, -3821735, 3507263, -2140649, -1600420, 3699596, - 811944, 531354, 954230, 3881043, 3900724, -2556880, 2071892, - -2797779, -3930395, -1528703, -3677745, -3041255, -1452451, 3475950, - 2176455, -1585221, -1257611, 1939314, -4083598, -1000202, -3190144, - -3157330, -3632928, 126922, 3412210, -983419, 2147896, 2715295, - -2967645, -3693493, -411027, -2477047, -671102, -1228525, -22981, - -1308169, -381987, 1349076, 1852771, -1430430, -3343383, 264944, - 508951, 3097992, 44288, -1100098, 904516, 3958618, -3724342, - -8578, 1653064, -3249728, 2389356, -210977, 759969, -1316856, - 189548, -3553272, 3159746, -1851402, -2409325, -177440, 1315589, - 1341330, 1285669, -1584928, -812732, -1439742, -3019102, -3881060, - -3628969, 3839961, 2091667, 3407706, 2316500, 3817976, -3342478, - 2244091, -2446433, -3562462, 266997, 2434439, -1235728, 3513181, - -3520352, -3759364, -1197226, -3193378, 900702, 1859098, 909542, - 819034, 495491, -1613174, -43260, -522500, -655327, -3122442, - 2031748, 3207046, -3556995, -525098, -768622, -3595838, 342297, - 286988, -2437823, 4108315, 3437287, -3342277, 1735879, 203044, - 2842341, 2691481, -2590150, 1265009, 4055324, 1247620, 2486353, - 1595974, -3767016, 1250494, 2635921, -3548272, -2994039, 1869119, - 1903435, -1050970, -1333058, 1237275, -3318210, -1430225, -451100, - 1312455, 3306115, -1962642, -1279661, 1917081, -2546312, -1374803, - 1500165, 777191, 2235880, 3406031, -542412, -2831860, -1671176, - -1846953, -2584293, -3724270, 594136, -3776993, -2013608, 2432395, - 2454455, -164721, 1957272, 3369112, 185531, -1207385, -3183426, - 162844, 1616392, 3014001, 810149, 1652634, -3694233, -1799107, - -3038916, 3523897, 3866901, 269760, 2213111, -975884, 1717735, - 472078, -426683, 1723600, -1803090, 1910376, -1667432, -1104333, - -260646, -3833893, -2939036, -2235985, -420899, -2286327, 183443, - -976891, 1612842, -3545687, -554416, 3919660, -48306, -1362209, - 3937738, 1400424, -846154, 1976782, +static const int32_t mld_zetas[MLDSA_N][2] = { + {0, 0}, + {25847, 1830765815}, + {-2608894, -1929875198}, + {-518909, -1927777021}, + {237124, 1640767044}, + {-777960, 1477910808}, + {-876248, 1612161320}, + {466468, 1640734244}, + {1826347, 308362795}, + {2353451, -1815525077}, + {-359251, -1374673747}, + {-2091905, -1091570561}, + {3119733, -1929495947}, + {-2884855, 515185417}, + {3111497, -285697463}, + {2680103, 625853735}, + {2725464, 1727305304}, + {1024112, 2082316400}, + {-1079900, -1364982364}, + {3585928, 858240904}, + {-549488, 1806278032}, + {-1119584, 222489248}, + {2619752, -346752664}, + {-2108549, 684667771}, + {-2118186, 1654287830}, + {-3859737, -878576921}, + {-1399561, -1257667337}, + {-3277672, -748618600}, + {1757237, 329347125}, + {-19422, 1837364258}, + {4010497, -1443016191}, + {280005, -1170414139}, + {2706023, -1846138265}, + {95776, -1631226336}, + {3077325, -1404529459}, + {3530437, 1838055109}, + {-1661693, 1594295555}, + {-3592148, -1076973524}, + {-2537516, -1898723372}, + {3915439, -594436433}, + {-3861115, -202001019}, + {-3043716, -475984260}, + {3574422, -561427818}, + {-2867647, 1797021249}, + {3539968, -1061813248}, + {-300467, 2059733581}, + {2348700, -1661512036}, + {-539299, -1104976547}, + {-1699267, -1750224323}, + {-1643818, -901666090}, + {3505694, 418987550}, + {-3821735, 1831915353}, + {3507263, -1925356481}, + {-2140649, 992097815}, + {-1600420, 879957084}, + {3699596, 2024403852}, + {811944, 1484874664}, + {531354, -1636082790}, + {954230, -285388938}, + {3881043, -1983539117}, + {3900724, -1495136972}, + {-2556880, -950076368}, + {2071892, -1714807468}, + {-2797779, -952438995}, + {-3930395, -1574918427}, + {-1528703, -654783359}, + {-3677745, 1350681039}, + {-3041255, -1974159335}, + {-1452451, -2143979939}, + {3475950, 1651689966}, + {2176455, 1599739335}, + {-1585221, 140455867}, + {-1257611, -1285853323}, + {1939314, -1039411342}, + {-4083598, -993005454}, + {-1000202, 1955560694}, + {-3190144, -1440787840}, + {-3157330, 1529189038}, + {-3632928, 568627424}, + {126922, -2131021878}, + {3412210, -783134478}, + {-983419, -247357819}, + {2147896, -588790216}, + {2715295, 1518161567}, + {-2967645, 289871779}, + {-3693493, -86965173}, + {-411027, -1262003603}, + {-2477047, 1708872713}, + {-671102, 2135294594}, + {-1228525, 1787797779}, + {-22981, -1018755525}, + {-1308169, 1638590967}, + {-381987, -889861155}, + {1349076, -120646188}, + {1852771, 1665705315}, + {-1430430, -1669960606}, + {-3343383, 1321868265}, + {264944, -916321552}, + {508951, 1225434135}, + {3097992, 1155548552}, + {44288, -1784632064}, + {-1100098, 2143745726}, + {904516, 666258756}, + {3958618, 1210558298}, + {-3724342, 675310538}, + {-8578, -1261461890}, + {1653064, -1555941048}, + {-3249728, -318346816}, + {2389356, -1999506068}, + {-210977, 628664287}, + {759969, -1499481951}, + {-1316856, -1729304568}, + {189548, -695180180}, + {-3553272, 1422575624}, + {3159746, -1375177022}, + {-1851402, 1424130038}, + {-2409325, 1777179795}, + {-177440, -1185330464}, + {1315589, 334803717}, + {1341330, 235321234}, + {1285669, -178766299}, + {-1584928, 168022240}, + {-812732, -518252220}, + {-1439742, 1206536194}, + {-3019102, 1957047970}, + {-3881060, 985155484}, + {-3628969, 1146323031}, + {3839961, -894060583}, + {2091667, -898413}, + {3407706, 991903578}, + {2316500, 1363007700}, + {3817976, 746144248}, + {-3342478, -1363460238}, + {2244091, 912367099}, + {-2446433, 30313375}, + {-3562462, -1420958686}, + {266997, -605900043}, + {2434439, -44694137}, + {-1235728, -326425360}, + {3513181, 2032221021}, + {-3520352, 2027833504}, + {-3759364, 1176904444}, + {-1197226, 1683520342}, + {-3193378, 1904936414}, + {900702, 14253662}, + {1859098, -421552614}, + {909542, -517299994}, + {819034, 1257750362}, + {495491, 1014493059}, + {-1613174, -818371958}, + {-43260, 2027935492}, + {-522500, 1926727420}, + {-655327, 863641633}, + {-3122442, 1747917558}, + {2031748, -1372618620}, + {3207046, 1931587462}, + {-3556995, 1819892093}, + {-525098, -325927722}, + {-768622, 128353682}, + {-3595838, 1258381762}, + {342297, 2124962073}, + {286988, 908452108}, + {-2437823, -1123881663}, + {4108315, 885133339}, + {3437287, -1223601433}, + {-3342277, 1851023419}, + {1735879, 137583815}, + {203044, 1629985060}, + {2842341, -1920467227}, + {2691481, -1176751719}, + {-2590150, -635454918}, + {1265009, 1967222129}, + {4055324, -1637785316}, + {1247620, -1354528380}, + {2486353, -642772911}, + {1595974, 6363718}, + {-3767016, -1536588520}, + {1250494, -72690498}, + {2635921, 45766801}, + {-3548272, -1287922800}, + {-2994039, 694382729}, + {1869119, -314284737}, + {1903435, 671509323}, + {-1050970, 1136965286}, + {-1333058, 235104446}, + {1237275, 985022747}, + {-3318210, -2070602178}, + {-1430225, 1779436847}, + {-451100, -1045062172}, + {1312455, 963438279}, + {3306115, 419615363}, + {-1962642, 1116720494}, + {-1279661, 831969619}, + {1917081, -1078959975}, + {-2546312, 1216882040}, + {-1374803, 1042326957}, + {1500165, -300448763}, + {777191, 604552167}, + {2235880, -270590488}, + {3406031, 1405999311}, + {-542412, 756955444}, + {-2831860, -1021949428}, + {-1671176, -1276805128}, + {-1846953, 713994583}, + {-2584293, -260312805}, + {-3724270, 608791570}, + {594136, 371462360}, + {-3776993, 940195359}, + {-2013608, 1554794072}, + {2432395, 173440395}, + {2454455, -1357098057}, + {-164721, -1542497137}, + {1957272, 1339088280}, + {3369112, -2126092136}, + {185531, -384158533}, + {-1207385, 2061661095}, + {-3183426, -2040058690}, + {162844, -1316619236}, + {1616392, 827959816}, + {3014001, -883155599}, + {810149, -853476187}, + {1652634, -1039370342}, + {-3694233, -596344473}, + {-1799107, 1726753853}, + {-3038916, -2047270596}, + {3523897, 6087993}, + {3866901, 702390549}, + {269760, -1547952704}, + {2213111, -1723816713}, + {-975884, -110126092}, + {1717735, -279505433}, + {472078, 394851342}, + {-426683, -1591599803}, + {1723600, 565464272}, + {-1803090, -260424530}, + {1910376, 283780712}, + {-1667432, -440824168}, + {-1104333, -1758099917}, + {-260646, -71875110}, + {-3833893, 776003547}, + {-2939036, 1119856484}, + {-2235985, -1600929361}, + {-420899, -1208667171}, + {-2286327, 1123958025}, + {183443, 1544891539}, + {-976891, 879867909}, + {1612842, -1499603926}, + {-3545687, 201262505}, + {-554416, 155290192}, + {3919660, -1809756372}, + {-48306, 2036925262}, + {-1362209, 1934038751}, + {3937738, -973777462}, + {1400424, 400711272}, + {-846154, -540420426}, + {1976782, 374860238}, }; diff --git a/proofs/cbmc/fqmul/Makefile b/proofs/cbmc/fqmul/Makefile index 8652000fc..dae52531d 100644 --- a/proofs/cbmc/fqmul/Makefile +++ b/proofs/cbmc/fqmul/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=mld_fqmul -USE_FUNCTION_CONTRACTS=mld_montgomery_reduce +USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/fqmul/fqmul_harness.c b/proofs/cbmc/fqmul/fqmul_harness.c index d36072a1c..c9b5740e7 100644 --- a/proofs/cbmc/fqmul/fqmul_harness.c +++ b/proofs/cbmc/fqmul/fqmul_harness.c @@ -3,9 +3,9 @@ #include "poly.h" -int32_t mld_fqmul(int32_t a, int32_t b); +int32_t mld_fqmul(int32_t a, int32_t b, int32_t b_twisted); void harness(void) { - int32_t a, b, r; - r = mld_fqmul(a, b); + int32_t a, b, b_twisted, r; + r = mld_fqmul(a, b, b_twisted); } diff --git a/proofs/cbmc/fqscale/Makefile b/proofs/cbmc/fqscale/Makefile index d821b2d26..df0e1e01e 100644 --- a/proofs/cbmc/fqscale/Makefile +++ b/proofs/cbmc/fqscale/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=mld_fqscale -USE_FUNCTION_CONTRACTS=mld_montgomery_reduce +USE_FUNCTION_CONTRACTS=mld_fqmul APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/ntt_butterfly_block/Makefile b/proofs/cbmc/invntt_2_layers/Makefile similarity index 90% rename from proofs/cbmc/ntt_butterfly_block/Makefile rename to proofs/cbmc/invntt_2_layers/Makefile index ae4b238e9..9dc8b52ba 100644 --- a/proofs/cbmc/ntt_butterfly_block/Makefile +++ b/proofs/cbmc/invntt_2_layers/Makefile @@ -4,11 +4,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = ntt_butterfly_block_harness +HARNESS_FILE = invntt_2_layers_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 = mld_ntt_butterfly_block +PROOF_UID = mld_invntt_2_layers DEFINES += INCLUDES += @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c -CHECK_FUNCTION_CONTRACTS=mld_ntt_butterfly_block -USE_FUNCTION_CONTRACTS=mld_fqmul +CHECK_FUNCTION_CONTRACTS=mld_invntt_2_layers +USE_FUNCTION_CONTRACTS=mld_invntt_2_layers_block APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = mld_ntt_butterfly_block +FUNCTION_NAME = mld_invntt_2_layers # 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/invntt_layer/invntt_layer_harness.c b/proofs/cbmc/invntt_2_layers/invntt_2_layers_harness.c similarity index 67% rename from proofs/cbmc/invntt_layer/invntt_layer_harness.c rename to proofs/cbmc/invntt_2_layers/invntt_2_layers_harness.c index 4f8fb4ce9..98ace678b 100644 --- a/proofs/cbmc/invntt_layer/invntt_layer_harness.c +++ b/proofs/cbmc/invntt_2_layers/invntt_2_layers_harness.c @@ -4,11 +4,11 @@ #include #include "params.h" -void mld_invntt_layer(int32_t r[MLDSA_N], unsigned layer); +void mld_invntt_2_layers(int32_t r[MLDSA_N], unsigned layer); void harness(void) { int32_t *r; unsigned layer; - mld_invntt_layer(r, layer); + mld_invntt_2_layers(r, layer); } diff --git a/proofs/cbmc/invntt_2_layers_block/Makefile b/proofs/cbmc/invntt_2_layers_block/Makefile new file mode 100644 index 000000000..280254baf --- /dev/null +++ b/proofs/cbmc/invntt_2_layers_block/Makefile @@ -0,0 +1,32 @@ +# 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 = invntt_2_layers_block_harness + +PROOF_UID = mld_invntt_2_layers_block + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_invntt_2_layers_block +USE_FUNCTION_CONTRACTS=mld_fqmul +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = mld_invntt_2_layers_block + +CBMC_OBJECT_BITS = 9 + +include ../Makefile.common diff --git a/proofs/cbmc/invntt_2_layers_block/invntt_2_layers_block_harness.c b/proofs/cbmc/invntt_2_layers_block/invntt_2_layers_block_harness.c new file mode 100644 index 000000000..a4d1bc4b1 --- /dev/null +++ b/proofs/cbmc/invntt_2_layers_block/invntt_2_layers_block_harness.c @@ -0,0 +1,21 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include +#include "params.h" + +void mld_invntt_2_layers_block(int32_t r[MLDSA_N], unsigned start, + unsigned len_inner, int32_t z_outer, + int32_t z_outer_twst, int32_t z_in_l, + int32_t z_in_l_twst, int32_t z_in_r, + int32_t z_in_r_twst, const int32_t bound); + +void harness(void) +{ + int32_t *r; + unsigned start, len_inner; + int32_t z_outer, z_outer_twst, z_in_l, z_in_l_twst, z_in_r, z_in_r_twst, + bound; + mld_invntt_2_layers_block(r, start, len_inner, z_outer, z_outer_twst, z_in_l, + z_in_l_twst, z_in_r, z_in_r_twst, bound); +} diff --git a/proofs/cbmc/invntt_layer/Makefile b/proofs/cbmc/invntt_layer/Makefile deleted file mode 100644 index b1503d8a5..000000000 --- a/proofs/cbmc/invntt_layer/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 = invntt_layer_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 = mld_invntt_layer - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c - -CHECK_FUNCTION_CONTRACTS=mld_invntt_layer -USE_FUNCTION_CONTRACTS=mld_fqmul -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 = mld_invntt_layer - -# 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/ntt_layer/Makefile b/proofs/cbmc/ntt_2_layers/Makefile similarity index 90% rename from proofs/cbmc/ntt_layer/Makefile rename to proofs/cbmc/ntt_2_layers/Makefile index e2c8a0816..e33e42a0e 100644 --- a/proofs/cbmc/ntt_layer/Makefile +++ b/proofs/cbmc/ntt_2_layers/Makefile @@ -4,11 +4,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = ntt_layer_harness +HARNESS_FILE = ntt_2_layers_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 = mld_ntt_layer +PROOF_UID = mld_ntt_2_layers DEFINES += INCLUDES += @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c -CHECK_FUNCTION_CONTRACTS=mld_ntt_layer -USE_FUNCTION_CONTRACTS=mld_ntt_butterfly_block +CHECK_FUNCTION_CONTRACTS=mld_ntt_2_layers +USE_FUNCTION_CONTRACTS=mld_ntt_2_layers_block APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = mld_ntt_layer +FUNCTION_NAME = mld_ntt_2_layers # 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/ntt_layer/ntt_layer_harness.c b/proofs/cbmc/ntt_2_layers/ntt_2_layers_harness.c similarity index 69% rename from proofs/cbmc/ntt_layer/ntt_layer_harness.c rename to proofs/cbmc/ntt_2_layers/ntt_2_layers_harness.c index e07f526f0..9680d0bad 100644 --- a/proofs/cbmc/ntt_layer/ntt_layer_harness.c +++ b/proofs/cbmc/ntt_2_layers/ntt_2_layers_harness.c @@ -4,11 +4,11 @@ #include #include "params.h" -void mld_ntt_layer(int32_t r[MLDSA_N], unsigned layer); +void mld_ntt_2_layers(int32_t r[MLDSA_N], unsigned layer); void harness(void) { int32_t *r; unsigned layer; - mld_ntt_layer(r, layer); + mld_ntt_2_layers(r, layer); } diff --git a/proofs/cbmc/ntt_2_layers_block/Makefile b/proofs/cbmc/ntt_2_layers_block/Makefile new file mode 100644 index 000000000..89b1074d9 --- /dev/null +++ b/proofs/cbmc/ntt_2_layers_block/Makefile @@ -0,0 +1,32 @@ +# 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 = ntt_2_layers_block_harness + +PROOF_UID = mld_ntt_2_layers_block + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_ntt_2_layers_block +USE_FUNCTION_CONTRACTS=mld_fqmul +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla #--smt2 + +FUNCTION_NAME = mld_ntt_2_layers_block + +CBMC_OBJECT_BITS = 9 + +include ../Makefile.common diff --git a/proofs/cbmc/ntt_2_layers_block/ntt_2_layers_block_harness.c b/proofs/cbmc/ntt_2_layers_block/ntt_2_layers_block_harness.c new file mode 100644 index 000000000..4742956a3 --- /dev/null +++ b/proofs/cbmc/ntt_2_layers_block/ntt_2_layers_block_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include +#include "params.h" + +void mld_ntt_2_layers_block(int32_t r[MLDSA_N], unsigned start, + unsigned len_inner, int32_t z0, int32_t z0_twst, + int32_t z1, int32_t z1_twst, int32_t z2, + int32_t z2_twst, const int32_t bound); + +void harness(void) +{ + int32_t *r; + unsigned start, len_inner; + int32_t z0, z0_twst, z1, z1_twst, z2, z2_twst, bound; + mld_ntt_2_layers_block(r, start, len_inner, z0, z0_twst, z1, z1_twst, z2, + z2_twst, bound); +} diff --git a/proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c b/proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c deleted file mode 100644 index fb4ffa2bb..000000000 --- a/proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c +++ /dev/null @@ -1,16 +0,0 @@ -// Copyright (c) The mldsa-native project authors -// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -#include -#include "params.h" - -void mld_ntt_butterfly_block(int32_t r[MLDSA_N], int32_t zeta, unsigned start, - unsigned len, unsigned bound); - -void harness(void) -{ - int32_t *r, zeta; - unsigned start, len; - unsigned bound; - mld_ntt_butterfly_block(r, zeta, start, len, bound); -} diff --git a/proofs/cbmc/poly_invntt_tomont_c/Makefile b/proofs/cbmc/poly_invntt_tomont_c/Makefile index 070ea4a38..473b3f702 100644 --- a/proofs/cbmc/poly_invntt_tomont_c/Makefile +++ b/proofs/cbmc/poly_invntt_tomont_c/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=mld_poly_invntt_tomont_c -USE_FUNCTION_CONTRACTS=mld_invntt_layer +USE_FUNCTION_CONTRACTS=mld_invntt_2_layers APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_ntt_c/Makefile b/proofs/cbmc/poly_ntt_c/Makefile index 6139dee9c..cfbb24a8a 100644 --- a/proofs/cbmc/poly_ntt_c/Makefile +++ b/proofs/cbmc/poly_ntt_c/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=mld_poly_ntt_c -USE_FUNCTION_CONTRACTS=mld_ntt_layer +USE_FUNCTION_CONTRACTS=mld_ntt_2_layers APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/scripts/autogen b/scripts/autogen index c2ddfd822..d0f17a753 100755 --- a/scripts/autogen +++ b/scripts/autogen @@ -714,17 +714,27 @@ def signed_reduce(a): def gen_c_zetas(): """Generate source and header file for zeta values used in - the reference NTT and invNTT""" + the reference NTT and invNTT. - # The zeta values are the powers of the chosen root of unity (17), - # converted to Montgomery form. + Each yielded entry is a pair (zeta_mont, zeta_twisted) where: + - zeta_mont = signed canonical representative of zeta * 2^32 mod q + - zeta_twisted = signed canonical 32-bit representative of + zeta_mont * q^{-1} mod 2^32 + The twisted form lets the C-reference fqmul skip the extra QINV + multiply that mld_montgomery_reduce would otherwise perform.""" - zeta = [0] # First entry is unused and set to 0 + # The zeta values are the powers of the chosen root of unity, converted + # to Montgomery form (and to its twisted-Montgomery counterpart). + + zeta_pairs = [(0, 0)] # First entry is unused for i in range(1, 256): - zeta.append(signed_reduce(pow(root_of_unity, i, modulus) * montgomery_factor)) + raw = pow(root_of_unity, i, modulus) + z_mont = prepare_root_for_montmul(raw, mult=False) + z_twisted = prepare_root_for_montmul(raw, mult=True) + zeta_pairs.append((z_mont, z_twisted)) # The source code stores the zeta table in bit reversed form - yield from (zeta[bitreverse(i, 8)] for i in range(256)) + yield from (zeta_pairs[bitreverse(i, 8)] for i in range(256)) def gen_c_zeta_file(): @@ -733,10 +743,11 @@ def gen_c_zeta_file(): yield "" yield "/*" yield " * Table of zeta values used in the reference NTT and inverse NTT." - yield " * See autogen for details." + yield " * Each row is (zeta_mont, zeta_twisted); see autogen for details." yield " */" - yield "static const int32_t mld_zetas[MLDSA_N] = {" - yield from map(lambda t: str(t) + ",", gen_c_zetas()) + yield "static const int32_t mld_zetas[MLDSA_N][2] = {" + for z_mont, z_twisted in gen_c_zetas(): + yield f"{{ {z_mont}, {z_twisted} }}," yield "};" yield "" diff --git a/scripts/check-magic b/scripts/check-magic index a4c5deba3..08a6cffae 100755 --- a/scripts/check-magic +++ b/scripts/check-magic @@ -38,6 +38,37 @@ FAIL = f"{RED}✗{NORMAL}" REMEMBERED = f"{BLUE}⊢{NORMAL}" +def join_block_comments(lines): + """Collapse multi-line C block comments onto their opening line. + + Each continuation line is replaced with an empty placeholder so the + overall line count - and therefore line numbers in diagnostics - is + unchanged. Only handles block comments that start and end with the + standard /* ... */ delimiters; line comments and strings are left + alone, which is sufficient for this script's input. + """ + out = list(lines) + i = 0 + n = len(out) + while i < n: + line = out[i] + if "/*" in line and "*/" not in line: + j = i + 1 + merged = line + while j < n and "*/" not in out[j]: + merged += " " + out[j].strip() + out[j] = "" + j += 1 + if j < n: + merged += " " + out[j].strip() + out[j] = "" + out[i] = merged + i = j + 1 + continue + i += 1 + return out + + def check_magic_numbers(): mldsa_q = 8380417 exceptions = [ @@ -131,6 +162,11 @@ def check_magic_numbers(): magic_dict = {"MLDSA_Q": mldsa_q, "MLD_REDUCE32_DOMAIN_MAX": 2143289343} magic_expr = None verified_magics = {} + # Pre-pass: collapse multi-line block comments onto their opening + # line so wrapped check-magic annotations are recognized. Consumed + # continuation lines are replaced with empty placeholders to preserve + # line numbers in diagnostics. + content = join_block_comments(content) for i, line in enumerate(content): if enabled is True and disable_marker in line: enabled = False