diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f7932a544..c899e6198 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -158,6 +158,9 @@ jobs: - name: monolithic_build_multilevel run: | make run -C examples/monolithic_build_multilevel + - name: multilevel_build + run: | + make run -C examples/multilevel_build build_kat: needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link] strategy: diff --git a/Makefile b/Makefile index 8445b0148..cd4db99df 100644 --- a/Makefile +++ b/Makefile @@ -149,3 +149,4 @@ clean: -make clean -C examples/mlkem_native_as_code_package >/dev/null -make clean -C examples/monolithic_build >/dev/null -make clean -C examples/monolithic_build_multilevel >/dev/null + -make clean -C examples/multilevel_build >/dev/null diff --git a/examples/README.md b/examples/README.md index 7f27501b0..a4594e5ba 100644 --- a/examples/README.md +++ b/examples/README.md @@ -2,23 +2,34 @@ # Usage examples -This directory contains minimal examples demonstrating how to use mlkem-native. +This directory contains minimal examples demonstrating how you can use mlkem-native. -## Using unmodified mlkem-native as a code package +## Single-level build -See [mlkem_native_as_code_package](mlkem_native_as_code_package). +See [mlkem_native_as_code_package](mlkem_native_as_code_package) for a basic example of how to build a single instance +of mlkem-native. -## Using mlkem-native as a code package, bring your own FIPS-202 +## Multi-level build + +See [multilevel_build](multilevel_build) for an example of how to build one instance of mlkem-native per security level, +in such a way that level-independent code is shared. + +## Custom FIPS202 implementation See [bring_your_own_fips202](bring_your_own_fips202) for an example of how to use mlkem-native with your own FIPS-202 implementation. -## Using mlkem-native as a code package, custom config + custom FIPS-202 backend +## Custom config + custom FIPS-202 backend See [custom_backend](custom_backend) for an example of how to use mlkem-native with a custom configuration file and a custom FIPS-202 backend. -## Building mlkem-native with a single compilation unit +## Monobuild See [monolithic_build](monolithic_build) for an example of how to build mlkem-native (with C backend) from a single auto-generated compilation unit. + +## Multi-level monobuild + +See [monolithic_build_multilevel](monolithic_build_multilevel) for an example of how to build all security levels of +mlkem-native (with C backend) inside a single compilation unit, sharing the level-independent code. diff --git a/examples/monolithic_build/README.md b/examples/monolithic_build/README.md index aee6b3472..1c316a966 100644 --- a/examples/monolithic_build/README.md +++ b/examples/monolithic_build/README.md @@ -3,7 +3,7 @@ # Single-level mlkem-native in a single compilation unit This directory contains a minimal example for how to build a single instance of mlkem-native in a single compilation -unit. +unit. Only the C-backend is exercised. The auto-generated source file [mlkem_native_monobuild.c](mlkem_native_monobuild.c) includes all mlkem-native C source files. Moreover, it clears all `#define`s clauses set by mlkem-native at the end, and is hence amenable to multiple diff --git a/examples/monolithic_build/mlkem_native_monobuild.c b/examples/monolithic_build/mlkem_native_monobuild.c index e0f3b0916..d10c9ddb2 100644 --- a/examples/monolithic_build/mlkem_native_monobuild.c +++ b/examples/monolithic_build/mlkem_native_monobuild.c @@ -15,14 +15,11 @@ #include "mlkem/cbd.c" #include "mlkem/debug/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/native/aarch64/src/aarch64_zetas.c" -#include "mlkem/native/aarch64/src/rej_uniform_table.c" -#include "mlkem/native/x86_64/src/basemul.c" -#include "mlkem/native/x86_64/src/consts.c" -#include "mlkem/native/x86_64/src/rej_uniform_avx2.c" -#include "mlkem/native/x86_64/src/rej_uniform_table.c" #include "mlkem/ntt.c" #include "mlkem/poly.c" #include "mlkem/polyvec.c" @@ -30,184 +27,11 @@ #include "mlkem/verify.c" #include "mlkem/zetas.c" -#if !defined(MLKEM_NATIVE_MONOBUILD_NO_FIPS202_SOURCES) -#include "mlkem/fips202/fips202.c" -#include "mlkem/fips202/fips202x4.c" -#include "mlkem/fips202/keccakf1600.c" -#include "mlkem/fips202/native/aarch64/src/keccakf1600_round_constants.c" -#include "mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c" -#endif /* MLKEM_NATIVE_MONOBUILD_NO_FIPS202_SOURCES */ - /* * Undo all #define directives from *.c or *.h files */ -/* mlkem/arith_backend.h */ -#if defined(MLKEM_NATIVE_ARITH_IMPL_H) -#undef MLKEM_NATIVE_ARITH_IMPL_H -#endif - -/* mlkem/cbd.c */ -#if defined(cbd2) -#undef cbd2 -#endif - -/* mlkem/cbd.c */ -#if defined(cbd3) -#undef cbd3 -#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_cbd_eta1) -#undef poly_cbd_eta1 -#endif - -/* mlkem/cbd.h */ -#if defined(poly_cbd_eta2) -#undef poly_cbd_eta2 -#endif - -/* mlkem/cbmc.h */ -#if defined(CBMC_CONCAT) -#undef CBMC_CONCAT -#endif - -/* mlkem/cbmc.h */ -#if defined(CBMC_CONCAT_) -#undef CBMC_CONCAT_ -#endif - -/* mlkem/cbmc.h */ -#if defined(EXISTS) -#undef EXISTS -#endif - -/* mlkem/cbmc.h */ -#if defined(__contract__) -#undef __contract__ -#endif - -/* mlkem/cbmc.h */ -#if defined(__loop__) -#undef __loop__ -#endif - -/* mlkem/cbmc.h */ -#if defined(array_abs_bound) -#undef array_abs_bound -#endif - -/* mlkem/cbmc.h */ -#if defined(array_bound) -#undef array_bound -#endif - -/* mlkem/cbmc.h */ -#if defined(array_bound_core) -#undef array_bound_core -#endif - -/* mlkem/cbmc.h */ -#if defined(assigns) -#undef assigns -#endif - -/* mlkem/cbmc.h */ -#if defined(assume) -#undef assume -#endif - -/* mlkem/cbmc.h */ -#if defined(cassert) -#undef cassert -#endif - -/* mlkem/cbmc.h */ -#if defined(decreases) -#undef decreases -#endif - -/* mlkem/cbmc.h */ -#if defined(ensures) -#undef ensures -#endif - -/* mlkem/cbmc.h */ -#if defined(forall) -#undef forall -#endif - -/* mlkem/cbmc.h */ -#if defined(invariant) -#undef invariant -#endif - -/* mlkem/cbmc.h */ -#if defined(loop_entry) -#undef loop_entry -#endif - -/* mlkem/cbmc.h */ -#if defined(memory_no_alias) -#undef memory_no_alias -#endif - -/* mlkem/cbmc.h */ -#if defined(memory_slice) -#undef memory_slice -#endif - -/* mlkem/cbmc.h */ -#if defined(object_whole) -#undef object_whole -#endif - -/* mlkem/cbmc.h */ -#if defined(old) -#undef old -#endif - -/* mlkem/cbmc.h */ -#if defined(readable) -#undef readable -#endif - -/* mlkem/cbmc.h */ -#if defined(requires) -#undef requires -#endif - -/* mlkem/cbmc.h */ -#if defined(return_value) -#undef return_value -#endif - -/* mlkem/cbmc.h */ -#if defined(same_object) -#undef same_object -#endif - -/* mlkem/cbmc.h */ -#if defined(writeable) -#undef writeable -#endif - /* mlkem/common.h */ #if defined(FIPS202_ASM_NAMESPACE) #undef FIPS202_ASM_NAMESPACE @@ -223,11 +47,21 @@ #undef MLKEM_ASM_NAMESPACE #endif +/* mlkem/common.h */ +#if defined(MLKEM_ASM_NAMESPACE_K) +#undef MLKEM_ASM_NAMESPACE_K +#endif + /* mlkem/common.h */ #if defined(MLKEM_NAMESPACE) #undef MLKEM_NAMESPACE #endif +/* mlkem/common.h */ +#if defined(MLKEM_NAMESPACE_K) +#undef MLKEM_NAMESPACE_K +#endif + /* mlkem/common.h */ #if defined(MLKEM_NATIVE_ARITH_BACKEND_NAME) #undef MLKEM_NATIVE_ARITH_BACKEND_NAME @@ -258,6 +92,16 @@ #undef MLKEM_NATIVE_MAKE_NAMESPACE_ #endif +/* mlkem/common.h */ +#if defined(MLKEM_NATIVE_MAKE_NAMESPACE_K) +#undef MLKEM_NATIVE_MAKE_NAMESPACE_K +#endif + +/* mlkem/common.h */ +#if defined(MLKEM_NATIVE_MAKE_NAMESPACE_K_) +#undef MLKEM_NATIVE_MAKE_NAMESPACE_K_ +#endif + /* mlkem/common.h */ #if defined(PREFIX_UNDERSCORE) #undef PREFIX_UNDERSCORE @@ -308,71 +152,6 @@ #undef MLKEM_NATIVE_FIPS202_BACKEND #endif -/* mlkem/debug/debug.c */ -#if defined(MLKEM_NATIVE_DEBUG_ERROR_HEADER) -#undef MLKEM_NATIVE_DEBUG_ERROR_HEADER -#endif - -/* mlkem/debug/debug.c */ -#if defined(empty_cu_debug) -#undef empty_cu_debug -#endif - -/* mlkem/debug/debug.h */ -#if defined(MLKEM_DEBUG_H) -#undef MLKEM_DEBUG_H -#endif - -/* mlkem/debug/debug.h */ -#if defined(debug_assert) -#undef debug_assert -#endif - -/* mlkem/debug/debug.h */ -#if defined(debug_assert_abs_bound) -#undef debug_assert_abs_bound -#endif - -/* mlkem/debug/debug.h */ -#if defined(debug_assert_abs_bound_2d) -#undef debug_assert_abs_bound_2d -#endif - -/* mlkem/debug/debug.h */ -#if defined(debug_assert_bound) -#undef debug_assert_bound -#endif - -/* mlkem/debug/debug.h */ -#if defined(debug_assert_bound_2d) -#undef debug_assert_bound_2d -#endif - -/* mlkem/debug/debug.h */ -#if defined(mlkem_debug_assert) -#undef mlkem_debug_assert -#endif - -/* mlkem/debug/debug.h */ -#if defined(mlkem_debug_check_bounds) -#undef mlkem_debug_check_bounds -#endif - -/* mlkem/indcpa.c */ -#if defined(MLKEM_GEN_MATRIX_NBLOCKS) -#undef MLKEM_GEN_MATRIX_NBLOCKS -#endif - -/* mlkem/indcpa.c */ -#if defined(gen_matrix_entry) -#undef gen_matrix_entry -#endif - -/* mlkem/indcpa.c */ -#if defined(gen_matrix_entry_x4) -#undef gen_matrix_entry_x4 -#endif - /* mlkem/indcpa.c */ #if defined(matvec_mul) #undef matvec_mul @@ -479,13 +258,23 @@ #endif /* mlkem/mlkem_native.h */ -#if defined(BUILD_INFO_CONCAT) -#undef BUILD_INFO_CONCAT +#if defined(BUILD_INFO_CONCAT2) +#undef BUILD_INFO_CONCAT2 +#endif + +/* mlkem/mlkem_native.h */ +#if defined(BUILD_INFO_CONCAT2_) +#undef BUILD_INFO_CONCAT2_ #endif /* mlkem/mlkem_native.h */ -#if defined(BUILD_INFO_CONCAT_) -#undef BUILD_INFO_CONCAT_ +#if defined(BUILD_INFO_CONCAT3) +#undef BUILD_INFO_CONCAT3 +#endif + +/* mlkem/mlkem_native.h */ +#if defined(BUILD_INFO_CONCAT3_) +#undef BUILD_INFO_CONCAT3_ #endif /* mlkem/mlkem_native.h */ @@ -668,649 +457,716 @@ #undef crypto_kem_keypair_derand #endif -/* mlkem/native/aarch64/clean.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_AARCH64_CLEAN) -#undef MLKEM_NATIVE_ARITH_BACKEND_AARCH64_CLEAN -#endif - -/* mlkem/native/aarch64/clean.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_IMPL) -#undef MLKEM_NATIVE_ARITH_BACKEND_IMPL +/* mlkem/params.h */ +#if defined(KECCAK_WAY) +#undef KECCAK_WAY #endif -/* mlkem/native/aarch64/clean.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_NAME) -#undef MLKEM_NATIVE_ARITH_BACKEND_NAME +/* mlkem/params.h */ +#if defined(MLKEM_DU) +#undef MLKEM_DU #endif -/* mlkem/native/aarch64/clean.h */ -#if defined(MLKEM_NATIVE_ARITH_PROFILE_H) -#undef MLKEM_NATIVE_ARITH_PROFILE_H +/* mlkem/params.h */ +#if defined(MLKEM_DV) +#undef MLKEM_DV #endif -/* mlkem/native/aarch64/opt.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_AARCH64_OPT) -#undef MLKEM_NATIVE_ARITH_BACKEND_AARCH64_OPT +/* mlkem/params.h */ +#if defined(MLKEM_ETA1) +#undef MLKEM_ETA1 #endif -/* mlkem/native/aarch64/opt.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_IMPL) -#undef MLKEM_NATIVE_ARITH_BACKEND_IMPL +/* mlkem/params.h */ +#if defined(MLKEM_ETA2) +#undef MLKEM_ETA2 #endif -/* mlkem/native/aarch64/opt.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_NAME) -#undef MLKEM_NATIVE_ARITH_BACKEND_NAME +/* mlkem/params.h */ +#if defined(MLKEM_INDCCA_CIPHERTEXTBYTES) +#undef MLKEM_INDCCA_CIPHERTEXTBYTES #endif -/* mlkem/native/aarch64/opt.h */ -#if defined(MLKEM_NATIVE_ARITH_PROFILE_H) -#undef MLKEM_NATIVE_ARITH_PROFILE_H +/* mlkem/params.h */ +#if defined(MLKEM_INDCCA_PUBLICKEYBYTES) +#undef MLKEM_INDCCA_PUBLICKEYBYTES #endif -/* mlkem/native/aarch64/src/aarch64_zetas.c */ -#if defined(empty_cu_aarch64_zetas) -#undef empty_cu_aarch64_zetas +/* mlkem/params.h */ +#if defined(MLKEM_INDCCA_SECRETKEYBYTES) +#undef MLKEM_INDCCA_SECRETKEYBYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(MLKEM_AARCH64_NATIVE_H) -#undef MLKEM_AARCH64_NATIVE_H +/* mlkem/params.h */ +#if defined(MLKEM_INDCPA_BYTES) +#undef MLKEM_INDCPA_BYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(aarch64_invntt_zetas_layer01234) -#undef aarch64_invntt_zetas_layer01234 +/* mlkem/params.h */ +#if defined(MLKEM_INDCPA_MSGBYTES) +#undef MLKEM_INDCPA_MSGBYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(aarch64_invntt_zetas_layer56) -#undef aarch64_invntt_zetas_layer56 +/* mlkem/params.h */ +#if defined(MLKEM_INDCPA_PUBLICKEYBYTES) +#undef MLKEM_INDCPA_PUBLICKEYBYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(aarch64_ntt_zetas_layer01234) -#undef aarch64_ntt_zetas_layer01234 +/* mlkem/params.h */ +#if defined(MLKEM_INDCPA_SECRETKEYBYTES) +#undef MLKEM_INDCPA_SECRETKEYBYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(aarch64_ntt_zetas_layer56) -#undef aarch64_ntt_zetas_layer56 +/* mlkem/params.h */ +#if defined(MLKEM_LVL) +#undef MLKEM_LVL #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(aarch64_zetas_mulcache_native) -#undef aarch64_zetas_mulcache_native +/* mlkem/params.h */ +#if defined(MLKEM_N) +#undef MLKEM_N #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(aarch64_zetas_mulcache_twisted_native) -#undef aarch64_zetas_mulcache_twisted_native +/* mlkem/params.h */ +#if defined(MLKEM_POLYBYTES) +#undef MLKEM_POLYBYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(intt_asm_clean) -#undef intt_asm_clean +/* mlkem/params.h */ +#if defined(MLKEM_POLYCOMPRESSEDBYTES_D10) +#undef MLKEM_POLYCOMPRESSEDBYTES_D10 #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(intt_asm_opt) -#undef intt_asm_opt +/* mlkem/params.h */ +#if defined(MLKEM_POLYCOMPRESSEDBYTES_D11) +#undef MLKEM_POLYCOMPRESSEDBYTES_D11 #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(ntt_asm_clean) -#undef ntt_asm_clean +/* mlkem/params.h */ +#if defined(MLKEM_POLYCOMPRESSEDBYTES_D4) +#undef MLKEM_POLYCOMPRESSEDBYTES_D4 #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(ntt_asm_opt) -#undef ntt_asm_opt +/* mlkem/params.h */ +#if defined(MLKEM_POLYCOMPRESSEDBYTES_D5) +#undef MLKEM_POLYCOMPRESSEDBYTES_D5 #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(poly_mulcache_compute_asm_clean) -#undef poly_mulcache_compute_asm_clean +/* mlkem/params.h */ +#if defined(MLKEM_POLYCOMPRESSEDBYTES_DU) +#undef MLKEM_POLYCOMPRESSEDBYTES_DU #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(poly_mulcache_compute_asm_opt) -#undef poly_mulcache_compute_asm_opt +/* mlkem/params.h */ +#if defined(MLKEM_POLYCOMPRESSEDBYTES_DV) +#undef MLKEM_POLYCOMPRESSEDBYTES_DV #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(poly_reduce_asm_clean) -#undef poly_reduce_asm_clean +/* mlkem/params.h */ +#if defined(MLKEM_POLYVECBYTES) +#undef MLKEM_POLYVECBYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(poly_reduce_asm_opt) -#undef poly_reduce_asm_opt +/* mlkem/params.h */ +#if defined(MLKEM_POLYVECCOMPRESSEDBYTES_DU) +#undef MLKEM_POLYVECCOMPRESSEDBYTES_DU #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(poly_tobytes_asm_clean) -#undef poly_tobytes_asm_clean +/* mlkem/params.h */ +#if defined(MLKEM_Q) +#undef MLKEM_Q #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(poly_tobytes_asm_opt) -#undef poly_tobytes_asm_opt +/* mlkem/params.h */ +#if defined(MLKEM_SSBYTES) +#undef MLKEM_SSBYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(poly_tomont_asm_clean) -#undef poly_tomont_asm_clean +/* mlkem/params.h */ +#if defined(MLKEM_SYMBYTES) +#undef MLKEM_SYMBYTES #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(poly_tomont_asm_opt) -#undef poly_tomont_asm_opt +/* mlkem/params.h */ +#if defined(PARAMS_H) +#undef PARAMS_H #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(polyvec_basemul_acc_montgomery_cached_asm_clean) -#undef polyvec_basemul_acc_montgomery_cached_asm_clean +/* mlkem/params.h */ +#if defined(UINT12_LIMIT) +#undef UINT12_LIMIT #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(polyvec_basemul_acc_montgomery_cached_asm_opt) -#undef polyvec_basemul_acc_montgomery_cached_asm_opt +/* mlkem/polyvec.c */ +#if defined(poly_cbd_eta1) +#undef poly_cbd_eta1 #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(rej_uniform_asm_clean) -#undef rej_uniform_asm_clean +/* mlkem/polyvec.c */ +#if defined(poly_cbd_eta2) +#undef poly_cbd_eta2 #endif -/* mlkem/native/aarch64/src/arith_native_aarch64.h */ -#if defined(rej_uniform_table) -#undef rej_uniform_table +/* mlkem/polyvec.h */ +#if defined(POLYVEC_H) +#undef POLYVEC_H #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_NATIVE_ARITH_PROFILE_IMPL_H) -#undef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +/* mlkem/polyvec.h */ +#if defined(poly_compress_du) +#undef poly_compress_du #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_USE_NATIVE_INTT) -#undef MLKEM_USE_NATIVE_INTT +/* mlkem/polyvec.h */ +#if defined(poly_compress_dv) +#undef poly_compress_dv #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_USE_NATIVE_NTT) -#undef MLKEM_USE_NATIVE_NTT +/* mlkem/polyvec.h */ +#if defined(poly_decompress_du) +#undef poly_decompress_du #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED) -#undef MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED +/* mlkem/polyvec.h */ +#if defined(poly_decompress_dv) +#undef poly_decompress_dv #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE) -#undef MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE +/* mlkem/polyvec.h */ +#if defined(poly_getnoise_eta1122_4x) +#undef poly_getnoise_eta1122_4x #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_REDUCE) -#undef MLKEM_USE_NATIVE_POLY_REDUCE +/* mlkem/polyvec.h */ +#if defined(poly_getnoise_eta1_4x) +#undef poly_getnoise_eta1_4x #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_TOBYTES) -#undef MLKEM_USE_NATIVE_POLY_TOBYTES +/* mlkem/polyvec.h */ +#if defined(poly_getnoise_eta2) +#undef poly_getnoise_eta2 #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_TOMONT) -#undef MLKEM_USE_NATIVE_POLY_TOMONT +/* mlkem/polyvec.h */ +#if defined(poly_getnoise_eta2_4x) +#undef poly_getnoise_eta2_4x #endif -/* mlkem/native/aarch64/src/clean_impl.h */ -#if defined(MLKEM_USE_NATIVE_REJ_UNIFORM) -#undef MLKEM_USE_NATIVE_REJ_UNIFORM +/* mlkem/polyvec.h */ +#if defined(polyvec) +#undef polyvec #endif -/* mlkem/native/aarch64/src/consts.h */ -#if defined(MLKEM_NATIVE_AARCH64_CONSTS) -#undef MLKEM_NATIVE_AARCH64_CONSTS +/* mlkem/polyvec.h */ +#if defined(polyvec_add) +#undef polyvec_add #endif -/* mlkem/native/aarch64/src/consts.h */ -#if defined(zetas_mulcache_native) -#undef zetas_mulcache_native +/* mlkem/polyvec.h */ +#if defined(polyvec_basemul_acc_montgomery) +#undef polyvec_basemul_acc_montgomery #endif -/* mlkem/native/aarch64/src/consts.h */ -#if defined(zetas_mulcache_twisted_native) -#undef zetas_mulcache_twisted_native +/* mlkem/polyvec.h */ +#if defined(polyvec_basemul_acc_montgomery_cached) +#undef polyvec_basemul_acc_montgomery_cached #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_NATIVE_ARITH_PROFILE_IMPL_H) -#undef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +/* mlkem/polyvec.h */ +#if defined(polyvec_compress_du) +#undef polyvec_compress_du #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_USE_NATIVE_INTT) -#undef MLKEM_USE_NATIVE_INTT +/* mlkem/polyvec.h */ +#if defined(polyvec_decompress_du) +#undef polyvec_decompress_du #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_USE_NATIVE_NTT) -#undef MLKEM_USE_NATIVE_NTT +/* mlkem/polyvec.h */ +#if defined(polyvec_frombytes) +#undef polyvec_frombytes #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED) -#undef MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED +/* mlkem/polyvec.h */ +#if defined(polyvec_invntt_tomont) +#undef polyvec_invntt_tomont #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE) -#undef MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE +/* mlkem/polyvec.h */ +#if defined(polyvec_mulcache) +#undef polyvec_mulcache #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_REDUCE) -#undef MLKEM_USE_NATIVE_POLY_REDUCE +/* mlkem/polyvec.h */ +#if defined(polyvec_mulcache_compute) +#undef polyvec_mulcache_compute #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_TOBYTES) -#undef MLKEM_USE_NATIVE_POLY_TOBYTES +/* mlkem/polyvec.h */ +#if defined(polyvec_ntt) +#undef polyvec_ntt #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_TOMONT) -#undef MLKEM_USE_NATIVE_POLY_TOMONT +/* mlkem/polyvec.h */ +#if defined(polyvec_reduce) +#undef polyvec_reduce #endif -/* mlkem/native/aarch64/src/opt_impl.h */ -#if defined(MLKEM_USE_NATIVE_REJ_UNIFORM) -#undef MLKEM_USE_NATIVE_REJ_UNIFORM +/* mlkem/polyvec.h */ +#if defined(polyvec_tobytes) +#undef polyvec_tobytes #endif -/* mlkem/native/aarch64/src/rej_uniform_table.c */ -#if defined(empty_cu_aarch64_rej_uniform_table) -#undef empty_cu_aarch64_rej_uniform_table +/* mlkem/polyvec.h */ +#if defined(polyvec_tomont) +#undef polyvec_tomont #endif -/* mlkem/native/api.h */ -#if defined(MLKEM_NATIVE_ARITH_NATIVE_API_H) -#undef MLKEM_NATIVE_ARITH_NATIVE_API_H -#endif -/* mlkem/native/default.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_DEFAULT_H) -#undef MLKEM_NATIVE_ARITH_BACKEND_DEFAULT_H -#endif +#if !defined(MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS) -/* mlkem/native/x86_64/default.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_IMPL) -#undef MLKEM_NATIVE_ARITH_BACKEND_IMPL -#endif +/* + * Undo all #define directives from *.c or *.h files + */ -/* mlkem/native/x86_64/default.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_NAME) -#undef MLKEM_NATIVE_ARITH_BACKEND_NAME +/* mlkem/arith_backend.h */ +#if defined(MLKEM_NATIVE_ARITH_IMPL_H) +#undef MLKEM_NATIVE_ARITH_IMPL_H #endif -/* mlkem/native/x86_64/default.h */ -#if defined(MLKEM_NATIVE_ARITH_BACKEND_X86_64_DEFAULT) -#undef MLKEM_NATIVE_ARITH_BACKEND_X86_64_DEFAULT +/* mlkem/cbd.c */ +#if defined(empty_cu_cbd) +#undef empty_cu_cbd #endif -/* mlkem/native/x86_64/default.h */ -#if defined(MLKEM_NATIVE_ARITH_PROFILE_H) -#undef MLKEM_NATIVE_ARITH_PROFILE_H +/* mlkem/cbd.c */ +#if defined(load24_littleendian) +#undef load24_littleendian #endif -/* mlkem/native/x86_64/src/align.h */ -#if defined(ALIGNED_INT16) -#undef ALIGNED_INT16 +/* mlkem/cbd.c */ +#if defined(load32_littleendian) +#undef load32_littleendian #endif -/* mlkem/native/x86_64/src/align.h */ -#if defined(ALIGNED_UINT8) -#undef ALIGNED_UINT8 +/* mlkem/cbd.h */ +#if defined(CBD_H) +#undef CBD_H #endif -/* mlkem/native/x86_64/src/align.h */ -#if defined(ALIGN_H) -#undef ALIGN_H +/* mlkem/cbd.h */ +#if defined(poly_cbd2) +#undef poly_cbd2 #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(MLKEM_X86_64_NATIVE_H) -#undef MLKEM_X86_64_NATIVE_H +/* mlkem/cbd.h */ +#if defined(poly_cbd3) +#undef poly_cbd3 #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(REJ_UNIFORM_AVX_BUFLEN) -#undef REJ_UNIFORM_AVX_BUFLEN +/* mlkem/cbmc.h */ +#if defined(CBMC_CONCAT) +#undef CBMC_CONCAT #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(REJ_UNIFORM_AVX_NBLOCKS) -#undef REJ_UNIFORM_AVX_NBLOCKS +/* mlkem/cbmc.h */ +#if defined(CBMC_CONCAT_) +#undef CBMC_CONCAT_ #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(basemul_avx2) -#undef basemul_avx2 +/* mlkem/cbmc.h */ +#if defined(EXISTS) +#undef EXISTS #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(invntt_avx2) -#undef invntt_avx2 +/* mlkem/cbmc.h */ +#if defined(__contract__) +#undef __contract__ #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(ntt_avx2) -#undef ntt_avx2 +/* mlkem/cbmc.h */ +#if defined(__loop__) +#undef __loop__ #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(nttfrombytes_avx2) -#undef nttfrombytes_avx2 +/* mlkem/cbmc.h */ +#if defined(array_abs_bound) +#undef array_abs_bound #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(nttpack_avx2) -#undef nttpack_avx2 +/* mlkem/cbmc.h */ +#if defined(array_bound) +#undef array_bound #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(ntttobytes_avx2) -#undef ntttobytes_avx2 +/* mlkem/cbmc.h */ +#if defined(array_bound_core) +#undef array_bound_core #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(nttunpack_avx2) -#undef nttunpack_avx2 +/* mlkem/cbmc.h */ +#if defined(assigns) +#undef assigns #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(polyvec_basemul_acc_montgomery_cached_avx2) -#undef polyvec_basemul_acc_montgomery_cached_avx2 +/* mlkem/cbmc.h */ +#if defined(assume) +#undef assume #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(reduce_avx2) -#undef reduce_avx2 +/* mlkem/cbmc.h */ +#if defined(cassert) +#undef cassert #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(rej_uniform_avx2) -#undef rej_uniform_avx2 +/* mlkem/cbmc.h */ +#if defined(decreases) +#undef decreases #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(rej_uniform_table) -#undef rej_uniform_table +/* mlkem/cbmc.h */ +#if defined(ensures) +#undef ensures #endif -/* mlkem/native/x86_64/src/arith_native_x86_64.h */ -#if defined(tomont_avx2) -#undef tomont_avx2 +/* mlkem/cbmc.h */ +#if defined(forall) +#undef forall #endif -/* mlkem/native/x86_64/src/basemul.c */ -#if defined(empty_cu_avx2_basemul) -#undef empty_cu_avx2_basemul +/* mlkem/cbmc.h */ +#if defined(invariant) +#undef invariant #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XFHI) -#undef AVX2_BACKEND_DATA_OFFSET_16XFHI +/* mlkem/cbmc.h */ +#if defined(loop_entry) +#undef loop_entry #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XFLO) -#undef AVX2_BACKEND_DATA_OFFSET_16XFLO +/* mlkem/cbmc.h */ +#if defined(memory_no_alias) +#undef memory_no_alias #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XMASK) -#undef AVX2_BACKEND_DATA_OFFSET_16XMASK +/* mlkem/cbmc.h */ +#if defined(memory_slice) +#undef memory_slice #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XMONTSQHI) -#undef AVX2_BACKEND_DATA_OFFSET_16XMONTSQHI +/* mlkem/cbmc.h */ +#if defined(object_whole) +#undef object_whole #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XMONTSQLO) -#undef AVX2_BACKEND_DATA_OFFSET_16XMONTSQLO +/* mlkem/cbmc.h */ +#if defined(old) +#undef old #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XQ) -#undef AVX2_BACKEND_DATA_OFFSET_16XQ +/* mlkem/cbmc.h */ +#if defined(readable) +#undef readable #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XQINV) -#undef AVX2_BACKEND_DATA_OFFSET_16XQINV +/* mlkem/cbmc.h */ +#if defined(requires) +#undef requires #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XSHIFT) -#undef AVX2_BACKEND_DATA_OFFSET_16XSHIFT +/* mlkem/cbmc.h */ +#if defined(return_value) +#undef return_value #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XV) -#undef AVX2_BACKEND_DATA_OFFSET_16XV +/* mlkem/cbmc.h */ +#if defined(same_object) +#undef same_object #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_REVIDXB) -#undef AVX2_BACKEND_DATA_OFFSET_REVIDXB +/* mlkem/cbmc.h */ +#if defined(writeable) +#undef writeable #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_REVIDXD) -#undef AVX2_BACKEND_DATA_OFFSET_REVIDXD +/* mlkem/debug/debug.c */ +#if defined(MLKEM_NATIVE_DEBUG_ERROR_HEADER) +#undef MLKEM_NATIVE_DEBUG_ERROR_HEADER #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP) -#undef AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP +/* mlkem/debug/debug.c */ +#if defined(empty_cu_debug) +#undef empty_cu_debug #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(FHI) -#undef FHI +/* mlkem/debug/debug.h */ +#if defined(MLKEM_DEBUG_H) +#undef MLKEM_DEBUG_H #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(FLO) -#undef FLO +/* mlkem/debug/debug.h */ +#if defined(debug_assert) +#undef debug_assert #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(MASK) -#undef MASK +/* mlkem/debug/debug.h */ +#if defined(debug_assert_abs_bound) +#undef debug_assert_abs_bound #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(MONT) -#undef MONT +/* mlkem/debug/debug.h */ +#if defined(debug_assert_abs_bound_2d) +#undef debug_assert_abs_bound_2d +#endif + +/* mlkem/debug/debug.h */ +#if defined(debug_assert_bound) +#undef debug_assert_bound +#endif + +/* mlkem/debug/debug.h */ +#if defined(debug_assert_bound_2d) +#undef debug_assert_bound_2d +#endif + +/* mlkem/debug/debug.h */ +#if defined(mlkem_debug_assert) +#undef mlkem_debug_assert +#endif + +/* mlkem/debug/debug.h */ +#if defined(mlkem_debug_check_bounds) +#undef mlkem_debug_check_bounds +#endif + +/* mlkem/fips202/fips202.c */ +#if defined(empty_cu_fips202) +#undef empty_cu_fips202 +#endif + +/* mlkem/fips202/fips202.c */ +#if defined(keccak_absorb_once) +#undef keccak_absorb_once +#endif + +/* mlkem/fips202/fips202.c */ +#if defined(keccak_squeeze_once) +#undef keccak_squeeze_once +#endif + +/* mlkem/fips202/fips202.c */ +#if defined(keccak_squeezeblocks) +#undef keccak_squeezeblocks +#endif + +/* mlkem/fips202/fips202.c */ +#if defined(shake256ctx) +#undef shake256ctx +#endif + +/* mlkem/fips202/fips202.h */ +#if defined(FIPS202_H) +#undef FIPS202_H +#endif + +/* mlkem/fips202/fips202.h */ +#if defined(SHA3_256_HASHBYTES) +#undef SHA3_256_HASHBYTES +#endif + +/* mlkem/fips202/fips202.h */ +#if defined(SHA3_256_RATE) +#undef SHA3_256_RATE +#endif + +/* mlkem/fips202/fips202.h */ +#if defined(SHA3_384_RATE) +#undef SHA3_384_RATE +#endif + +/* mlkem/fips202/fips202.h */ +#if defined(SHA3_512_HASHBYTES) +#undef SHA3_512_HASHBYTES +#endif + +/* mlkem/fips202/fips202.h */ +#if defined(SHA3_512_RATE) +#undef SHA3_512_RATE +#endif + +/* mlkem/fips202/fips202.h */ +#if defined(SHAKE128_RATE) +#undef SHAKE128_RATE #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(MONTSQHI) -#undef MONTSQHI +/* mlkem/fips202/fips202.h */ +#if defined(SHAKE256_RATE) +#undef SHAKE256_RATE #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(MONTSQLO) -#undef MONTSQLO +/* mlkem/fips202/fips202.h */ +#if defined(sha3_256) +#undef sha3_256 #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(Q) -#undef Q +/* mlkem/fips202/fips202.h */ +#if defined(sha3_512) +#undef sha3_512 #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(QINV) -#undef QINV +/* mlkem/fips202/fips202.h */ +#if defined(shake128_absorb_once) +#undef shake128_absorb_once #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(SHIFT) -#undef SHIFT +/* mlkem/fips202/fips202.h */ +#if defined(shake128_release) +#undef shake128_release #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(V) -#undef V +/* mlkem/fips202/fips202.h */ +#if defined(shake128_squeezeblocks) +#undef shake128_squeezeblocks #endif -/* mlkem/native/x86_64/src/consts.c */ -#if defined(empty_cu_consts) -#undef empty_cu_consts +/* mlkem/fips202/fips202.h */ +#if defined(shake128ctx) +#undef shake128ctx #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XFHI) -#undef AVX2_BACKEND_DATA_OFFSET_16XFHI +/* mlkem/fips202/fips202.h */ +#if defined(shake256) +#undef shake256 #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XFLO) -#undef AVX2_BACKEND_DATA_OFFSET_16XFLO +/* mlkem/fips202/fips202_backend.h */ +#if defined(MLKEM_NATIVE_FIPS202_IMPL_H) +#undef MLKEM_NATIVE_FIPS202_IMPL_H #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XMASK) -#undef AVX2_BACKEND_DATA_OFFSET_16XMASK +/* mlkem/fips202/fips202x4.c */ +#if defined(empty_cu_fips202x4) +#undef empty_cu_fips202x4 #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XMONTSQHI) -#undef AVX2_BACKEND_DATA_OFFSET_16XMONTSQHI +/* mlkem/fips202/fips202x4.c */ +#if defined(keccak_absorb_once_x4) +#undef keccak_absorb_once_x4 #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XMONTSQLO) -#undef AVX2_BACKEND_DATA_OFFSET_16XMONTSQLO +/* mlkem/fips202/fips202x4.c */ +#if defined(keccak_squeezeblocks_x4) +#undef keccak_squeezeblocks_x4 #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XQ) -#undef AVX2_BACKEND_DATA_OFFSET_16XQ +/* mlkem/fips202/fips202x4.c */ +#if defined(shake256x4_absorb_once) +#undef shake256x4_absorb_once #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XQINV) -#undef AVX2_BACKEND_DATA_OFFSET_16XQINV +/* mlkem/fips202/fips202x4.c */ +#if defined(shake256x4_ctx) +#undef shake256x4_ctx #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XSHIFT) -#undef AVX2_BACKEND_DATA_OFFSET_16XSHIFT +/* mlkem/fips202/fips202x4.c */ +#if defined(shake256x4_squeezeblocks) +#undef shake256x4_squeezeblocks #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_16XV) -#undef AVX2_BACKEND_DATA_OFFSET_16XV +/* mlkem/fips202/fips202x4.h */ +#if defined(FIPS_202X4_H) +#undef FIPS_202X4_H #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_REVIDXB) -#undef AVX2_BACKEND_DATA_OFFSET_REVIDXB +/* mlkem/fips202/fips202x4.h */ +#if defined(shake128x4_absorb_once) +#undef shake128x4_absorb_once #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_REVIDXD) -#undef AVX2_BACKEND_DATA_OFFSET_REVIDXD +/* mlkem/fips202/fips202x4.h */ +#if defined(shake128x4_release) +#undef shake128x4_release #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP) -#undef AVX2_BACKEND_DATA_OFFSET_ZETAS_EXP +/* mlkem/fips202/fips202x4.h */ +#if defined(shake128x4_squeezeblocks) +#undef shake128x4_squeezeblocks #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(CONSTS_H) -#undef CONSTS_H +/* mlkem/fips202/fips202x4.h */ +#if defined(shake128x4ctx) +#undef shake128x4ctx #endif -/* mlkem/native/x86_64/src/consts.h */ -#if defined(qdata) -#undef qdata +/* mlkem/fips202/fips202x4.h */ +#if defined(shake256x4) +#undef shake256x4 #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_NATIVE_ARITH_PROFILE_IMPL_H) -#undef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +/* mlkem/fips202/keccakf1600.c */ +#if defined(KeccakF_RoundConstants) +#undef KeccakF_RoundConstants #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_INTT) -#undef MLKEM_USE_NATIVE_INTT +/* mlkem/fips202/keccakf1600.c */ +#if defined(NROUNDS) +#undef NROUNDS #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_NTT) -#undef MLKEM_USE_NATIVE_NTT +/* mlkem/fips202/keccakf1600.c */ +#if defined(ROL) +#undef ROL #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER) -#undef MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER +/* mlkem/fips202/keccakf1600.c */ +#if defined(empty_cu_keccakf1600) +#undef empty_cu_keccakf1600 #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED) -#undef MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED +/* mlkem/fips202/keccakf1600.h */ +#if defined(KECCAKF1600_H) +#undef KECCAKF1600_H #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_FROMBYTES) -#undef MLKEM_USE_NATIVE_POLY_FROMBYTES +/* mlkem/fips202/keccakf1600.h */ +#if defined(KECCAK_LANES) +#undef KECCAK_LANES #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE) -#undef MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE +/* mlkem/fips202/keccakf1600.h */ +#if defined(KeccakF1600_StateExtractBytes) +#undef KeccakF1600_StateExtractBytes #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_REDUCE) -#undef MLKEM_USE_NATIVE_POLY_REDUCE +/* mlkem/fips202/keccakf1600.h */ +#if defined(KeccakF1600_StatePermute) +#undef KeccakF1600_StatePermute #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_TOBYTES) -#undef MLKEM_USE_NATIVE_POLY_TOBYTES +/* mlkem/fips202/keccakf1600.h */ +#if defined(KeccakF1600_StateXORBytes) +#undef KeccakF1600_StateXORBytes #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_POLY_TOMONT) -#undef MLKEM_USE_NATIVE_POLY_TOMONT +/* mlkem/fips202/keccakf1600.h */ +#if defined(KeccakF1600x4_StateExtractBytes) +#undef KeccakF1600x4_StateExtractBytes #endif -/* mlkem/native/x86_64/src/default_impl.h */ -#if defined(MLKEM_USE_NATIVE_REJ_UNIFORM) -#undef MLKEM_USE_NATIVE_REJ_UNIFORM +/* mlkem/fips202/keccakf1600.h */ +#if defined(KeccakF1600x4_StatePermute) +#undef KeccakF1600x4_StatePermute #endif -/* mlkem/native/x86_64/src/rej_uniform_avx2.c */ -#if defined(empty_cu_rej_uniform_avx2) -#undef empty_cu_rej_uniform_avx2 +/* mlkem/fips202/keccakf1600.h */ +#if defined(KeccakF1600x4_StateXORBytes) +#undef KeccakF1600x4_StateXORBytes #endif -/* mlkem/native/x86_64/src/rej_uniform_table.c */ -#if defined(empty_cu_avx2_rej_uniform_table) -#undef empty_cu_avx2_rej_uniform_table +/* mlkem/ntt.c */ +#if defined(empty_cu_ntt) +#undef empty_cu_ntt #endif /* mlkem/ntt.c */ @@ -1353,169 +1209,84 @@ #undef zetas #endif -/* mlkem/params.h */ -#if defined(KECCAK_WAY) -#undef KECCAK_WAY +/* mlkem/poly.c */ +#if defined(empty_cu_poly) +#undef empty_cu_poly #endif -/* mlkem/params.h */ -#if defined(MLKEM_ETA1) -#undef MLKEM_ETA1 +/* mlkem/poly.h */ +#if defined(INVNTT_BOUND) +#undef INVNTT_BOUND #endif -/* mlkem/params.h */ -#if defined(MLKEM_ETA2) -#undef MLKEM_ETA2 +/* mlkem/poly.h */ +#if defined(NTT_BOUND) +#undef NTT_BOUND #endif -/* mlkem/params.h */ -#if defined(MLKEM_INDCCA_CIPHERTEXTBYTES) -#undef MLKEM_INDCCA_CIPHERTEXTBYTES +/* mlkem/poly.h */ +#if defined(POLY_H) +#undef POLY_H #endif -/* mlkem/params.h */ -#if defined(MLKEM_INDCCA_PUBLICKEYBYTES) -#undef MLKEM_INDCCA_PUBLICKEYBYTES +/* mlkem/poly.h */ +#if defined(poly) +#undef poly #endif -/* mlkem/params.h */ -#if defined(MLKEM_INDCCA_SECRETKEYBYTES) -#undef MLKEM_INDCCA_SECRETKEYBYTES +/* mlkem/poly.h */ +#if defined(poly_add) +#undef poly_add #endif -/* mlkem/params.h */ -#if defined(MLKEM_INDCPA_BYTES) -#undef MLKEM_INDCPA_BYTES +/* mlkem/poly.h */ +#if defined(poly_basemul_montgomery_cached) +#undef poly_basemul_montgomery_cached #endif -/* mlkem/params.h */ -#if defined(MLKEM_INDCPA_MSGBYTES) -#undef MLKEM_INDCPA_MSGBYTES +/* mlkem/poly.h */ +#if defined(poly_compress_d10) +#undef poly_compress_d10 #endif -/* mlkem/params.h */ -#if defined(MLKEM_INDCPA_PUBLICKEYBYTES) -#undef MLKEM_INDCPA_PUBLICKEYBYTES +/* mlkem/poly.h */ +#if defined(poly_compress_d11) +#undef poly_compress_d11 #endif -/* mlkem/params.h */ -#if defined(MLKEM_INDCPA_SECRETKEYBYTES) -#undef MLKEM_INDCPA_SECRETKEYBYTES +/* mlkem/poly.h */ +#if defined(poly_compress_d4) +#undef poly_compress_d4 #endif -/* mlkem/params.h */ -#if defined(MLKEM_LVL) -#undef MLKEM_LVL +/* mlkem/poly.h */ +#if defined(poly_compress_d5) +#undef poly_compress_d5 #endif -/* mlkem/params.h */ -#if defined(MLKEM_N) -#undef MLKEM_N +/* mlkem/poly.h */ +#if defined(poly_decompress_d10) +#undef poly_decompress_d10 #endif -/* mlkem/params.h */ -#if defined(MLKEM_POLYBYTES) -#undef MLKEM_POLYBYTES +/* mlkem/poly.h */ +#if defined(poly_decompress_d11) +#undef poly_decompress_d11 #endif -/* mlkem/params.h */ -#if defined(MLKEM_POLYCOMPRESSEDBYTES_DU) -#undef MLKEM_POLYCOMPRESSEDBYTES_DU +/* mlkem/poly.h */ +#if defined(poly_decompress_d4) +#undef poly_decompress_d4 #endif -/* mlkem/params.h */ -#if defined(MLKEM_POLYCOMPRESSEDBYTES_DV) -#undef MLKEM_POLYCOMPRESSEDBYTES_DV +/* mlkem/poly.h */ +#if defined(poly_decompress_d5) +#undef poly_decompress_d5 #endif -/* mlkem/params.h */ -#if defined(MLKEM_POLYVECBYTES) -#undef MLKEM_POLYVECBYTES -#endif - -/* mlkem/params.h */ -#if defined(MLKEM_POLYVECCOMPRESSEDBYTES_DU) -#undef MLKEM_POLYVECCOMPRESSEDBYTES_DU -#endif - -/* mlkem/params.h */ -#if defined(MLKEM_Q) -#undef MLKEM_Q -#endif - -/* mlkem/params.h */ -#if defined(MLKEM_SSBYTES) -#undef MLKEM_SSBYTES -#endif - -/* mlkem/params.h */ -#if defined(MLKEM_SYMBYTES) -#undef MLKEM_SYMBYTES -#endif - -/* mlkem/params.h */ -#if defined(PARAMS_H) -#undef PARAMS_H -#endif - -/* mlkem/params.h */ -#if defined(UINT12_LIMIT) -#undef UINT12_LIMIT -#endif - -/* mlkem/poly.h */ -#if defined(INVNTT_BOUND) -#undef INVNTT_BOUND -#endif - -/* mlkem/poly.h */ -#if defined(NTT_BOUND) -#undef NTT_BOUND -#endif - -/* mlkem/poly.h */ -#if defined(POLY_H) -#undef POLY_H -#endif - -/* mlkem/poly.h */ -#if defined(poly) -#undef poly -#endif - -/* mlkem/poly.h */ -#if defined(poly_add) -#undef poly_add -#endif - -/* mlkem/poly.h */ -#if defined(poly_basemul_montgomery_cached) -#undef poly_basemul_montgomery_cached -#endif - -/* mlkem/poly.h */ -#if defined(poly_compress_du) -#undef poly_compress_du -#endif - -/* mlkem/poly.h */ -#if defined(poly_compress_dv) -#undef poly_compress_dv -#endif - -/* mlkem/poly.h */ -#if defined(poly_decompress_du) -#undef poly_decompress_du -#endif - -/* mlkem/poly.h */ -#if defined(poly_decompress_dv) -#undef poly_decompress_dv -#endif - -/* mlkem/poly.h */ -#if defined(poly_frombytes) -#undef poly_frombytes +/* mlkem/poly.h */ +#if defined(poly_frombytes) +#undef poly_frombytes #endif /* mlkem/poly.h */ @@ -1523,26 +1294,6 @@ #undef poly_frommsg #endif -/* mlkem/poly.h */ -#if defined(poly_getnoise_eta1122_4x) -#undef poly_getnoise_eta1122_4x -#endif - -/* mlkem/poly.h */ -#if defined(poly_getnoise_eta1_4x) -#undef poly_getnoise_eta1_4x -#endif - -/* mlkem/poly.h */ -#if defined(poly_getnoise_eta2) -#undef poly_getnoise_eta2 -#endif - -/* mlkem/poly.h */ -#if defined(poly_getnoise_eta2_4x) -#undef poly_getnoise_eta2_4x -#endif - /* mlkem/poly.h */ #if defined(poly_mulcache) #undef poly_mulcache @@ -1628,79 +1379,9 @@ #undef scalar_signed_to_unsigned_q #endif -/* mlkem/polyvec.h */ -#if defined(POLYVEC_H) -#undef POLYVEC_H -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec) -#undef polyvec -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_add) -#undef polyvec_add -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_basemul_acc_montgomery) -#undef polyvec_basemul_acc_montgomery -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_basemul_acc_montgomery_cached) -#undef polyvec_basemul_acc_montgomery_cached -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_compress_du) -#undef polyvec_compress_du -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_decompress_du) -#undef polyvec_decompress_du -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_frombytes) -#undef polyvec_frombytes -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_invntt_tomont) -#undef polyvec_invntt_tomont -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_mulcache) -#undef polyvec_mulcache -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_mulcache_compute) -#undef polyvec_mulcache_compute -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_ntt) -#undef polyvec_ntt -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_reduce) -#undef polyvec_reduce -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_tobytes) -#undef polyvec_tobytes -#endif - -/* mlkem/polyvec.h */ -#if defined(polyvec_tomont) -#undef polyvec_tomont +/* mlkem/randombytes.h */ +#if defined(RANDOMBYTES_H) +#undef RANDOMBYTES_H #endif /* mlkem/reduce.h */ @@ -1738,6 +1419,21 @@ #undef montgomery_reduce_generic #endif +/* mlkem/rej_uniform.c */ +#if defined(MLKEM_GEN_MATRIX_NBLOCKS) +#undef MLKEM_GEN_MATRIX_NBLOCKS +#endif + +/* mlkem/rej_uniform.c */ +#if defined(empty_cu_rej_uniform) +#undef empty_cu_rej_uniform +#endif + +/* mlkem/rej_uniform.c */ +#if defined(rej_uniform) +#undef rej_uniform +#endif + /* mlkem/rej_uniform.c */ #if defined(rej_uniform_scalar) #undef rej_uniform_scalar @@ -1749,8 +1445,13 @@ #endif /* mlkem/rej_uniform.h */ -#if defined(rej_uniform) -#undef rej_uniform +#if defined(poly_rej_uniform) +#undef poly_rej_uniform +#endif + +/* mlkem/rej_uniform.h */ +#if defined(poly_rej_uniform_x4) +#undef poly_rej_uniform_x4 #endif /* mlkem/symmetric.h */ @@ -1973,491 +1674,9 @@ #undef value_barrier_u8 #endif - -#if !defined(MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS) - -/* - * Undo all #define directives from *.c or *.h files - */ - -/* mlkem/fips202/fips202.c */ -#if defined(keccak_absorb_once) -#undef keccak_absorb_once -#endif - -/* mlkem/fips202/fips202.c */ -#if defined(keccak_squeeze_once) -#undef keccak_squeeze_once -#endif - -/* mlkem/fips202/fips202.c */ -#if defined(keccak_squeezeblocks) -#undef keccak_squeezeblocks -#endif - -/* mlkem/fips202/fips202.c */ -#if defined(shake256ctx) -#undef shake256ctx -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(FIPS202_H) -#undef FIPS202_H -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(SHA3_256_HASHBYTES) -#undef SHA3_256_HASHBYTES -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(SHA3_256_RATE) -#undef SHA3_256_RATE -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(SHA3_384_RATE) -#undef SHA3_384_RATE -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(SHA3_512_HASHBYTES) -#undef SHA3_512_HASHBYTES -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(SHA3_512_RATE) -#undef SHA3_512_RATE -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(SHAKE128_RATE) -#undef SHAKE128_RATE -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(SHAKE256_RATE) -#undef SHAKE256_RATE -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(sha3_256) -#undef sha3_256 -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(sha3_512) -#undef sha3_512 -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(shake128_absorb_once) -#undef shake128_absorb_once -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(shake128_release) -#undef shake128_release -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(shake128_squeezeblocks) -#undef shake128_squeezeblocks -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(shake128ctx) -#undef shake128ctx -#endif - -/* mlkem/fips202/fips202.h */ -#if defined(shake256) -#undef shake256 -#endif - -/* mlkem/fips202/fips202_backend.h */ -#if defined(MLKEM_NATIVE_FIPS202_IMPL_H) -#undef MLKEM_NATIVE_FIPS202_IMPL_H -#endif - -/* mlkem/fips202/fips202x4.c */ -#if defined(keccak_absorb_once_x4) -#undef keccak_absorb_once_x4 -#endif - -/* mlkem/fips202/fips202x4.c */ -#if defined(keccak_squeezeblocks_x4) -#undef keccak_squeezeblocks_x4 -#endif - -/* mlkem/fips202/fips202x4.c */ -#if defined(shake256x4_absorb_once) -#undef shake256x4_absorb_once -#endif - -/* mlkem/fips202/fips202x4.c */ -#if defined(shake256x4_ctx) -#undef shake256x4_ctx -#endif - -/* mlkem/fips202/fips202x4.c */ -#if defined(shake256x4_squeezeblocks) -#undef shake256x4_squeezeblocks -#endif - -/* mlkem/fips202/fips202x4.h */ -#if defined(FIPS_202X4_H) -#undef FIPS_202X4_H -#endif - -/* mlkem/fips202/fips202x4.h */ -#if defined(shake128x4_absorb_once) -#undef shake128x4_absorb_once -#endif - -/* mlkem/fips202/fips202x4.h */ -#if defined(shake128x4_release) -#undef shake128x4_release -#endif - -/* mlkem/fips202/fips202x4.h */ -#if defined(shake128x4_squeezeblocks) -#undef shake128x4_squeezeblocks -#endif - -/* mlkem/fips202/fips202x4.h */ -#if defined(shake128x4ctx) -#undef shake128x4ctx -#endif - -/* mlkem/fips202/fips202x4.h */ -#if defined(shake256x4) -#undef shake256x4 -#endif - -/* mlkem/fips202/keccakf1600.c */ -#if defined(KeccakF_RoundConstants) -#undef KeccakF_RoundConstants -#endif - -/* mlkem/fips202/keccakf1600.c */ -#if defined(NROUNDS) -#undef NROUNDS -#endif - -/* mlkem/fips202/keccakf1600.c */ -#if defined(ROL) -#undef ROL -#endif - -/* mlkem/fips202/keccakf1600.h */ -#if defined(KECCAKF1600_H) -#undef KECCAKF1600_H -#endif - -/* mlkem/fips202/keccakf1600.h */ -#if defined(KECCAK_LANES) -#undef KECCAK_LANES -#endif - -/* mlkem/fips202/keccakf1600.h */ -#if defined(KeccakF1600_StateExtractBytes) -#undef KeccakF1600_StateExtractBytes -#endif - -/* mlkem/fips202/keccakf1600.h */ -#if defined(KeccakF1600_StatePermute) -#undef KeccakF1600_StatePermute -#endif - -/* mlkem/fips202/keccakf1600.h */ -#if defined(KeccakF1600_StateXORBytes) -#undef KeccakF1600_StateXORBytes -#endif - -/* mlkem/fips202/keccakf1600.h */ -#if defined(KeccakF1600x4_StateExtractBytes) -#undef KeccakF1600x4_StateExtractBytes -#endif - -/* mlkem/fips202/keccakf1600.h */ -#if defined(KeccakF1600x4_StatePermute) -#undef KeccakF1600x4_StatePermute -#endif - -/* mlkem/fips202/keccakf1600.h */ -#if defined(KeccakF1600x4_StateXORBytes) -#undef KeccakF1600x4_StateXORBytes -#endif - -/* mlkem/fips202/native/aarch64/cortex_a55.h */ -#if defined(FIPS202_NATIVE_PROFILE_H) -#undef FIPS202_NATIVE_PROFILE_H -#endif - -/* mlkem/fips202/native/aarch64/cortex_a55.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_AARCH64_A55) -#undef MLKEM_NATIVE_FIPS202_BACKEND_AARCH64_A55 -#endif - -/* mlkem/fips202/native/aarch64/cortex_a55.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_IMPL) -#undef MLKEM_NATIVE_FIPS202_BACKEND_IMPL -#endif - -/* mlkem/fips202/native/aarch64/cortex_a55.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_NAME) -#undef MLKEM_NATIVE_FIPS202_BACKEND_NAME -#endif - -/* mlkem/fips202/native/aarch64/default.h */ -#if defined(FIPS202_NATIVE_PROFILE_H) -#undef FIPS202_NATIVE_PROFILE_H -#endif - -/* mlkem/fips202/native/aarch64/default.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_AARCH64_DEFAULT) -#undef MLKEM_NATIVE_FIPS202_BACKEND_AARCH64_DEFAULT -#endif - -/* mlkem/fips202/native/aarch64/default.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_IMPL) -#undef MLKEM_NATIVE_FIPS202_BACKEND_IMPL -#endif - -/* mlkem/fips202/native/aarch64/default.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_NAME) -#undef MLKEM_NATIVE_FIPS202_BACKEND_NAME -#endif - -/* mlkem/fips202/native/aarch64/src/cortex_a55_impl.h */ -#if defined(FIPS202_NATIVE_PROFILE_IMPL_H) -#undef FIPS202_NATIVE_PROFILE_IMPL_H -#endif - -/* mlkem/fips202/native/aarch64/src/cortex_a55_impl.h */ -#if defined(MLKEM_USE_FIPS202_X1_NATIVE) -#undef MLKEM_USE_FIPS202_X1_NATIVE -#endif - -/* mlkem/fips202/native/aarch64/src/default_impl.h */ -#if defined(FIPS202_NATIVE_PROFILE_IMPL_H) -#undef FIPS202_NATIVE_PROFILE_IMPL_H -#endif - -/* mlkem/fips202/native/aarch64/src/default_impl.h */ -#if defined(MLKEM_USE_FIPS202_X1_NATIVE) -#undef MLKEM_USE_FIPS202_X1_NATIVE -#endif - -/* mlkem/fips202/native/aarch64/src/default_impl.h */ -#if defined(MLKEM_USE_FIPS202_X2_NATIVE) -#undef MLKEM_USE_FIPS202_X2_NATIVE -#endif - -/* mlkem/fips202/native/aarch64/src/default_impl.h */ -#if defined(MLKEM_USE_FIPS202_X4_NATIVE) -#undef MLKEM_USE_FIPS202_X4_NATIVE -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(FIPS202_AARCH64_NATIVE_H) -#undef FIPS202_AARCH64_NATIVE_H -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(keccak_f1600_x1_scalar_asm_opt) -#undef keccak_f1600_x1_scalar_asm_opt -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(keccak_f1600_x1_v84a_asm_clean) -#undef keccak_f1600_x1_v84a_asm_clean -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(keccak_f1600_x2_v84a_asm_clean) -#undef keccak_f1600_x2_v84a_asm_clean -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(keccak_f1600_x2_v8a_v84a_asm_hybrid) -#undef keccak_f1600_x2_v8a_v84a_asm_hybrid -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(keccak_f1600_x4_scalar_v84a_asm_hybrid_opt) -#undef keccak_f1600_x4_scalar_v84a_asm_hybrid_opt -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(keccak_f1600_x4_scalar_v8a_asm_hybrid_opt) -#undef keccak_f1600_x4_scalar_v8a_asm_hybrid_opt -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt) -#undef keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt -#endif - -/* mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h */ -#if defined(keccakf1600_round_constants) -#undef keccakf1600_round_constants -#endif - -/* mlkem/fips202/native/aarch64/src/keccakf1600_round_constants.c */ -#if defined(empty_cu_keccakf1600_round_constants) -#undef empty_cu_keccakf1600_round_constants -#endif - -/* mlkem/fips202/native/api.h */ -#if defined(MLKEM_NATIVE_FIPS202_NATIVE_API_H) -#undef MLKEM_NATIVE_FIPS202_NATIVE_API_H -#endif - -/* mlkem/fips202/native/default.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_DEFAULT_H) -#undef MLKEM_NATIVE_FIPS202_BACKEND_DEFAULT_H -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(ANDnu256) -#undef ANDnu256 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(CONST256) -#undef CONST256 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(CONST256_64) -#undef CONST256_64 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(ROL64in256) -#undef ROL64in256 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(ROL64in256_56) -#undef ROL64in256_56 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(ROL64in256_8) -#undef ROL64in256_8 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(SCATTER_STORE256) -#undef SCATTER_STORE256 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(STORE256) -#undef STORE256 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(SnP_laneLengthInBytes) -#undef SnP_laneLengthInBytes -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(XOR256) -#undef XOR256 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(XOReq256) -#undef XOReq256 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(copyFromState) -#undef copyFromState -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(copyStateVariables) -#undef copyStateVariables -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(copyToState) -#undef copyToState -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(declareABCDE) -#undef declareABCDE -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(empty_cu_avx2_keccakx4) -#undef empty_cu_avx2_keccakx4 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(prepareTheta) -#undef prepareTheta -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(rounds24) -#undef rounds24 -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(thetaRhoPiChiIota) -#undef thetaRhoPiChiIota -#endif - -/* mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c */ -#if defined(thetaRhoPiChiIotaPrepareTheta) -#undef thetaRhoPiChiIotaPrepareTheta -#endif - -/* mlkem/fips202/native/x86_64/src/xkcp_impl.h */ -#if defined(KeccakP1600times4_PermuteAll_24rounds) -#undef KeccakP1600times4_PermuteAll_24rounds -#endif - -/* mlkem/fips202/native/x86_64/src/xkcp_impl.h */ -#if defined(MLKEM_NATIVE_FIPS202_PROFILE_IMPL_H) -#undef MLKEM_NATIVE_FIPS202_PROFILE_IMPL_H -#endif - -/* mlkem/fips202/native/x86_64/src/xkcp_impl.h */ -#if defined(MLKEM_USE_FIPS202_X4_NATIVE) -#undef MLKEM_USE_FIPS202_X4_NATIVE -#endif - -/* mlkem/fips202/native/x86_64/xkcp.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_IMPL) -#undef MLKEM_NATIVE_FIPS202_BACKEND_IMPL -#endif - -/* mlkem/fips202/native/x86_64/xkcp.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_NAME) -#undef MLKEM_NATIVE_FIPS202_BACKEND_NAME -#endif - -/* mlkem/fips202/native/x86_64/xkcp.h */ -#if defined(MLKEM_NATIVE_FIPS202_BACKEND_X86_64_XKCP) -#undef MLKEM_NATIVE_FIPS202_BACKEND_X86_64_XKCP -#endif - -/* mlkem/fips202/native/x86_64/xkcp.h */ -#if defined(MLKEM_NATIVE_FIPS202_PROFILE_H) -#undef MLKEM_NATIVE_FIPS202_PROFILE_H -#endif - -/* mlkem/randombytes.h */ -#if defined(RANDOMBYTES_H) -#undef RANDOMBYTES_H +/* mlkem/zetas.c */ +#if defined(empty_cu_zetas) +#undef empty_cu_zetas #endif #endif /* MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS */ diff --git a/examples/monolithic_build_multilevel/README.md b/examples/monolithic_build_multilevel/README.md index d1a9c8914..78db9cecf 100644 --- a/examples/monolithic_build_multilevel/README.md +++ b/examples/monolithic_build_multilevel/README.md @@ -3,7 +3,7 @@ # Multi-level mlkem-native in a single compilation unit This directory contains a minimal example for how to build multiple instances of mlkem-native in a single compilation -unit. +unit. Only the C-backend is exercised. The auto-generated source file [mlkem_native_monobuild.c](mlkem_native_monobuild.c) includes all mlkem-native C source files. Moreover, it clears all `#define`s clauses set by mlkem-native at the end, and is hence amenable to multiple @@ -17,19 +17,33 @@ appropriately first, and then includes the monobuild: ```C /* Three instances of mlkem-native for all security levels */ +/* Include level-independent code */ +#define MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED +#define MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS + #define MLKEM_NATIVE_CONFIG_FILE "config_512.h" #include "mlkem_native_monobuild.c" #undef MLKEM_NATIVE_CONFIG_FILE -#define MLKEM_NATIVE_CONFIG_FILE "config_768.h" +/* Exclude level-independent code */ +#undef MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED +#define MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED + +#define MLKEM_NATIVE_CONFIG_FILE "config_1024.h" #include "mlkem_native_monobuild.c" #undef MLKEM_NATIVE_CONFIG_FILE -#define MLKEM_NATIVE_CONFIG_FILE "config_1024.h" +#define MLKEM_NATIVE_CONFIG_FILE "config_768.h" +#undef MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS #include "mlkem_native_monobuild.c" #undef MLKEM_NATIVE_CONFIG_FILE ``` +Note the setting `MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED` which forces the inclusion of all level-independent +code in the MLKEM-512 build, and the setting `MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED`, which drops all +level-independent code in the subsequent builds. Finally, `MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS` entails that +`mlkem_native_monobuild.c` does not `#undefine` the `#define` clauses from level-independent files. + To make the monolithic multi-level build accessible from the application sources, we provide [mlkem_native_all.h](mlkem_native_all.h), which includes [mlkem_native.h](../../mlkem/mlkem_native.h) once per configuration. Note that we don't refer to the configuration using `MLKEM_NATIVE_CONFIG_FILE`, but by setting diff --git a/examples/monolithic_build_multilevel/config_1024.h b/examples/monolithic_build_multilevel/config_1024.h index db6a54033..a8ac69c87 100644 --- a/examples/monolithic_build_multilevel/config_1024.h +++ b/examples/monolithic_build_multilevel/config_1024.h @@ -46,7 +46,8 @@ * This can also be set using CFLAGS. * *****************************************************************************/ -#define MLKEM_NAMESPACE_PREFIX mlkem1024 +#define MLKEM_NAMESPACE_PREFIX mlkem +#define MLKEM_NAMESPACE_PREFIX_ADD_LEVEL /****************************************************************************** * Name: FIPS202_NAMESPACE_PREFIX diff --git a/examples/monolithic_build_multilevel/config_512.h b/examples/monolithic_build_multilevel/config_512.h index a7c7e2924..870569fe9 100644 --- a/examples/monolithic_build_multilevel/config_512.h +++ b/examples/monolithic_build_multilevel/config_512.h @@ -46,7 +46,8 @@ * This can also be set using CFLAGS. * *****************************************************************************/ -#define MLKEM_NAMESPACE_PREFIX mlkem512 +#define MLKEM_NAMESPACE_PREFIX mlkem +#define MLKEM_NAMESPACE_PREFIX_ADD_LEVEL /****************************************************************************** * Name: FIPS202_NAMESPACE_PREFIX diff --git a/examples/monolithic_build_multilevel/config_768.h b/examples/monolithic_build_multilevel/config_768.h index fc66b7952..244d3af1e 100644 --- a/examples/monolithic_build_multilevel/config_768.h +++ b/examples/monolithic_build_multilevel/config_768.h @@ -46,7 +46,8 @@ * This can also be set using CFLAGS. * *****************************************************************************/ -#define MLKEM_NAMESPACE_PREFIX mlkem768 +#define MLKEM_NAMESPACE_PREFIX mlkem +#define MLKEM_NAMESPACE_PREFIX_ADD_LEVEL /****************************************************************************** * Name: FIPS202_NAMESPACE_PREFIX diff --git a/examples/monolithic_build_multilevel/mlkem_native_all.c b/examples/monolithic_build_multilevel/mlkem_native_all.c index cc5059611..f5109b8b0 100644 --- a/examples/monolithic_build_multilevel/mlkem_native_all.c +++ b/examples/monolithic_build_multilevel/mlkem_native_all.c @@ -3,21 +3,27 @@ * SPDX-License-Identifier: Apache-2.0 */ +#define MLKEM_NATIVE_MULTILEVEL_BUILD + /* Three instances of mlkem-native for all security levels */ +/* Include level-independent code */ +#define MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED #define MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS #define MLKEM_NATIVE_CONFIG_FILE "config_512.h" #include "mlkem_native_monobuild.c" #undef MLKEM_NATIVE_CONFIG_FILE -#define MLKEM_NATIVE_MONOBUILD_NO_FIPS202_SOURCES +/* Exclude level-independent code */ +#undef MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED +#define MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED -#define MLKEM_NATIVE_CONFIG_FILE "config_768.h" +#define MLKEM_NATIVE_CONFIG_FILE "config_1024.h" #include "mlkem_native_monobuild.c" #undef MLKEM_NATIVE_CONFIG_FILE -#define MLKEM_NATIVE_CONFIG_FILE "config_1024.h" +#define MLKEM_NATIVE_CONFIG_FILE "config_768.h" #undef MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS #include "mlkem_native_monobuild.c" #undef MLKEM_NATIVE_CONFIG_FILE diff --git a/examples/multilevel_build/.gitignore b/examples/multilevel_build/.gitignore new file mode 100644 index 000000000..cd7c285d8 --- /dev/null +++ b/examples/multilevel_build/.gitignore @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +build diff --git a/examples/multilevel_build/Makefile b/examples/multilevel_build/Makefile new file mode 100644 index 000000000..17364cf07 --- /dev/null +++ b/examples/multilevel_build/Makefile @@ -0,0 +1,109 @@ +# (SPDX-License-Identifier: CC-BY-4.0) + +.PHONY: build run clean mlkem512_objs mlkem768_objs mlkem1024_objs mlkem_objs +.DEFAULT_GOAL := all + +Q ?= @ +# Append cross-prefix for cross compilation +# Remove or ignore for native builds +CC ?= gcc +# When called from the root Makefile, CROSS_PREFIX has already been added here +ifeq (,$(findstring $(CROSS_PREFIX),$(CC))) +CC := $(CROSS_PREFIX)$(CC) +endif + +# Part A: +# +# mlkem-native source and header files +# +# If you are not concerned about minimizing for a specific backend, +# you can just include _all_ source files into your build. +MLKEM_NATIVE_SOURCE_ALL := $(wildcard \ + mlkem_native/**/*.c \ + mlkem_native/**/**/*.c \ + mlkem_native/**/**/**/*.c \ + mlkem_native/**/**/**/**/*.c) +MLKEM_NATIVE_SOURCE:=$(foreach S,$(MLKEM_NATIVE_SOURCE_ALL),\ + $(if $(findstring /native/,$S),,$S)) + +BUILD_DIR=build +MLKEM512_DIR = $(BUILD_DIR)/mlkem512 +MLKEM768_DIR = $(BUILD_DIR)/mlkem768 +MLKEM1024_DIR = $(BUILD_DIR)/mlkem1024 + +MLKEM512_OBJS=$(patsubst %,$(MLKEM512_DIR)/%.o,$(MLKEM_NATIVE_SOURCE)) +MLKEM768_OBJS=$(patsubst %,$(MLKEM768_DIR)/%.o,$(MLKEM_NATIVE_SOURCE)) +MLKEM1024_OBJS=$(patsubst %,$(MLKEM1024_DIR)/%.o,$(MLKEM_NATIVE_SOURCE)) + +$(MLKEM512_OBJS): $(MLKEM512_DIR)/%.c.o: %.c + $(Q)[ -d $(@D) ] || mkdir -p $(@D) + $(Q)$(CC) -DMLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED -DMLKEM_K=2 $(CFLAGS) -c $^ -o $@ + +$(MLKEM768_OBJS): $(MLKEM768_DIR)/%.c.o: %.c + $(Q)[ -d $(@D) ] || mkdir -p $(@D) + $(Q)$(CC) -DMLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED -DMLKEM_K=3 $(CFLAGS) -c $^ -o $@ + +$(MLKEM1024_OBJS): $(MLKEM1024_DIR)/%.c.o: %.c + $(Q)[ -d $(@D) ] || mkdir -p $(@D) + $(Q)$(CC) -DMLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED -DMLKEM_K=4 $(CFLAGS) -c $^ -o $@ + +mlkem512_objs: $(MLKEM512_OBJS) +mlkem768_objs: $(MLKEM768_OBJS) +mlkem1024_objs: $(MLKEM1024_OBJS) +mlkem_objs: mlkem512_objs mlkem768_objs mlkem1024_objs + +# Part B: +# +# Random number generator +# +# !!! WARNING !!! +# +# The randombytes() implementation used here is for TESTING ONLY. +# You MUST NOT use this implementation outside of testing. +# +# !!! WARNING !!! +RNG_SOURCE=$(wildcard test_only_rng/*.c) + +# Part C: +# +# Your application source code +APP_SOURCE=$(wildcard *.c) + +BIN=test_binary + +CFLAGS := \ + -Wall \ + -Wextra \ + -Werror \ + -Wmissing-prototypes \ + -Wshadow \ + -Werror \ + -Wpointer-arith \ + -Wredundant-decls \ + -Wno-long-long \ + -Wno-unknown-pragmas \ + -Wno-unused-command-line-argument \ + -fomit-frame-pointer \ + -DMLKEM_NAMESPACE_PREFIX=mlkem \ + -DMLKEM_NAMESPACE_PREFIX_ADD_LEVEL\ + -std=c99 \ + -pedantic \ + -MMD \ + $(CFLAGS) + +BINARY_NAME_FULL=$(BUILD_DIR)/$(BIN) + +$(BINARY_NAME_FULL): $(APP_SOURCE) $(RNG_SOURCE) $(MLKEM512_OBJS) $(MLKEM768_OBJS) $(MLKEM1024_OBJS) + echo "$@" + mkdir -p $(BUILD_DIR) + $(CC) $(CFLAGS) $^ -o $@ + +all: build + +build: $(BINARY_NAME_FULL) + +run: $(BINARY_NAME_FULL) + $(EXEC_WRAPPER) ./$(BINARY_NAME_FULL) + +clean: + rm -rf $(BUILD_DIR) diff --git a/examples/multilevel_build/README.md b/examples/multilevel_build/README.md new file mode 100644 index 000000000..f4d0329b9 --- /dev/null +++ b/examples/multilevel_build/README.md @@ -0,0 +1,18 @@ +[//]: # (SPDX-License-Identifier: CC-BY-4.0) + +# Multi-level build + +This directory contains a minimal example for how to build mlkem-native with support for all 3 security levels +MLKEM-512, MLKEM-768, and MLKEM-1024, and so that level-independent code is shared. In this example, only the C-backend +of mlkem-native is used. + +The library is built 3 times in different build directories `build/mlkem{512,768,1024}`. For the MLKEM-512 build, we set +`MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED` to force the inclusion of all level-independent code in the +MLKEM512-build. For MLKEM-768 and MLKEM-1024, we set `MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED` to not include any +level-independent code. Finally, we use the common namespace prefix `mlkem` as `MLKEM_NAMESPACE_PREFIX` for all three +builds, but set `MLKEM_NAMESPACE_PREFIX_ADD_LEVEL` to additionally suffix level-dependent functions with `512/768/1024`, +while level-independent functions are named `mlkem_xxx`. + +## Usage + +Build this example with `make build`, run with `make run`. diff --git a/examples/multilevel_build/main.c b/examples/multilevel_build/main.c new file mode 100644 index 000000000..4e512b592 --- /dev/null +++ b/examples/multilevel_build/main.c @@ -0,0 +1,111 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#include +#include +#include + +#include "mlkem_native_all.h" + +static int test_keys_mlkem512(void) +{ + uint8_t pk[MLKEM512_PUBLICKEYBYTES]; + uint8_t sk[MLKEM512_SECRETKEYBYTES]; + uint8_t ct[MLKEM512_CIPHERTEXTBYTES]; + uint8_t key_a[MLKEM512_BYTES]; + uint8_t key_b[MLKEM512_BYTES]; + + /* Alice generates a public key */ + mlkem512_keypair(pk, sk); + + /* Bob derives a secret key and creates a response */ + mlkem512_enc(ct, key_b, pk); + + /* Alice uses Bobs response to get her shared key */ + mlkem512_dec(key_a, ct, sk); + + if (memcmp(key_a, key_b, MLKEM512_BYTES)) + { + printf("[MLKEM-512] ERROR keys\n"); + return 1; + } + + printf("[MLKEM-512] OK\n"); + return 0; +} + +static int test_keys_mlkem768(void) +{ + uint8_t pk[MLKEM768_PUBLICKEYBYTES]; + uint8_t sk[MLKEM768_SECRETKEYBYTES]; + uint8_t ct[MLKEM768_CIPHERTEXTBYTES]; + uint8_t key_a[MLKEM768_BYTES]; + uint8_t key_b[MLKEM768_BYTES]; + + /* Alice generates a public key */ + mlkem768_keypair(pk, sk); + + /* Bob derives a secret key and creates a response */ + mlkem768_enc(ct, key_b, pk); + + /* Alice uses Bobs response to get her shared key */ + mlkem768_dec(key_a, ct, sk); + + if (memcmp(key_a, key_b, MLKEM768_BYTES)) + { + printf("[MLKEM-768] ERROR keys\n"); + return 1; + } + + printf("[MLKEM-768] OK\n"); + return 0; +} + +static int test_keys_mlkem1024(void) +{ + uint8_t pk[MLKEM1024_PUBLICKEYBYTES]; + uint8_t sk[MLKEM1024_SECRETKEYBYTES]; + uint8_t ct[MLKEM1024_CIPHERTEXTBYTES]; + uint8_t key_a[MLKEM1024_BYTES]; + uint8_t key_b[MLKEM1024_BYTES]; + + /* Alice generates a public key */ + mlkem1024_keypair(pk, sk); + + /* Bob derives a secret key and creates a response */ + mlkem1024_enc(ct, key_b, pk); + + /* Alice uses Bobs response to get her shared key */ + mlkem1024_dec(key_a, ct, sk); + + if (memcmp(key_a, key_b, MLKEM1024_BYTES)) + { + printf("[MLKEM-1024] ERROR keys\n"); + return 1; + } + + printf("[MLKEM-1024] OK\n"); + return 0; +} + +int main(void) +{ + if (test_keys_mlkem512() != 0) + { + return 1; + } + + if (test_keys_mlkem768() != 0) + { + return 1; + } + + if (test_keys_mlkem1024() != 0) + { + return 1; + } + + return 0; +} diff --git a/examples/multilevel_build/mlkem_native/mlkem b/examples/multilevel_build/mlkem_native/mlkem new file mode 120000 index 000000000..f4ec7bdb2 --- /dev/null +++ b/examples/multilevel_build/mlkem_native/mlkem @@ -0,0 +1 @@ +../../../mlkem \ No newline at end of file diff --git a/examples/multilevel_build/mlkem_native_all.h b/examples/multilevel_build/mlkem_native_all.h new file mode 100644 index 000000000..40c4cef53 --- /dev/null +++ b/examples/multilevel_build/mlkem_native_all.h @@ -0,0 +1,39 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#if !defined(MLKEM_NATIVE_ALL_H) +#define MLKEM_NATIVE_ALL_H + +/* API for MLKEM-512 */ +#define BUILD_INFO_LVL 512 +#define BUILD_INFO_NAMESPACE(sym) mlkem512_##sym +#define BUILD_INFO_NO_STANDARD_API +#include "mlkem_native/mlkem/mlkem_native.h" +#undef BUILD_INFO_LVL +#undef BUILD_INFO_NAMESPACE +#undef BUILD_INFO_NO_STANDARD_API +#undef MLKEM_NATIVE_H + +/* API for MLKEM-768 */ +#define BUILD_INFO_LVL 768 +#define BUILD_INFO_NAMESPACE(sym) mlkem768_##sym +#define BUILD_INFO_NO_STANDARD_API +#include "mlkem_native/mlkem/mlkem_native.h" +#undef BUILD_INFO_LVL +#undef BUILD_INFO_NAMESPACE +#undef BUILD_INFO_NO_STANDARD_API +#undef MLKEM_NATIVE_H + +/* API for MLKEM-1024 */ +#define BUILD_INFO_LVL 1024 +#define BUILD_INFO_NAMESPACE(sym) mlkem1024_##sym +#define BUILD_INFO_NO_STANDARD_API +#include "mlkem_native/mlkem/mlkem_native.h" +#undef BUILD_INFO_LVL +#undef BUILD_INFO_NAMESPACE +#undef BUILD_INFO_NO_STANDARD_API +#undef MLKEM_NATIVE_H + +#endif /* MLKEM_NATIVE_ALL_H */ diff --git a/examples/multilevel_build/test_only_rng/notrandombytes.c b/examples/multilevel_build/test_only_rng/notrandombytes.c new file mode 100644 index 000000000..909518b82 --- /dev/null +++ b/examples/multilevel_build/test_only_rng/notrandombytes.c @@ -0,0 +1,93 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: LicenseRef-PD-hp OR CC0-1.0 OR 0BSD OR MIT-0 OR MI + * Based on https://cr.yp.to/papers.html#surf by Daniel. J. Bernstein + */ + +/** + * WARNING + * + * The randombytes() implementation in this file is for TESTING ONLY. + * You MUST NOT use this implementation outside of testing. + * + */ + +#include +#include "../mlkem_native/mlkem/randombytes.h" + +static uint32_t seed[32] = {3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5, 8, 9, 7, 9, 3, + 2, 3, 8, 4, 6, 2, 6, 4, 3, 3, 8, 3, 2, 7, 9, 5}; +static uint32_t in[12]; +static uint32_t out[8]; +static int32_t outleft = 0; + +#define ROTATE(x, b) (((x) << (b)) | ((x) >> (32 - (b)))) +#define MUSH(i, b) x = t[i] += (((x ^ seed[i]) + sum) ^ ROTATE(x, b)); + +static void surf(void) +{ + uint32_t t[12]; + uint32_t x; + uint32_t sum = 0; + int32_t r; + int32_t i; + int32_t loop; + + for (i = 0; i < 12; ++i) + { + t[i] = in[i] ^ seed[12 + i]; + } + for (i = 0; i < 8; ++i) + { + out[i] = seed[24 + i]; + } + x = t[11]; + for (loop = 0; loop < 2; ++loop) + { + for (r = 0; r < 16; ++r) + { + sum += 0x9e3779b9; + MUSH(0, 5) + MUSH(1, 7) + MUSH(2, 9) + MUSH(3, 13) + MUSH(4, 5) + MUSH(5, 7) + MUSH(6, 9) + MUSH(7, 13) + MUSH(8, 5) + MUSH(9, 7) + MUSH(10, 9) + MUSH(11, 13) + } + for (i = 0; i < 8; ++i) + { + out[i] ^= t[i + 4]; + } + } +} + +void randombytes(uint8_t *buf, size_t n) +{ + while (n > 0) + { + if (!outleft) + { + if (!++in[0]) + { + if (!++in[1]) + { + if (!++in[2]) + { + ++in[3]; + } + } + } + surf(); + outleft = 8; + } + *buf = (uint8_t)out[--outleft]; + ++buf; + --n; + } +} diff --git a/mlkem/cbd.c b/mlkem/cbd.c index 35b2a3dda..1e6b7c5d1 100644 --- a/mlkem/cbd.c +++ b/mlkem/cbd.c @@ -2,8 +2,11 @@ * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 */ -#include "cbd.h" +#include "common.h" +#ifndef MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED + #include +#include "cbd.h" /* Static namespacing * This is to facilitate building multiple instances @@ -11,8 +14,6 @@ * within a single compilation unit. */ #define load32_littleendian MLKEM_NAMESPACE(load32_littleendian) #define load24_littleendian MLKEM_NAMESPACE(load24_littleendian) -#define cbd2 MLKEM_NAMESPACE(cbd2) -#define cbd3 MLKEM_NAMESPACE(cbd3) /* End of static namespacing */ /************************************************* @@ -35,39 +36,8 @@ static uint32_t load32_littleendian(const uint8_t x[4]) return r; } -#if 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; -} -#endif /* MLKEM_ETA1 == 3 */ - -/************************************************* - * Name: 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 - **************************************************/ -static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]) +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++) @@ -92,19 +62,29 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]) } } -#if MLKEM_ETA1 == 3 +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == 3 /************************************************* - * Name: cbd3 + * Name: load24_littleendian * - * Description: Given an array of uniformly random bytes, compute - * polynomial with coefficients distributed according to - * a centered binomial distribution with parameter eta=3. + * Description: load 3 bytes into a 32-bit integer + * in little-endian order. * 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 + * Arguments: - const uint8_t *x: pointer to input byte array + * + * Returns 32-bit unsigned integer loaded from x (most significant byte is zero) **************************************************/ -static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]) +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++) @@ -129,28 +109,12 @@ static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]) } } } -#endif /* MLKEM_ETA1 == 3 */ +#endif /* defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == \ + 3 */ -MLKEM_NATIVE_INTERNAL_API -void poly_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4]) -{ -#if MLKEM_ETA1 == 2 - cbd2(r, buf); -#elif MLKEM_ETA1 == 3 - cbd3(r, buf); -#else -#error "This implementation requires eta1 in {2,3}" -#endif -} +#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ -#if MLKEM_K == 2 || MLKEM_K == 4 -MLKEM_NATIVE_INTERNAL_API -void poly_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4]) -{ -#if MLKEM_ETA2 == 2 - cbd2(r, buf); -#else -#error "This implementation requires eta2 = 2" -#endif -} -#endif /* MLKEM_K == 2 || MLKEM_K == 4 */ +#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 index 15db89570..54c1f5b90 100644 --- a/mlkem/cbd.h +++ b/mlkem/cbd.h @@ -9,46 +9,35 @@ #include "common.h" #include "poly.h" -#define poly_cbd_eta1 MLKEM_NAMESPACE(poly_cbd_eta1) +#define poly_cbd2 MLKEM_NAMESPACE(poly_cbd2) /************************************************* - * Name: poly_cbd_eta1 + * Name: poly_cbd2 * * Description: Given an array of uniformly random bytes, compute * polynomial with coefficients distributed according to - * a centered binomial distribution with parameter MLKEM_ETA1. + * 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_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4]) -__contract__( - requires(memory_no_alias(r, sizeof(poly))) - requires(memory_no_alias(buf, MLKEM_ETA1 * MLKEM_N / 4)) - assigns(memory_slice(r, sizeof(poly))) - ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_ETA1 + 1)) -); +void poly_cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]); -#if MLKEM_K == 2 || MLKEM_K == 4 -#define poly_cbd_eta2 MLKEM_NAMESPACE(poly_cbd_eta2) +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_ETA1 == 3 +#define poly_cbd3 MLKEM_NAMESPACE(poly_cbd3) /************************************************* - * Name: poly_cbd_eta1 + * Name: poly_cbd3 * * Description: Given an array of uniformly random bytes, compute * polynomial with coefficients distributed according to - * a centered binomial distribution with parameter MLKEM_ETA2. + * 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_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4]) -__contract__( - requires(memory_no_alias(r, sizeof(poly))) - requires(memory_no_alias(buf, MLKEM_ETA2 * MLKEM_N / 4)) - assigns(memory_slice(r, sizeof(poly))) - ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1)) -); -#endif /* MLKEM_K == 2 || MLKEM_K == 4 */ +void poly_cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]); +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD || MLKEM_ETA1 == 3 */ -#endif +#endif /* CBD_H */ diff --git a/mlkem/common.h b/mlkem/common.h index da886780c..4ffe0a74f 100644 --- a/mlkem/common.h +++ b/mlkem/common.h @@ -49,16 +49,28 @@ #define MLKEM_NAMESPACE(s) \ MLKEM_NATIVE_MAKE_NAMESPACE(MLKEM_NAMESPACE_PREFIX, s) +#if defined(MLKEM_NAMESPACE_PREFIX_ADD_LEVEL) +#define MLKEM_NATIVE_MAKE_NAMESPACE_K_(x1, x2, x3) x1##x2##_##x3 +#define MLKEM_NATIVE_MAKE_NAMESPACE_K(x1, x2, x3) \ + MLKEM_NATIVE_MAKE_NAMESPACE_K_(x1, x2, x3) +#define MLKEM_NAMESPACE_K(s) \ + MLKEM_NATIVE_MAKE_NAMESPACE_K(MLKEM_NAMESPACE_PREFIX, MLKEM_LVL, s) +#else +#define MLKEM_NAMESPACE_K(s) MLKEM_NAMESPACE(s) +#endif + /* On Apple platforms, we need to emit leading underscore * in front of assembly symbols. We thus introducee a separate * namespace wrapper for ASM symbols. */ #if !defined(__APPLE__) #define MLKEM_ASM_NAMESPACE(sym) MLKEM_NAMESPACE(sym) +#define MLKEM_ASM_NAMESPACE_K(sym) MLKEM_NAMESPACE_K(sym) #define FIPS202_ASM_NAMESPACE(sym) FIPS202_NAMESPACE(sym) #else #define PREFIX_UNDERSCORE_(sym) _##sym #define PREFIX_UNDERSCORE(sym) PREFIX_UNDERSCORE_(sym) #define MLKEM_ASM_NAMESPACE(sym) PREFIX_UNDERSCORE(MLKEM_NAMESPACE(sym)) +#define MLKEM_ASM_NAMESPACE_K(sym) PREFIX_UNDERSCORE(MLKEM_NAMESPACE_K(sym)) #define FIPS202_ASM_NAMESPACE(sym) PREFIX_UNDERSCORE(FIPS202_NAMESPACE(sym)) #endif diff --git a/mlkem/config.h b/mlkem/config.h index 92b9507d1..f09416428 100644 --- a/mlkem/config.h +++ b/mlkem/config.h @@ -40,7 +40,7 @@ /* #define MLKEM_NATIVE_CONFIG_FILE "config.h" */ /****************************************************************************** - * Name: MLKEM_NAMESPACE + * Name: MLKEM_NAMESPACE_PREFIX * * Description: The prefix to use to namespace global symbols * from mlkem/. @@ -53,7 +53,23 @@ #endif /****************************************************************************** - * Name: FIPS202_NAMESPACE + * Name: MLKEM_NAMESPACE_PREFIX_ADD_LEVEL + * + * Description: If set, the level (512, 768, 1024) is added to the namespace + * prefix MLKEM_NAMESPACE_PREFIX for all functions which are + * level-dependent. Level-independent functions will have there + * symbol prefixed by MLKEM_NAMESPACE_PREFIX only. + * + * This is intended to be used for multi-level builds where + * level-independent code should be shared across levels. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLKEM_NAMESPACE_PREFIX_ADD_LEVEL */ + +/****************************************************************************** + * Name: FIPS202_NAMESPACE_PREFIX * * Description: The prefix to use to namespace global symbols * from mlkem/fips202/. @@ -65,6 +81,57 @@ #define FIPS202_NAMESPACE_PREFIX FIPS202_DEFAULT_NAMESPACE_PREFIX #endif +/****************************************************************************** + * Name: MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED + * + * Description: This is for multi-level builds of mlkem-native only. If you + * need only a single security level build of mlkem-native, + * keep this unset. + * + * If this is set, all MLKEM_K-independent code will be included + * in the build, including code needed only for other security + * levels. + * + * Example: poly_cbd3 is only needed for MLKEM_K == 2. Yet, if + * this option is set for a build with MLKEM_K==3/4, it would + * be included. + * + * To build mlkem-native with support for all security levels, + * build it three times -- once per level -- and set the option + * MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED for exactly one of + * them, and MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED for the + * others. + * + * See examples/multilevel_build for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED */ + +/****************************************************************************** + * Name: MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED + * + * Description: This is for multi-level builds of mlkem-native only. If you + * need only a single security level build of mlkem-native, + * keep this unset. + * + * If this is set, no MLKEM_K-independent code will be included + * in the build. + * + * To build mlkem-native with support for all security levels, + * build it three times -- once per level -- and set the option + * MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED for exactly one of + * them, and MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED for the + * others. + * + * See examples/multilevel_build for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ + /****************************************************************************** * Name: MLKEM_USE_NATIVE * diff --git a/mlkem/debug/debug.c b/mlkem/debug/debug.c index 310b033ab..e64515742 100644 --- a/mlkem/debug/debug.c +++ b/mlkem/debug/debug.c @@ -4,7 +4,7 @@ */ #include "../common.h" -#if defined(MLKEM_DEBUG) +#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) && defined(MLKEM_DEBUG) #include #include @@ -48,9 +48,9 @@ void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr, exit(1); } -#else /* MLKEM_DEBUG */ +#else /* !MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED && MLKEM_DEBUG */ -#define empty_cu_debug MLKEM_NAMESPACE(empty_cu_debug) +#define empty_cu_debug MLKEM_NAMESPACE_K(empty_cu_debug) int empty_cu_debug; -#endif /* MLKEM_DEBUG */ +#endif /* !MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED && MLKEM_DEBUG */ diff --git a/mlkem/debug/debug.h b/mlkem/debug/debug.h index 030c98fb1..ff44b4e3d 100644 --- a/mlkem/debug/debug.h +++ b/mlkem/debug/debug.h @@ -4,7 +4,6 @@ */ #ifndef MLKEM_DEBUG_H #define MLKEM_DEBUG_H - #include "../common.h" #if defined(MLKEM_DEBUG) @@ -128,5 +127,4 @@ void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr, #endif /* MLKEM_DEBUG */ - #endif /* MLKEM_DEBUG_H */ diff --git a/mlkem/fips202/fips202.c b/mlkem/fips202/fips202.c index 6dca89fb5..03d3c8cc6 100644 --- a/mlkem/fips202/fips202.c +++ b/mlkem/fips202/fips202.c @@ -11,10 +11,12 @@ * from https://twitter.com/tweetfips202 * by Gilles Van Assche, Daniel J. Bernstein, and Peter Schwabe */ +#include "../common.h" +#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) + #include #include #include - #include "fips202.h" #include "keccakf1600.h" @@ -212,3 +214,10 @@ void sha3_512(uint8_t *output, const uint8_t *input, size_t inlen) /* Squeeze output */ keccak_squeeze_once(output, 64, ctx, SHA3_512_RATE); } + +#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ + +#define empty_cu_fips202 MLKEM_NAMESPACE_K(empty_cu_fips202) +int empty_cu_fips202; + +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/fips202/fips202.h b/mlkem/fips202/fips202.h index 0abb64dc7..953bc9664 100644 --- a/mlkem/fips202/fips202.h +++ b/mlkem/fips202/fips202.h @@ -4,7 +4,6 @@ */ #ifndef FIPS202_H #define FIPS202_H - #include #include #include "../cbmc.h" @@ -142,4 +141,4 @@ __contract__( assigns(memory_slice(output, SHA3_512_HASHBYTES)) ); -#endif +#endif /* FIPS202_H */ diff --git a/mlkem/fips202/fips202x4.c b/mlkem/fips202/fips202x4.c index 4ba78edad..bce629e62 100644 --- a/mlkem/fips202/fips202x4.c +++ b/mlkem/fips202/fips202x4.c @@ -2,9 +2,12 @@ * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 */ -#include "fips202x4.h" +#include "../common.h" +#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) + #include #include "fips202.h" +#include "fips202x4.h" #include "keccakf1600.h" #define shake256x4_ctx FIPS202_NAMESPACE(shake256x4_ctx) @@ -177,3 +180,10 @@ void shake256x4(uint8_t *out0, uint8_t *out1, uint8_t *out2, uint8_t *out3, memcpy(out3, tmp3, outlen); } } + +#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ + +#define empty_cu_fips202x4 MLKEM_NAMESPACE_K(empty_cu_fips202x4) +int empty_cu_fips202x4; + +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/fips202/fips202x4.h b/mlkem/fips202/fips202x4.h index 2a7f8dfb2..8a6cf7cfb 100644 --- a/mlkem/fips202/fips202x4.h +++ b/mlkem/fips202/fips202x4.h @@ -75,4 +75,4 @@ __contract__( assigns(memory_slice(out3, outlen)) ); -#endif +#endif /* FIPS_202X4_H */ diff --git a/mlkem/fips202/keccakf1600.c b/mlkem/fips202/keccakf1600.c index 54e00835b..bd749b9af 100644 --- a/mlkem/fips202/keccakf1600.c +++ b/mlkem/fips202/keccakf1600.c @@ -13,8 +13,10 @@ #include #include -#include "fips202_backend.h" #include "keccakf1600.h" +#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) + +#include "fips202_backend.h" #define NROUNDS 24 #define ROL(a, offset) ((a << offset) ^ (a >> (64 - offset))) @@ -399,3 +401,10 @@ void KeccakF1600_StatePermute(uint64_t *state) keccak_f1600_x1_native(state); } #endif /* !MLKEM_USE_FIPS202_X1_NATIVE */ + +#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED */ + +#define empty_cu_keccakf1600 MLKEM_NAMESPACE_K(empty_cu_keccakf1600) +int empty_cu_keccakf1600; + +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED */ diff --git a/mlkem/fips202/keccakf1600.h b/mlkem/fips202/keccakf1600.h index bb694bb78..2fae28cb9 100644 --- a/mlkem/fips202/keccakf1600.h +++ b/mlkem/fips202/keccakf1600.h @@ -4,7 +4,6 @@ */ #ifndef KECCAKF1600_H #define KECCAKF1600_H - #include #include "../cbmc.h" #include "../common.h" @@ -103,4 +102,4 @@ __contract__( #define KeccakF1600_StatePermute FIPS202_NAMESPACE(keccak_f1600_x1_asm) #endif -#endif +#endif /* KECCAKF1600_H */ diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index cad1937a1..e4aad0ba0 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -25,15 +25,13 @@ * This is to facilitate building multiple instances * of mlkem-native (e.g. with varying security levels) * within a single compilation unit. */ -#define pack_pk MLKEM_NAMESPACE(pack_pk) -#define unpack_pk MLKEM_NAMESPACE(unpack_pk) -#define pack_sk MLKEM_NAMESPACE(pack_sk) -#define unpack_sk MLKEM_NAMESPACE(unpack_sk) -#define pack_ciphertext MLKEM_NAMESPACE(pack_ciphertext) -#define unpack_ciphertext MLKEM_NAMESPACE(unpack_ciphertext) -#define gen_matrix_entry_x4 MLKEM_NAMESPACE(gen_matrix_entry_x4) -#define gen_matrix_entry MLKEM_NAMESPACE(gen_matrix_entry) -#define matvec_mul MLKEM_NAMESPACE(matvec_mul) +#define pack_pk MLKEM_NAMESPACE_K(pack_pk) +#define unpack_pk MLKEM_NAMESPACE_K(unpack_pk) +#define pack_sk MLKEM_NAMESPACE_K(pack_sk) +#define unpack_sk MLKEM_NAMESPACE_K(unpack_sk) +#define pack_ciphertext MLKEM_NAMESPACE_K(pack_ciphertext) +#define unpack_ciphertext MLKEM_NAMESPACE_K(unpack_ciphertext) +#define matvec_mul MLKEM_NAMESPACE_K(matvec_mul) /* End of static namespacing */ /************************************************* @@ -145,127 +143,11 @@ static void unpack_ciphertext(polyvec *b, poly *v, poly_decompress_dv(v, c + MLKEM_POLYVECCOMPRESSEDBYTES_DU); } -#ifndef MLKEM_GEN_MATRIX_NBLOCKS -#define MLKEM_GEN_MATRIX_NBLOCKS \ - ((12 * MLKEM_N / 8 * (1 << 12) / MLKEM_Q + XOF_RATE) / XOF_RATE) -#endif - -/* - * Generate four A matrix entries from a seed, using rejection - * sampling on the output of a XOF. - */ -static void gen_matrix_entry_x4(poly *vec, uint8_t *seed[4]) -__contract__( - requires(memory_no_alias(vec, sizeof(poly) * 4)) - requires(memory_no_alias(seed, sizeof(uint8_t*) * 4)) - requires(memory_no_alias(seed[0], MLKEM_SYMBYTES + 2)) - requires(memory_no_alias(seed[1], MLKEM_SYMBYTES + 2)) - requires(memory_no_alias(seed[2], MLKEM_SYMBYTES + 2)) - requires(memory_no_alias(seed[3], MLKEM_SYMBYTES + 2)) - assigns(memory_slice(vec, sizeof(poly) * 4)) - ensures(array_bound(vec[0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)) - ensures(array_bound(vec[1].coeffs, 0, MLKEM_N, 0, MLKEM_Q)) - ensures(array_bound(vec[2].coeffs, 0, MLKEM_N, 0, MLKEM_Q)) - ensures(array_bound(vec[3].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) -{ - /* Temporary buffers for XOF output before rejection sampling */ - uint8_t buf0[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; - uint8_t buf1[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; - uint8_t buf2[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; - uint8_t buf3[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; - - /* Tracks the number of coefficients we have already sampled */ - unsigned int ctr[KECCAK_WAY]; - xof_x4_ctx statex; - unsigned int buflen; - - /* seed is MLKEM_SYMBYTES + 2 bytes long, but padded to MLKEM_SYMBYTES + 16 */ - xof_x4_absorb(&statex, seed[0], seed[1], seed[2], seed[3], - MLKEM_SYMBYTES + 2); - - /* - * Initially, squeeze heuristic number of MLKEM_GEN_MATRIX_NBLOCKS. - * This should generate the matrix entries with high probability. - */ - xof_x4_squeezeblocks(buf0, buf1, buf2, buf3, MLKEM_GEN_MATRIX_NBLOCKS, - &statex); - buflen = MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE; - ctr[0] = rej_uniform(vec[0].coeffs, MLKEM_N, 0, buf0, buflen); - ctr[1] = rej_uniform(vec[1].coeffs, MLKEM_N, 0, buf1, buflen); - ctr[2] = rej_uniform(vec[2].coeffs, MLKEM_N, 0, buf2, buflen); - ctr[3] = rej_uniform(vec[3].coeffs, MLKEM_N, 0, buf3, buflen); - - /* - * So long as not all matrix entries have been generated, squeeze - * one more block a time until we're done. - */ - buflen = XOF_RATE; - while (ctr[0] < MLKEM_N || ctr[1] < MLKEM_N || ctr[2] < MLKEM_N || - ctr[3] < MLKEM_N) - __loop__( - assigns(ctr, statex, memory_slice(vec, sizeof(poly) * 4), object_whole(buf0), - object_whole(buf1), object_whole(buf2), object_whole(buf3)) - invariant(ctr[0] <= MLKEM_N && ctr[1] <= MLKEM_N) - invariant(ctr[2] <= MLKEM_N && ctr[3] <= MLKEM_N) - invariant(ctr[0] > 0 ==> array_bound(vec[0].coeffs, 0, ctr[0], 0, MLKEM_Q)) - invariant(ctr[1] > 0 ==> array_bound(vec[1].coeffs, 0, ctr[1], 0, MLKEM_Q)) - invariant(ctr[2] > 0 ==> array_bound(vec[2].coeffs, 0, ctr[2], 0, MLKEM_Q)) - invariant(ctr[3] > 0 ==> array_bound(vec[3].coeffs, 0, ctr[3], 0, MLKEM_Q))) - { - xof_x4_squeezeblocks(buf0, buf1, buf2, buf3, 1, &statex); - ctr[0] = rej_uniform(vec[0].coeffs, MLKEM_N, ctr[0], buf0, buflen); - ctr[1] = rej_uniform(vec[1].coeffs, MLKEM_N, ctr[1], buf1, buflen); - ctr[2] = rej_uniform(vec[2].coeffs, MLKEM_N, ctr[2], buf2, buflen); - ctr[3] = rej_uniform(vec[3].coeffs, MLKEM_N, ctr[3], buf3, buflen); - } - - xof_x4_release(&statex); -} - -/* - * Generate a single A matrix entry from a seed, using rejection - * sampling on the output of a XOF. - */ -static void gen_matrix_entry(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 2]) -__contract__( - requires(memory_no_alias(entry, sizeof(poly))) - requires(memory_no_alias(seed, MLKEM_SYMBYTES + 2)) - assigns(memory_slice(entry, sizeof(poly))) - ensures(array_bound(entry->coeffs, 0, MLKEM_N, 0, MLKEM_Q))) -{ - xof_ctx state; - uint8_t buf[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; - unsigned int ctr, buflen; - - xof_absorb(&state, seed, MLKEM_SYMBYTES + 2); - - /* Initially, squeeze + sample heuristic number of MLKEM_GEN_MATRIX_NBLOCKS. - */ - /* This should generate the matrix entry with high probability. */ - xof_squeezeblocks(buf, MLKEM_GEN_MATRIX_NBLOCKS, &state); - buflen = MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE; - ctr = rej_uniform(entry->coeffs, MLKEM_N, 0, buf, buflen); - - /* Squeeze + sample one more block a time until we're done */ - buflen = XOF_RATE; - while (ctr < MLKEM_N) - __loop__( - assigns(ctr, state, memory_slice(entry, sizeof(poly)), object_whole(buf)) - invariant(ctr <= MLKEM_N) - invariant(array_bound(entry->coeffs, 0, ctr, 0, MLKEM_Q))) - { - xof_squeezeblocks(buf, 1, &state); - ctr = rej_uniform(entry->coeffs, MLKEM_N, ctr, buf, buflen); - } - - xof_release(&state); -} - #if !defined(MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER) /* This namespacing is not done at the top to avoid a naming conflict * with native backends, which are currently not yet namespaced. */ #define poly_permute_bitrev_to_custom \ - MLKEM_NAMESPACE(poly_permute_bitrev_to_custom) + MLKEM_NAMESPACE_K(poly_permute_bitrev_to_custom) static INLINE void poly_permute_bitrev_to_custom(poly *data) __contract__( @@ -328,7 +210,7 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed) * This call writes across polyvec boundaries for K=2 and K=3. * This is intentional and safe. */ - gen_matrix_entry_x4(&a[0].vec[0] + i, seedxy); + poly_rej_uniform_x4(&a[0].vec[0] + i, seedxy); } /* For left over polynomial, we use single keccak. */ @@ -349,7 +231,7 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed) seed0[MLKEM_SYMBYTES + 1] = x; } - gen_matrix_entry(&a[0].vec[0] + i, seed0); + poly_rej_uniform(&a[0].vec[0] + i, seed0); i++; } diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h index 011f1aa4f..2c4fda3c4 100644 --- a/mlkem/indcpa.h +++ b/mlkem/indcpa.h @@ -10,7 +10,7 @@ #include "common.h" #include "polyvec.h" -#define gen_matrix MLKEM_NAMESPACE(gen_matrix) +#define gen_matrix MLKEM_NAMESPACE_K(gen_matrix) /************************************************* * Name: gen_matrix * @@ -34,7 +34,7 @@ __contract__( array_bound(a[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))); ); -#define indcpa_keypair_derand MLKEM_NAMESPACE(indcpa_keypair_derand) +#define indcpa_keypair_derand MLKEM_NAMESPACE_K(indcpa_keypair_derand) /************************************************* * Name: indcpa_keypair_derand * @@ -60,7 +60,7 @@ __contract__( assigns(object_whole(sk)) ); -#define indcpa_enc MLKEM_NAMESPACE(indcpa_enc) +#define indcpa_enc MLKEM_NAMESPACE_K(indcpa_enc) /************************************************* * Name: indcpa_enc * @@ -89,7 +89,7 @@ __contract__( assigns(object_whole(c)) ); -#define indcpa_dec MLKEM_NAMESPACE(indcpa_dec) +#define indcpa_dec MLKEM_NAMESPACE_K(indcpa_dec) /************************************************* * Name: indcpa_dec * diff --git a/mlkem/kem.c b/mlkem/kem.c index 5779d3273..88c3843be 100644 --- a/mlkem/kem.c +++ b/mlkem/kem.c @@ -16,8 +16,8 @@ * This is to facilitate building multiple instances * of mlkem-native (e.g. with varying security levels) * within a single compilation unit. */ -#define check_pk MLKEM_NAMESPACE(check_pk) -#define check_sk MLKEM_NAMESPACE(check_sk) +#define check_pk MLKEM_NAMESPACE_K(check_pk) +#define check_sk MLKEM_NAMESPACE_K(check_sk) /* End of static namespacing */ #if defined(CBMC) diff --git a/mlkem/kem.h b/mlkem/kem.h index f866e7795..93caa796b 100644 --- a/mlkem/kem.h +++ b/mlkem/kem.h @@ -27,11 +27,11 @@ #endif #else -#define crypto_kem_keypair_derand MLKEM_NAMESPACE(keypair_derand) -#define crypto_kem_keypair MLKEM_NAMESPACE(keypair) -#define crypto_kem_enc_derand MLKEM_NAMESPACE(enc_derand) -#define crypto_kem_enc MLKEM_NAMESPACE(enc) -#define crypto_kem_dec MLKEM_NAMESPACE(dec) +#define crypto_kem_keypair_derand MLKEM_NAMESPACE_K(keypair_derand) +#define crypto_kem_keypair MLKEM_NAMESPACE_K(keypair) +#define crypto_kem_enc_derand MLKEM_NAMESPACE_K(enc_derand) +#define crypto_kem_enc MLKEM_NAMESPACE_K(enc) +#define crypto_kem_dec MLKEM_NAMESPACE_K(dec) #endif /************************************************* diff --git a/mlkem/mlkem_native.h b/mlkem/mlkem_native.h index 4aed4efbb..12d1d12e6 100644 --- a/mlkem/mlkem_native.h +++ b/mlkem/mlkem_native.h @@ -59,9 +59,17 @@ #error MLKEM_NAMESPACE_PREFIX not set by config file #endif -#define BUILD_INFO_CONCAT_(x, y) x##_##y -#define BUILD_INFO_CONCAT(x, y) BUILD_INFO_CONCAT_(x, y) -#define BUILD_INFO_NAMESPACE(sym) BUILD_INFO_CONCAT(MLKEM_NAMESPACE_PREFIX, sym) +#if defined(MLKEM_NATIVE_NAMESPACE_PREFIX_ADD_LEVEL) +#define BUILD_INFO_CONCAT3_(x, y, z) x##y##_##z +#define BUILD_INFO_CONCAT3(x, y, z) BUILD_INFO_CONCAT_(x, y, z) +#define BUILD_INFO_NAMESPACE(sym) \ + BUILD_INFO_CONCAT3(MLKEM_NAMESPACE_PREFIX, BUILD_INFO_LVL, sym) +#else +#define BUILD_INFO_CONCAT2_(x, y) x##_##y +#define BUILD_INFO_CONCAT2(x, y) BUILD_INFO_CONCAT2_(x, y) +#define BUILD_INFO_NAMESPACE(sym) \ + BUILD_INFO_CONCAT2(MLKEM_NAMESPACE_PREFIX, sym) +#endif #endif /* BUILD_INFO_LVL */ diff --git a/mlkem/native/aarch64/src/arith_native_aarch64.h b/mlkem/native/aarch64/src/arith_native_aarch64.h index cd46ea5a1..a784a3027 100644 --- a/mlkem/native/aarch64/src/arith_native_aarch64.h +++ b/mlkem/native/aarch64/src/arith_native_aarch64.h @@ -75,14 +75,14 @@ void poly_tobytes_asm_clean(uint8_t *r, const int16_t *a); void poly_tobytes_asm_opt(uint8_t *r, const int16_t *a); #define polyvec_basemul_acc_montgomery_cached_asm_clean \ - MLKEM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_clean) + MLKEM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_clean) void polyvec_basemul_acc_montgomery_cached_asm_clean(int16_t *r, const int16_t *a, const int16_t *b, const int16_t *b_cache); #define polyvec_basemul_acc_montgomery_cached_asm_opt \ - MLKEM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt) + MLKEM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_opt) void polyvec_basemul_acc_montgomery_cached_asm_opt(int16_t *r, const int16_t *a, const int16_t *b, const int16_t *b_cache); diff --git a/mlkem/native/aarch64/src/polyvec_clean.S b/mlkem/native/aarch64/src/polyvec_clean.S index ef590db9c..0b6df6345 100644 --- a/mlkem/native/aarch64/src/polyvec_clean.S +++ b/mlkem/native/aarch64/src/polyvec_clean.S @@ -138,9 +138,9 @@ t0 .req v28 #if MLKEM_K == 2 -.global MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_clean) +.global MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_clean) -MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_clean): +MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_clean): push_stack mov wtmp, #3329 @@ -176,9 +176,9 @@ k2_loop_start: #endif /* MLKEM_K == 2 */ #if MLKEM_K == 3 -.global MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_clean) +.global MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_clean) -MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_clean): +MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_clean): push_stack mov wtmp, #3329 dup modulus.8h, wtmp @@ -218,9 +218,9 @@ k3_loop_start: #endif /* MLKEM_K == 3 */ #if MLKEM_K == 4 -.global MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_clean) +.global MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_clean) -MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_clean): +MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_clean): push_stack mov wtmp, #3329 dup modulus.8h, wtmp diff --git a/mlkem/native/aarch64/src/polyvec_opt.S b/mlkem/native/aarch64/src/polyvec_opt.S index efbc609eb..7a27fda3e 100644 --- a/mlkem/native/aarch64/src/polyvec_opt.S +++ b/mlkem/native/aarch64/src/polyvec_opt.S @@ -138,9 +138,9 @@ t0 .req v28 #if MLKEM_K == 2 -.global MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt) +.global MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_opt) -MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt): +MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_opt): push_stack mov wtmp, #3329 @@ -508,9 +508,9 @@ MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt): #endif /* MLKEM_K == 2 */ #if MLKEM_K == 3 -.global MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt) +.global MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_opt) -MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt): +MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_opt): push_stack mov wtmp, #3329 dup modulus.8h, wtmp @@ -982,9 +982,9 @@ MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt): #endif /* MLKEM_K == 3 */ #if MLKEM_K == 4 -.global MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt) +.global MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_opt) -MLKEM_ASM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_opt): +MLKEM_ASM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_asm_opt): push_stack mov wtmp, #3329 dup modulus.8h, wtmp 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 07f958a75..acf3ae56b 100644 --- a/mlkem/native/x86_64/src/arith_native_x86_64.h +++ b/mlkem/native/x86_64/src/arith_native_x86_64.h @@ -42,7 +42,7 @@ void basemul_avx2(__m256i *r, const __m256i *a, const __m256i *b, const __m256i *qdata); #define polyvec_basemul_acc_montgomery_cached_avx2 \ - MLKEM_NAMESPACE(polyvec_basemul_acc_montgomery_cached_avx2) + MLKEM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached_avx2) void polyvec_basemul_acc_montgomery_cached_avx2( poly *r, const polyvec *a, const polyvec *b, const polyvec_mulcache *b_cache); diff --git a/mlkem/ntt.c b/mlkem/ntt.c index b24555b75..09985aad4 100644 --- a/mlkem/ntt.c +++ b/mlkem/ntt.c @@ -2,8 +2,10 @@ * Copyright (c) 2024 The mlkem-native project authors * SPDX-License-Identifier: Apache-2.0 */ -#include +#include "common.h" +#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) +#include #include "arith_backend.h" #include "debug/debug.h" #include "ntt.h" @@ -255,3 +257,10 @@ void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2], 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 index 877886ad8..4e80d3ab3 100644 --- a/mlkem/ntt.h +++ b/mlkem/ntt.h @@ -4,10 +4,10 @@ */ #ifndef NTT_H #define NTT_H +#include "common.h" #include #include "cbmc.h" -#include "common.h" #include "poly.h" #include "reduce.h" @@ -99,5 +99,4 @@ __contract__( ensures(array_abs_bound(r, 0, 2, 2 * MLKEM_Q)) ); - -#endif +#endif /* NTT_H */ diff --git a/mlkem/params.h b/mlkem/params.h index fa751f977..57ea4c8ba 100644 --- a/mlkem/params.h +++ b/mlkem/params.h @@ -25,23 +25,34 @@ #define MLKEM_POLYBYTES 384 #define MLKEM_POLYVECBYTES (MLKEM_K * MLKEM_POLYBYTES) +#define MLKEM_POLYCOMPRESSEDBYTES_D4 128 +#define MLKEM_POLYCOMPRESSEDBYTES_D5 160 +#define MLKEM_POLYCOMPRESSEDBYTES_D10 320 +#define MLKEM_POLYCOMPRESSEDBYTES_D11 352 + #if MLKEM_K == 2 #define MLKEM_LVL 512 #define MLKEM_ETA1 3 -#define MLKEM_POLYCOMPRESSEDBYTES_DV 128 -#define MLKEM_POLYCOMPRESSEDBYTES_DU 320 +#define MLKEM_DU 10 +#define MLKEM_DV 4 +#define MLKEM_POLYCOMPRESSEDBYTES_DV MLKEM_POLYCOMPRESSEDBYTES_D4 +#define MLKEM_POLYCOMPRESSEDBYTES_DU MLKEM_POLYCOMPRESSEDBYTES_D10 #define MLKEM_POLYVECCOMPRESSEDBYTES_DU (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #elif MLKEM_K == 3 #define MLKEM_LVL 768 #define MLKEM_ETA1 2 -#define MLKEM_POLYCOMPRESSEDBYTES_DV 128 -#define MLKEM_POLYCOMPRESSEDBYTES_DU 320 +#define MLKEM_DU 10 +#define MLKEM_DV 4 +#define MLKEM_POLYCOMPRESSEDBYTES_DV MLKEM_POLYCOMPRESSEDBYTES_D4 +#define MLKEM_POLYCOMPRESSEDBYTES_DU MLKEM_POLYCOMPRESSEDBYTES_D10 #define MLKEM_POLYVECCOMPRESSEDBYTES_DU (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #elif MLKEM_K == 4 #define MLKEM_LVL 1024 #define MLKEM_ETA1 2 -#define MLKEM_POLYCOMPRESSEDBYTES_DV 160 -#define MLKEM_POLYCOMPRESSEDBYTES_DU 352 +#define MLKEM_DU 11 +#define MLKEM_DV 5 +#define MLKEM_POLYCOMPRESSEDBYTES_DV MLKEM_POLYCOMPRESSEDBYTES_D5 +#define MLKEM_POLYCOMPRESSEDBYTES_DU MLKEM_POLYCOMPRESSEDBYTES_D11 #define MLKEM_POLYVECCOMPRESSEDBYTES_DU (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #endif diff --git a/mlkem/poly.c b/mlkem/poly.c index f7a09314e..987f5ec29 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -2,9 +2,11 @@ * 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 "cbd.h" #include "cbmc.h" @@ -16,44 +18,38 @@ #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_du(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DU], const poly *a) +void poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const poly *a) { - unsigned j; + unsigned i; debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); -#if (MLKEM_POLYCOMPRESSEDBYTES_DU == 352) - for (j = 0; j < MLKEM_N / 8; j++) - __loop__(invariant(j <= MLKEM_N / 8)) + for (i = 0; i < MLKEM_N / 8; i++) + __loop__(invariant(i <= MLKEM_N / 8)) { - unsigned k; - uint16_t t[8]; - for (k = 0; k < 8; k++) + unsigned j; + uint8_t t[8] = {0}; + for (j = 0; j < 8; j++) __loop__( - invariant(k <= 8) - invariant(forall(r, 0, k, t[r] < (1u << 11)))) + invariant(i <= MLKEM_N / 8 && j <= 8) + invariant(array_bound(t, 0, j, 0, 16))) { - t[k] = scalar_compress_d11(a->coeffs[8 * j + k]); + t[j] = scalar_compress_d4(a->coeffs[8 * i + j]); } - /* - * 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); + 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); } +} -#elif (MLKEM_POLYCOMPRESSEDBYTES_DU == 320) +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)) { @@ -77,45 +73,29 @@ void poly_compress_du(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DU], const poly *a) r[5 * j + 3] = (t[2] >> 4) | ((t[3] << 6) & 0xFF); r[5 * j + 4] = (t[3] >> 2); } -#else -#error "MLKEM_POLYCOMPRESSEDBYTES_DU needs to be in {320,352}" -#endif } - MLKEM_NATIVE_INTERNAL_API -void poly_decompress_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU]) +void poly_decompress_d4(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D4]) { - unsigned j; -#if (MLKEM_POLYCOMPRESSEDBYTES_DU == 352) - for (j = 0; j < MLKEM_N / 8; j++) + unsigned i; + for (i = 0; i < MLKEM_N / 2; i++) __loop__( - invariant(j <= MLKEM_N / 8) - invariant(array_bound(r->coeffs, 0, 8 * j, 0, MLKEM_Q))) + invariant(i <= MLKEM_N / 2) + invariant(array_bound(r->coeffs, 0, 2 * i, 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]); - } + r->coeffs[2 * i + 0] = scalar_decompress_d4((a[i] >> 0) & 0xF); + r->coeffs[2 * i + 1] = scalar_decompress_d4((a[i] >> 4) & 0xF); } -#elif (MLKEM_POLYCOMPRESSEDBYTES_DU == 320) + + 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) @@ -138,39 +118,19 @@ void poly_decompress_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU]) r->coeffs[4 * j + k] = scalar_decompress_d10(t[k]); } } -#else -#error "MLKEM_POLYCOMPRESSEDBYTES_DU needs to be in {320,352}" -#endif 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_dv(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DV], const poly *a) +void poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const poly *a) { unsigned i; debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q); -#if (MLKEM_POLYCOMPRESSEDBYTES_DV == 128) - 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); - } -#elif (MLKEM_POLYCOMPRESSEDBYTES_DV == 160) for (i = 0; i < MLKEM_N / 8; i++) __loop__(invariant(i <= MLKEM_N / 8)) { @@ -195,25 +155,49 @@ void poly_compress_dv(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DV], const poly *a) 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)); } -#else -#error "MLKEM_POLYCOMPRESSEDBYTES_DV needs to be in {128, 160}" -#endif } MLKEM_NATIVE_INTERNAL_API -void poly_decompress_dv(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV]) +void poly_compress_d11(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const poly *a) { - unsigned i; -#if (MLKEM_POLYCOMPRESSEDBYTES_DV == 128) - 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))) + 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)) { - r->coeffs[2 * i + 0] = scalar_decompress_d4((a[i] >> 0) & 0xF); - r->coeffs[2 * i + 1] = scalar_decompress_d4((a[i] >> 4) & 0xF); + 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); } -#elif (MLKEM_POLYCOMPRESSEDBYTES_DV == 160) +} + +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) @@ -250,13 +234,47 @@ void poly_decompress_dv(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV]) r->coeffs[8 * i + j] = scalar_decompress_d5(t[j]); } } -#else -#error "MLKEM_POLYCOMPRESSEDBYTES_DV needs to be in {128, 160}" -#endif 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) @@ -374,93 +392,6 @@ void poly_tomsg(uint8_t msg[MLKEM_INDCPA_MSGBYTES], const poly *a) } } -MLKEM_NATIVE_INTERNAL_API -void poly_getnoise_eta1_4x(poly *r0, poly *r1, poly *r2, poly *r3, - const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0, - uint8_t nonce1, uint8_t nonce2, uint8_t nonce3) -{ - ALIGN uint8_t buf0[MLKEM_ETA1 * MLKEM_N / 4]; - ALIGN uint8_t buf1[MLKEM_ETA1 * MLKEM_N / 4]; - ALIGN uint8_t buf2[MLKEM_ETA1 * MLKEM_N / 4]; - ALIGN uint8_t buf3[MLKEM_ETA1 * MLKEM_N / 4]; - ALIGN uint8_t extkey0[MLKEM_SYMBYTES + 1]; - ALIGN uint8_t extkey1[MLKEM_SYMBYTES + 1]; - ALIGN uint8_t extkey2[MLKEM_SYMBYTES + 1]; - ALIGN uint8_t extkey3[MLKEM_SYMBYTES + 1]; - memcpy(extkey0, seed, MLKEM_SYMBYTES); - memcpy(extkey1, seed, MLKEM_SYMBYTES); - memcpy(extkey2, seed, MLKEM_SYMBYTES); - memcpy(extkey3, seed, MLKEM_SYMBYTES); - extkey0[MLKEM_SYMBYTES] = nonce0; - extkey1[MLKEM_SYMBYTES] = nonce1; - extkey2[MLKEM_SYMBYTES] = nonce2; - extkey3[MLKEM_SYMBYTES] = nonce3; - prf_eta1_x4(buf0, buf1, buf2, buf3, extkey0, extkey1, extkey2, extkey3); - poly_cbd_eta1(r0, buf0); - poly_cbd_eta1(r1, buf1); - poly_cbd_eta1(r2, buf2); - poly_cbd_eta1(r3, buf3); - - debug_assert_abs_bound(r0, MLKEM_N, MLKEM_ETA1 + 1); - debug_assert_abs_bound(r1, MLKEM_N, MLKEM_ETA1 + 1); - debug_assert_abs_bound(r2, MLKEM_N, MLKEM_ETA1 + 1); - debug_assert_abs_bound(r3, MLKEM_N, MLKEM_ETA1 + 1); -} - -#if MLKEM_K == 2 || MLKEM_K == 4 -MLKEM_NATIVE_INTERNAL_API -void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES], - uint8_t nonce) -{ - ALIGN uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4]; - ALIGN uint8_t extkey[MLKEM_SYMBYTES + 1]; - - memcpy(extkey, seed, MLKEM_SYMBYTES); - extkey[MLKEM_SYMBYTES] = nonce; - prf_eta2(buf, extkey); - - poly_cbd_eta2(r, buf); - - debug_assert_abs_bound(r, MLKEM_N, MLKEM_ETA1 + 1); -} -#endif /* MLKEM_K == 2 || MLKEM_K == 4 */ - -#if MLKEM_K == 2 -MLKEM_NATIVE_INTERNAL_API -void poly_getnoise_eta1122_4x(poly *r0, poly *r1, poly *r2, poly *r3, - const uint8_t seed[MLKEM_SYMBYTES], - uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, - uint8_t nonce3) -{ - ALIGN uint8_t buf1[KECCAK_WAY / 2][MLKEM_ETA1 * MLKEM_N / 4]; - ALIGN uint8_t buf2[KECCAK_WAY / 2][MLKEM_ETA2 * MLKEM_N / 4]; - ALIGN uint8_t extkey[KECCAK_WAY][MLKEM_SYMBYTES + 1]; - memcpy(extkey[0], seed, MLKEM_SYMBYTES); - memcpy(extkey[1], seed, MLKEM_SYMBYTES); - memcpy(extkey[2], seed, MLKEM_SYMBYTES); - memcpy(extkey[3], seed, MLKEM_SYMBYTES); - extkey[0][MLKEM_SYMBYTES] = nonce0; - extkey[1][MLKEM_SYMBYTES] = nonce1; - extkey[2][MLKEM_SYMBYTES] = nonce2; - extkey[3][MLKEM_SYMBYTES] = nonce3; - - prf_eta1(buf1[0], extkey[0]); - prf_eta1(buf1[1], extkey[1]); - prf_eta2(buf2[0], extkey[2]); - prf_eta2(buf2[1], extkey[3]); - - poly_cbd_eta1(r0, buf1[0]); - poly_cbd_eta1(r1, buf1[1]); - poly_cbd_eta2(r2, buf2[0]); - poly_cbd_eta2(r3, buf2[1]); - - debug_assert_abs_bound(r0, MLKEM_N, MLKEM_ETA1 + 1); - debug_assert_abs_bound(r1, MLKEM_N, MLKEM_ETA1 + 1); - debug_assert_abs_bound(r2, MLKEM_N, MLKEM_ETA2 + 1); - debug_assert_abs_bound(r3, MLKEM_N, MLKEM_ETA2 + 1); -} -#endif /* MLKEM_K == 2 */ - MLKEM_NATIVE_INTERNAL_API void poly_basemul_montgomery_cached(poly *r, const poly *a, const poly *b, const poly_mulcache *b_cache) @@ -595,3 +526,10 @@ void poly_mulcache_compute(poly_mulcache *x, const poly *a) * of poly_basemul_montgomery_cached() does still include the check. */ } #endif /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */ + +#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ + +#define empty_cu_poly MLKEM_NAMESPACE_K(empty_cu_poly) +int empty_cu_poly; + +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/poly.h b/mlkem/poly.h index 0fc0bed88..6a14c785d 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -321,98 +321,150 @@ __contract__( return (uint16_t)c; } -#define poly_compress_du MLKEM_NAMESPACE(poly_compress_du) +#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_du + * Name: poly_compress_d4 * - * Description: Compression (du bits) and subsequent serialization of a - *polynomial + * Description: Compression (4 bits) and subsequent serialization of a + * polynomial * * Arguments: - uint8_t *r: pointer to output byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES) + * (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_du(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DU], const poly *a) -__contract__( - requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_DU)) - requires(memory_no_alias(a, sizeof(poly))) - requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) - assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_DU)) -); +void poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const poly *a); -#define poly_decompress_du MLKEM_NAMESPACE(poly_decompress_du) +#define poly_compress_d10 MLKEM_NAMESPACE(poly_compress_d10) /************************************************* - * Name: poly_decompress_du + * Name: poly_compress_d10 * - * Description: De-serialization and subsequent decompression (du bits) of a - *polynomial; approximate inverse of poly_compress_du + * 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 bytes) + * (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_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU]) -__contract__( - requires(memory_no_alias(a, MLKEM_POLYCOMPRESSEDBYTES_DU)) - requires(memory_no_alias(r, sizeof(poly))) - assigns(memory_slice(r, sizeof(poly))) - ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) -); +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) */ -#define poly_compress_dv MLKEM_NAMESPACE(poly_compress_dv) +#if defined(MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED) || MLKEM_K == 4 +#define poly_compress_d5 MLKEM_NAMESPACE(poly_compress_d5) /************************************************* - * Name: poly_compress_dv + * Name: poly_compress_d5 * - * Description: Compression (dv bits) and subsequent serialization of a - *polynomial + * Description: Compression (5 bits) and subsequent serialization of a + * polynomial * * Arguments: - uint8_t *r: pointer to output byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES_DV) + * (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_dv(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DV], const poly *a) -__contract__( - requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_DV)) - requires(memory_no_alias(a, sizeof(poly))) - requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) - assigns(object_whole(r)) -); +void poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const poly *a); -#define poly_decompress_dv MLKEM_NAMESPACE(poly_decompress_dv) +#define poly_compress_d11 MLKEM_NAMESPACE(poly_compress_d11) /************************************************* - * Name: poly_decompress_dv + * 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 + * 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_DV - *bytes) + * (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_dv(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV]) -__contract__( - requires(memory_no_alias(a, MLKEM_POLYCOMPRESSEDBYTES_DV)) - requires(memory_no_alias(r, sizeof(poly))) - assigns(object_whole(r)) - ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) -); +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) /************************************************* @@ -500,144 +552,6 @@ __contract__( assigns(object_whole(msg)) ); -#define poly_getnoise_eta1_4x MLKEM_NAMESPACE(poly_getnoise_eta1_4x) -/************************************************* - * Name: poly_getnoise_eta1_4x - * - * Description: Batch sample four polynomials deterministically from a seed - * and nonces, with output polynomials close to centered binomial distribution - * with parameter MLKEM_ETA1. - * - * Arguments: - poly *r{0,1,2,3}: pointer to output polynomial - * - const uint8_t *seed: pointer to input seed - * (of length MLKEM_SYMBYTES bytes) - * - uint8_t nonce{0,1,2,3}: one-byte input nonce - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_getnoise_eta1_4x(poly *r0, poly *r1, poly *r2, poly *r3, - const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0, - uint8_t nonce1, uint8_t nonce2, uint8_t nonce3) -/* Depending on MLKEM_K, the pointers passed to this function belong - to the same objects, so we cannot use memory_no_alias for r0-r3. - - NOTE: Somehow it is important to use memory_no_alias() first in the - conjunctions defining each case. -*/ -#if MLKEM_K == 2 -__contract__( - requires(memory_no_alias(seed, MLKEM_SYMBYTES)) - requires( /* Case A: r0, r1 consecutive, r2, r3 consecutive */ - (memory_no_alias(r0, 2 * sizeof(poly)) && memory_no_alias(r2, 2 * sizeof(poly)) && - r1 == r0 + 1 && r3 == r2 + 1 && !same_object(r0, r2))) - assigns(memory_slice(r0, sizeof(poly))) - assigns(memory_slice(r1, sizeof(poly))) - assigns(memory_slice(r2, sizeof(poly))) - assigns(memory_slice(r3, sizeof(poly))) - ensures( - array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)); -); -#elif MLKEM_K == 4 -__contract__( - requires(memory_no_alias(seed, MLKEM_SYMBYTES)) - requires( /* Case B: r0, r1, r2, r3 consecutive */ - (memory_no_alias(r0, 4 * sizeof(poly)) && r1 == r0 + 1 && r2 == r0 + 2 && r3 == r0 + 3)) - assigns(memory_slice(r0, sizeof(poly))) - assigns(memory_slice(r1, sizeof(poly))) - assigns(memory_slice(r2, sizeof(poly))) - assigns(memory_slice(r3, sizeof(poly))) - ensures( - array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)); -); -#elif MLKEM_K == 3 -__contract__( - requires(memory_no_alias(seed, MLKEM_SYMBYTES)) - requires( /* Case C: r0, r1, r2 consecutive */ - (memory_no_alias(r0, 3 * sizeof(poly)) && memory_no_alias(r3, 1 * sizeof(poly)) && - r1 == r0 + 1 && r2 == r0 + 2 && !same_object(r3, r0))) - assigns(memory_slice(r0, sizeof(poly))) - assigns(memory_slice(r1, sizeof(poly))) - assigns(memory_slice(r2, sizeof(poly))) - assigns(memory_slice(r3, sizeof(poly))) - ensures( - array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)); -); -#endif /* MLKEM_K */ - -#if MLKEM_ETA1 == MLKEM_ETA2 -/* - * We only require poly_getnoise_eta2_4x for ml-kem-768 and ml-kem-1024 - * where MLKEM_ETA2 = MLKEM_ETA1 = 2. - * For ml-kem-512, poly_getnoise_eta1122_4x is used instead. - */ -#define poly_getnoise_eta2_4x poly_getnoise_eta1_4x -#endif /* MLKEM_ETA1 == MLKEM_ETA2 */ - -#if MLKEM_K == 2 || MLKEM_K == 4 -#define poly_getnoise_eta2 MLKEM_NAMESPACE(poly_getnoise_eta2) -/************************************************* - * Name: poly_getnoise_eta2 - * - * Description: Sample a polynomial deterministically from a seed and a nonce, - * with output polynomial close to centered binomial distribution - * with parameter MLKEM_ETA2 - * - * Arguments: - poly *r: pointer to output polynomial - * - const uint8_t *seed: pointer to input seed - * (of length MLKEM_SYMBYTES bytes) - * - uint8_t nonce: one-byte input nonce - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES], - uint8_t nonce) -__contract__( - requires(memory_no_alias(r, sizeof(poly))) - requires(memory_no_alias(seed, MLKEM_SYMBYTES)) - assigns(object_whole(r)) - ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1)) -); -#endif /* MLKEM_K == 2 || MLKEM_K == 4 */ - -#if MLKEM_K == 2 -#define poly_getnoise_eta1122_4x MLKEM_NAMESPACE(poly_getnoise_eta1122_4x) -/************************************************* - * Name: poly_getnoise_eta1122_4x - * - * Description: Batch sample four polynomials deterministically from a seed - * and a nonces, with output polynomials close to centered binomial - * distribution with parameter MLKEM_ETA1 and MLKEM_ETA2 - * - * Arguments: - poly *r{0,1,2,3}: pointer to output polynomial - * - const uint8_t *seed: pointer to input seed - * (of length MLKEM_SYMBYTES bytes) - * - uint8_t nonce{0,1,2,3}: one-byte input nonce - **************************************************/ -MLKEM_NATIVE_INTERNAL_API -void poly_getnoise_eta1122_4x(poly *r0, poly *r1, poly *r2, poly *r3, - const uint8_t seed[MLKEM_SYMBYTES], - uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, - uint8_t nonce3) -__contract__( - requires( /* r0, r1 consecutive, r2, r3 consecutive */ - (memory_no_alias(r0, 2 * sizeof(poly)) && memory_no_alias(r2, 2 * sizeof(poly)) && - r1 == r0 + 1 && r3 == r2 + 1 && !same_object(r0, r2))) - requires(memory_no_alias(seed, MLKEM_SYMBYTES)) - assigns(object_whole(r0), object_whole(r1), object_whole(r2), object_whole(r3)) - ensures(array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) - && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA2 + 1) - && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA2 + 1)); -); -#endif /* MLKEM_K == 2 */ - #define poly_basemul_montgomery_cached \ MLKEM_NAMESPACE(poly_basemul_montgomery_cached) /************************************************* @@ -801,4 +715,4 @@ __contract__( assigns(object_whole(r)) ); -#endif +#endif /* POLY_H */ diff --git a/mlkem/polyvec.c b/mlkem/polyvec.c index 8c9d9ff75..c5866cbca 100644 --- a/mlkem/polyvec.c +++ b/mlkem/polyvec.c @@ -4,12 +4,23 @@ */ #include "polyvec.h" #include +#include #include "arith_backend.h" +#include "cbd.h" #include "ntt.h" #include "poly.h" +#include "symmetric.h" #include "debug/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 poly_cbd_eta1 MLKEM_NAMESPACE_K(poly_cbd_eta1) +#define poly_cbd_eta2 MLKEM_NAMESPACE_K(poly_cbd_eta2) +/* End of static namespacing */ + MLKEM_NATIVE_INTERNAL_API void polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU], const polyvec *a) @@ -175,3 +186,145 @@ void polyvec_tomont(polyvec *r) debug_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, MLKEM_Q); } + + +/************************************************* + * Name: poly_cbd_eta1 + * + * Description: Given an array of uniformly random bytes, compute + * polynomial with coefficients distributed according to + * a centered binomial distribution with parameter MLKEM_ETA1. + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *buf: pointer to input byte array + **************************************************/ +static INLINE void poly_cbd_eta1(poly *r, + const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4]) +__contract__( + requires(memory_no_alias(r, sizeof(poly))) + requires(memory_no_alias(buf, MLKEM_ETA1 * MLKEM_N / 4)) + assigns(memory_slice(r, sizeof(poly))) + ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_ETA1 + 1)) +) +{ +#if MLKEM_ETA1 == 2 + poly_cbd2(r, buf); +#elif MLKEM_ETA1 == 3 + poly_cbd3(r, buf); +#else +#error "Invalid value of MLKEM_ETA1" +#endif +} + +MLKEM_NATIVE_INTERNAL_API +void poly_getnoise_eta1_4x(poly *r0, poly *r1, poly *r2, poly *r3, + const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0, + uint8_t nonce1, uint8_t nonce2, uint8_t nonce3) +{ + ALIGN uint8_t buf0[MLKEM_ETA1 * MLKEM_N / 4]; + ALIGN uint8_t buf1[MLKEM_ETA1 * MLKEM_N / 4]; + ALIGN uint8_t buf2[MLKEM_ETA1 * MLKEM_N / 4]; + ALIGN uint8_t buf3[MLKEM_ETA1 * MLKEM_N / 4]; + ALIGN uint8_t extkey0[MLKEM_SYMBYTES + 1]; + ALIGN uint8_t extkey1[MLKEM_SYMBYTES + 1]; + ALIGN uint8_t extkey2[MLKEM_SYMBYTES + 1]; + ALIGN uint8_t extkey3[MLKEM_SYMBYTES + 1]; + memcpy(extkey0, seed, MLKEM_SYMBYTES); + memcpy(extkey1, seed, MLKEM_SYMBYTES); + memcpy(extkey2, seed, MLKEM_SYMBYTES); + memcpy(extkey3, seed, MLKEM_SYMBYTES); + extkey0[MLKEM_SYMBYTES] = nonce0; + extkey1[MLKEM_SYMBYTES] = nonce1; + extkey2[MLKEM_SYMBYTES] = nonce2; + extkey3[MLKEM_SYMBYTES] = nonce3; + prf_eta1_x4(buf0, buf1, buf2, buf3, extkey0, extkey1, extkey2, extkey3); + poly_cbd_eta1(r0, buf0); + poly_cbd_eta1(r1, buf1); + poly_cbd_eta1(r2, buf2); + poly_cbd_eta1(r3, buf3); + + debug_assert_abs_bound(r0, MLKEM_N, MLKEM_ETA1 + 1); + debug_assert_abs_bound(r1, MLKEM_N, MLKEM_ETA1 + 1); + debug_assert_abs_bound(r2, MLKEM_N, MLKEM_ETA1 + 1); + debug_assert_abs_bound(r3, MLKEM_N, MLKEM_ETA1 + 1); +} + +#if MLKEM_K == 2 || MLKEM_K == 4 +/************************************************* + * Name: poly_cbd_eta2 + * + * Description: Given an array of uniformly random bytes, compute + * polynomial with coefficients distributed according to + * a centered binomial distribution with parameter MLKEM_ETA2. + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *buf: pointer to input byte array + **************************************************/ +static INLINE void poly_cbd_eta2(poly *r, + const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4]) +__contract__( + requires(memory_no_alias(r, sizeof(poly))) + requires(memory_no_alias(buf, MLKEM_ETA2 * MLKEM_N / 4)) + assigns(memory_slice(r, sizeof(poly))) + ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1))) +{ +#if MLKEM_ETA2 == 2 + poly_cbd2(r, buf); +#else +#error "Invalid value of MLKEM_ETA2" +#endif +} + +MLKEM_NATIVE_INTERNAL_API +void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES], + uint8_t nonce) +{ + ALIGN uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4]; + ALIGN uint8_t extkey[MLKEM_SYMBYTES + 1]; + + memcpy(extkey, seed, MLKEM_SYMBYTES); + extkey[MLKEM_SYMBYTES] = nonce; + prf_eta2(buf, extkey); + + poly_cbd_eta2(r, buf); + + debug_assert_abs_bound(r, MLKEM_N, MLKEM_ETA1 + 1); +} +#endif /* MLKEM_K == 2 || MLKEM_K == 4 */ + + +#if MLKEM_K == 2 +MLKEM_NATIVE_INTERNAL_API +void poly_getnoise_eta1122_4x(poly *r0, poly *r1, poly *r2, poly *r3, + const uint8_t seed[MLKEM_SYMBYTES], + uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, + uint8_t nonce3) +{ + ALIGN uint8_t buf1[KECCAK_WAY / 2][MLKEM_ETA1 * MLKEM_N / 4]; + ALIGN uint8_t buf2[KECCAK_WAY / 2][MLKEM_ETA2 * MLKEM_N / 4]; + ALIGN uint8_t extkey[KECCAK_WAY][MLKEM_SYMBYTES + 1]; + memcpy(extkey[0], seed, MLKEM_SYMBYTES); + memcpy(extkey[1], seed, MLKEM_SYMBYTES); + memcpy(extkey[2], seed, MLKEM_SYMBYTES); + memcpy(extkey[3], seed, MLKEM_SYMBYTES); + extkey[0][MLKEM_SYMBYTES] = nonce0; + extkey[1][MLKEM_SYMBYTES] = nonce1; + extkey[2][MLKEM_SYMBYTES] = nonce2; + extkey[3][MLKEM_SYMBYTES] = nonce3; + + prf_eta1(buf1[0], extkey[0]); + prf_eta1(buf1[1], extkey[1]); + prf_eta2(buf2[0], extkey[2]); + prf_eta2(buf2[1], extkey[3]); + + poly_cbd_eta1(r0, buf1[0]); + poly_cbd_eta1(r1, buf1[1]); + poly_cbd_eta2(r2, buf2[0]); + poly_cbd_eta2(r3, buf2[1]); + + debug_assert_abs_bound(r0, MLKEM_N, MLKEM_ETA1 + 1); + debug_assert_abs_bound(r1, MLKEM_N, MLKEM_ETA1 + 1); + debug_assert_abs_bound(r2, MLKEM_N, MLKEM_ETA2 + 1); + debug_assert_abs_bound(r3, MLKEM_N, MLKEM_ETA2 + 1); +} +#endif /* MLKEM_K == 2 */ diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h index 77003c94b..8be8579e0 100644 --- a/mlkem/polyvec.h +++ b/mlkem/polyvec.h @@ -9,19 +9,144 @@ #include "common.h" #include "poly.h" -#define polyvec MLKEM_NAMESPACE(polyvec) +#define polyvec MLKEM_NAMESPACE_K(polyvec) typedef struct { poly vec[MLKEM_K]; } ALIGN polyvec; -#define polyvec_mulcache MLKEM_NAMESPACE(polyvec_mulcache) +#define polyvec_mulcache MLKEM_NAMESPACE_K(polyvec_mulcache) typedef struct { poly_mulcache vec[MLKEM_K]; } polyvec_mulcache; -#define polyvec_compress_du MLKEM_NAMESPACE(polyvec_compress_du) +#define poly_compress_du MLKEM_NAMESPACE_K(poly_compress_du) +/************************************************* + * Name: poly_compress_du + * + * Description: Compression (du bits) and subsequent serialization of a + * polynomial + * + * Arguments: - uint8_t *r: pointer to output byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_DU bytes) + * - const poly *a: pointer to input polynomial + * Coefficients must be unsigned canonical, + * i.e. in [0,1,..,MLKEM_Q-1]. + **************************************************/ +static INLINE void poly_compress_du(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DU], + const poly *a) +__contract__( + requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_DU)) + requires(memory_no_alias(a, sizeof(poly))) + requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) + assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_DU))) +{ +#if MLKEM_DU == 10 + poly_compress_d10(r, a); +#elif MLKEM_DU == 11 + poly_compress_d11(r, a); +#else +#error "Invalid value of MLKEM_DU" +#endif +} + +#define poly_decompress_du MLKEM_NAMESPACE_K(poly_decompress_du) +/************************************************* + * Name: poly_decompress_du + * + * Description: De-serialization and subsequent decompression (du bits) of a + * polynomial; approximate inverse of poly_compress_du + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *a: pointer to input byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_DU bytes) + * + * Upon return, the coefficients of the output polynomial are unsigned-canonical + * (non-negative and smaller than MLKEM_Q). + * + **************************************************/ +static INLINE void poly_decompress_du( + poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU]) +__contract__( + requires(memory_no_alias(a, MLKEM_POLYCOMPRESSEDBYTES_DU)) + requires(memory_no_alias(r, sizeof(poly))) + assigns(memory_slice(r, sizeof(poly))) + ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +{ +#if MLKEM_DU == 10 + poly_decompress_d10(r, a); +#elif MLKEM_DU == 11 + poly_decompress_d11(r, a); +#else +#error "Invalid value of MLKEM_DU" +#endif +} + +#define poly_compress_dv MLKEM_NAMESPACE_K(poly_compress_dv) +/************************************************* + * Name: poly_compress_dv + * + * Description: Compression (dv bits) and subsequent serialization of a + * polynomial + * + * Arguments: - uint8_t *r: pointer to output byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES_DV bytes) + * - const poly *a: pointer to input polynomial + * Coefficients must be unsigned canonical, + * i.e. in [0,1,..,MLKEM_Q-1]. + **************************************************/ +static INLINE void poly_compress_dv(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DV], + const poly *a) +__contract__( + requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_DV)) + requires(memory_no_alias(a, sizeof(poly))) + requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q)) + assigns(object_whole(r))) +{ +#if MLKEM_DV == 4 + poly_compress_d4(r, a); +#elif MLKEM_DV == 5 + poly_compress_d5(r, a); +#else +#error "Invalid value of MLKEM_DV" +#endif +} + + +#define poly_decompress_dv MLKEM_NAMESPACE_K(poly_decompress_dv) +/************************************************* + * Name: poly_decompress_dv + * + * 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_DV bytes) + * + * Upon return, the coefficients of the output polynomial are unsigned-canonical + * (non-negative and smaller than MLKEM_Q). + * + **************************************************/ +static INLINE void poly_decompress_dv( + poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV]) +__contract__( + requires(memory_no_alias(a, MLKEM_POLYCOMPRESSEDBYTES_DV)) + requires(memory_no_alias(r, sizeof(poly))) + assigns(object_whole(r)) + ensures(array_bound(r->coeffs, 0, MLKEM_N, 0, MLKEM_Q))) +{ +#if MLKEM_DV == 4 + poly_decompress_d4(r, a); +#elif MLKEM_DV == 5 + poly_decompress_d5(r, a); +#else +#error "Invalid value of MLKEM_DV" +#endif +} + +#define polyvec_compress_du MLKEM_NAMESPACE_K(polyvec_compress_du) /************************************************* * Name: polyvec_compress_du * @@ -44,7 +169,7 @@ __contract__( assigns(object_whole(r)) ); -#define polyvec_decompress_du MLKEM_NAMESPACE(polyvec_decompress_du) +#define polyvec_decompress_du MLKEM_NAMESPACE_K(polyvec_decompress_du) /************************************************* * Name: polyvec_decompress_du * @@ -67,7 +192,7 @@ __contract__( array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); -#define polyvec_tobytes MLKEM_NAMESPACE(polyvec_tobytes) +#define polyvec_tobytes MLKEM_NAMESPACE_K(polyvec_tobytes) /************************************************* * Name: polyvec_tobytes * @@ -88,7 +213,7 @@ __contract__( assigns(object_whole(r)) ); -#define polyvec_frombytes MLKEM_NAMESPACE(polyvec_frombytes) +#define polyvec_frombytes MLKEM_NAMESPACE_K(polyvec_frombytes) /************************************************* * Name: polyvec_frombytes * @@ -110,7 +235,7 @@ __contract__( array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, UINT12_LIMIT))) ); -#define polyvec_ntt MLKEM_NAMESPACE(polyvec_ntt) +#define polyvec_ntt MLKEM_NAMESPACE_K(polyvec_ntt) /************************************************* * Name: polyvec_ntt * @@ -136,7 +261,7 @@ __contract__( array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, NTT_BOUND))) ); -#define polyvec_invntt_tomont MLKEM_NAMESPACE(polyvec_invntt_tomont) +#define polyvec_invntt_tomont MLKEM_NAMESPACE_K(polyvec_invntt_tomont) /************************************************* * Name: polyvec_invntt_tomont * @@ -162,7 +287,7 @@ __contract__( ); #define polyvec_basemul_acc_montgomery \ - MLKEM_NAMESPACE(polyvec_basemul_acc_montgomery) + MLKEM_NAMESPACE_K(polyvec_basemul_acc_montgomery) /************************************************* * Name: polyvec_basemul_acc_montgomery * @@ -186,7 +311,7 @@ __contract__( #define polyvec_basemul_acc_montgomery_cached \ - MLKEM_NAMESPACE(polyvec_basemul_acc_montgomery_cached) + MLKEM_NAMESPACE_K(polyvec_basemul_acc_montgomery_cached) /************************************************* * Name: polyvec_basemul_acc_montgomery_cached * @@ -218,7 +343,7 @@ __contract__( assigns(memory_slice(r, sizeof(poly))) ); -#define polyvec_mulcache_compute MLKEM_NAMESPACE(polyvec_mulcache_compute) +#define polyvec_mulcache_compute MLKEM_NAMESPACE_K(polyvec_mulcache_compute) /************************************************************ * Name: polyvec_mulcache_compute * @@ -252,7 +377,7 @@ __contract__( assigns(object_whole(x)) ); -#define polyvec_reduce MLKEM_NAMESPACE(polyvec_reduce) +#define polyvec_reduce MLKEM_NAMESPACE_K(polyvec_reduce) /************************************************* * Name: polyvec_reduce * @@ -278,7 +403,7 @@ __contract__( array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) ); -#define polyvec_add MLKEM_NAMESPACE(polyvec_add) +#define polyvec_add MLKEM_NAMESPACE_K(polyvec_add) /************************************************* * Name: polyvec_add * @@ -309,7 +434,7 @@ __contract__( assigns(object_whole(r)) ); -#define polyvec_tomont MLKEM_NAMESPACE(polyvec_tomont) +#define polyvec_tomont MLKEM_NAMESPACE_K(polyvec_tomont) /************************************************* * Name: polyvec_tomont * @@ -329,4 +454,142 @@ __contract__( array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q))) ); +#define poly_getnoise_eta1_4x MLKEM_NAMESPACE_K(poly_getnoise_eta1_4x) +/************************************************* + * Name: poly_getnoise_eta1_4x + * + * Description: Batch sample four polynomials deterministically from a seed + * and nonces, with output polynomials close to centered binomial distribution + * with parameter MLKEM_ETA1. + * + * Arguments: - poly *r{0,1,2,3}: pointer to output polynomial + * - const uint8_t *seed: pointer to input seed + * (of length MLKEM_SYMBYTES bytes) + * - uint8_t nonce{0,1,2,3}: one-byte input nonce + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_getnoise_eta1_4x(poly *r0, poly *r1, poly *r2, poly *r3, + const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0, + uint8_t nonce1, uint8_t nonce2, uint8_t nonce3) +/* Depending on MLKEM_K, the pointers passed to this function belong + to the same objects, so we cannot use memory_no_alias for r0-r3. + + NOTE: Somehow it is important to use memory_no_alias() first in the + conjunctions defining each case. +*/ +#if MLKEM_K == 2 +__contract__( + requires(memory_no_alias(seed, MLKEM_SYMBYTES)) + requires( /* Case A: r0, r1 consecutive, r2, r3 consecutive */ + (memory_no_alias(r0, 2 * sizeof(poly)) && memory_no_alias(r2, 2 * sizeof(poly)) && + r1 == r0 + 1 && r3 == r2 + 1 && !same_object(r0, r2))) + assigns(memory_slice(r0, sizeof(poly))) + assigns(memory_slice(r1, sizeof(poly))) + assigns(memory_slice(r2, sizeof(poly))) + assigns(memory_slice(r3, sizeof(poly))) + ensures( + array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)); +); +#elif MLKEM_K == 4 +__contract__( + requires(memory_no_alias(seed, MLKEM_SYMBYTES)) + requires( /* Case B: r0, r1, r2, r3 consecutive */ + (memory_no_alias(r0, 4 * sizeof(poly)) && r1 == r0 + 1 && r2 == r0 + 2 && r3 == r0 + 3)) + assigns(memory_slice(r0, sizeof(poly))) + assigns(memory_slice(r1, sizeof(poly))) + assigns(memory_slice(r2, sizeof(poly))) + assigns(memory_slice(r3, sizeof(poly))) + ensures( + array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)); +); +#elif MLKEM_K == 3 +__contract__( + requires(memory_no_alias(seed, MLKEM_SYMBYTES)) + requires( /* Case C: r0, r1, r2 consecutive */ + (memory_no_alias(r0, 3 * sizeof(poly)) && memory_no_alias(r3, 1 * sizeof(poly)) && + r1 == r0 + 1 && r2 == r0 + 2 && !same_object(r3, r0))) + assigns(memory_slice(r0, sizeof(poly))) + assigns(memory_slice(r1, sizeof(poly))) + assigns(memory_slice(r2, sizeof(poly))) + assigns(memory_slice(r3, sizeof(poly))) + ensures( + array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1)); +); +#endif /* MLKEM_K */ + +#if MLKEM_ETA1 == MLKEM_ETA2 +/* + * We only require poly_getnoise_eta2_4x for ml-kem-768 and ml-kem-1024 + * where MLKEM_ETA2 = MLKEM_ETA1 = 2. + * For ml-kem-512, poly_getnoise_eta1122_4x is used instead. + */ +#define poly_getnoise_eta2_4x poly_getnoise_eta1_4x +#endif /* MLKEM_ETA1 == MLKEM_ETA2 */ + +#if MLKEM_K == 2 || MLKEM_K == 4 +#define poly_getnoise_eta2 MLKEM_NAMESPACE_K(poly_getnoise_eta2) +/************************************************* + * Name: poly_getnoise_eta2 + * + * Description: Sample a polynomial deterministically from a seed and a nonce, + * with output polynomial close to centered binomial distribution + * with parameter MLKEM_ETA2 + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *seed: pointer to input seed + * (of length MLKEM_SYMBYTES bytes) + * - uint8_t nonce: one-byte input nonce + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES], + uint8_t nonce) +__contract__( + requires(memory_no_alias(r, sizeof(poly))) + requires(memory_no_alias(seed, MLKEM_SYMBYTES)) + assigns(object_whole(r)) + ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1)) +); +#endif /* MLKEM_K == 2 || MLKEM_K == 4 */ + +#if MLKEM_K == 2 +#define poly_getnoise_eta1122_4x MLKEM_NAMESPACE_K(poly_getnoise_eta1122_4x) +/************************************************* + * Name: poly_getnoise_eta1122_4x + * + * Description: Batch sample four polynomials deterministically from a seed + * and a nonces, with output polynomials close to centered binomial + * distribution with parameter MLKEM_ETA1 and MLKEM_ETA2 + * + * Arguments: - poly *r{0,1,2,3}: pointer to output polynomial + * - const uint8_t *seed: pointer to input seed + * (of length MLKEM_SYMBYTES bytes) + * - uint8_t nonce{0,1,2,3}: one-byte input nonce + **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_getnoise_eta1122_4x(poly *r0, poly *r1, poly *r2, poly *r3, + const uint8_t seed[MLKEM_SYMBYTES], + uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, + uint8_t nonce3) +__contract__( + requires( /* r0, r1 consecutive, r2, r3 consecutive */ + (memory_no_alias(r0, 2 * sizeof(poly)) && memory_no_alias(r2, 2 * sizeof(poly)) && + r1 == r0 + 1 && r3 == r2 + 1 && !same_object(r0, r2))) + requires(memory_no_alias(seed, MLKEM_SYMBYTES)) + assigns(object_whole(r0), object_whole(r1), object_whole(r2), object_whole(r3)) + ensures(array_abs_bound(r0->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r1->coeffs,0, MLKEM_N, MLKEM_ETA1 + 1) + && array_abs_bound(r2->coeffs,0, MLKEM_N, MLKEM_ETA2 + 1) + && array_abs_bound(r3->coeffs,0, MLKEM_N, MLKEM_ETA2 + 1)); +); +#endif /* MLKEM_K == 2 */ + #endif diff --git a/mlkem/rej_uniform.c b/mlkem/rej_uniform.c index 69741fed5..fbebe9688 100644 --- a/mlkem/rej_uniform.c +++ b/mlkem/rej_uniform.c @@ -2,47 +2,24 @@ * 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 "rej_uniform.h" #include "arith_backend.h" #include "debug/debug.h" +#include "fips202/fips202.h" +#include "fips202/fips202x4.h" +#include "rej_uniform.h" +#include "symmetric.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 rej_uniform MLKEM_NAMESPACE(rej_uniform) #define rej_uniform_scalar MLKEM_NAMESPACE(rej_uniform_scalar) /* End of static namespacing */ -/************************************************* - * Name: rej_uniform_scalar - * - * Description: Run rejection sampling on uniform random bytes to generate - * uniform random integers mod q - * - * Arguments: - int16_t *r: pointer to output buffer - * - unsigned int target: requested number of 16-bit integers - * (uniform mod q). - * Must be <= 4096. - * - unsigned int offset: number of 16-bit integers that have - * already been sampled. - * Must be <= target. - * - const uint8_t *buf: pointer to input buffer - * (assumed to be uniform random bytes) - * - unsigned int buflen: length of input buffer in bytes - * Must be <= 4096. - * Must be a multiple of 3. - * - * Note: Strictly speaking, only a few values of buflen near UINT_MAX need - * excluding. The limit of 4096 is somewhat arbitary but sufficient for all - * uses of this function. Similarly, the actual limit for target is UINT_MAX/2. - * - * Returns the new offset of sampled 16-bit integers, at most target, - * and at least the initial offset. - * If the new offset is strictly less than len, all of the input buffers - * is guaranteed to have been consumed. If it is equal to len, no information - * is provided on how many bytes of the input buffer have been consumed. - **************************************************/ static unsigned int rej_uniform_scalar(int16_t *r, unsigned int target, unsigned int offset, const uint8_t *buf, unsigned int buflen) @@ -88,16 +65,61 @@ __contract__( } #if !defined(MLKEM_USE_NATIVE_REJ_UNIFORM) -unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset, - const uint8_t *buf, unsigned int buflen) +/************************************************* + * Name: rej_uniform + * + * Description: Run rejection sampling on uniform random bytes to generate + * uniform random integers mod q + * + * Arguments: - int16_t *r: pointer to output buffer + * - unsigned int target: requested number of 16-bit integers + * (uniform mod q). + * Must be <= 4096. + * - unsigned int offset: number of 16-bit integers that have + * already been sampled. + * Must be <= target. + * - const uint8_t *buf: pointer to input buffer + * (assumed to be uniform random bytes) + * - unsigned int buflen: length of input buffer in bytes + * Must be <= 4096. + * Must be a multiple of 3. + * + * Note: Strictly speaking, only a few values of buflen near UINT_MAX need + * excluding. The limit of 4096 is somewhat arbitary but sufficient for all + * uses of this function. Similarly, the actual limit for target is UINT_MAX/2. + * + * Returns the new offset of sampled 16-bit integers, at most target, + * and at least the initial offset. + * If the new offset is strictly less than len, all of the input buffers + * is guaranteed to have been consumed. If it is equal to len, no information + * is provided on how many bytes of the input buffer have been consumed. + **************************************************/ + +/* + * NOTE: The signature differs from the Kyber reference implementation + * in that it adds the offset and always expects the base of the target + * buffer. This avoids shifting the buffer base in the caller, which appears + * tricky to reason about. + */ +static unsigned int rej_uniform(int16_t *r, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen) +__contract__( + requires(offset <= target && target <= 4096 && buflen <= 4096 && buflen % 3 == 0) + requires(memory_no_alias(r, sizeof(int16_t) * target)) + requires(memory_no_alias(buf, buflen)) + requires(offset > 0 ==> array_bound(r, 0, offset, 0, MLKEM_Q)) + assigns(memory_slice(r, sizeof(int16_t) * target)) + ensures(offset <= return_value && return_value <= target) + ensures(return_value > 0 ==> array_bound(r, 0, return_value, 0, MLKEM_Q)) +) { return rej_uniform_scalar(r, target, offset, buf, buflen); } #else /* MLKEM_USE_NATIVE_REJ_UNIFORM */ - -MLKEM_NATIVE_INTERNAL_API -unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset, - const uint8_t *buf, unsigned int buflen) +static unsigned int rej_uniform(int16_t *r, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen) { int ret; @@ -113,3 +135,103 @@ unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset, return rej_uniform_scalar(r, target, offset, buf, buflen); } #endif /* MLKEM_USE_NATIVE_REJ_UNIFORM */ + +#ifndef MLKEM_GEN_MATRIX_NBLOCKS +#define MLKEM_GEN_MATRIX_NBLOCKS \ + ((12 * MLKEM_N / 8 * (1 << 12) / MLKEM_Q + XOF_RATE) / XOF_RATE) +#endif + +MLKEM_NATIVE_INTERNAL_API +void poly_rej_uniform_x4(poly *vec, uint8_t *seed[4]) +{ + /* Temporary buffers for XOF output before rejection sampling */ + uint8_t buf0[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; + uint8_t buf1[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; + uint8_t buf2[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; + uint8_t buf3[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; + + /* Tracks the number of coefficients we have already sampled */ + unsigned int ctr[KECCAK_WAY]; + xof_x4_ctx statex; + unsigned int buflen; + + /* seed is MLKEM_SYMBYTES + 2 bytes long, but padded to MLKEM_SYMBYTES + 16 */ + xof_x4_absorb(&statex, seed[0], seed[1], seed[2], seed[3], + MLKEM_SYMBYTES + 2); + + /* + * Initially, squeeze heuristic number of MLKEM_GEN_MATRIX_NBLOCKS. + * This should generate the matrix entries with high probability. + */ + xof_x4_squeezeblocks(buf0, buf1, buf2, buf3, MLKEM_GEN_MATRIX_NBLOCKS, + &statex); + buflen = MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE; + ctr[0] = rej_uniform(vec[0].coeffs, MLKEM_N, 0, buf0, buflen); + ctr[1] = rej_uniform(vec[1].coeffs, MLKEM_N, 0, buf1, buflen); + ctr[2] = rej_uniform(vec[2].coeffs, MLKEM_N, 0, buf2, buflen); + ctr[3] = rej_uniform(vec[3].coeffs, MLKEM_N, 0, buf3, buflen); + + /* + * So long as not all matrix entries have been generated, squeeze + * one more block a time until we're done. + */ + buflen = XOF_RATE; + while (ctr[0] < MLKEM_N || ctr[1] < MLKEM_N || ctr[2] < MLKEM_N || + ctr[3] < MLKEM_N) + __loop__( + assigns(ctr, statex, memory_slice(vec, sizeof(poly) * 4), object_whole(buf0), + object_whole(buf1), object_whole(buf2), object_whole(buf3)) + invariant(ctr[0] <= MLKEM_N && ctr[1] <= MLKEM_N) + invariant(ctr[2] <= MLKEM_N && ctr[3] <= MLKEM_N) + invariant(ctr[0] > 0 ==> array_bound(vec[0].coeffs, 0, ctr[0], 0, MLKEM_Q)) + invariant(ctr[1] > 0 ==> array_bound(vec[1].coeffs, 0, ctr[1], 0, MLKEM_Q)) + invariant(ctr[2] > 0 ==> array_bound(vec[2].coeffs, 0, ctr[2], 0, MLKEM_Q)) + invariant(ctr[3] > 0 ==> array_bound(vec[3].coeffs, 0, ctr[3], 0, MLKEM_Q))) + { + xof_x4_squeezeblocks(buf0, buf1, buf2, buf3, 1, &statex); + ctr[0] = rej_uniform(vec[0].coeffs, MLKEM_N, ctr[0], buf0, buflen); + ctr[1] = rej_uniform(vec[1].coeffs, MLKEM_N, ctr[1], buf1, buflen); + ctr[2] = rej_uniform(vec[2].coeffs, MLKEM_N, ctr[2], buf2, buflen); + ctr[3] = rej_uniform(vec[3].coeffs, MLKEM_N, ctr[3], buf3, buflen); + } + + xof_x4_release(&statex); +} + +MLKEM_NATIVE_INTERNAL_API +void poly_rej_uniform(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 2]) +{ + xof_ctx state; + uint8_t buf[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE]; + unsigned int ctr, buflen; + + xof_absorb(&state, seed, MLKEM_SYMBYTES + 2); + + /* Initially, squeeze + sample heuristic number of MLKEM_GEN_MATRIX_NBLOCKS. + */ + /* This should generate the matrix entry with high probability. */ + xof_squeezeblocks(buf, MLKEM_GEN_MATRIX_NBLOCKS, &state); + buflen = MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE; + ctr = rej_uniform(entry->coeffs, MLKEM_N, 0, buf, buflen); + + /* Squeeze + sample one more block a time until we're done */ + buflen = XOF_RATE; + while (ctr < MLKEM_N) + __loop__( + assigns(ctr, state, memory_slice(entry, sizeof(poly)), object_whole(buf)) + invariant(ctr <= MLKEM_N) + invariant(array_bound(entry->coeffs, 0, ctr, 0, MLKEM_Q))) + { + xof_squeezeblocks(buf, 1, &state); + ctr = rej_uniform(entry->coeffs, MLKEM_N, ctr, buf, buflen); + } + + xof_release(&state); +} + +#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ + +#define empty_cu_rej_uniform MLKEM_NAMESPACE_K(empty_cu_rej_uniform) +int empty_cu_rej_uniform; + +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/rej_uniform.h b/mlkem/rej_uniform.h index 13db836bc..801287259 100644 --- a/mlkem/rej_uniform.h +++ b/mlkem/rej_uniform.h @@ -9,54 +9,55 @@ #include #include "cbmc.h" #include "common.h" +#include "poly.h" -#define rej_uniform MLKEM_NAMESPACE(rej_uniform) +#define poly_rej_uniform_x4 MLKEM_NAMESPACE(poly_rej_uniform_x4) /************************************************* - * Name: rej_uniform + * Name: poly_rej_uniform_x4 * - * Description: Run rejection sampling on uniform random bytes to generate - * uniform random integers mod q + * Description: Generate four polynomials using rejection sampling + * on (pseudo-)uniformly random bytes sampled from a seed. * - * Arguments: - int16_t *r: pointer to output buffer - * - unsigned int target: requested number of 16-bit integers - * (uniform mod q). - * Must be <= 4096. - * - unsigned int offset: number of 16-bit integers that have - * already been sampled. - * Must be <= target. - * - const uint8_t *buf: pointer to input buffer - * (assumed to be uniform random bytes) - * - unsigned int buflen: length of input buffer in bytes - * Must be <= 4096. - * Must be a multiple of 3. + * Arguments: - poly *vec: Pointer to an array of 4 polynomials + * to be sampled. + * - uint8_t *seed[4]: Pointer to array of four pointers + * pointing to the seed buffers of size + * MLKEM_SYMBYTES + 2 each. * - * Note: Strictly speaking, only a few values of buflen near UINT_MAX need - * excluding. The limit of 4096 is somewhat arbitary but sufficient for all - * uses of this function. Similarly, the actual limit for target is UINT_MAX/2. - * - * Returns the new offset of sampled 16-bit integers, at most target, - * and at least the initial offset. - * If the new offset is strictly less than len, all of the input buffers - * is guaranteed to have been consumed. If it is equal to len, no information - * is provided on how many bytes of the input buffer have been consumed. **************************************************/ +MLKEM_NATIVE_INTERNAL_API +void poly_rej_uniform_x4(poly *vec, uint8_t *seed[4]) +__contract__( + requires(memory_no_alias(vec, sizeof(poly) * 4)) + requires(memory_no_alias(seed, sizeof(uint8_t*) * 4)) + requires(memory_no_alias(seed[0], MLKEM_SYMBYTES + 2)) + requires(memory_no_alias(seed[1], MLKEM_SYMBYTES + 2)) + requires(memory_no_alias(seed[2], MLKEM_SYMBYTES + 2)) + requires(memory_no_alias(seed[3], MLKEM_SYMBYTES + 2)) + assigns(memory_slice(vec, sizeof(poly) * 4)) + ensures(array_bound(vec[0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)) + ensures(array_bound(vec[1].coeffs, 0, MLKEM_N, 0, MLKEM_Q)) + ensures(array_bound(vec[2].coeffs, 0, MLKEM_N, 0, MLKEM_Q)) + ensures(array_bound(vec[3].coeffs, 0, MLKEM_N, 0, MLKEM_Q))); -/* - * NOTE: The signature differs from the Kyber reference implementation - * in that it adds the offset and always expects the base of the target - * buffer. This avoids shifting the buffer base in the caller, which appears - * tricky to reason about. - */ +#define poly_rej_uniform MLKEM_NAMESPACE(poly_rej_uniform) +/************************************************* + * Name: poly_rej_uniform + * + * Description: Generate polynomial using rejection sampling + * on (pseudo-)uniformly random bytes sampled from a seed. + * + * Arguments: - poly *vec: Pointer to polynomial to be sampled. + * - uint8_t *seed: Pointer to seed buffer of size + * MLKEM_SYMBYTES + 2 each. + * + **************************************************/ MLKEM_NATIVE_INTERNAL_API -unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset, - const uint8_t *buf, unsigned int buflen) +void poly_rej_uniform(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 2]) __contract__( - requires(offset <= target && target <= 4096 && buflen <= 4096 && buflen % 3 == 0) - requires(memory_no_alias(r, sizeof(int16_t) * target)) - requires(memory_no_alias(buf, buflen)) - requires(offset > 0 ==> array_bound(r, 0, offset, 0, MLKEM_Q)) - assigns(memory_slice(r, sizeof(int16_t) * target)) - ensures(offset <= return_value && return_value <= target) - ensures(return_value > 0 ==> array_bound(r, 0, return_value, 0, MLKEM_Q)) -); -#endif + requires(memory_no_alias(entry, sizeof(poly))) + requires(memory_no_alias(seed, MLKEM_SYMBYTES + 2)) + assigns(memory_slice(entry, sizeof(poly))) + ensures(array_bound(entry->coeffs, 0, MLKEM_N, 0, MLKEM_Q))); + +#endif /* REJ_UNIFORM_H */ diff --git a/mlkem/symmetric.h b/mlkem/symmetric.h index a53df36b6..d4c8f968e 100644 --- a/mlkem/symmetric.h +++ b/mlkem/symmetric.h @@ -10,6 +10,7 @@ #include "cbmc.h" #include "common.h" #include "fips202/fips202.h" +#include "fips202/fips202x4.h" /* Macros denoting FIPS-203 specific Hash functions */ diff --git a/mlkem/verify.c b/mlkem/verify.c index b7078fcc1..9f39dcd22 100644 --- a/mlkem/verify.c +++ b/mlkem/verify.c @@ -4,7 +4,8 @@ */ #include "verify.h" -#if !defined(MLKEM_USE_ASM_VALUE_BARRIER) +#if !defined(MLKEM_USE_ASM_VALUE_BARRIER) && \ + !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) /* * Masking value used in constant-time functions from * verify.h to block the compiler's range analysis and @@ -12,9 +13,11 @@ */ volatile uint64_t ct_opt_blocker_u64 = 0; -#else /* MLKEM_USE_ASM_VALUE_BARRIER */ +#else /* MLKEM_USE_ASM_VALUE_BARRIER && \ + !MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ -#define empty_cu_verify MLKEM_NAMESPACE(empty_cu_verify) +#define empty_cu_verify MLKEM_NAMESPACE_K(empty_cu_verify) int empty_cu_verify; -#endif /* MLKEM_USE_ASM_VALUE_BARRIER */ +#endif /* MLKEM_USE_ASM_VALUE_BARRIER && \ + !MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/mlkem/verify.h b/mlkem/verify.h index aa8e8437e..f6ecf5eba 100644 --- a/mlkem/verify.h +++ b/mlkem/verify.h @@ -314,4 +314,4 @@ __contract__( } } -#endif +#endif /* VERIFY_H */ diff --git a/mlkem/zetas.c b/mlkem/zetas.c index 1a26e0dd5..4ef887c62 100644 --- a/mlkem/zetas.c +++ b/mlkem/zetas.c @@ -8,6 +8,8 @@ * Do not modify it directly. */ +#include "common.h" +#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED) #include "ntt.h" /* @@ -28,3 +30,10 @@ ALIGN const int16_t zetas[128] = { -1187, -1659, -1185, -1530, -1278, 794, -1510, -854, -870, 478, -108, -308, 996, 991, 958, -1460, 1522, 1628, }; + +#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ + +#define empty_cu_zetas MLKEM_NAMESPACE_K(empty_cu_zetas) +int empty_cu_zetas; + +#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */ diff --git a/proofs/cbmc/gen_matrix/Makefile b/proofs/cbmc/gen_matrix/Makefile index 1b18b3625..9e927981c 100644 --- a/proofs/cbmc/gen_matrix/Makefile +++ b/proofs/cbmc/gen_matrix/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix_entry $(MLKEM_NAMESPACE)gen_matrix_entry_x4 $(MLKEM_NAMESPACE)poly_permute_bitrev_to_custom +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform $(MLKEM_NAMESPACE)poly_rej_uniform_x4 $(MLKEM_NAMESPACE)poly_permute_bitrev_to_custom APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/gen_matrix_entry/gen_matrix_entry_harness.c b/proofs/cbmc/gen_matrix_entry/gen_matrix_entry_harness.c index fd3d8635d..232cd2ec3 100644 --- a/proofs/cbmc/gen_matrix_entry/gen_matrix_entry_harness.c +++ b/proofs/cbmc/gen_matrix_entry/gen_matrix_entry_harness.c @@ -6,12 +6,12 @@ #include "poly.h" // declare here since it's static in non-CBMC builds -#define gen_matrix_entry MLKEM_NAMESPACE(gen_matrix_entry) -void gen_matrix_entry(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 16]); +#define poly_rej_uniform MLKEM_NAMESPACE(poly_rej_uniform) +void poly_rej_uniform(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 16]); void harness(void) { poly *out; uint8_t *seed; - gen_matrix_entry(out, seed); + poly_rej_uniform(out, seed); } diff --git a/proofs/cbmc/invntt_layer/Makefile b/proofs/cbmc/invntt_layer/Makefile index 88eebc8b9..77ca82d2f 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 = 8 +CBMC_OBJECT_BITS = 9 # 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/poly_cbd_eta1/Makefile b/proofs/cbmc/poly_cbd_eta1/Makefile index bc3c16d16..409e3b4d6 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 +PROJECT_SOURCES += $(SRCDIR)/mlkem/cbd.c $(SRCDIR)/mlkem/polyvec.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta1 USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c b/proofs/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c index cc0bd954d..b3b0978e4 100644 --- a/proofs/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c +++ b/proofs/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c @@ -2,7 +2,10 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "poly.h" + +#define poly_cbd_eta1 MLKEM_NAMESPACE(poly_cbd_eta1) +void poly_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4]); void harness(void) { diff --git a/proofs/cbmc/poly_cbd_eta2/Makefile b/proofs/cbmc/poly_cbd_eta2/Makefile index 95ee738b4..27472c186 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 +PROJECT_SOURCES += $(SRCDIR)/mlkem/cbd.c $(SRCDIR)/mlkem/polyvec.c # Only relevant for K=2 or K=4 ifeq ($(MLKEM_K),2) diff --git a/proofs/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c b/proofs/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c index f3b27572a..6f40df578 100644 --- a/proofs/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c +++ b/proofs/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c @@ -2,7 +2,10 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 -#include +#include "poly.h" + +#define poly_cbd_eta2 MLKEM_NAMESPACE(poly_cbd_eta2) +void poly_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4]); void harness(void) { 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 53d04761f..c3b06996c 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 "poly.h" +#include "polyvec.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 e7a185235..685748b7e 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 "poly.h" +#include "polyvec.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 6b1f02d8b..d64f6b68e 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 "poly.h" +#include "polyvec.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 202f15951..3816fb8a3 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 "poly.h" +#include "polyvec.h" void harness(void) { diff --git a/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile b/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile index d1f214d46..f602715d8 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/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.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 56b1ed2fb..367e10c8c 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 66653e735..a163b03ba 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/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_getnoise_eta1_4x USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta1 $(FIPS202_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 9231f3055..6fc13427e 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 6f1f5aa7f..51645df77 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/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.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 2fcb3b634..c82ff5508 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/gen_matrix_entry/Makefile b/proofs/cbmc/poly_rej_uniform/Makefile similarity index 87% rename from proofs/cbmc/gen_matrix_entry/Makefile rename to proofs/cbmc/poly_rej_uniform/Makefile index 9999c3ed2..339c8196c 100644 --- a/proofs/cbmc/gen_matrix_entry/Makefile +++ b/proofs/cbmc/poly_rej_uniform/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = gen_matrix_entry_harness +HARNESS_FILE = poly_rej_uniform_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = gen_matrix_entry +PROOF_UID = poly_rej_uniform DEFINES += INCLUDES += @@ -16,9 +16,9 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c $(SRCDIR)/mlkem/fips202/fips202.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/rej_uniform.c $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix_entry +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128_absorb_once $(FIPS202_NAMESPACE)shake128_squeezeblocks $(MLKEM_NAMESPACE)rej_uniform APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(MLKEM_NAMESPACE)gen_matrix_entry +FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_rej_uniform # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will diff --git a/proofs/cbmc/gen_matrix_entry/cbmc-proof.txt b/proofs/cbmc/poly_rej_uniform/cbmc-proof.txt similarity index 100% rename from proofs/cbmc/gen_matrix_entry/cbmc-proof.txt rename to proofs/cbmc/poly_rej_uniform/cbmc-proof.txt diff --git a/proofs/cbmc/poly_rej_uniform/poly_rej_uniform_harness.c b/proofs/cbmc/poly_rej_uniform/poly_rej_uniform_harness.c new file mode 100644 index 000000000..d65d33240 --- /dev/null +++ b/proofs/cbmc/poly_rej_uniform/poly_rej_uniform_harness.c @@ -0,0 +1,13 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "rej_uniform.h" + +void harness(void) +{ + poly *out; + uint8_t *seed; + poly_rej_uniform(out, seed); +} diff --git a/proofs/cbmc/gen_matrix_entry_x4/Makefile b/proofs/cbmc/poly_rej_uniform_x4/Makefile similarity index 87% rename from proofs/cbmc/gen_matrix_entry_x4/Makefile rename to proofs/cbmc/poly_rej_uniform_x4/Makefile index 4202357a3..253250e9a 100644 --- a/proofs/cbmc/gen_matrix_entry_x4/Makefile +++ b/proofs/cbmc/poly_rej_uniform_x4/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = gen_matrix_entry_x4_harness +HARNESS_FILE = poly_rej_uniform_x4_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = gen_matrix_entry_x4 +PROOF_UID = poly_rej_uniform_x4 DEFINES += INCLUDES += @@ -16,9 +16,9 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c $(SRCDIR)/mlkem/fips202/fips202x4.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/rej_uniform.c $(SRCDIR)/mlkem/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix_entry_x4 +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform_x4 USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128x4_absorb_once $(FIPS202_NAMESPACE)shake128x4_squeezeblocks $(MLKEM_NAMESPACE)rej_uniform APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = $(MLKEM_NAMESPACE)gen_matrix_entry_x4 +FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_rej_uniform_x4 # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will diff --git a/proofs/cbmc/gen_matrix_entry_x4/cbmc-proof.txt b/proofs/cbmc/poly_rej_uniform_x4/cbmc-proof.txt similarity index 100% rename from proofs/cbmc/gen_matrix_entry_x4/cbmc-proof.txt rename to proofs/cbmc/poly_rej_uniform_x4/cbmc-proof.txt diff --git a/proofs/cbmc/gen_matrix_entry_x4/gen_matrix_entry_x4_harness.c b/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c similarity index 51% rename from proofs/cbmc/gen_matrix_entry_x4/gen_matrix_entry_x4_harness.c rename to proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c index 403ca1e9e..fd0b19b09 100644 --- a/proofs/cbmc/gen_matrix_entry_x4/gen_matrix_entry_x4_harness.c +++ b/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c @@ -3,15 +3,11 @@ // SPDX-License-Identifier: MIT-0 #include -#include "poly.h" - -// declare here since it's static in non-CBMC builds -#define gen_matrix_entry_x4 MLKEM_NAMESPACE(gen_matrix_entry_x4) -void gen_matrix_entry_x4(poly vec[4], uint8_t *seed[4]); +#include "rej_uniform.h" void harness(void) { poly out[4]; uint8_t *seed[4]; - gen_matrix_entry_x4(out, seed); + poly_rej_uniform_x4(out, seed); } diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile index 808591641..387f77dbf 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile @@ -36,7 +36,7 @@ FUNCTION_NAME = polyvec_basemul_acc_montgomery # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 8 +CBMC_OBJECT_BITS = 9 # 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/polyvec_basemul_acc_montgomery_cached/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile index a0e9205a1..036e93afa 100644 --- a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile @@ -36,7 +36,7 @@ FUNCTION_NAME = polyvec_basemul_acc_montgomery_cached # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 8 +CBMC_OBJECT_BITS = 9 # 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/rej_uniform/rej_uniform_harness.c b/proofs/cbmc/rej_uniform/rej_uniform_harness.c index fadefc59a..eccac7a54 100644 --- a/proofs/cbmc/rej_uniform/rej_uniform_harness.c +++ b/proofs/cbmc/rej_uniform/rej_uniform_harness.c @@ -2,8 +2,12 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 +#include #include "cbmc.h" -#include "rej_uniform.h" + +#define rej_uniform MLKEM_NAMESPACE(rej_uniform) +unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset, + const uint8_t *buf, unsigned int buflen); void harness(void) { diff --git a/scripts/autogen b/scripts/autogen index 5aacfd1ff..1a9af238b 100755 --- a/scripts/autogen +++ b/scripts/autogen @@ -103,6 +103,8 @@ def gen_c_zetas(): def gen_c_zeta_file(dry_run=False): def gen(): yield from gen_header() + yield '#include "common.h"' + yield "#if !defined(MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED)" yield '#include "ntt.h"' yield "" yield "/*" @@ -113,6 +115,13 @@ def gen_c_zeta_file(dry_run=False): yield from map(lambda t: str(t) + ",", gen_c_zetas()) yield "};" yield "" + yield "#else /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */" + yield "" + yield "#define empty_cu_zetas MLKEM_NAMESPACE_K(empty_cu_zetas)" + yield "int empty_cu_zetas;" + yield "" + yield "#endif /* MLKEM_NATIVE_MULTILEVEL_BUILD_NO_SHARED */" + yield "" update_file("mlkem/zetas.c", "\n".join(gen()), dry_run=dry_run) @@ -624,14 +633,32 @@ def gen_monolithic_undef_all_core(filt=None): def gen_monolithic_source_file(dry_run=False): - def fips202(c): - return "fips202/" in c + def not_native(c): + return "native/" not in c + + # List of level-specific source files + # All other files only need including and building once + # in multilevel build. + def k_specific(c): + # For now, we exclude native files from the monobuild + if not_native(c) is False: + return 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" ] + for f in k_specific_sources: + if c.endswith(f): + return True + return False - def randombytes(c): - return "randombytes.h" in c + def k_generic(c): + # For now, we exclude native files from the monobuild + if not_native(c) is False: + return False - def shared(c): - return randombytes(c) or fips202(c) + return not k_specific(c) def gen(): yield from gen_header() @@ -639,18 +666,13 @@ def gen_monolithic_source_file(dry_run=False): yield " * Monolithic compilation unit bundling all compilation units within mlkem-native" yield " */" yield "" - for c in filter(lambda c: not fips202(c), get_c_source_files()): - yield f'#include "{c}"' - yield "" - yield "#if !defined(MLKEM_NATIVE_MONOBUILD_NO_FIPS202_SOURCES)" - for c in filter(fips202, get_c_source_files()): + for c in filter(not_native, get_c_source_files()): yield f'#include "{c}"' - yield "#endif /* MLKEM_NATIVE_MONOBUILD_NO_FIPS202_SOURCES */" yield "" - yield from gen_monolithic_undef_all_core(filt=lambda c: not shared(c)) + yield from gen_monolithic_undef_all_core(filt=k_specific) yield "" yield "#if !defined(MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS)" - yield from gen_monolithic_undef_all_core(filt=shared) + yield from gen_monolithic_undef_all_core(filt=k_generic) yield "#endif /* MLKEM_NATIVE_MONOBUILD_KEEP_SHARED_HEADERS */" yield "" diff --git a/scripts/tests b/scripts/tests index 084b2fd57..9da4c8a3c 100755 --- a/scripts/tests +++ b/scripts/tests @@ -188,6 +188,7 @@ class TEST_TYPES(Enum): MLKEM_NATIVE_AS_CODE_PACKAGE = 9 MONOLITHIC_BUILD = 10 MONOLITHIC_BUILD_MULTILEVEL = 11 + MULTILEVEL_BUILD = 12 def is_benchmark(self): return self in [TEST_TYPES.BENCH, TEST_TYPES.BENCH_COMPONENTS] @@ -203,6 +204,7 @@ class TEST_TYPES(Enum): TEST_TYPES.MLKEM_NATIVE_AS_CODE_PACKAGE, TEST_TYPES.MONOLITHIC_BUILD, TEST_TYPES.MONOLITHIC_BUILD_MULTILEVEL, + TEST_TYPES.MULTILEVEL_BUILD, ] @staticmethod @@ -237,6 +239,8 @@ class TEST_TYPES(Enum): return "Example (monolithic build)" if self == TEST_TYPES.MONOLITHIC_BUILD_MULTILEVEL: return "Example (monolithic build, multilevel)" + if self == TEST_TYPES.MULTILEVEL_BUILD: + return "Example (multilevel build)" def make_dir(self): if self == TEST_TYPES.BRING_YOUR_OWN_FIPS202: @@ -249,6 +253,8 @@ class TEST_TYPES(Enum): return "examples/monolithic_build" if self == TEST_TYPES.MONOLITHIC_BUILD_MULTILEVEL: return "examples/monolithic_build_multilevel" + if self == TEST_TYPES.MULTILEVEL_BUILD: + return "examples/multilevel_build" return "" def make_target(self): @@ -274,6 +280,8 @@ class TEST_TYPES(Enum): return "" if self == TEST_TYPES.MONOLITHIC_BUILD_MULTILEVEL: return "" + if self == TEST_TYPES.MULTILEVEL_BUILD: + return "" def make_run_target(self, scheme): t = self.make_target()