From 4d29d8f23d19892d1b2699b811dd1f5298103dd2 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 24 Mar 2025 04:34:20 +0000 Subject: [PATCH 01/12] CBMC: Refine bounds for input and output of base multiplication Previously, the base multiplication would assume that one of its inputs is bound by 4096 in absolute value, but make no assumptions about the other input ("b-input" henceforth) and its mulcache. This commit refines the bounds slightly, as follows: - The b-input is assumed to be bound by MLK_NTT_BOUND in absolute value. This comes for free since all values for b _are_ results of the NTT. - The b-cache-input is assumed to be bound by MLKEM_Q in absolute value. With those additional bounds in place, it can be showed that the result of the base multiplication is below INT16_MAX/2 in absolute value. Accordingly, this can be added as a precondition for the inverse NTT. Those refined bounds can help in subsequent commits to improve the reduction strategy inside the inverse NTT. For the native AVX2 backend, the new output bound for the mulcache forces an explicit zeroization of the mulcache. This is not ideal since the cache is in fact entirely unused, but the performance penalty should be marginal (if the compiler can't eliminate the zeroization in the first place). Signed-off-by: Hanno Becker --- mlkem/src/indcpa.c | 23 ++++++++++++++++------ mlkem/src/native/api.h | 4 ++++ mlkem/src/poly.h | 25 ++++++++++++------------ mlkem/src/poly_k.c | 43 ++++++++++++++++++++++-------------------- mlkem/src/poly_k.h | 22 ++++++++++++++------- 5 files changed, 71 insertions(+), 46 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 49cd5a1f08..22b471d55c 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -336,9 +336,11 @@ void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES], * - mlk_polymat a: Input matrix. Must be in NTT domain * and have coefficients of absolute value < 4096. * - mlk_polyvec v: Input polynomial vector. Must be in NTT - * domain. + * domain and have coefficients of absolute value + * < MLK_NTT_BOUND. * - mlk_polyvec vc: Mulcache for v, computed via - * mlk_polyvec_mulcache_compute(). + * mlk_polyvec_mulcache_compute(). Must have coefficients + * of absolute value < MLKEM_Q. * * Specification: Implements @[FIPS203, Section 2.4.7, Eq (2.12), (2.13)] * @@ -353,17 +355,26 @@ __contract__( requires(forall(k0, 0, MLKEM_K, forall(k1, 0, MLKEM_K, array_bound(a->vec[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))) - assigns(memory_slice(out, sizeof(mlk_polyvec)))) + requires(forall(k1, 0, MLKEM_K, + array_abs_bound(v->vec[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + requires(forall(k2, 0, MLKEM_K, + array_abs_bound(vc->vec[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q))) + assigns(memory_slice(out, sizeof(mlk_polyvec))) + ensures(forall(k3, 0, MLKEM_K, + array_abs_bound(out->vec[k3].coeffs, 0, MLKEM_N, INT16_MAX/2)))) { unsigned i; for (i = 0; i < MLKEM_K; i++) __loop__( assigns(i, memory_slice(out, sizeof(mlk_polyvec))) invariant(i <= MLKEM_K) + invariant(forall(k, 0, i, + array_abs_bound(out->vec[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))) decreases(MLKEM_K - i)) - { - mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc); - } + { + mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, + vc); + } } /************************************************* diff --git a/mlkem/src/native/api.h b/mlkem/src/native/api.h index 0308f2bd51..47fe221fb3 100644 --- a/mlkem/src/native/api.h +++ b/mlkem/src/native/api.h @@ -156,6 +156,7 @@ MLK_MUST_CHECK_RETURN_VALUE static MLK_INLINE int mlk_intt_native(int16_t p[MLKEM_N]) __contract__( requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N)) + requires(array_abs_bound(p, 0, MLKEM_N, INT16_MAX/2)) assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N)) ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS) ensures((return_value == MLK_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLKEM_N, MLK_INVNTT_BOUND)) @@ -269,6 +270,7 @@ __contract__( requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 2 */ @@ -304,6 +306,7 @@ __contract__( requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 3 */ @@ -339,6 +342,7 @@ __contract__( requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 4 */ #endif /* MLK_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */ diff --git a/mlkem/src/poly.h b/mlkem/src/poly.h index 587062cce5..8c94627acb 100644 --- a/mlkem/src/poly.h +++ b/mlkem/src/poly.h @@ -60,14 +60,16 @@ typedef struct **************************************************/ static MLK_ALWAYS_INLINE int16_t mlk_montgomery_reduce(int32_t a) __contract__( - requires(a < +(INT32_MAX - (((int32_t)1 << 15) * MLKEM_Q)) && - a > -(INT32_MAX - (((int32_t)1 << 15) * MLKEM_Q))) - /* We don't attempt to express an input-dependent output bound - * as the post-condition here. There are two call-sites for this - * function: - * - The base multiplication: Here, we need no output bound. - * - mlk_fqmul: Here, we inline this function and prove another spec - * for mlk_fqmul which does have a post-condition bound. */ + /* This specification is only relevant for Montgomery reduction + * during base multiplication, and the input bound is tailored to that. + * The output bound, albeit weak, allows one addition/subtraction prior + * to risk of overflow; this can be useful for the inverse NTT, for example. + * + * For the use of montgomery_reduce in fqmul, we inline this + * function instead of calling it by contract. */ + requires(a <= +(4 * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND) && + a >= -(4 * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND)) + ensures(return_value < (INT16_MAX / 2) && return_value > -(INT16_MAX / 2)) ) { /* check-magic: 62209 == unsigned_mod(pow(MLKEM_Q, -1, 2^16), 2^16) */ @@ -148,17 +150,13 @@ __contract__( * - Caches `b_1 * \gamma` in @[FIPS203, Algorithm 12, BaseCaseMultiply, L1] * ************************************************************/ -/* - * NOTE: The default C implementation of this function populates - * the mulcache with values in (-q,q), but this is not needed for the - * higher level safety proofs, and thus not part of the spec. - */ MLK_INTERNAL_API void mlk_poly_mulcache_compute(mlk_poly_mulcache *x, const mlk_poly *a) __contract__( requires(memory_no_alias(x, sizeof(mlk_poly_mulcache))) requires(memory_no_alias(a, sizeof(mlk_poly))) assigns(memory_slice(x, sizeof(mlk_poly_mulcache))) + ensures(array_abs_bound(x->coeffs, 0, MLKEM_N/2, MLKEM_Q)) ); #define mlk_poly_reduce MLK_NAMESPACE(poly_reduce) @@ -310,6 +308,7 @@ MLK_INTERNAL_API void mlk_poly_invntt_tomont(mlk_poly *r) __contract__( requires(memory_no_alias(r, sizeof(mlk_poly))) + requires(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2)) assigns(memory_slice(r, sizeof(mlk_poly))) ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND)) ); diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c index d729d2d26f..27e56a35d9 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -162,29 +162,32 @@ __contract__( unsigned i; mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); + mlk_assert_abs_bound_2d(b, MLKEM_K, MLKEM_N, MLK_NTT_BOUND); + mlk_assert_abs_bound_2d(b_cache, MLKEM_K, MLKEM_N / 2, MLKEM_Q); + for (i = 0; i < MLKEM_N / 2; i++) - __loop__(invariant(i <= MLKEM_N / 2) - decreases(MLKEM_N / 2 - i)) - { - unsigned k; - int32_t t[2] = {0}; - for (k = 0; k < MLKEM_K; k++) - __loop__( - invariant(k <= MLKEM_K && - t[0] <= (int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768 && - t[0] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) && - t[1] <= ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) && - t[1] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768)) - decreases(MLKEM_K - k)) + __loop__( + invariant(i <= MLKEM_N / 2) + invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2))) + decreases(MLKEM_N / 2 - i)) { - t[0] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i]; - t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i]; - t[1] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1]; - t[1] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i]; + unsigned k; + int32_t t[2] = {0}; + for (k = 0; k < MLKEM_K; k++) + __loop__( + invariant(k <= MLKEM_K && i <= MLKEM_N / 2) + invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1))) + decreases(MLKEM_K - k)) + { + t[0] += + (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i]; + t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i]; + t[1] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1]; + t[1] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i]; + } + r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]); + r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]); } - r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]); - r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]); - } } MLK_INTERNAL_API diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h index 9089a8e431..742e741e65 100644 --- a/mlkem/src/poly_k.h +++ b/mlkem/src/poly_k.h @@ -357,9 +357,11 @@ MLK_INTERNAL_API void mlk_polyvec_invntt_tomont(mlk_polyvec *r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) + requires(forall(k0, 0, MLKEM_K, + array_abs_bound(r->vec[k0].coeffs, 0, MLKEM_N, INT16_MAX/2))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(j, 0, MLKEM_K, - array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND))) + array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND))) ); #define mlk_polyvec_basemul_acc_montgomery_cached \ @@ -372,7 +374,11 @@ __contract__( * * Bounds: * - Every coefficient of a is assumed to be in [0..4095] - * - No bounds guarantees for the coefficients in the result. + * - Every coefficient of b is assumed to be bound by + * MLK_NTT_BOUND in absolute value. + * - Every coefficient of b_cache is assumed to be bound by + * MLKEM_Q in absolute value. + * - The output bounds are below INT16_MAX/2 in absolute value. * * Arguments: - mlk_poly *r: pointer to output polynomial * - const mlk_polyvec a: pointer to first input polynomial vector @@ -399,7 +405,12 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache))) requires(forall(k1, 0, MLKEM_K, array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(k2, 0, MLKEM_K, + array_abs_bound(b->vec[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + requires(forall(k3, 0, MLKEM_K, + array_abs_bound(b_cache->vec[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q))) assigns(memory_slice(r, sizeof(mlk_poly))) + ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_polyvec_mulcache_compute MLK_NAMESPACE_K(polyvec_mulcache_compute) @@ -427,17 +438,14 @@ __contract__( * - Caches `b_1 * \gamma` in @[FIPS203, Algorithm 12, BaseCaseMultiply, L1] * ************************************************************/ -/* - * NOTE: The default C implementation of this function populates - * the mulcache with values in (-q,q), but this is not needed for the - * higher level safety proofs, and thus not part of the spec. - */ MLK_INTERNAL_API void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache *x, const mlk_polyvec *a) __contract__( requires(memory_no_alias(x, sizeof(mlk_polyvec_mulcache))) requires(memory_no_alias(a, sizeof(mlk_polyvec))) assigns(memory_slice(x, sizeof(mlk_polyvec_mulcache))) + ensures(forall(k0, 0, MLKEM_K, + array_abs_bound(x->vec[k0].coeffs, 0, MLKEM_N/2, MLKEM_Q))) ); #define mlk_polyvec_reduce MLK_NAMESPACE_K(polyvec_reduce) From 93018afaf33e8440bdb47a2687cdd4d2c02f12dc Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Mon, 9 Jun 2025 15:04:08 +0100 Subject: [PATCH 02/12] Use --arrays-uf-always here to improve proof speed. Signed-off-by: Rod Chapman --- proofs/cbmc/matvec_mul/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/cbmc/matvec_mul/Makefile b/proofs/cbmc/matvec_mul/Makefile index 65fc7e878b..bdc703c31c 100644 --- a/proofs/cbmc/matvec_mul/Makefile +++ b/proofs/cbmc/matvec_mul/Makefile @@ -35,7 +35,7 @@ CBMCFLAGS=--smt2 # # For functions that use large and multi-dimensional arrays, this yields # a substantial improvement in proof performance. -CBMCFLAGS += --no-array-field-sensitivity +CBMCFLAGS += --arrays-uf-always CBMCFLAGS += --slice-formula FUNCTION_NAME = mlk_matvec_mul From 0c0a8a1e6f01024f71d8691013def7228ee59550 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 09:54:48 +0100 Subject: [PATCH 03/12] Fix merge conflicts and complete rebase again main branch. Signed-off-by: Rod Chapman --- mlkem/src/indcpa.c | 80 ++++++++++--------- mlkem/src/indcpa.h | 2 +- mlkem/src/poly.c | 1 + mlkem/src/poly_k.c | 47 ++++++----- mlkem/src/poly_k.h | 52 ++++++------ proofs/cbmc/polyvec_add/polyvec_add_harness.c | 2 +- ...ec_basemul_acc_montgomery_cached_harness.c | 4 +- ...mul_acc_montgomery_cached_native_harness.c | 4 +- .../polyvec_compress_du_harness.c | 2 +- .../polyvec_decompress_du_harness.c | 2 +- .../polyvec_frombytes_harness.c | 2 +- .../polyvec_invntt_tomont_harness.c | 2 +- .../polyvec_mulcache_compute_harness.c | 4 +- proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c | 2 +- .../polyvec_reduce/polyvec_reduce_harness.c | 2 +- .../polyvec_tobytes/polyvec_tobytes_harness.c | 2 +- .../polyvec_tomont/polyvec_tomont_harness.c | 2 +- 17 files changed, 115 insertions(+), 97 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 22b471d55c..41597876cd 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -58,8 +58,7 @@ * Implements @[FIPS203, Algorithm 13 (K-PKE.KeyGen), L19] * **************************************************/ -static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], - const mlk_polyvec *pk, +static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], mlk_polyvec pk, const uint8_t seed[MLKEM_SYMBYTES]) { mlk_assert_bound_2d(pk->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -83,7 +82,7 @@ static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], * Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt), L2-3] * **************************************************/ -static void mlk_unpack_pk(mlk_polyvec *pk, uint8_t seed[MLKEM_SYMBYTES], +static void mlk_unpack_pk(mlk_polyvec pk, uint8_t seed[MLKEM_SYMBYTES], const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]) { mlk_polyvec_frombytes(pk, packedpk); @@ -108,8 +107,7 @@ static void mlk_unpack_pk(mlk_polyvec *pk, uint8_t seed[MLKEM_SYMBYTES], * Implements @[FIPS203, Algorithm 13 (K-PKE.KeyGen), L20] * **************************************************/ -static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], - const mlk_polyvec *sk) +static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], mlk_polyvec sk) { mlk_assert_bound_2d(sk->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); mlk_polyvec_tobytes(r, sk); @@ -129,7 +127,7 @@ static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], * Implements @[FIPS203, Algorithm 15 (K-PKE.Decrypt), L5] * **************************************************/ -static void mlk_unpack_sk(mlk_polyvec *sk, +static void mlk_unpack_sk(mlk_polyvec sk, const uint8_t packedsk[MLKEM_INDCPA_SECRETKEYBYTES]) { mlk_polyvec_frombytes(sk, packedsk); @@ -150,8 +148,8 @@ static void mlk_unpack_sk(mlk_polyvec *sk, * Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt), L22-23] * **************************************************/ -static void mlk_pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], - const mlk_polyvec *b, mlk_poly *v) +static void mlk_pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], mlk_polyvec b, + mlk_poly *v) { mlk_polyvec_compress_du(r, b); mlk_poly_compress_dv(r + MLKEM_POLYVECCOMPRESSEDBYTES_DU, v); @@ -171,7 +169,7 @@ static void mlk_pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], * Implements @[FIPS203, Algorithm 15 (K-PKE.Decrypt), L1-4] * **************************************************/ -static void mlk_unpack_ciphertext(mlk_polyvec *b, mlk_poly *v, +static void mlk_unpack_ciphertext(mlk_polyvec b, mlk_poly *v, const uint8_t c[MLKEM_INDCPA_BYTES]) { mlk_polyvec_decompress_du(b, c); @@ -245,7 +243,7 @@ __contract__( * * Not static for benchmarking */ MLK_INTERNAL_API -void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES], +void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES], int transposed) { unsigned i, j; @@ -278,11 +276,7 @@ void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES], } } - mlk_poly_rej_uniform_x4(&a->vec[i / MLKEM_K].vec[i % MLKEM_K], - &a->vec[(i + 1) / MLKEM_K].vec[(i + 1) % MLKEM_K], - &a->vec[(i + 2) / MLKEM_K].vec[(i + 2) % MLKEM_K], - &a->vec[(i + 3) / MLKEM_K].vec[(i + 3) % MLKEM_K], - seed_ext); + mlk_poly_rej_uniform_x4(&a[i], &a[i + 1], &a[i + 2], &a[i + 3], seed_ext); } #else /* !MLK_CONFIG_SERIAL_FIPS202_ONLY */ /* When using serial FIPS202, sample all entries individually. */ @@ -310,7 +304,7 @@ void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES], seed_ext[0][MLKEM_SYMBYTES + 1] = x; } - mlk_poly_rej_uniform(&a->vec[i / MLKEM_K].vec[i % MLKEM_K], seed_ext[0]); + mlk_poly_rej_uniform(&a[i], seed_ext[0]); } mlk_assert(i == MLKEM_K * MLKEM_K); @@ -345,36 +339,48 @@ void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES], * Specification: Implements @[FIPS203, Section 2.4.7, Eq (2.12), (2.13)] * **************************************************/ -static void mlk_matvec_mul(mlk_polyvec *out, const mlk_polymat *a, - const mlk_polyvec *v, const mlk_polyvec_mulcache *vc) +static void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a, + const mlk_polyvec v, const mlk_polyvec_mulcache vc) __contract__( requires(memory_no_alias(out, sizeof(mlk_polyvec))) requires(memory_no_alias(a, sizeof(mlk_polymat))) requires(memory_no_alias(v, sizeof(mlk_polyvec))) requires(memory_no_alias(vc, sizeof(mlk_polyvec_mulcache))) - requires(forall(k0, 0, MLKEM_K, - forall(k1, 0, MLKEM_K, - array_bound(a->vec[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))) + requires(forall(k0, 0, MLKEM_K * MLKEM_K, + array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) requires(forall(k1, 0, MLKEM_K, - array_abs_bound(v->vec[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + array_abs_bound(v[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) requires(forall(k2, 0, MLKEM_K, - array_abs_bound(vc->vec[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q))) - assigns(memory_slice(out, sizeof(mlk_polyvec))) + array_abs_bound(vc[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q))) + assigns(object_whole(out)) ensures(forall(k3, 0, MLKEM_K, - array_abs_bound(out->vec[k3].coeffs, 0, MLKEM_N, INT16_MAX/2)))) + array_abs_bound(out[k3].coeffs, 0, MLKEM_N, INT16_MAX/2)))) { - unsigned i; - for (i = 0; i < MLKEM_K; i++) - __loop__( - assigns(i, memory_slice(out, sizeof(mlk_polyvec))) - invariant(i <= MLKEM_K) - invariant(forall(k, 0, i, - array_abs_bound(out->vec[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))) - decreases(MLKEM_K - i)) - { - mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, - vc); - } + /* Temporary on the "refine-bounds" branch - unroll to a simple + * sequence of calls for each possible value of MLKEM_K to + * simplify proof. + */ + mlk_polyvec_basemul_acc_montgomery_cached(&out[0], &a[0], v, vc); + mlk_polyvec_basemul_acc_montgomery_cached(&out[1], &a[MLKEM_K], v, vc); + +#if MLKEM_K == 3 + mlk_polyvec_basemul_acc_montgomery_cached(&out[2], &a[MLKEM_K * 2], v, vc); +#elif MLKEM_K == 4 + mlk_polyvec_basemul_acc_montgomery_cached(&out[2], &a[MLKEM_K * 2], v, vc); + mlk_polyvec_basemul_acc_montgomery_cached(&out[3], &a[MLKEM_K * 3], v, vc); +#endif + + // unsigned i; + // for (i = 0; i < MLKEM_K; i++) + // __loop__( + // assigns(i, object_whole(out)) + // invariant(i <= MLKEM_K) + // invariant(forall(k, 0, i, + // array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))) + // { + // mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, + // vc); + // } } /************************************************* diff --git a/mlkem/src/indcpa.h b/mlkem/src/indcpa.h index b31756dcb6..1ea20bd726 100644 --- a/mlkem/src/indcpa.h +++ b/mlkem/src/indcpa.h @@ -38,7 +38,7 @@ * **************************************************/ MLK_INTERNAL_API -void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES], +void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES], int transposed) __contract__( requires(memory_no_alias(a, sizeof(mlk_polymat))) diff --git a/mlkem/src/poly.c b/mlkem/src/poly.c index 4e3900d327..08aef7f1ed 100644 --- a/mlkem/src/poly.c +++ b/mlkem/src/poly.c @@ -280,6 +280,7 @@ __contract__( requires(memory_no_alias(x, sizeof(mlk_poly_mulcache))) requires(memory_no_alias(a, sizeof(mlk_poly))) assigns(memory_slice(x, sizeof(mlk_poly_mulcache))) + ensures(array_abs_bound(x->coeffs, 0, MLKEM_N/2, MLKEM_Q)) ) { unsigned i; diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c index 27e56a35d9..c0d52257c5 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -45,26 +45,26 @@ * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */ MLK_INTERNAL_API void mlk_polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU], - const mlk_polyvec *a) + const mlk_polyvec a) { unsigned i; mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); for (i = 0; i < MLKEM_K; i++) { - mlk_poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &a->vec[i]); + mlk_poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &a[i]); } } /* Reference: `polyvec_decompress()` in the reference implementation @[REF]. */ MLK_INTERNAL_API -void mlk_polyvec_decompress_du(mlk_polyvec *r, +void mlk_polyvec_decompress_du(mlk_polyvec r, const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES_DU]) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_decompress_du(&r->vec[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU); + mlk_poly_decompress_du(&r[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU); } mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -76,7 +76,7 @@ void mlk_polyvec_decompress_du(mlk_polyvec *r, * The reference implementation works with coefficients * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */ MLK_INTERNAL_API -void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a) +void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec a) { unsigned i; mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -94,12 +94,12 @@ void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a) /* Reference: `polyvec_frombytes()` in the reference implementation @[REF]. */ MLK_INTERNAL_API -void mlk_polyvec_frombytes(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES]) +void mlk_polyvec_frombytes(mlk_polyvec r, const uint8_t a[MLKEM_POLYVECBYTES]) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_frombytes(&r->vec[i], a + i * MLKEM_POLYBYTES); + mlk_poly_frombytes(&r[i], a + i * MLKEM_POLYBYTES); } mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); @@ -107,12 +107,12 @@ void mlk_polyvec_frombytes(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES]) /* Reference: `polyvec_ntt()` in the reference implementation @[REF]. */ MLK_INTERNAL_API -void mlk_polyvec_ntt(mlk_polyvec *r) +void mlk_polyvec_ntt(mlk_polyvec r) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_ntt(&r->vec[i]); + mlk_poly_ntt(&r[i]); } mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLK_NTT_BOUND); @@ -124,12 +124,12 @@ void mlk_polyvec_ntt(mlk_polyvec *r) * the end. This allows us to drop a call to `poly_reduce()` * from the base multiplication. */ MLK_INTERNAL_API -void mlk_polyvec_invntt_tomont(mlk_polyvec *r) +void mlk_polyvec_invntt_tomont(mlk_polyvec r) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_invntt_tomont(&r->vec[i]); + mlk_poly_invntt_tomont(&r[i]); } mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND); @@ -156,7 +156,12 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache))) requires(forall(k1, 0, MLKEM_K, array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(k2, 0, MLKEM_K, + array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + requires(forall(k3, 0, MLKEM_K, + array_abs_bound(b_cache[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q))) assigns(memory_slice(r, sizeof(mlk_poly))) + ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2)) ) { unsigned i; @@ -192,8 +197,8 @@ __contract__( MLK_INTERNAL_API void mlk_polyvec_basemul_acc_montgomery_cached( - mlk_poly *r, const mlk_polyvec *a, const mlk_polyvec *b, - const mlk_polyvec_mulcache *b_cache) + mlk_poly *r, const mlk_polyvec a, const mlk_polyvec b, + const mlk_polyvec_mulcache b_cache) { #if defined(MLK_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED) { @@ -227,12 +232,12 @@ void mlk_polyvec_basemul_acc_montgomery_cached( * multiplication cache ('mulcache'). This idea originates * from @[NeonNTT] and is used at the C level here. */ MLK_INTERNAL_API -void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache *x, const mlk_polyvec *a) +void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache x, const mlk_polyvec a) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_mulcache_compute(&x->vec[i], &a->vec[i]); + mlk_poly_mulcache_compute(&x[i], &a[i]); } } @@ -244,12 +249,12 @@ void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache *x, const mlk_polyvec *a) * This conditional addition is then dropped from all * polynomial compression functions instead (see `compress.c`). */ MLK_INTERNAL_API -void mlk_polyvec_reduce(mlk_polyvec *r) +void mlk_polyvec_reduce(mlk_polyvec r) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_reduce(&r->vec[i]); + mlk_poly_reduce(&r[i]); } mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -259,7 +264,7 @@ void mlk_polyvec_reduce(mlk_polyvec *r) * - We use destructive version (output=first input) to avoid * reasoning about aliasing in the CBMC specification */ MLK_INTERNAL_API -void mlk_polyvec_add(mlk_polyvec *r, const mlk_polyvec *b) +void mlk_polyvec_add(mlk_polyvec r, const mlk_polyvec b) { unsigned i; for (i = 0; i < MLKEM_K; i++) @@ -277,18 +282,18 @@ void mlk_polyvec_add(mlk_polyvec *r, const mlk_polyvec *b) decreases(MLKEM_K - i) ) { - mlk_poly_add(&r->vec[i], &b->vec[i]); + mlk_poly_add(&r[i], &b[i]); } } /* Reference: `polyvec_tomont()` in the reference implementation @[REF]. */ MLK_INTERNAL_API -void mlk_polyvec_tomont(mlk_polyvec *r) +void mlk_polyvec_tomont(mlk_polyvec r) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_tomont(&r->vec[i]); + mlk_poly_tomont(&r[i]); } mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLKEM_Q); diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h index 742e741e65..9cb91e3f31 100644 --- a/mlkem/src/poly_k.h +++ b/mlkem/src/poly_k.h @@ -210,7 +210,7 @@ __contract__( **************************************************/ MLK_INTERNAL_API void mlk_polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU], - const mlk_polyvec *a) + const mlk_polyvec a) __contract__( requires(memory_no_alias(r, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) requires(memory_no_alias(a, sizeof(mlk_polyvec))) @@ -238,14 +238,14 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_decompress_du(mlk_polyvec *r, +void mlk_polyvec_decompress_du(mlk_polyvec r, const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES_DU]) __contract__( requires(memory_no_alias(a, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) requires(memory_no_alias(r, sizeof(mlk_polyvec))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(k0, 0, MLKEM_K, - array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(r[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); #define mlk_polyvec_tobytes MLK_NAMESPACE_K(polyvec_tobytes) @@ -266,7 +266,7 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a) +void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec a) __contract__( requires(memory_no_alias(a, sizeof(mlk_polyvec))) requires(memory_no_alias(r, MLKEM_POLYVECBYTES)) @@ -294,13 +294,13 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_frombytes(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES]) +void mlk_polyvec_frombytes(mlk_polyvec r, const uint8_t a[MLKEM_POLYVECBYTES]) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(memory_no_alias(a, MLKEM_POLYVECBYTES)) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(k0, 0, MLKEM_K, - array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + array_bound(r[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) ); #define mlk_polyvec_ntt MLK_NAMESPACE_K(polyvec_ntt) @@ -323,14 +323,14 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_ntt(mlk_polyvec *r) +void mlk_polyvec_ntt(mlk_polyvec r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(forall(j, 0, MLKEM_K, array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(j, 0, MLKEM_K, - array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) ); #define mlk_polyvec_invntt_tomont MLK_NAMESPACE_K(polyvec_invntt_tomont) @@ -354,14 +354,14 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_invntt_tomont(mlk_polyvec *r) +void mlk_polyvec_invntt_tomont(mlk_polyvec r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(forall(k0, 0, MLKEM_K, array_abs_bound(r->vec[k0].coeffs, 0, MLKEM_N, INT16_MAX/2))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(j, 0, MLKEM_K, - array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND))) + array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND))) ); #define mlk_polyvec_basemul_acc_montgomery_cached \ @@ -396,23 +396,24 @@ __contract__( **************************************************/ MLK_INTERNAL_API void mlk_polyvec_basemul_acc_montgomery_cached( - mlk_poly *r, const mlk_polyvec *a, const mlk_polyvec *b, - const mlk_polyvec_mulcache *b_cache) + mlk_poly *r, const mlk_polyvec a, const mlk_polyvec b, + const mlk_polyvec_mulcache b_cache) __contract__( requires(memory_no_alias(r, sizeof(mlk_poly))) requires(memory_no_alias(a, sizeof(mlk_polyvec))) requires(memory_no_alias(b, sizeof(mlk_polyvec))) requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache))) requires(forall(k1, 0, MLKEM_K, - array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + array_bound(a[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) requires(forall(k2, 0, MLKEM_K, - array_abs_bound(b->vec[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) requires(forall(k3, 0, MLKEM_K, - array_abs_bound(b_cache->vec[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q))) + array_abs_bound(b_cache[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q))) assigns(memory_slice(r, sizeof(mlk_poly))) ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2)) ); + #define mlk_polyvec_mulcache_compute MLK_NAMESPACE_K(polyvec_mulcache_compute) /************************************************************ * Name: mlk_polyvec_mulcache_compute @@ -438,14 +439,19 @@ __contract__( * - Caches `b_1 * \gamma` in @[FIPS203, Algorithm 12, BaseCaseMultiply, L1] * ************************************************************/ +/* + * NOTE: The default C implementation of this function populates + * the mulcache with values in (-q,q), but this is not needed for the + * higher level safety proofs, and thus not part of the spec. + */ MLK_INTERNAL_API -void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache *x, const mlk_polyvec *a) +void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache x, const mlk_polyvec a) __contract__( requires(memory_no_alias(x, sizeof(mlk_polyvec_mulcache))) requires(memory_no_alias(a, sizeof(mlk_polyvec))) assigns(memory_slice(x, sizeof(mlk_polyvec_mulcache))) ensures(forall(k0, 0, MLKEM_K, - array_abs_bound(x->vec[k0].coeffs, 0, MLKEM_N/2, MLKEM_Q))) + array_abs_bound(x[k0].coeffs, 0, MLKEM_N/2, MLKEM_Q))) ); #define mlk_polyvec_reduce MLK_NAMESPACE_K(polyvec_reduce) @@ -471,12 +477,12 @@ __contract__( * use of mlk_poly_reduce() in the context of (de)serialization. */ MLK_INTERNAL_API -void mlk_polyvec_reduce(mlk_polyvec *r) +void mlk_polyvec_reduce(mlk_polyvec r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(k0, 0, MLKEM_K, - array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(r[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); #define mlk_polyvec_add MLK_NAMESPACE_K(polyvec_add) @@ -503,13 +509,13 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_add(mlk_polyvec *r, const mlk_polyvec *b) +void mlk_polyvec_add(mlk_polyvec r, const mlk_polyvec b) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(memory_no_alias(b, sizeof(mlk_polyvec))) requires(forall(j0, 0, MLKEM_K, forall(k0, 0, MLKEM_N, - (int32_t)r->vec[j0].coeffs[k0] + b->vec[j0].coeffs[k0] <= INT16_MAX))) + (int32_t)r[j0].coeffs[k0] + b[j0].coeffs[k0] <= INT16_MAX))) requires(forall(j1, 0, MLKEM_K, forall(k1, 0, MLKEM_N, (int32_t)r->vec[j1].coeffs[k1] + b->vec[j1].coeffs[k1] >= INT16_MIN))) @@ -532,12 +538,12 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_tomont(mlk_polyvec *r) +void mlk_polyvec_tomont(mlk_polyvec r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(j, 0, MLKEM_K, - array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q))) + array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLKEM_Q))) ); #define mlk_poly_getnoise_eta1_4x MLK_NAMESPACE_K(poly_getnoise_eta1_4x) diff --git a/proofs/cbmc/polyvec_add/polyvec_add_harness.c b/proofs/cbmc/polyvec_add/polyvec_add_harness.c index 5923c177ff..4a6cdeca90 100644 --- a/proofs/cbmc/polyvec_add/polyvec_add_harness.c +++ b/proofs/cbmc/polyvec_add/polyvec_add_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_polyvec *r, *b; + mlk_poly *r, *b; mlk_polyvec_add(r, b); } diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c index 0f8d7355bb..869e078421 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c @@ -7,8 +7,8 @@ void harness(void) { mlk_poly *r; - mlk_polyvec *a, *b; - mlk_polyvec_mulcache *b_cached; + mlk_poly *a, *b; + mlk_poly_mulcache *b_cached; mlk_polyvec_basemul_acc_montgomery_cached(r, a, b, b_cached); } diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c index 0f8d7355bb..869e078421 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c @@ -7,8 +7,8 @@ void harness(void) { mlk_poly *r; - mlk_polyvec *a, *b; - mlk_polyvec_mulcache *b_cached; + mlk_poly *a, *b; + mlk_poly_mulcache *b_cached; mlk_polyvec_basemul_acc_montgomery_cached(r, a, b, b_cached); } diff --git a/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c b/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c index 5fd0899be0..5b7df4dd11 100644 --- a/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c +++ b/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_polyvec *r; + mlk_poly *r; uint8_t *a; mlk_polyvec_compress_du(a, r); diff --git a/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c b/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c index 9b2dbc6da1..853d555046 100644 --- a/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c +++ b/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_polyvec *a; + mlk_poly *a; uint8_t *r; mlk_polyvec_decompress_du(a, r); diff --git a/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c b/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c index 9a200adf63..02e9d3d576 100644 --- a/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c +++ b/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c @@ -6,7 +6,7 @@ void harness(void) { - mlk_polyvec *a; + mlk_poly *a; uint8_t *r; mlk_polyvec_frombytes(a, r); } diff --git a/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c b/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c index e8bf6e6546..b86aff4f77 100644 --- a/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c +++ b/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_polyvec *r; + mlk_poly *r; mlk_polyvec_invntt_tomont(r); } diff --git a/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c b/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c index b560a52706..53d4178406 100644 --- a/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c +++ b/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c @@ -6,8 +6,8 @@ void harness(void) { - mlk_polyvec_mulcache *x; - mlk_polyvec *a; + mlk_poly_mulcache *x; + mlk_poly *a; mlk_polyvec_mulcache_compute(x, a); } diff --git a/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c index 03690ecc01..3c4d15c5f4 100644 --- a/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c +++ b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_polyvec *r; + mlk_poly *r; mlk_polyvec_ntt(r); } diff --git a/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c b/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c index 26b38a3636..a3d0fb4d83 100644 --- a/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c +++ b/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_polyvec *a; + mlk_poly *a; mlk_polyvec_reduce(a); } diff --git a/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c b/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c index 16616aa1aa..9ccb5961ae 100644 --- a/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c +++ b/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c @@ -6,7 +6,7 @@ void harness(void) { - mlk_polyvec *a; + mlk_poly *a; uint8_t *r; mlk_polyvec_tobytes(r, a); } diff --git a/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c b/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c index 72ee9743b2..9561889df4 100644 --- a/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c +++ b/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_polyvec *a; + mlk_poly *a; mlk_polyvec_tomont(a); } From fc96603bc1dac30e236657d2fbbe6cf6f0e382e8 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:21:24 +0100 Subject: [PATCH 04/12] Use C90 comments /* */ not C99 // style. Signed-off-by: Rod Chapman --- mlkem/src/indcpa.c | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 41597876cd..0eba5d7c5f 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -370,17 +370,18 @@ __contract__( mlk_polyvec_basemul_acc_montgomery_cached(&out[3], &a[MLKEM_K * 3], v, vc); #endif - // unsigned i; - // for (i = 0; i < MLKEM_K; i++) - // __loop__( - // assigns(i, object_whole(out)) - // invariant(i <= MLKEM_K) - // invariant(forall(k, 0, i, - // array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))) - // { - // mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, - // vc); - // } + /* unsigned i; + * for (i = 0; i < MLKEM_K; i++) + * __loop__( + * assigns(i, object_whole(out)) + * invariant(i <= MLKEM_K) + * invariant(forall(k, 0, i, + * array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))) + * { + * mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, + * vc); + * } + */ } /************************************************* From e26b222c98003836676370fbf501145054d0635b Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:36:30 +0100 Subject: [PATCH 05/12] Update component testing code for new type signatures. Signed-off-by: Rod Chapman --- test/bench/bench_components_mlkem.c | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/test/bench/bench_components_mlkem.c b/test/bench/bench_components_mlkem.c index 6ca262b7be..8bcfa16b56 100644 --- a/test/bench/bench_components_mlkem.c +++ b/test/bench/bench_components_mlkem.c @@ -160,52 +160,52 @@ static int bench(void) /* mlk_polyvec */ /* mlk_polyvec_compress_du */ BENCH("mlk_polyvec_compress_du", - mlk_polyvec_compress_du((uint8_t *)data0, (const mlk_polyvec *)data1)) + mlk_polyvec_compress_du((uint8_t *)data0, (const mlk_poly *)data1)) /* mlk_polyvec_decompress_du */ BENCH("mlk_polyvec_decompress_du", - mlk_polyvec_decompress_du((mlk_polyvec *)data0, (uint8_t *)data1)) + mlk_polyvec_decompress_du((mlk_poly *)data0, (uint8_t *)data1)) /* mlk_polyvec_tobytes */ BENCH("mlk_polyvec_tobytes", - mlk_polyvec_tobytes((uint8_t *)data0, (const mlk_polyvec *)data1)) + mlk_polyvec_tobytes((uint8_t *)data0, (const mlk_poly *)data1)) /* mlk_polyvec_frombytes */ BENCH("mlk_polyvec_frombytes", - mlk_polyvec_frombytes((mlk_polyvec *)data0, (uint8_t *)data1)) + mlk_polyvec_frombytes((mlk_poly *)data0, (uint8_t *)data1)) /* mlk_polyvec_ntt */ - BENCH("mlk_polyvec_ntt", mlk_polyvec_ntt((mlk_polyvec *)data0)) + BENCH("mlk_polyvec_ntt", mlk_polyvec_ntt((mlk_poly *)data0)) /* mlk_polyvec_invntt_tomont */ BENCH("mlk_polyvec_invntt_tomont", - mlk_polyvec_invntt_tomont((mlk_polyvec *)data0)) + mlk_polyvec_invntt_tomont((mlk_poly *)data0)) /* mlk_polyvec_basemul_acc_montgomery_cached */ BENCH("mlk_polyvec_basemul_acc_montgomery_cached", mlk_polyvec_basemul_acc_montgomery_cached( - (mlk_poly *)data0, (const mlk_polyvec *)data1, - (const mlk_polyvec *)data2, (const mlk_polyvec_mulcache *)data3)) + (mlk_poly *)data0, (const mlk_poly *)data1, (const mlk_poly *)data2, + (const mlk_poly_mulcache *)data3)) /* mlk_polyvec_mulcache_compute */ BENCH("mlk_polyvec_mulcache_compute", - mlk_polyvec_mulcache_compute((mlk_polyvec_mulcache *)data0, - (const mlk_polyvec *)data1)) + mlk_polyvec_mulcache_compute((mlk_poly_mulcache *)data0, + (const mlk_poly *)data1)) /* mlk_polyvec_reduce */ - BENCH("mlk_polyvec_reduce", mlk_polyvec_reduce((mlk_polyvec *)data0)) + BENCH("mlk_polyvec_reduce", mlk_polyvec_reduce((mlk_poly *)data0)) /* mlk_polyvec_add */ BENCH("mlk_polyvec_add", - mlk_polyvec_add((mlk_polyvec *)data0, (const mlk_polyvec *)data1)) + mlk_polyvec_add((mlk_poly *)data0, (const mlk_poly *)data1)) /* mlk_polyvec_tomont */ - BENCH("mlk_polyvec_tomont", mlk_polyvec_tomont((mlk_polyvec *)data0)) + BENCH("mlk_polyvec_tomont", mlk_polyvec_tomont((mlk_poly *)data0)) /* indcpa */ /* mlk_gen_matrix */ BENCH("mlk_gen_matrix", - mlk_gen_matrix((mlk_polymat *)data0, (uint8_t *)data1, 0)) + mlk_gen_matrix((mlk_poly *)data0, (uint8_t *)data1, 0)) #if defined(MLK_ARITH_BACKEND_AARCH64) From 3b856e9c8c6839f7bb45fad7dd9f640e12172da4 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:58:10 +0100 Subject: [PATCH 06/12] Re-generate auto-generated files to meet lint requirements. Signed-off-by: Rod Chapman --- test/bench/bench_components_mlkem.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/bench/bench_components_mlkem.c b/test/bench/bench_components_mlkem.c index 8bcfa16b56..9331bc3baa 100644 --- a/test/bench/bench_components_mlkem.c +++ b/test/bench/bench_components_mlkem.c @@ -84,7 +84,7 @@ static int bench(void) BENCH("mlk_poly_rej_uniform_x4", mlk_poly_rej_uniform_x4((mlk_poly *)data0, (mlk_poly *)data1, (mlk_poly *)data2, (mlk_poly *)data3, - (uint8_t (*)[64])data4)) + (uint8_t(*)[64])data4)) /* mlk_poly */ /* mlk_poly_compress_du */ From a495f8c5ea948b817d02b30389e496d76e184f9c Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 11:19:45 +0100 Subject: [PATCH 07/12] Update post-condition on native implementions of polyvec_basemul_acc_montgomery_cached_asm_k[234] TODO - Re-check specifications and proof of AArch64 implementations of these 3 functions. Signed-off-by: Rod Chapman --- mlkem/src/native/aarch64/src/arith_native_aarch64.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/mlkem/src/native/aarch64/src/arith_native_aarch64.h b/mlkem/src/native/aarch64/src/arith_native_aarch64.h index 2941ecbd4b..3468a0f072 100644 --- a/mlkem/src/native/aarch64/src/arith_native_aarch64.h +++ b/mlkem/src/native/aarch64/src/arith_native_aarch64.h @@ -115,6 +115,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N)) @@ -122,6 +125,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \ @@ -132,6 +136,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N)) @@ -139,6 +146,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \ @@ -149,6 +157,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N)) @@ -156,6 +167,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm) From 1681c4a82aaa2d78743f7cb26544f23368333444 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 11:41:15 +0100 Subject: [PATCH 08/12] Update master copies of AArch64 arithmetic back-end specs. Signed-off-by: Rod Chapman --- dev/aarch64_clean/src/arith_native_aarch64.h | 12 ++++++++++++ dev/aarch64_opt/src/arith_native_aarch64.h | 12 ++++++++++++ 2 files changed, 24 insertions(+) diff --git a/dev/aarch64_clean/src/arith_native_aarch64.h b/dev/aarch64_clean/src/arith_native_aarch64.h index fc62ac2279..f8dc4bbb89 100644 --- a/dev/aarch64_clean/src/arith_native_aarch64.h +++ b/dev/aarch64_clean/src/arith_native_aarch64.h @@ -115,6 +115,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N)) @@ -122,6 +125,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \ @@ -132,6 +136,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N)) @@ -139,6 +146,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \ @@ -149,6 +157,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N)) @@ -156,6 +167,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm) diff --git a/dev/aarch64_opt/src/arith_native_aarch64.h b/dev/aarch64_opt/src/arith_native_aarch64.h index bce864a299..6c694bee9e 100644 --- a/dev/aarch64_opt/src/arith_native_aarch64.h +++ b/dev/aarch64_opt/src/arith_native_aarch64.h @@ -115,6 +115,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N)) @@ -122,6 +125,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \ @@ -132,6 +136,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N)) @@ -139,6 +146,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \ @@ -149,6 +157,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4( /* This must be kept in sync with the HOL-Light specification in * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml. */ +/* TODO - refine_bounds branch - Check HOL-Light specification has the + * INT16_MAX/2 bound on post-condition and re-prove/ + */ __contract__( requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N)) @@ -156,6 +167,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2))) requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm) From 908d19801b43127cb98cd9a9e0095846f627bb5c Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Sun, 2 Nov 2025 05:35:24 +0000 Subject: [PATCH 09/12] Switch mlk_polyvec and mlk_polymat to struct wrappers - Change mlk_polyvec back to struct `{ mlk_poly vec[MLKEM_K]; }` - Change mlk_polymat to struct `{ mlk_polyvec vec[MLKEM_K]; }` - Update all function signatures to use pointer style - Fix all implementations to use struct member access - Update tests, benchmarks, and CBMC harnesses - Add consistent const annotations Signed-off-by: Hanno Becker --- mlkem/src/indcpa.c | 72 +++++++++---------- mlkem/src/indcpa.h | 2 +- mlkem/src/poly_k.c | 42 +++++------ mlkem/src/poly_k.h | 40 +++++------ proofs/cbmc/polyvec_add/polyvec_add_harness.c | 2 +- ...ec_basemul_acc_montgomery_cached_harness.c | 4 +- ...mul_acc_montgomery_cached_native_harness.c | 4 +- .../polyvec_compress_du_harness.c | 2 +- .../polyvec_decompress_du_harness.c | 2 +- .../polyvec_frombytes_harness.c | 2 +- .../polyvec_invntt_tomont_harness.c | 2 +- .../polyvec_mulcache_compute_harness.c | 4 +- proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c | 2 +- .../polyvec_reduce/polyvec_reduce_harness.c | 2 +- .../polyvec_tobytes/polyvec_tobytes_harness.c | 2 +- .../polyvec_tomont/polyvec_tomont_harness.c | 2 +- test/bench/bench_components_mlkem.c | 28 ++++---- 17 files changed, 103 insertions(+), 111 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 0eba5d7c5f..aba5261d9c 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -58,7 +58,8 @@ * Implements @[FIPS203, Algorithm 13 (K-PKE.KeyGen), L19] * **************************************************/ -static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], mlk_polyvec pk, +static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], + const mlk_polyvec *pk, const uint8_t seed[MLKEM_SYMBYTES]) { mlk_assert_bound_2d(pk->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -82,7 +83,7 @@ static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], mlk_polyvec pk, * Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt), L2-3] * **************************************************/ -static void mlk_unpack_pk(mlk_polyvec pk, uint8_t seed[MLKEM_SYMBYTES], +static void mlk_unpack_pk(mlk_polyvec *pk, uint8_t seed[MLKEM_SYMBYTES], const uint8_t packedpk[MLKEM_INDCPA_PUBLICKEYBYTES]) { mlk_polyvec_frombytes(pk, packedpk); @@ -107,7 +108,8 @@ static void mlk_unpack_pk(mlk_polyvec pk, uint8_t seed[MLKEM_SYMBYTES], * Implements @[FIPS203, Algorithm 13 (K-PKE.KeyGen), L20] * **************************************************/ -static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], mlk_polyvec sk) +static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], + const mlk_polyvec *sk) { mlk_assert_bound_2d(sk->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); mlk_polyvec_tobytes(r, sk); @@ -127,7 +129,7 @@ static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], mlk_polyvec sk) * Implements @[FIPS203, Algorithm 15 (K-PKE.Decrypt), L5] * **************************************************/ -static void mlk_unpack_sk(mlk_polyvec sk, +static void mlk_unpack_sk(mlk_polyvec *sk, const uint8_t packedsk[MLKEM_INDCPA_SECRETKEYBYTES]) { mlk_polyvec_frombytes(sk, packedsk); @@ -148,8 +150,8 @@ static void mlk_unpack_sk(mlk_polyvec sk, * Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt), L22-23] * **************************************************/ -static void mlk_pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], mlk_polyvec b, - mlk_poly *v) +static void mlk_pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], + const mlk_polyvec *b, mlk_poly *v) { mlk_polyvec_compress_du(r, b); mlk_poly_compress_dv(r + MLKEM_POLYVECCOMPRESSEDBYTES_DU, v); @@ -169,7 +171,7 @@ static void mlk_pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], mlk_polyvec b, * Implements @[FIPS203, Algorithm 15 (K-PKE.Decrypt), L1-4] * **************************************************/ -static void mlk_unpack_ciphertext(mlk_polyvec b, mlk_poly *v, +static void mlk_unpack_ciphertext(mlk_polyvec *b, mlk_poly *v, const uint8_t c[MLKEM_INDCPA_BYTES]) { mlk_polyvec_decompress_du(b, c); @@ -243,7 +245,7 @@ __contract__( * * Not static for benchmarking */ MLK_INTERNAL_API -void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES], +void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed) { unsigned i, j; @@ -276,7 +278,11 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES], } } - mlk_poly_rej_uniform_x4(&a[i], &a[i + 1], &a[i + 2], &a[i + 3], seed_ext); + mlk_poly_rej_uniform_x4(&a->vec[i / MLKEM_K].vec[i % MLKEM_K], + &a->vec[(i + 1) / MLKEM_K].vec[(i + 1) % MLKEM_K], + &a->vec[(i + 2) / MLKEM_K].vec[(i + 2) % MLKEM_K], + &a->vec[(i + 3) / MLKEM_K].vec[(i + 3) % MLKEM_K], + seed_ext); } #else /* !MLK_CONFIG_SERIAL_FIPS202_ONLY */ /* When using serial FIPS202, sample all entries individually. */ @@ -304,7 +310,7 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES], seed_ext[0][MLKEM_SYMBYTES + 1] = x; } - mlk_poly_rej_uniform(&a[i], seed_ext[0]); + mlk_poly_rej_uniform(&a->vec[i / MLKEM_K].vec[i % MLKEM_K], seed_ext[0]); } mlk_assert(i == MLKEM_K * MLKEM_K); @@ -339,15 +345,16 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES], * Specification: Implements @[FIPS203, Section 2.4.7, Eq (2.12), (2.13)] * **************************************************/ -static void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a, - const mlk_polyvec v, const mlk_polyvec_mulcache vc) +static void mlk_matvec_mul(mlk_polyvec *out, const mlk_polymat *a, + const mlk_polyvec *v, const mlk_polyvec_mulcache *vc) __contract__( requires(memory_no_alias(out, sizeof(mlk_polyvec))) requires(memory_no_alias(a, sizeof(mlk_polymat))) requires(memory_no_alias(v, sizeof(mlk_polyvec))) requires(memory_no_alias(vc, sizeof(mlk_polyvec_mulcache))) - requires(forall(k0, 0, MLKEM_K * MLKEM_K, - array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + requires(forall(k0, 0, MLKEM_K, + forall(k1, 0, MLKEM_K, + array_bound(a->vec[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))) requires(forall(k1, 0, MLKEM_K, array_abs_bound(v[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) requires(forall(k2, 0, MLKEM_K, @@ -356,32 +363,17 @@ __contract__( ensures(forall(k3, 0, MLKEM_K, array_abs_bound(out[k3].coeffs, 0, MLKEM_N, INT16_MAX/2)))) { - /* Temporary on the "refine-bounds" branch - unroll to a simple - * sequence of calls for each possible value of MLKEM_K to - * simplify proof. - */ - mlk_polyvec_basemul_acc_montgomery_cached(&out[0], &a[0], v, vc); - mlk_polyvec_basemul_acc_montgomery_cached(&out[1], &a[MLKEM_K], v, vc); - -#if MLKEM_K == 3 - mlk_polyvec_basemul_acc_montgomery_cached(&out[2], &a[MLKEM_K * 2], v, vc); -#elif MLKEM_K == 4 - mlk_polyvec_basemul_acc_montgomery_cached(&out[2], &a[MLKEM_K * 2], v, vc); - mlk_polyvec_basemul_acc_montgomery_cached(&out[3], &a[MLKEM_K * 3], v, vc); -#endif - - /* unsigned i; - * for (i = 0; i < MLKEM_K; i++) - * __loop__( - * assigns(i, object_whole(out)) - * invariant(i <= MLKEM_K) - * invariant(forall(k, 0, i, - * array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))) - * { - * mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, - * vc); - * } - */ + unsigned i; + for (i = 0; i < MLKEM_K; i++) + __loop__( + assigns(i, object_whole(out)) + invariant(i <= MLKEM_K)) + invariant(forall(k, 0, i, + array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))) + { + mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, + vc); + } } /************************************************* diff --git a/mlkem/src/indcpa.h b/mlkem/src/indcpa.h index 1ea20bd726..b31756dcb6 100644 --- a/mlkem/src/indcpa.h +++ b/mlkem/src/indcpa.h @@ -38,7 +38,7 @@ * **************************************************/ MLK_INTERNAL_API -void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES], +void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed) __contract__( requires(memory_no_alias(a, sizeof(mlk_polymat))) diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c index c0d52257c5..30bbd192c1 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -45,26 +45,26 @@ * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */ MLK_INTERNAL_API void mlk_polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU], - const mlk_polyvec a) + const mlk_polyvec *a) { unsigned i; mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); for (i = 0; i < MLKEM_K; i++) { - mlk_poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &a[i]); + mlk_poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &a->vec[i]); } } /* Reference: `polyvec_decompress()` in the reference implementation @[REF]. */ MLK_INTERNAL_API -void mlk_polyvec_decompress_du(mlk_polyvec r, +void mlk_polyvec_decompress_du(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES_DU]) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_decompress_du(&r[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU); + mlk_poly_decompress_du(&r->vec[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU); } mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -76,7 +76,7 @@ void mlk_polyvec_decompress_du(mlk_polyvec r, * The reference implementation works with coefficients * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */ MLK_INTERNAL_API -void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec a) +void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a) { unsigned i; mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -94,12 +94,12 @@ void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec a) /* Reference: `polyvec_frombytes()` in the reference implementation @[REF]. */ MLK_INTERNAL_API -void mlk_polyvec_frombytes(mlk_polyvec r, const uint8_t a[MLKEM_POLYVECBYTES]) +void mlk_polyvec_frombytes(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES]) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_frombytes(&r[i], a + i * MLKEM_POLYBYTES); + mlk_poly_frombytes(&r->vec[i], a + i * MLKEM_POLYBYTES); } mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); @@ -107,12 +107,12 @@ void mlk_polyvec_frombytes(mlk_polyvec r, const uint8_t a[MLKEM_POLYVECBYTES]) /* Reference: `polyvec_ntt()` in the reference implementation @[REF]. */ MLK_INTERNAL_API -void mlk_polyvec_ntt(mlk_polyvec r) +void mlk_polyvec_ntt(mlk_polyvec *r) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_ntt(&r[i]); + mlk_poly_ntt(&r->vec[i]); } mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLK_NTT_BOUND); @@ -124,12 +124,12 @@ void mlk_polyvec_ntt(mlk_polyvec r) * the end. This allows us to drop a call to `poly_reduce()` * from the base multiplication. */ MLK_INTERNAL_API -void mlk_polyvec_invntt_tomont(mlk_polyvec r) +void mlk_polyvec_invntt_tomont(mlk_polyvec *r) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_invntt_tomont(&r[i]); + mlk_poly_invntt_tomont(&r->vec[i]); } mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND); @@ -197,8 +197,8 @@ __contract__( MLK_INTERNAL_API void mlk_polyvec_basemul_acc_montgomery_cached( - mlk_poly *r, const mlk_polyvec a, const mlk_polyvec b, - const mlk_polyvec_mulcache b_cache) + mlk_poly *r, const mlk_polyvec *a, const mlk_polyvec *b, + const mlk_polyvec_mulcache *b_cache) { #if defined(MLK_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED) { @@ -232,12 +232,12 @@ void mlk_polyvec_basemul_acc_montgomery_cached( * multiplication cache ('mulcache'). This idea originates * from @[NeonNTT] and is used at the C level here. */ MLK_INTERNAL_API -void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache x, const mlk_polyvec a) +void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache *x, const mlk_polyvec *a) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_mulcache_compute(&x[i], &a[i]); + mlk_poly_mulcache_compute(&x->vec[i], &a->vec[i]); } } @@ -249,12 +249,12 @@ void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache x, const mlk_polyvec a) * This conditional addition is then dropped from all * polynomial compression functions instead (see `compress.c`). */ MLK_INTERNAL_API -void mlk_polyvec_reduce(mlk_polyvec r) +void mlk_polyvec_reduce(mlk_polyvec *r) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_reduce(&r[i]); + mlk_poly_reduce(&r->vec[i]); } mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -264,7 +264,7 @@ void mlk_polyvec_reduce(mlk_polyvec r) * - We use destructive version (output=first input) to avoid * reasoning about aliasing in the CBMC specification */ MLK_INTERNAL_API -void mlk_polyvec_add(mlk_polyvec r, const mlk_polyvec b) +void mlk_polyvec_add(mlk_polyvec *r, const mlk_polyvec *b) { unsigned i; for (i = 0; i < MLKEM_K; i++) @@ -282,18 +282,18 @@ void mlk_polyvec_add(mlk_polyvec r, const mlk_polyvec b) decreases(MLKEM_K - i) ) { - mlk_poly_add(&r[i], &b[i]); + mlk_poly_add(&r->vec[i], &b->vec[i]); } } /* Reference: `polyvec_tomont()` in the reference implementation @[REF]. */ MLK_INTERNAL_API -void mlk_polyvec_tomont(mlk_polyvec r) +void mlk_polyvec_tomont(mlk_polyvec *r) { unsigned i; for (i = 0; i < MLKEM_K; i++) { - mlk_poly_tomont(&r[i]); + mlk_poly_tomont(&r->vec[i]); } mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLKEM_Q); diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h index 9cb91e3f31..700fc8d92f 100644 --- a/mlkem/src/poly_k.h +++ b/mlkem/src/poly_k.h @@ -210,7 +210,7 @@ __contract__( **************************************************/ MLK_INTERNAL_API void mlk_polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU], - const mlk_polyvec a) + const mlk_polyvec *a) __contract__( requires(memory_no_alias(r, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) requires(memory_no_alias(a, sizeof(mlk_polyvec))) @@ -238,14 +238,14 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_decompress_du(mlk_polyvec r, +void mlk_polyvec_decompress_du(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES_DU]) __contract__( requires(memory_no_alias(a, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) requires(memory_no_alias(r, sizeof(mlk_polyvec))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(k0, 0, MLKEM_K, - array_bound(r[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); #define mlk_polyvec_tobytes MLK_NAMESPACE_K(polyvec_tobytes) @@ -266,7 +266,7 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec a) +void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a) __contract__( requires(memory_no_alias(a, sizeof(mlk_polyvec))) requires(memory_no_alias(r, MLKEM_POLYVECBYTES)) @@ -294,13 +294,13 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_frombytes(mlk_polyvec r, const uint8_t a[MLKEM_POLYVECBYTES]) +void mlk_polyvec_frombytes(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES]) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(memory_no_alias(a, MLKEM_POLYVECBYTES)) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(k0, 0, MLKEM_K, - array_bound(r[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) ); #define mlk_polyvec_ntt MLK_NAMESPACE_K(polyvec_ntt) @@ -323,14 +323,14 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_ntt(mlk_polyvec r) +void mlk_polyvec_ntt(mlk_polyvec *r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(forall(j, 0, MLKEM_K, array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(j, 0, MLKEM_K, - array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) ); #define mlk_polyvec_invntt_tomont MLK_NAMESPACE_K(polyvec_invntt_tomont) @@ -354,14 +354,14 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_invntt_tomont(mlk_polyvec r) +void mlk_polyvec_invntt_tomont(mlk_polyvec *r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(forall(k0, 0, MLKEM_K, array_abs_bound(r->vec[k0].coeffs, 0, MLKEM_N, INT16_MAX/2))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(j, 0, MLKEM_K, - array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND))) + array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND))) ); #define mlk_polyvec_basemul_acc_montgomery_cached \ @@ -396,15 +396,15 @@ __contract__( **************************************************/ MLK_INTERNAL_API void mlk_polyvec_basemul_acc_montgomery_cached( - mlk_poly *r, const mlk_polyvec a, const mlk_polyvec b, - const mlk_polyvec_mulcache b_cache) + mlk_poly *r, const mlk_polyvec *a, const mlk_polyvec *b, + const mlk_polyvec_mulcache *b_cache) __contract__( requires(memory_no_alias(r, sizeof(mlk_poly))) requires(memory_no_alias(a, sizeof(mlk_polyvec))) requires(memory_no_alias(b, sizeof(mlk_polyvec))) requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache))) requires(forall(k1, 0, MLKEM_K, - array_bound(a[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) + array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) requires(forall(k2, 0, MLKEM_K, array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) requires(forall(k3, 0, MLKEM_K, @@ -445,7 +445,7 @@ __contract__( * higher level safety proofs, and thus not part of the spec. */ MLK_INTERNAL_API -void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache x, const mlk_polyvec a) +void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache *x, const mlk_polyvec *a) __contract__( requires(memory_no_alias(x, sizeof(mlk_polyvec_mulcache))) requires(memory_no_alias(a, sizeof(mlk_polyvec))) @@ -477,12 +477,12 @@ __contract__( * use of mlk_poly_reduce() in the context of (de)serialization. */ MLK_INTERNAL_API -void mlk_polyvec_reduce(mlk_polyvec r) +void mlk_polyvec_reduce(mlk_polyvec *r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(k0, 0, MLKEM_K, - array_bound(r[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); #define mlk_polyvec_add MLK_NAMESPACE_K(polyvec_add) @@ -509,13 +509,13 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_add(mlk_polyvec r, const mlk_polyvec b) +void mlk_polyvec_add(mlk_polyvec *r, const mlk_polyvec *b) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) requires(memory_no_alias(b, sizeof(mlk_polyvec))) requires(forall(j0, 0, MLKEM_K, forall(k0, 0, MLKEM_N, - (int32_t)r[j0].coeffs[k0] + b[j0].coeffs[k0] <= INT16_MAX))) + (int32_t)r->vec[j0].coeffs[k0] + b->vec[j0].coeffs[k0] <= INT16_MAX))) requires(forall(j1, 0, MLKEM_K, forall(k1, 0, MLKEM_N, (int32_t)r->vec[j1].coeffs[k1] + b->vec[j1].coeffs[k1] >= INT16_MIN))) @@ -538,12 +538,12 @@ __contract__( * **************************************************/ MLK_INTERNAL_API -void mlk_polyvec_tomont(mlk_polyvec r) +void mlk_polyvec_tomont(mlk_polyvec *r) __contract__( requires(memory_no_alias(r, sizeof(mlk_polyvec))) assigns(memory_slice(r, sizeof(mlk_polyvec))) ensures(forall(j, 0, MLKEM_K, - array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLKEM_Q))) + array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q))) ); #define mlk_poly_getnoise_eta1_4x MLK_NAMESPACE_K(poly_getnoise_eta1_4x) diff --git a/proofs/cbmc/polyvec_add/polyvec_add_harness.c b/proofs/cbmc/polyvec_add/polyvec_add_harness.c index 4a6cdeca90..5923c177ff 100644 --- a/proofs/cbmc/polyvec_add/polyvec_add_harness.c +++ b/proofs/cbmc/polyvec_add/polyvec_add_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_poly *r, *b; + mlk_polyvec *r, *b; mlk_polyvec_add(r, b); } diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c index 869e078421..0f8d7355bb 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c @@ -7,8 +7,8 @@ void harness(void) { mlk_poly *r; - mlk_poly *a, *b; - mlk_poly_mulcache *b_cached; + mlk_polyvec *a, *b; + mlk_polyvec_mulcache *b_cached; mlk_polyvec_basemul_acc_montgomery_cached(r, a, b, b_cached); } diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c index 869e078421..0f8d7355bb 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c @@ -7,8 +7,8 @@ void harness(void) { mlk_poly *r; - mlk_poly *a, *b; - mlk_poly_mulcache *b_cached; + mlk_polyvec *a, *b; + mlk_polyvec_mulcache *b_cached; mlk_polyvec_basemul_acc_montgomery_cached(r, a, b, b_cached); } diff --git a/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c b/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c index 5b7df4dd11..5fd0899be0 100644 --- a/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c +++ b/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_poly *r; + mlk_polyvec *r; uint8_t *a; mlk_polyvec_compress_du(a, r); diff --git a/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c b/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c index 853d555046..9b2dbc6da1 100644 --- a/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c +++ b/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_poly *a; + mlk_polyvec *a; uint8_t *r; mlk_polyvec_decompress_du(a, r); diff --git a/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c b/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c index 02e9d3d576..9a200adf63 100644 --- a/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c +++ b/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c @@ -6,7 +6,7 @@ void harness(void) { - mlk_poly *a; + mlk_polyvec *a; uint8_t *r; mlk_polyvec_frombytes(a, r); } diff --git a/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c b/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c index b86aff4f77..e8bf6e6546 100644 --- a/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c +++ b/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_poly *r; + mlk_polyvec *r; mlk_polyvec_invntt_tomont(r); } diff --git a/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c b/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c index 53d4178406..b560a52706 100644 --- a/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c +++ b/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c @@ -6,8 +6,8 @@ void harness(void) { - mlk_poly_mulcache *x; - mlk_poly *a; + mlk_polyvec_mulcache *x; + mlk_polyvec *a; mlk_polyvec_mulcache_compute(x, a); } diff --git a/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c index 3c4d15c5f4..03690ecc01 100644 --- a/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c +++ b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_poly *r; + mlk_polyvec *r; mlk_polyvec_ntt(r); } diff --git a/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c b/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c index a3d0fb4d83..26b38a3636 100644 --- a/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c +++ b/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_poly *a; + mlk_polyvec *a; mlk_polyvec_reduce(a); } diff --git a/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c b/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c index 9ccb5961ae..16616aa1aa 100644 --- a/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c +++ b/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c @@ -6,7 +6,7 @@ void harness(void) { - mlk_poly *a; + mlk_polyvec *a; uint8_t *r; mlk_polyvec_tobytes(r, a); } diff --git a/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c b/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c index 9561889df4..72ee9743b2 100644 --- a/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c +++ b/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c @@ -6,6 +6,6 @@ void harness(void) { - mlk_poly *a; + mlk_polyvec *a; mlk_polyvec_tomont(a); } diff --git a/test/bench/bench_components_mlkem.c b/test/bench/bench_components_mlkem.c index 9331bc3baa..82ba4ec260 100644 --- a/test/bench/bench_components_mlkem.c +++ b/test/bench/bench_components_mlkem.c @@ -160,52 +160,52 @@ static int bench(void) /* mlk_polyvec */ /* mlk_polyvec_compress_du */ BENCH("mlk_polyvec_compress_du", - mlk_polyvec_compress_du((uint8_t *)data0, (const mlk_poly *)data1)) + mlk_polyvec_compress_du((uint8_t *)data0, (const mlk_polyvec *)data1)) /* mlk_polyvec_decompress_du */ BENCH("mlk_polyvec_decompress_du", - mlk_polyvec_decompress_du((mlk_poly *)data0, (uint8_t *)data1)) + mlk_polyvec_decompress_du((mlk_polyvec *)data0, (uint8_t *)data1)) /* mlk_polyvec_tobytes */ BENCH("mlk_polyvec_tobytes", - mlk_polyvec_tobytes((uint8_t *)data0, (const mlk_poly *)data1)) + mlk_polyvec_tobytes((uint8_t *)data0, (const mlk_polyvec *)data1)) /* mlk_polyvec_frombytes */ BENCH("mlk_polyvec_frombytes", - mlk_polyvec_frombytes((mlk_poly *)data0, (uint8_t *)data1)) + mlk_polyvec_frombytes((mlk_polyvec *)data0, (uint8_t *)data1)) /* mlk_polyvec_ntt */ - BENCH("mlk_polyvec_ntt", mlk_polyvec_ntt((mlk_poly *)data0)) + BENCH("mlk_polyvec_ntt", mlk_polyvec_ntt((mlk_polyvec *)data0)) /* mlk_polyvec_invntt_tomont */ BENCH("mlk_polyvec_invntt_tomont", - mlk_polyvec_invntt_tomont((mlk_poly *)data0)) + mlk_polyvec_invntt_tomont((mlk_polyvec *)data0)) /* mlk_polyvec_basemul_acc_montgomery_cached */ BENCH("mlk_polyvec_basemul_acc_montgomery_cached", mlk_polyvec_basemul_acc_montgomery_cached( - (mlk_poly *)data0, (const mlk_poly *)data1, (const mlk_poly *)data2, - (const mlk_poly_mulcache *)data3)) + (mlk_poly *)data0, (const mlk_polyvec *)data1, + (const mlk_polyvec *)data2, (const mlk_polyvec_mulcache *)data3)) /* mlk_polyvec_mulcache_compute */ BENCH("mlk_polyvec_mulcache_compute", - mlk_polyvec_mulcache_compute((mlk_poly_mulcache *)data0, - (const mlk_poly *)data1)) + mlk_polyvec_mulcache_compute((mlk_polyvec_mulcache *)data0, + (const mlk_polyvec *)data1)) /* mlk_polyvec_reduce */ - BENCH("mlk_polyvec_reduce", mlk_polyvec_reduce((mlk_poly *)data0)) + BENCH("mlk_polyvec_reduce", mlk_polyvec_reduce((mlk_polyvec *)data0)) /* mlk_polyvec_add */ BENCH("mlk_polyvec_add", - mlk_polyvec_add((mlk_poly *)data0, (const mlk_poly *)data1)) + mlk_polyvec_add((mlk_polyvec *)data0, (const mlk_polyvec *)data1)) /* mlk_polyvec_tomont */ - BENCH("mlk_polyvec_tomont", mlk_polyvec_tomont((mlk_poly *)data0)) + BENCH("mlk_polyvec_tomont", mlk_polyvec_tomont((mlk_polyvec *)data0)) /* indcpa */ /* mlk_gen_matrix */ BENCH("mlk_gen_matrix", - mlk_gen_matrix((mlk_poly *)data0, (uint8_t *)data1, 0)) + mlk_gen_matrix((mlk_polymat *)data0, (uint8_t *)data1, 0)) #if defined(MLK_ARITH_BACKEND_AARCH64) From 43d027759b73c010ed58c26d3350c5ce5789c579 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Wed, 17 Dec 2025 11:12:37 +0000 Subject: [PATCH 10/12] Correct build errors following rebase Signed-off-by: Rod Chapman --- mlkem/src/indcpa.c | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index aba5261d9c..27c0e1dd6d 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -367,13 +367,13 @@ __contract__( for (i = 0; i < MLKEM_K; i++) __loop__( assigns(i, object_whole(out)) - invariant(i <= MLKEM_K)) + invariant(i <= MLKEM_K) invariant(forall(k, 0, i, - array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))) - { - mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, - vc); - } + array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2))) + ) + { + mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc); + } } /************************************************* From 1602ef81f370a0325e324931d6ff482543278047 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Wed, 17 Dec 2025 11:26:20 +0000 Subject: [PATCH 11/12] Correct contracts following rebase Signed-off-by: Rod Chapman --- mlkem/src/indcpa.c | 8 ++++---- mlkem/src/poly_k.c | 4 ++-- mlkem/src/poly_k.h | 6 +++--- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 27c0e1dd6d..eb26b97d59 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -356,12 +356,12 @@ __contract__( forall(k1, 0, MLKEM_K, array_bound(a->vec[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))) requires(forall(k1, 0, MLKEM_K, - array_abs_bound(v[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + array_abs_bound(v->vec[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) requires(forall(k2, 0, MLKEM_K, - array_abs_bound(vc[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q))) + array_abs_bound(vc->vec[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q))) assigns(object_whole(out)) ensures(forall(k3, 0, MLKEM_K, - array_abs_bound(out[k3].coeffs, 0, MLKEM_N, INT16_MAX/2)))) + array_abs_bound(out->vec[k3].coeffs, 0, MLKEM_N, INT16_MAX/2)))) { unsigned i; for (i = 0; i < MLKEM_K; i++) @@ -369,7 +369,7 @@ __contract__( assigns(i, object_whole(out)) invariant(i <= MLKEM_K) invariant(forall(k, 0, i, - array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2))) + array_abs_bound(out->vec[k].coeffs, 0, MLKEM_N, INT16_MAX/2))) ) { mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc); diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c index 30bbd192c1..5953a745c1 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -157,9 +157,9 @@ __contract__( requires(forall(k1, 0, MLKEM_K, array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) requires(forall(k2, 0, MLKEM_K, - array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + array_abs_bound(b->vec[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) requires(forall(k3, 0, MLKEM_K, - array_abs_bound(b_cache[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q))) + array_abs_bound(b_cache->vec[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q))) assigns(memory_slice(r, sizeof(mlk_poly))) ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2)) ) diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h index 700fc8d92f..f8b2574b1f 100644 --- a/mlkem/src/poly_k.h +++ b/mlkem/src/poly_k.h @@ -406,9 +406,9 @@ __contract__( requires(forall(k1, 0, MLKEM_K, array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))) requires(forall(k2, 0, MLKEM_K, - array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) + array_abs_bound(b->vec[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND))) requires(forall(k3, 0, MLKEM_K, - array_abs_bound(b_cache[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q))) + array_abs_bound(b_cache->vec[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q))) assigns(memory_slice(r, sizeof(mlk_poly))) ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2)) ); @@ -451,7 +451,7 @@ __contract__( requires(memory_no_alias(a, sizeof(mlk_polyvec))) assigns(memory_slice(x, sizeof(mlk_polyvec_mulcache))) ensures(forall(k0, 0, MLKEM_K, - array_abs_bound(x[k0].coeffs, 0, MLKEM_N/2, MLKEM_Q))) + array_abs_bound(x->vec[k0].coeffs, 0, MLKEM_N/2, MLKEM_Q))) ); #define mlk_polyvec_reduce MLK_NAMESPACE_K(polyvec_reduce) From 7cd3fa08d6d6876be4805269fbd6fd28ef807c5c Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Mon, 23 Mar 2026 17:40:21 +0000 Subject: [PATCH 12/12] Correct loop contracts to add decreases clauses Signed-off-by: Rod Chapman --- mlkem/src/poly_k.c | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c index 5953a745c1..054a3c0908 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -173,26 +173,27 @@ __contract__( for (i = 0; i < MLKEM_N / 2; i++) __loop__( invariant(i <= MLKEM_N / 2) - invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2))) - decreases(MLKEM_N / 2 - i)) - { - unsigned k; - int32_t t[2] = {0}; - for (k = 0; k < MLKEM_K; k++) - __loop__( + invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2)) + decreases(MLKEM_N / 2 - i) + ) + { + unsigned k; + int32_t t[2] = {0}; + for (k = 0; k < MLKEM_K; k++) + __loop__( invariant(k <= MLKEM_K && i <= MLKEM_N / 2) - invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1))) - decreases(MLKEM_K - k)) - { - t[0] += - (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i]; - t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i]; - t[1] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1]; - t[1] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i]; - } - r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]); - r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]); + invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1)) + decreases(MLKEM_K - k) + ) + { + t[0] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i]; + t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i]; + t[1] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1]; + t[1] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i]; } + r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]); + r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]); + } } MLK_INTERNAL_API