From f18ce9fb4f57e8698b5ee46023a9d6b23cbe2864 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Sun, 2 Nov 2025 05:35:24 +0000 Subject: [PATCH 01/10] 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 | 155 ++++++++++-------- mlkem/src/indcpa.h | 6 +- mlkem/src/kem.c | 6 +- mlkem/src/poly_k.c | 76 ++++----- mlkem/src/poly_k.h | 65 +++++--- proofs/cbmc/gen_matrix/gen_matrix_harness.c | 2 +- .../gen_matrix_serial_harness.c | 2 +- proofs/cbmc/matvec_mul/matvec_mul_harness.c | 9 +- ...polymat_permute_bitrev_to_custom_harness.c | 4 +- ..._permute_bitrev_to_custom_native_harness.c | 4 +- proofs/cbmc/polyvec_add/polyvec_add_harness.c | 2 +- ...ec_basemul_acc_montgomery_cached_harness.c | 4 +- ..._basemul_acc_montgomery_cached_c_harness.c | 9 +- ...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_components_mlkem.c | 28 ++-- test/test_unit.c | 28 ++-- 25 files changed, 225 insertions(+), 199 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 0b4315e01d..1e8ebdf74b 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -59,10 +59,11 @@ * 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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); + mlk_assert_bound_2d(pk->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); mlk_polyvec_tobytes(r, pk); mlk_memcpy(r + MLKEM_POLYVECBYTES, seed, MLKEM_SYMBYTES); } @@ -83,7 +84,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); @@ -108,9 +109,10 @@ 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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); + mlk_assert_bound_2d(sk->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); mlk_polyvec_tobytes(r, sk); } @@ -128,7 +130,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); @@ -149,8 +151,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); @@ -170,7 +172,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); @@ -183,16 +185,16 @@ static void mlk_unpack_ciphertext(mlk_polyvec b, mlk_poly *v, * * We don't inline this into gen_matrix to avoid having to split the CBMC * proof for gen_matrix based on MLK_USE_NATIVE_NTT_CUSTOM_ORDER. */ -static void mlk_polymat_permute_bitrev_to_custom(mlk_polymat a) +static void mlk_polymat_permute_bitrev_to_custom(mlk_polymat *a) __contract__( /* We don't specify that this should be a permutation, but only * that it does not change the bound established at the end of mlk_gen_matrix. */ requires(memory_no_alias(a, sizeof(mlk_polymat))) - requires(forall(x, 0, MLKEM_K * MLKEM_K, - array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + requires(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K, + array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) assigns(object_whole(a)) - ensures(forall(x, 0, MLKEM_K * MLKEM_K, - array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) + ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K, + array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))) { #if defined(MLK_USE_NATIVE_NTT_CUSTOM_ORDER) unsigned i; @@ -200,11 +202,12 @@ __contract__( __loop__( assigns(i, object_whole(a)) invariant(i <= MLKEM_K * MLKEM_K) - invariant(forall(x, 0, MLKEM_K * MLKEM_K, - array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + invariant(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K, + array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) ) { - mlk_poly_permute_bitrev_to_custom(a[i].coeffs); + mlk_poly_permute_bitrev_to_custom( + a->vec[i / MLKEM_K].vec[i % MLKEM_K].coeffs); } #else /* MLK_USE_NATIVE_NTT_CUSTOM_ORDER */ /* Nothing to do */ @@ -220,7 +223,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; @@ -253,7 +256,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. */ @@ -281,7 +288,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); @@ -314,15 +321,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)))) assigns(object_whole(out))) { unsigned i; @@ -331,7 +339,7 @@ __contract__( assigns(i, object_whole(out)) invariant(i <= MLKEM_K)) { - mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, vc); + mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc); } } @@ -370,47 +378,49 @@ void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], */ MLK_CT_TESTING_DECLASSIFY(publicseed, MLKEM_SYMBYTES); - mlk_gen_matrix(a, publicseed, 0 /* no transpose */); + mlk_gen_matrix(&a, publicseed, 0 /* no transpose */); #if MLKEM_K == 2 - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &e[0], &e[1], noiseseed, 0, 1, - 2, 3); + mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &e.vec[0], &e.vec[1], + noiseseed, 0, 1, 2, 3); #elif MLKEM_K == 3 /* * Only the first three output buffers are needed. * The laster parameter is a dummy that's overwritten later. */ - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], - &pkpv[0] /* irrelevant */, noiseseed, 0, 1, 2, + mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &skpv.vec[2], + &pkpv.vec[0] /* irrelevant */, noiseseed, 0, 1, 2, 0xFF /* irrelevant */); /* Same here */ - mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &pkpv[0] /* irrelevant */, - noiseseed, 3, 4, 5, 0xFF /* irrelevant */); + mlk_poly_getnoise_eta1_4x(&e.vec[0], &e.vec[1], &e.vec[2], + &pkpv.vec[0] /* irrelevant */, noiseseed, 3, 4, 5, + 0xFF /* irrelevant */); #elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], &skpv[3], noiseseed, - 0, 1, 2, 3); - mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &e[3], noiseseed, 4, 5, 6, 7); -#endif + mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &skpv.vec[2], + &skpv.vec[3], noiseseed, 0, 1, 2, 3); + mlk_poly_getnoise_eta1_4x(&e.vec[0], &e.vec[1], &e.vec[2], &e.vec[3], + noiseseed, 4, 5, 6, 7); +#endif /* MLKEM_K == 4 */ - mlk_polyvec_ntt(skpv); - mlk_polyvec_ntt(e); + mlk_polyvec_ntt(&skpv); + mlk_polyvec_ntt(&e); - mlk_polyvec_mulcache_compute(skpv_cache, skpv); - mlk_matvec_mul(pkpv, a, skpv, skpv_cache); - mlk_polyvec_tomont(pkpv); + mlk_polyvec_mulcache_compute(&skpv_cache, &skpv); + mlk_matvec_mul(&pkpv, &a, &skpv, &skpv_cache); + mlk_polyvec_tomont(&pkpv); - mlk_polyvec_add(pkpv, e); - mlk_polyvec_reduce(pkpv); - mlk_polyvec_reduce(skpv); + mlk_polyvec_add(&pkpv, &e); + mlk_polyvec_reduce(&pkpv); + mlk_polyvec_reduce(&skpv); - mlk_pack_sk(sk, skpv); - mlk_pack_pk(pk, pkpv, publicseed); + mlk_pack_sk(sk, &skpv); + mlk_pack_pk(pk, &pkpv, publicseed); /* Specification: Partially implements * @[FIPS203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(buf, sizeof(buf)); mlk_zeroize(coins_with_domain_separator, sizeof(coins_with_domain_separator)); - mlk_zeroize(a, sizeof(a)); + mlk_zeroize(&a, sizeof(a)); mlk_zeroize(&e, sizeof(e)); mlk_zeroize(&skpv, sizeof(skpv)); mlk_zeroize(&skpv_cache, sizeof(skpv_cache)); @@ -436,7 +446,7 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_poly v, k, epp; mlk_polyvec_mulcache sp_cache; - mlk_unpack_pk(pkpv, seed, pk); + mlk_unpack_pk(&pkpv, seed, pk); mlk_poly_frommsg(&k, m); /* @@ -447,44 +457,47 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], */ MLK_CT_TESTING_DECLASSIFY(seed, MLKEM_SYMBYTES); - mlk_gen_matrix(at, seed, 1 /* transpose */); + mlk_gen_matrix(&at, seed, 1 /* transpose */); #if MLKEM_K == 2 - mlk_poly_getnoise_eta1122_4x(&sp[0], &sp[1], &ep[0], &ep[1], coins, 0, 1, 2, - 3); + mlk_poly_getnoise_eta1122_4x(&sp.vec[0], &sp.vec[1], &ep.vec[0], &ep.vec[1], + coins, 0, 1, 2, 3); mlk_poly_getnoise_eta2(&epp, coins, 4); #elif MLKEM_K == 3 /* * In this call, only the first three output buffers are needed. * The last parameter is a dummy that's overwritten later. */ - mlk_poly_getnoise_eta1_4x(&sp[0], &sp[1], &sp[2], &b[0], coins, 0, 1, 2, - 0xFF); + mlk_poly_getnoise_eta1_4x(&sp.vec[0], &sp.vec[1], &sp.vec[2], &b.vec[0], + coins, 0, 1, 2, 0xFF); /* The fourth output buffer in this call _is_ used. */ - mlk_poly_getnoise_eta2_4x(&ep[0], &ep[1], &ep[2], &epp, coins, 3, 4, 5, 6); + mlk_poly_getnoise_eta2_4x(&ep.vec[0], &ep.vec[1], &ep.vec[2], &epp, coins, 3, + 4, 5, 6); #elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&sp[0], &sp[1], &sp[2], &sp[3], coins, 0, 1, 2, 3); - mlk_poly_getnoise_eta2_4x(&ep[0], &ep[1], &ep[2], &ep[3], coins, 4, 5, 6, 7); + mlk_poly_getnoise_eta1_4x(&sp.vec[0], &sp.vec[1], &sp.vec[2], &sp.vec[3], + coins, 0, 1, 2, 3); + mlk_poly_getnoise_eta2_4x(&ep.vec[0], &ep.vec[1], &ep.vec[2], &ep.vec[3], + coins, 4, 5, 6, 7); mlk_poly_getnoise_eta2(&epp, coins, 8); -#endif +#endif /* MLKEM_K == 4 */ - mlk_polyvec_ntt(sp); + mlk_polyvec_ntt(&sp); - mlk_polyvec_mulcache_compute(sp_cache, sp); - mlk_matvec_mul(b, at, sp, sp_cache); - mlk_polyvec_basemul_acc_montgomery_cached(&v, pkpv, sp, sp_cache); + mlk_polyvec_mulcache_compute(&sp_cache, &sp); + mlk_matvec_mul(&b, &at, &sp, &sp_cache); + mlk_polyvec_basemul_acc_montgomery_cached(&v, &pkpv, &sp, &sp_cache); - mlk_polyvec_invntt_tomont(b); + mlk_polyvec_invntt_tomont(&b); mlk_poly_invntt_tomont(&v); - mlk_polyvec_add(b, ep); + mlk_polyvec_add(&b, &ep); mlk_poly_add(&v, &epp); mlk_poly_add(&v, &k); - mlk_polyvec_reduce(b); + mlk_polyvec_reduce(&b); mlk_poly_reduce(&v); - mlk_pack_ciphertext(c, b, &v); + mlk_pack_ciphertext(c, &b, &v); /* Specification: Partially implements * @[FIPS203, Section 3.3, Destruction of intermediate values] */ @@ -493,7 +506,7 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_zeroize(&sp_cache, sizeof(sp_cache)); mlk_zeroize(&b, sizeof(b)); mlk_zeroize(&v, sizeof(v)); - mlk_zeroize(at, sizeof(at)); + mlk_zeroize(&at, sizeof(at)); mlk_zeroize(&k, sizeof(k)); mlk_zeroize(&ep, sizeof(ep)); mlk_zeroize(&epp, sizeof(epp)); @@ -511,12 +524,12 @@ void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], mlk_poly v, sb; mlk_polyvec_mulcache b_cache; - mlk_unpack_ciphertext(b, &v, c); - mlk_unpack_sk(skpv, sk); + mlk_unpack_ciphertext(&b, &v, c); + mlk_unpack_sk(&skpv, sk); - mlk_polyvec_ntt(b); - mlk_polyvec_mulcache_compute(b_cache, b); - mlk_polyvec_basemul_acc_montgomery_cached(&sb, skpv, b, b_cache); + mlk_polyvec_ntt(&b); + mlk_polyvec_mulcache_compute(&b_cache, &b); + mlk_polyvec_basemul_acc_montgomery_cached(&sb, &skpv, &b, &b_cache); mlk_poly_invntt_tomont(&sb); mlk_poly_sub(&v, &sb); diff --git a/mlkem/src/indcpa.h b/mlkem/src/indcpa.h index 4c44d0d411..dcc2ac7d13 100644 --- a/mlkem/src/indcpa.h +++ b/mlkem/src/indcpa.h @@ -39,15 +39,15 @@ * **************************************************/ 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))) requires(memory_no_alias(seed, MLKEM_SYMBYTES)) requires(transposed == 0 || transposed == 1) assigns(object_whole(a)) - ensures(forall(x, 0, MLKEM_K * MLKEM_K, - array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K, + array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) ); #define mlk_indcpa_keypair_derand MLK_NAMESPACE_K(indcpa_keypair_derand) diff --git a/mlkem/src/kem.c b/mlkem/src/kem.c index 6a49a032ac..b1eee54c9e 100644 --- a/mlkem/src/kem.c +++ b/mlkem/src/kem.c @@ -46,9 +46,9 @@ int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]) mlk_polyvec p; uint8_t p_reencoded[MLKEM_POLYVECBYTES]; - mlk_polyvec_frombytes(p, pk); - mlk_polyvec_reduce(p); - mlk_polyvec_tobytes(p_reencoded, p); + mlk_polyvec_frombytes(&p, pk); + mlk_polyvec_reduce(&p); + mlk_polyvec_tobytes(p_reencoded, &p); /* We use a constant-time memcmp here to avoid having to * declassify the PK before the PCT has succeeded. */ diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c index 15d916b627..f83fa35962 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -47,29 +47,29 @@ * 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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); + 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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); + mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); } /* Reference: `polyvec_tobytes()` in the reference implementation @[REF]. @@ -78,10 +78,10 @@ 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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); + mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); for (i = 0; i < MLKEM_K; i++) __loop__( @@ -89,34 +89,34 @@ void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec a) invariant(i <= MLKEM_K) ) { - mlk_poly_tobytes(&r[i * MLKEM_POLYBYTES], &a[i]); + mlk_poly_tobytes(&r[i * MLKEM_POLYBYTES], &a->vec[i]); } } /* 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, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); + mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); } /* 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, MLKEM_K, MLKEM_N, MLK_NTT_BOUND); + mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLK_NTT_BOUND); } /* Reference: `polyvec_invntt_tomont()` in the reference implementation @[REF]. @@ -125,15 +125,15 @@ 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, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND); + mlk_assert_abs_bound_2d(r->vec, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND); } /* Reference: `polyvec_basemul_acc_montgomery()` in the @@ -148,20 +148,20 @@ void mlk_polyvec_invntt_tomont(mlk_polyvec r) * more modular reductions since it reduces after every modular * multiplication. */ MLK_STATIC_TESTABLE void mlk_polyvec_basemul_acc_montgomery_cached_c( - 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))) assigns(object_whole(r)) ) { unsigned i; - mlk_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); + mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); for (i = 0; i < MLKEM_N / 2; i++) __loop__(invariant(i <= MLKEM_N / 2)) @@ -176,10 +176,10 @@ __contract__( t[1] <= ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) && t[1] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768))) { - t[0] += (int32_t)a[k].coeffs[2 * i + 1] * b_cache[k].coeffs[i]; - t[0] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i]; - t[1] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i + 1]; - t[1] += (int32_t)a[k].coeffs[2 * i + 1] * b[k].coeffs[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]; } r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]); r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]); @@ -188,8 +188,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) { @@ -225,12 +225,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]); } } @@ -242,41 +242,41 @@ 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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); + mlk_assert_bound_2d(r->vec, MLKEM_K, MLKEM_N, 0, MLKEM_Q); } /* Reference: `polyvec_add()` in the reference implementation @[REF]. * - 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++) { - 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, MLKEM_K, MLKEM_N, MLKEM_Q); + 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 db9c856d86..b2e46db33c 100644 --- a/mlkem/src/poly_k.h +++ b/mlkem/src/poly_k.h @@ -29,9 +29,20 @@ #define mlk_polyvec_mulcache MLK_ADD_PARAM_SET(mlk_polyvec_mulcache) /* End of parameter set namespacing */ -typedef mlk_poly mlk_polyvec[MLKEM_K]; -typedef mlk_poly mlk_polymat[MLKEM_K * MLKEM_K]; -typedef mlk_poly_mulcache mlk_polyvec_mulcache[MLKEM_K]; +typedef struct +{ + mlk_poly vec[MLKEM_K]; +} MLK_ALIGN mlk_polyvec; + +typedef struct +{ + mlk_polyvec vec[MLKEM_K]; +} mlk_polymat; + +typedef struct +{ + mlk_poly_mulcache vec[MLKEM_K]; +} mlk_polyvec_mulcache; #define mlk_poly_compress_du MLK_NAMESPACE_K(poly_compress_du) /************************************************* @@ -200,12 +211,12 @@ __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))) requires(forall(k0, 0, MLKEM_K, - array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(a->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) assigns(object_whole(r)) ); @@ -228,14 +239,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(object_whole(r)) 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) @@ -256,12 +267,12 @@ __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)) requires(forall(k0, 0, MLKEM_K, - array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(a->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) assigns(object_whole(r)) ); @@ -284,13 +295,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(object_whole(r)) 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) @@ -313,14 +324,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[j].coeffs, 0, MLKEM_N, MLKEM_Q))) + array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q))) assigns(object_whole(r)) 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) @@ -344,12 +355,12 @@ __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))) assigns(object_whole(r)) 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 \ @@ -380,15 +391,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))) assigns(object_whole(r)) ); @@ -423,7 +434,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))) @@ -453,12 +464,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(object_whole(r)) 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) @@ -485,16 +496,16 @@ __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[j1].coeffs[k1] + b[j1].coeffs[k1] >= INT16_MIN))) + (int32_t)r->vec[j1].coeffs[k1] + b->vec[j1].coeffs[k1] >= INT16_MIN))) assigns(object_whole(r)) ); @@ -514,13 +525,13 @@ __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))) assigns(object_whole(r)) 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/gen_matrix/gen_matrix_harness.c b/proofs/cbmc/gen_matrix/gen_matrix_harness.c index b6005322de..1eb9f2b851 100644 --- a/proofs/cbmc/gen_matrix/gen_matrix_harness.c +++ b/proofs/cbmc/gen_matrix/gen_matrix_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_poly *a; + mlk_polymat *a; uint8_t *seed; int transposed; mlk_gen_matrix(a, seed, transposed); diff --git a/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c b/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c index b6005322de..1eb9f2b851 100644 --- a/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c +++ b/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_poly *a; + mlk_polymat *a; uint8_t *seed; int transposed; mlk_gen_matrix(a, seed, transposed); diff --git a/proofs/cbmc/matvec_mul/matvec_mul_harness.c b/proofs/cbmc/matvec_mul/matvec_mul_harness.c index 286e47e4ba..04b537afaa 100644 --- a/proofs/cbmc/matvec_mul/matvec_mul_harness.c +++ b/proofs/cbmc/matvec_mul/matvec_mul_harness.c @@ -6,12 +6,13 @@ #include "poly_k.h" #define mlk_matvec_mul MLK_NAMESPACE(matvec_mul) -void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a, mlk_polyvec const v, - mlk_polyvec_mulcache const vc); +void mlk_matvec_mul(mlk_polyvec *out, const mlk_polymat *a, + const mlk_polyvec *v, const mlk_polyvec_mulcache *vc); void harness(void) { - mlk_poly *out, *a, *v; - mlk_poly_mulcache *vc; + mlk_polyvec *out, *v; + mlk_polymat *a; + mlk_polyvec_mulcache *vc; mlk_matvec_mul(out, a, v, vc); } diff --git a/proofs/cbmc/polymat_permute_bitrev_to_custom/polymat_permute_bitrev_to_custom_harness.c b/proofs/cbmc/polymat_permute_bitrev_to_custom/polymat_permute_bitrev_to_custom_harness.c index c661b46012..9c78c53957 100644 --- a/proofs/cbmc/polymat_permute_bitrev_to_custom/polymat_permute_bitrev_to_custom_harness.c +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom/polymat_permute_bitrev_to_custom_harness.c @@ -5,10 +5,10 @@ #include #include "poly_k.h" -void mlk_polymat_permute_bitrev_to_custom(mlk_polymat a); +void mlk_polymat_permute_bitrev_to_custom(mlk_polymat *a); void harness(void) { - mlk_poly *a; + mlk_polymat *a; mlk_polymat_permute_bitrev_to_custom(a); } diff --git a/proofs/cbmc/polymat_permute_bitrev_to_custom_native/polymat_permute_bitrev_to_custom_native_harness.c b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/polymat_permute_bitrev_to_custom_native_harness.c index c661b46012..9c78c53957 100644 --- a/proofs/cbmc/polymat_permute_bitrev_to_custom_native/polymat_permute_bitrev_to_custom_native_harness.c +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/polymat_permute_bitrev_to_custom_native_harness.c @@ -5,10 +5,10 @@ #include #include "poly_k.h" -void mlk_polymat_permute_bitrev_to_custom(mlk_polymat a); +void mlk_polymat_permute_bitrev_to_custom(mlk_polymat *a); void harness(void) { - mlk_poly *a; + mlk_polymat *a; mlk_polymat_permute_bitrev_to_custom(a); } 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_c/polyvec_basemul_acc_montgomery_cached_c_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_c/polyvec_basemul_acc_montgomery_cached_c_harness.c index a7fb4d0c0e..c9b806c857 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_c/polyvec_basemul_acc_montgomery_cached_c_harness.c +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_c/polyvec_basemul_acc_montgomery_cached_c_harness.c @@ -7,13 +7,14 @@ #define mlk_polyvec_basemul_acc_montgomery_cached_c \ MLK_ADD_PARAM_SET(mlk_polyvec_basemul_acc_montgomery_cached_c) void mlk_polyvec_basemul_acc_montgomery_cached_c( - 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); void harness(void) { - mlk_poly *r, *a, *b; - mlk_poly_mulcache *b_cache; + mlk_poly *r; + mlk_polyvec *a, *b; + mlk_polyvec_mulcache *b_cache; mlk_polyvec_basemul_acc_montgomery_cached_c(r, a, b, b_cache); } 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_components_mlkem.c b/test/bench_components_mlkem.c index 26858d627c..2802bf3112 100644 --- a/test/bench_components_mlkem.c +++ b/test/bench_components_mlkem.c @@ -147,52 +147,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) diff --git a/test/test_unit.c b/test/test_unit.c index 56ed1bafb7..82a011537b 100644 --- a/test/test_unit.c +++ b/test/test_unit.c @@ -29,8 +29,8 @@ void mlk_poly_invntt_tomont_c(mlk_poly *r); void mlk_poly_tobytes_c(uint8_t r[MLKEM_POLYBYTES], const mlk_poly *a); void mlk_poly_frombytes_c(mlk_poly *r, const uint8_t a[MLKEM_POLYBYTES]); void mlk_polyvec_basemul_acc_montgomery_cached_c( - 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); void mlk_poly_mulcache_compute_c(mlk_poly_mulcache *x, const mlk_poly *a); #define CHECK(x) \ @@ -509,24 +509,24 @@ static int test_polyvec_basemul_core(const int16_t *a, const int16_t *b, /* Copy test data to structures */ for (i = 0; i < MLKEM_K; i++) { - memcpy(test_a[i].coeffs, &a[i * MLKEM_N], MLKEM_N * sizeof(int16_t)); - memcpy(test_b[i].coeffs, &b[i * MLKEM_N], MLKEM_N * sizeof(int16_t)); - memcpy(ref_a[i].coeffs, &a[i * MLKEM_N], MLKEM_N * sizeof(int16_t)); - memcpy(ref_b[i].coeffs, &b[i * MLKEM_N], MLKEM_N * sizeof(int16_t)); + memcpy(test_a.vec[i].coeffs, &a[i * MLKEM_N], MLKEM_N * sizeof(int16_t)); + memcpy(test_b.vec[i].coeffs, &b[i * MLKEM_N], MLKEM_N * sizeof(int16_t)); + memcpy(ref_a.vec[i].coeffs, &a[i * MLKEM_N], MLKEM_N * sizeof(int16_t)); + memcpy(ref_b.vec[i].coeffs, &b[i * MLKEM_N], MLKEM_N * sizeof(int16_t)); #ifdef MLK_USE_NATIVE_NTT_CUSTOM_ORDER - mlk_poly_permute_bitrev_to_custom(test_a[i].coeffs); - mlk_poly_permute_bitrev_to_custom(test_b[i].coeffs); + mlk_poly_permute_bitrev_to_custom(test_a.vec[i].coeffs); + mlk_poly_permute_bitrev_to_custom(test_b.vec[i].coeffs); #endif - mlk_poly_mulcache_compute_c(&ref_cache[i], &ref_b[i]); - mlk_poly_mulcache_compute(&test_cache[i], &test_b[i]); + mlk_poly_mulcache_compute_c(&ref_cache.vec[i], &ref_b.vec[i]); + mlk_poly_mulcache_compute(&test_cache.vec[i], &test_b.vec[i]); } - mlk_polyvec_basemul_acc_montgomery_cached(&test_result, test_a, test_b, - test_cache); - mlk_polyvec_basemul_acc_montgomery_cached_c(&ref_result, ref_a, ref_b, - ref_cache); + mlk_polyvec_basemul_acc_montgomery_cached(&test_result, &test_a, &test_b, + &test_cache); + mlk_polyvec_basemul_acc_montgomery_cached_c(&ref_result, &ref_a, &ref_b, + &ref_cache); #ifdef MLK_USE_NATIVE_NTT_CUSTOM_ORDER mlk_poly_permute_bitrev_to_custom(ref_result.coeffs); From 9561e1eb911fb4732bfba528d4fdb0bf38ad193b Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Wed, 9 Jul 2025 20:47:50 +0100 Subject: [PATCH 02/10] 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 | 134 ++++++++++-------- mlkem/src/indcpa.h | 6 +- mlkem/src/kem.c | 6 +- mlkem/src/poly_k.c | 52 +++---- mlkem/src/poly_k.h | 65 +++++---- proofs/cbmc/gen_matrix/gen_matrix_harness.c | 2 +- .../gen_matrix_serial_harness.c | 2 +- proofs/cbmc/matvec_mul/matvec_mul_harness.c | 10 +- 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_components_mlkem.c | 28 ++-- 21 files changed, 180 insertions(+), 155 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 0b4315e01d..ccfc63e518 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -59,7 +59,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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -83,7 +84,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); @@ -108,7 +109,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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); mlk_polyvec_tobytes(r, sk); @@ -128,7 +130,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); @@ -149,8 +151,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); @@ -170,7 +172,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); @@ -220,7 +222,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; @@ -253,7 +255,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. */ @@ -281,7 +287,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); @@ -314,15 +320,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)))) assigns(object_whole(out))) { unsigned i; @@ -331,7 +338,7 @@ __contract__( assigns(i, object_whole(out)) invariant(i <= MLKEM_K)) { - mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, vc); + mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc); } } @@ -370,47 +377,49 @@ void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], */ MLK_CT_TESTING_DECLASSIFY(publicseed, MLKEM_SYMBYTES); - mlk_gen_matrix(a, publicseed, 0 /* no transpose */); + mlk_gen_matrix(&a, publicseed, 0 /* no transpose */); #if MLKEM_K == 2 - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &e[0], &e[1], noiseseed, 0, 1, - 2, 3); + mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &e.vec[0], &e.vec[1], + noiseseed, 0, 1, 2, 3); #elif MLKEM_K == 3 /* * Only the first three output buffers are needed. * The laster parameter is a dummy that's overwritten later. */ - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], - &pkpv[0] /* irrelevant */, noiseseed, 0, 1, 2, + mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &skpv.vec[2], + &pkpv.vec[0] /* irrelevant */, noiseseed, 0, 1, 2, 0xFF /* irrelevant */); /* Same here */ - mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &pkpv[0] /* irrelevant */, - noiseseed, 3, 4, 5, 0xFF /* irrelevant */); + mlk_poly_getnoise_eta1_4x(&e.vec[0], &e.vec[1], &e.vec[2], + &pkpv.vec[0] /* irrelevant */, noiseseed, 3, 4, 5, + 0xFF /* irrelevant */); #elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], &skpv[3], noiseseed, - 0, 1, 2, 3); - mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &e[3], noiseseed, 4, 5, 6, 7); -#endif + mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &skpv.vec[2], + &skpv.vec[3], noiseseed, 0, 1, 2, 3); + mlk_poly_getnoise_eta1_4x(&e.vec[0], &e.vec[1], &e.vec[2], &e.vec[3], + noiseseed, 4, 5, 6, 7); +#endif /* MLKEM_K == 4 */ - mlk_polyvec_ntt(skpv); - mlk_polyvec_ntt(e); + mlk_polyvec_ntt(&skpv); + mlk_polyvec_ntt(&e); - mlk_polyvec_mulcache_compute(skpv_cache, skpv); - mlk_matvec_mul(pkpv, a, skpv, skpv_cache); - mlk_polyvec_tomont(pkpv); + mlk_polyvec_mulcache_compute(&skpv_cache, &skpv); + mlk_matvec_mul(&pkpv, &a, &skpv, &skpv_cache); + mlk_polyvec_tomont(&pkpv); - mlk_polyvec_add(pkpv, e); - mlk_polyvec_reduce(pkpv); - mlk_polyvec_reduce(skpv); + mlk_polyvec_add(&pkpv, &e); + mlk_polyvec_reduce(&pkpv); + mlk_polyvec_reduce(&skpv); - mlk_pack_sk(sk, skpv); - mlk_pack_pk(pk, pkpv, publicseed); + mlk_pack_sk(sk, &skpv); + mlk_pack_pk(pk, &pkpv, publicseed); /* Specification: Partially implements * @[FIPS203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(buf, sizeof(buf)); mlk_zeroize(coins_with_domain_separator, sizeof(coins_with_domain_separator)); - mlk_zeroize(a, sizeof(a)); + mlk_zeroize(&a, sizeof(a)); mlk_zeroize(&e, sizeof(e)); mlk_zeroize(&skpv, sizeof(skpv)); mlk_zeroize(&skpv_cache, sizeof(skpv_cache)); @@ -436,7 +445,7 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_poly v, k, epp; mlk_polyvec_mulcache sp_cache; - mlk_unpack_pk(pkpv, seed, pk); + mlk_unpack_pk(&pkpv, seed, pk); mlk_poly_frommsg(&k, m); /* @@ -447,44 +456,47 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], */ MLK_CT_TESTING_DECLASSIFY(seed, MLKEM_SYMBYTES); - mlk_gen_matrix(at, seed, 1 /* transpose */); + mlk_gen_matrix(&at, seed, 1 /* transpose */); #if MLKEM_K == 2 - mlk_poly_getnoise_eta1122_4x(&sp[0], &sp[1], &ep[0], &ep[1], coins, 0, 1, 2, - 3); + mlk_poly_getnoise_eta1122_4x(&sp.vec[0], &sp.vec[1], &ep.vec[0], &ep.vec[1], + coins, 0, 1, 2, 3); mlk_poly_getnoise_eta2(&epp, coins, 4); #elif MLKEM_K == 3 /* * In this call, only the first three output buffers are needed. * The last parameter is a dummy that's overwritten later. */ - mlk_poly_getnoise_eta1_4x(&sp[0], &sp[1], &sp[2], &b[0], coins, 0, 1, 2, - 0xFF); + mlk_poly_getnoise_eta1_4x(&sp.vec[0], &sp.vec[1], &sp.vec[2], &b.vec[0], + coins, 0, 1, 2, 0xFF); /* The fourth output buffer in this call _is_ used. */ - mlk_poly_getnoise_eta2_4x(&ep[0], &ep[1], &ep[2], &epp, coins, 3, 4, 5, 6); + mlk_poly_getnoise_eta2_4x(&ep.vec[0], &ep.vec[1], &ep.vec[2], &epp, coins, 3, + 4, 5, 6); #elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&sp[0], &sp[1], &sp[2], &sp[3], coins, 0, 1, 2, 3); - mlk_poly_getnoise_eta2_4x(&ep[0], &ep[1], &ep[2], &ep[3], coins, 4, 5, 6, 7); + mlk_poly_getnoise_eta1_4x(&sp.vec[0], &sp.vec[1], &sp.vec[2], &sp.vec[3], + coins, 0, 1, 2, 3); + mlk_poly_getnoise_eta2_4x(&ep.vec[0], &ep.vec[1], &ep.vec[2], &ep.vec[3], + coins, 4, 5, 6, 7); mlk_poly_getnoise_eta2(&epp, coins, 8); -#endif +#endif /* MLKEM_K == 4 */ - mlk_polyvec_ntt(sp); + mlk_polyvec_ntt(&sp); - mlk_polyvec_mulcache_compute(sp_cache, sp); - mlk_matvec_mul(b, at, sp, sp_cache); - mlk_polyvec_basemul_acc_montgomery_cached(&v, pkpv, sp, sp_cache); + mlk_polyvec_mulcache_compute(&sp_cache, &sp); + mlk_matvec_mul(&b, &at, &sp, &sp_cache); + mlk_polyvec_basemul_acc_montgomery_cached(&v, &pkpv, &sp, &sp_cache); - mlk_polyvec_invntt_tomont(b); + mlk_polyvec_invntt_tomont(&b); mlk_poly_invntt_tomont(&v); - mlk_polyvec_add(b, ep); + mlk_polyvec_add(&b, &ep); mlk_poly_add(&v, &epp); mlk_poly_add(&v, &k); - mlk_polyvec_reduce(b); + mlk_polyvec_reduce(&b); mlk_poly_reduce(&v); - mlk_pack_ciphertext(c, b, &v); + mlk_pack_ciphertext(c, &b, &v); /* Specification: Partially implements * @[FIPS203, Section 3.3, Destruction of intermediate values] */ @@ -493,7 +505,7 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_zeroize(&sp_cache, sizeof(sp_cache)); mlk_zeroize(&b, sizeof(b)); mlk_zeroize(&v, sizeof(v)); - mlk_zeroize(at, sizeof(at)); + mlk_zeroize(&at, sizeof(at)); mlk_zeroize(&k, sizeof(k)); mlk_zeroize(&ep, sizeof(ep)); mlk_zeroize(&epp, sizeof(epp)); @@ -511,12 +523,12 @@ void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], mlk_poly v, sb; mlk_polyvec_mulcache b_cache; - mlk_unpack_ciphertext(b, &v, c); - mlk_unpack_sk(skpv, sk); + mlk_unpack_ciphertext(&b, &v, c); + mlk_unpack_sk(&skpv, sk); - mlk_polyvec_ntt(b); - mlk_polyvec_mulcache_compute(b_cache, b); - mlk_polyvec_basemul_acc_montgomery_cached(&sb, skpv, b, b_cache); + mlk_polyvec_ntt(&b); + mlk_polyvec_mulcache_compute(&b_cache, &b); + mlk_polyvec_basemul_acc_montgomery_cached(&sb, &skpv, &b, &b_cache); mlk_poly_invntt_tomont(&sb); mlk_poly_sub(&v, &sb); diff --git a/mlkem/src/indcpa.h b/mlkem/src/indcpa.h index 4c44d0d411..dcc2ac7d13 100644 --- a/mlkem/src/indcpa.h +++ b/mlkem/src/indcpa.h @@ -39,15 +39,15 @@ * **************************************************/ 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))) requires(memory_no_alias(seed, MLKEM_SYMBYTES)) requires(transposed == 0 || transposed == 1) assigns(object_whole(a)) - ensures(forall(x, 0, MLKEM_K * MLKEM_K, - array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K, + array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) ); #define mlk_indcpa_keypair_derand MLK_NAMESPACE_K(indcpa_keypair_derand) diff --git a/mlkem/src/kem.c b/mlkem/src/kem.c index 6a49a032ac..b1eee54c9e 100644 --- a/mlkem/src/kem.c +++ b/mlkem/src/kem.c @@ -46,9 +46,9 @@ int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]) mlk_polyvec p; uint8_t p_reencoded[MLKEM_POLYVECBYTES]; - mlk_polyvec_frombytes(p, pk); - mlk_polyvec_reduce(p); - mlk_polyvec_tobytes(p_reencoded, p); + mlk_polyvec_frombytes(&p, pk); + mlk_polyvec_reduce(&p); + mlk_polyvec_tobytes(p_reencoded, &p); /* We use a constant-time memcmp here to avoid having to * declassify the PK before the PCT has succeeded. */ diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c index 15d916b627..ecd7d363a5 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -47,26 +47,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, 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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -78,7 +78,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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -89,18 +89,18 @@ void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec a) invariant(i <= MLKEM_K) ) { - mlk_poly_tobytes(&r[i * MLKEM_POLYBYTES], &a[i]); + mlk_poly_tobytes(r + i * MLKEM_POLYBYTES, &a->vec[i]); } } /* 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, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); @@ -108,12 +108,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, MLKEM_K, MLKEM_N, MLK_NTT_BOUND); @@ -125,12 +125,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, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND); @@ -176,10 +176,10 @@ __contract__( t[1] <= ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) && t[1] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768))) { - t[0] += (int32_t)a[k].coeffs[2 * i + 1] * b_cache[k].coeffs[i]; - t[0] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i]; - t[1] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i + 1]; - t[1] += (int32_t)a[k].coeffs[2 * i + 1] * b[k].coeffs[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]; } r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]); r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]); @@ -188,8 +188,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) { @@ -225,12 +225,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]); } } @@ -242,12 +242,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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -257,23 +257,23 @@ 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++) { - 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, MLKEM_K, MLKEM_N, MLKEM_Q); diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h index db9c856d86..b2e46db33c 100644 --- a/mlkem/src/poly_k.h +++ b/mlkem/src/poly_k.h @@ -29,9 +29,20 @@ #define mlk_polyvec_mulcache MLK_ADD_PARAM_SET(mlk_polyvec_mulcache) /* End of parameter set namespacing */ -typedef mlk_poly mlk_polyvec[MLKEM_K]; -typedef mlk_poly mlk_polymat[MLKEM_K * MLKEM_K]; -typedef mlk_poly_mulcache mlk_polyvec_mulcache[MLKEM_K]; +typedef struct +{ + mlk_poly vec[MLKEM_K]; +} MLK_ALIGN mlk_polyvec; + +typedef struct +{ + mlk_polyvec vec[MLKEM_K]; +} mlk_polymat; + +typedef struct +{ + mlk_poly_mulcache vec[MLKEM_K]; +} mlk_polyvec_mulcache; #define mlk_poly_compress_du MLK_NAMESPACE_K(poly_compress_du) /************************************************* @@ -200,12 +211,12 @@ __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))) requires(forall(k0, 0, MLKEM_K, - array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(a->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) assigns(object_whole(r)) ); @@ -228,14 +239,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(object_whole(r)) 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) @@ -256,12 +267,12 @@ __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)) requires(forall(k0, 0, MLKEM_K, - array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(a->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) assigns(object_whole(r)) ); @@ -284,13 +295,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(object_whole(r)) 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) @@ -313,14 +324,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[j].coeffs, 0, MLKEM_N, MLKEM_Q))) + array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q))) assigns(object_whole(r)) 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) @@ -344,12 +355,12 @@ __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))) assigns(object_whole(r)) 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 \ @@ -380,15 +391,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))) assigns(object_whole(r)) ); @@ -423,7 +434,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))) @@ -453,12 +464,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(object_whole(r)) 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) @@ -485,16 +496,16 @@ __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[j1].coeffs[k1] + b[j1].coeffs[k1] >= INT16_MIN))) + (int32_t)r->vec[j1].coeffs[k1] + b->vec[j1].coeffs[k1] >= INT16_MIN))) assigns(object_whole(r)) ); @@ -514,13 +525,13 @@ __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))) assigns(object_whole(r)) 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/gen_matrix/gen_matrix_harness.c b/proofs/cbmc/gen_matrix/gen_matrix_harness.c index b6005322de..1eb9f2b851 100644 --- a/proofs/cbmc/gen_matrix/gen_matrix_harness.c +++ b/proofs/cbmc/gen_matrix/gen_matrix_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_poly *a; + mlk_polymat *a; uint8_t *seed; int transposed; mlk_gen_matrix(a, seed, transposed); diff --git a/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c b/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c index b6005322de..1eb9f2b851 100644 --- a/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c +++ b/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_poly *a; + mlk_polymat *a; uint8_t *seed; int transposed; mlk_gen_matrix(a, seed, transposed); diff --git a/proofs/cbmc/matvec_mul/matvec_mul_harness.c b/proofs/cbmc/matvec_mul/matvec_mul_harness.c index 286e47e4ba..6b7caf94a0 100644 --- a/proofs/cbmc/matvec_mul/matvec_mul_harness.c +++ b/proofs/cbmc/matvec_mul/matvec_mul_harness.c @@ -6,12 +6,14 @@ #include "poly_k.h" #define mlk_matvec_mul MLK_NAMESPACE(matvec_mul) -void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a, mlk_polyvec const v, - mlk_polyvec_mulcache const vc); +void mlk_matvec_mul(mlk_polyvec *out, const mlk_polymat *a, + mlk_polyvec const *v, mlk_polyvec_mulcache const *vc); void harness(void) { - mlk_poly *out, *a, *v; - mlk_poly_mulcache *vc; + mlk_polyvec *out; + mlk_polymat *a; + mlk_polyvec *v; + mlk_polyvec_mulcache *vc; mlk_matvec_mul(out, a, v, vc); } 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_components_mlkem.c b/test/bench_components_mlkem.c index 26858d627c..2802bf3112 100644 --- a/test/bench_components_mlkem.c +++ b/test/bench_components_mlkem.c @@ -147,52 +147,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 dbd46a3afac900d9bc805d753006a1cad3011e3c Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 24 Mar 2025 04:34:20 +0000 Subject: [PATCH 03/10] 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 | 20 +++++++++++++++----- mlkem/src/native/api.h | 4 ++++ mlkem/src/poly.h | 27 +++++++++++++-------------- mlkem/src/poly_k.c | 14 ++++++++------ mlkem/src/poly_k.h | 24 ++++++++++++++++-------- 5 files changed, 56 insertions(+), 33 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index ccfc63e518..b687eed2dc 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -313,9 +313,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)] * @@ -330,13 +332,21 @@ __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(object_whole(out))) + 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, object_whole(out)) - invariant(i <= MLKEM_K)) + 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)))) { 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 20f9654664..6b997992cc 100644 --- a/mlkem/src/native/api.h +++ b/mlkem/src/native/api.h @@ -155,6 +155,7 @@ __contract__( 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)) @@ -264,6 +265,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 */ @@ -298,6 +300,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 */ @@ -332,6 +335,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 c013f99141..2194ec4422 100644 --- a/mlkem/src/poly.h +++ b/mlkem/src/poly.h @@ -61,14 +61,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) */ @@ -149,17 +151,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(object_whole(x)) + 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) @@ -311,6 +309,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 ecd7d363a5..751c7475f5 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -163,18 +163,20 @@ __contract__( unsigned i; mlk_assert_bound_2d(a, 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)) + __loop__( + invariant(i <= MLKEM_N / 2) + invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2))) { 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))) + invariant(k <= MLKEM_K && i <= MLKEM_N / 2) + invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1))) { 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]; diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h index b2e46db33c..ae16ec151f 100644 --- a/mlkem/src/poly_k.h +++ b/mlkem/src/poly_k.h @@ -358,9 +358,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(object_whole(r)) 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 \ @@ -373,7 +375,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 @@ -400,7 +406,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))) - assigns(object_whole(r)) + 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) @@ -428,17 +439,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(object_whole(x)) + 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 1e4a6ce07b24e79ef661c6b82d6af590f30d5c0d Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Mon, 9 Jun 2025 15:04:08 +0100 Subject: [PATCH 04/10] 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 fe70de2d95a038df90ccf0d36c225840ea1b2707 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 09:54:48 +0100 Subject: [PATCH 05/10] Fix merge conflicts and complete rebase again main branch. Signed-off-by: Rod Chapman --- mlkem/src/indcpa.c | 175 +++++++++--------- mlkem/src/indcpa.h | 6 +- mlkem/src/kem.c | 6 +- mlkem/src/poly.c | 1 + mlkem/src/poly_k.c | 57 +++--- mlkem/src/poly_k.h | 79 ++++---- proofs/cbmc/gen_matrix/gen_matrix_harness.c | 2 +- .../gen_matrix_serial_harness.c | 2 +- proofs/cbmc/matvec_mul/matvec_mul_harness.c | 14 +- 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 +- 21 files changed, 188 insertions(+), 184 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index b687eed2dc..701237be4a 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -59,8 +59,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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -84,7 +83,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); @@ -109,8 +108,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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); mlk_polyvec_tobytes(r, sk); @@ -130,7 +128,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); @@ -151,8 +149,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); @@ -172,7 +170,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); @@ -222,7 +220,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; @@ -255,11 +253,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. */ @@ -287,7 +281,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); @@ -322,34 +316,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)))) - { - 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); + // } } /* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF]. @@ -387,49 +395,47 @@ void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES], */ MLK_CT_TESTING_DECLASSIFY(publicseed, MLKEM_SYMBYTES); - mlk_gen_matrix(&a, publicseed, 0 /* no transpose */); + mlk_gen_matrix(a, publicseed, 0 /* no transpose */); #if MLKEM_K == 2 - mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &e.vec[0], &e.vec[1], - noiseseed, 0, 1, 2, 3); + mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &e[0], &e[1], noiseseed, 0, 1, + 2, 3); #elif MLKEM_K == 3 /* * Only the first three output buffers are needed. * The laster parameter is a dummy that's overwritten later. */ - mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &skpv.vec[2], - &pkpv.vec[0] /* irrelevant */, noiseseed, 0, 1, 2, + mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], + &pkpv[0] /* irrelevant */, noiseseed, 0, 1, 2, 0xFF /* irrelevant */); /* Same here */ - mlk_poly_getnoise_eta1_4x(&e.vec[0], &e.vec[1], &e.vec[2], - &pkpv.vec[0] /* irrelevant */, noiseseed, 3, 4, 5, - 0xFF /* irrelevant */); + mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &pkpv[0] /* irrelevant */, + noiseseed, 3, 4, 5, 0xFF /* irrelevant */); #elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&skpv.vec[0], &skpv.vec[1], &skpv.vec[2], - &skpv.vec[3], noiseseed, 0, 1, 2, 3); - mlk_poly_getnoise_eta1_4x(&e.vec[0], &e.vec[1], &e.vec[2], &e.vec[3], - noiseseed, 4, 5, 6, 7); -#endif /* MLKEM_K == 4 */ + mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], &skpv[3], noiseseed, + 0, 1, 2, 3); + mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &e[3], noiseseed, 4, 5, 6, 7); +#endif - mlk_polyvec_ntt(&skpv); - mlk_polyvec_ntt(&e); + mlk_polyvec_ntt(skpv); + mlk_polyvec_ntt(e); - mlk_polyvec_mulcache_compute(&skpv_cache, &skpv); - mlk_matvec_mul(&pkpv, &a, &skpv, &skpv_cache); - mlk_polyvec_tomont(&pkpv); + mlk_polyvec_mulcache_compute(skpv_cache, skpv); + mlk_matvec_mul(pkpv, a, skpv, skpv_cache); + mlk_polyvec_tomont(pkpv); - mlk_polyvec_add(&pkpv, &e); - mlk_polyvec_reduce(&pkpv); - mlk_polyvec_reduce(&skpv); + mlk_polyvec_add(pkpv, e); + mlk_polyvec_reduce(pkpv); + mlk_polyvec_reduce(skpv); - mlk_pack_sk(sk, &skpv); - mlk_pack_pk(pk, &pkpv, publicseed); + mlk_pack_sk(sk, skpv); + mlk_pack_pk(pk, pkpv, publicseed); /* Specification: Partially implements * @[FIPS203, Section 3.3, Destruction of intermediate values] */ mlk_zeroize(buf, sizeof(buf)); mlk_zeroize(coins_with_domain_separator, sizeof(coins_with_domain_separator)); - mlk_zeroize(&a, sizeof(a)); + mlk_zeroize(a, sizeof(a)); mlk_zeroize(&e, sizeof(e)); mlk_zeroize(&skpv, sizeof(skpv)); mlk_zeroize(&skpv_cache, sizeof(skpv_cache)); @@ -455,7 +461,7 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_poly v, k, epp; mlk_polyvec_mulcache sp_cache; - mlk_unpack_pk(&pkpv, seed, pk); + mlk_unpack_pk(pkpv, seed, pk); mlk_poly_frommsg(&k, m); /* @@ -466,47 +472,44 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], */ MLK_CT_TESTING_DECLASSIFY(seed, MLKEM_SYMBYTES); - mlk_gen_matrix(&at, seed, 1 /* transpose */); + mlk_gen_matrix(at, seed, 1 /* transpose */); #if MLKEM_K == 2 - mlk_poly_getnoise_eta1122_4x(&sp.vec[0], &sp.vec[1], &ep.vec[0], &ep.vec[1], - coins, 0, 1, 2, 3); + mlk_poly_getnoise_eta1122_4x(&sp[0], &sp[1], &ep[0], &ep[1], coins, 0, 1, 2, + 3); mlk_poly_getnoise_eta2(&epp, coins, 4); #elif MLKEM_K == 3 /* * In this call, only the first three output buffers are needed. * The last parameter is a dummy that's overwritten later. */ - mlk_poly_getnoise_eta1_4x(&sp.vec[0], &sp.vec[1], &sp.vec[2], &b.vec[0], - coins, 0, 1, 2, 0xFF); + mlk_poly_getnoise_eta1_4x(&sp[0], &sp[1], &sp[2], &b[0], coins, 0, 1, 2, + 0xFF); /* The fourth output buffer in this call _is_ used. */ - mlk_poly_getnoise_eta2_4x(&ep.vec[0], &ep.vec[1], &ep.vec[2], &epp, coins, 3, - 4, 5, 6); + mlk_poly_getnoise_eta2_4x(&ep[0], &ep[1], &ep[2], &epp, coins, 3, 4, 5, 6); #elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&sp.vec[0], &sp.vec[1], &sp.vec[2], &sp.vec[3], - coins, 0, 1, 2, 3); - mlk_poly_getnoise_eta2_4x(&ep.vec[0], &ep.vec[1], &ep.vec[2], &ep.vec[3], - coins, 4, 5, 6, 7); + mlk_poly_getnoise_eta1_4x(&sp[0], &sp[1], &sp[2], &sp[3], coins, 0, 1, 2, 3); + mlk_poly_getnoise_eta2_4x(&ep[0], &ep[1], &ep[2], &ep[3], coins, 4, 5, 6, 7); mlk_poly_getnoise_eta2(&epp, coins, 8); -#endif /* MLKEM_K == 4 */ +#endif - mlk_polyvec_ntt(&sp); + mlk_polyvec_ntt(sp); - mlk_polyvec_mulcache_compute(&sp_cache, &sp); - mlk_matvec_mul(&b, &at, &sp, &sp_cache); - mlk_polyvec_basemul_acc_montgomery_cached(&v, &pkpv, &sp, &sp_cache); + mlk_polyvec_mulcache_compute(sp_cache, sp); + mlk_matvec_mul(b, at, sp, sp_cache); + mlk_polyvec_basemul_acc_montgomery_cached(&v, pkpv, sp, sp_cache); - mlk_polyvec_invntt_tomont(&b); + mlk_polyvec_invntt_tomont(b); mlk_poly_invntt_tomont(&v); - mlk_polyvec_add(&b, &ep); + mlk_polyvec_add(b, ep); mlk_poly_add(&v, &epp); mlk_poly_add(&v, &k); - mlk_polyvec_reduce(&b); + mlk_polyvec_reduce(b); mlk_poly_reduce(&v); - mlk_pack_ciphertext(c, &b, &v); + mlk_pack_ciphertext(c, b, &v); /* Specification: Partially implements * @[FIPS203, Section 3.3, Destruction of intermediate values] */ @@ -515,7 +518,7 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_zeroize(&sp_cache, sizeof(sp_cache)); mlk_zeroize(&b, sizeof(b)); mlk_zeroize(&v, sizeof(v)); - mlk_zeroize(&at, sizeof(at)); + mlk_zeroize(at, sizeof(at)); mlk_zeroize(&k, sizeof(k)); mlk_zeroize(&ep, sizeof(ep)); mlk_zeroize(&epp, sizeof(epp)); @@ -533,12 +536,12 @@ void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], mlk_poly v, sb; mlk_polyvec_mulcache b_cache; - mlk_unpack_ciphertext(&b, &v, c); - mlk_unpack_sk(&skpv, sk); + mlk_unpack_ciphertext(b, &v, c); + mlk_unpack_sk(skpv, sk); - mlk_polyvec_ntt(&b); - mlk_polyvec_mulcache_compute(&b_cache, &b); - mlk_polyvec_basemul_acc_montgomery_cached(&sb, &skpv, &b, &b_cache); + mlk_polyvec_ntt(b); + mlk_polyvec_mulcache_compute(b_cache, b); + mlk_polyvec_basemul_acc_montgomery_cached(&sb, skpv, b, b_cache); mlk_poly_invntt_tomont(&sb); mlk_poly_sub(&v, &sb); diff --git a/mlkem/src/indcpa.h b/mlkem/src/indcpa.h index dcc2ac7d13..4c44d0d411 100644 --- a/mlkem/src/indcpa.h +++ b/mlkem/src/indcpa.h @@ -39,15 +39,15 @@ * **************************************************/ 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))) requires(memory_no_alias(seed, MLKEM_SYMBYTES)) requires(transposed == 0 || transposed == 1) assigns(object_whole(a)) - ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K, - array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) + ensures(forall(x, 0, MLKEM_K * MLKEM_K, + array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); #define mlk_indcpa_keypair_derand MLK_NAMESPACE_K(indcpa_keypair_derand) diff --git a/mlkem/src/kem.c b/mlkem/src/kem.c index b1eee54c9e..6a49a032ac 100644 --- a/mlkem/src/kem.c +++ b/mlkem/src/kem.c @@ -46,9 +46,9 @@ int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]) mlk_polyvec p; uint8_t p_reencoded[MLKEM_POLYVECBYTES]; - mlk_polyvec_frombytes(&p, pk); - mlk_polyvec_reduce(&p); - mlk_polyvec_tobytes(p_reencoded, &p); + mlk_polyvec_frombytes(p, pk); + mlk_polyvec_reduce(p); + mlk_polyvec_tobytes(p_reencoded, p); /* We use a constant-time memcmp here to avoid having to * declassify the PK before the PCT has succeeded. */ diff --git a/mlkem/src/poly.c b/mlkem/src/poly.c index 858b744820..e61414d841 100644 --- a/mlkem/src/poly.c +++ b/mlkem/src/poly.c @@ -277,6 +277,7 @@ __contract__( requires(memory_no_alias(x, sizeof(mlk_poly_mulcache))) requires(memory_no_alias(a, sizeof(mlk_poly))) assigns(object_whole(x)) + 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 751c7475f5..c713c99393 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -47,26 +47,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, 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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -78,7 +78,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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -89,18 +89,18 @@ void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a) invariant(i <= MLKEM_K) ) { - mlk_poly_tobytes(r + i * MLKEM_POLYBYTES, &a->vec[i]); + mlk_poly_tobytes(&r[i * MLKEM_POLYBYTES], &a[i]); } } /* 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, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); @@ -108,12 +108,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, MLKEM_K, MLKEM_N, MLK_NTT_BOUND); @@ -125,12 +125,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, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND); @@ -157,7 +157,12 @@ __contract__( 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))) + 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(object_whole(r)) + ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2)) ) { unsigned i; @@ -178,10 +183,10 @@ __contract__( invariant(k <= MLKEM_K && i <= MLKEM_N / 2) invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1))) { - 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]; + t[0] += (int32_t)a[k].coeffs[2 * i + 1] * b_cache[k].coeffs[i]; + t[0] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i]; + t[1] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i + 1]; + t[1] += (int32_t)a[k].coeffs[2 * i + 1] * b[k].coeffs[2 * i]; } r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]); r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]); @@ -190,8 +195,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, MLKEM_K, MLKEM_N, 0, MLKEM_Q); @@ -259,23 +264,23 @@ 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++) { - 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, MLKEM_K, MLKEM_N, MLKEM_Q); diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h index ae16ec151f..34997a65d1 100644 --- a/mlkem/src/poly_k.h +++ b/mlkem/src/poly_k.h @@ -29,20 +29,9 @@ #define mlk_polyvec_mulcache MLK_ADD_PARAM_SET(mlk_polyvec_mulcache) /* End of parameter set namespacing */ -typedef struct -{ - mlk_poly vec[MLKEM_K]; -} MLK_ALIGN mlk_polyvec; - -typedef struct -{ - mlk_polyvec vec[MLKEM_K]; -} mlk_polymat; - -typedef struct -{ - mlk_poly_mulcache vec[MLKEM_K]; -} mlk_polyvec_mulcache; +typedef mlk_poly mlk_polyvec[MLKEM_K]; +typedef mlk_poly mlk_polymat[MLKEM_K * MLKEM_K]; +typedef mlk_poly_mulcache mlk_polyvec_mulcache[MLKEM_K]; #define mlk_poly_compress_du MLK_NAMESPACE_K(poly_compress_du) /************************************************* @@ -211,12 +200,12 @@ __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))) requires(forall(k0, 0, MLKEM_K, - array_bound(a->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) assigns(object_whole(r)) ); @@ -239,14 +228,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(object_whole(r)) 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) @@ -267,12 +256,12 @@ __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)) requires(forall(k0, 0, MLKEM_K, - array_bound(a->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) + array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) assigns(object_whole(r)) ); @@ -295,13 +284,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(object_whole(r)) 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) @@ -324,14 +313,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))) + array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLKEM_Q))) assigns(object_whole(r)) 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) @@ -355,14 +344,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))) + array_abs_bound(r[k0].coeffs, 0, MLKEM_N, INT16_MAX/2))) assigns(object_whole(r)) 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 \ @@ -397,23 +386,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 @@ -439,14 +429,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(object_whole(x)) 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) @@ -472,12 +467,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(object_whole(r)) 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) @@ -504,16 +499,16 @@ __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))) + (int32_t)r[j1].coeffs[k1] + b[j1].coeffs[k1] >= INT16_MIN))) assigns(object_whole(r)) ); @@ -533,13 +528,13 @@ __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))) assigns(object_whole(r)) 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/gen_matrix/gen_matrix_harness.c b/proofs/cbmc/gen_matrix/gen_matrix_harness.c index 1eb9f2b851..b6005322de 100644 --- a/proofs/cbmc/gen_matrix/gen_matrix_harness.c +++ b/proofs/cbmc/gen_matrix/gen_matrix_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_polymat *a; + mlk_poly *a; uint8_t *seed; int transposed; mlk_gen_matrix(a, seed, transposed); diff --git a/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c b/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c index 1eb9f2b851..b6005322de 100644 --- a/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c +++ b/proofs/cbmc/gen_matrix_serial/gen_matrix_serial_harness.c @@ -7,7 +7,7 @@ void harness(void) { - mlk_polymat *a; + mlk_poly *a; uint8_t *seed; int transposed; mlk_gen_matrix(a, seed, transposed); diff --git a/proofs/cbmc/matvec_mul/matvec_mul_harness.c b/proofs/cbmc/matvec_mul/matvec_mul_harness.c index 6b7caf94a0..2353a403ff 100644 --- a/proofs/cbmc/matvec_mul/matvec_mul_harness.c +++ b/proofs/cbmc/matvec_mul/matvec_mul_harness.c @@ -5,15 +5,15 @@ #include "indcpa.h" #include "poly_k.h" -#define mlk_matvec_mul MLK_NAMESPACE(matvec_mul) -void mlk_matvec_mul(mlk_polyvec *out, const mlk_polymat *a, - mlk_polyvec const *v, mlk_polyvec_mulcache const *vc); +#define mlk_matvec_mul MLK_ADD_PARAM_SET(mlk_matvec_mul) +void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a, const mlk_polyvec v, + const mlk_polyvec_mulcache vc); void harness(void) { - mlk_polyvec *out; - mlk_polymat *a; - mlk_polyvec *v; - mlk_polyvec_mulcache *vc; + mlk_poly *out; + mlk_poly *a; + mlk_poly *v; + mlk_poly_mulcache *vc; mlk_matvec_mul(out, a, v, vc); } 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 d3d1e9cc4560796d51ec8b711348187074e2bc13 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:21:24 +0100 Subject: [PATCH 06/10] 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 701237be4a..c016fac52b 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -347,17 +347,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); + * } + */ } /* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF]. From 695acb03cea2f8eb4bad47b6874f786e4d227b4c Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:36:30 +0100 Subject: [PATCH 07/10] Update component testing code for new type signatures. Signed-off-by: Rod Chapman --- test/bench_components_mlkem.c | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/test/bench_components_mlkem.c b/test/bench_components_mlkem.c index 2802bf3112..55791078cf 100644 --- a/test/bench_components_mlkem.c +++ b/test/bench_components_mlkem.c @@ -71,7 +71,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 */ @@ -147,52 +147,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 ec4fd6d7d001c08b7d77170cdb0f752da4707f4d Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:58:10 +0100 Subject: [PATCH 08/10] Re-generate auto-generated files to meet lint requirements. Signed-off-by: Rod Chapman --- test/bench_components_mlkem.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/bench_components_mlkem.c b/test/bench_components_mlkem.c index 55791078cf..26858d627c 100644 --- a/test/bench_components_mlkem.c +++ b/test/bench_components_mlkem.c @@ -71,7 +71,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 2a8542fd0e560218ae8ede07f89a6632e7ea537c Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 11:19:45 +0100 Subject: [PATCH 09/10] 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 e0978c122a..6f74428ba7 100644 --- a/mlkem/src/native/aarch64/src/arith_native_aarch64.h +++ b/mlkem/src/native/aarch64/src/arith_native_aarch64.h @@ -116,6 +116,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/arm/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)) @@ -123,6 +126,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 \ @@ -133,6 +137,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/arm/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)) @@ -140,6 +147,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 \ @@ -150,6 +158,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/arm/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)) @@ -157,6 +168,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 44ba0459cff79709ec19a4f21afecd48a596c923 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 11:41:15 +0100 Subject: [PATCH 10/10] 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 6faf533d49..21f00f0054 100644 --- a/dev/aarch64_clean/src/arith_native_aarch64.h +++ b/dev/aarch64_clean/src/arith_native_aarch64.h @@ -117,6 +117,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/arm/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)) @@ -124,6 +127,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 \ @@ -134,6 +138,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/arm/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)) @@ -141,6 +148,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 \ @@ -151,6 +159,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/arm/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)) @@ -158,6 +169,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 35399c8c10..b832730d4e 100644 --- a/dev/aarch64_opt/src/arith_native_aarch64.h +++ b/dev/aarch64_opt/src/arith_native_aarch64.h @@ -116,6 +116,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/arm/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)) @@ -123,6 +126,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 \ @@ -133,6 +137,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/arm/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)) @@ -140,6 +147,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 \ @@ -150,6 +158,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/arm/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)) @@ -157,6 +168,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)