From c3e44f0b263cbef7d0c778be848ae3de4ae31fb5 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 20 Jan 2025 19:31:57 +0000 Subject: [PATCH 1/2] Introduce separate CUs for arithmetic, compression, sampling This commit merges `cbd.*` and `rej_uniform.*` into `sampling.*`. It also moves `ntt.*` and `reduce.h` into `poly.*`. Finally, compression-related routines are moved into newly created `compress.*`. Signed-off-by: Hanno Becker --- .../bring_your_own_fips202/mlkem_native/cbd.c | 1 - .../bring_your_own_fips202/mlkem_native/cbd.h | 1 - .../mlkem_native/compress.c | 1 + .../mlkem_native/compress.h | 1 + .../bring_your_own_fips202/mlkem_native/ntt.c | 1 - .../bring_your_own_fips202/mlkem_native/ntt.h | 1 - .../mlkem_native/reduce.h | 1 - .../mlkem_native/rej_uniform.c | 1 - .../mlkem_native/rej_uniform.h | 1 - .../mlkem_native/sampling.c | 1 + .../mlkem_native/sampling.h | 1 + .../custom_backend/mlkem_native/mlkem/cbd.c | 1 - .../custom_backend/mlkem_native/mlkem/cbd.h | 1 - .../mlkem_native/mlkem/compress.c | 1 + .../mlkem_native/mlkem/compress.h | 1 + .../custom_backend/mlkem_native/mlkem/ntt.c | 1 - .../custom_backend/mlkem_native/mlkem/ntt.h | 1 - .../mlkem_native/mlkem/reduce.h | 1 - .../mlkem_native/mlkem/rej_uniform.c | 1 - .../mlkem_native/mlkem/rej_uniform.h | 1 - .../mlkem_native/mlkem/sampling.c | 1 + .../mlkem_native/mlkem/sampling.h | 1 + .../monolithic_build/mlkem_native_monobuild.c | 404 +++++---- mlkem/cbd.c | 120 --- mlkem/cbd.h | 43 - mlkem/compress.c | 395 +++++++++ mlkem/compress.h | 495 +++++++++++ mlkem/indcpa.c | 3 +- mlkem/ntt.c | 266 ------ mlkem/ntt.h | 102 --- mlkem/params.h | 1 + mlkem/poly.c | 809 ++++++++++-------- mlkem/poly.h | 571 ++---------- mlkem/polyvec.c | 5 +- mlkem/polyvec.h | 1 + mlkem/reduce.h | 209 ----- mlkem/{rej_uniform.c => sampling.c} | 112 ++- mlkem/{rej_uniform.h => sampling.h} | 37 +- mlkem/zetas.c | 2 +- proofs/cbmc/barrett_reduce/Makefile | 2 +- .../barrett_reduce/barrett_reduce_harness.c | 6 +- proofs/cbmc/basemul_cached/Makefile | 2 +- .../basemul_cached/basemul_cached_harness.c | 7 +- proofs/cbmc/fqmul/fqmul_harness.c | 6 +- proofs/cbmc/invntt_layer/Makefile | 2 +- .../montgomery_reduce_harness.c | 6 +- proofs/cbmc/ntt_butterfly_block/Makefile | 2 +- proofs/cbmc/ntt_layer/Makefile | 2 +- proofs/cbmc/poly_cbd_eta1/Makefile | 2 +- proofs/cbmc/poly_cbd_eta2/Makefile | 2 +- proofs/cbmc/poly_compress_du/Makefile | 2 +- proofs/cbmc/poly_compress_dv/Makefile | 2 +- proofs/cbmc/poly_decompress_du/Makefile | 2 +- proofs/cbmc/poly_decompress_dv/Makefile | 2 +- proofs/cbmc/poly_frombytes/Makefile | 2 +- .../poly_frombytes/poly_frombytes_harness.c | 2 +- proofs/cbmc/poly_frommsg/Makefile | 2 +- .../cbmc/poly_frommsg/poly_frommsg_harness.c | 2 +- proofs/cbmc/poly_invntt_tomont/Makefile | 2 +- .../poly_invntt_tomont_harness.c | 2 +- proofs/cbmc/poly_mulcache_compute/Makefile | 2 +- .../poly_mulcache_compute_harness.c | 1 - proofs/cbmc/poly_ntt/Makefile | 2 +- proofs/cbmc/poly_ntt/poly_ntt_harness.c | 2 +- proofs/cbmc/poly_rej_uniform/Makefile | 2 +- .../poly_rej_uniform_harness.c | 2 +- proofs/cbmc/poly_rej_uniform_x4/Makefile | 2 +- .../poly_rej_uniform_x4_harness.c | 2 +- proofs/cbmc/poly_tobytes/Makefile | 2 +- .../cbmc/poly_tobytes/poly_tobytes_harness.c | 2 +- proofs/cbmc/poly_tomsg/Makefile | 2 +- proofs/cbmc/poly_tomsg/poly_tomsg_harness.c | 2 +- proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c | 1 - proofs/cbmc/rej_uniform/Makefile | 2 +- proofs/cbmc/rej_uniform_scalar/Makefile | 2 +- .../rej_uniform_scalar_harness.c | 3 +- .../scalar_compress_d1_harness.c | 2 +- .../scalar_compress_d10_harness.c | 2 +- .../scalar_compress_d11_harness.c | 2 +- .../scalar_compress_d4_harness.c | 2 +- .../scalar_compress_d5_harness.c | 2 +- .../scalar_decompress_d10_harness.c | 2 +- .../scalar_decompress_d11_harness.c | 2 +- .../scalar_decompress_d4_harness.c | 2 +- .../scalar_decompress_d5_harness.c | 2 +- .../scalar_signed_to_unsigned_q_harness.c | 6 +- scripts/autogen | 2 +- 87 files changed, 1823 insertions(+), 1890 deletions(-) delete mode 120000 examples/bring_your_own_fips202/mlkem_native/cbd.c delete mode 120000 examples/bring_your_own_fips202/mlkem_native/cbd.h create mode 120000 examples/bring_your_own_fips202/mlkem_native/compress.c create mode 120000 examples/bring_your_own_fips202/mlkem_native/compress.h delete mode 120000 examples/bring_your_own_fips202/mlkem_native/ntt.c delete mode 120000 examples/bring_your_own_fips202/mlkem_native/ntt.h delete mode 120000 examples/bring_your_own_fips202/mlkem_native/reduce.h delete mode 120000 examples/bring_your_own_fips202/mlkem_native/rej_uniform.c delete mode 120000 examples/bring_your_own_fips202/mlkem_native/rej_uniform.h create mode 120000 examples/bring_your_own_fips202/mlkem_native/sampling.c create mode 120000 examples/bring_your_own_fips202/mlkem_native/sampling.h delete mode 120000 examples/custom_backend/mlkem_native/mlkem/cbd.c delete mode 120000 examples/custom_backend/mlkem_native/mlkem/cbd.h create mode 120000 examples/custom_backend/mlkem_native/mlkem/compress.c create mode 120000 examples/custom_backend/mlkem_native/mlkem/compress.h delete mode 120000 examples/custom_backend/mlkem_native/mlkem/ntt.c delete mode 120000 examples/custom_backend/mlkem_native/mlkem/ntt.h delete mode 120000 examples/custom_backend/mlkem_native/mlkem/reduce.h delete mode 120000 examples/custom_backend/mlkem_native/mlkem/rej_uniform.c delete mode 120000 examples/custom_backend/mlkem_native/mlkem/rej_uniform.h create mode 120000 examples/custom_backend/mlkem_native/mlkem/sampling.c create mode 120000 examples/custom_backend/mlkem_native/mlkem/sampling.h delete mode 100644 mlkem/cbd.c delete mode 100644 mlkem/cbd.h create mode 100644 mlkem/compress.c create mode 100644 mlkem/compress.h delete mode 100644 mlkem/ntt.c delete mode 100644 mlkem/ntt.h delete mode 100644 mlkem/reduce.h rename mlkem/{rej_uniform.c => sampling.c} (73%) rename mlkem/{rej_uniform.h => sampling.h} (63%) diff --git a/examples/bring_your_own_fips202/mlkem_native/cbd.c b/examples/bring_your_own_fips202/mlkem_native/cbd.c deleted file mode 120000 index 4eddab21c..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/cbd.c +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/cbd.c \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/cbd.h b/examples/bring_your_own_fips202/mlkem_native/cbd.h deleted file mode 120000 index 02d999ea6..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/cbd.h +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/cbd.h \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/compress.c b/examples/bring_your_own_fips202/mlkem_native/compress.c new file mode 120000 index 000000000..d705a51b2 --- /dev/null +++ b/examples/bring_your_own_fips202/mlkem_native/compress.c @@ -0,0 +1 @@ +../../../mlkem/compress.c \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/compress.h b/examples/bring_your_own_fips202/mlkem_native/compress.h new file mode 120000 index 000000000..3c760c645 --- /dev/null +++ b/examples/bring_your_own_fips202/mlkem_native/compress.h @@ -0,0 +1 @@ +../../../mlkem/compress.h \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/ntt.c b/examples/bring_your_own_fips202/mlkem_native/ntt.c deleted file mode 120000 index 957883d8b..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/ntt.c +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/ntt.c \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/ntt.h b/examples/bring_your_own_fips202/mlkem_native/ntt.h deleted file mode 120000 index 4fa1e50b9..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/ntt.h +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/ntt.h \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/reduce.h b/examples/bring_your_own_fips202/mlkem_native/reduce.h deleted file mode 120000 index f543b43a2..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/reduce.h +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/reduce.h \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/rej_uniform.c b/examples/bring_your_own_fips202/mlkem_native/rej_uniform.c deleted file mode 120000 index fb0ee1f67..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/rej_uniform.c +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/rej_uniform.c \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/rej_uniform.h b/examples/bring_your_own_fips202/mlkem_native/rej_uniform.h deleted file mode 120000 index 490f38487..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/rej_uniform.h +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/rej_uniform.h \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/sampling.c b/examples/bring_your_own_fips202/mlkem_native/sampling.c new file mode 120000 index 000000000..6474d64d5 --- /dev/null +++ b/examples/bring_your_own_fips202/mlkem_native/sampling.c @@ -0,0 +1 @@ +../../../mlkem/sampling.c \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/sampling.h b/examples/bring_your_own_fips202/mlkem_native/sampling.h new file mode 120000 index 000000000..64ec6be90 --- /dev/null +++ b/examples/bring_your_own_fips202/mlkem_native/sampling.h @@ -0,0 +1 @@ +../../../mlkem/sampling.h \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/cbd.c b/examples/custom_backend/mlkem_native/mlkem/cbd.c deleted file mode 120000 index 66131480c..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/cbd.c +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/cbd.c \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/cbd.h b/examples/custom_backend/mlkem_native/mlkem/cbd.h deleted file mode 120000 index 941b8bd44..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/cbd.h +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/cbd.h \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/compress.c b/examples/custom_backend/mlkem_native/mlkem/compress.c new file mode 120000 index 000000000..cd6877708 --- /dev/null +++ b/examples/custom_backend/mlkem_native/mlkem/compress.c @@ -0,0 +1 @@ +../../../../mlkem/compress.c \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/compress.h b/examples/custom_backend/mlkem_native/mlkem/compress.h new file mode 120000 index 000000000..8aa09d3db --- /dev/null +++ b/examples/custom_backend/mlkem_native/mlkem/compress.h @@ -0,0 +1 @@ +../../../../mlkem/compress.h \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/ntt.c b/examples/custom_backend/mlkem_native/mlkem/ntt.c deleted file mode 120000 index 693bc94f2..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/ntt.c +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/ntt.c \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/ntt.h b/examples/custom_backend/mlkem_native/mlkem/ntt.h deleted file mode 120000 index 5ea1982c5..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/ntt.h +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/ntt.h \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/reduce.h b/examples/custom_backend/mlkem_native/mlkem/reduce.h deleted file mode 120000 index 6b2408820..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/reduce.h +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/reduce.h \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/rej_uniform.c b/examples/custom_backend/mlkem_native/mlkem/rej_uniform.c deleted file mode 120000 index bcc45b521..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/rej_uniform.c +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/rej_uniform.c \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/rej_uniform.h b/examples/custom_backend/mlkem_native/mlkem/rej_uniform.h deleted file mode 120000 index 1d2f26cdb..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/rej_uniform.h +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/rej_uniform.h \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/sampling.c b/examples/custom_backend/mlkem_native/mlkem/sampling.c new file mode 120000 index 000000000..6eb8bb8ae --- /dev/null +++ b/examples/custom_backend/mlkem_native/mlkem/sampling.c @@ -0,0 +1 @@ +../../../../mlkem/sampling.c \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/sampling.h b/examples/custom_backend/mlkem_native/mlkem/sampling.h new file mode 120000 index 000000000..5eab5ee26 --- /dev/null +++ b/examples/custom_backend/mlkem_native/mlkem/sampling.h @@ -0,0 +1 @@ +../../../../mlkem/sampling.h \ No newline at end of file diff --git a/examples/monolithic_build/mlkem_native_monobuild.c b/examples/monolithic_build/mlkem_native_monobuild.c index 56766331e..35fd29f74 100644 --- a/examples/monolithic_build/mlkem_native_monobuild.c +++ b/examples/monolithic_build/mlkem_native_monobuild.c @@ -13,17 +13,16 @@ * mlkem-native */ -#include "mlkem/cbd.c" +#include "mlkem/compress.c" #include "mlkem/debug.c" #include "mlkem/fips202/fips202.c" #include "mlkem/fips202/fips202x4.c" #include "mlkem/fips202/keccakf1600.c" #include "mlkem/indcpa.c" #include "mlkem/kem.c" -#include "mlkem/ntt.c" #include "mlkem/poly.c" #include "mlkem/polyvec.c" -#include "mlkem/rej_uniform.c" +#include "mlkem/sampling.c" #include "mlkem/verify.c" #include "mlkem/zetas.c" @@ -437,6 +436,11 @@ #undef crypto_kem_keypair_derand #endif +/* mlkem/params.h */ +#if defined(HALF_Q) +#undef HALF_Q +#endif + /* mlkem/params.h */ #if defined(KECCAK_WAY) #undef KECCAK_WAY @@ -714,36 +718,6 @@ #undef MLKEM_NATIVE_ARITH_IMPL_H #endif -/* mlkem/cbd.c */ -#if defined(empty_cu_cbd) -#undef empty_cu_cbd -#endif - -/* mlkem/cbd.c */ -#if defined(load24_littleendian) -#undef load24_littleendian -#endif - -/* mlkem/cbd.c */ -#if defined(load32_littleendian) -#undef load32_littleendian -#endif - -/* mlkem/cbd.h */ -#if defined(CBD_H) -#undef CBD_H -#endif - -/* mlkem/cbd.h */ -#if defined(poly_cbd2) -#undef poly_cbd2 -#endif - -/* mlkem/cbd.h */ -#if defined(poly_cbd3) -#undef poly_cbd3 -#endif - /* mlkem/cbmc.h */ #if defined(CBMC_CONCAT) #undef CBMC_CONCAT @@ -869,6 +843,121 @@ #undef writeable #endif +/* mlkem/compress.c */ +#if defined(empty_cu_compress) +#undef empty_cu_compress +#endif + +/* mlkem/compress.h */ +#if defined(COMPRESS_H) +#undef COMPRESS_H +#endif + +/* mlkem/compress.h */ +#if defined(poly_compress_d10) +#undef poly_compress_d10 +#endif + +/* mlkem/compress.h */ +#if defined(poly_compress_d11) +#undef poly_compress_d11 +#endif + +/* mlkem/compress.h */ +#if defined(poly_compress_d4) +#undef poly_compress_d4 +#endif + +/* mlkem/compress.h */ +#if defined(poly_compress_d5) +#undef poly_compress_d5 +#endif + +/* mlkem/compress.h */ +#if defined(poly_decompress_d10) +#undef poly_decompress_d10 +#endif + +/* mlkem/compress.h */ +#if defined(poly_decompress_d11) +#undef poly_decompress_d11 +#endif + +/* mlkem/compress.h */ +#if defined(poly_decompress_d4) +#undef poly_decompress_d4 +#endif + +/* mlkem/compress.h */ +#if defined(poly_decompress_d5) +#undef poly_decompress_d5 +#endif + +/* mlkem/compress.h */ +#if defined(poly_frombytes) +#undef poly_frombytes +#endif + +/* mlkem/compress.h */ +#if defined(poly_frommsg) +#undef poly_frommsg +#endif + +/* mlkem/compress.h */ +#if defined(poly_tobytes) +#undef poly_tobytes +#endif + +/* mlkem/compress.h */ +#if defined(poly_tomsg) +#undef poly_tomsg +#endif + +/* mlkem/compress.h */ +#if defined(scalar_compress_d1) +#undef scalar_compress_d1 +#endif + +/* mlkem/compress.h */ +#if defined(scalar_compress_d10) +#undef scalar_compress_d10 +#endif + +/* mlkem/compress.h */ +#if defined(scalar_compress_d11) +#undef scalar_compress_d11 +#endif + +/* mlkem/compress.h */ +#if defined(scalar_compress_d4) +#undef scalar_compress_d4 +#endif + +/* mlkem/compress.h */ +#if defined(scalar_compress_d5) +#undef scalar_compress_d5 +#endif + +/* mlkem/compress.h */ +#if defined(scalar_decompress_d10) +#undef scalar_decompress_d10 +#endif + +/* mlkem/compress.h */ +#if defined(scalar_decompress_d11) +#undef scalar_decompress_d11 +#endif + +/* mlkem/compress.h */ +#if defined(scalar_decompress_d4) +#undef scalar_decompress_d4 +#endif + +/* mlkem/compress.h */ +#if defined(scalar_decompress_d5) +#undef scalar_decompress_d5 +#endif + /* mlkem/debug.c */ #if defined(MLKEM_NATIVE_DEBUG_ERROR_HEADER) #undef MLKEM_NATIVE_DEBUG_ERROR_HEADER @@ -1144,54 +1233,59 @@ #undef KeccakF1600x4_StateXORBytes #endif -/* mlkem/ntt.c */ -#if defined(empty_cu_ntt) -#undef empty_cu_ntt +/* mlkem/poly.c */ +#if defined(barrett_reduce) +#undef barrett_reduce #endif -/* mlkem/ntt.c */ -#if defined(invntt_layer) -#undef invntt_layer +/* mlkem/poly.c */ +#if defined(basemul_cached) +#undef basemul_cached #endif -/* mlkem/ntt.c */ -#if defined(ntt_butterfly_block) -#undef ntt_butterfly_block +/* mlkem/poly.c */ +#if defined(cast_uint16_to_int16) +#undef cast_uint16_to_int16 #endif -/* mlkem/ntt.c */ -#if defined(ntt_layer) -#undef ntt_layer +/* mlkem/poly.c */ +#if defined(empty_cu_poly) +#undef empty_cu_poly #endif -/* mlkem/ntt.h */ -#if defined(NTT_H) -#undef NTT_H +/* mlkem/poly.c */ +#if defined(fqmul) +#undef fqmul #endif -/* mlkem/ntt.h */ -#if defined(basemul_cached) -#undef basemul_cached +/* mlkem/poly.c */ +#if defined(invntt_layer) +#undef invntt_layer #endif -/* mlkem/ntt.h */ -#if defined(poly_invntt_tomont) -#undef poly_invntt_tomont +/* mlkem/poly.c */ +#if defined(montgomery_reduce) +#undef montgomery_reduce #endif -/* mlkem/ntt.h */ -#if defined(poly_ntt) -#undef poly_ntt +/* mlkem/poly.c */ +#if defined(montgomery_reduce_generic) +#undef montgomery_reduce_generic #endif -/* mlkem/ntt.h */ -#if defined(zetas) -#undef zetas +/* mlkem/poly.c */ +#if defined(ntt_butterfly_block) +#undef ntt_butterfly_block #endif /* mlkem/poly.c */ -#if defined(empty_cu_poly) -#undef empty_cu_poly +#if defined(ntt_layer) +#undef ntt_layer +#endif + +/* mlkem/poly.c */ +#if defined(scalar_signed_to_unsigned_q) +#undef scalar_signed_to_unsigned_q #endif /* mlkem/poly.h */ @@ -1225,53 +1319,8 @@ #endif /* mlkem/poly.h */ -#if defined(poly_compress_d10) -#undef poly_compress_d10 -#endif - -/* mlkem/poly.h */ -#if defined(poly_compress_d11) -#undef poly_compress_d11 -#endif - -/* mlkem/poly.h */ -#if defined(poly_compress_d4) -#undef poly_compress_d4 -#endif - -/* mlkem/poly.h */ -#if defined(poly_compress_d5) -#undef poly_compress_d5 -#endif - -/* mlkem/poly.h */ -#if defined(poly_decompress_d10) -#undef poly_decompress_d10 -#endif - -/* mlkem/poly.h */ -#if defined(poly_decompress_d11) -#undef poly_decompress_d11 -#endif - -/* mlkem/poly.h */ -#if defined(poly_decompress_d4) -#undef poly_decompress_d4 -#endif - -/* mlkem/poly.h */ -#if defined(poly_decompress_d5) -#undef poly_decompress_d5 -#endif - -/* mlkem/poly.h */ -#if defined(poly_frombytes) -#undef poly_frombytes -#endif - -/* mlkem/poly.h */ -#if defined(poly_frommsg) -#undef poly_frommsg +#if defined(poly_invntt_tomont) +#undef poly_invntt_tomont #endif /* mlkem/poly.h */ @@ -1284,6 +1333,11 @@ #undef poly_mulcache_compute #endif +/* mlkem/poly.h */ +#if defined(poly_ntt) +#undef poly_ntt +#endif + /* mlkem/poly.h */ #if defined(poly_reduce) #undef poly_reduce @@ -1294,69 +1348,14 @@ #undef poly_sub #endif -/* mlkem/poly.h */ -#if defined(poly_tobytes) -#undef poly_tobytes -#endif - /* mlkem/poly.h */ #if defined(poly_tomont) #undef poly_tomont #endif /* mlkem/poly.h */ -#if defined(poly_tomsg) -#undef poly_tomsg -#endif - -/* mlkem/poly.h */ -#if defined(scalar_compress_d1) -#undef scalar_compress_d1 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_compress_d10) -#undef scalar_compress_d10 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_compress_d11) -#undef scalar_compress_d11 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_compress_d4) -#undef scalar_compress_d4 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_compress_d5) -#undef scalar_compress_d5 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_decompress_d10) -#undef scalar_decompress_d10 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_decompress_d11) -#undef scalar_decompress_d11 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_decompress_d4) -#undef scalar_decompress_d4 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_decompress_d5) -#undef scalar_decompress_d5 -#endif - -/* mlkem/poly.h */ -#if defined(scalar_signed_to_unsigned_q) -#undef scalar_signed_to_unsigned_q +#if defined(zetas) +#undef zetas #endif /* mlkem/randombytes.h */ @@ -1364,72 +1363,57 @@ #undef RANDOMBYTES_H #endif -/* mlkem/reduce.h */ -#if defined(HALF_Q) -#undef HALF_Q -#endif - -/* mlkem/reduce.h */ -#if defined(REDUCE_H) -#undef REDUCE_H -#endif - -/* mlkem/reduce.h */ -#if defined(barrett_reduce) -#undef barrett_reduce -#endif - -/* mlkem/reduce.h */ -#if defined(cast_uint16_to_int16) -#undef cast_uint16_to_int16 -#endif - -/* mlkem/reduce.h */ -#if defined(fqmul) -#undef fqmul -#endif - -/* mlkem/reduce.h */ -#if defined(montgomery_reduce) -#undef montgomery_reduce +/* mlkem/sampling.c */ +#if defined(MLKEM_GEN_MATRIX_NBLOCKS) +#undef MLKEM_GEN_MATRIX_NBLOCKS #endif -/* mlkem/reduce.h */ -#if defined(montgomery_reduce_generic) -#undef montgomery_reduce_generic +/* mlkem/sampling.c */ +#if defined(empty_cu_sampling) +#undef empty_cu_sampling #endif -/* mlkem/rej_uniform.c */ -#if defined(MLKEM_GEN_MATRIX_NBLOCKS) -#undef MLKEM_GEN_MATRIX_NBLOCKS +/* mlkem/sampling.c */ +#if defined(load24_littleendian) +#undef load24_littleendian #endif -/* mlkem/rej_uniform.c */ -#if defined(empty_cu_rej_uniform) -#undef empty_cu_rej_uniform +/* mlkem/sampling.c */ +#if defined(load32_littleendian) +#undef load32_littleendian #endif -/* mlkem/rej_uniform.c */ +/* mlkem/sampling.c */ #if defined(rej_uniform) #undef rej_uniform #endif -/* mlkem/rej_uniform.c */ +/* mlkem/sampling.c */ #if defined(rej_uniform_scalar) #undef rej_uniform_scalar #endif -/* mlkem/rej_uniform.h */ -#if defined(REJ_UNIFORM_H) -#undef REJ_UNIFORM_H +/* mlkem/sampling.h */ +#if defined(SAMPLING_H) +#undef SAMPLING_H +#endif + +/* mlkem/sampling.h */ +#if defined(poly_cbd2) +#undef poly_cbd2 +#endif + +/* mlkem/sampling.h */ +#if defined(poly_cbd3) +#undef poly_cbd3 #endif -/* mlkem/rej_uniform.h */ +/* mlkem/sampling.h */ #if defined(poly_rej_uniform) #undef poly_rej_uniform #endif -/* mlkem/rej_uniform.h */ +/* mlkem/sampling.h */ #if defined(poly_rej_uniform_x4) #undef poly_rej_uniform_x4 #endif diff --git a/mlkem/cbd.c b/mlkem/cbd.c deleted file mode 100644 index 1e6b7c5d1..000000000 --- a/mlkem/cbd.c +++ /dev/null @@ -1,120 +0,0 @@ -/* - * Copyright (c) 2024 The mlkem-native project authors - * SPDX-License-Identifier: Apache-2.0 - */ -#include "common.h" -#ifndef MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED - -#include -#include "cbd.h" - -/* Static namespacing - * This is to facilitate building multiple instances - * of mlkem-native (e.g. with varying security levels) - * within a single compilation unit. */ -#define load32_littleendian MLKEM_NAMESPACE(load32_littleendian) -#define load24_littleendian MLKEM_NAMESPACE(load24_littleendian) -/* End of static namespacing */ - -/************************************************* - * Name: load32_littleendian - * - * Description: load 4 bytes into a 32-bit integer - * in little-endian order - * - * Arguments: - const uint8_t *x: pointer to input byte array - * - * Returns 32-bit unsigned integer loaded from x - **************************************************/ -static uint32_t load32_littleendian(const uint8_t x[4]) -{ - uint32_t r; - r = (uint32_t)x[0]; - r |= (uint32_t)x[1] << 8; - r |= (uint32_t)x[2] << 16; - r |= (uint32_t)x[3] << 24; - return r; -} - -MLKEM_NATIVE_INTERNAL_API -void poly_cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]) -{ - unsigned i; - for (i = 0; i < MLKEM_N / 8; i++) - __loop__( - invariant(i <= MLKEM_N / 8) - invariant(array_abs_bound(r->coeffs, 0, 8 * i, 3))) - { - unsigned j; - uint32_t t = load32_littleendian(buf + 4 * i); - uint32_t d = t & 0x55555555; - d += (t >> 1) & 0x55555555; - - for (j = 0; j < 8; j++) - __loop__( - invariant(i <= MLKEM_N / 8 && j <= 8) - invariant(array_abs_bound(r->coeffs, 0, 8 * i + j, 3))) - { - const int16_t a = (d >> (4 * j + 0)) & 0x3; - const int16_t b = (d >> (4 * j + 2)) & 0x3; - r->coeffs[8 * i + j] = a - b; - } - } -} - -#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == 3 -/************************************************* - * Name: load24_littleendian - * - * Description: load 3 bytes into a 32-bit integer - * in little-endian order. - * This function is only needed for ML-KEM-512 - * - * Arguments: - const uint8_t *x: pointer to input byte array - * - * Returns 32-bit unsigned integer loaded from x (most significant byte is zero) - **************************************************/ -static uint32_t load24_littleendian(const uint8_t x[3]) -{ - uint32_t r; - r = (uint32_t)x[0]; - r |= (uint32_t)x[1] << 8; - r |= (uint32_t)x[2] << 16; - return r; -} - -MLKEM_NATIVE_INTERNAL_API -void poly_cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]) -{ - unsigned i; - for (i = 0; i < MLKEM_N / 4; i++) - __loop__( - invariant(i <= MLKEM_N / 4) - invariant(array_abs_bound(r->coeffs, 0, 4 * i, 4))) - { - unsigned j; - const uint32_t t = load24_littleendian(buf + 3 * i); - uint32_t d = t & 0x00249249; - d += (t >> 1) & 0x00249249; - d += (t >> 2) & 0x00249249; - - for (j = 0; j < 4; j++) - __loop__( - invariant(i <= MLKEM_N / 4 && j <= 4) - invariant(array_abs_bound(r->coeffs, 0, 4 * i + j, 4))) - { - const int16_t a = (d >> (6 * j + 0)) & 0x7; - const int16_t b = (d >> (6 * j + 3)) & 0x7; - r->coeffs[4 * i + j] = a - b; - } - } -} -#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == \ - 3 */ - -#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ - -#define empty_cu_cbd MLKEM_NAMESPACE_K(empty_cu_cbd) -int empty_cu_cbd; - -#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/cbd.h b/mlkem/cbd.h deleted file mode 100644 index 54c1f5b90..000000000 --- a/mlkem/cbd.h +++ /dev/null @@ -1,43 +0,0 @@ -/* - * Copyright (c) 2024 The mlkem-native project authors - * SPDX-License-Identifier: Apache-2.0 - */ -#ifndef CBD_H -#define CBD_H - -#include -#include "common.h" -#include "poly.h" - -#define poly_cbd2 MLKEM_NAMESPACE(poly_cbd2) -/************************************************* - * Name: poly_cbd2 - * - * Description: Given an array of uniformly random bytes, compute - * polynomial with coefficients distributed according to - * a centered binomial distribution with parameter eta=2 - * - * Arguments: - poly *r: pointer to output polynomial - * - const uint8_t *buf: pointer to input byte array - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]); - -#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == 3 -#define poly_cbd3 MLKEM_NAMESPACE(poly_cbd3) -/************************************************* - * Name: poly_cbd3 - * - * Description: Given an array of uniformly random bytes, compute - * polynomial with coefficients distributed according to - * a centered binomial distribution with parameter eta=3. - * This function is only needed for ML-KEM-512 - * - * Arguments: - poly *r: pointer to output polynomial - * - const uint8_t *buf: pointer to input byte array - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]); -#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD || MLKEM_ETA1 == 3 */ - -#endif /* CBD_H */ diff --git a/mlkem/compress.c b/mlkem/compress.c new file mode 100644 index 000000000..fd6ea2a35 --- /dev/null +++ b/mlkem/compress.c @@ -0,0 +1,395 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ +#include "common.h" +#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) + +#include +#include +#include "arith_backend.h" +#include "cbmc.h" +#include "compress.h" +#include "debug.h" +#include "verify.h" + +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || (MLKEM_K == 2 || MLKEM_K == 3) +MLKEM_NATIVE_INTERNAL_API +void poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const poly *a) +{ + unsigned i; + debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + + for (i = 0; i < MLKEM_N / 8; i++) + __loop__(invariant(i <= MLKEM_N / 8)) + { + unsigned j; + uint8_t t[8] = {0}; + for (j = 0; j < 8; j++) + __loop__( + invariant(i <= MLKEM_N / 8 && j <= 8) + invariant(array_bound(t, 0, j, 0, 16))) + { + t[j] = scalar_compress_d4(a->coeffs[8 * i + j]); + } + + r[i * 4] = t[0] | (t[1] << 4); + r[i * 4 + 1] = t[2] | (t[3] << 4); + r[i * 4 + 2] = t[4] | (t[5] << 4); + r[i * 4 + 3] = t[6] | (t[7] << 4); + } +} + +MLKEM_NATIVE_INTERNAL_API +void poly_compress_d10(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], const poly *a) +{ + unsigned j; + debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + for (j = 0; j < MLKEM_N / 4; j++) + __loop__(invariant(j <= MLKEM_N / 4)) + { + unsigned k; + uint16_t t[4]; + for (k = 0; k < 4; k++) + __loop__( + invariant(k <= 4) + invariant(forall(r, 0, k, t[r] < (1u << 10)))) + { + t[k] = scalar_compress_d10(a->coeffs[4 * j + k]); + } + + /* + * Make all implicit truncation explicit. No data is being + * truncated for the LHS's since each t[i] is 10-bit in size. + */ + r[5 * j + 0] = (t[0] >> 0) & 0xFF; + r[5 * j + 1] = (t[0] >> 8) | ((t[1] << 2) & 0xFF); + r[5 * j + 2] = (t[1] >> 6) | ((t[2] << 4) & 0xFF); + r[5 * j + 3] = (t[2] >> 4) | ((t[3] << 6) & 0xFF); + r[5 * j + 4] = (t[3] >> 2); + } +} + +MLKEM_NATIVE_INTERNAL_API +void poly_decompress_d4(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D4]) +{ + unsigned i; + for (i = 0; i < MLKEM_N / 2; i++) + __loop__( + invariant(i <= MLKEM_N / 2) + invariant(array_bound(r->coeffs, 0, 2 * i, 0, MLKEM_Q))) + { + r->coeffs[2 * i + 0] = scalar_decompress_d4((a[i] >> 0) & 0xF); + r->coeffs[2 * i + 1] = scalar_decompress_d4((a[i] >> 4) & 0xF); + } + + debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q); +} + +MLKEM_NATIVE_INTERNAL_API +void poly_decompress_d10(poly *r, + const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D10]) +{ + unsigned j; + for (j = 0; j < MLKEM_N / 4; j++) + __loop__( + invariant(j <= MLKEM_N / 4) + invariant(array_bound(r->coeffs, 0, 4 * j, 0, MLKEM_Q))) + { + unsigned k; + uint16_t t[4]; + uint8_t const *base = &a[5 * j]; + + t[0] = 0x3FF & ((base[0] >> 0) | ((uint16_t)base[1] << 8)); + t[1] = 0x3FF & ((base[1] >> 2) | ((uint16_t)base[2] << 6)); + t[2] = 0x3FF & ((base[2] >> 4) | ((uint16_t)base[3] << 4)); + t[3] = 0x3FF & ((base[3] >> 6) | ((uint16_t)base[4] << 2)); + + for (k = 0; k < 4; k++) + __loop__( + invariant(k <= 4) + invariant(array_bound(r->coeffs, 0, 4 * j + k, 0, MLKEM_Q))) + { + r->coeffs[4 * j + k] = scalar_decompress_d10(t[k]); + } + } + + debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q); +} +#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || (MLKEM_K == 2 \ + || MLKEM_K == 3) */ + +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_K == 4 +MLKEM_NATIVE_INTERNAL_API +void poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const poly *a) +{ + unsigned i; + debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + + for (i = 0; i < MLKEM_N / 8; i++) + __loop__(invariant(i <= MLKEM_N / 8)) + { + unsigned j; + uint8_t t[8] = {0}; + for (j = 0; j < 8; j++) + __loop__( + invariant(i <= MLKEM_N / 8 && j <= 8) + invariant(array_bound(t, 0, j, 0, 32))) + { + t[j] = scalar_compress_d5(a->coeffs[8 * i + j]); + } + + /* + * Explicitly truncate to avoid warning about + * implicit truncation in CBMC, and use array indexing into + * r rather than pointer-arithmetic to simplify verification + */ + r[i * 5] = 0xFF & ((t[0] >> 0) | (t[1] << 5)); + r[i * 5 + 1] = 0xFF & ((t[1] >> 3) | (t[2] << 2) | (t[3] << 7)); + r[i * 5 + 2] = 0xFF & ((t[3] >> 1) | (t[4] << 4)); + r[i * 5 + 3] = 0xFF & ((t[4] >> 4) | (t[5] << 1) | (t[6] << 6)); + r[i * 5 + 4] = 0xFF & ((t[6] >> 2) | (t[7] << 3)); + } +} + +MLKEM_NATIVE_INTERNAL_API +void poly_compress_d11(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const poly *a) +{ + unsigned j; + debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + + for (j = 0; j < MLKEM_N / 8; j++) + __loop__(invariant(j <= MLKEM_N / 8)) + { + unsigned k; + uint16_t t[8]; + for (k = 0; k < 8; k++) + __loop__( + invariant(k <= 8) + invariant(forall(r, 0, k, t[r] < (1u << 11)))) + { + t[k] = scalar_compress_d11(a->coeffs[8 * j + k]); + } + + /* + * Make all implicit truncation explicit. No data is being + * truncated for the LHS's since each t[i] is 11-bit in size. + */ + r[11 * j + 0] = (t[0] >> 0) & 0xFF; + r[11 * j + 1] = (t[0] >> 8) | ((t[1] << 3) & 0xFF); + r[11 * j + 2] = (t[1] >> 5) | ((t[2] << 6) & 0xFF); + r[11 * j + 3] = (t[2] >> 2) & 0xFF; + r[11 * j + 4] = (t[2] >> 10) | ((t[3] << 1) & 0xFF); + r[11 * j + 5] = (t[3] >> 7) | ((t[4] << 4) & 0xFF); + r[11 * j + 6] = (t[4] >> 4) | ((t[5] << 7) & 0xFF); + r[11 * j + 7] = (t[5] >> 1) & 0xFF; + r[11 * j + 8] = (t[5] >> 9) | ((t[6] << 2) & 0xFF); + r[11 * j + 9] = (t[6] >> 6) | ((t[7] << 5) & 0xFF); + r[11 * j + 10] = (t[7] >> 3); + } +} + +MLKEM_NATIVE_INTERNAL_API +void poly_decompress_d5(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D5]) +{ + unsigned i; + for (i = 0; i < MLKEM_N / 8; i++) + __loop__( + invariant(i <= MLKEM_N / 8) + invariant(array_bound(r->coeffs, 0, 8 * i, 0, MLKEM_Q))) + { + unsigned j; + uint8_t t[8]; + const unsigned offset = i * 5; + /* + * Explicitly truncate to avoid warning about + * implicit truncation in CBMC and unwind loop for ease + * of proof. + */ + + /* + * Decompress 5 8-bit bytes (so 40 bits) into + * 8 5-bit values stored in t[] + */ + t[0] = 0x1F & (a[offset + 0] >> 0); + t[1] = 0x1F & ((a[offset + 0] >> 5) | (a[offset + 1] << 3)); + t[2] = 0x1F & (a[offset + 1] >> 2); + t[3] = 0x1F & ((a[offset + 1] >> 7) | (a[offset + 2] << 1)); + t[4] = 0x1F & ((a[offset + 2] >> 4) | (a[offset + 3] << 4)); + t[5] = 0x1F & (a[offset + 3] >> 1); + t[6] = 0x1F & ((a[offset + 3] >> 6) | (a[offset + 4] << 2)); + t[7] = 0x1F & (a[offset + 4] >> 3); + + /* and copy to the correct slice in r[] */ + for (j = 0; j < 8; j++) + __loop__( + invariant(j <= 8 && i <= MLKEM_N / 8) + invariant(array_bound(r->coeffs, 0, 8 * i + j, 0, MLKEM_Q))) + { + r->coeffs[8 * i + j] = scalar_decompress_d5(t[j]); + } + } + + debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q); +} + +MLKEM_NATIVE_INTERNAL_API +void poly_decompress_d11(poly *r, + const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D11]) +{ + unsigned j; + for (j = 0; j < MLKEM_N / 8; j++) + __loop__( + invariant(j <= MLKEM_N / 8) + invariant(array_bound(r->coeffs, 0, 8 * j, 0, MLKEM_Q))) + { + unsigned k; + uint16_t t[8]; + uint8_t const *base = &a[11 * j]; + t[0] = 0x7FF & ((base[0] >> 0) | ((uint16_t)base[1] << 8)); + t[1] = 0x7FF & ((base[1] >> 3) | ((uint16_t)base[2] << 5)); + t[2] = 0x7FF & ((base[2] >> 6) | ((uint16_t)base[3] << 2) | + ((uint16_t)base[4] << 10)); + t[3] = 0x7FF & ((base[4] >> 1) | ((uint16_t)base[5] << 7)); + t[4] = 0x7FF & ((base[5] >> 4) | ((uint16_t)base[6] << 4)); + t[5] = 0x7FF & ((base[6] >> 7) | ((uint16_t)base[7] << 1) | + ((uint16_t)base[8] << 9)); + t[6] = 0x7FF & ((base[8] >> 2) | ((uint16_t)base[9] << 6)); + t[7] = 0x7FF & ((base[9] >> 5) | ((uint16_t)base[10] << 3)); + + for (k = 0; k < 8; k++) + __loop__( + invariant(k <= 8) + invariant(array_bound(r->coeffs, 0, 8 * j + k, 0, MLKEM_Q))) + { + r->coeffs[8 * j + k] = scalar_decompress_d11(t[k]); + } + } + + debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q); +} +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD) || MLKEM_K == 4 */ + +#if !defined(MLKEM_USE_NATIVE_POLY_TOBYTES) +MLKEM_NATIVE_INTERNAL_API +void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a) +{ + unsigned i; + debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + + for (i = 0; i < MLKEM_N / 2; i++) + __loop__(invariant(i <= MLKEM_N / 2)) + { + const uint16_t t0 = a->coeffs[2 * i]; + const uint16_t t1 = a->coeffs[2 * i + 1]; + /* + * t0 and t1 are both < MLKEM_Q, so contain at most 12 bits each of + * significant data, so these can be packed into 24 bits or exactly + * 3 bytes, as follows. + */ + + /* Least significant bits 0 - 7 of t0. */ + r[3 * i + 0] = t0 & 0xFF; + + /* + * Most significant bits 8 - 11 of t0 become the least significant + * nibble of the second byte. The least significant 4 bits + * of t1 become the upper nibble of the second byte. + */ + r[3 * i + 1] = (t0 >> 8) | ((t1 << 4) & 0xF0); + + /* Bits 4 - 11 of t1 become the third byte. */ + r[3 * i + 2] = t1 >> 4; + } +} +#else /* MLKEM_USE_NATIVE_POLY_TOBYTES */ +MLKEM_NATIVE_INTERNAL_API +void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a) +{ + debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + poly_tobytes_native(r, a); +} +#endif /* MLKEM_USE_NATIVE_POLY_TOBYTES */ + +#if !defined(MLKEM_USE_NATIVE_POLY_FROMBYTES) +MLKEM_NATIVE_INTERNAL_API +void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES]) +{ + unsigned i; + for (i = 0; i < MLKEM_N / 2; i++) + __loop__( + invariant(i <= MLKEM_N / 2) + invariant(array_bound(r->coeffs, 0, 2 * i, 0, UINT12_LIMIT))) + { + const uint8_t t0 = a[3 * i + 0]; + const uint8_t t1 = a[3 * i + 1]; + const uint8_t t2 = a[3 * i + 2]; + r->coeffs[2 * i + 0] = t0 | ((t1 << 8) & 0xFFF); + r->coeffs[2 * i + 1] = (t1 >> 4) | (t2 << 4); + } + + /* Note that the coefficients are not canonical */ + debug_assert_bound(r, MLKEM_N, 0, UINT12_LIMIT); +} +#else /* MLKEM_USE_NATIVE_POLY_FROMBYTES */ +MLKEM_NATIVE_INTERNAL_API +void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES]) +{ + poly_frombytes_native(r, a); +} +#endif /* MLKEM_USE_NATIVE_POLY_FROMBYTES */ + +MLKEM_NATIVE_INTERNAL_API +void poly_frommsg(poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES]) +{ + unsigned i; +#if (MLKEM_INDCPA_MSGBYTES != MLKEM_N / 8) +#error "MLKEM_INDCPA_MSGBYTES must be equal to MLKEM_N/8 bytes!" +#endif + + for (i = 0; i < MLKEM_N / 8; i++) + __loop__( + invariant(i <= MLKEM_N / 8) + invariant(array_bound(r->coeffs, 0, 8 * i, 0, MLKEM_Q))) + { + unsigned j; + for (j = 0; j < 8; j++) + __loop__( + invariant(i < MLKEM_N / 8 && j <= 8) + invariant(array_bound(r->coeffs, 0, 8 * i + j, 0, MLKEM_Q))) + { + /* Prevent the compiler from recognizing this as a bit selection */ + uint8_t mask = value_barrier_u8(1u << j); + r->coeffs[8 * i + j] = ct_sel_int16(HALF_Q, 0, msg[i] & mask); + } + } + debug_assert_abs_bound(r, MLKEM_N, MLKEM_Q); +} + +MLKEM_NATIVE_INTERNAL_API +void poly_tomsg(uint8_t msg[MLKEM_INDCPA_MSGBYTES], const poly *a) +{ + unsigned i; + debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + + for (i = 0; i < MLKEM_N / 8; i++) + __loop__(invariant(i <= MLKEM_N / 8)) + { + unsigned j; + msg[i] = 0; + for (j = 0; j < 8; j++) + __loop__( + invariant(i <= MLKEM_N / 8 && j <= 8)) + { + uint32_t t = scalar_compress_d1(a->coeffs[8 * i + j]); + msg[i] |= t << j; + } + } +} + +#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ + +#define empty_cu_compress MLKEM_NAMESPACE_K(empty_cu_compress) +int empty_cu_compress; + +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/compress.h b/mlkem/compress.h new file mode 100644 index 000000000..409dbe519 --- /dev/null +++ b/mlkem/compress.h @@ -0,0 +1,495 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ +#ifndef COMPRESS_H +#define COMPRESS_H + +#include +#include +#include "cbmc.h" +#include "common.h" +#include "debug.h" +#include "poly.h" +#include "verify.h" + +/* Static namespacing + * This is to facilitate building multiple instances + * of mlkem-native (e.g. with varying security levels) + * within a single compilation unit. */ +#define scalar_compress_d1 MLKEM_NAMESPACE(scalar_compress_d1) +#define scalar_compress_d4 MLKEM_NAMESPACE(scalar_compress_d4) +#define scalar_compress_d5 MLKEM_NAMESPACE(scalar_compress_d5) +#define scalar_compress_d10 MLKEM_NAMESPACE(scalar_compress_d10) +#define scalar_compress_d11 MLKEM_NAMESPACE(scalar_compress_d11) +#define scalar_decompress_d4 MLKEM_NAMESPACE(scalar_decompress_d4) +#define scalar_decompress_d5 MLKEM_NAMESPACE(scalar_decompress_d5) +#define scalar_decompress_d10 MLKEM_NAMESPACE(scalar_decompress_d10) +#define scalar_decompress_d11 MLKEM_NAMESPACE(scalar_decompress_d11) +/* End of static namespacing */ + +/************************************************************ + * Name: scalar_compress_d1 + * + * Description: Computes round(u * 2 / q) + * + * Implements Compress_d from FIPS203, Eq (4.7), + * for d = 1. + * + * Arguments: - u: Unsigned canonical modulus modulo q + * to be compressed. + ************************************************************/ +/* + * The multiplication in this routine will exceed UINT32_MAX + * and wrap around for large values of u. This is expected and required. + */ +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "unsigned-overflow" +#endif +static INLINE uint32_t scalar_compress_d1(uint16_t u) +__contract__( + requires(u <= MLKEM_Q - 1) + ensures(return_value < 2) + ensures(return_value == (((uint32_t)u * 2 + MLKEM_Q / 2) / MLKEM_Q) % 2) ) +{ + uint32_t d0 = u << 1; + d0 *= 645083; + d0 += 1u << 30; + d0 >>= 31; + return d0; +} +#ifdef CBMC +#pragma CPROVER check pop +#endif + +/************************************************************ + * Name: scalar_compress_d4 + * + * Description: Computes round(u * 16 / q) % 16 + * + * Implements Compress_d from FIPS203, Eq (4.7), + * for d = 4. + * + * Arguments: - u: Unsigned canonical modulus modulo q + * to be compressed. + ************************************************************/ +/* + * The multiplication in this routine will exceed UINT32_MAX + * and wrap around for large values of u. This is expected and required. + */ +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "unsigned-overflow" +#endif +static INLINE uint32_t scalar_compress_d4(uint16_t u) +__contract__( + requires(u <= MLKEM_Q - 1) + ensures(return_value < 16) + ensures(return_value == (((uint32_t)u * 16 + MLKEM_Q / 2) / MLKEM_Q) % 16)) +{ + uint32_t d0 = (uint32_t)u * 1290160; /* 16 * round(2^28 / MLKEM_Q) */ + return (d0 + (1u << 27)) >> 28; /* round(d0/2^28) */ +} +#ifdef CBMC +#pragma CPROVER check pop +#endif + +/************************************************************ + * Name: scalar_decompress_d4 + * + * Description: Computes round(u * q / 16) + * + * Implements Decompress_d from FIPS203, Eq (4.8), + * for d = 4. + * + * Arguments: - u: Unsigned canonical modulus modulo 16 + * to be decompressed. + ************************************************************/ +static INLINE uint16_t scalar_decompress_d4(uint32_t u) +__contract__( + requires(0 <= u && u < 16) + ensures(return_value <= (MLKEM_Q - 1)) +) { return ((u * MLKEM_Q) + 8) / 16; } + +/************************************************************ + * Name: scalar_compress_d5 + * + * Description: Computes round(u * 32 / q) % 32 + * + * Implements Compress_d from FIPS203, Eq (4.7), + * for d = 5. + * + * Arguments: - u: Unsigned canonical modulus modulo q + * to be compressed. + ************************************************************/ +/* + * The multiplication in this routine will exceed UINT32_MAX + * and wrap around for large values of u. This is expected and required. + */ +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "unsigned-overflow" +#endif +static INLINE uint32_t scalar_compress_d5(uint16_t u) +__contract__( + requires(u <= MLKEM_Q - 1) + ensures(return_value < 32) + ensures(return_value == (((uint32_t)u * 32 + MLKEM_Q / 2) / MLKEM_Q) % 32) ) +{ + uint32_t d0 = (uint32_t)u * 1290176; /* 2^5 * round(2^27 / MLKEM_Q) */ + return (d0 + (1u << 26)) >> 27; /* round(d0/2^27) */ +} +#ifdef CBMC +#pragma CPROVER check pop +#endif + +/************************************************************ + * Name: scalar_decompress_d5 + * + * Description: Computes round(u * q / 32) + * + * Implements Decompress_d from FIPS203, Eq (4.8), + * for d = 5. + * + * Arguments: - u: Unsigned canonical modulus modulo 32 + * to be decompressed. + ************************************************************/ +static INLINE uint16_t scalar_decompress_d5(uint32_t u) +__contract__( + requires(0 <= u && u < 32) + ensures(return_value <= MLKEM_Q - 1) +) { return ((u * MLKEM_Q) + 16) / 32; } + +/************************************************************ + * Name: scalar_compress_d10 + * + * Description: Computes round(u * 2**10 / q) % 2**10 + * + * Implements Compress_d from FIPS203, Eq (4.7), + * for d = 10. + * + * Arguments: - u: Unsigned canonical modulus modulo q + * to be compressed. + ************************************************************/ +/* + * The multiplication in this routine will exceed UINT32_MAX + * and wrap around for large values of u. This is expected and required. + */ +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "unsigned-overflow" +#endif +static INLINE uint32_t scalar_compress_d10(uint16_t u) +__contract__( + requires(u <= MLKEM_Q - 1) + ensures(return_value < (1u << 10)) + ensures(return_value == (((uint32_t)u * (1u << 10) + MLKEM_Q / 2) / MLKEM_Q) % (1 << 10))) +{ + uint64_t d0 = (uint64_t)u * 2642263040; /* 2^10 * round(2^32 / MLKEM_Q) */ + d0 = (d0 + ((uint64_t)1u << 32)) >> 33; + return (d0 & 0x3FF); +} +#ifdef CBMC +#pragma CPROVER check pop +#endif + +/************************************************************ + * Name: scalar_decompress_d10 + * + * Description: Computes round(u * q / 1024) + * + * Implements Decompress_d from FIPS203, Eq (4.8), + * for d = 10. + * + * Arguments: - u: Unsigned canonical modulus modulo 16 + * to be decompressed. + ************************************************************/ +static INLINE uint16_t scalar_decompress_d10(uint32_t u) +__contract__( + requires(0 <= u && u < 1024) + ensures(return_value <= (MLKEM_Q - 1)) +) { return ((u * MLKEM_Q) + 512) / 1024; } + +/************************************************************ + * Name: scalar_compress_d11 + * + * Description: Computes round(u * 2**11 / q) % 2**11 + * + * Implements Compress_d from FIPS203, Eq (4.7), + * for d = 11. + * + * Arguments: - u: Unsigned canonical modulus modulo q + * to be compressed. + ************************************************************/ +/* + * The multiplication in this routine will exceed UINT32_MAX + * and wrap around for large values of u. This is expected and required. + */ +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "unsigned-overflow" +#endif +static INLINE uint32_t scalar_compress_d11(uint16_t u) +__contract__( + requires(u <= MLKEM_Q - 1) + ensures(return_value < (1u << 11)) + ensures(return_value == (((uint32_t)u * (1u << 11) + MLKEM_Q / 2) / MLKEM_Q) % (1 << 11))) +{ + uint64_t d0 = (uint64_t)u * 5284526080; /* 2^11 * round(2^33 / MLKEM_Q) */ + d0 = (d0 + ((uint64_t)1u << 32)) >> 33; + return (d0 & 0x7FF); +} +#ifdef CBMC +#pragma CPROVER check pop +#endif + +/************************************************************ + * Name: scalar_decompress_d11 + * + * Description: Computes round(u * q / 1024) + * + * Implements Decompress_d from FIPS203, Eq (4.8), + * for d = 10. + * + * Arguments: - u: Unsigned canonical modulus modulo 16 + * to be decompressed. + ************************************************************/ +static INLINE uint16_t scalar_decompress_d11(uint32_t u) +__contract__( + requires(0 <= u && u < 2048) + ensures(return_value <= (MLKEM_Q - 1)) +) { return ((u * MLKEM_Q) + 1024) / 2048; } + +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || \ + (MLKEM_K == 2 || MLKEM_K == 3) +#define poly_compress_d4 MLKEM_NAMESPACE(poly_compress_d4) +/************************************************* + * Name: poly_compress_d4 + * + * Description: Compression (4 bits) and subsequent serialization of a + * polynomial + * + * Arguments: - uint8_t *r: pointer to output byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_D4 bytes) + * - const poly *a: pointer to input polynomial + * Coefficients must be unsigned canonical, + * i.e. in [0,1,..,MLKEM_Q-1]. + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const poly *a); + +#define poly_compress_d10 MLKEM_NAMESPACE(poly_compress_d10) +/************************************************* + * Name: poly_compress_d10 + * + * Description: Compression (10 bits) and subsequent serialization of a + * polynomial + * + * Arguments: - uint8_t *r: pointer to output byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_D10 bytes) + * - const poly *a: pointer to input polynomial + * Coefficients must be unsigned canonical, + * i.e. in [0,1,..,MLKEM_Q-1]. + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_compress_d10(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], const poly *a); + +#define poly_decompress_d4 MLKEM_NAMESPACE(poly_decompress_d4) +/************************************************* + * Name: poly_decompress_d4 + * + * Description: De-serialization and subsequent decompression (dv bits) of a + * polynomial; approximate inverse of poly_compress + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *a: pointer to input byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_D4 bytes) + * + * Upon return, the coefficients of the output polynomial are unsigned-canonical + * (non-negative and smaller than MLKEM_Q). + * + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_decompress_d4(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D4]); + +#define poly_decompress_d10 MLKEM_NAMESPACE(poly_decompress_d10) +/************************************************* + * Name: poly_decompress_d10 + * + * Description: De-serialization and subsequent decompression (10 bits) of a + * polynomial; approximate inverse of poly_compress_d10 + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *a: pointer to input byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_D10 bytes) + * + * Upon return, the coefficients of the output polynomial are unsigned-canonical + * (non-negative and smaller than MLKEM_Q). + * + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_decompress_d10(poly *r, + const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D10]); +#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || (MLKEM_K == 2 \ + || MLKEM_K == 3) */ + +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_K == 4 +#define poly_compress_d5 MLKEM_NAMESPACE(poly_compress_d5) +/************************************************* + * Name: poly_compress_d5 + * + * Description: Compression (5 bits) and subsequent serialization of a + * polynomial + * + * Arguments: - uint8_t *r: pointer to output byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_D5 bytes) + * - const poly *a: pointer to input polynomial + * Coefficients must be unsigned canonical, + * i.e. in [0,1,..,MLKEM_Q-1]. + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const poly *a); + +#define poly_compress_d11 MLKEM_NAMESPACE(poly_compress_d11) +/************************************************* + * Name: poly_compress_d11 + * + * Description: Compression (11 bits) and subsequent serialization of a + * polynomial + * + * Arguments: - uint8_t *r: pointer to output byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_D11 bytes) + * - const poly *a: pointer to input polynomial + * Coefficients must be unsigned canonical, + * i.e. in [0,1,..,MLKEM_Q-1]. + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_compress_d11(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const poly *a); + +#define poly_decompress_d5 MLKEM_NAMESPACE(poly_decompress_d5) +/************************************************* + * Name: poly_decompress_d5 + * + * Description: De-serialization and subsequent decompression (dv bits) of a + * polynomial; approximate inverse of poly_compress + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *a: pointer to input byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_D5 bytes) + * + * Upon return, the coefficients of the output polynomial are unsigned-canonical + * (non-negative and smaller than MLKEM_Q). + * + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_decompress_d5(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D5]); + +#define poly_decompress_d11 MLKEM_NAMESPACE(poly_decompress_d11) +/************************************************* + * Name: poly_decompress_d11 + * + * Description: De-serialization and subsequent decompression (11 bits) of a + * polynomial; approximate inverse of poly_compress_d11 + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *a: pointer to input byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_D11 bytes) + * + * Upon return, the coefficients of the output polynomial are unsigned-canonical + * (non-negative and smaller than MLKEM_Q). + * + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_decompress_d11(poly *r, + const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D11]); +#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_K == 4 \ + */ + +#define poly_tobytes MLKEM_NAMESPACE(poly_tobytes) +/************************************************* + * Name: poly_tobytes + * + * Description: Serialization of a polynomial. + * Signed coefficients are converted to + * unsigned form before serialization. + * + * Arguments: INPUT: + * - a: const pointer to input polynomial, + * with each coefficient in the range [0,1,..,Q-1] + * OUTPUT + * - r: pointer to output byte array + * (of MLKEM_POLYBYTES bytes) + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a) +__contract__( + requires(memory_no_alias(r, MLKEM_POLYBYTES)) + requires(memory_no_alias(a, sizeof(poly))) + requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) + assigns(object_whole(r)) +); + + +#define poly_frombytes MLKEM_NAMESPACE(poly_frombytes) +/************************************************* + * Name: poly_frombytes + * + * Description: De-serialization of a polynomial. + * + * Arguments: INPUT + * - a: pointer to input byte array + * (of MLKEM_POLYBYTES bytes) + * OUTPUT + * - r: pointer to output polynomial, with + * each coefficient unsigned and in the range + * 0 .. 4095 + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES]) +__contract__( + requires(memory_no_alias(a, MLKEM_POLYBYTES)) + requires(memory_no_alias(r, sizeof(poly))) + assigns(memory_slice(r, sizeof(poly))) + ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, UINT12_LIMIT)) +); + + +#define poly_frommsg MLKEM_NAMESPACE(poly_frommsg) +/************************************************* + * Name: poly_frommsg + * + * Description: Convert 32-byte message to polynomial + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *msg: pointer to input message + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_frommsg(poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES]) +__contract__( + requires(memory_no_alias(msg, MLKEM_INDCPA_MSGBYTES)) + requires(memory_no_alias(r, sizeof(poly))) + assigns(object_whole(r)) + ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) +); + +#define poly_tomsg MLKEM_NAMESPACE(poly_tomsg) +/************************************************* + * Name: poly_tomsg + * + * Description: Convert polynomial to 32-byte message + * + * Arguments: - uint8_t *msg: pointer to output message + * - const poly *r: pointer to input polynomial + * Coefficients must be unsigned canonical + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_tomsg(uint8_t msg[MLKEM_INDCPA_MSGBYTES], const poly *r) +__contract__( + requires(memory_no_alias(msg, MLKEM_INDCPA_MSGBYTES)) + requires(memory_no_alias(r, sizeof(poly))) + requires(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) + assigns(object_whole(msg)) +); + +#endif /* COMPRESS_H */ diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 390cc6f29..488cb5f4d 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -9,11 +9,10 @@ #include "fips202/fips202.h" #include "fips202/fips202x4.h" #include "indcpa.h" -#include "ntt.h" #include "poly.h" #include "polyvec.h" #include "randombytes.h" -#include "rej_uniform.h" +#include "sampling.h" #include "symmetric.h" #include "arith_backend.h" diff --git a/mlkem/ntt.c b/mlkem/ntt.c deleted file mode 100644 index 3651c8da9..000000000 --- a/mlkem/ntt.c +++ /dev/null @@ -1,266 +0,0 @@ -/* - * Copyright (c) 2024 The mlkem-native project authors - * SPDX-License-Identifier: Apache-2.0 - */ -#include "common.h" -#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) - -#include -#include "arith_backend.h" -#include "debug.h" -#include "ntt.h" -#include "reduce.h" - -/* Static namespacing - * This is to facilitate building multiple instances - * of mlkem-native (e.g. with varying security levels) - * within a single compilation unit. */ -#define ntt_butterfly_block MLKEM_NAMESPACE(ntt_butterfly_block) -#define ntt_layer MLKEM_NAMESPACE(ntt_layer) -#define invntt_layer MLKEM_NAMESPACE(invntt_layer) -/* End of static namespacing */ - -#if !defined(MLKEM_USE_NATIVE_NTT) -/* - * Computes a block CT butterflies with a fixed twiddle factor, - * using Montgomery multiplication. - * Parameters: - * - r: Pointer to base of polynomial (_not_ the base of butterfly block) - * - root: Twiddle factor to use for the butterfly. This must be in - * Montgomery form and signed canonical. - * - start: Offset to the beginning of the butterfly block - * - len: Index difference between coefficients subject to a butterfly - * - bound: Ghost variable describing coefficient bound: Prior to `start`, - * coefficients must be bound by `bound + MLKEM_Q`. Post `start`, - * they must be bound by `bound`. - * When this function returns, output coefficients in the index range - * [start, start+2*len) have bound bumped to `bound + MLKEM_Q`. - * Example: - * - start=8, len=4 - * This would compute the following four butterflies - * 8 -- 12 - * 9 -- 13 - * 10 -- 14 - * 11 -- 15 - * - start=4, len=2 - * This would compute the following two butterflies - * 4 -- 6 - * 5 -- 7 - */ -static void ntt_butterfly_block(int16_t r[MLKEM_N], int16_t zeta, - unsigned start, unsigned len, int bound) -__contract__( - requires(start < MLKEM_N) - requires(1 <= len && len <= MLKEM_N / 2 && start + 2 * len <= MLKEM_N) - requires(0 <= bound && bound < INT16_MAX - MLKEM_Q) - requires(-HALF_Q < zeta && zeta < HALF_Q) - requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) - requires(array_abs_bound(r, 0, start, bound + MLKEM_Q)) - requires(array_abs_bound(r, start, MLKEM_N, bound)) - assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) - ensures(array_abs_bound(r, 0, start + 2*len, bound + MLKEM_Q)) - ensures(array_abs_bound(r, start + 2 * len, MLKEM_N, bound))) -{ - /* `bound` is a ghost variable only needed in the CBMC specification */ - unsigned j; - ((void)bound); - for (j = start; j < start + len; j++) - __loop__( - invariant(start <= j && j <= start + len) - /* - * Coefficients are updated in strided pairs, so the bounds for the - * intermediate states alternate twice between the old and new bound - */ - invariant(array_abs_bound(r, 0, j, bound + MLKEM_Q)) - invariant(array_abs_bound(r, j, start + len, bound)) - invariant(array_abs_bound(r, start + len, j + len, bound + MLKEM_Q)) - invariant(array_abs_bound(r, j + len, MLKEM_N, bound))) - { - int16_t t; - t = fqmul(r[j + len], zeta); - r[j + len] = r[j] - t; - r[j] = r[j] + t; - } -} - -/* - *Compute one layer of forward NTT - * Parameters: - * - r: Pointer to base of polynomial - * - len: Stride of butterflies in this layer. - * - layer: Ghost variable indicating which layer is being applied. - * Must match `len` via `len == MLKEM_N >> layer`. - * Note: `len` could be dropped and computed in the function, but - * we are following the structure of the reference NTT from the - * official Kyber implementation here, merely adding `layer` as - * a ghost variable for the specifications. - */ -static void ntt_layer(int16_t r[MLKEM_N], unsigned len, unsigned layer) -__contract__( - requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) - requires(1 <= layer && layer <= 7 && len == (MLKEM_N >> layer)) - requires(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q)) - assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) - ensures(array_abs_bound(r, 0, MLKEM_N, (layer + 1) * MLKEM_Q))) -{ - unsigned start, k; - /* `layer` is a ghost variable only needed in the CBMC specification */ - ((void)layer); - /* Twiddle factors for layer n start at index 2^(layer-1) */ - k = MLKEM_N / (2 * len); - for (start = 0; start < MLKEM_N; start += 2 * len) - __loop__( - invariant(start < MLKEM_N + 2 * len) - invariant(k <= MLKEM_N / 2 && 2 * len * k == start + MLKEM_N) - invariant(array_abs_bound(r, 0, start, layer * MLKEM_Q + MLKEM_Q)) - invariant(array_abs_bound(r, start, MLKEM_N, layer * MLKEM_Q))) - { - int16_t zeta = zetas[k++]; - ntt_butterfly_block(r, zeta, start, len, layer * MLKEM_Q); - } -} - -/* - * Compute full forward NTT - * NOTE: This particular implementation satisfies a much tighter - * bound on the output coefficients (5*q) than the contractual one (8*q), - * but this is not needed in the calling code. Should we change the - * base multiplication strategy to require smaller NTT output bounds, - * the proof may need strengthening. - */ - -MLKEM_NATIVE_INTERNAL_API -void poly_ntt(poly *p) -{ - unsigned len, layer; - int16_t *r; - debug_assert_abs_bound(p, MLKEM_N, MLKEM_Q); - r = p->coeffs; - - for (len = 128, layer = 1; len >= 2; len >>= 1, layer++) - __loop__( - invariant(1 <= layer && layer <= 8 && len == (MLKEM_N >> layer)) - invariant(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q))) - { - ntt_layer(r, len, layer); - } - - /* Check the stronger bound */ - debug_assert_abs_bound(p, MLKEM_N, NTT_BOUND); -} -#else /* MLKEM_USE_NATIVE_NTT */ - -MLKEM_NATIVE_INTERNAL_API -void poly_ntt(poly *p) -{ - debug_assert_abs_bound(p, MLKEM_N, MLKEM_Q); - ntt_native(p); - debug_assert_abs_bound(p, MLKEM_N, NTT_BOUND); -} -#endif /* MLKEM_USE_NATIVE_NTT */ - -#if !defined(MLKEM_USE_NATIVE_INTT) - -/* Compute one layer of inverse NTT */ -static void invntt_layer(int16_t *r, unsigned len, unsigned layer) -__contract__( - requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) - requires(2 <= len && len <= 128 && 1 <= layer && layer <= 7) - requires(len == (1 << (8 - layer))) - requires(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)) - assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) - ensures(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))) -{ - unsigned start, k; - /* `layer` is a ghost variable used only in the specification */ - ((void)layer); - k = MLKEM_N / len - 1; - for (start = 0; start < MLKEM_N; start += 2 * len) - __loop__( - invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)) - invariant(start <= MLKEM_N && k <= 127) - /* Normalised form of k == MLKEM_N / len - 1 - start / (2 * len) */ - invariant(2 * len * k + start == 2 * MLKEM_N - 2 * len)) - { - unsigned j; - int16_t zeta = zetas[k--]; - for (j = start; j < start + len; j++) - __loop__( - invariant(start <= j && j <= start + len) - invariant(start <= MLKEM_N && k <= 127) - invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))) - { - int16_t t = r[j]; - r[j] = barrett_reduce(t + r[j + len]); - r[j + len] = r[j + len] - t; - r[j + len] = fqmul(r[j + len], zeta); - } - } -} - -MLKEM_NATIVE_INTERNAL_API -void poly_invntt_tomont(poly *p) -{ - /* - * Scale input polynomial to account for Montgomery factor - * and NTT twist. This also brings coefficients down to - * absolute value < MLKEM_Q. - */ - unsigned j, len, layer; - const int16_t f = 1441; - int16_t *r = p->coeffs; - - for (j = 0; j < MLKEM_N; j++) - __loop__( - invariant(j <= MLKEM_N) - invariant(array_abs_bound(r, 0, j, MLKEM_Q))) - { - r[j] = fqmul(r[j], f); - } - - /* Run the invNTT layers */ - for (len = 2, layer = 7; len <= 128; len <<= 1, layer--) - __loop__( - invariant(2 <= len && len <= 256 && layer <= 7 && len == (1 << (8 - layer))) - invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))) - { - invntt_layer(p->coeffs, len, layer); - } - - debug_assert_abs_bound(p, MLKEM_N, INVNTT_BOUND); -} -#else /* MLKEM_USE_NATIVE_INTT */ - -MLKEM_NATIVE_INTERNAL_API -void poly_invntt_tomont(poly *p) -{ - intt_native(p); - debug_assert_abs_bound(p, MLKEM_N, INVNTT_BOUND); -} -#endif /* MLKEM_USE_NATIVE_INTT */ - -MLKEM_NATIVE_INTERNAL_API -void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2], - int16_t b_cached) -{ - int32_t t0, t1; - debug_assert_bound(a, 2, 0, UINT12_LIMIT); - - t0 = (int32_t)a[1] * b_cached; - t0 += (int32_t)a[0] * b[0]; - t1 = (int32_t)a[0] * b[1]; - t1 += (int32_t)a[1] * b[0]; - - /* |ti| < 2 * q * 2^15 */ - r[0] = montgomery_reduce(t0); - r[1] = montgomery_reduce(t1); - - debug_assert_abs_bound(r, 2, 2 * MLKEM_Q); -} - -#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ - -#define empty_cu_ntt MLKEM_NAMESPACE_K(empty_cu_ntt) -int empty_cu_ntt; - -#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/ntt.h b/mlkem/ntt.h deleted file mode 100644 index 4e80d3ab3..000000000 --- a/mlkem/ntt.h +++ /dev/null @@ -1,102 +0,0 @@ -/* - * Copyright (c) 2024 The mlkem-native project authors - * SPDX-License-Identifier: Apache-2.0 - */ -#ifndef NTT_H -#define NTT_H -#include "common.h" - -#include -#include "cbmc.h" -#include "poly.h" -#include "reduce.h" - -#define zetas MLKEM_NAMESPACE(zetas) -extern const int16_t zetas[128]; - -#define poly_ntt MLKEM_NAMESPACE(poly_ntt) -/************************************************* - * Name: poly_ntt - * - * Description: Computes negacyclic number-theoretic transform (NTT) of - * a polynomial in place. - * - * The input is assumed to be in normal order and - * coefficient-wise bound by MLKEM_Q in absolute value. - * - * The output polynomial is in bitreversed order, and - * coefficient-wise bound by NTT_BOUND in absolute value. - * - * (NOTE: Sometimes the input to the NTT is actually smaller, - * which gives better bounds.) - * - * Arguments: - poly *p: pointer to in/output polynomial - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_ntt(poly *r) -__contract__( - requires(memory_no_alias(r, sizeof(poly))) - requires(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_Q)) - assigns(memory_slice(r, sizeof(poly))) - ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, NTT_BOUND)) -); - -#define poly_invntt_tomont MLKEM_NAMESPACE(poly_invntt_tomont) -/************************************************* - * Name: poly_invntt_tomont - * - * Description: Computes inverse of negacyclic number-theoretic transform (NTT) - * of a polynomial in place; - * inputs assumed to be in bitreversed order, output in normal - * order - * - * The input is assumed to be in bitreversed order, and can - * have arbitrary coefficients in int16_t. - * - * The output polynomial is in normal order, and - * coefficient-wise bound by INVNTT_BOUND in absolute value. - * - * Arguments: - uint16_t *a: pointer to in/output polynomial - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_invntt_tomont(poly *r) -__contract__( - requires(memory_no_alias(r, sizeof(poly))) - assigns(memory_slice(r, sizeof(poly))) - ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INVNTT_BOUND)) -); - -#define basemul_cached MLKEM_NAMESPACE(basemul_cached) -/************************************************************ - * Name: basemul_cached - * - * Description: Computes a representative modulo q of - * (a0*b0 + a1*b_cached, a0*b1 + a1*b0)/65536 - * - * If b_cached is b1*zeta, this represents the - * product of (a0 + a1*X) and (b0 + b1*X) in - * Fq[X]/(X^2 - zeta). - * - * Arguments: - r: Pointer to output polynomial - * Upon return, coefficients are bound by - * 2*MLKEM_Q in absolute value. - * - a: Pointer to first input polynomial - * Every coefficient must be in [0..4095] - * - b: Pointer to second input polynomial - * Can have arbitrary int16_t coefficients - * - b_cached: Some precomputed value, typically derived from - * b1 and a twiddle factor. Can be an arbitary int16_t. - ************************************************************/ -MLKEM_NATIVE_INTERNAL_API -void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2], - int16_t b_cached) -__contract__( - requires(memory_no_alias(r, 2 * sizeof(int16_t))) - requires(memory_no_alias(a, 2 * sizeof(int16_t))) - requires(memory_no_alias(b, 2 * sizeof(int16_t))) - requires(array_bound(a, 0, 2, 0, UINT12_LIMIT)) - assigns(memory_slice(r, 2 * sizeof(int16_t))) - ensures(array_abs_bound(r, 0, 2, 2 * MLKEM_Q)) -); - -#endif /* NTT_H */ diff --git a/mlkem/params.h b/mlkem/params.h index 57ea4c8ba..7f6c12625 100644 --- a/mlkem/params.h +++ b/mlkem/params.h @@ -18,6 +18,7 @@ #define MLKEM_N 256 #define MLKEM_Q 3329 #define UINT12_LIMIT 4096 +#define HALF_Q ((MLKEM_Q + 1) / 2) /* 1665 */ #define MLKEM_SYMBYTES 32 /* size in bytes of hashes, and seeds */ #define MLKEM_SSBYTES 32 /* size in bytes of shared key */ diff --git a/mlkem/poly.c b/mlkem/poly.c index 26b358a25..14bbbb9f3 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -8,388 +8,246 @@ #include #include #include "arith_backend.h" -#include "cbd.h" #include "cbmc.h" #include "debug.h" #include "fips202/fips202x4.h" -#include "ntt.h" #include "poly.h" -#include "reduce.h" +#include "sampling.h" #include "symmetric.h" #include "verify.h" -#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || (MLKEM_K == 2 || MLKEM_K == 3) -MLKEM_NATIVE_INTERNAL_API -void poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const poly *a) -{ - unsigned i; - debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); - - for (i = 0; i < MLKEM_N / 8; i++) - __loop__(invariant(i <= MLKEM_N / 8)) - { - unsigned j; - uint8_t t[8] = {0}; - for (j = 0; j < 8; j++) - __loop__( - invariant(i <= MLKEM_N / 8 && j <= 8) - invariant(array_bound(t, 0, j, 0, 16))) - { - t[j] = scalar_compress_d4(a->coeffs[8 * i + j]); - } - - r[i * 4] = t[0] | (t[1] << 4); - r[i * 4 + 1] = t[2] | (t[3] << 4); - r[i * 4 + 2] = t[4] | (t[5] << 4); - r[i * 4 + 3] = t[6] | (t[7] << 4); - } -} - -MLKEM_NATIVE_INTERNAL_API -void poly_compress_d10(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], const poly *a) -{ - unsigned j; - debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); - for (j = 0; j < MLKEM_N / 4; j++) - __loop__(invariant(j <= MLKEM_N / 4)) - { - unsigned k; - uint16_t t[4]; - for (k = 0; k < 4; k++) - __loop__( - invariant(k <= 4) - invariant(forall(r, 0, k, t[r] < (1u << 10)))) - { - t[k] = scalar_compress_d10(a->coeffs[4 * j + k]); - } - - /* - * Make all implicit truncation explicit. No data is being - * truncated for the LHS's since each t[i] is 10-bit in size. - */ - r[5 * j + 0] = (t[0] >> 0) & 0xFF; - r[5 * j + 1] = (t[0] >> 8) | ((t[1] << 2) & 0xFF); - r[5 * j + 2] = (t[1] >> 6) | ((t[2] << 4) & 0xFF); - r[5 * j + 3] = (t[2] >> 4) | ((t[3] << 6) & 0xFF); - r[5 * j + 4] = (t[3] >> 2); - } -} - -MLKEM_NATIVE_INTERNAL_API -void poly_decompress_d4(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D4]) -{ - unsigned i; - for (i = 0; i < MLKEM_N / 2; i++) - __loop__( - invariant(i <= MLKEM_N / 2) - invariant(array_bound(r->coeffs, 0, 2 * i, 0, MLKEM_Q))) - { - r->coeffs[2 * i + 0] = scalar_decompress_d4((a[i] >> 0) & 0xF); - r->coeffs[2 * i + 1] = scalar_decompress_d4((a[i] >> 4) & 0xF); - } - - debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q); -} - -MLKEM_NATIVE_INTERNAL_API -void poly_decompress_d10(poly *r, - const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D10]) +/* Static namespacing + * This is to facilitate building multiple instances + * of mlkem-native (e.g. with varying security levels) + * within a single compilation unit. */ +#define cast_uint16_to_int16 MLKEM_NAMESPACE(cast_uint16_to_int16) +#define montgomery_reduce_generic MLKEM_NAMESPACE(montgomery_reduce_generic) +#define montgomery_reduce MLKEM_NAMESPACE(montgomery_reduce) +#define fqmul MLKEM_NAMESPACE(fqmul) +#define barrett_reduce MLKEM_NAMESPACE(barrett_reduce) +#define basemul_cached MLKEM_NAMESPACE(basemul_cached) +#define scalar_signed_to_unsigned_q MLKEM_NAMESPACE(scalar_signed_to_unsigned_q) +#define ntt_butterfly_block MLKEM_NAMESPACE(ntt_butterfly_block) +#define ntt_layer MLKEM_NAMESPACE(ntt_layer) +#define invntt_layer MLKEM_NAMESPACE(invntt_layer) +/* End of static namespacing */ + +/************************************************* + * Name: cast_uint16_to_int16 + * + * Description: Cast uint16 value to int16 + * + * Returns: + * input x in 0 .. 32767: returns value unchanged + * input x in 32768 .. 65535: returns (x - 65536) + **************************************************/ +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "conversion" +#endif +ALWAYS_INLINE +static INLINE int16_t cast_uint16_to_int16(uint16_t x) { - unsigned j; - for (j = 0; j < MLKEM_N / 4; j++) - __loop__( - invariant(j <= MLKEM_N / 4) - invariant(array_bound(r->coeffs, 0, 4 * j, 0, MLKEM_Q))) - { - unsigned k; - uint16_t t[4]; - uint8_t const *base = &a[5 * j]; - - t[0] = 0x3FF & ((base[0] >> 0) | ((uint16_t)base[1] << 8)); - t[1] = 0x3FF & ((base[1] >> 2) | ((uint16_t)base[2] << 6)); - t[2] = 0x3FF & ((base[2] >> 4) | ((uint16_t)base[3] << 4)); - t[3] = 0x3FF & ((base[3] >> 6) | ((uint16_t)base[4] << 2)); - - for (k = 0; k < 4; k++) - __loop__( - invariant(k <= 4) - invariant(array_bound(r->coeffs, 0, 4 * j + k, 0, MLKEM_Q))) - { - r->coeffs[4 * j + k] = scalar_decompress_d10(t[k]); - } - } - - debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q); + /* + * PORTABILITY: This relies on uint16_t -> int16_t + * being implemented as the inverse of int16_t -> uint16_t, + * which is implementation-defined (C99 6.3.1.3 (3)) + * CBMC (correctly) fails to prove this conversion is OK, + * so we have to suppress that check here + */ + return (int16_t)x; } -#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || (MLKEM_K == 2 \ - || MLKEM_K == 3) */ +#ifdef CBMC +#pragma CPROVER check pop +#endif -#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_K == 4 -MLKEM_NATIVE_INTERNAL_API -void poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const poly *a) +/************************************************* + * Name: montgomery_reduce_generic + * + * Description: Generic Montgomery reduction; given a 32-bit integer a, computes + * 16-bit integer congruent to a * R^-1 mod q, where R=2^16 + * + * Arguments: - int32_t a: input integer to be reduced + * + * Returns: integer congruent to a * R^-1 modulo q, with absolute value + * <= ceil(|a| / 2^16) + (MLKEM_Q + 1)/2 + * + **************************************************/ +ALWAYS_INLINE +static INLINE int16_t montgomery_reduce_generic(int32_t a) { - unsigned i; - debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + /* QINV == -3327 converted to uint16_t == -3327 + 65536 == 62209 */ + const uint32_t QINV = 62209; /* q^-1 mod 2^16 */ - for (i = 0; i < MLKEM_N / 8; i++) - __loop__(invariant(i <= MLKEM_N / 8)) - { - unsigned j; - uint8_t t[8] = {0}; - for (j = 0; j < 8; j++) - __loop__( - invariant(i <= MLKEM_N / 8 && j <= 8) - invariant(array_bound(t, 0, j, 0, 32))) - { - t[j] = scalar_compress_d5(a->coeffs[8 * i + j]); - } + /* Compute a*q^{-1} mod 2^16 in unsigned representatives */ + const uint16_t a_reduced = a & UINT16_MAX; + const uint16_t a_inverted = (a_reduced * QINV) & UINT16_MAX; - /* - * Explicitly truncate to avoid warning about - * implicit truncation in CBMC, and use array indexing into - * r rather than pointer-arithmetic to simplify verification - */ - r[i * 5] = 0xFF & ((t[0] >> 0) | (t[1] << 5)); - r[i * 5 + 1] = 0xFF & ((t[1] >> 3) | (t[2] << 2) | (t[3] << 7)); - r[i * 5 + 2] = 0xFF & ((t[3] >> 1) | (t[4] << 4)); - r[i * 5 + 3] = 0xFF & ((t[4] >> 4) | (t[5] << 1) | (t[6] << 6)); - r[i * 5 + 4] = 0xFF & ((t[6] >> 2) | (t[7] << 3)); - } -} + /* Lift to signed canonical representative mod 2^16. */ + const int16_t t = cast_uint16_to_int16(a_inverted); -MLKEM_NATIVE_INTERNAL_API -void poly_compress_d11(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const poly *a) -{ - unsigned j; - debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + int32_t r = a - ((int32_t)t * MLKEM_Q); + /* Bounds: |r| <= |a| + 2^15 * MLKEM_Q */ - for (j = 0; j < MLKEM_N / 8; j++) - __loop__(invariant(j <= MLKEM_N / 8)) - { - unsigned k; - uint16_t t[8]; - for (k = 0; k < 8; k++) - __loop__( - invariant(k <= 8) - invariant(forall(r, 0, k, t[r] < (1u << 11)))) - { - t[k] = scalar_compress_d11(a->coeffs[8 * j + k]); - } + /* + * PORTABILITY: Right-shift on a signed integer is, strictly-speaking, + * implementation-defined for negative left argument. Here, + * we assume it's sign-preserving "arithmetic" shift right. (C99 6.5.7 (5)) + */ + r = r >> 16; + /* Bounds: |r >> 16| <= ceil(|r| / 2^16) + * <= ceil(|a| / 2^16 + MLKEM_Q / 2) + * <= ceil(|a| / 2^16) + (MLKEM_Q + 1) / 2 + * + * (Note that |a >> n| = ceil(|a| / 2^16) for negative a) + */ - /* - * Make all implicit truncation explicit. No data is being - * truncated for the LHS's since each t[i] is 11-bit in size. - */ - r[11 * j + 0] = (t[0] >> 0) & 0xFF; - r[11 * j + 1] = (t[0] >> 8) | ((t[1] << 3) & 0xFF); - r[11 * j + 2] = (t[1] >> 5) | ((t[2] << 6) & 0xFF); - r[11 * j + 3] = (t[2] >> 2) & 0xFF; - r[11 * j + 4] = (t[2] >> 10) | ((t[3] << 1) & 0xFF); - r[11 * j + 5] = (t[3] >> 7) | ((t[4] << 4) & 0xFF); - r[11 * j + 6] = (t[4] >> 4) | ((t[5] << 7) & 0xFF); - r[11 * j + 7] = (t[5] >> 1) & 0xFF; - r[11 * j + 8] = (t[5] >> 9) | ((t[6] << 2) & 0xFF); - r[11 * j + 9] = (t[6] >> 6) | ((t[7] << 5) & 0xFF); - r[11 * j + 10] = (t[7] >> 3); - } + return (int16_t)r; } -MLKEM_NATIVE_INTERNAL_API -void poly_decompress_d5(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D5]) +/************************************************* + * Name: montgomery_reduce + * + * Description: Montgomery reduction + * + * Arguments: - int32_t a: input integer to be reduced + * Must be smaller than 2 * 2^12 * 2^15 in absolute value. + * + * Returns: integer congruent to a * R^-1 modulo q, + * smaller than 2 * q in absolute value. + **************************************************/ +static INLINE int16_t montgomery_reduce(int32_t a) +__contract__( + requires(a > -(2 * UINT12_LIMIT * 32768)) + requires(a < (2 * UINT12_LIMIT * 32768)) + ensures(return_value > -2 * MLKEM_Q && return_value < 2 * MLKEM_Q) +) { - unsigned i; - for (i = 0; i < MLKEM_N / 8; i++) - __loop__( - invariant(i <= MLKEM_N / 8) - invariant(array_bound(r->coeffs, 0, 8 * i, 0, MLKEM_Q))) - { - unsigned j; - uint8_t t[8]; - const unsigned offset = i * 5; - /* - * Explicitly truncate to avoid warning about - * implicit truncation in CBMC and unwind loop for ease - * of proof. - */ - - /* - * Decompress 5 8-bit bytes (so 40 bits) into - * 8 5-bit values stored in t[] - */ - t[0] = 0x1F & (a[offset + 0] >> 0); - t[1] = 0x1F & ((a[offset + 0] >> 5) | (a[offset + 1] << 3)); - t[2] = 0x1F & (a[offset + 1] >> 2); - t[3] = 0x1F & ((a[offset + 1] >> 7) | (a[offset + 2] << 1)); - t[4] = 0x1F & ((a[offset + 2] >> 4) | (a[offset + 3] << 4)); - t[5] = 0x1F & (a[offset + 3] >> 1); - t[6] = 0x1F & ((a[offset + 3] >> 6) | (a[offset + 4] << 2)); - t[7] = 0x1F & (a[offset + 4] >> 3); - - /* and copy to the correct slice in r[] */ - for (j = 0; j < 8; j++) - __loop__( - invariant(j <= 8 && i <= MLKEM_N / 8) - invariant(array_bound(r->coeffs, 0, 8 * i + j, 0, MLKEM_Q))) - { - r->coeffs[8 * i + j] = scalar_decompress_d5(t[j]); - } - } - - debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q); + int16_t res; + debug_assert_abs_bound(&a, 1, 2 * UINT12_LIMIT * 32768); + + res = montgomery_reduce_generic(a); + /* Bounds: + * |res| <= ceil(|a| / 2^16) + (MLKEM_Q + 1) / 2 + * <= ceil(2 * UINT12_LIMIT * 32768 / 65536) + (MLKEM_Q + 1) / 2 + * <= UINT12_LIMIT + (MLKEM_Q + 1) / 2 + * < 2 * MLKEM_Q */ + + debug_assert_abs_bound(&res, 1, 2 * MLKEM_Q); + return res; } -MLKEM_NATIVE_INTERNAL_API -void poly_decompress_d11(poly *r, - const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D11]) +#if !defined(MLKEM_USE_NATIVE_POLY_TOMONT) || \ + !defined(MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE) || \ + !defined(MLKEM_USE_NATIVE_NTT) || !defined(MLKEM_USE_NATIVE_INTT) +/************************************************* + * Name: fqmul + * + * Description: Montgomery multiplication modulo q=3329 + * + * Arguments: - int16_t a: first factor + * Can be any int16_t. + * - int16_t b: second factor. + * Must be signed canonical (abs value <(q+1)/2) + * + * Returns 16-bit integer congruent to a*b*R^{-1} mod q, and + * smaller than q in absolute value. + * + **************************************************/ +static INLINE int16_t fqmul(int16_t a, int16_t b) +__contract__( + requires(b > -HALF_Q) + requires(b < HALF_Q) + ensures(return_value > -MLKEM_Q && return_value < MLKEM_Q) +) { - unsigned j; - for (j = 0; j < MLKEM_N / 8; j++) - __loop__( - invariant(j <= MLKEM_N / 8) - invariant(array_bound(r->coeffs, 0, 8 * j, 0, MLKEM_Q))) - { - unsigned k; - uint16_t t[8]; - uint8_t const *base = &a[11 * j]; - t[0] = 0x7FF & ((base[0] >> 0) | ((uint16_t)base[1] << 8)); - t[1] = 0x7FF & ((base[1] >> 3) | ((uint16_t)base[2] << 5)); - t[2] = 0x7FF & ((base[2] >> 6) | ((uint16_t)base[3] << 2) | - ((uint16_t)base[4] << 10)); - t[3] = 0x7FF & ((base[4] >> 1) | ((uint16_t)base[5] << 7)); - t[4] = 0x7FF & ((base[5] >> 4) | ((uint16_t)base[6] << 4)); - t[5] = 0x7FF & ((base[6] >> 7) | ((uint16_t)base[7] << 1) | - ((uint16_t)base[8] << 9)); - t[6] = 0x7FF & ((base[8] >> 2) | ((uint16_t)base[9] << 6)); - t[7] = 0x7FF & ((base[9] >> 5) | ((uint16_t)base[10] << 3)); - - for (k = 0; k < 8; k++) - __loop__( - invariant(k <= 8) - invariant(array_bound(r->coeffs, 0, 8 * j + k, 0, MLKEM_Q))) - { - r->coeffs[8 * j + k] = scalar_decompress_d11(t[k]); - } - } + int16_t res; + debug_assert_abs_bound(&b, 1, HALF_Q); + + res = montgomery_reduce((int32_t)a * (int32_t)b); + /* Bounds: + * |res| <= ceil(|a| * |b| / 2^16) + (MLKEM_Q + 1) / 2 + * <= ceil(2^15 * ((MLKEM_Q - 1)/2) / 2^16) + (MLKEM_Q + 1) / 2 + * <= ceil((MLKEM_Q - 1) / 4) + (MLKEM_Q + 1) / 2 + * < MLKEM_Q + */ - debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q); + debug_assert_abs_bound(&res, 1, MLKEM_Q); + return res; } -#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD) || MLKEM_K == 4 */ - -#if !defined(MLKEM_USE_NATIVE_POLY_TOBYTES) -MLKEM_NATIVE_INTERNAL_API -void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a) +#endif /* !defined(MLKEM_USE_NATIVE_POLY_TOMONT) || \ + !defined(MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE) || \ + !defined(MLKEM_USE_NATIVE_NTT) || \ + !defined(MLKEM_USE_NATIVE_INTT) */ + +#if !defined(MLKEM_USE_NATIVE_POLY_REDUCE) || !defined(MLKEM_USE_NATIVE_INTT) +/************************************************* + * Name: barrett_reduce + * + * Description: Barrett reduction; given a 16-bit integer a, computes + * centered representative congruent to a mod q in + * {-(q-1)/2,...,(q-1)/2} + * + * Arguments: - int16_t a: input integer to be reduced + * + * Returns: integer in {-(q-1)/2,...,(q-1)/2} congruent to a modulo q. + **************************************************/ +static INLINE int16_t barrett_reduce(int16_t a) +__contract__( + ensures(return_value > -HALF_Q && return_value < HALF_Q) +) { - unsigned i; - debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); - - for (i = 0; i < MLKEM_N / 2; i++) - __loop__(invariant(i <= MLKEM_N / 2)) - { - const uint16_t t0 = a->coeffs[2 * i]; - const uint16_t t1 = a->coeffs[2 * i + 1]; - /* - * t0 and t1 are both < MLKEM_Q, so contain at most 12 bits each of - * significant data, so these can be packed into 24 bits or exactly - * 3 bytes, as follows. - */ - - /* Least significant bits 0 - 7 of t0. */ - r[3 * i + 0] = t0 & 0xFF; - - /* - * Most significant bits 8 - 11 of t0 become the least significant - * nibble of the second byte. The least significant 4 bits - * of t1 become the upper nibble of the second byte. - */ - r[3 * i + 1] = (t0 >> 8) | ((t1 << 4) & 0xF0); + /* + * To divide by MLKEM_Q using Barrett multiplication, the "magic number" + * multiplier is round_to_nearest(2**26/MLKEM_Q) + */ + const int BPOWER = 26; + const int32_t barrett_multiplier = ((1 << BPOWER) + MLKEM_Q / 2) / MLKEM_Q; - /* Bits 4 - 11 of t1 become the third byte. */ - r[3 * i + 2] = t1 >> 4; - } -} -#else /* MLKEM_USE_NATIVE_POLY_TOBYTES */ -MLKEM_NATIVE_INTERNAL_API -void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a) -{ - debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); - poly_tobytes_native(r, a); -} -#endif /* MLKEM_USE_NATIVE_POLY_TOBYTES */ + /* + * Compute round_to_nearest(a/MLKEM_Q) using the multiplier + * above and shift by BPOWER places. + * PORTABILITY: Right-shift on a signed integer is, strictly-speaking, + * implementation-defined for negative left argument. Here, + * we assume it's sign-preserving "arithmetic" shift right. (C99 6.5.7 (5)) + */ + const int32_t t = (barrett_multiplier * a + (1 << (BPOWER - 1))) >> BPOWER; -#if !defined(MLKEM_USE_NATIVE_POLY_FROMBYTES) -MLKEM_NATIVE_INTERNAL_API -void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES]) -{ - unsigned i; - for (i = 0; i < MLKEM_N / 2; i++) - __loop__( - invariant(i <= MLKEM_N / 2) - invariant(array_bound(r->coeffs, 0, 2 * i, 0, UINT12_LIMIT))) - { - const uint8_t t0 = a[3 * i + 0]; - const uint8_t t1 = a[3 * i + 1]; - const uint8_t t2 = a[3 * i + 2]; - r->coeffs[2 * i + 0] = t0 | ((t1 << 8) & 0xFFF); - r->coeffs[2 * i + 1] = (t1 >> 4) | (t2 << 4); - } + /* + * t is in -10 .. +10, so we need 32-bit math to + * evaluate t * MLKEM_Q and the subsequent subtraction + */ + int16_t res = (int16_t)(a - t * MLKEM_Q); - /* Note that the coefficients are not canonical */ - debug_assert_bound(r, MLKEM_N, 0, UINT12_LIMIT); -} -#else /* MLKEM_USE_NATIVE_POLY_FROMBYTES */ -MLKEM_NATIVE_INTERNAL_API -void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES]) -{ - poly_frombytes_native(r, a); + debug_assert_abs_bound(&res, 1, HALF_Q); + return res; } -#endif /* MLKEM_USE_NATIVE_POLY_FROMBYTES */ - -MLKEM_NATIVE_INTERNAL_API -void poly_frommsg(poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES]) +#endif /* !defined(MLKEM_USE_NATIVE_POLY_REDUCE) || \ + !defined(MLKEM_USE_NATIVE_INTT) */ + +static void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2], + int16_t b_cached) +__contract__( + requires(memory_no_alias(r, 2 * sizeof(int16_t))) + requires(memory_no_alias(a, 2 * sizeof(int16_t))) + requires(memory_no_alias(b, 2 * sizeof(int16_t))) + requires(array_bound(a, 0, 2, 0, UINT12_LIMIT)) + assigns(memory_slice(r, 2 * sizeof(int16_t))) + ensures(array_abs_bound(r, 0, 2, 2 * MLKEM_Q))) { - unsigned i; -#if (MLKEM_INDCPA_MSGBYTES != MLKEM_N / 8) -#error "MLKEM_INDCPA_MSGBYTES must be equal to MLKEM_N/8 bytes!" -#endif + int32_t t0, t1; + debug_assert_bound(a, 2, 0, UINT12_LIMIT); - for (i = 0; i < MLKEM_N / 8; i++) - __loop__( - invariant(i <= MLKEM_N / 8) - invariant(array_bound(r->coeffs, 0, 8 * i, 0, MLKEM_Q))) - { - unsigned j; - for (j = 0; j < 8; j++) - __loop__( - invariant(i < MLKEM_N / 8 && j <= 8) - invariant(array_bound(r->coeffs, 0, 8 * i + j, 0, MLKEM_Q))) - { - /* Prevent the compiler from recognizing this as a bit selection */ - uint8_t mask = value_barrier_u8(1u << j); - r->coeffs[8 * i + j] = ct_sel_int16(HALF_Q, 0, msg[i] & mask); - } - } - debug_assert_abs_bound(r, MLKEM_N, MLKEM_Q); -} + t0 = (int32_t)a[1] * b_cached; + t0 += (int32_t)a[0] * b[0]; + t1 = (int32_t)a[0] * b[1]; + t1 += (int32_t)a[1] * b[0]; -MLKEM_NATIVE_INTERNAL_API -void poly_tomsg(uint8_t msg[MLKEM_INDCPA_MSGBYTES], const poly *a) -{ - unsigned i; - debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); + /* |ti| < 2 * q * 2^15 */ + r[0] = montgomery_reduce(t0); + r[1] = montgomery_reduce(t1); - for (i = 0; i < MLKEM_N / 8; i++) - __loop__(invariant(i <= MLKEM_N / 8)) - { - unsigned j; - msg[i] = 0; - for (j = 0; j < 8; j++) - __loop__( - invariant(i <= MLKEM_N / 8 && j <= 8)) - { - uint32_t t = scalar_compress_d1(a->coeffs[8 * i + j]); - msg[i] |= t << j; - } - } + debug_assert_abs_bound(r, 2, 2 * MLKEM_Q); } MLKEM_NATIVE_INTERNAL_API @@ -440,6 +298,40 @@ void poly_tomont(poly *r) #endif /* MLKEM_USE_NATIVE_POLY_TOMONT */ #if !defined(MLKEM_USE_NATIVE_POLY_REDUCE) +/************************************************************ + * Name: scalar_signed_to_unsigned_q + * + * Description: converts signed polynomial coefficient + * from signed (-3328 .. 3328) form to + * unsigned form (0 .. 3328). + * + * Note: Cryptographic constant time implementation + * + * Examples: 0 -> 0 + * 1 -> 1 + * 3328 -> 3328 + * -1 -> 3328 + * -2 -> 3327 + * -3328 -> 1 + * + * Arguments: c: signed coefficient to be converted + ************************************************************/ +static INLINE uint16_t scalar_signed_to_unsigned_q(int16_t c) +__contract__( + requires(c > -MLKEM_Q && c < MLKEM_Q) + ensures(return_value >= 0 && return_value < MLKEM_Q) + ensures(return_value == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q))) +{ + debug_assert_abs_bound(&c, 1, MLKEM_Q); + + /* Add Q if c is negative, but in constant time */ + c = ct_sel_int16(c + MLKEM_Q, c, ct_cmask_neg_i16(c)); + + /* and therefore cast to uint16_t is safe. */ + debug_assert_bound(&c, 1, 0, MLKEM_Q); + return (uint16_t)c; +} + MLKEM_NATIVE_INTERNAL_API void poly_reduce(poly *r) { @@ -527,6 +419,225 @@ void poly_mulcache_compute(poly_mulcache *x, const poly *a) } #endif /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */ +#if !defined(MLKEM_USE_NATIVE_NTT) +/* + * Computes a block CT butterflies with a fixed twiddle factor, + * using Montgomery multiplication. + * Parameters: + * - r: Pointer to base of polynomial (_not_ the base of butterfly block) + * - root: Twiddle factor to use for the butterfly. This must be in + * Montgomery form and signed canonical. + * - start: Offset to the beginning of the butterfly block + * - len: Index difference between coefficients subject to a butterfly + * - bound: Ghost variable describing coefficient bound: Prior to `start`, + * coefficients must be bound by `bound + MLKEM_Q`. Post `start`, + * they must be bound by `bound`. + * When this function returns, output coefficients in the index range + * [start, start+2*len) have bound bumped to `bound + MLKEM_Q`. + * Example: + * - start=8, len=4 + * This would compute the following four butterflies + * 8 -- 12 + * 9 -- 13 + * 10 -- 14 + * 11 -- 15 + * - start=4, len=2 + * This would compute the following two butterflies + * 4 -- 6 + * 5 -- 7 + */ +static void ntt_butterfly_block(int16_t r[MLKEM_N], int16_t zeta, + unsigned start, unsigned len, int bound) +__contract__( + requires(start < MLKEM_N) + requires(1 <= len && len <= MLKEM_N / 2 && start + 2 * len <= MLKEM_N) + requires(0 <= bound && bound < INT16_MAX - MLKEM_Q) + requires(-HALF_Q < zeta && zeta < HALF_Q) + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(array_abs_bound(r, 0, start, bound + MLKEM_Q)) + requires(array_abs_bound(r, start, MLKEM_N, bound)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, start + 2*len, bound + MLKEM_Q)) + ensures(array_abs_bound(r, start + 2 * len, MLKEM_N, bound))) +{ + /* `bound` is a ghost variable only needed in the CBMC specification */ + unsigned j; + ((void)bound); + for (j = start; j < start + len; j++) + __loop__( + invariant(start <= j && j <= start + len) + /* + * Coefficients are updated in strided pairs, so the bounds for the + * intermediate states alternate twice between the old and new bound + */ + invariant(array_abs_bound(r, 0, j, bound + MLKEM_Q)) + invariant(array_abs_bound(r, j, start + len, bound)) + invariant(array_abs_bound(r, start + len, j + len, bound + MLKEM_Q)) + invariant(array_abs_bound(r, j + len, MLKEM_N, bound))) + { + int16_t t; + t = fqmul(r[j + len], zeta); + r[j + len] = r[j] - t; + r[j] = r[j] + t; + } +} + +/* + *Compute one layer of forward NTT + * Parameters: + * - r: Pointer to base of polynomial + * - len: Stride of butterflies in this layer. + * - layer: Ghost variable indicating which layer is being applied. + * Must match `len` via `len == MLKEM_N >> layer`. + * Note: `len` could be dropped and computed in the function, but + * we are following the structure of the reference NTT from the + * official Kyber implementation here, merely adding `layer` as + * a ghost variable for the specifications. + */ +static void ntt_layer(int16_t r[MLKEM_N], unsigned len, unsigned layer) +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(1 <= layer && layer <= 7 && len == (MLKEM_N >> layer)) + requires(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, (layer + 1) * MLKEM_Q))) +{ + unsigned start, k; + /* `layer` is a ghost variable only needed in the CBMC specification */ + ((void)layer); + /* Twiddle factors for layer n start at index 2^(layer-1) */ + k = MLKEM_N / (2 * len); + for (start = 0; start < MLKEM_N; start += 2 * len) + __loop__( + invariant(start < MLKEM_N + 2 * len) + invariant(k <= MLKEM_N / 2 && 2 * len * k == start + MLKEM_N) + invariant(array_abs_bound(r, 0, start, layer * MLKEM_Q + MLKEM_Q)) + invariant(array_abs_bound(r, start, MLKEM_N, layer * MLKEM_Q))) + { + int16_t zeta = zetas[k++]; + ntt_butterfly_block(r, zeta, start, len, layer * MLKEM_Q); + } +} + +/* + * Compute full forward NTT + * NOTE: This particular implementation satisfies a much tighter + * bound on the output coefficients (5*q) than the contractual one (8*q), + * but this is not needed in the calling code. Should we change the + * base multiplication strategy to require smaller NTT output bounds, + * the proof may need strengthening. + */ + +MLKEM_NATIVE_INTERNAL_API +void poly_ntt(poly *p) +{ + unsigned len, layer; + int16_t *r; + debug_assert_abs_bound(p, MLKEM_N, MLKEM_Q); + r = p->coeffs; + + for (len = 128, layer = 1; len >= 2; len >>= 1, layer++) + __loop__( + invariant(1 <= layer && layer <= 8 && len == (MLKEM_N >> layer)) + invariant(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q))) + { + ntt_layer(r, len, layer); + } + + /* Check the stronger bound */ + debug_assert_abs_bound(p, MLKEM_N, NTT_BOUND); +} +#else /* MLKEM_USE_NATIVE_NTT */ + +MLKEM_NATIVE_INTERNAL_API +void poly_ntt(poly *p) +{ + debug_assert_abs_bound(p, MLKEM_N, MLKEM_Q); + ntt_native(p); + debug_assert_abs_bound(p, MLKEM_N, NTT_BOUND); +} +#endif /* MLKEM_USE_NATIVE_NTT */ + +#if !defined(MLKEM_USE_NATIVE_INTT) + +/* Compute one layer of inverse NTT */ +static void invntt_layer(int16_t *r, unsigned len, unsigned layer) +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(2 <= len && len <= 128 && 1 <= layer && layer <= 7) + requires(len == (1 << (8 - layer))) + requires(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))) +{ + unsigned start, k; + /* `layer` is a ghost variable used only in the specification */ + ((void)layer); + k = MLKEM_N / len - 1; + for (start = 0; start < MLKEM_N; start += 2 * len) + __loop__( + invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q)) + invariant(start <= MLKEM_N && k <= 127) + /* Normalised form of k == MLKEM_N / len - 1 - start / (2 * len) */ + invariant(2 * len * k + start == 2 * MLKEM_N - 2 * len)) + { + unsigned j; + int16_t zeta = zetas[k--]; + for (j = start; j < start + len; j++) + __loop__( + invariant(start <= j && j <= start + len) + invariant(start <= MLKEM_N && k <= 127) + invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))) + { + int16_t t = r[j]; + r[j] = barrett_reduce(t + r[j + len]); + r[j + len] = r[j + len] - t; + r[j + len] = fqmul(r[j + len], zeta); + } + } +} + +MLKEM_NATIVE_INTERNAL_API +void poly_invntt_tomont(poly *p) +{ + /* + * Scale input polynomial to account for Montgomery factor + * and NTT twist. This also brings coefficients down to + * absolute value < MLKEM_Q. + */ + unsigned j, len, layer; + const int16_t f = 1441; + int16_t *r = p->coeffs; + + for (j = 0; j < MLKEM_N; j++) + __loop__( + invariant(j <= MLKEM_N) + invariant(array_abs_bound(r, 0, j, MLKEM_Q))) + { + r[j] = fqmul(r[j], f); + } + + /* Run the invNTT layers */ + for (len = 2, layer = 7; len <= 128; len <<= 1, layer--) + __loop__( + invariant(2 <= len && len <= 256 && layer <= 7 && len == (1 << (8 - layer))) + invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))) + { + invntt_layer(p->coeffs, len, layer); + } + + debug_assert_abs_bound(p, MLKEM_N, INVNTT_BOUND); +} +#else /* MLKEM_USE_NATIVE_INTT */ + +MLKEM_NATIVE_INTERNAL_API +void poly_invntt_tomont(poly *p) +{ + intt_native(p); + debug_assert_abs_bound(p, MLKEM_N, INVNTT_BOUND); +} +#endif /* MLKEM_USE_NATIVE_INTT */ + #else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ #define empty_cu_poly MLKEM_NAMESPACE_K(empty_cu_poly) diff --git a/mlkem/poly.h b/mlkem/poly.h index 6a14c785d..cb0d67c1a 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -9,7 +9,7 @@ #include #include "cbmc.h" #include "common.h" -#include "reduce.h" +#include "debug.h" #include "verify.h" /* Absolute exclusive upper bound for the output of the inverse NTT */ @@ -18,6 +18,9 @@ /* Absolute exclusive upper bound for the output of the forward NTT */ #define NTT_BOUND (8 * MLKEM_Q) +#define zetas MLKEM_NAMESPACE(zetas) +extern const int16_t zetas[128]; + /* * Elements of R_q = Z_q[X]/(X^n + 1). Represents polynomial * coeffs[0] + X*coeffs[1] + X^2*coeffs[2] + ... + X^{n-1}*coeffs[n-1] @@ -38,520 +41,6 @@ typedef struct int16_t coeffs[MLKEM_N >> 1]; } poly_mulcache; -/* Static namespacing - * This is to facilitate building multiple instances - * of mlkem-native (e.g. with varying security levels) - * within a single compilation unit. */ -#define scalar_compress_d1 MLKEM_NAMESPACE(scalar_compress_d1) -#define scalar_compress_d4 MLKEM_NAMESPACE(scalar_compress_d4) -#define scalar_compress_d5 MLKEM_NAMESPACE(scalar_compress_d5) -#define scalar_compress_d10 MLKEM_NAMESPACE(scalar_compress_d10) -#define scalar_compress_d11 MLKEM_NAMESPACE(scalar_compress_d11) -#define scalar_decompress_d4 MLKEM_NAMESPACE(scalar_decompress_d4) -#define scalar_decompress_d5 MLKEM_NAMESPACE(scalar_decompress_d5) -#define scalar_decompress_d10 MLKEM_NAMESPACE(scalar_decompress_d10) -#define scalar_decompress_d11 MLKEM_NAMESPACE(scalar_decompress_d11) -#define scalar_signed_to_unsigned_q MLKEM_NAMESPACE(scalar_signed_to_unsigned_q) -/* End of static namespacing */ - -/************************************************************ - * Name: scalar_compress_d1 - * - * Description: Computes round(u * 2 / q) - * - * Implements Compress_d from FIPS203, Eq (4.7), - * for d = 1. - * - * Arguments: - u: Unsigned canonical modulus modulo q - * to be compressed. - ************************************************************/ -/* - * The multiplication in this routine will exceed UINT32_MAX - * and wrap around for large values of u. This is expected and required. - */ -#ifdef CBMC -#pragma CPROVER check push -#pragma CPROVER check disable "unsigned-overflow" -#endif -static INLINE uint32_t scalar_compress_d1(uint16_t u) -__contract__( - requires(u <= MLKEM_Q - 1) - ensures(return_value < 2) - ensures(return_value == (((uint32_t)u * 2 + MLKEM_Q / 2) / MLKEM_Q) % 2) ) -{ - uint32_t d0 = u << 1; - d0 *= 645083; - d0 += 1u << 30; - d0 >>= 31; - return d0; -} -#ifdef CBMC -#pragma CPROVER check pop -#endif - -/************************************************************ - * Name: scalar_compress_d4 - * - * Description: Computes round(u * 16 / q) % 16 - * - * Implements Compress_d from FIPS203, Eq (4.7), - * for d = 4. - * - * Arguments: - u: Unsigned canonical modulus modulo q - * to be compressed. - ************************************************************/ -/* - * The multiplication in this routine will exceed UINT32_MAX - * and wrap around for large values of u. This is expected and required. - */ -#ifdef CBMC -#pragma CPROVER check push -#pragma CPROVER check disable "unsigned-overflow" -#endif -static INLINE uint32_t scalar_compress_d4(uint16_t u) -__contract__( - requires(u <= MLKEM_Q - 1) - ensures(return_value < 16) - ensures(return_value == (((uint32_t)u * 16 + MLKEM_Q / 2) / MLKEM_Q) % 16)) -{ - uint32_t d0 = (uint32_t)u * 1290160; /* 16 * round(2^28 / MLKEM_Q) */ - return (d0 + (1u << 27)) >> 28; /* round(d0/2^28) */ -} -#ifdef CBMC -#pragma CPROVER check pop -#endif - -/************************************************************ - * Name: scalar_decompress_d4 - * - * Description: Computes round(u * q / 16) - * - * Implements Decompress_d from FIPS203, Eq (4.8), - * for d = 4. - * - * Arguments: - u: Unsigned canonical modulus modulo 16 - * to be decompressed. - ************************************************************/ -static INLINE uint16_t scalar_decompress_d4(uint32_t u) -__contract__( - requires(0 <= u && u < 16) - ensures(return_value <= (MLKEM_Q - 1)) -) { return ((u * MLKEM_Q) + 8) / 16; } - -/************************************************************ - * Name: scalar_compress_d5 - * - * Description: Computes round(u * 32 / q) % 32 - * - * Implements Compress_d from FIPS203, Eq (4.7), - * for d = 5. - * - * Arguments: - u: Unsigned canonical modulus modulo q - * to be compressed. - ************************************************************/ -/* - * The multiplication in this routine will exceed UINT32_MAX - * and wrap around for large values of u. This is expected and required. - */ -#ifdef CBMC -#pragma CPROVER check push -#pragma CPROVER check disable "unsigned-overflow" -#endif -static INLINE uint32_t scalar_compress_d5(uint16_t u) -__contract__( - requires(u <= MLKEM_Q - 1) - ensures(return_value < 32) - ensures(return_value == (((uint32_t)u * 32 + MLKEM_Q / 2) / MLKEM_Q) % 32) ) -{ - uint32_t d0 = (uint32_t)u * 1290176; /* 2^5 * round(2^27 / MLKEM_Q) */ - return (d0 + (1u << 26)) >> 27; /* round(d0/2^27) */ -} -#ifdef CBMC -#pragma CPROVER check pop -#endif - -/************************************************************ - * Name: scalar_decompress_d5 - * - * Description: Computes round(u * q / 32) - * - * Implements Decompress_d from FIPS203, Eq (4.8), - * for d = 5. - * - * Arguments: - u: Unsigned canonical modulus modulo 32 - * to be decompressed. - ************************************************************/ -static INLINE uint16_t scalar_decompress_d5(uint32_t u) -__contract__( - requires(0 <= u && u < 32) - ensures(return_value <= MLKEM_Q - 1) -) { return ((u * MLKEM_Q) + 16) / 32; } - -/************************************************************ - * Name: scalar_compress_d10 - * - * Description: Computes round(u * 2**10 / q) % 2**10 - * - * Implements Compress_d from FIPS203, Eq (4.7), - * for d = 10. - * - * Arguments: - u: Unsigned canonical modulus modulo q - * to be compressed. - ************************************************************/ -/* - * The multiplication in this routine will exceed UINT32_MAX - * and wrap around for large values of u. This is expected and required. - */ -#ifdef CBMC -#pragma CPROVER check push -#pragma CPROVER check disable "unsigned-overflow" -#endif -static INLINE uint32_t scalar_compress_d10(uint16_t u) -__contract__( - requires(u <= MLKEM_Q - 1) - ensures(return_value < (1u << 10)) - ensures(return_value == (((uint32_t)u * (1u << 10) + MLKEM_Q / 2) / MLKEM_Q) % (1 << 10))) -{ - uint64_t d0 = (uint64_t)u * 2642263040; /* 2^10 * round(2^32 / MLKEM_Q) */ - d0 = (d0 + ((uint64_t)1u << 32)) >> 33; - return (d0 & 0x3FF); -} -#ifdef CBMC -#pragma CPROVER check pop -#endif - -/************************************************************ - * Name: scalar_decompress_d10 - * - * Description: Computes round(u * q / 1024) - * - * Implements Decompress_d from FIPS203, Eq (4.8), - * for d = 10. - * - * Arguments: - u: Unsigned canonical modulus modulo 16 - * to be decompressed. - ************************************************************/ -static INLINE uint16_t scalar_decompress_d10(uint32_t u) -__contract__( - requires(0 <= u && u < 1024) - ensures(return_value <= (MLKEM_Q - 1)) -) { return ((u * MLKEM_Q) + 512) / 1024; } - -/************************************************************ - * Name: scalar_compress_d11 - * - * Description: Computes round(u * 2**11 / q) % 2**11 - * - * Implements Compress_d from FIPS203, Eq (4.7), - * for d = 11. - * - * Arguments: - u: Unsigned canonical modulus modulo q - * to be compressed. - ************************************************************/ -/* - * The multiplication in this routine will exceed UINT32_MAX - * and wrap around for large values of u. This is expected and required. - */ -#ifdef CBMC -#pragma CPROVER check push -#pragma CPROVER check disable "unsigned-overflow" -#endif -static INLINE uint32_t scalar_compress_d11(uint16_t u) -__contract__( - requires(u <= MLKEM_Q - 1) - ensures(return_value < (1u << 11)) - ensures(return_value == (((uint32_t)u * (1u << 11) + MLKEM_Q / 2) / MLKEM_Q) % (1 << 11))) -{ - uint64_t d0 = (uint64_t)u * 5284526080; /* 2^11 * round(2^33 / MLKEM_Q) */ - d0 = (d0 + ((uint64_t)1u << 32)) >> 33; - return (d0 & 0x7FF); -} -#ifdef CBMC -#pragma CPROVER check pop -#endif - -/************************************************************ - * Name: scalar_decompress_d11 - * - * Description: Computes round(u * q / 1024) - * - * Implements Decompress_d from FIPS203, Eq (4.8), - * for d = 10. - * - * Arguments: - u: Unsigned canonical modulus modulo 16 - * to be decompressed. - ************************************************************/ -static INLINE uint16_t scalar_decompress_d11(uint32_t u) -__contract__( - requires(0 <= u && u < 2048) - ensures(return_value <= (MLKEM_Q - 1)) -) { return ((u * MLKEM_Q) + 1024) / 2048; } - -/************************************************************ - * Name: scalar_signed_to_unsigned_q - * - * Description: converts signed polynomial coefficient - * from signed (-3328 .. 3328) form to - * unsigned form (0 .. 3328). - * - * Note: Cryptographic constant time implementation - * - * Examples: 0 -> 0 - * 1 -> 1 - * 3328 -> 3328 - * -1 -> 3328 - * -2 -> 3327 - * -3328 -> 1 - * - * Arguments: c: signed coefficient to be converted - ************************************************************/ -static INLINE uint16_t scalar_signed_to_unsigned_q(int16_t c) -__contract__( - requires(c > -MLKEM_Q && c < MLKEM_Q) - ensures(return_value >= 0 && return_value < MLKEM_Q) - ensures(return_value == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q))) -{ - debug_assert_abs_bound(&c, 1, MLKEM_Q); - - /* Add Q if c is negative, but in constant time */ - c = ct_sel_int16(c + MLKEM_Q, c, ct_cmask_neg_i16(c)); - - /* and therefore cast to uint16_t is safe. */ - debug_assert_bound(&c, 1, 0, MLKEM_Q); - return (uint16_t)c; -} - -#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || \ - (MLKEM_K == 2 || MLKEM_K == 3) -#define poly_compress_d4 MLKEM_NAMESPACE(poly_compress_d4) -/************************************************* - * Name: poly_compress_d4 - * - * Description: Compression (4 bits) and subsequent serialization of a - * polynomial - * - * Arguments: - uint8_t *r: pointer to output byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_D4 bytes) - * - const poly *a: pointer to input polynomial - * Coefficients must be unsigned canonical, - * i.e. in [0,1,..,MLKEM_Q-1]. - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const poly *a); - -#define poly_compress_d10 MLKEM_NAMESPACE(poly_compress_d10) -/************************************************* - * Name: poly_compress_d10 - * - * Description: Compression (10 bits) and subsequent serialization of a - * polynomial - * - * Arguments: - uint8_t *r: pointer to output byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_D10 bytes) - * - const poly *a: pointer to input polynomial - * Coefficients must be unsigned canonical, - * i.e. in [0,1,..,MLKEM_Q-1]. - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_compress_d10(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], const poly *a); - -#define poly_decompress_d4 MLKEM_NAMESPACE(poly_decompress_d4) -/************************************************* - * Name: poly_decompress_d4 - * - * Description: De-serialization and subsequent decompression (dv bits) of a - * polynomial; approximate inverse of poly_compress - * - * Arguments: - poly *r: pointer to output polynomial - * - const uint8_t *a: pointer to input byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_D4 bytes) - * - * Upon return, the coefficients of the output polynomial are unsigned-canonical - * (non-negative and smaller than MLKEM_Q). - * - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_decompress_d4(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D4]); - -#define poly_decompress_d10 MLKEM_NAMESPACE(poly_decompress_d10) -/************************************************* - * Name: poly_decompress_d10 - * - * Description: De-serialization and subsequent decompression (10 bits) of a - * polynomial; approximate inverse of poly_compress_d10 - * - * Arguments: - poly *r: pointer to output polynomial - * - const uint8_t *a: pointer to input byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_D10 bytes) - * - * Upon return, the coefficients of the output polynomial are unsigned-canonical - * (non-negative and smaller than MLKEM_Q). - * - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_decompress_d10(poly *r, - const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D10]); -#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || (MLKEM_K == 2 \ - || MLKEM_K == 3) */ - -#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_K == 4 -#define poly_compress_d5 MLKEM_NAMESPACE(poly_compress_d5) -/************************************************* - * Name: poly_compress_d5 - * - * Description: Compression (5 bits) and subsequent serialization of a - * polynomial - * - * Arguments: - uint8_t *r: pointer to output byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_D5 bytes) - * - const poly *a: pointer to input polynomial - * Coefficients must be unsigned canonical, - * i.e. in [0,1,..,MLKEM_Q-1]. - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const poly *a); - -#define poly_compress_d11 MLKEM_NAMESPACE(poly_compress_d11) -/************************************************* - * Name: poly_compress_d11 - * - * Description: Compression (11 bits) and subsequent serialization of a - * polynomial - * - * Arguments: - uint8_t *r: pointer to output byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_D11 bytes) - * - const poly *a: pointer to input polynomial - * Coefficients must be unsigned canonical, - * i.e. in [0,1,..,MLKEM_Q-1]. - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_compress_d11(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const poly *a); - -#define poly_decompress_d5 MLKEM_NAMESPACE(poly_decompress_d5) -/************************************************* - * Name: poly_decompress_d5 - * - * Description: De-serialization and subsequent decompression (dv bits) of a - * polynomial; approximate inverse of poly_compress - * - * Arguments: - poly *r: pointer to output polynomial - * - const uint8_t *a: pointer to input byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_D5 bytes) - * - * Upon return, the coefficients of the output polynomial are unsigned-canonical - * (non-negative and smaller than MLKEM_Q). - * - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_decompress_d5(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D5]); - -#define poly_decompress_d11 MLKEM_NAMESPACE(poly_decompress_d11) -/************************************************* - * Name: poly_decompress_d11 - * - * Description: De-serialization and subsequent decompression (11 bits) of a - * polynomial; approximate inverse of poly_compress_d11 - * - * Arguments: - poly *r: pointer to output polynomial - * - const uint8_t *a: pointer to input byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_D11 bytes) - * - * Upon return, the coefficients of the output polynomial are unsigned-canonical - * (non-negative and smaller than MLKEM_Q). - * - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_decompress_d11(poly *r, - const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D11]); -#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_K == 4 \ - */ - -#define poly_tobytes MLKEM_NAMESPACE(poly_tobytes) -/************************************************* - * Name: poly_tobytes - * - * Description: Serialization of a polynomial. - * Signed coefficients are converted to - * unsigned form before serialization. - * - * Arguments: INPUT: - * - a: const pointer to input polynomial, - * with each coefficient in the range [0,1,..,Q-1] - * OUTPUT - * - r: pointer to output byte array - * (of MLKEM_POLYBYTES bytes) - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a) -__contract__( - requires(memory_no_alias(r, MLKEM_POLYBYTES)) - requires(memory_no_alias(a, sizeof(poly))) - requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) - assigns(object_whole(r)) -); - - -#define poly_frombytes MLKEM_NAMESPACE(poly_frombytes) -/************************************************* - * Name: poly_frombytes - * - * Description: De-serialization of a polynomial. - * - * Arguments: INPUT - * - a: pointer to input byte array - * (of MLKEM_POLYBYTES bytes) - * OUTPUT - * - r: pointer to output polynomial, with - * each coefficient unsigned and in the range - * 0 .. 4095 - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES]) -__contract__( - requires(memory_no_alias(a, MLKEM_POLYBYTES)) - requires(memory_no_alias(r, sizeof(poly))) - assigns(memory_slice(r, sizeof(poly))) - ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, UINT12_LIMIT)) -); - - -#define poly_frommsg MLKEM_NAMESPACE(poly_frommsg) -/************************************************* - * Name: poly_frommsg - * - * Description: Convert 32-byte message to polynomial - * - * Arguments: - poly *r: pointer to output polynomial - * - const uint8_t *msg: pointer to input message - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_frommsg(poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES]) -__contract__( - requires(memory_no_alias(msg, MLKEM_INDCPA_MSGBYTES)) - requires(memory_no_alias(r, sizeof(poly))) - assigns(object_whole(r)) - ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) -); - -#define poly_tomsg MLKEM_NAMESPACE(poly_tomsg) -/************************************************* - * Name: poly_tomsg - * - * Description: Convert polynomial to 32-byte message - * - * Arguments: - uint8_t *msg: pointer to output message - * - const poly *r: pointer to input polynomial - * Coefficients must be unsigned canonical - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_tomsg(uint8_t msg[MLKEM_INDCPA_MSGBYTES], const poly *r) -__contract__( - requires(memory_no_alias(msg, MLKEM_INDCPA_MSGBYTES)) - requires(memory_no_alias(r, sizeof(poly))) - requires(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) - assigns(object_whole(msg)) -); - #define poly_basemul_montgomery_cached \ MLKEM_NAMESPACE(poly_basemul_montgomery_cached) /************************************************* @@ -715,4 +204,56 @@ __contract__( assigns(object_whole(r)) ); +#define poly_ntt MLKEM_NAMESPACE(poly_ntt) +/************************************************* + * Name: poly_ntt + * + * Description: Computes negacyclic number-theoretic transform (NTT) of + * a polynomial in place. + * + * The input is assumed to be in normal order and + * coefficient-wise bound by MLKEM_Q in absolute value. + * + * The output polynomial is in bitreversed order, and + * coefficient-wise bound by NTT_BOUND in absolute value. + * + * (NOTE: Sometimes the input to the NTT is actually smaller, + * which gives better bounds.) + * + * Arguments: - poly *p: pointer to in/output polynomial + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_ntt(poly *r) +__contract__( + requires(memory_no_alias(r, sizeof(poly))) + requires(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_Q)) + assigns(memory_slice(r, sizeof(poly))) + ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, NTT_BOUND)) +); + +#define poly_invntt_tomont MLKEM_NAMESPACE(poly_invntt_tomont) +/************************************************* + * Name: poly_invntt_tomont + * + * Description: Computes inverse of negacyclic number-theoretic transform (NTT) + * of a polynomial in place; + * inputs assumed to be in bitreversed order, output in normal + * order + * + * The input is assumed to be in bitreversed order, and can + * have arbitrary coefficients in int16_t. + * + * The output polynomial is in normal order, and + * coefficient-wise bound by INVNTT_BOUND in absolute value. + * + * Arguments: - uint16_t *a: pointer to in/output polynomial + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_invntt_tomont(poly *r) +__contract__( + requires(memory_no_alias(r, sizeof(poly))) + assigns(memory_slice(r, sizeof(poly))) + ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INVNTT_BOUND)) +); + #endif /* POLY_H */ diff --git a/mlkem/polyvec.c b/mlkem/polyvec.c index 50ea1c34a..3ec40630f 100644 --- a/mlkem/polyvec.c +++ b/mlkem/polyvec.c @@ -6,9 +6,8 @@ #include #include #include "arith_backend.h" -#include "cbd.h" -#include "ntt.h" -#include "poly.h" +#include "compress.h" +#include "sampling.h" #include "symmetric.h" #include "debug.h" diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h index 8be8579e0..cd3d72349 100644 --- a/mlkem/polyvec.h +++ b/mlkem/polyvec.h @@ -7,6 +7,7 @@ #include #include "common.h" +#include "compress.h" #include "poly.h" #define polyvec MLKEM_NAMESPACE_K(polyvec) diff --git a/mlkem/reduce.h b/mlkem/reduce.h deleted file mode 100644 index b432a4201..000000000 --- a/mlkem/reduce.h +++ /dev/null @@ -1,209 +0,0 @@ -/* - * Copyright (c) 2024 The mlkem-native project authors - * SPDX-License-Identifier: Apache-2.0 - */ -#ifndef REDUCE_H -#define REDUCE_H - -#include -#include "cbmc.h" -#include "common.h" -#include "debug.h" - -/* Static namespacing - * This is to facilitate building multiple instances - * of mlkem-native (e.g. with varying security levels) - * within a single compilation unit. */ -#define cast_uint16_to_int16 MLKEM_NAMESPACE(cast_uint16_to_int16) -#define montgomery_reduce_generic MLKEM_NAMESPACE(montgomery_reduce_generic) -#define montgomery_reduce MLKEM_NAMESPACE(montgomery_reduce) -#define fqmul MLKEM_NAMESPACE(fqmul) -#define barrett_reduce MLKEM_NAMESPACE(barrett_reduce) -/* End of static namespacing */ - -#define HALF_Q ((MLKEM_Q + 1) / 2) /* 1665 */ - -/************************************************* - * Name: cast_uint16_to_int16 - * - * Description: Cast uint16 value to int16 - * - * Returns: - * input x in 0 .. 32767: returns value unchanged - * input x in 32768 .. 65535: returns (x - 65536) - **************************************************/ -#ifdef CBMC -#pragma CPROVER check push -#pragma CPROVER check disable "conversion" -#endif -ALWAYS_INLINE -static INLINE int16_t cast_uint16_to_int16(uint16_t x) -{ - /* - * PORTABILITY: This relies on uint16_t -> int16_t - * being implemented as the inverse of int16_t -> uint16_t, - * which is implementation-defined (C99 6.3.1.3 (3)) - * CBMC (correctly) fails to prove this conversion is OK, - * so we have to suppress that check here - */ - return (int16_t)x; -} -#ifdef CBMC -#pragma CPROVER check pop -#endif - -/************************************************* - * Name: montgomery_reduce_generic - * - * Description: Generic Montgomery reduction; given a 32-bit integer a, computes - * 16-bit integer congruent to a * R^-1 mod q, where R=2^16 - * - * Arguments: - int32_t a: input integer to be reduced - * - * Returns: integer congruent to a * R^-1 modulo q, with absolute value - * <= ceil(|a| / 2^16) + (MLKEM_Q + 1)/2 - * - **************************************************/ -ALWAYS_INLINE -static INLINE int16_t montgomery_reduce_generic(int32_t a) -{ - /* QINV == -3327 converted to uint16_t == -3327 + 65536 == 62209 */ - const uint32_t QINV = 62209; /* q^-1 mod 2^16 */ - - /* Compute a*q^{-1} mod 2^16 in unsigned representatives */ - const uint16_t a_reduced = a & UINT16_MAX; - const uint16_t a_inverted = (a_reduced * QINV) & UINT16_MAX; - - /* Lift to signed canonical representative mod 2^16. */ - const int16_t t = cast_uint16_to_int16(a_inverted); - - int32_t r = a - ((int32_t)t * MLKEM_Q); - /* Bounds: |r| <= |a| + 2^15 * MLKEM_Q */ - - /* - * PORTABILITY: Right-shift on a signed integer is, strictly-speaking, - * implementation-defined for negative left argument. Here, - * we assume it's sign-preserving "arithmetic" shift right. (C99 6.5.7 (5)) - */ - r = r >> 16; - /* Bounds: |r >> 16| <= ceil(|r| / 2^16) - * <= ceil(|a| / 2^16 + MLKEM_Q / 2) - * <= ceil(|a| / 2^16) + (MLKEM_Q + 1) / 2 - * - * (Note that |a >> n| = ceil(|a| / 2^16) for negative a) - */ - - return (int16_t)r; -} - -/************************************************* - * Name: montgomery_reduce - * - * Description: Montgomery reduction - * - * Arguments: - int32_t a: input integer to be reduced - * Must be smaller than 2 * 2^12 * 2^15 in absolute value. - * - * Returns: integer congruent to a * R^-1 modulo q, - * smaller than 2 * q in absolute value. - **************************************************/ -static INLINE int16_t montgomery_reduce(int32_t a) -__contract__( - requires(a > -(2 * UINT12_LIMIT * 32768)) - requires(a < (2 * UINT12_LIMIT * 32768)) - ensures(return_value > -2 * MLKEM_Q && return_value < 2 * MLKEM_Q) -) -{ - int16_t res; - debug_assert_abs_bound(&a, 1, 2 * UINT12_LIMIT * 32768); - - res = montgomery_reduce_generic(a); - /* Bounds: - * |res| <= ceil(|a| / 2^16) + (MLKEM_Q + 1) / 2 - * <= ceil(2 * UINT12_LIMIT * 32768 / 65536) + (MLKEM_Q + 1) / 2 - * <= UINT12_LIMIT + (MLKEM_Q + 1) / 2 - * < 2 * MLKEM_Q */ - - debug_assert_abs_bound(&res, 1, 2 * MLKEM_Q); - return res; -} - -/************************************************* - * Name: fqmul - * - * Description: Montgomery multiplication modulo q=3329 - * - * Arguments: - int16_t a: first factor - * Can be any int16_t. - * - int16_t b: second factor. - * Must be signed canonical (abs value <(q+1)/2) - * - * Returns 16-bit integer congruent to a*b*R^{-1} mod q, and - * smaller than q in absolute value. - * - **************************************************/ -static INLINE int16_t fqmul(int16_t a, int16_t b) -__contract__( - requires(b > -HALF_Q) - requires(b < HALF_Q) - ensures(return_value > -MLKEM_Q && return_value < MLKEM_Q) -) -{ - int16_t res; - debug_assert_abs_bound(&b, 1, HALF_Q); - - res = montgomery_reduce((int32_t)a * (int32_t)b); - /* Bounds: - * |res| <= ceil(|a| * |b| / 2^16) + (MLKEM_Q + 1) / 2 - * <= ceil(2^15 * ((MLKEM_Q - 1)/2) / 2^16) + (MLKEM_Q + 1) / 2 - * <= ceil((MLKEM_Q - 1) / 4) + (MLKEM_Q + 1) / 2 - * < MLKEM_Q - */ - - debug_assert_abs_bound(&res, 1, MLKEM_Q); - return res; -} - -/************************************************* - * Name: barrett_reduce - * - * Description: Barrett reduction; given a 16-bit integer a, computes - * centered representative congruent to a mod q in - * {-(q-1)/2,...,(q-1)/2} - * - * Arguments: - int16_t a: input integer to be reduced - * - * Returns: integer in {-(q-1)/2,...,(q-1)/2} congruent to a modulo q. - **************************************************/ -static INLINE int16_t barrett_reduce(int16_t a) -__contract__( - ensures(return_value > -HALF_Q && return_value < HALF_Q) -) -{ - /* - * To divide by MLKEM_Q using Barrett multiplication, the "magic number" - * multiplier is round_to_nearest(2**26/MLKEM_Q) - */ - const int BPOWER = 26; - const int32_t barrett_multiplier = ((1 << BPOWER) + MLKEM_Q / 2) / MLKEM_Q; - - /* - * Compute round_to_nearest(a/MLKEM_Q) using the multiplier - * above and shift by BPOWER places. - * PORTABILITY: Right-shift on a signed integer is, strictly-speaking, - * implementation-defined for negative left argument. Here, - * we assume it's sign-preserving "arithmetic" shift right. (C99 6.5.7 (5)) - */ - const int32_t t = (barrett_multiplier * a + (1 << (BPOWER - 1))) >> BPOWER; - - /* - * t is in -10 .. +10, so we need 32-bit math to - * evaluate t * MLKEM_Q and the subsequent subtraction - */ - int16_t res = (int16_t)(a - t * MLKEM_Q); - - debug_assert_abs_bound(&res, 1, HALF_Q); - return res; -} - -#endif diff --git a/mlkem/rej_uniform.c b/mlkem/sampling.c similarity index 73% rename from mlkem/rej_uniform.c rename to mlkem/sampling.c index 626a440e2..3402ab253 100644 --- a/mlkem/rej_uniform.c +++ b/mlkem/sampling.c @@ -9,7 +9,7 @@ #include "debug.h" #include "fips202/fips202.h" #include "fips202/fips202x4.h" -#include "rej_uniform.h" +#include "sampling.h" #include "symmetric.h" /* Static namespacing @@ -18,6 +18,8 @@ * within a single compilation unit. */ #define rej_uniform MLKEM_NAMESPACE(rej_uniform) #define rej_uniform_scalar MLKEM_NAMESPACE(rej_uniform_scalar) +#define load32_littleendian MLKEM_NAMESPACE(load32_littleendian) +#define load24_littleendian MLKEM_NAMESPACE(load24_littleendian) /* End of static namespacing */ static unsigned int rej_uniform_scalar(int16_t *r, unsigned int target, @@ -229,9 +231,113 @@ void poly_rej_uniform(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 2]) xof_release(&state); } +/* Static namespacing + * This is to facilitate building multiple instances + * of mlkem-native (e.g. with varying security levels) + * within a single compilation unit. */ +#define load32_littleendian MLKEM_NAMESPACE(load32_littleendian) +#define load24_littleendian MLKEM_NAMESPACE(load24_littleendian) +/* End of static namespacing */ + +/************************************************* + * Name: load32_littleendian + * + * Description: load 4 bytes into a 32-bit integer + * in little-endian order + * + * Arguments: - const uint8_t *x: pointer to input byte array + * + * Returns 32-bit unsigned integer loaded from x + **************************************************/ +static uint32_t load32_littleendian(const uint8_t x[4]) +{ + uint32_t r; + r = (uint32_t)x[0]; + r |= (uint32_t)x[1] << 8; + r |= (uint32_t)x[2] << 16; + r |= (uint32_t)x[3] << 24; + return r; +} + +MLKEM_NATIVE_INTERNAL_API +void poly_cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]) +{ + unsigned i; + for (i = 0; i < MLKEM_N / 8; i++) + __loop__( + invariant(i <= MLKEM_N / 8) + invariant(array_abs_bound(r->coeffs, 0, 8 * i, 3))) + { + unsigned j; + uint32_t t = load32_littleendian(buf + 4 * i); + uint32_t d = t & 0x55555555; + d += (t >> 1) & 0x55555555; + + for (j = 0; j < 8; j++) + __loop__( + invariant(i <= MLKEM_N / 8 && j <= 8) + invariant(array_abs_bound(r->coeffs, 0, 8 * i + j, 3))) + { + const int16_t a = (d >> (4 * j + 0)) & 0x3; + const int16_t b = (d >> (4 * j + 2)) & 0x3; + r->coeffs[8 * i + j] = a - b; + } + } +} + +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == 3 +/************************************************* + * Name: load24_littleendian + * + * Description: load 3 bytes into a 32-bit integer + * in little-endian order. + * This function is only needed for ML-KEM-512 + * + * Arguments: - const uint8_t *x: pointer to input byte array + * + * Returns 32-bit unsigned integer loaded from x (most significant byte is zero) + **************************************************/ +static uint32_t load24_littleendian(const uint8_t x[3]) +{ + uint32_t r; + r = (uint32_t)x[0]; + r |= (uint32_t)x[1] << 8; + r |= (uint32_t)x[2] << 16; + return r; +} + +MLKEM_NATIVE_INTERNAL_API +void poly_cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]) +{ + unsigned i; + for (i = 0; i < MLKEM_N / 4; i++) + __loop__( + invariant(i <= MLKEM_N / 4) + invariant(array_abs_bound(r->coeffs, 0, 4 * i, 4))) + { + unsigned j; + const uint32_t t = load24_littleendian(buf + 3 * i); + uint32_t d = t & 0x00249249; + d += (t >> 1) & 0x00249249; + d += (t >> 2) & 0x00249249; + + for (j = 0; j < 4; j++) + __loop__( + invariant(i <= MLKEM_N / 4 && j <= 4) + invariant(array_abs_bound(r->coeffs, 0, 4 * i + j, 4))) + { + const int16_t a = (d >> (6 * j + 0)) & 0x7; + const int16_t b = (d >> (6 * j + 3)) & 0x7; + r->coeffs[4 * i + j] = a - b; + } + } +} +#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == \ + 3 */ + #else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ -#define empty_cu_rej_uniform MLKEM_NAMESPACE_K(empty_cu_rej_uniform) -int empty_cu_rej_uniform; +#define empty_cu_sampling MLKEM_NAMESPACE_K(empty_cu_sampling) +int empty_cu_sampling; #endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/rej_uniform.h b/mlkem/sampling.h similarity index 63% rename from mlkem/rej_uniform.h rename to mlkem/sampling.h index 801287259..cc524e0fc 100644 --- a/mlkem/rej_uniform.h +++ b/mlkem/sampling.h @@ -2,8 +2,8 @@ * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 */ -#ifndef REJ_UNIFORM_H -#define REJ_UNIFORM_H +#ifndef SAMPLING_H +#define SAMPLING_H #include #include @@ -11,6 +11,37 @@ #include "common.h" #include "poly.h" +#define poly_cbd2 MLKEM_NAMESPACE(poly_cbd2) +/************************************************* + * Name: poly_cbd2 + * + * Description: Given an array of uniformly random bytes, compute + * polynomial with coefficients distributed according to + * a centered binomial distribution with parameter eta=2 + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *buf: pointer to input byte array + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]); + +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == 3 +#define poly_cbd3 MLKEM_NAMESPACE(poly_cbd3) +/************************************************* + * Name: poly_cbd3 + * + * Description: Given an array of uniformly random bytes, compute + * polynomial with coefficients distributed according to + * a centered binomial distribution with parameter eta=3. + * This function is only needed for ML-KEM-512 + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *buf: pointer to input byte array + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]); +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD || MLKEM_ETA1 == 3 */ + #define poly_rej_uniform_x4 MLKEM_NAMESPACE(poly_rej_uniform_x4) /************************************************* * Name: poly_rej_uniform_x4 @@ -60,4 +91,4 @@ __contract__( assigns(memory_slice(entry, sizeof(poly))) ensures(array_bound(entry->coeffs, 0, MLKEM_N, 0, MLKEM_Q))); -#endif /* REJ_UNIFORM_H */ +#endif /* SAMPLING_H */ diff --git a/mlkem/zetas.c b/mlkem/zetas.c index 4ef887c62..987f0dce4 100644 --- a/mlkem/zetas.c +++ b/mlkem/zetas.c @@ -10,7 +10,7 @@ #include "common.h" #if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) -#include "ntt.h" +#include "poly.h" /* * Table of zeta values used in the reference NTT and inverse NTT. diff --git a/proofs/cbmc/barrett_reduce/Makefile b/proofs/cbmc/barrett_reduce/Makefile index e339c38b2..45b3f7f66 100644 --- a/proofs/cbmc/barrett_reduce/Makefile +++ b/proofs/cbmc/barrett_reduce/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Some unit including reduce.h +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)barrett_reduce USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/barrett_reduce/barrett_reduce_harness.c b/proofs/cbmc/barrett_reduce/barrett_reduce_harness.c index f7080316b..6c213774c 100644 --- a/proofs/cbmc/barrett_reduce/barrett_reduce_harness.c +++ b/proofs/cbmc/barrett_reduce/barrett_reduce_harness.c @@ -2,7 +2,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "reduce.h" +#include +#include "common.h" + +#define barrett_reduce MLKEM_NAMESPACE(barrett_reduce) +int16_t barrett_reduce(int16_t a); void harness(void) { diff --git a/proofs/cbmc/basemul_cached/Makefile b/proofs/cbmc/basemul_cached/Makefile index 5ba01f852..905355ffb 100644 --- a/proofs/cbmc/basemul_cached/Makefile +++ b/proofs/cbmc/basemul_cached/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)basemul_cached USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)montgomery_reduce diff --git a/proofs/cbmc/basemul_cached/basemul_cached_harness.c b/proofs/cbmc/basemul_cached/basemul_cached_harness.c index ef397b63f..df83f2349 100644 --- a/proofs/cbmc/basemul_cached/basemul_cached_harness.c +++ b/proofs/cbmc/basemul_cached/basemul_cached_harness.c @@ -2,9 +2,12 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 +#include +#include "common.h" -#include "ntt.h" -#include "reduce.h" +#define basemul_cached MLKEM_NAMESPACE(basemul_cached) +void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2], + int16_t b_cached); void harness(void) { diff --git a/proofs/cbmc/fqmul/fqmul_harness.c b/proofs/cbmc/fqmul/fqmul_harness.c index 2466a3321..4b58c2ad7 100644 --- a/proofs/cbmc/fqmul/fqmul_harness.c +++ b/proofs/cbmc/fqmul/fqmul_harness.c @@ -2,7 +2,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "reduce.h" +#include +#include "common.h" + +#define fqmul MLKEM_NAMESPACE(fqmul) +int16_t fqmul(int16_t a, int16_t b); void harness(void) { diff --git a/proofs/cbmc/invntt_layer/Makefile b/proofs/cbmc/invntt_layer/Makefile index 77ca82d2f..e372b0760 100644 --- a/proofs/cbmc/invntt_layer/Makefile +++ b/proofs/cbmc/invntt_layer/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c $(SRCDIR)/mlkem/zetas.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/zetas.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul $(MLKEM_NAMESPACE)barrett_reduce diff --git a/proofs/cbmc/montgomery_reduce/montgomery_reduce_harness.c b/proofs/cbmc/montgomery_reduce/montgomery_reduce_harness.c index aa7282aa4..f6daae9fe 100644 --- a/proofs/cbmc/montgomery_reduce/montgomery_reduce_harness.c +++ b/proofs/cbmc/montgomery_reduce/montgomery_reduce_harness.c @@ -2,7 +2,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "reduce.h" +#include +#include "common.h" + +#define montgomery_reduce MLKEM_NAMESPACE(montgomery_reduce) +int16_t montgomery_reduce(int32_t a); void harness(void) { diff --git a/proofs/cbmc/ntt_butterfly_block/Makefile b/proofs/cbmc/ntt_butterfly_block/Makefile index c1c6d7928..aa1fadd8a 100644 --- a/proofs/cbmc/ntt_butterfly_block/Makefile +++ b/proofs/cbmc/ntt_butterfly_block/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_butterfly_block USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul diff --git a/proofs/cbmc/ntt_layer/Makefile b/proofs/cbmc/ntt_layer/Makefile index 12f43a14b..86632eabb 100644 --- a/proofs/cbmc/ntt_layer/Makefile +++ b/proofs/cbmc/ntt_layer/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c $(SRCDIR)/mlkem/zetas.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/zetas.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_butterfly_block diff --git a/proofs/cbmc/poly_cbd_eta1/Makefile b/proofs/cbmc/poly_cbd_eta1/Makefile index 409e3b4d6..d8a73b209 100644 --- a/proofs/cbmc/poly_cbd_eta1/Makefile +++ b/proofs/cbmc/poly_cbd_eta1/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/cbd.c $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c $(SRCDIR)/mlkem/polyvec.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta1 USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/poly_cbd_eta2/Makefile b/proofs/cbmc/poly_cbd_eta2/Makefile index 27472c186..8c3efb20f 100644 --- a/proofs/cbmc/poly_cbd_eta2/Makefile +++ b/proofs/cbmc/poly_cbd_eta2/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/cbd.c $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c $(SRCDIR)/mlkem/polyvec.c # Only relevant for K=2 or K=4 ifeq ($(MLKEM_K),2) diff --git a/proofs/cbmc/poly_compress_du/Makefile b/proofs/cbmc/poly_compress_du/Makefile index f71bfef85..8f5b030c8 100644 --- a/proofs/cbmc/poly_compress_du/Makefile +++ b/proofs/cbmc/poly_compress_du/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du USE_FUNCTION_CONTRACTS = diff --git a/proofs/cbmc/poly_compress_dv/Makefile b/proofs/cbmc/poly_compress_dv/Makefile index 8fc356ea9..850163e66 100644 --- a/proofs/cbmc/poly_compress_dv/Makefile +++ b/proofs/cbmc/poly_compress_dv/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_dv diff --git a/proofs/cbmc/poly_decompress_du/Makefile b/proofs/cbmc/poly_decompress_du/Makefile index 3736ecfee..7f038096a 100644 --- a/proofs/cbmc/poly_decompress_du/Makefile +++ b/proofs/cbmc/poly_decompress_du/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_du diff --git a/proofs/cbmc/poly_decompress_dv/Makefile b/proofs/cbmc/poly_decompress_dv/Makefile index 6d0e20f49..38f9ba533 100644 --- a/proofs/cbmc/poly_decompress_dv/Makefile +++ b/proofs/cbmc/poly_decompress_dv/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_dv diff --git a/proofs/cbmc/poly_frombytes/Makefile b/proofs/cbmc/poly_frombytes/Makefile index 8d7439548..1b41ea11a 100644 --- a/proofs/cbmc/poly_frombytes/Makefile +++ b/proofs/cbmc/poly_frombytes/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_frombytes USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c b/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c index 26cddc74a..77c5f2d06 100644 --- a/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c +++ b/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/poly_frommsg/Makefile b/proofs/cbmc/poly_frommsg/Makefile index fe885494d..15448e3a3 100644 --- a/proofs/cbmc/poly_frommsg/Makefile +++ b/proofs/cbmc/poly_frommsg/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_frommsg USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ct_sel_int16 $(MLKEM_NAMESPACE)value_barrier_u8 diff --git a/proofs/cbmc/poly_frommsg/poly_frommsg_harness.c b/proofs/cbmc/poly_frommsg/poly_frommsg_harness.c index ec66290cc..e33f94881 100644 --- a/proofs/cbmc/poly_frommsg/poly_frommsg_harness.c +++ b/proofs/cbmc/poly_frommsg/poly_frommsg_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/poly_invntt_tomont/Makefile b/proofs/cbmc/poly_invntt_tomont/Makefile index 7647a0897..6772c2112 100644 --- a/proofs/cbmc/poly_invntt_tomont/Makefile +++ b/proofs/cbmc/poly_invntt_tomont/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_invntt_tomont USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer $(MLKEM_NAMESPACE)fqmul diff --git a/proofs/cbmc/poly_invntt_tomont/poly_invntt_tomont_harness.c b/proofs/cbmc/poly_invntt_tomont/poly_invntt_tomont_harness.c index b203a532f..5d48b3eae 100644 --- a/proofs/cbmc/poly_invntt_tomont/poly_invntt_tomont_harness.c +++ b/proofs/cbmc/poly_invntt_tomont/poly_invntt_tomont_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "ntt.h" +#include "poly.h" void harness(void) { diff --git a/proofs/cbmc/poly_mulcache_compute/Makefile b/proofs/cbmc/poly_mulcache_compute/Makefile index 9983be818..394301103 100644 --- a/proofs/cbmc/poly_mulcache_compute/Makefile +++ b/proofs/cbmc/poly_mulcache_compute/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/ntt.c $(SRCDIR)/mlkem/zetas.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/zetas.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_mulcache_compute USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul diff --git a/proofs/cbmc/poly_mulcache_compute/poly_mulcache_compute_harness.c b/proofs/cbmc/poly_mulcache_compute/poly_mulcache_compute_harness.c index 5ca4127fe..7a90ed537 100644 --- a/proofs/cbmc/poly_mulcache_compute/poly_mulcache_compute_harness.c +++ b/proofs/cbmc/poly_mulcache_compute/poly_mulcache_compute_harness.c @@ -2,7 +2,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "ntt.h" #include "poly.h" void harness(void) diff --git a/proofs/cbmc/poly_ntt/Makefile b/proofs/cbmc/poly_ntt/Makefile index 1cceb286e..1ee5f2742 100644 --- a/proofs/cbmc/poly_ntt/Makefile +++ b/proofs/cbmc/poly_ntt/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_ntt USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_layer diff --git a/proofs/cbmc/poly_ntt/poly_ntt_harness.c b/proofs/cbmc/poly_ntt/poly_ntt_harness.c index 8e09972c0..333d34f63 100644 --- a/proofs/cbmc/poly_ntt/poly_ntt_harness.c +++ b/proofs/cbmc/poly_ntt/poly_ntt_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include void harness(void) { diff --git a/proofs/cbmc/poly_rej_uniform/Makefile b/proofs/cbmc/poly_rej_uniform/Makefile index 2eae2baab..396858333 100644 --- a/proofs/cbmc/poly_rej_uniform/Makefile +++ b/proofs/cbmc/poly_rej_uniform/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/rej_uniform.c $(SRCDIR)/mlkem/fips202/fips202.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c $(SRCDIR)/mlkem/fips202/fips202.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake128_absorb_once $(MLKEM_NAMESPACE)shake128_squeezeblocks $(MLKEM_NAMESPACE)rej_uniform diff --git a/proofs/cbmc/poly_rej_uniform/poly_rej_uniform_harness.c b/proofs/cbmc/poly_rej_uniform/poly_rej_uniform_harness.c index d65d33240..71b01603e 100644 --- a/proofs/cbmc/poly_rej_uniform/poly_rej_uniform_harness.c +++ b/proofs/cbmc/poly_rej_uniform/poly_rej_uniform_harness.c @@ -3,7 +3,7 @@ // SPDX-License-Identifier: MIT-0 #include -#include "rej_uniform.h" +#include "sampling.h" void harness(void) { diff --git a/proofs/cbmc/poly_rej_uniform_x4/Makefile b/proofs/cbmc/poly_rej_uniform_x4/Makefile index 9c2d29a89..442245c22 100644 --- a/proofs/cbmc/poly_rej_uniform_x4/Makefile +++ b/proofs/cbmc/poly_rej_uniform_x4/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/rej_uniform.c $(SRCDIR)/mlkem/fips202/fips202x4.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c $(SRCDIR)/mlkem/fips202/fips202x4.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform_x4 USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake128x4_absorb_once $(MLKEM_NAMESPACE)shake128x4_squeezeblocks $(MLKEM_NAMESPACE)rej_uniform diff --git a/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c b/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c index fd0b19b09..829ce65a1 100644 --- a/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c +++ b/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c @@ -3,7 +3,7 @@ // SPDX-License-Identifier: MIT-0 #include -#include "rej_uniform.h" +#include "sampling.h" void harness(void) { diff --git a/proofs/cbmc/poly_tobytes/Makefile b/proofs/cbmc/poly_tobytes/Makefile index 966ef6a46..0b175b440 100644 --- a/proofs/cbmc/poly_tobytes/Makefile +++ b/proofs/cbmc/poly_tobytes/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_tobytes USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c b/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c index 855a57e5d..de83a4d32 100644 --- a/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c +++ b/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/poly_tomsg/Makefile b/proofs/cbmc/poly_tomsg/Makefile index b16621adf..3ed79668e 100644 --- a/proofs/cbmc/poly_tomsg/Makefile +++ b/proofs/cbmc/poly_tomsg/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_tomsg USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c b/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c index 48542ea06..36c56d0f5 100644 --- a/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c +++ b/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c index 0221aed3d..aee8de115 100644 --- a/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c +++ b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c @@ -2,7 +2,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "ntt.h" #include "polyvec.h" void harness(void) diff --git a/proofs/cbmc/rej_uniform/Makefile b/proofs/cbmc/rej_uniform/Makefile index 5e057139e..d768bbf1e 100644 --- a/proofs/cbmc/rej_uniform/Makefile +++ b/proofs/cbmc/rej_uniform/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/rej_uniform.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)rej_uniform USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)rej_uniform_scalar diff --git a/proofs/cbmc/rej_uniform_scalar/Makefile b/proofs/cbmc/rej_uniform_scalar/Makefile index bc4e48c80..0af5d930d 100644 --- a/proofs/cbmc/rej_uniform_scalar/Makefile +++ b/proofs/cbmc/rej_uniform_scalar/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/rej_uniform.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)rej_uniform_scalar USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/rej_uniform_scalar/rej_uniform_scalar_harness.c b/proofs/cbmc/rej_uniform_scalar/rej_uniform_scalar_harness.c index 2cb2a3efa..a9678eff8 100644 --- a/proofs/cbmc/rej_uniform_scalar/rej_uniform_scalar_harness.c +++ b/proofs/cbmc/rej_uniform_scalar/rej_uniform_scalar_harness.c @@ -2,8 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include "cbmc.h" -#include "rej_uniform.h" +#include "sampling.h" #define rej_uniform_scalar MLKEM_NAMESPACE(rej_uniform_scalar) unsigned int rej_uniform_scalar(int16_t *r, unsigned int target, diff --git a/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c b/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c index 1b7f92ac8..42fb73a8c 100644 --- a/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c +++ b/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c b/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c index a58b2b2c5..a84b36af2 100644 --- a/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c +++ b/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c b/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c index 90e73d79a..56dfc4913 100644 --- a/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c +++ b/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c b/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c index 7d5866819..4ac18801c 100644 --- a/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c +++ b/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c b/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c index 5922cb881..6c50800ec 100644 --- a/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c +++ b/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_decompress_d10/scalar_decompress_d10_harness.c b/proofs/cbmc/scalar_decompress_d10/scalar_decompress_d10_harness.c index 70a6c0de8..863200667 100644 --- a/proofs/cbmc/scalar_decompress_d10/scalar_decompress_d10_harness.c +++ b/proofs/cbmc/scalar_decompress_d10/scalar_decompress_d10_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_decompress_d11/scalar_decompress_d11_harness.c b/proofs/cbmc/scalar_decompress_d11/scalar_decompress_d11_harness.c index 11323a85d..b86db78ea 100644 --- a/proofs/cbmc/scalar_decompress_d11/scalar_decompress_d11_harness.c +++ b/proofs/cbmc/scalar_decompress_d11/scalar_decompress_d11_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_decompress_d4/scalar_decompress_d4_harness.c b/proofs/cbmc/scalar_decompress_d4/scalar_decompress_d4_harness.c index f01f22d46..6717104e0 100644 --- a/proofs/cbmc/scalar_decompress_d4/scalar_decompress_d4_harness.c +++ b/proofs/cbmc/scalar_decompress_d4/scalar_decompress_d4_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_decompress_d5/scalar_decompress_d5_harness.c b/proofs/cbmc/scalar_decompress_d5/scalar_decompress_d5_harness.c index fa2340594..cd691cfb0 100644 --- a/proofs/cbmc/scalar_decompress_d5/scalar_decompress_d5_harness.c +++ b/proofs/cbmc/scalar_decompress_d5/scalar_decompress_d5_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "compress.h" void harness(void) { diff --git a/proofs/cbmc/scalar_signed_to_unsigned_q/scalar_signed_to_unsigned_q_harness.c b/proofs/cbmc/scalar_signed_to_unsigned_q/scalar_signed_to_unsigned_q_harness.c index 3d80fd494..6dd93f363 100644 --- a/proofs/cbmc/scalar_signed_to_unsigned_q/scalar_signed_to_unsigned_q_harness.c +++ b/proofs/cbmc/scalar_signed_to_unsigned_q/scalar_signed_to_unsigned_q_harness.c @@ -2,7 +2,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 -#include +#include +#include "common.h" + +#define scalar_signed_to_unsigned_q MLKEM_NAMESPACE(scalar_signed_to_unsigned_q) +uint16_t scalar_signed_to_unsigned_q(int16_t c); void harness(void) { diff --git a/scripts/autogen b/scripts/autogen index 1a9af238b..f9e7df0ac 100755 --- a/scripts/autogen +++ b/scripts/autogen @@ -105,7 +105,7 @@ def gen_c_zeta_file(dry_run=False): yield from gen_header() yield '#include "common.h"' yield "#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED)" - yield '#include "ntt.h"' + yield '#include "poly.h"' yield "" yield "/*" yield " * Table of zeta values used in the reference NTT and inverse NTT." From 51f5adb00127f8be294506545bd9ae50e01a049f Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Tue, 21 Jan 2025 08:44:58 +0000 Subject: [PATCH 2/2] Rename polyvec -> poly_k Originally, polyvec was exclusively home to functions dealing with the `polyvec` structure. Recent changes have invalidated that: In addition to functions operating on `struct polyvec`, polyvec.[ch] hosts all poly-related functionality that depends on the security-level (e.g. the `poly_cbd_eta[12]` wrappers). This commit renames `polyvec.[ch]` to `poly_k.[ch]` to reflect this change in meaning. This change was obtained by - Manual renaming of the files `polyvec.[ch]` -> `poly_k.[ch]` - ```bash git ls-files \ | xargs -I {} sh \ -c "sed -i '' 's/polyvec\.\([ch]\)/poly_k.\1/g' {}" ``` - Manual updating of symlinks in * examples/bring_your_own_fips202 * examples/custom_backend - Bump CBMC OBJECT_BITS from 9 to 10 in invntt_layer, to counter a CBMC failure for MLKEM_K=4. Signed-off-by: Hanno Becker --- .../mlkem_native/poly_k.c | 1 + .../mlkem_native/poly_k.h | 1 + .../mlkem_native/polyvec.c | 1 - .../mlkem_native/polyvec.h | 1 - .../mlkem_native/mlkem/poly_k.c | 1 + .../mlkem_native/mlkem/poly_k.h | 1 + .../mlkem_native/mlkem/polyvec.c | 1 - .../mlkem_native/mlkem/polyvec.h | 1 - .../monolithic_build/mlkem_native_monobuild.c | 56 +++++++++---------- mlkem/indcpa.c | 2 +- mlkem/indcpa.h | 2 +- mlkem/native/aarch64/src/clean_impl.h | 2 +- mlkem/native/aarch64/src/opt_impl.h | 2 +- mlkem/native/api.h | 2 +- mlkem/native/x86_64/src/arith_native_x86_64.h | 2 +- mlkem/native/x86_64/src/basemul.c | 2 +- mlkem/native/x86_64/src/default_impl.h | 2 +- mlkem/{polyvec.c => poly_k.c} | 2 +- mlkem/{polyvec.h => poly_k.h} | 4 +- proofs/cbmc/invntt_layer/Makefile | 2 +- proofs/cbmc/matvec_mul/matvec_mul_harness.c | 2 +- proofs/cbmc/poly_cbd_eta1/Makefile | 2 +- proofs/cbmc/poly_cbd_eta2/Makefile | 2 +- .../poly_compress_du_harness.c | 2 +- .../poly_compress_dv_harness.c | 2 +- .../poly_decompress_du_harness.c | 2 +- .../poly_decompress_dv_harness.c | 2 +- proofs/cbmc/poly_getnoise_eta1122_4x/Makefile | 2 +- .../poly_getnoise_eta1122_4x_harness.c | 2 +- proofs/cbmc/poly_getnoise_eta1_4x/Makefile | 2 +- .../poly_getnoise_eta1_4x_harness.c | 2 +- proofs/cbmc/poly_getnoise_eta2/Makefile | 2 +- .../poly_getnoise_eta2_harness.c | 2 +- proofs/cbmc/polyvec_add/Makefile | 2 +- proofs/cbmc/polyvec_add/polyvec_add_harness.c | 2 +- .../polyvec_basemul_acc_montgomery/Makefile | 2 +- .../polyvec_basemul_acc_montgomery_harness.c | 2 +- .../Makefile | 2 +- ...ec_basemul_acc_montgomery_cached_harness.c | 2 +- proofs/cbmc/polyvec_compress_du/Makefile | 2 +- .../polyvec_compress_du_harness.c | 2 +- proofs/cbmc/polyvec_decompress_du/Makefile | 2 +- .../polyvec_decompress_du_harness.c | 2 +- proofs/cbmc/polyvec_frombytes/Makefile | 2 +- .../polyvec_frombytes_harness.c | 2 +- proofs/cbmc/polyvec_invntt_tomont/Makefile | 2 +- .../polyvec_invntt_tomont_harness.c | 2 +- proofs/cbmc/polyvec_mulcache_compute/Makefile | 2 +- .../polyvec_mulcache_compute_harness.c | 2 +- proofs/cbmc/polyvec_ntt/Makefile | 2 +- proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c | 2 +- proofs/cbmc/polyvec_reduce/Makefile | 2 +- .../polyvec_reduce/polyvec_reduce_harness.c | 2 +- proofs/cbmc/polyvec_tobytes/Makefile | 2 +- .../polyvec_tobytes/polyvec_tobytes_harness.c | 2 +- proofs/cbmc/polyvec_tomont/Makefile | 2 +- .../polyvec_tomont/polyvec_tomont_harness.c | 2 +- scripts/autogen | 2 +- test/bench_components_mlkem.c | 2 +- 59 files changed, 83 insertions(+), 83 deletions(-) create mode 120000 examples/bring_your_own_fips202/mlkem_native/poly_k.c create mode 120000 examples/bring_your_own_fips202/mlkem_native/poly_k.h delete mode 120000 examples/bring_your_own_fips202/mlkem_native/polyvec.c delete mode 120000 examples/bring_your_own_fips202/mlkem_native/polyvec.h create mode 120000 examples/custom_backend/mlkem_native/mlkem/poly_k.c create mode 120000 examples/custom_backend/mlkem_native/mlkem/poly_k.h delete mode 120000 examples/custom_backend/mlkem_native/mlkem/polyvec.c delete mode 120000 examples/custom_backend/mlkem_native/mlkem/polyvec.h rename mlkem/{polyvec.c => poly_k.c} (99%) rename mlkem/{polyvec.h => poly_k.h} (99%) diff --git a/examples/bring_your_own_fips202/mlkem_native/poly_k.c b/examples/bring_your_own_fips202/mlkem_native/poly_k.c new file mode 120000 index 000000000..2a7f2cb82 --- /dev/null +++ b/examples/bring_your_own_fips202/mlkem_native/poly_k.c @@ -0,0 +1 @@ +../../../mlkem/poly_k.c \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/poly_k.h b/examples/bring_your_own_fips202/mlkem_native/poly_k.h new file mode 120000 index 000000000..0aada7662 --- /dev/null +++ b/examples/bring_your_own_fips202/mlkem_native/poly_k.h @@ -0,0 +1 @@ +../../../mlkem/poly_k.h \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/polyvec.c b/examples/bring_your_own_fips202/mlkem_native/polyvec.c deleted file mode 120000 index 83d5cd88f..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/polyvec.c +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/polyvec.c \ No newline at end of file diff --git a/examples/bring_your_own_fips202/mlkem_native/polyvec.h b/examples/bring_your_own_fips202/mlkem_native/polyvec.h deleted file mode 120000 index cc19e1f8c..000000000 --- a/examples/bring_your_own_fips202/mlkem_native/polyvec.h +++ /dev/null @@ -1 +0,0 @@ -../../../mlkem/polyvec.h \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/poly_k.c b/examples/custom_backend/mlkem_native/mlkem/poly_k.c new file mode 120000 index 000000000..392905ab9 --- /dev/null +++ b/examples/custom_backend/mlkem_native/mlkem/poly_k.c @@ -0,0 +1 @@ +../../../../mlkem/poly_k.c \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/poly_k.h b/examples/custom_backend/mlkem_native/mlkem/poly_k.h new file mode 120000 index 000000000..8580e282c --- /dev/null +++ b/examples/custom_backend/mlkem_native/mlkem/poly_k.h @@ -0,0 +1 @@ +../../../../mlkem/poly_k.h \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/polyvec.c b/examples/custom_backend/mlkem_native/mlkem/polyvec.c deleted file mode 120000 index 358c967ff..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/polyvec.c +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/polyvec.c \ No newline at end of file diff --git a/examples/custom_backend/mlkem_native/mlkem/polyvec.h b/examples/custom_backend/mlkem_native/mlkem/polyvec.h deleted file mode 120000 index b3a001d95..000000000 --- a/examples/custom_backend/mlkem_native/mlkem/polyvec.h +++ /dev/null @@ -1 +0,0 @@ -../../../../mlkem/polyvec.h \ No newline at end of file diff --git a/examples/monolithic_build/mlkem_native_monobuild.c b/examples/monolithic_build/mlkem_native_monobuild.c index 35fd29f74..78df7551f 100644 --- a/examples/monolithic_build/mlkem_native_monobuild.c +++ b/examples/monolithic_build/mlkem_native_monobuild.c @@ -21,7 +21,7 @@ #include "mlkem/indcpa.c" #include "mlkem/kem.c" #include "mlkem/poly.c" -#include "mlkem/polyvec.c" +#include "mlkem/poly_k.c" #include "mlkem/sampling.c" #include "mlkem/verify.c" #include "mlkem/zetas.c" @@ -581,127 +581,127 @@ #undef UINT12_LIMIT #endif -/* mlkem/polyvec.c */ +/* mlkem/poly_k.c */ #if defined(poly_cbd_eta1) #undef poly_cbd_eta1 #endif -/* mlkem/polyvec.c */ +/* mlkem/poly_k.c */ #if defined(poly_cbd_eta2) #undef poly_cbd_eta2 #endif -/* mlkem/polyvec.h */ -#if defined(POLYVEC_H) -#undef POLYVEC_H +/* mlkem/poly_k.h */ +#if defined(POLY_K_H) +#undef POLY_K_H #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(poly_compress_du) #undef poly_compress_du #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(poly_compress_dv) #undef poly_compress_dv #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(poly_decompress_du) #undef poly_decompress_du #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(poly_decompress_dv) #undef poly_decompress_dv #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(poly_getnoise_eta1122_4x) #undef poly_getnoise_eta1122_4x #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(poly_getnoise_eta1_4x) #undef poly_getnoise_eta1_4x #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(poly_getnoise_eta2) #undef poly_getnoise_eta2 #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(poly_getnoise_eta2_4x) #undef poly_getnoise_eta2_4x #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec) #undef polyvec #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_add) #undef polyvec_add #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_basemul_acc_montgomery) #undef polyvec_basemul_acc_montgomery #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_basemul_acc_montgomery_cached) #undef polyvec_basemul_acc_montgomery_cached #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_compress_du) #undef polyvec_compress_du #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_decompress_du) #undef polyvec_decompress_du #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_frombytes) #undef polyvec_frombytes #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_invntt_tomont) #undef polyvec_invntt_tomont #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_mulcache) #undef polyvec_mulcache #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_mulcache_compute) #undef polyvec_mulcache_compute #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_ntt) #undef polyvec_ntt #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_reduce) #undef polyvec_reduce #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_tobytes) #undef polyvec_tobytes #endif -/* mlkem/polyvec.h */ +/* mlkem/poly_k.h */ #if defined(polyvec_tomont) #undef polyvec_tomont #endif diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 488cb5f4d..b08ca55bc 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -10,7 +10,7 @@ #include "fips202/fips202x4.h" #include "indcpa.h" #include "poly.h" -#include "polyvec.h" +#include "poly_k.h" #include "randombytes.h" #include "sampling.h" #include "symmetric.h" diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h index 2c4fda3c4..b4d5985bf 100644 --- a/mlkem/indcpa.h +++ b/mlkem/indcpa.h @@ -8,7 +8,7 @@ #include #include "cbmc.h" #include "common.h" -#include "polyvec.h" +#include "poly_k.h" #define gen_matrix MLKEM_NAMESPACE_K(gen_matrix) /************************************************* diff --git a/mlkem/native/aarch64/src/clean_impl.h b/mlkem/native/aarch64/src/clean_impl.h index 805adef12..ec84b3181 100644 --- a/mlkem/native/aarch64/src/clean_impl.h +++ b/mlkem/native/aarch64/src/clean_impl.h @@ -13,7 +13,7 @@ #include "arith_native_aarch64.h" #include "../../../poly.h" -#include "../../../polyvec.h" +#include "../../../poly_k.h" /* Set of primitives that this backend replaces */ #define MLKEM_USE_NATIVE_NTT diff --git a/mlkem/native/aarch64/src/opt_impl.h b/mlkem/native/aarch64/src/opt_impl.h index b92f3adfe..83a3a0a23 100644 --- a/mlkem/native/aarch64/src/opt_impl.h +++ b/mlkem/native/aarch64/src/opt_impl.h @@ -13,7 +13,7 @@ #include "arith_native_aarch64.h" #include "../../../poly.h" -#include "../../../polyvec.h" +#include "../../../poly_k.h" /* Set of primitives that this backend replaces */ #define MLKEM_USE_NATIVE_NTT diff --git a/mlkem/native/api.h b/mlkem/native/api.h index 5732b97ca..24ca8f8e5 100644 --- a/mlkem/native/api.h +++ b/mlkem/native/api.h @@ -24,7 +24,7 @@ #include #include "../poly.h" -#include "../polyvec.h" +#include "../poly_k.h" /* * This is the C<->native interface allowing for the drop-in of diff --git a/mlkem/native/x86_64/src/arith_native_x86_64.h b/mlkem/native/x86_64/src/arith_native_x86_64.h index acf3ae56b..4d9032ff6 100644 --- a/mlkem/native/x86_64/src/arith_native_x86_64.h +++ b/mlkem/native/x86_64/src/arith_native_x86_64.h @@ -9,7 +9,7 @@ #include #include -#include "../../../polyvec.h" +#include "../../../poly_k.h" #include "consts.h" #define REJ_UNIFORM_AVX_NBLOCKS 3 /* See MLKEM_GEN_MATRIX_NBLOCKS */ diff --git a/mlkem/native/x86_64/src/basemul.c b/mlkem/native/x86_64/src/basemul.c index 8a23ddcc3..e66d0473c 100644 --- a/mlkem/native/x86_64/src/basemul.c +++ b/mlkem/native/x86_64/src/basemul.c @@ -8,7 +8,7 @@ #if defined(MLKEM_NATIVE_ARITH_BACKEND_X86_64_DEFAULT) #include "../../../poly.h" -#include "../../../polyvec.h" +#include "../../../poly_k.h" #include "arith_native_x86_64.h" #include "consts.h" diff --git a/mlkem/native/x86_64/src/default_impl.h b/mlkem/native/x86_64/src/default_impl.h index cdbd44da1..8c31831ee 100644 --- a/mlkem/native/x86_64/src/default_impl.h +++ b/mlkem/native/x86_64/src/default_impl.h @@ -13,7 +13,7 @@ #include #include "../../../poly.h" -#include "../../../polyvec.h" +#include "../../../poly_k.h" #include "arith_native_x86_64.h" #define MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER diff --git a/mlkem/polyvec.c b/mlkem/poly_k.c similarity index 99% rename from mlkem/polyvec.c rename to mlkem/poly_k.c index 3ec40630f..cd3bf120c 100644 --- a/mlkem/polyvec.c +++ b/mlkem/poly_k.c @@ -2,7 +2,7 @@ * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 */ -#include "polyvec.h" +#include "poly_k.h" #include #include #include "arith_backend.h" diff --git a/mlkem/polyvec.h b/mlkem/poly_k.h similarity index 99% rename from mlkem/polyvec.h rename to mlkem/poly_k.h index cd3d72349..0aea95912 100644 --- a/mlkem/polyvec.h +++ b/mlkem/poly_k.h @@ -2,8 +2,8 @@ * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 */ -#ifndef POLYVEC_H -#define POLYVEC_H +#ifndef POLY_K_H +#define POLY_K_H #include #include "common.h" diff --git a/proofs/cbmc/invntt_layer/Makefile b/proofs/cbmc/invntt_layer/Makefile index e372b0760..fde0e1370 100644 --- a/proofs/cbmc/invntt_layer/Makefile +++ b/proofs/cbmc/invntt_layer/Makefile @@ -36,7 +36,7 @@ FUNCTION_NAME = invntt_layer # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 9 +CBMC_OBJECT_BITS = 10 # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file diff --git a/proofs/cbmc/matvec_mul/matvec_mul_harness.c b/proofs/cbmc/matvec_mul/matvec_mul_harness.c index 7b7bbd865..28de396ca 100644 --- a/proofs/cbmc/matvec_mul/matvec_mul_harness.c +++ b/proofs/cbmc/matvec_mul/matvec_mul_harness.c @@ -3,7 +3,7 @@ // SPDX-License-Identifier: MIT-0 #include "indcpa.h" -#include "polyvec.h" +#include "poly_k.h" #define matvec_mul MLKEM_NAMESPACE(matvec_mul) void matvec_mul(polyvec *out, polyvec const *a, polyvec const *v, diff --git a/proofs/cbmc/poly_cbd_eta1/Makefile b/proofs/cbmc/poly_cbd_eta1/Makefile index d8a73b209..abfb98bb7 100644 --- a/proofs/cbmc/poly_cbd_eta1/Makefile +++ b/proofs/cbmc/poly_cbd_eta1/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta1 USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/poly_cbd_eta2/Makefile b/proofs/cbmc/poly_cbd_eta2/Makefile index 8c3efb20f..33f04417f 100644 --- a/proofs/cbmc/poly_cbd_eta2/Makefile +++ b/proofs/cbmc/poly_cbd_eta2/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c $(SRCDIR)/mlkem/poly_k.c # Only relevant for K=2 or K=4 ifeq ($(MLKEM_K),2) diff --git a/proofs/cbmc/poly_compress_du/poly_compress_du_harness.c b/proofs/cbmc/poly_compress_du/poly_compress_du_harness.c index c3b06996c..c54aa2cb5 100644 --- a/proofs/cbmc/poly_compress_du/poly_compress_du_harness.c +++ b/proofs/cbmc/poly_compress_du/poly_compress_du_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/poly_compress_dv/poly_compress_dv_harness.c b/proofs/cbmc/poly_compress_dv/poly_compress_dv_harness.c index 685748b7e..4d12e18ba 100644 --- a/proofs/cbmc/poly_compress_dv/poly_compress_dv_harness.c +++ b/proofs/cbmc/poly_compress_dv/poly_compress_dv_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/poly_decompress_du/poly_decompress_du_harness.c b/proofs/cbmc/poly_decompress_du/poly_decompress_du_harness.c index d64f6b68e..445803e4b 100644 --- a/proofs/cbmc/poly_decompress_du/poly_decompress_du_harness.c +++ b/proofs/cbmc/poly_decompress_du/poly_decompress_du_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/poly_decompress_dv/poly_decompress_dv_harness.c b/proofs/cbmc/poly_decompress_dv/poly_decompress_dv_harness.c index 3816fb8a3..5178f16bd 100644 --- a/proofs/cbmc/poly_decompress_dv/poly_decompress_dv_harness.c +++ b/proofs/cbmc/poly_decompress_dv/poly_decompress_dv_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile b/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile index 15dc91293..4b55ef465 100644 --- a/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile +++ b/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c # Only relevant for K=2 ifeq ($(MLKEM_K),2) diff --git a/proofs/cbmc/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c b/proofs/cbmc/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c index 367e10c8c..9d6f65cba 100644 --- a/proofs/cbmc/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c +++ b/proofs/cbmc/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include void harness(void) { diff --git a/proofs/cbmc/poly_getnoise_eta1_4x/Makefile b/proofs/cbmc/poly_getnoise_eta1_4x/Makefile index ec1f04b23..96859a541 100644 --- a/proofs/cbmc/poly_getnoise_eta1_4x/Makefile +++ b/proofs/cbmc/poly_getnoise_eta1_4x/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_getnoise_eta1_4x USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta1 $(MLKEM_NAMESPACE)shake256x4 diff --git a/proofs/cbmc/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c b/proofs/cbmc/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c index 6fc13427e..17df0797c 100644 --- a/proofs/cbmc/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c +++ b/proofs/cbmc/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include void harness(void) { diff --git a/proofs/cbmc/poly_getnoise_eta2/Makefile b/proofs/cbmc/poly_getnoise_eta2/Makefile index f801954b3..b4d1dc859 100644 --- a/proofs/cbmc/poly_getnoise_eta2/Makefile +++ b/proofs/cbmc/poly_getnoise_eta2/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c # Only relevant for K=2 or K=4 ifeq ($(MLKEM_K),2) diff --git a/proofs/cbmc/poly_getnoise_eta2/poly_getnoise_eta2_harness.c b/proofs/cbmc/poly_getnoise_eta2/poly_getnoise_eta2_harness.c index c82ff5508..580ed60ad 100644 --- a/proofs/cbmc/poly_getnoise_eta2/poly_getnoise_eta2_harness.c +++ b/proofs/cbmc/poly_getnoise_eta2/poly_getnoise_eta2_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include void harness(void) { diff --git a/proofs/cbmc/polyvec_add/Makefile b/proofs/cbmc/polyvec_add/Makefile index e54e830ce..2670efe07 100644 --- a/proofs/cbmc/polyvec_add/Makefile +++ b/proofs/cbmc/polyvec_add/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_add.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_add USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_add diff --git a/proofs/cbmc/polyvec_add/polyvec_add_harness.c b/proofs/cbmc/polyvec_add/polyvec_add_harness.c index c849a0cc4..6b09a7018 100644 --- a/proofs/cbmc/polyvec_add/polyvec_add_harness.c +++ b/proofs/cbmc/polyvec_add/polyvec_add_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile index 387f77dbf..1c82e5765 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_mulcache_compute $(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery/polyvec_basemul_acc_montgomery_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery/polyvec_basemul_acc_montgomery_harness.c index 31fbfbd8e..ec978f9c3 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery/polyvec_basemul_acc_montgomery_harness.c +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery/polyvec_basemul_acc_montgomery_harness.c @@ -1,7 +1,7 @@ // Copyright (c) 2024 The mlkem-native project authors // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile index 036e93afa..c47aba795 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_basemul_montgomery_cached $(MLKEM_NAMESPACE)poly_add 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 5f0882fcc..3eb072c4e 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 @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_compress_du/Makefile b/proofs/cbmc/polyvec_compress_du/Makefile index 6d4592c14..a9ec93b56 100644 --- a/proofs/cbmc/polyvec_compress_du/Makefile +++ b/proofs/cbmc/polyvec_compress_du/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_compress_du.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_compress_du USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du 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 d1d471273..92ea6b7ec 100644 --- a/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c +++ b/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c @@ -3,7 +3,7 @@ // SPDX-License-Identifier: MIT-0 AND Apache-2.0 #include "poly.h" -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_decompress_du/Makefile b/proofs/cbmc/polyvec_decompress_du/Makefile index 2ad128295..b013bb381 100644 --- a/proofs/cbmc/polyvec_decompress_du/Makefile +++ b/proofs/cbmc/polyvec_decompress_du/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_decompress_du.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_decompress_du 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 a845e5fd6..1b2de3108 100644 --- a/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c +++ b/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c @@ -3,7 +3,7 @@ // SPDX-License-Identifier: MIT-0 AND Apache-2.0 #include "poly.h" -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_frombytes/Makefile b/proofs/cbmc/polyvec_frombytes/Makefile index aabf8c3f6..9d09c1309 100644 --- a/proofs/cbmc/polyvec_frombytes/Makefile +++ b/proofs/cbmc/polyvec_frombytes/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_frombytes.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_frombytes USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_frombytes diff --git a/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c b/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c index c2edba02a..5dab099c6 100644 --- a/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c +++ b/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include void harness(void) { diff --git a/proofs/cbmc/polyvec_invntt_tomont/Makefile b/proofs/cbmc/polyvec_invntt_tomont/Makefile index 7b8ab296f..4dc0c1068 100644 --- a/proofs/cbmc/polyvec_invntt_tomont/Makefile +++ b/proofs/cbmc/polyvec_invntt_tomont/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_invntt_tomont.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_invntt_tomont USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_invntt_tomont 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 6c5a4fab3..9d8f5e2f0 100644 --- a/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c +++ b/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_mulcache_compute/Makefile b/proofs/cbmc/polyvec_mulcache_compute/Makefile index e6711cbf6..d641360f2 100644 --- a/proofs/cbmc/polyvec_mulcache_compute/Makefile +++ b/proofs/cbmc/polyvec_mulcache_compute/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_mulcache_compute.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_mulcache_compute USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_mulcache_compute 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 0113fa8c6..8b9c54956 100644 --- a/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c +++ b/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_ntt/Makefile b/proofs/cbmc/polyvec_ntt/Makefile index b785bb54e..2409fc7b1 100644 --- a/proofs/cbmc/polyvec_ntt/Makefile +++ b/proofs/cbmc/polyvec_ntt/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_ntt.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_ntt USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_ntt diff --git a/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c index aee8de115..8fc8730aa 100644 --- a/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c +++ b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 AND Apache-2.0 -#include "polyvec.h" +#include "poly_k.h" void harness(void) { diff --git a/proofs/cbmc/polyvec_reduce/Makefile b/proofs/cbmc/polyvec_reduce/Makefile index 07b3aeb08..3c9587c56 100644 --- a/proofs/cbmc/polyvec_reduce/Makefile +++ b/proofs/cbmc/polyvec_reduce/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_reduce.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_reduce USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_reduce diff --git a/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c b/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c index ffc4d7c16..b481a4c31 100644 --- a/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c +++ b/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include void harness(void) { diff --git a/proofs/cbmc/polyvec_tobytes/Makefile b/proofs/cbmc/polyvec_tobytes/Makefile index 3a3c3bcba..3158b0793 100644 --- a/proofs/cbmc/polyvec_tobytes/Makefile +++ b/proofs/cbmc/polyvec_tobytes/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_tobytes.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_tobytes USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_tobytes diff --git a/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c b/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c index 4e1e1bc04..ffca8d213 100644 --- a/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c +++ b/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include void harness(void) { diff --git a/proofs/cbmc/polyvec_tomont/Makefile b/proofs/cbmc/polyvec_tomont/Makefile index 425a41ad0..78ac30814 100644 --- a/proofs/cbmc/polyvec_tomont/Makefile +++ b/proofs/cbmc/polyvec_tomont/Makefile @@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += $(MLKEM_NAMESPACE)polyvec_tomont.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_tomont USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_tomont diff --git a/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c b/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c index 55b1a564c..e1766d1cb 100644 --- a/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c +++ b/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c @@ -2,7 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include void harness(void) { diff --git a/scripts/autogen b/scripts/autogen index f9e7df0ac..a8f07235b 100755 --- a/scripts/autogen +++ b/scripts/autogen @@ -647,7 +647,7 @@ def gen_monolithic_source_file(dry_run=False): k_specific_sources = ["mlkem_native.h", "params.h", "config.h", "common.h", "indcpa.c", "indcpa.h", "kem.c", "kem.h", - "polyvec.c", "polyvec.h" ] + "poly_k.c", "poly_k.h" ] for f in k_specific_sources: if c.endswith(f): return True diff --git a/test/bench_components_mlkem.c b/test/bench_components_mlkem.c index a90a83f4c..d00240513 100644 --- a/test/bench_components_mlkem.c +++ b/test/bench_components_mlkem.c @@ -17,7 +17,7 @@ #include "../mlkem/fips202/keccakf1600.h" #include "../mlkem/indcpa.h" #include "../mlkem/poly.h" -#include "../mlkem/polyvec.h" +#include "../mlkem/poly_k.h" #define NWARMUP 50 #define NITERERATIONS 300