From d83012deb12fe67dfd69a3e29f9bc7e374fef36f Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Wed, 9 Jul 2025 20:47:50 +0100 Subject: [PATCH 1/3] 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 | 137 ++++++++++-------- mlkem/src/indcpa.h | 6 +- mlkem/src/kem.c | 6 +- mlkem/src/poly_k.c | 56 +++---- mlkem/src/poly_k.h | 65 +++++---- proofs/cbmc/gen_matrix/gen_matrix_harness.c | 2 +- .../gen_matrix_native_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, 184 insertions(+), 158 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 556f7692e..dd38be82a 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); @@ -201,7 +203,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; @@ -238,7 +240,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); } /* For MLKEM_K == 3, sample the last entry individually. */ @@ -259,7 +265,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]); i++; } @@ -271,7 +277,8 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES], */ for (i = 0; i < MLKEM_K * MLKEM_K; i++) { - 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); } /* Specification: Partially implements @@ -296,15 +303,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; @@ -313,7 +321,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); } } @@ -352,47 +360,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)); @@ -418,7 +428,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); /* @@ -429,44 +439,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] */ @@ -475,7 +488,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)); @@ -493,12 +506,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 4c44d0d41..dcc2ac7d1 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 65099d847..1325d3932 100644 --- a/mlkem/src/kem.c +++ b/mlkem/src/kem.c @@ -58,9 +58,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 f86b13417..33bdedb7e 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -46,26 +46,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); @@ -77,25 +77,25 @@ 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); for (i = 0; i < MLKEM_K; i++) { - 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); @@ -103,12 +103,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); @@ -120,12 +120,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); @@ -145,8 +145,8 @@ void mlk_polyvec_invntt_tomont(mlk_polyvec r) * multiplication. */ 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) { unsigned i; mlk_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); @@ -163,10 +163,10 @@ void mlk_polyvec_basemul_acc_montgomery_cached( 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]); @@ -176,8 +176,8 @@ void mlk_polyvec_basemul_acc_montgomery_cached( #else /* !MLK_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */ 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) { mlk_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT); /* Omitting bounds assertion for cache since native implementations may @@ -204,12 +204,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]); } } @@ -221,12 +221,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); @@ -236,23 +236,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 f7a40ff5f..9a230d9d3 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 b6005322d..1eb9f2b85 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_native/gen_matrix_native_harness.c b/proofs/cbmc/gen_matrix_native/gen_matrix_native_harness.c index b6005322d..1eb9f2b85 100644 --- a/proofs/cbmc/gen_matrix_native/gen_matrix_native_harness.c +++ b/proofs/cbmc/gen_matrix_native/gen_matrix_native_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 286e47e4b..6b7caf94a 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 4a6cdeca9..5923c177f 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 869e07842..0f8d7355b 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 869e07842..0f8d7355b 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 5b7df4dd1..5fd0899be 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 853d55504..9b2dbc6da 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 02e9d3d57..9a200adf6 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 b86aff4f7..e8bf6e654 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 53d417840..b560a5270 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 3c4d15c5f..03690ecc0 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 a3d0fb4d8..26b38a363 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 9ccb5961a..16616aa1a 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 9561889df..72ee9743b 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 26858d627..2802bf311 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 08888cd0aca5b71206e0a937c46e8e962d2b128b Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 24 Mar 2025 04:34:20 +0000 Subject: [PATCH 2/3] 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 | 13 +++++++------ mlkem/src/poly_k.h | 24 ++++++++++++++++-------- 5 files changed, 55 insertions(+), 33 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index dd38be82a..aee8d08c5 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -296,9 +296,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)] * @@ -313,13 +315,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 aea28a3af..6494cb6db 100644 --- a/mlkem/src/native/api.h +++ b/mlkem/src/native/api.h @@ -143,6 +143,7 @@ __contract__( static MLK_INLINE void 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(array_abs_bound(p, 0, MLKEM_N, MLK_INVNTT_BOUND)) ); @@ -244,6 +245,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2))) requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 2 */ @@ -277,6 +279,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2))) requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2)) ); #endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 3 */ @@ -310,6 +313,7 @@ __contract__( requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2))) requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT)) assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + 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 20fb65e72..42ec24b6c 100644 --- a/mlkem/src/poly.h +++ b/mlkem/src/poly.h @@ -89,14 +89,16 @@ static MLK_ALWAYS_INLINE int16_t mlk_cast_uint16_to_int16(uint16_t x) **************************************************/ 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) */ @@ -177,17 +179,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) @@ -339,6 +337,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 33bdedb7e..ccd75fcbe 100644 --- a/mlkem/src/poly_k.c +++ b/mlkem/src/poly_k.c @@ -150,18 +150,19 @@ void mlk_polyvec_basemul_acc_montgomery_cached( { 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 9a230d9d3..d19c1c133 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 a86fbc47ff5d6af30f75a9d80e2197523859df54 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Mon, 9 Jun 2025 15:04:08 +0100 Subject: [PATCH 3/3] 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 65223be1c..7a0b8dd37 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