From 740548f130195f7cc763df6d3283ef38c336454a Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Wed, 9 Jul 2025 20:47:50 +0100 Subject: [PATCH 1/9] 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 | 52 +++---- 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, 182 insertions(+), 156 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 6dd35ee29..5f436f557 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -57,7 +57,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); @@ -81,7 +82,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); @@ -106,7 +107,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); @@ -126,7 +128,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); @@ -147,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], 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); @@ -168,7 +170,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); @@ -199,7 +201,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; @@ -236,7 +238,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. */ @@ -257,7 +263,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++; } @@ -269,7 +275,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 @@ -294,15 +301,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; @@ -311,7 +319,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); } } @@ -350,47 +358,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)); @@ -416,7 +426,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); /* @@ -427,44 +437,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] */ @@ -473,7 +486,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)); @@ -491,12 +504,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 6a49a032a..b1eee54c9 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 15d916b62..ecd7d363a 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 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 e7263c90234a61624eb28cace2a38f1b7a3bfc5a Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 24 Mar 2025 04:34:20 +0000 Subject: [PATCH 2/9] 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 5f436f557..54ac6e2c4 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -294,9 +294,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)] * @@ -311,13 +313,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 20f965466..6b997992c 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 815564eb1..fa7172b49 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 ecd7d363a..751c7475f 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 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 cf1eadc923fffc8fc89d7e9f2d211a1db8b8f993 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Mon, 9 Jun 2025 15:04:08 +0100 Subject: [PATCH 3/9] 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 65fc7e878..bdc703c31 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 0c5e0e8b79dd29cc787888530348adf040f999a3 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 09:54:48 +0100 Subject: [PATCH 4/9] Fix merge conflicts and complete rebase again main branch. Signed-off-by: Rod Chapman --- mlkem/src/indcpa.c | 178 +++++++++--------- 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_native_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, 189 insertions(+), 186 deletions(-) diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 54ac6e2c4..0f7890dba 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -57,8 +57,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); @@ -82,7 +81,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); @@ -107,8 +106,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); @@ -128,7 +126,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); @@ -149,8 +147,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); @@ -170,7 +168,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); @@ -201,7 +199,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,11 +236,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); } /* For MLKEM_K == 3, sample the last entry individually. */ @@ -263,7 +257,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]); i++; } @@ -275,8 +269,7 @@ 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->vec[i / MLKEM_K].vec[i % MLKEM_K].coeffs); + mlk_poly_permute_bitrev_to_custom(a[i].coeffs); } /* Specification: Partially implements @@ -303,34 +296,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]. @@ -368,49 +375,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)); @@ -436,7 +441,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,47 +452,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] */ @@ -496,7 +498,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)); @@ -514,12 +516,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 dcc2ac7d1..4c44d0d41 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 b1eee54c9..6a49a032a 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 970d3e5a7..d185f603d 100644 --- a/mlkem/src/poly.c +++ b/mlkem/src/poly.c @@ -273,6 +273,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 751c7475f..c713c9939 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 d19c1c133..3668a22d9 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 1eb9f2b85..b6005322d 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_native/gen_matrix_native_harness.c b/proofs/cbmc/gen_matrix_native/gen_matrix_native_harness.c index 1eb9f2b85..b6005322d 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_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 6b7caf94a..2353a403f 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 5923c177f..4a6cdeca9 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 0f8d7355b..869e07842 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 0f8d7355b..869e07842 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 5fd0899be..5b7df4dd1 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 9b2dbc6da..853d55504 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 9a200adf6..02e9d3d57 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 e8bf6e654..b86aff4f7 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 b560a5270..53d417840 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 03690ecc0..3c4d15c5f 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 26b38a363..a3d0fb4d8 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 16616aa1a..9ccb5961a 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 72ee9743b..9561889df 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 d6598e53a7a2d0ab466a6da39b3ddf9e5a042431 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:21:24 +0100 Subject: [PATCH 5/9] 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 0f7890dba..9503725c2 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -327,17 +327,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 73208d88902fbfc776c230d9efeb1d2ba5ee9c46 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:36:30 +0100 Subject: [PATCH 6/9] 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 2802bf311..55791078c 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 78fae004af0f127f85668b69774808cb31d412e9 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 10:58:10 +0100 Subject: [PATCH 7/9] 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 55791078c..26858d627 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 26702ea4b74d873bba10b5ae74053e2c10a29849 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 11:19:45 +0100 Subject: [PATCH 8/9] 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 e0978c122..6f74428ba 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 dca2a1fdd8f1c245d7038630e8d5cd7b58a7be9a Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 7 Oct 2025 11:41:15 +0100 Subject: [PATCH 9/9] 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 6faf533d4..21f00f005 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 35399c8c1..b832730d4 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)