From cb6b7a811742f83961fa7df57716497c5c63efd4 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 20 Jan 2025 16:44:58 +0000 Subject: [PATCH] Remove FIPS202_NAMESPACE_PREFIX configuration option Previously, the namespace for FIPS202 symbols could be separately defined from the namespace for MLKEM-specific symbols. This was primarily to allow for a multi-level build where FIPS202 code is shared. Now that multi-level builds are possible even with sharing of all level-independent code (not merely FIPS202), there is no longer a use of a separate FIPS202 namespace. Note also that when a custom FIPS202 implementation is used, the user is in full control of namespacing since they are expected to replace the FIPS202 headers. In light of the above, this commit merges the FIPS202_NAMESPACE_PREFIX configuration option into MLKEM_NAMESPACE_PREFIX. The latter now controls prefixing of _all_ global symbols in an mlkem-native build. If users want to share common code in a multilevel build, this should be done by setting MLKEM_NAMESPACE_PREFIX_ADD_LEVEL, and dropping the level from the MLKEM_NAMESPACE_PREFIX; all this is already demonstrated in the example `example/multilevel_build`. It is therefore no longer necessary to demonstrate a shared-FIPS202 build in the `Makefile`, which was done so far. Instead, the default build can be simplified to three independent builds of libmlkem{512,768,1024}, each with their own FIPS202. Again, usage examples are now provided in `examples/*`, while the user should not need to inspect the test Makefiles. Signed-off-by: Hanno Becker --- Makefile | 2 +- .../bring_your_own_fips202/fips202/fips202.h | 12 +- .../fips202/fips202x4.h | 8 +- .../mlkem_native/custom_config.h | 8 -- examples/monolithic_build/config_512.h | 11 -- .../monolithic_build/mlkem_native_monobuild.c | 20 ---- .../monolithic_build_multilevel/config_1024.h | 11 -- .../monolithic_build_multilevel/config_512.h | 11 -- .../monolithic_build_multilevel/config_768.h | 11 -- mlkem/common.h | 5 - mlkem/config.h | 37 ++---- mlkem/fips202/fips202.c | 8 +- mlkem/fips202/fips202.h | 14 +-- mlkem/fips202/fips202x4.c | 10 +- mlkem/fips202/fips202x4.h | 10 +- mlkem/fips202/keccakf1600.c | 2 +- mlkem/fips202/keccakf1600.h | 15 ++- .../aarch64/src/fips202_native_aarch64.h | 17 ++- .../src/keccak_f1600_x1_scalar_asm_opt.S | 4 +- .../src/keccak_f1600_x1_v84a_asm_clean.S | 4 +- .../src/keccak_f1600_x2_v84a_asm_clean.S | 4 +- .../src/keccak_f1600_x2_v8a_v84a_asm_hybrid.S | 4 +- ...ccak_f1600_x4_scalar_v84a_asm_hybrid_opt.S | 4 +- ...eccak_f1600_x4_v8a_scalar_hybrid_asm_opt.S | 4 +- ..._f1600_x4_v8a_v84a_scalar_hybrid_asm_opt.S | 4 +- .../x86_64/src/KeccakP-1600-times4-SIMD256.c | 2 +- mlkem/fips202/native/x86_64/src/xkcp_impl.h | 2 +- .../KeccakF1600_StateExtractBytes/Makefile | 4 +- .../KeccakF1600_StateExtractBytes_BE/Makefile | 4 +- proofs/cbmc/KeccakF1600_StatePermute/Makefile | 4 +- .../cbmc/KeccakF1600_StateXORBytes/Makefile | 4 +- .../KeccakF1600_StateXORBytes_BE/Makefile | 4 +- .../KeccakF1600x4_StateExtractBytes/Makefile | 6 +- .../cbmc/KeccakF1600x4_StatePermute/Makefile | 6 +- .../cbmc/KeccakF1600x4_StateXORBytes/Makefile | 6 +- proofs/cbmc/crypto_kem_dec/Makefile | 2 +- proofs/cbmc/crypto_kem_enc_derand/Makefile | 2 +- .../cbmc/crypto_kem_keypair_derand/Makefile | 2 +- proofs/cbmc/indcpa_keypair_derand/Makefile | 2 +- proofs/cbmc/keccak_absorb_once/Makefile | 4 +- .../keccak_absorb_once_harness.c | 2 +- proofs/cbmc/keccak_absorb_once_x4/Makefile | 4 +- .../keccak_absorb_once_x4_harness.c | 2 +- proofs/cbmc/keccak_squeeze_once/Makefile | 4 +- .../keccak_squeeze_once_harness.c | 2 +- proofs/cbmc/keccak_squeezeblocks/Makefile | 4 +- .../keccak_squeezeblocks_harness.c | 2 +- proofs/cbmc/keccak_squeezeblocks_x4/Makefile | 4 +- .../keccak_squeezeblocks_x4_harness.c | 2 +- proofs/cbmc/keccakf1600_extractbytes/Makefile | 4 +- proofs/cbmc/keccakf1600_permute/Makefile | 4 +- proofs/cbmc/keccakf1600_xorbytes/Makefile | 4 +- proofs/cbmc/poly_getnoise_eta1122_4x/Makefile | 2 +- proofs/cbmc/poly_getnoise_eta1_4x/Makefile | 2 +- proofs/cbmc/poly_getnoise_eta2/Makefile | 4 +- proofs/cbmc/poly_rej_uniform/Makefile | 2 +- proofs/cbmc/poly_rej_uniform_x4/Makefile | 2 +- proofs/cbmc/sha3_256/Makefile | 6 +- proofs/cbmc/sha3_512/Makefile | 6 +- proofs/cbmc/shake128_absorb_once/Makefile | 6 +- proofs/cbmc/shake128_squeezeblocks/Makefile | 6 +- proofs/cbmc/shake128x4_absorb_once/Makefile | 6 +- proofs/cbmc/shake128x4_squeezeblocks/Makefile | 6 +- proofs/cbmc/shake256/Makefile | 6 +- proofs/cbmc/shake256x4/Makefile | 6 +- scripts/check-namespace | 21 +--- test/mk/components.mk | 44 +++---- test/mk/config.mk~ | 111 ------------------ test/mk/rules.mk | 19 +-- 69 files changed, 171 insertions(+), 416 deletions(-) delete mode 100644 test/mk/config.mk~ diff --git a/Makefile b/Makefile index cd4db99df..aea2fd637 100644 --- a/Makefile +++ b/Makefile @@ -91,7 +91,7 @@ acvp_1024: $(MLKEM1024_DIR)/bin/acvp_mlkem1024 $(Q)echo " ACVP ML-MEM-1024: $^" acvp: acvp_512 acvp_768 acvp_1024 -lib: $(BUILD_DIR)/libmlkem.a +lib: $(BUILD_DIR)/libmlkem.a $(BUILD_DIR)/libmlkem512.a $(BUILD_DIR)/libmlkem768.a $(BUILD_DIR)/libmlkem1024.a # Enforce setting CYCLES make variable when # building benchmarking binaries diff --git a/examples/bring_your_own_fips202/fips202/fips202.h b/examples/bring_your_own_fips202/fips202/fips202.h index 4966a0fad..376ccee65 100644 --- a/examples/bring_your_own_fips202/fips202/fips202.h +++ b/examples/bring_your_own_fips202/fips202/fips202.h @@ -29,7 +29,7 @@ typedef sha3_ctx_t shake128ctx; * This function does not support being called multiple times * with the same state. */ -#define shake128_absorb_once FIPS202_NAMESPACE(shake128_absorb_once) +#define shake128_absorb_once MLKEM_NAMESPACE(shake128_absorb_once) /************************************************* * Name: shake128_absorb_once * @@ -56,7 +56,7 @@ static INLINE void shake128_absorb_once(shake128ctx *state, * * Supports being called multiple times */ -#define shake128_squeezeblocks FIPS202_NAMESPACE(shake128_squeezeblocks) +#define shake128_squeezeblocks MLKEM_NAMESPACE(shake128_squeezeblocks) /************************************************* * Name: shake128_squeezeblocks * @@ -76,12 +76,12 @@ static INLINE void shake128_squeezeblocks(uint8_t *output, size_t nblocks, } /* Free the state */ -#define shake128_release FIPS202_NAMESPACE(shake128_release) +#define shake128_release MLKEM_NAMESPACE(shake128_release) static INLINE void shake128_release(shake128ctx *state) { ((void)state); } /* One-stop SHAKE256 call. Aliasing between input and * output is not permitted */ -#define shake256 FIPS202_NAMESPACE(shake256) +#define shake256 MLKEM_NAMESPACE(shake256) /************************************************* * Name: shake256 * @@ -105,7 +105,7 @@ static INLINE void shake256(uint8_t *output, size_t outlen, /* One-stop SHA3_256 call. Aliasing between input and * output is not permitted */ #define SHA3_256_HASHBYTES 32 -#define sha3_256 FIPS202_NAMESPACE(sha3_256) +#define sha3_256 MLKEM_NAMESPACE(sha3_256) /************************************************* * Name: sha3_256 * @@ -123,7 +123,7 @@ static INLINE void sha3_256(uint8_t *output, const uint8_t *input, size_t inlen) /* One-stop SHA3_512 call. Aliasing between input and * output is not permitted */ #define SHA3_512_HASHBYTES 64 -#define sha3_512 FIPS202_NAMESPACE(sha3_512) +#define sha3_512 MLKEM_NAMESPACE(sha3_512) /************************************************* * Name: sha3_512 * diff --git a/examples/bring_your_own_fips202/fips202/fips202x4.h b/examples/bring_your_own_fips202/fips202/fips202x4.h index 7b2051a2f..d71716d87 100644 --- a/examples/bring_your_own_fips202/fips202/fips202x4.h +++ b/examples/bring_your_own_fips202/fips202/fips202x4.h @@ -21,7 +21,7 @@ typedef shake128ctx shake128x4ctx[4]; -#define shake128x4_absorb_once FIPS202_NAMESPACE(shake128x4_absorb_once) +#define shake128x4_absorb_once MLKEM_NAMESPACE(shake128x4_absorb_once) static INLINE void shake128x4_absorb_once(shake128x4ctx *state, const uint8_t *in0, const uint8_t *in1, @@ -42,7 +42,7 @@ __contract__( shake128_absorb_once(&(*state)[3], in3, inlen); } -#define shake128x4_squeezeblocks FIPS202_NAMESPACE(shake128x4_squeezeblocks) +#define shake128x4_squeezeblocks MLKEM_NAMESPACE(shake128x4_squeezeblocks) static INLINE void shake128x4_squeezeblocks(uint8_t *out0, uint8_t *out1, uint8_t *out2, uint8_t *out3, size_t nblocks, @@ -66,7 +66,7 @@ __contract__( shake128_squeezeblocks(out3, nblocks, &(*state)[3]); } -#define shake128x4_release FIPS202_NAMESPACE(shake128x4_release) +#define shake128x4_release MLKEM_NAMESPACE(shake128x4_release) static INLINE void shake128x4_release(shake128x4ctx *state) { shake128_release(&(*state)[0]); @@ -75,7 +75,7 @@ static INLINE void shake128x4_release(shake128x4ctx *state) shake128_release(&(*state)[3]); } -#define shake256x4 FIPS202_NAMESPACE(shake256x4) +#define shake256x4 MLKEM_NAMESPACE(shake256x4) static INLINE void shake256x4(uint8_t *out0, uint8_t *out1, uint8_t *out2, uint8_t *out3, size_t outlen, uint8_t *in0, uint8_t *in1, uint8_t *in2, uint8_t *in3, diff --git a/examples/custom_backend/mlkem_native/custom_config.h b/examples/custom_backend/mlkem_native/custom_config.h index 446cf1e38..910008c74 100644 --- a/examples/custom_backend/mlkem_native/custom_config.h +++ b/examples/custom_backend/mlkem_native/custom_config.h @@ -41,14 +41,6 @@ *****************************************************************************/ #define MLKEM_NAMESPACE_PREFIX CUSTOM_TINY_SHA3 -/****************************************************************************** - * Name: FIPS202_NAMESPACE_PREFIX - * - * Description: The prefix to use to namespace global symbols - * from mlkem/fips202/. - *****************************************************************************/ -#define FIPS202_NAMESPACE_PREFIX CUSTOM_TINY_SHA3 - /****************************************************************************** * Name: MLKEM_USE_NATIVE * diff --git a/examples/monolithic_build/config_512.h b/examples/monolithic_build/config_512.h index a7c7e2924..bdd5d1d56 100644 --- a/examples/monolithic_build/config_512.h +++ b/examples/monolithic_build/config_512.h @@ -48,17 +48,6 @@ *****************************************************************************/ #define MLKEM_NAMESPACE_PREFIX mlkem512 -/****************************************************************************** - * Name: FIPS202_NAMESPACE_PREFIX - * - * Description: The prefix to use to namespace global symbols - * from mlkem/fips202/. - * - * This can also be set using CFLAGS. - * - *****************************************************************************/ -#define FIPS202_NAMESPACE_PREFIX fips202 - /****************************************************************************** * Name: MLKEM_USE_NATIVE * diff --git a/examples/monolithic_build/mlkem_native_monobuild.c b/examples/monolithic_build/mlkem_native_monobuild.c index d10c9ddb2..67a851a91 100644 --- a/examples/monolithic_build/mlkem_native_monobuild.c +++ b/examples/monolithic_build/mlkem_native_monobuild.c @@ -32,16 +32,6 @@ * Undo all #define directives from *.c or *.h files */ -/* mlkem/common.h */ -#if defined(FIPS202_ASM_NAMESPACE) -#undef FIPS202_ASM_NAMESPACE -#endif - -/* mlkem/common.h */ -#if defined(FIPS202_NAMESPACE) -#undef FIPS202_NAMESPACE -#endif - /* mlkem/common.h */ #if defined(MLKEM_ASM_NAMESPACE) #undef MLKEM_ASM_NAMESPACE @@ -112,16 +102,6 @@ #undef PREFIX_UNDERSCORE_ #endif -/* mlkem/config.h */ -#if defined(FIPS202_DEFAULT_NAMESPACE_PREFIX) -#undef FIPS202_DEFAULT_NAMESPACE_PREFIX -#endif - -/* mlkem/config.h */ -#if defined(FIPS202_NAMESPACE_PREFIX) -#undef FIPS202_NAMESPACE_PREFIX -#endif - /* mlkem/config.h */ #if defined(MLKEM_DEFAULT_NAMESPACE_PREFIX) #undef MLKEM_DEFAULT_NAMESPACE_PREFIX diff --git a/examples/monolithic_build_multilevel/config_1024.h b/examples/monolithic_build_multilevel/config_1024.h index a8ac69c87..092eb94b8 100644 --- a/examples/monolithic_build_multilevel/config_1024.h +++ b/examples/monolithic_build_multilevel/config_1024.h @@ -49,17 +49,6 @@ #define MLKEM_NAMESPACE_PREFIX mlkem #define MLKEM_NAMESPACE_PREFIX_ADD_LEVEL -/****************************************************************************** - * Name: FIPS202_NAMESPACE_PREFIX - * - * Description: The prefix to use to namespace global symbols - * from mlkem/fips202/. - * - * This can also be set using CFLAGS. - * - *****************************************************************************/ -#define FIPS202_NAMESPACE_PREFIX fips202 - /****************************************************************************** * Name: MLKEM_USE_NATIVE * diff --git a/examples/monolithic_build_multilevel/config_512.h b/examples/monolithic_build_multilevel/config_512.h index 870569fe9..de6f77398 100644 --- a/examples/monolithic_build_multilevel/config_512.h +++ b/examples/monolithic_build_multilevel/config_512.h @@ -49,17 +49,6 @@ #define MLKEM_NAMESPACE_PREFIX mlkem #define MLKEM_NAMESPACE_PREFIX_ADD_LEVEL -/****************************************************************************** - * Name: FIPS202_NAMESPACE_PREFIX - * - * Description: The prefix to use to namespace global symbols - * from mlkem/fips202/. - * - * This can also be set using CFLAGS. - * - *****************************************************************************/ -#define FIPS202_NAMESPACE_PREFIX fips202 - /****************************************************************************** * Name: MLKEM_USE_NATIVE * diff --git a/examples/monolithic_build_multilevel/config_768.h b/examples/monolithic_build_multilevel/config_768.h index 244d3af1e..d27e6d0c6 100644 --- a/examples/monolithic_build_multilevel/config_768.h +++ b/examples/monolithic_build_multilevel/config_768.h @@ -49,17 +49,6 @@ #define MLKEM_NAMESPACE_PREFIX mlkem #define MLKEM_NAMESPACE_PREFIX_ADD_LEVEL -/****************************************************************************** - * Name: FIPS202_NAMESPACE_PREFIX - * - * Description: The prefix to use to namespace global symbols - * from mlkem/fips202/. - * - * This can also be set using CFLAGS. - * - *****************************************************************************/ -#define FIPS202_NAMESPACE_PREFIX fips202 - /****************************************************************************** * Name: MLKEM_USE_NATIVE * diff --git a/mlkem/common.h b/mlkem/common.h index 4ffe0a74f..4f326333e 100644 --- a/mlkem/common.h +++ b/mlkem/common.h @@ -43,9 +43,6 @@ #define MLKEM_NATIVE_MAKE_NAMESPACE_(x1, x2) x1##_##x2 #define MLKEM_NATIVE_MAKE_NAMESPACE(x1, x2) MLKEM_NATIVE_MAKE_NAMESPACE_(x1, x2) -#define FIPS202_NAMESPACE(s) \ - MLKEM_NATIVE_MAKE_NAMESPACE(FIPS202_NAMESPACE_PREFIX, s) - #define MLKEM_NAMESPACE(s) \ MLKEM_NATIVE_MAKE_NAMESPACE(MLKEM_NAMESPACE_PREFIX, s) @@ -65,13 +62,11 @@ #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 #endif /* MLKEM_NATIVE_COMMON_H */ diff --git a/mlkem/config.h b/mlkem/config.h index f09416428..24a49709c 100644 --- a/mlkem/config.h +++ b/mlkem/config.h @@ -42,8 +42,10 @@ /****************************************************************************** * Name: MLKEM_NAMESPACE_PREFIX * - * Description: The prefix to use to namespace global symbols - * from mlkem/. + * Description: The prefix to use to namespace global symbols from mlkem/. + * + * Level-dependent symbols will additionally be prefixed with the + * security level if MLKEM_NAMESPACE_PREFIX_ADD_LEVEL is set. * * This can also be set using CFLAGS. * @@ -68,19 +70,6 @@ *****************************************************************************/ /* #define MLKEM_NAMESPACE_PREFIX_ADD_LEVEL */ -/****************************************************************************** - * Name: FIPS202_NAMESPACE_PREFIX - * - * Description: The prefix to use to namespace global symbols - * from mlkem/fips202/. - * - * This can also be set using CFLAGS. - * - *****************************************************************************/ -#if !defined(FIPS202_NAMESPACE_PREFIX) -#define FIPS202_NAMESPACE_PREFIX FIPS202_DEFAULT_NAMESPACE_PREFIX -#endif - /****************************************************************************** * Name: MLKEM_NATIVE_MULTILEVEL_BUILD_WITH_SHARED * @@ -179,25 +168,13 @@ /* Default namespace * * Don't change this. If you need a different namespace, re-define - * MLKEM_NAMESPACE above instead, and remove the following. - */ - -/* - * The default FIPS202 namespace is - * - * PQCP_MLKEM_NATIVE_FIPS202__ + * MLKEM_NAMESPACE_PREFIX above instead, and remove the following. * - * e.g., PQCP_MLKEM_NATIVE_FIPS202_C_ - */ - -#define FIPS202_DEFAULT_NAMESPACE_PREFIX PQCP_MLKEM_NATIVE_FIPS202 - -/* * The default MLKEM namespace is * - * PQCP_MLKEM_NATIVE_MLKEM__ + * PQCP_MLKEM_NATIVE_MLKEM_ * - * e.g., PQCP_MLKEM_NATIVE_MLKEM512_AARCH64_OPT_ + * e.g., PQCP_MLKEM_NATIVE_MLKEM512_ */ #if MLKEM_K == 2 diff --git a/mlkem/fips202/fips202.c b/mlkem/fips202/fips202.c index 03d3c8cc6..4ed8915d5 100644 --- a/mlkem/fips202/fips202.c +++ b/mlkem/fips202/fips202.c @@ -24,9 +24,9 @@ * This is to facilitate building multiple instances * of mlkem-native (e.g. with varying security levels) * within a single compilation unit. */ -#define keccak_absorb_once FIPS202_NAMESPACE(keccak_absorb_once) -#define keccak_squeeze_once FIPS202_NAMESPACE(keccak_squeeze_once) -#define keccak_squeezeblocks FIPS202_NAMESPACE(keccak_squeezeblocks) +#define keccak_absorb_once MLKEM_NAMESPACE(keccak_absorb_once) +#define keccak_squeeze_once MLKEM_NAMESPACE(keccak_squeeze_once) +#define keccak_squeezeblocks MLKEM_NAMESPACE(keccak_squeezeblocks) /* End of static namespacing */ /************************************************* @@ -185,7 +185,7 @@ void shake128_squeezeblocks(uint8_t *output, size_t nblocks, shake128ctx *state) void shake128_release(shake128ctx *state) { (void)state; } -#define shake256ctx FIPS202_NAMESPACE(shake256ctx) +#define shake256ctx MLKEM_NAMESPACE(shake256ctx) typedef shake128ctx shake256ctx; void shake256(uint8_t *output, size_t outlen, const uint8_t *input, size_t inlen) diff --git a/mlkem/fips202/fips202.h b/mlkem/fips202/fips202.h index 953bc9664..d5179fc6c 100644 --- a/mlkem/fips202/fips202.h +++ b/mlkem/fips202/fips202.h @@ -17,7 +17,7 @@ /* Context for non-incremental API */ -#define shake128ctx FIPS202_NAMESPACE(shake128ctx) +#define shake128ctx MLKEM_NAMESPACE(shake128ctx) typedef struct { uint64_t ctx[25]; @@ -28,7 +28,7 @@ typedef struct * This function does not support being called multiple times * with the same state. */ -#define shake128_absorb_once FIPS202_NAMESPACE(shake128_absorb_once) +#define shake128_absorb_once MLKEM_NAMESPACE(shake128_absorb_once) /************************************************* * Name: shake128_absorb_once * @@ -55,7 +55,7 @@ __contract__( * * Supports being called multiple times */ -#define shake128_squeezeblocks FIPS202_NAMESPACE(shake128_squeezeblocks) +#define shake128_squeezeblocks MLKEM_NAMESPACE(shake128_squeezeblocks) /************************************************* * Name: shake128_squeezeblocks * @@ -77,12 +77,12 @@ __contract__( ); /* Free the state */ -#define shake128_release FIPS202_NAMESPACE(shake128_release) +#define shake128_release MLKEM_NAMESPACE(shake128_release) void shake128_release(shake128ctx *state); /* One-stop SHAKE256 call. Aliasing between input and * output is not permitted */ -#define shake256 FIPS202_NAMESPACE(shake256) +#define shake256 MLKEM_NAMESPACE(shake256) /************************************************* * Name: shake256 * @@ -104,7 +104,7 @@ __contract__( /* One-stop SHA3_256 call. Aliasing between input and * output is not permitted */ #define SHA3_256_HASHBYTES 32 -#define sha3_256 FIPS202_NAMESPACE(sha3_256) +#define sha3_256 MLKEM_NAMESPACE(sha3_256) /************************************************* * Name: sha3_256 * @@ -124,7 +124,7 @@ __contract__( /* One-stop SHA3_512 call. Aliasing between input and * output is not permitted */ #define SHA3_512_HASHBYTES 64 -#define sha3_512 FIPS202_NAMESPACE(sha3_512) +#define sha3_512 MLKEM_NAMESPACE(sha3_512) /************************************************* * Name: sha3_512 * diff --git a/mlkem/fips202/fips202x4.c b/mlkem/fips202/fips202x4.c index bce629e62..9dfbcf1fe 100644 --- a/mlkem/fips202/fips202x4.c +++ b/mlkem/fips202/fips202x4.c @@ -10,17 +10,17 @@ #include "fips202x4.h" #include "keccakf1600.h" -#define shake256x4_ctx FIPS202_NAMESPACE(shake256x4_ctx) +#define shake256x4_ctx MLKEM_NAMESPACE(shake256x4_ctx) typedef shake128x4ctx shake256x4_ctx; /* Static namespacing * This is to facilitate building multiple instances * of mlkem-native (e.g. with varying security levels) * within a single compilation unit. */ -#define keccak_absorb_once_x4 FIPS202_NAMESPACE(keccak_absorb_once_x4) -#define keccak_squeezeblocks_x4 FIPS202_NAMESPACE(keccak_squeezeblocks_x4) -#define shake256x4_absorb_once FIPS202_NAMESPACE(shake256x4_absorb_once) -#define shake256x4_squeezeblocks FIPS202_NAMESPACE(shake256x4_squeezeblocks) +#define keccak_absorb_once_x4 MLKEM_NAMESPACE(keccak_absorb_once_x4) +#define keccak_squeezeblocks_x4 MLKEM_NAMESPACE(keccak_squeezeblocks_x4) +#define shake256x4_absorb_once MLKEM_NAMESPACE(shake256x4_absorb_once) +#define shake256x4_squeezeblocks MLKEM_NAMESPACE(shake256x4_squeezeblocks) /* End of static namespacing */ static void keccak_absorb_once_x4(uint64_t *s, uint32_t r, const uint8_t *in0, diff --git a/mlkem/fips202/fips202x4.h b/mlkem/fips202/fips202x4.h index 8a6cf7cfb..da9ea40c7 100644 --- a/mlkem/fips202/fips202x4.h +++ b/mlkem/fips202/fips202x4.h @@ -15,13 +15,13 @@ #include "keccakf1600.h" /* Context for non-incremental API */ -#define shake128x4ctx FIPS202_NAMESPACE(shake128x4ctx) +#define shake128x4ctx MLKEM_NAMESPACE(shake128x4ctx) typedef struct { uint64_t ctx[KECCAK_LANES * KECCAK_WAY]; } shake128x4ctx; -#define shake128x4_absorb_once FIPS202_NAMESPACE(shake128x4_absorb_once) +#define shake128x4_absorb_once MLKEM_NAMESPACE(shake128x4_absorb_once) void shake128x4_absorb_once(shake128x4ctx *state, const uint8_t *in0, const uint8_t *in1, const uint8_t *in2, const uint8_t *in3, size_t inlen) @@ -34,7 +34,7 @@ __contract__( assigns(object_whole(state)) ); -#define shake128x4_squeezeblocks FIPS202_NAMESPACE(shake128x4_squeezeblocks) +#define shake128x4_squeezeblocks MLKEM_NAMESPACE(shake128x4_squeezeblocks) void shake128x4_squeezeblocks(uint8_t *out0, uint8_t *out1, uint8_t *out2, uint8_t *out3, size_t nblocks, shake128x4ctx *state) @@ -52,10 +52,10 @@ __contract__( object_whole(state)) ); -#define shake128x4_release FIPS202_NAMESPACE(shake128x4_release) +#define shake128x4_release MLKEM_NAMESPACE(shake128x4_release) void shake128x4_release(shake128x4ctx *state); -#define shake256x4 FIPS202_NAMESPACE(shake256x4) +#define shake256x4 MLKEM_NAMESPACE(shake256x4) void shake256x4(uint8_t *out0, uint8_t *out1, uint8_t *out2, uint8_t *out3, size_t outlen, uint8_t *in0, uint8_t *in1, uint8_t *in2, uint8_t *in3, size_t inlen) diff --git a/mlkem/fips202/keccakf1600.c b/mlkem/fips202/keccakf1600.c index bd749b9af..dd87fb9a1 100644 --- a/mlkem/fips202/keccakf1600.c +++ b/mlkem/fips202/keccakf1600.c @@ -25,7 +25,7 @@ * This is to facilitate building multiple instances * of mlkem-native (e.g. with varying security levels) * within a single compilation unit. */ -#define KeccakF_RoundConstants FIPS202_NAMESPACE(KeccakF_RoundConstants) +#define KeccakF_RoundConstants MLKEM_NAMESPACE(KeccakF_RoundConstants) /* End of static namespacing */ void KeccakF1600_StateExtractBytes(uint64_t *state, unsigned char *data, diff --git a/mlkem/fips202/keccakf1600.h b/mlkem/fips202/keccakf1600.h index 2fae28cb9..6d22a6073 100644 --- a/mlkem/fips202/keccakf1600.h +++ b/mlkem/fips202/keccakf1600.h @@ -17,7 +17,7 @@ */ #define KeccakF1600_StateExtractBytes \ - FIPS202_NAMESPACE(KeccakF1600_StateExtractBytes) + MLKEM_NAMESPACE(KeccakF1600_StateExtractBytes) void KeccakF1600_StateExtractBytes(uint64_t *state, unsigned char *data, unsigned int offset, unsigned int length) __contract__( @@ -28,7 +28,7 @@ __contract__( assigns(memory_slice(data, length)) ); -#define KeccakF1600_StateXORBytes FIPS202_NAMESPACE(KeccakF1600_StateXORBytes) +#define KeccakF1600_StateXORBytes MLKEM_NAMESPACE(KeccakF1600_StateXORBytes) void KeccakF1600_StateXORBytes(uint64_t *state, const unsigned char *data, unsigned int offset, unsigned int length) __contract__( @@ -40,7 +40,7 @@ __contract__( ); #define KeccakF1600x4_StateExtractBytes \ - FIPS202_NAMESPACE(KeccakF1600x4_StateExtractBytes) + MLKEM_NAMESPACE(KeccakF1600x4_StateExtractBytes) void KeccakF1600x4_StateExtractBytes(uint64_t *state, unsigned char *data0, unsigned char *data1, unsigned char *data2, unsigned char *data3, unsigned int offset, @@ -59,8 +59,7 @@ __contract__( assigns(memory_slice(data3, length)) ); -#define KeccakF1600x4_StateXORBytes \ - FIPS202_NAMESPACE(KeccakF1600x4_StateXORBytes) +#define KeccakF1600x4_StateXORBytes MLKEM_NAMESPACE(KeccakF1600x4_StateXORBytes) void KeccakF1600x4_StateXORBytes(uint64_t *state, const unsigned char *data0, const unsigned char *data1, const unsigned char *data2, @@ -82,7 +81,7 @@ __contract__( ); -#define KeccakF1600x4_StatePermute FIPS202_NAMESPACE(KeccakF1600x4_StatePermute) +#define KeccakF1600x4_StatePermute MLKEM_NAMESPACE(KeccakF1600x4_StatePermute) void KeccakF1600x4_StatePermute(uint64_t *state) __contract__( requires(memory_no_alias(state, sizeof(uint64_t) * KECCAK_LANES * KECCAK_WAY)) @@ -91,7 +90,7 @@ __contract__( #if !defined(MLKEM_USE_FIPS202_X1_ASM) -#define KeccakF1600_StatePermute FIPS202_NAMESPACE(KeccakF1600_StatePermute) +#define KeccakF1600_StatePermute MLKEM_NAMESPACE(KeccakF1600_StatePermute) void KeccakF1600_StatePermute(uint64_t *state) __contract__( requires(memory_no_alias(state, sizeof(uint64_t) * KECCAK_LANES)) @@ -99,7 +98,7 @@ __contract__( ); #else -#define KeccakF1600_StatePermute FIPS202_NAMESPACE(keccak_f1600_x1_asm) +#define KeccakF1600_StatePermute MLKEM_NAMESPACE(keccak_f1600_x1_asm) #endif #endif /* KECCAKF1600_H */ diff --git a/mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h b/mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h index 71efbaba3..449c637a9 100644 --- a/mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h +++ b/mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h @@ -9,38 +9,37 @@ #include "../../../../common.h" #define keccak_f1600_x1_scalar_asm_opt \ - FIPS202_NAMESPACE(keccak_f1600_x1_scalar_asm_opt) + MLKEM_NAMESPACE(keccak_f1600_x1_scalar_asm_opt) void keccak_f1600_x1_scalar_asm_opt(uint64_t *state, uint64_t const *rc); #define keccak_f1600_x1_v84a_asm_clean \ - FIPS202_NAMESPACE(keccak_f1600_x1_v84a_asm_clean) + MLKEM_NAMESPACE(keccak_f1600_x1_v84a_asm_clean) void keccak_f1600_x1_v84a_asm_clean(uint64_t *state, uint64_t const *rc); #define keccak_f1600_x2_v84a_asm_clean \ - FIPS202_NAMESPACE(keccak_f1600_x2_v84a_asm_clean) + MLKEM_NAMESPACE(keccak_f1600_x2_v84a_asm_clean) void keccak_f1600_x2_v84a_asm_clean(uint64_t *state, uint64_t const *rc); #define keccak_f1600_x2_v8a_v84a_asm_hybrid \ - FIPS202_NAMESPACE(keccak_f1600_x2_v8a_v84a_asm_hybrid) + MLKEM_NAMESPACE(keccak_f1600_x2_v8a_v84a_asm_hybrid) void keccak_f1600_x2_v8a_v84a_asm_hybrid(uint64_t *state, uint64_t const *rc); #define keccak_f1600_x4_scalar_v8a_asm_hybrid_opt \ - FIPS202_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid_opt) + MLKEM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid_opt) void keccak_f1600_x4_scalar_v8a_asm_hybrid_opt(uint64_t *state, uint64_t const *rc); #define keccak_f1600_x4_scalar_v84a_asm_hybrid_opt \ - FIPS202_NAMESPACE(keccak_f1600_x4_scalar_v84a_asm_hybrid_opt) + MLKEM_NAMESPACE(keccak_f1600_x4_scalar_v84a_asm_hybrid_opt) void keccak_f1600_x4_scalar_v84a_asm_hybrid_opt(uint64_t *state, uint64_t const *rc); #define keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt \ - FIPS202_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt) + MLKEM_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt) void keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt(uint64_t *state, uint64_t const *rc); -#define keccakf1600_round_constants \ - FIPS202_NAMESPACE(keccakf1600_round_constants) +#define keccakf1600_round_constants MLKEM_NAMESPACE(keccakf1600_round_constants) extern const uint64_t keccakf1600_round_constants[]; #endif /* FIPS202_AARCH64_NATIVE_H */ diff --git a/mlkem/fips202/native/aarch64/src/keccak_f1600_x1_scalar_asm_opt.S b/mlkem/fips202/native/aarch64/src/keccak_f1600_x1_scalar_asm_opt.S index 1487355cc..1c73ef734 100644 --- a/mlkem/fips202/native/aarch64/src/keccak_f1600_x1_scalar_asm_opt.S +++ b/mlkem/fips202/native/aarch64/src/keccak_f1600_x1_scalar_asm_opt.S @@ -164,9 +164,9 @@ .text .balign 16 -.global FIPS202_ASM_NAMESPACE(keccak_f1600_x1_scalar_asm_opt) +.global MLKEM_ASM_NAMESPACE(keccak_f1600_x1_scalar_asm_opt) -FIPS202_ASM_NAMESPACE(keccak_f1600_x1_scalar_asm_opt): +MLKEM_ASM_NAMESPACE(keccak_f1600_x1_scalar_asm_opt): alloc_stack save_gprs diff --git a/mlkem/fips202/native/aarch64/src/keccak_f1600_x1_v84a_asm_clean.S b/mlkem/fips202/native/aarch64/src/keccak_f1600_x1_v84a_asm_clean.S index 6858f1c60..3ae44231e 100644 --- a/mlkem/fips202/native/aarch64/src/keccak_f1600_x1_v84a_asm_clean.S +++ b/mlkem/fips202/native/aarch64/src/keccak_f1600_x1_v84a_asm_clean.S @@ -310,9 +310,9 @@ .text .align 4 -.global FIPS202_ASM_NAMESPACE(keccak_f1600_x1_v84a_asm_clean) +.global MLKEM_ASM_NAMESPACE(keccak_f1600_x1_v84a_asm_clean) -FIPS202_ASM_NAMESPACE(keccak_f1600_x1_v84a_asm_clean): +MLKEM_ASM_NAMESPACE(keccak_f1600_x1_v84a_asm_clean): alloc_stack save_vregs mov const_addr, input_rc diff --git a/mlkem/fips202/native/aarch64/src/keccak_f1600_x2_v84a_asm_clean.S b/mlkem/fips202/native/aarch64/src/keccak_f1600_x2_v84a_asm_clean.S index 56da76638..ac57e24d8 100644 --- a/mlkem/fips202/native/aarch64/src/keccak_f1600_x2_v84a_asm_clean.S +++ b/mlkem/fips202/native/aarch64/src/keccak_f1600_x2_v84a_asm_clean.S @@ -338,9 +338,9 @@ .text .align 4 -.global FIPS202_ASM_NAMESPACE(keccak_f1600_x2_v84a_asm_clean) +.global MLKEM_ASM_NAMESPACE(keccak_f1600_x2_v84a_asm_clean) -FIPS202_ASM_NAMESPACE(keccak_f1600_x2_v84a_asm_clean): +MLKEM_ASM_NAMESPACE(keccak_f1600_x2_v84a_asm_clean): alloc_stack save_vregs mov const_addr, input_rc diff --git a/mlkem/fips202/native/aarch64/src/keccak_f1600_x2_v8a_v84a_asm_hybrid.S b/mlkem/fips202/native/aarch64/src/keccak_f1600_x2_v8a_v84a_asm_hybrid.S index 47ea61430..687ac0e9d 100644 --- a/mlkem/fips202/native/aarch64/src/keccak_f1600_x2_v8a_v84a_asm_hybrid.S +++ b/mlkem/fips202/native/aarch64/src/keccak_f1600_x2_v8a_v84a_asm_hybrid.S @@ -379,9 +379,9 @@ .text .align 4 -.global FIPS202_ASM_NAMESPACE(keccak_f1600_x2_v8a_v84a_asm_hybrid) +.global MLKEM_ASM_NAMESPACE(keccak_f1600_x2_v8a_v84a_asm_hybrid) -FIPS202_ASM_NAMESPACE(keccak_f1600_x2_v8a_v84a_asm_hybrid): +MLKEM_ASM_NAMESPACE(keccak_f1600_x2_v8a_v84a_asm_hybrid): alloc_stack save_gprs save_vregs diff --git a/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_scalar_v84a_asm_hybrid_opt.S b/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_scalar_v84a_asm_hybrid_opt.S index 487be5973..70fec9351 100644 --- a/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_scalar_v84a_asm_hybrid_opt.S +++ b/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_scalar_v84a_asm_hybrid_opt.S @@ -875,11 +875,11 @@ ror sAsu, sAsu,#(64-55) .endm -.global FIPS202_ASM_NAMESPACE(keccak_f1600_x4_scalar_v84a_asm_hybrid_opt) +.global MLKEM_ASM_NAMESPACE(keccak_f1600_x4_scalar_v84a_asm_hybrid_opt) .text .align 4 -FIPS202_ASM_NAMESPACE(keccak_f1600_x4_scalar_v84a_asm_hybrid_opt): +MLKEM_ASM_NAMESPACE(keccak_f1600_x4_scalar_v84a_asm_hybrid_opt): alloc_stack save_gprs save_vregs diff --git a/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm_opt.S b/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm_opt.S index 467c9cda8..2925da52a 100644 --- a/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm_opt.S +++ b/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm_opt.S @@ -857,11 +857,11 @@ ror sAsu, sAsu,#(64-55) .endm -.global FIPS202_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid_opt) +.global MLKEM_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid_opt) .text .align 4 -FIPS202_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid_opt): +MLKEM_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid_opt): alloc_stack save_gprs save_vregs diff --git a/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm_opt.S b/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm_opt.S index 329b62488..02f45e80c 100644 --- a/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm_opt.S +++ b/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm_opt.S @@ -875,11 +875,11 @@ ror sAsu, sAsu,#(64-55) .endm -.global FIPS202_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt) +.global MLKEM_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt) .text .align 4 -FIPS202_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt): +MLKEM_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm_opt): alloc_stack save_gprs save_vregs diff --git a/mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c b/mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c index bedd674ef..ef1095d81 100644 --- a/mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c +++ b/mlkem/fips202/native/x86_64/src/KeccakP-1600-times4-SIMD256.c @@ -456,7 +456,7 @@ void KeccakP1600times4_PermuteAll_24rounds(void *states) #else /* Dummy constant to keep compiler happy despite empty CU */ -#define empty_cu_avx2_keccakx4 FIPS202_NAMESPACE(empty_cu_avx2_keccakx4) +#define empty_cu_avx2_keccakx4 MLKEM_NAMESPACE(empty_cu_avx2_keccakx4) int empty_cu_avx2_keccakx4; #endif /* MLKEM_NATIVE_FIPS202_BACKEND_X86_64_XKCP */ diff --git a/mlkem/fips202/native/x86_64/src/xkcp_impl.h b/mlkem/fips202/native/x86_64/src/xkcp_impl.h index 40211a046..5a1d857ec 100644 --- a/mlkem/fips202/native/x86_64/src/xkcp_impl.h +++ b/mlkem/fips202/native/x86_64/src/xkcp_impl.h @@ -13,7 +13,7 @@ #include "../../../../common.h" #define KeccakP1600times4_PermuteAll_24rounds \ - FIPS202_NAMESPACE(KeccakP1600times4_PermuteAll_24rounds) + MLKEM_NAMESPACE(KeccakP1600times4_PermuteAll_24rounds) void KeccakP1600times4_PermuteAll_24rounds(void *states); #define MLKEM_USE_FIPS202_X4_NATIVE diff --git a/proofs/cbmc/KeccakF1600_StateExtractBytes/Makefile b/proofs/cbmc/KeccakF1600_StateExtractBytes/Makefile index 46fffcbbf..fbf09004c 100644 --- a/proofs/cbmc/KeccakF1600_StateExtractBytes/Makefile +++ b/proofs/cbmc/KeccakF1600_StateExtractBytes/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,7 +29,7 @@ CBMCFLAGS=--bitwuzla # CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes # 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/KeccakF1600_StateExtractBytes_BE/Makefile b/proofs/cbmc/KeccakF1600_StateExtractBytes_BE/Makefile index 7f10b666e..66e6af215 100644 --- a/proofs/cbmc/KeccakF1600_StateExtractBytes_BE/Makefile +++ b/proofs/cbmc/KeccakF1600_StateExtractBytes_BE/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla --big-endian DEFINES += -DSYS_BIG_ENDIAN=1 -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes # 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/KeccakF1600_StatePermute/Makefile b/proofs/cbmc/KeccakF1600_StatePermute/Makefile index 6d6182e91..935fc57a1 100644 --- a/proofs/cbmc/KeccakF1600_StatePermute/Makefile +++ b/proofs/cbmc/KeccakF1600_StatePermute/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StatePermute +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StatePermute USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -38,7 +38,7 @@ CBMCFLAGS=--smt2 # a substantial improvement in proof performance. CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600_StatePermute +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StatePermute # 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/KeccakF1600_StateXORBytes/Makefile b/proofs/cbmc/KeccakF1600_StateXORBytes/Makefile index 88f647349..7d28feb5c 100644 --- a/proofs/cbmc/KeccakF1600_StateXORBytes/Makefile +++ b/proofs/cbmc/KeccakF1600_StateXORBytes/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateXORBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateXORBytes USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600_StateXORBytes +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StateXORBytes # 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/KeccakF1600_StateXORBytes_BE/Makefile b/proofs/cbmc/KeccakF1600_StateXORBytes_BE/Makefile index 6708c7e91..44018898a 100644 --- a/proofs/cbmc/KeccakF1600_StateXORBytes_BE/Makefile +++ b/proofs/cbmc/KeccakF1600_StateXORBytes_BE/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateXORBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateXORBytes USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,7 +29,7 @@ CBMCFLAGS=--bitwuzla --big-endian DEFINES += -DSYS_BIG_ENDIAN -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600_StateXORBytes +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StateXORBytes # 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/KeccakF1600x4_StateExtractBytes/Makefile b/proofs/cbmc/KeccakF1600x4_StateExtractBytes/Makefile index af37ae346..70d556db6 100644 --- a/proofs/cbmc/KeccakF1600x4_StateExtractBytes/Makefile +++ b/proofs/cbmc/KeccakF1600x4_StateExtractBytes/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600x4_StateExtractBytes -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StateExtractBytes +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,7 +29,7 @@ CBMCFLAGS=--bitwuzla # CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600x4_StateExtractBytes +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600x4_StateExtractBytes # 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/KeccakF1600x4_StatePermute/Makefile b/proofs/cbmc/KeccakF1600x4_StatePermute/Makefile index ba587a4cd..2e73ec86f 100644 --- a/proofs/cbmc/KeccakF1600x4_StatePermute/Makefile +++ b/proofs/cbmc/KeccakF1600x4_StatePermute/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600x4_StatePermute -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StatePermute +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StatePermute +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StatePermute APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -38,7 +38,7 @@ CBMCFLAGS=--smt2 # a substantial improvement in proof performance. CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600x4_StatePermute +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600x4_StatePermute # 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/KeccakF1600x4_StateXORBytes/Makefile b/proofs/cbmc/KeccakF1600x4_StateXORBytes/Makefile index ce6e20869..6ee0f58b6 100644 --- a/proofs/cbmc/KeccakF1600x4_StateXORBytes/Makefile +++ b/proofs/cbmc/KeccakF1600x4_StateXORBytes/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600x4_StateXORBytes -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateXORBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StateXORBytes +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateXORBytes APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600x4_StateXORBytes +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600x4_StateXORBytes # 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/crypto_kem_dec/Makefile b/proofs/cbmc/crypto_kem_dec/Makefile index ec2e9227f..fea30ad7f 100644 --- a/proofs/cbmc/crypto_kem_dec/Makefile +++ b/proofs/cbmc/crypto_kem_dec/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)dec -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_512 $(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)indcpa_dec $(FIPS202_NAMESPACE)shake256 $(MLKEM_NAMESPACE)ct_memcmp $(MLKEM_NAMESPACE)ct_cmov_zero memcmp +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)sha3_512 $(MLKEM_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)indcpa_dec $(MLKEM_NAMESPACE)shake256 $(MLKEM_NAMESPACE)ct_memcmp $(MLKEM_NAMESPACE)ct_cmov_zero memcmp APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/crypto_kem_enc_derand/Makefile b/proofs/cbmc/crypto_kem_enc_derand/Makefile index 305955442..5e4e806cb 100644 --- a/proofs/cbmc/crypto_kem_enc_derand/Makefile +++ b/proofs/cbmc/crypto_kem_enc_derand/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)enc_derand -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_256 $(FIPS202_NAMESPACE)sha3_512 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)polyvec_frombytes $(MLKEM_NAMESPACE)polyvec_reduce $(MLKEM_NAMESPACE)polyvec_tobytes memcmp +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)sha3_512 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)polyvec_frombytes $(MLKEM_NAMESPACE)polyvec_reduce $(MLKEM_NAMESPACE)polyvec_tobytes memcmp APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/crypto_kem_keypair_derand/Makefile b/proofs/cbmc/crypto_kem_keypair_derand/Makefile index c89fc716f..0ad4ed72a 100644 --- a/proofs/cbmc/crypto_kem_keypair_derand/Makefile +++ b/proofs/cbmc/crypto_kem_keypair_derand/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keypair_derand -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_keypair_derand +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_keypair_derand APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/indcpa_keypair_derand/Makefile b/proofs/cbmc/indcpa_keypair_derand/Makefile index 57cdb4afb..6a3b28280 100644 --- a/proofs/cbmc/indcpa_keypair_derand/Makefile +++ b/proofs/cbmc/indcpa_keypair_derand/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)indcpa_keypair_derand -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_512 $(MLKEM_NAMESPACE)gen_matrix $(MLKEM_NAMESPACE)poly_getnoise_eta1_4x $(MLKEM_NAMESPACE)polyvec_ntt $(MLKEM_NAMESPACE)polyvec_mulcache_compute $(MLKEM_NAMESPACE)matvec_mul $(MLKEM_NAMESPACE)polyvec_tomont $(MLKEM_NAMESPACE)polyvec_add $(MLKEM_NAMESPACE)polyvec_reduce $(MLKEM_NAMESPACE)polyvec_tobytes +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)sha3_512 $(MLKEM_NAMESPACE)gen_matrix $(MLKEM_NAMESPACE)poly_getnoise_eta1_4x $(MLKEM_NAMESPACE)polyvec_ntt $(MLKEM_NAMESPACE)polyvec_mulcache_compute $(MLKEM_NAMESPACE)matvec_mul $(MLKEM_NAMESPACE)polyvec_tomont $(MLKEM_NAMESPACE)polyvec_add $(MLKEM_NAMESPACE)polyvec_reduce $(MLKEM_NAMESPACE)polyvec_tobytes APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/keccak_absorb_once/Makefile b/proofs/cbmc/keccak_absorb_once/Makefile index 3d51d8a0e..2cc389c63 100644 --- a/proofs/cbmc/keccak_absorb_once/Makefile +++ b/proofs/cbmc/keccak_absorb_once/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_absorb_once -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateXORBytes $(FIPS202_NAMESPACE)KeccakF1600_StatePermute +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_absorb_once +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateXORBytes $(MLKEM_NAMESPACE)KeccakF1600_StatePermute APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/keccak_absorb_once/keccak_absorb_once_harness.c b/proofs/cbmc/keccak_absorb_once/keccak_absorb_once_harness.c index 73dec832c..03e4b062b 100644 --- a/proofs/cbmc/keccak_absorb_once/keccak_absorb_once_harness.c +++ b/proofs/cbmc/keccak_absorb_once/keccak_absorb_once_harness.c @@ -7,7 +7,7 @@ #include #include -#define keccak_absorb_once FIPS202_NAMESPACE(keccak_absorb_once) +#define keccak_absorb_once MLKEM_NAMESPACE(keccak_absorb_once) void keccak_absorb_once(uint64_t *s, uint32_t r, const uint8_t *m, size_t mlen, uint8_t p); diff --git a/proofs/cbmc/keccak_absorb_once_x4/Makefile b/proofs/cbmc/keccak_absorb_once_x4/Makefile index e2009cc7a..eb5bd95ad 100644 --- a/proofs/cbmc/keccak_absorb_once_x4/Makefile +++ b/proofs/cbmc/keccak_absorb_once_x4/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_absorb_once_x4 -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600x4_StatePermute $(FIPS202_NAMESPACE)KeccakF1600x4_StateXORBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_absorb_once_x4 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StatePermute $(MLKEM_NAMESPACE)KeccakF1600x4_StateXORBytes APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/keccak_absorb_once_x4/keccak_absorb_once_x4_harness.c b/proofs/cbmc/keccak_absorb_once_x4/keccak_absorb_once_x4_harness.c index 88af9286b..7dafe5825 100644 --- a/proofs/cbmc/keccak_absorb_once_x4/keccak_absorb_once_x4_harness.c +++ b/proofs/cbmc/keccak_absorb_once_x4/keccak_absorb_once_x4_harness.c @@ -7,7 +7,7 @@ #include #include -#define keccak_absorb_once_x4 FIPS202_NAMESPACE(keccak_absorb_once_x4) +#define keccak_absorb_once_x4 MLKEM_NAMESPACE(keccak_absorb_once_x4) void keccak_absorb_once_x4(uint64_t *s, uint32_t r, const uint8_t *in0, const uint8_t *in1, const uint8_t *in2, const uint8_t *in3, size_t inlen, uint8_t p); diff --git a/proofs/cbmc/keccak_squeeze_once/Makefile b/proofs/cbmc/keccak_squeeze_once/Makefile index 1b7737ca9..3615162d5 100644 --- a/proofs/cbmc/keccak_squeeze_once/Makefile +++ b/proofs/cbmc/keccak_squeeze_once/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_squeeze_once -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes $(FIPS202_NAMESPACE)KeccakF1600_StatePermute +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_squeeze_once +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes $(MLKEM_NAMESPACE)KeccakF1600_StatePermute APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/keccak_squeeze_once/keccak_squeeze_once_harness.c b/proofs/cbmc/keccak_squeeze_once/keccak_squeeze_once_harness.c index 7d2c8715e..fb43557f6 100644 --- a/proofs/cbmc/keccak_squeeze_once/keccak_squeeze_once_harness.c +++ b/proofs/cbmc/keccak_squeeze_once/keccak_squeeze_once_harness.c @@ -7,7 +7,7 @@ #include #include -#define keccak_squeeze_once FIPS202_NAMESPACE(keccak_squeeze_once) +#define keccak_squeeze_once MLKEM_NAMESPACE(keccak_squeeze_once) void keccak_squeeze_once(uint8_t *h, size_t outlen, uint64_t *s, uint32_t r); void harness(void) diff --git a/proofs/cbmc/keccak_squeezeblocks/Makefile b/proofs/cbmc/keccak_squeezeblocks/Makefile index 41ac2d69b..9df75aefd 100644 --- a/proofs/cbmc/keccak_squeezeblocks/Makefile +++ b/proofs/cbmc/keccak_squeezeblocks/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_squeezeblocks -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes $(FIPS202_NAMESPACE)KeccakF1600_StatePermute +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_squeezeblocks +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes $(MLKEM_NAMESPACE)KeccakF1600_StatePermute APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/keccak_squeezeblocks/keccak_squeezeblocks_harness.c b/proofs/cbmc/keccak_squeezeblocks/keccak_squeezeblocks_harness.c index a818187eb..abb8802a3 100644 --- a/proofs/cbmc/keccak_squeezeblocks/keccak_squeezeblocks_harness.c +++ b/proofs/cbmc/keccak_squeezeblocks/keccak_squeezeblocks_harness.c @@ -7,7 +7,7 @@ #include #include -#define keccak_squeezeblocks FIPS202_NAMESPACE(keccak_squeezeblocks) +#define keccak_squeezeblocks MLKEM_NAMESPACE(keccak_squeezeblocks) void keccak_squeezeblocks(uint8_t *h, size_t nblocks, uint64_t *s, uint32_t r); void harness(void) diff --git a/proofs/cbmc/keccak_squeezeblocks_x4/Makefile b/proofs/cbmc/keccak_squeezeblocks_x4/Makefile index f7393a254..4e82e962f 100644 --- a/proofs/cbmc/keccak_squeezeblocks_x4/Makefile +++ b/proofs/cbmc/keccak_squeezeblocks_x4/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_squeezeblocks_x4 -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600x4_StateExtractBytes $(FIPS202_NAMESPACE)KeccakF1600x4_StatePermute +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_squeezeblocks_x4 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StateExtractBytes $(MLKEM_NAMESPACE)KeccakF1600x4_StatePermute APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/keccak_squeezeblocks_x4/keccak_squeezeblocks_x4_harness.c b/proofs/cbmc/keccak_squeezeblocks_x4/keccak_squeezeblocks_x4_harness.c index 549f1541d..ed89e8c66 100644 --- a/proofs/cbmc/keccak_squeezeblocks_x4/keccak_squeezeblocks_x4_harness.c +++ b/proofs/cbmc/keccak_squeezeblocks_x4/keccak_squeezeblocks_x4_harness.c @@ -7,7 +7,7 @@ #include #include -#define keccak_squeezeblocks_x4 FIPS202_NAMESPACE(keccak_squeezeblocks_x4) +#define keccak_squeezeblocks_x4 MLKEM_NAMESPACE(keccak_squeezeblocks_x4) void keccak_squeezeblocks_x4(uint8_t *out0, uint8_t *out1, uint8_t *out2, uint8_t *out3, size_t nblocks, uint64_t *s, uint32_t r); diff --git a/proofs/cbmc/keccakf1600_extractbytes/Makefile b/proofs/cbmc/keccakf1600_extractbytes/Makefile index c3b368b7d..d1fcffbc9 100644 --- a/proofs/cbmc/keccakf1600_extractbytes/Makefile +++ b/proofs/cbmc/keccakf1600_extractbytes/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,7 +29,7 @@ CBMCFLAGS=--bitwuzla # CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600_StateExtractBytes +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StateExtractBytes # 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/keccakf1600_permute/Makefile b/proofs/cbmc/keccakf1600_permute/Makefile index 234aa40df..8e9211cc0 100644 --- a/proofs/cbmc/keccakf1600_permute/Makefile +++ b/proofs/cbmc/keccakf1600_permute/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StatePermute +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StatePermute USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -38,7 +38,7 @@ CBMCFLAGS=--smt2 # a substantial improvement in proof performance. CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600_StatePermute +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StatePermute # 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/keccakf1600_xorbytes/Makefile b/proofs/cbmc/keccakf1600_xorbytes/Makefile index b649ce81f..3ccb65816 100644 --- a/proofs/cbmc/keccakf1600_xorbytes/Makefile +++ b/proofs/cbmc/keccakf1600_xorbytes/Makefile @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)KeccakF1600_StateXORBytes +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StateXORBytes USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)KeccakF1600_StateXORBytes +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StateXORBytes # 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/poly_getnoise_eta1122_4x/Makefile b/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile index f602715d8..15dc91293 100644 --- a/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile +++ b/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile @@ -21,7 +21,7 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c # Only relevant for K=2 ifeq ($(MLKEM_K),2) CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_getnoise_eta1122_4x -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta1 $(MLKEM_NAMESPACE)poly_cbd_eta2 $(FIPS202_NAMESPACE)shake256 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta1 $(MLKEM_NAMESPACE)poly_cbd_eta2 $(MLKEM_NAMESPACE)shake256 else CHECK_FUNCTION_CONTRACTS= USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/poly_getnoise_eta1_4x/Makefile b/proofs/cbmc/poly_getnoise_eta1_4x/Makefile index a163b03ba..ec1f04b23 100644 --- a/proofs/cbmc/poly_getnoise_eta1_4x/Makefile +++ b/proofs/cbmc/poly_getnoise_eta1_4x/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).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 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta1 $(MLKEM_NAMESPACE)shake256x4 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_getnoise_eta2/Makefile b/proofs/cbmc/poly_getnoise_eta2/Makefile index 51645df77..f801954b3 100644 --- a/proofs/cbmc/poly_getnoise_eta2/Makefile +++ b/proofs/cbmc/poly_getnoise_eta2/Makefile @@ -21,10 +21,10 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c # Only relevant for K=2 or K=4 ifeq ($(MLKEM_K),2) CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_getnoise_eta2 -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta2 $(FIPS202_NAMESPACE)shake256 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta2 $(MLKEM_NAMESPACE)shake256 else ifeq ($(MLKEM_K),4) CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_getnoise_eta2 -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta2 $(FIPS202_NAMESPACE)shake256 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_cbd_eta2 $(MLKEM_NAMESPACE)shake256 else CHECK_FUNCTION_CONTRACTS= USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/poly_rej_uniform/Makefile b/proofs/cbmc/poly_rej_uniform/Makefile index 339c8196c..2eae2baab 100644 --- a/proofs/cbmc/poly_rej_uniform/Makefile +++ b/proofs/cbmc/poly_rej_uniform/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/rej_uniform.c $(SRCDIR)/mlkem/fips202/fips202.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128_absorb_once $(FIPS202_NAMESPACE)shake128_squeezeblocks $(MLKEM_NAMESPACE)rej_uniform +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake128_absorb_once $(MLKEM_NAMESPACE)shake128_squeezeblocks $(MLKEM_NAMESPACE)rej_uniform APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_rej_uniform_x4/Makefile b/proofs/cbmc/poly_rej_uniform_x4/Makefile index 253250e9a..9c2d29a89 100644 --- a/proofs/cbmc/poly_rej_uniform_x4/Makefile +++ b/proofs/cbmc/poly_rej_uniform_x4/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/rej_uniform.c $(SRCDIR)/mlkem/fips202/fips202x4.c 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 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake128x4_absorb_once $(MLKEM_NAMESPACE)shake128x4_squeezeblocks $(MLKEM_NAMESPACE)rej_uniform APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/sha3_256/Makefile b/proofs/cbmc/sha3_256/Makefile index 799e32ad7..78c19a212 100644 --- a/proofs/cbmc/sha3_256/Makefile +++ b/proofs/cbmc/sha3_256/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_256 -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_absorb_once $(FIPS202_NAMESPACE)keccak_squeeze_once +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)sha3_256 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_absorb_once $(MLKEM_NAMESPACE)keccak_squeeze_once APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)sha3_256 +FUNCTION_NAME = $(MLKEM_NAMESPACE)sha3_256 # 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/sha3_512/Makefile b/proofs/cbmc/sha3_512/Makefile index db289f2ba..30a380653 100644 --- a/proofs/cbmc/sha3_512/Makefile +++ b/proofs/cbmc/sha3_512/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)sha3_512 -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_absorb_once $(FIPS202_NAMESPACE)keccak_squeeze_once +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)sha3_512 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_absorb_once $(MLKEM_NAMESPACE)keccak_squeeze_once APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)sha3_512 +FUNCTION_NAME = $(MLKEM_NAMESPACE)sha3_512 # 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/shake128_absorb_once/Makefile b/proofs/cbmc/shake128_absorb_once/Makefile index ac6819ff4..34ed19d6b 100644 --- a/proofs/cbmc/shake128_absorb_once/Makefile +++ b/proofs/cbmc/shake128_absorb_once/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128_absorb_once -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_absorb_once +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake128_absorb_once +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_absorb_once APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)shake128_absorb_once +FUNCTION_NAME = $(MLKEM_NAMESPACE)shake128_absorb_once # 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/shake128_squeezeblocks/Makefile b/proofs/cbmc/shake128_squeezeblocks/Makefile index 43fc874d1..d2f5032db 100644 --- a/proofs/cbmc/shake128_squeezeblocks/Makefile +++ b/proofs/cbmc/shake128_squeezeblocks/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128_squeezeblocks -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_squeezeblocks +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake128_squeezeblocks +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_squeezeblocks APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)shake128_squeezeblocks +FUNCTION_NAME = $(MLKEM_NAMESPACE)shake128_squeezeblocks # 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/shake128x4_absorb_once/Makefile b/proofs/cbmc/shake128x4_absorb_once/Makefile index 62b533674..280530e1c 100644 --- a/proofs/cbmc/shake128x4_absorb_once/Makefile +++ b/proofs/cbmc/shake128x4_absorb_once/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128x4_absorb_once -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_absorb_once_x4 +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake128x4_absorb_once +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_absorb_once_x4 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)shake128x4_absorb_once +FUNCTION_NAME = $(MLKEM_NAMESPACE)shake128x4_absorb_once # 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/shake128x4_squeezeblocks/Makefile b/proofs/cbmc/shake128x4_squeezeblocks/Makefile index 29e164a7e..b7de82e0e 100644 --- a/proofs/cbmc/shake128x4_squeezeblocks/Makefile +++ b/proofs/cbmc/shake128x4_squeezeblocks/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128x4_squeezeblocks -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_squeezeblocks_x4 +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake128x4_squeezeblocks +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_squeezeblocks_x4 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)shake128x4_squeezeblocks +FUNCTION_NAME = $(MLKEM_NAMESPACE)shake128x4_squeezeblocks # 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/shake256/Makefile b/proofs/cbmc/shake256/Makefile index cd06b3589..02da46f21 100644 --- a/proofs/cbmc/shake256/Makefile +++ b/proofs/cbmc/shake256/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256 -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_absorb_once $(FIPS202_NAMESPACE)keccak_squeeze_once +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake256 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_absorb_once $(MLKEM_NAMESPACE)keccak_squeeze_once APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)shake256 +FUNCTION_NAME = $(MLKEM_NAMESPACE)shake256 # 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/shake256x4/Makefile b/proofs/cbmc/shake256x4/Makefile index 1aadb0fe5..68e9e6f92 100644 --- a/proofs/cbmc/shake256x4/Makefile +++ b/proofs/cbmc/shake256x4/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256x4 -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)keccak_absorb_once_x4 $(FIPS202_NAMESPACE)keccak_squeezeblocks_x4 +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)shake256x4 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)keccak_absorb_once_x4 $(MLKEM_NAMESPACE)keccak_squeezeblocks_x4 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(FIPS202_NAMESPACE)shake256x4 +FUNCTION_NAME = $(MLKEM_NAMESPACE)shake256x4 # 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/scripts/check-namespace b/scripts/check-namespace index 2b498bbcf..b9654882d 100755 --- a/scripts/check-namespace +++ b/scripts/check-namespace @@ -65,24 +65,13 @@ def check_folder(folder, namespace): assert checked > 0 -def list_mlkem_namespaces(lvl): - return [ - f"PQCP_MLKEM_NATIVE_MLKEM{lvl}", - ] - - -def list_fips202_namespaces(): - return [ - f"PQCP_MLKEM_NATIVE_FIPS202", - ] - +def make_mlkem_namespace(lvl): + return [f"PQCP_MLKEM_NATIVE_MLKEM{lvl}"] def run(): - check_folder("test/build/mlkem512/mlkem", list_mlkem_namespaces(512)) - check_folder("test/build/mlkem768/mlkem", list_mlkem_namespaces(768)) - check_folder("test/build/mlkem1024/mlkem", list_mlkem_namespaces(1024)) - check_folder("test/build/mlkem/fips202", list_fips202_namespaces()) - + check_folder("test/build/mlkem512/mlkem", make_mlkem_namespace(512)) + check_folder("test/build/mlkem768/mlkem", make_mlkem_namespace(768)) + check_folder("test/build/mlkem1024/mlkem", make_mlkem_namespace(1024)) if __name__ == "__main__": run() diff --git a/test/mk/components.mk b/test/mk/components.mk index 724a2a35f..bca2373d8 100644 --- a/test/mk/components.mk +++ b/test/mk/components.mk @@ -5,11 +5,6 @@ ifeq ($(OPT),1) FIPS202_SRCS += $(wildcard mlkem/fips202/native/aarch64/src/*.S) $(wildcard mlkem/fips202/native/aarch64/src/*.c) $(wildcard mlkem/fips202/native/x86_64/src/*.c) endif -$(BUILD_DIR)/libmlkem.a: $(call OBJS, $(FIPS202_SRCS)) -$(BUILD_DIR)/libmlkem512.a: $(call OBJS, $(FIPS202_SRCS)) -$(BUILD_DIR)/libmlkem768.a: $(call OBJS, $(FIPS202_SRCS)) -$(BUILD_DIR)/libmlkem1024.a: $(call OBJS, $(FIPS202_SRCS)) - SOURCES += $(wildcard mlkem/*.c) $(wildcard mlkem/debug/*.c) ifeq ($(OPT),1) SOURCES += $(wildcard mlkem/native/aarch64/src/*.[csS]) $(wildcard mlkem/native/x86_64/src/*.[csS]) @@ -23,31 +18,18 @@ MLKEM512_DIR = $(BUILD_DIR)/mlkem512 MLKEM768_DIR = $(BUILD_DIR)/mlkem768 MLKEM1024_DIR = $(BUILD_DIR)/mlkem1024 -# build lib.a -define BUILD_LIB -$(BUILD_DIR)/lib$(1).a: CFLAGS += -static -$(BUILD_DIR)/lib$(1).a: $(call MAKE_OBJS,$(BUILD_DIR)/$(1),$(SOURCES)) - -# NOTE: -# libmlkem.a does not link against libmlkem{512,768,1024}.a, but the underlying object files. -# Still, we currently need a dependency on libmlkem{512,768,1024}.a here as otherwise there is -# a hiccup with the setting of MLKEM_K (TODO: look at this more closely) -$(BUILD_DIR)/libmlkem.a: $(BUILD_DIR)/lib$(1).a $(call MAKE_OBJS,$(BUILD_DIR)/$(1),$(SOURCES)) -endef +MLKEM512_OBJS = $(call MAKE_OBJS,$(MLKEM512_DIR),$(SOURCES) $(FIPS202_SRCS)) +$(MLKEM512_OBJS): CFLAGS += -DMLKEM_K=2 +MLKEM768_OBJS = $(call MAKE_OBJS,$(MLKEM768_DIR),$(SOURCES) $(FIPS202_SRCS)) +$(MLKEM768_OBJS): CFLAGS += -DMLKEM_K=3 +MLKEM1024_OBJS = $(call MAKE_OBJS,$(MLKEM1024_DIR),$(SOURCES) $(FIPS202_SRCS)) +$(MLKEM1024_OBJS): CFLAGS += -DMLKEM_K=4 -$(BUILD_DIR)/libmlkem512.a: CFLAGS += -DMLKEM_K=2 -$(BUILD_DIR)/libmlkem768.a: CFLAGS += -DMLKEM_K=3 -$(BUILD_DIR)/libmlkem1024.a: CFLAGS += -DMLKEM_K=4 +$(BUILD_DIR)/libmlkem512.a: $(MLKEM512_OBJS) +$(BUILD_DIR)/libmlkem768.a: $(MLKEM768_OBJS) +$(BUILD_DIR)/libmlkem1024.a: $(MLKEM1024_OBJS) -# build libmlkem512.a libmlkem768.a libmlkem1024.a -$(foreach scheme,mlkem512 mlkem768 mlkem1024, \ - $(eval $(call BUILD_LIB,$(scheme)))) - -# rules for compilation for all tests: mainly linking with mlkem static link library -define ADD_SOURCE -$(BUILD_DIR)/$(1)/bin/$(2)$(shell echo $(1) | tr -d -c 0-9): LDLIBS += -L$(BUILD_DIR) -l$(1) -$(BUILD_DIR)/$(1)/bin/$(2)$(shell echo $(1) | tr -d -c 0-9): $(BUILD_DIR)/$(1)/test/$(2).c.o $(BUILD_DIR)/lib$(1).a -endef +$(BUILD_DIR)/libmlkem.a: $(MLKEM512_OBJS) $(MLKEM768_OBJS) $(MLKEM1024_OBJS) $(MLKEM512_DIR)/bin/bench_mlkem512: CFLAGS += -Itest/hal $(MLKEM768_DIR)/bin/bench_mlkem768: CFLAGS += -Itest/hal @@ -67,6 +49,12 @@ $(MLKEM512_DIR)/bin/%: CFLAGS += -DMLKEM_K=2 $(MLKEM768_DIR)/bin/%: CFLAGS += -DMLKEM_K=3 $(MLKEM1024_DIR)/bin/%: CFLAGS += -DMLKEM_K=4 +# Link tests with respective library +define ADD_SOURCE +$(BUILD_DIR)/$(1)/bin/$(2)$(shell echo $(1) | tr -d -c 0-9): LDLIBS += -L$(BUILD_DIR) -l$(1) +$(BUILD_DIR)/$(1)/bin/$(2)$(shell echo $(1) | tr -d -c 0-9): $(BUILD_DIR)/$(1)/test/$(2).c.o $(BUILD_DIR)/lib$(1).a +endef + $(foreach scheme,mlkem512 mlkem768 mlkem1024, \ $(foreach test,$(ALL_TESTS), \ $(eval $(call ADD_SOURCE,$(scheme),$(test))) \ diff --git a/test/mk/config.mk~ b/test/mk/config.mk~ deleted file mode 100644 index 5368abf51..000000000 --- a/test/mk/config.mk~ +++ /dev/null @@ -1,111 +0,0 @@ -# SPDX-License-Identifier: Apache-2.0 -ifndef _CONFIG -_CONFIG := - -SRCDIR := $(CURDIR) - -############## -# GCC config # -############## - -CROSS_PREFIX ?= -CC ?= gcc -CPP ?= cpp -AR ?= ar -CC := $(CROSS_PREFIX)$(CC) -CPP := $(CROSS_PREFIX)$(CPP) -AR := $(CROSS_PREFIX)$(AR) -LD := $(CC) -OBJCOPY := $(CROSS_PREFIX)objcopy -SIZE := $(CROSS_PREFIX)size - -# NOTE: gcc-ar is a wrapper around ar that ensures proper integration with GCC plugins, -# such as lto. Using gcc-ar is preferred when creating or linking static libraries -# if the binary is compiled with -flto. However, it is not universally present, so -# only use it if available. -CC_AR ?= $(if $(and $(findstring gcc,$(shell $(CC) --version)), $(findstring gcc-ar, $(shell which $(CROSS_PREFIX)gcc-ar))),gcc-ar,ar) -CC_AR := $(CROSS_PREFIX)$(CC_AR) - -################# -# Common config # -################# -CFLAGS := \ - -Wall \ - -Wextra \ - -Wpedantic \ - -Werror \ - -Wmissing-prototypes \ - -Wshadow \ - -Wpointer-arith \ - -Wno-long-long \ - -Wno-unknown-pragmas \ - -Wno-unused-command-line-argument \ - -O3 \ - -fomit-frame-pointer \ - -std=c99 \ - -pedantic \ - -MMD \ - $(CFLAGS) - -################## -# Some Variables # -################## -Q ?= @ - -HOST_PLATFORM := $(shell uname -s)-$(shell uname -m) -# linux x86_64 -ifeq ($(HOST_PLATFORM),Linux-x86_64) - CFLAGS += -z noexecstack -endif - -ifeq ($(CYCLES),PMU) - CFLAGS += -DPMU_CYCLES -endif - -ifeq ($(CYCLES),PERF) - CFLAGS += -DPERF_CYCLES -endif - -ifeq ($(CYCLES),M1) - CFLAGS += -DM1_CYCLES -endif - -############################## -# Include retained variables # -############################## - -AUTO ?= 1 -CYCLES ?= -OPT ?= 1 -RETAINED_VARS := CROSS_PREFIX CYCLES OPT AUTO - -ifeq ($(AUTO),1) -include mk/auto.mk -endif - -BUILD_DIR ?= test/build - -MAKE_OBJS = $(2:%=$(1)/%.o) -OBJS = $(call MAKE_OBJS,$(BUILD_DIR),$(1)) - -CONFIG := $(BUILD_DIR)/config.mk - --include $(CONFIG) - -$(CONFIG): - @echo " GEN $@" - $(Q)[ -d $(@D) ] || mkdir -p $(@D) - @echo "# These variables are retained and can't be changed without a clean" > $@ - @$(foreach var,$(RETAINED_VARS),echo "$(var) := $($(var))" >> $@; echo "LAST_$(var) := $($(var))" >> $@;) - -define VAR_CHECK -ifneq ($$(origin LAST_$(1)),undefined) -ifneq "$$($(1))" "$$(LAST_$(1))" -$$(info Variable $(1) changed, forcing rebuild!) -.PHONY: $(CONFIG) -endif -endif -endef - -$(foreach VAR,$(RETAINED_VARS),$(eval $(call VAR_CHECK,$(VAR)))) -endif diff --git a/test/mk/rules.mk b/test/mk/rules.mk index cd5b0576f..0c93c9e97 100644 --- a/test/mk/rules.mk +++ b/test/mk/rules.mk @@ -1,4 +1,5 @@ # SPDX-License-Identifier: Apache-2.0 + $(BUILD_DIR)/mlkem512/bin/%: $(CONFIG) $(Q)echo " LD $@" $(Q)[ -d $(@D) ] || mkdir -p $(@D) @@ -19,10 +20,10 @@ $(BUILD_DIR)/%.a: $(CONFIG) $(Q)[ -d $(@D) ] || mkdir -p $(@D) $(Q)rm -f $@ $(Q)$(CC_AR) rcs $@ $(filter %.o,$^) - -# NOTE: -# $AR doesn't care about duplicated symbols, one can only find it out via actually linking. -# The easiest one to do this that one can think of is to create a dummy C file with empty main function on the fly, pipe it to $CC and link with the built library + # $AR doesn't care about duplicated symbols, one can only find it out + # via actually linking. The easiest one to do this that one can think + # of is to create a dummy C file with empty main function on the fly, + # pipe it to $CC and link with the built library $(eval _LIB := $(subst $(BUILD_DIR)/lib,,$(@:%.a=%))) $(eval _CFLAGS := $(subst -static,,$(CFLAGS))) @@ -42,16 +43,6 @@ else # if not on macOS endif $(Q)echo " AR Checked for duplicated symbols" -$(BUILD_DIR)/%.c.o: %.c $(CONFIG) - $(Q)echo " CC $@" - $(Q)[ -d $(@D) ] || mkdir -p $(@D) - $(Q)$(CC) -c -o $@ $(CFLAGS) $< - -$(BUILD_DIR)/%.S.o: %.S $(CONFIG) - $(Q)echo " AS $@" - $(Q)[ -d $(@D) ] || mkdir -p $(@D) - $(Q)$(CC) -c -o $@ $(CFLAGS) $< - $(BUILD_DIR)/mlkem512/%.c.o: %.c $(CONFIG) $(Q)echo " CC $@" $(Q)[ -d $(@D) ] || mkdir -p $(@D)