From 7f590c0cff58052b82a1de5349d84938910cb2c4 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 13:23:21 -0700 Subject: [PATCH 01/18] Namespacing: Switch to mlkem-native style namespace, api, common, and config Signed-off-by: Jake Massimo --- Makefile | 1 + mldsa/api.h | 98 ++++---------- mldsa/common.h | 79 ++++++++++- mldsa/config.h | 103 +++++++++++++- .../native/aarch64/src/arith_native_aarch64.h | 15 +-- mldsa/packing.h | 1 + mldsa/params.h | 19 +-- mldsa/sign.h | 19 +-- test/acvp_mldsa.c | 1 + test/gen_KAT.c | 1 + test/mk/auto.mk | 127 ++++++++++++++---- test/mk/compiler.mk | 66 +++++++++ 12 files changed, 387 insertions(+), 143 deletions(-) create mode 100644 test/mk/compiler.mk diff --git a/Makefile b/Makefile index 86593360..84d6a679 100644 --- a/Makefile +++ b/Makefile @@ -33,6 +33,7 @@ $(error Neither 'shasum' nor 'sha256sum' found. Please install one of these tool endif include test/mk/config.mk +include test/mk/compiler.mk include test/mk/components.mk include test/mk/rules.mk diff --git a/mldsa/api.h b/mldsa/api.h index 43805455..c3584747 100644 --- a/mldsa/api.h +++ b/mldsa/api.h @@ -7,107 +7,57 @@ #include #include +#include "common.h" #define MLD_44_PUBLICKEYBYTES 1312 #define MLD_44_SECRETKEYBYTES 2560 #define MLD_44_BYTES 2420 -#define MLD_44_ref_PUBLICKEYBYTES MLD_44_PUBLICKEYBYTES -#define MLD_44_ref_SECRETKEYBYTES MLD_44_SECRETKEYBYTES -#define MLD_44_ref_BYTES MLD_44_BYTES - -int MLD_44_ref_keypair(uint8_t *pk, uint8_t *sk); - -int MLD_44_ref_signature(uint8_t *sig, size_t *siglen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *sk); - -int MLD_44_ref(uint8_t *sm, size_t *smlen, const uint8_t *m, size_t mlen, - const uint8_t *ctx, size_t ctxlen, const uint8_t *sk); - -int MLD_44_ref_verify(const uint8_t *sig, size_t siglen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *pk); - -int MLD_44_ref_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen, - const uint8_t *ctx, size_t ctxlen, const uint8_t *pk); - #define MLD_65_PUBLICKEYBYTES 1952 #define MLD_65_SECRETKEYBYTES 4032 #define MLD_65_BYTES 3309 -#define MLD_65_ref_PUBLICKEYBYTES MLD_65_PUBLICKEYBYTES -#define MLD_65_ref_SECRETKEYBYTES MLD_65_SECRETKEYBYTES -#define MLD_65_ref_BYTES MLD_65_BYTES - -int MLD_65_ref_keypair(uint8_t *pk, uint8_t *sk); - -int MLD_65_ref_signature(uint8_t *sig, size_t *siglen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *sk); - -int MLD_65_ref(uint8_t *sm, size_t *smlen, const uint8_t *m, size_t mlen, - const uint8_t *ctx, size_t ctxlen, const uint8_t *sk); - -int MLD_65_ref_verify(const uint8_t *sig, size_t siglen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *pk); - -int MLD_65_ref_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen, - const uint8_t *ctx, size_t ctxlen, const uint8_t *pk); - #define MLD_87_PUBLICKEYBYTES 2592 #define MLD_87_SECRETKEYBYTES 4896 #define MLD_87_BYTES 4627 -#define MLD_87_ref_PUBLICKEYBYTES MLD_87_PUBLICKEYBYTES -#define MLD_87_ref_SECRETKEYBYTES MLD_87_SECRETKEYBYTES -#define MLD_87_ref_BYTES MLD_87_BYTES - -int MLD_87_ref_keypair(uint8_t *pk, uint8_t *sk); +int MLD_NAMESPACE_K(keypair)(uint8_t *pk, uint8_t *sk); -int MLD_87_ref_signature(uint8_t *sig, size_t *siglen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *sk); +int MLD_NAMESPACE_K(signature)(uint8_t *sig, size_t *siglen, const uint8_t *m, + size_t mlen, const uint8_t *ctx, size_t ctxlen, + const uint8_t *sk); -int MLD_87_ref(uint8_t *sm, size_t *smlen, const uint8_t *m, size_t mlen, - const uint8_t *ctx, size_t ctxlen, const uint8_t *sk); +int MLD_NAMESPACE_K(sign)(uint8_t *sm, size_t *smlen, const uint8_t *m, + size_t mlen, const uint8_t *ctx, size_t ctxlen, + const uint8_t *sk); -int MLD_87_ref_verify(const uint8_t *sig, size_t siglen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *pk); +int MLD_NAMESPACE_K(verify)(const uint8_t *sig, size_t siglen, const uint8_t *m, + size_t mlen, const uint8_t *ctx, size_t ctxlen, + const uint8_t *pk); -int MLD_87_ref_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen, - const uint8_t *ctx, size_t ctxlen, const uint8_t *pk); +int MLD_NAMESPACE_K(open)(uint8_t *m, size_t *mlen, const uint8_t *sm, + size_t smlen, const uint8_t *ctx, size_t ctxlen, + const uint8_t *pk); -#if MLDSA_MODE == 2 +#if MLD_CONFIG_PARAMETER_SET == 44 #define CRYPTO_PUBLICKEYBYTES MLD_44_PUBLICKEYBYTES #define CRYPTO_SECRETKEYBYTES MLD_44_SECRETKEYBYTES #define CRYPTO_BYTES MLD_44_BYTES -#define crypto_sign_keypair MLD_44_ref_keypair -#define crypto_sign_signature MLD_44_ref_signature -#define crypto_sign MLD_44_ref -#define crypto_sign_verify MLD_44_ref_verify -#define crypto_sign_open MLD_44_ref_open -#elif MLDSA_MODE == 3 +#elif MLD_CONFIG_PARAMETER_SET == 65 #define CRYPTO_PUBLICKEYBYTES MLD_65_PUBLICKEYBYTES #define CRYPTO_SECRETKEYBYTES MLD_65_SECRETKEYBYTES #define CRYPTO_BYTES MLD_65_BYTES -#define crypto_sign_keypair MLD_65_ref_keypair -#define crypto_sign_signature MLD_65_ref_signature -#define crypto_sign MLD_65_ref -#define crypto_sign_verify MLD_65_ref_verify -#define crypto_sign_open MLD_65_ref_open -#elif MLDSA_MODE == 5 +#elif MLD_CONFIG_PARAMETER_SET == 87 #define CRYPTO_PUBLICKEYBYTES MLD_87_PUBLICKEYBYTES #define CRYPTO_SECRETKEYBYTES MLD_87_SECRETKEYBYTES #define CRYPTO_BYTES MLD_87_BYTES -#define crypto_sign_keypair MLD_87_ref_keypair -#define crypto_sign_signature MLD_87_ref_signature -#define crypto_sign MLD_87_ref -#define crypto_sign_verify MLD_87_ref_verify -#define crypto_sign_open MLD_87_ref_open -#endif /* MLDSA_MODE == 5 */ +#endif + +#define crypto_sign_keypair MLD_NAMESPACE_K(keypair) +#define crypto_sign_signature MLD_NAMESPACE_K(signature) +#define crypto_sign MLD_NAMESPACE_K(sign) +#define crypto_sign_verify MLD_NAMESPACE_K(verify) +#define crypto_sign_open MLD_NAMESPACE_K(open) #endif /* !MLD_API_H */ diff --git a/mldsa/common.h b/mldsa/common.h index bd09ba99..28c1cce2 100644 --- a/mldsa/common.h +++ b/mldsa/common.h @@ -16,19 +16,50 @@ #include "params.h" #include "sys.h" +/* Internal and public API have external linkage by default, but + * this can be overwritten by the user, e.g. for single-CU builds. */ +#if !defined(MLD_CONFIG_INTERNAL_API_QUALIFIER) +#define MLD_INTERNAL_API +#else +#define MLD_INTERNAL_API MLD_CONFIG_INTERNAL_API_QUALIFIER +#endif -#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) && \ - !defined(MLD_CONFIG_ARITH_BACKEND_FILE) -#error Bad configuration: MLD_CONFIG_USE_NATIVE_BACKEND_ARITH is set, but MLD_CONFIG_ARITH_BACKEND_FILE is not. +#if !defined(MLD_CONFIG_EXTERNAL_API_QUALIFIER) +#define MLD_EXTERNAL_API +#else +#define MLD_EXTERNAL_API MLD_CONFIG_EXTERNAL_API_QUALIFIER #endif -#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) -#include MLD_CONFIG_ARITH_BACKEND_FILE +#if defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) || \ + defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) +#define MLD_MULTILEVEL_BUILD #endif #define MLD_CONCAT_(x1, x2) x1##x2 #define MLD_CONCAT(x1, x2) MLD_CONCAT_(x1, x2) +#if defined(MLD_MULTILEVEL_BUILD) +#define MLD_ADD_PARAM_SET(s) MLD_CONCAT(s, MLD_CONFIG_PARAMETER_SET) +#else +#define MLD_ADD_PARAM_SET(s) s +#endif + +#define MLD_NAMESPACE_PREFIX MLD_CONCAT(MLD_CONFIG_NAMESPACE_PREFIX, _) +#define MLD_NAMESPACE_PREFIX_K \ + MLD_CONCAT(MLD_ADD_PARAM_SET(MLD_CONFIG_NAMESPACE_PREFIX), _) + +/* Functions are prefixed by MLD_CONFIG_NAMESPACE_PREFIX. + * + * If multiple parameter sets are used, functions depending on the parameter + * set are additionally prefixed with 44/65/87. See config.h. + * + * Example: If MLD_CONFIG_NAMESPACE_PREFIX is PQCP_MLDSA_NATIVE_MLDSA, then + * MLD_NAMESPACE_K(keypair) becomes PQCP_MLDSA_NATIVE_MLDSA44_keypair/ + * PQCP_MLDSA_NATIVE_MLDSA65_keypair/PQCP_MLDSA_NATIVE_MLDSA87_keypair. + */ +#define MLD_NAMESPACE(s) MLD_CONCAT(MLD_NAMESPACE_PREFIX, s) +#define MLD_NAMESPACE_K(s) MLD_CONCAT(MLD_NAMESPACE_PREFIX_K, s) + /* On Apple platforms, we need to emit leading underscore * in front of assembly symbols. We thus introducee a separate * namespace wrapper for ASM symbols. */ @@ -53,11 +84,47 @@ * all source files are included, even those that are not needed. * Those files are appropriately guarded and will be empty when unneeded. * The following is to avoid compilers complaining about this. */ -#define MLD_EMPTY_CU(s) extern int MLD_NAMESPACE(empty_cu_##s); +#define MLD_EMPTY_CU(s) extern int MLD_NAMESPACE_K(empty_cu_##s); + +/* MLD_CONFIG_NO_ASM takes precedence over MLD_USE_NATIVE_XXX */ +#if defined(MLD_CONFIG_NO_ASM) +#undef MLD_CONFIG_USE_NATIVE_BACKEND_ARITH +#undef MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 +#endif + +#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) && \ + !defined(MLD_CONFIG_ARITH_BACKEND_FILE) +#error Bad configuration: MLD_CONFIG_USE_NATIVE_BACKEND_ARITH is set, but MLD_CONFIG_ARITH_BACKEND_FILE is not. +#endif + +#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202) && \ + !defined(MLD_CONFIG_FIPS202_BACKEND_FILE) +#error Bad configuration: MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 is set, but MLD_CONFIG_FIPS202_BACKEND_FILE is not. +#endif + +#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) +#include MLD_CONFIG_ARITH_BACKEND_FILE +/* Include to enforce consistency of API and implementation, + * and conduct sanity checks on the backend. + * + * Keep this _after_ the inclusion of the backend; otherwise, + * the sanity checks won't have an effect. */ +#if defined(MLD_CHECK_APIS) && !defined(__ASSEMBLER__) +#include "native/api.h" +#endif +#endif /* MLD_CONFIG_USE_NATIVE_BACKEND_ARITH */ #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202) #include MLD_CONFIG_FIPS202_BACKEND_FILE +/* Include to enforce consistency of API and implementation, + * and conduct sanity checks on the backend. + * + * Keep this _after_ the inclusion of the backend; otherwise, + * the sanity checks won't have an effect. */ +#if defined(MLD_CHECK_APIS) && !defined(__ASSEMBLER__) +#include "fips202/native/api.h" #endif +#endif /* MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */ #if !defined(__ASSEMBLER__) #include diff --git a/mldsa/config.h b/mldsa/config.h index 34979470..ac966f58 100644 --- a/mldsa/config.h +++ b/mldsa/config.h @@ -7,20 +7,90 @@ #define MLD_RANDOMIZED_SIGNING +/****************************************************************************** + * Name: MLD_CONFIG_PARAMETER_SET + * + * Description: Specifies the parameter set for ML-DSA + * - MLD_CONFIG_PARAMETER_SET=44 corresponds to ML-DSA-44 + * - MLD_CONFIG_PARAMETER_SET=65 corresponds to ML-DSA-65 + * - MLD_CONFIG_PARAMETER_SET=87 corresponds to ML-DSA-87 + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +#ifndef MLD_CONFIG_PARAMETER_SET +/* Map legacy MLDSA_MODE to new parameter set for backward compatibility */ #ifndef MLDSA_MODE #define MLDSA_MODE 2 #endif #if MLDSA_MODE == 2 -#define MLD_NAMESPACETOP MLD_44_ref -#define MLD_NAMESPACE(s) MLD_44_ref_##s +#define MLD_CONFIG_PARAMETER_SET 44 #elif MLDSA_MODE == 3 -#define MLD_NAMESPACETOP MLD_65_ref -#define MLD_NAMESPACE(s) MLD_65_ref_##s +#define MLD_CONFIG_PARAMETER_SET 65 #elif MLDSA_MODE == 5 -#define MLD_NAMESPACETOP MLD_87_ref -#define MLD_NAMESPACE(s) MLD_87_ref_##s +#define MLD_CONFIG_PARAMETER_SET 87 +#else +#define MLD_CONFIG_PARAMETER_SET 44 /* Default to ML-DSA-44 */ #endif +#endif /* !MLD_CONFIG_PARAMETER_SET */ + +/****************************************************************************** + * Name: MLD_CONFIG_NAMESPACE_PREFIX + * + * Description: The prefix to use to namespace global symbols from mldsa/. + * + * In a multi-level build (that is, if either + * - MLD_CONFIG_MULTILEVEL_WITH_SHARED, or + * - MLD_CONFIG_MULTILEVEL_NO_SHARED, + * are set, level-dependent symbols will additionally be prefixed + * with the parameter set (44/65/87). + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +#if !defined(MLD_CONFIG_NAMESPACE_PREFIX) +#define MLD_CONFIG_NAMESPACE_PREFIX MLD_DEFAULT_NAMESPACE_PREFIX +#endif + +/****************************************************************************** + * Name: MLD_CONFIG_MULTILEVEL_WITH_SHARED + * + * Description: This is for multi-level builds of mldsa-native only. If you + * need only a single parameter set, keep this unset. + * + * If this is set, all MLD_CONFIG_PARAMETER_SET-independent + * code will be included in the build, including code needed only + * for other parameter sets. + * + * To build mldsa-native with support for all parameter sets, + * build it three times -- once per parameter set -- and set the + * option MLD_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of + * them, and MLD_CONFIG_MULTILEVEL_NO_SHARED for the others. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_WITH_SHARED */ + +/****************************************************************************** + * Name: MLD_CONFIG_MULTILEVEL_NO_SHARED + * + * Description: This is for multi-level builds of mldsa-native only. If you + * need only a single parameter set, keep this unset. + * + * If this is set, no MLD_CONFIG_PARAMETER_SET-independent code + * will be included in the build. + * + * To build mldsa-native with support for all parameter sets, + * build it three times -- once per parameter set -- and set the + * option MLD_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of + * them, and MLD_CONFIG_MULTILEVEL_NO_SHARED for the others. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ /****************************************************************************** @@ -205,6 +275,27 @@ *****************************************************************************/ /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */ +/************************* Config internals ********************************/ + +/* Default namespace + * + * Don't change this. If you need a different namespace, re-define + * MLD_CONFIG_NAMESPACE_PREFIX above instead, and remove the following. + * + * The default MLDSA namespace is + * + * PQCP_MLDSA_NATIVE_MLDSA_ + * + * e.g., PQCP_MLDSA_NATIVE_MLDSA44_ + */ + +#if MLD_CONFIG_PARAMETER_SET == 44 +#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA44 +#elif MLD_CONFIG_PARAMETER_SET == 65 +#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA65 +#elif MLD_CONFIG_PARAMETER_SET == 87 +#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA87 +#endif #endif /* !MLD_CONFIG_H */ diff --git a/mldsa/native/aarch64/src/arith_native_aarch64.h b/mldsa/native/aarch64/src/arith_native_aarch64.h index e011ab4c..1ac66ab3 100644 --- a/mldsa/native/aarch64/src/arith_native_aarch64.h +++ b/mldsa/native/aarch64/src/arith_native_aarch64.h @@ -11,21 +11,18 @@ #include "../../../common.h" #define mld_aarch64_ntt_zetas_layer123456 \ - MLD_NAMESPACE(mld_aarch64_ntt_zetas_layer123456) -#define mld_aarch64_ntt_zetas_layer78 \ - MLD_NAMESPACE(mld_aarch64_ntt_zetas_layer78) - -#define mld_aarch64_intt_zetas_layer78 \ - MLD_NAMESPACE(mld_aarch64_intt_zetas_layer78) + MLD_NAMESPACE(aarch64_ntt_zetas_layer123456) +#define mld_aarch64_ntt_zetas_layer78 MLD_NAMESPACE(aarch64_ntt_zetas_layer78) +#define mld_aarch64_intt_zetas_layer78 MLD_NAMESPACE(aarch64_intt_zetas_layer78) #define mld_aarch64_intt_zetas_layer123456 \ - MLD_NAMESPACE(mld_aarch64_intt_zetas_layer123456) + MLD_NAMESPACE(aarch64_intt_zetas_layer123456) +#define mld_rej_uniform_table MLD_NAMESPACE(rej_uniform_table) +#define mld_rej_uniform_eta_table MLD_NAMESPACE(rej_uniform_eta_table) extern const int32_t mld_aarch64_ntt_zetas_layer123456[]; extern const int32_t mld_aarch64_ntt_zetas_layer78[]; - extern const int32_t mld_aarch64_intt_zetas_layer78[]; extern const int32_t mld_aarch64_intt_zetas_layer123456[]; - extern const uint8_t mld_rej_uniform_table[]; extern const uint8_t mld_rej_uniform_eta_table[]; diff --git a/mldsa/packing.h b/mldsa/packing.h index c1d932ce..3efeda2d 100644 --- a/mldsa/packing.h +++ b/mldsa/packing.h @@ -6,6 +6,7 @@ #define MLD_PACKING_H #include +#include "api.h" #include "polyvec.h" #define mld_pack_pk MLD_NAMESPACE(pack_pk) diff --git a/mldsa/params.h b/mldsa/params.h index 0e1747e1..920fc798 100644 --- a/mldsa/params.h +++ b/mldsa/params.h @@ -5,7 +5,7 @@ #ifndef MLD_PARAMS_H #define MLD_PARAMS_H -#include "common.h" +#include "config.h" #define MLDSA_SEEDBYTES 32 #define MLDSA_CRHBYTES 64 @@ -16,7 +16,7 @@ #define MLDSA_Q_HALF ((MLDSA_Q + 1) / 2) /* 4190209 */ #define MLDSA_D 13 -#if MLDSA_MODE == 2 +#if MLD_CONFIG_PARAMETER_SET == 44 #define MLDSA_K 4 #define MLDSA_L 4 @@ -31,7 +31,7 @@ #define MLDSA_POLYW1_PACKEDBYTES 192 #define MLDSA_POLYETA_PACKEDBYTES 96 -#elif MLDSA_MODE == 3 +#elif MLD_CONFIG_PARAMETER_SET == 65 #define MLDSA_K 6 #define MLDSA_L 5 @@ -46,7 +46,7 @@ #define MLDSA_POLYW1_PACKEDBYTES 128 #define MLDSA_POLYETA_PACKEDBYTES 128 -#elif MLDSA_MODE == 5 +#elif MLD_CONFIG_PARAMETER_SET == 87 #define MLDSA_K 8 #define MLDSA_L 7 @@ -61,19 +61,10 @@ #define MLDSA_POLYW1_PACKEDBYTES 128 #define MLDSA_POLYETA_PACKEDBYTES 96 -#endif /* MLDSA_MODE == 5 */ +#endif /* MLD_CONFIG_PARAMETER_SET == 87 */ #define MLDSA_POLYT1_PACKEDBYTES 320 #define MLDSA_POLYT0_PACKEDBYTES 416 #define MLDSA_POLYVECH_PACKEDBYTES (MLDSA_OMEGA + MLDSA_K) -#define CRYPTO_PUBLICKEYBYTES \ - (MLDSA_SEEDBYTES + MLDSA_K * MLDSA_POLYT1_PACKEDBYTES) -#define CRYPTO_SECRETKEYBYTES \ - (2 * MLDSA_SEEDBYTES + MLDSA_TRBYTES + MLDSA_L * MLDSA_POLYETA_PACKEDBYTES + \ - MLDSA_K * MLDSA_POLYETA_PACKEDBYTES + MLDSA_K * MLDSA_POLYT0_PACKEDBYTES) -#define CRYPTO_BYTES \ - (MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES + \ - MLDSA_POLYVECH_PACKEDBYTES) - #endif /* !MLD_PARAMS_H */ diff --git a/mldsa/sign.h b/mldsa/sign.h index acf05bdf..40985b40 100644 --- a/mldsa/sign.h +++ b/mldsa/sign.h @@ -14,6 +14,16 @@ #include "sys.h" #define crypto_sign_keypair_internal MLD_NAMESPACE(keypair_internal) +#define crypto_sign_keypair MLD_NAMESPACE_K(keypair) +#define crypto_sign_signature_internal MLD_NAMESPACE(signature_internal) +#define crypto_sign_signature MLD_NAMESPACE_K(signature) +#define crypto_sign_signature_extmu MLD_NAMESPACE_K(signature_extmu) +#define crypto_sign MLD_NAMESPACE_K(sign) +#define crypto_sign_verify_internal MLD_NAMESPACE_K(verify_internal) +#define crypto_sign_verify MLD_NAMESPACE_K(verify) +#define crypto_sign_verify_extmu MLD_NAMESPACE_K(verify_extmu) +#define crypto_sign_open MLD_NAMESPACE_K(open) + /************************************************* * Name: crypto_sign_keypair_internal * @@ -43,7 +53,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_keypair MLD_NAMESPACE(keypair) /************************************************* * Name: crypto_sign_keypair * @@ -69,7 +78,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_signature_internal MLD_NAMESPACE(signature_internal) /************************************************* * Name: crypto_sign_signature_internal * @@ -115,7 +123,6 @@ __contract__( (return_value == -1 && *siglen == 0)) ); -#define crypto_sign_signature MLD_NAMESPACE(signature) /************************************************* * Name: crypto_sign_signature * @@ -150,7 +157,6 @@ __contract__( (return_value == -1 && *siglen == 0)) ); -#define crypto_sign_signature_extmu MLD_NAMESPACE(signature_extmu) /************************************************* * Name: crypto_sign_signature_extmu * @@ -180,7 +186,6 @@ __contract__( (return_value == -1 && *siglen == 0)) ); -#define crypto_sign MLD_NAMESPACETOP /************************************************* * Name: crypto_sign * @@ -215,7 +220,6 @@ __contract__( (return_value == -1)) ); -#define crypto_sign_verify_internal MLD_NAMESPACE(verify_internal) /************************************************* * Name: crypto_sign_verify_internal * @@ -246,7 +250,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_verify MLD_NAMESPACE(verify) /************************************************* * Name: crypto_sign_verify * @@ -276,7 +279,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_verify_extmu MLD_NAMESPACE(verify_extmu) /************************************************* * Name: crypto_sign_verify_extmu * @@ -301,7 +303,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_open MLD_NAMESPACE(open) /************************************************* * Name: crypto_sign_open * diff --git a/test/acvp_mldsa.c b/test/acvp_mldsa.c index 29eb696d..86e66cc4 100644 --- a/test/acvp_mldsa.c +++ b/test/acvp_mldsa.c @@ -7,6 +7,7 @@ #include #include +#include "../mldsa/api.h" #include "../mldsa/sign.h" #define USAGE "acvp_mldsa{lvl} [keyGen|sigGen|sigVer] {test specific arguments}" diff --git a/test/gen_KAT.c b/test/gen_KAT.c index f57ca9c0..d75640a1 100644 --- a/test/gen_KAT.c +++ b/test/gen_KAT.c @@ -6,6 +6,7 @@ #include #include #include +#include "../mldsa/api.h" #include "../mldsa/fips202/fips202.h" #include "../mldsa/sign.h" #include "../mldsa/sys.h" diff --git a/test/mk/auto.mk b/test/mk/auto.mk index aa2f0750..65a3dd4a 100644 --- a/test/mk/auto.mk +++ b/test/mk/auto.mk @@ -1,38 +1,115 @@ # Copyright (c) The mlkem-native project authors # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +# +# Automatically detect system architecture and set preprocessor flags accordingly +# This file detects host CPU capabilities and combines them with compiler support +# to enable optimal compilation flags. -# Automatically detect system architecture and set preprocessor etc accordingly +ifndef _AUTO_MK +_AUTO_MK := + +# Helper function to check if host CPU supports a feature +# Usage: $(call check_host_feature,feature_pattern,source_command) +define check_host_feature +$(shell $(2) 2>/dev/null | grep -q "$(1)" && echo 1 || echo 0) +endef + +# x86_64 architecture detection +ifeq ($(ARCH),x86_64) + +# Host CPU feature detection for x86_64 ifeq ($(HOST_PLATFORM),Linux-x86_64) -ifeq ($(CROSS_PREFIX),) - CFLAGS += -mavx2 -mbmi2 -mpopcnt -maes - CFLAGS += -DMLD_FORCE_X86_64 -else ifneq ($(findstring aarch64_be, $(CROSS_PREFIX)),) - CFLAGS += -DMLD_FORCE_AARCH64_EB -else ifneq ($(findstring aarch64, $(CROSS_PREFIX)),) - CFLAGS += -DMLD_FORCE_AARCH64 +# Linux: Use /proc/cpuinfo +MLD_HOST_SUPPORTS_AVX2 := $(call check_host_feature,avx2,cat /proc/cpuinfo) +MLD_HOST_SUPPORTS_SSE2 := $(call check_host_feature,sse2,cat /proc/cpuinfo) +MLD_HOST_SUPPORTS_BMI2 := $(call check_host_feature,bmi2,cat /proc/cpuinfo) +else ifeq ($(HOST_PLATFORM),Darwin-x86_64) +# macOS: Use sysctl +MLD_HOST_SUPPORTS_AVX2 := $(call check_host_feature,AVX2,sysctl -n machdep.cpu.leaf7_features) +MLD_HOST_SUPPORTS_SSE2 := $(call check_host_feature,SSE2,sysctl -n machdep.cpu.features) +MLD_HOST_SUPPORTS_BMI2 := $(call check_host_feature,BMI2,sysctl -n machdep.cpu.leaf7_features) +else ifneq ($(CROSS_PREFIX),) +# Cross-compilation: assume all features are supported +MLD_HOST_SUPPORTS_AVX2 := 1 +MLD_HOST_SUPPORTS_SSE2 := 1 +MLD_HOST_SUPPORTS_BMI2 := 1 else +# Other platforms: assume no support +MLD_HOST_SUPPORTS_AVX2 := 0 +MLD_HOST_SUPPORTS_SSE2 := 0 +MLD_HOST_SUPPORTS_BMI2 := 0 +endif # HOST_PLATFORM x86_64 -endif +endif # x86_64 -# linux aarch64 -else ifeq ($(HOST_PLATFORM),Linux-aarch64) -ifeq ($(CROSS_PREFIX),) - CFLAGS += -DMLD_FORCE_AARCH64 -else ifneq ($(findstring x86_64, $(CROSS_PREFIX)),) - CFLAGS += -mavx2 -mbmi2 -mpopcnt -maes - CFLAGS += -DMLD_FORCE_X86_64 -else -endif +# AArch64 architecture detection +ifeq ($(ARCH),aarch64) -# darwin aarch64 +# Host CPU feature detection for AArch64 +ifeq ($(HOST_PLATFORM),Linux-aarch64) +# Linux: Use /proc/cpuinfo (look for sha3 in Features line) +MLD_HOST_SUPPORTS_SHA3 := $(call check_host_feature,sha3,cat /proc/cpuinfo) else ifeq ($(HOST_PLATFORM),Darwin-arm64) -ifeq ($(CROSS_PREFIX),) - CFLAGS += -DMLD_FORCE_AARCH64 -else ifneq ($(findstring x86_64, $(CROSS_PREFIX)),) - CFLAGS += -DMLD_FORCE_X86_64 -else ifneq ($(findstring aarch64, $(CROSS_PREFIX)),) - CFLAGS += -DMLD_FORCE_AARCH64 +# macOS: Use sysctl to check for SHA3 support +MLD_HOST_SUPPORTS_SHA3 := $(call check_host_feature,1,sysctl -n hw.optional.armv8_2_sha3) +else ifneq ($(CROSS_PREFIX),) +# Cross-compilation: assume all features are supported +MLD_HOST_SUPPORTS_SHA3 := 1 else +# Other platforms: assume no support +MLD_HOST_SUPPORTS_SHA3 := 0 +endif # HOST_PLATFORM aarch64 + +endif # aarch64 + +# Only apply CFLAGS modifications if AUTO=1 +ifeq ($(AUTO),1) + +# x86_64 CFLAGS configuration +ifeq ($(ARCH),x86_64) +CFLAGS += -DMLD_FORCE_X86_64 + +# Add flags only if both compiler and host support the feature +ifeq ($(MLD_COMPILER_SUPPORTS_AVX2)$(MLD_HOST_SUPPORTS_AVX2),11) +CFLAGS += -mavx2 endif + +ifeq ($(MLD_COMPILER_SUPPORTS_BMI2)$(MLD_HOST_SUPPORTS_BMI2),11) +CFLAGS += -mbmi2 endif +endif # x86_64 + +# AArch64 CFLAGS configuration +ifeq ($(ARCH),aarch64) +CFLAGS += -DMLD_FORCE_AARCH64 + +# Add SHA3 flags only if both compiler and host support it +ifeq ($(MLD_COMPILER_SUPPORTS_SHA3)$(MLD_HOST_SUPPORTS_SHA3),11) +CFLAGS += -march=armv8.4-a+sha3 +endif +endif # aarch64 + +# AArch64 Big Endian CFLAGS configuration +ifeq ($(ARCH),aarch64_be) +CFLAGS += -DMLD_FORCE_AARCH64_EB +endif # aarch64_be + +# RISC-V 64-bit CFLAGS configuration +ifeq ($(ARCH),riscv64) +CFLAGS += -DMLD_FORCE_RISCV64 +endif # riscv64 + +# RISC-V 32-bit CFLAGS configuration +ifeq ($(ARCH),riscv32) +CFLAGS += -DMLD_FORCE_RISCV32 +endif # riscv32 + +# PowerPC 64-bit Little Endian CFLAGS configuration +ifeq ($(ARCH),powerpc64le) +CFLAGS += -DMLD_FORCE_PPC64LE +endif # powerpc64le + +endif # AUTO=1 + +endif # _AUTO_MK diff --git a/test/mk/compiler.mk b/test/mk/compiler.mk new file mode 100644 index 00000000..6c410b2c --- /dev/null +++ b/test/mk/compiler.mk @@ -0,0 +1,66 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +# +# Compiler feature detection for mldsa-native +# This file detects whether the compiler supports various architectural features +# used by mldsa-native through compile-time tests with C code containing inline assembly. +# +# Feature detection can be overridden by setting the corresponding variable on the command line: +# make MLD_COMPILER_SUPPORTS_SHA3=0 # Disable SHA3 detection +# make MLD_COMPILER_SUPPORTS_AVX2=0 # Disable AVX2 detection +# make MLD_COMPILER_SUPPORTS_BMI2=0 # Disable BMI2 detection +# make MLD_COMPILER_SUPPORTS_SSE2=0 # Disable SSE2 detection + +ifndef _COMPILER_MK +_COMPILER_MK := + +# Normalize architecture names +ARCH := $(shell uname -m) +ifeq ($(ARCH),arm64) +ARCH := aarch64 +endif + +# Override ARCH for cross-compilation based on CROSS_PREFIX +ifneq ($(CROSS_PREFIX),) +ifneq ($(findstring x86_64, $(CROSS_PREFIX)),) +ARCH := x86_64 +else ifneq ($(findstring aarch64_be, $(CROSS_PREFIX)),) +ARCH := aarch64_be +else ifneq ($(findstring aarch64, $(CROSS_PREFIX)),) +ARCH := aarch64 +else ifneq ($(findstring riscv64, $(CROSS_PREFIX)),) +ARCH := riscv64 +else ifneq ($(findstring riscv32, $(CROSS_PREFIX)),) +ARCH := riscv32 +else ifneq ($(findstring powerpc64le, $(CROSS_PREFIX)),) +ARCH := powerpc64le +endif +endif # CROSS_PREFIX + +# x86_64 feature detection +ifeq ($(ARCH),x86_64) + +# Test AVX2 support using C with inline assembly +# Can be overridden by setting MLD_COMPILER_SUPPORTS_AVX2=0/1 on command line +MLD_COMPILER_SUPPORTS_AVX2 ?= $(shell echo 'int main() { __asm__("vpxor %%ymm0, %%ymm1, %%ymm2" ::: "ymm0", "ymm1", "ymm2"); return 0; }' | $(CC) -mavx2 -x c - -c -o /dev/null 2>/dev/null && echo 1 || echo 0) + +# Test SSE2 support using C with inline assembly +# Can be overridden by setting MLD_COMPILER_SUPPORTS_SSE2=0/1 on command line +MLD_COMPILER_SUPPORTS_SSE2 ?= $(shell echo 'int main() { __asm__("pxor %%xmm0, %%xmm1" ::: "xmm0", "xmm1"); return 0; }' | $(CC) -msse2 -x c - -c -o /dev/null 2>/dev/null && echo 1 || echo 0) + +# Test BMI2 support using C with inline assembly +# Can be overridden by setting MLD_COMPILER_SUPPORTS_BMI2=0/1 on command line +MLD_COMPILER_SUPPORTS_BMI2 ?= $(shell echo 'int main() { __asm__("pdep %%eax, %%ebx, %%ecx" ::: "eax", "ebx", "ecx"); return 0; }' | $(CC) -mbmi2 -x c - -c -o /dev/null 2>/dev/null && echo 1 || echo 0) + +endif # x86_64 + +# AArch64 feature detection +ifeq ($(ARCH),aarch64) + +# Test SHA3 support (Armv8.4-a+SHA3) using C with inline assembly +# Can be overridden by setting MLD_COMPILER_SUPPORTS_SHA3=0/1 on command line +MLD_COMPILER_SUPPORTS_SHA3 ?= $(shell echo 'int main() { __asm__("eor3 v0.16b, v1.16b, v2.16b, v3.16b" ::: "v0", "v1", "v2", "v3"); return 0; }' | $(CC) -march=armv8.4-a+sha3 -x c - -c -o /dev/null 2>/dev/null && echo 1 || echo 0) + +endif # aarch64 + +endif # _COMPILER_MK From e5995286e1d0c1039dfdd9a8e06f36717e081804 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 13:26:59 -0700 Subject: [PATCH 02/18] Update CMBC proof files Signed-off-by: Jake Massimo --- proofs/cbmc/Makefile.common | 2 + proofs/cbmc/Makefile_params.common | 16 ++++---- proofs/cbmc/check_pct/Makefile | 2 +- proofs/cbmc/check_pct/check_pct_harness.c | 1 + proofs/cbmc/crypto_sign/Makefile | 4 +- proofs/cbmc/crypto_sign/crypto_sign_harness.c | 1 + proofs/cbmc/crypto_sign_keypair/Makefile | 6 +-- .../crypto_sign_keypair_harness.c | 1 + .../crypto_sign_keypair_internal/Makefile | 24 ++++++------ .../crypto_sign_keypair_internal_harness.c | 1 + proofs/cbmc/crypto_sign_open/Makefile | 6 +-- .../crypto_sign_open_harness.c | 1 + proofs/cbmc/crypto_sign_signature/Makefile | 6 +-- .../crypto_sign_signature_harness.c | 1 + .../cbmc/crypto_sign_signature_extmu/Makefile | 6 +-- .../crypto_sign_signature_extmu_harness.c | 1 + .../crypto_sign_signature_internal/Makefile | 12 +++--- .../crypto_sign_signature_internal_harness.c | 1 + proofs/cbmc/crypto_sign_verify/Makefile | 6 +-- .../crypto_sign_verify_harness.c | 1 + proofs/cbmc/crypto_sign_verify_extmu/Makefile | 6 +-- .../crypto_sign_verify_extmu_harness.c | 3 +- .../cbmc/crypto_sign_verify_internal/Makefile | 38 +++++++++---------- .../crypto_sign_verify_internal_harness.c | 1 + proofs/cbmc/invntt_tomont/Makefile | 4 +- proofs/cbmc/mld_h/mld_h_harness.c | 1 + proofs/cbmc/mld_sample_s1_s2/Makefile | 2 +- .../mld_sample_s1_s2_harness.c | 1 + proofs/cbmc/ntt/Makefile | 4 +- proofs/cbmc/pack_pk/Makefile | 6 +-- proofs/cbmc/pack_sig/Makefile | 6 +-- proofs/cbmc/pack_sk/Makefile | 6 +-- proofs/cbmc/poly_add/Makefile | 4 +- proofs/cbmc/poly_caddq/Makefile | 4 +- proofs/cbmc/poly_challenge/Makefile | 4 +- proofs/cbmc/poly_chknorm/Makefile | 4 +- proofs/cbmc/poly_decompose/Makefile | 4 +- proofs/cbmc/poly_invntt_tomont/Makefile | 6 +-- proofs/cbmc/poly_make_hint/Makefile | 4 +- proofs/cbmc/poly_ntt/Makefile | 6 +-- .../cbmc/poly_pointwise_montgomery/Makefile | 4 +- proofs/cbmc/poly_power2round/Makefile | 4 +- proofs/cbmc/poly_reduce/Makefile | 4 +- proofs/cbmc/poly_shiftl/Makefile | 4 +- proofs/cbmc/poly_sub/Makefile | 4 +- proofs/cbmc/poly_uniform/Makefile | 4 +- proofs/cbmc/poly_uniform_4x/Makefile | 4 +- proofs/cbmc/poly_uniform_eta_4x/Makefile | 4 +- proofs/cbmc/poly_uniform_gamma1/Makefile | 6 +-- proofs/cbmc/poly_uniform_gamma1_4x/Makefile | 6 +-- proofs/cbmc/poly_use_hint/Makefile | 4 +- proofs/cbmc/polyeta_pack/Makefile | 4 +- proofs/cbmc/polyeta_unpack/Makefile | 4 +- proofs/cbmc/polyt0_pack/Makefile | 4 +- proofs/cbmc/polyt0_unpack/Makefile | 4 +- proofs/cbmc/polyt1_pack/Makefile | 4 +- proofs/cbmc/polyt1_unpack/Makefile | 4 +- proofs/cbmc/polyvec_matrix_expand/Makefile | 6 +-- .../Makefile | 6 +-- proofs/cbmc/polyveck_add/Makefile | 6 +-- proofs/cbmc/polyveck_caddq/Makefile | 6 +-- proofs/cbmc/polyveck_chknorm/Makefile | 6 +-- proofs/cbmc/polyveck_decompose/Makefile | 6 +-- proofs/cbmc/polyveck_invntt_tomont/Makefile | 6 +-- proofs/cbmc/polyveck_make_hint/Makefile | 6 +-- proofs/cbmc/polyveck_ntt/Makefile | 6 +-- proofs/cbmc/polyveck_pack_eta/Makefile | 6 +-- proofs/cbmc/polyveck_pack_t0/Makefile | 6 +-- proofs/cbmc/polyveck_pack_w1/Makefile | 6 +-- .../Makefile | 6 +-- proofs/cbmc/polyveck_power2round/Makefile | 6 +-- proofs/cbmc/polyveck_reduce/Makefile | 6 +-- proofs/cbmc/polyveck_shiftl/Makefile | 6 +-- proofs/cbmc/polyveck_sub/Makefile | 6 +-- proofs/cbmc/polyveck_unpack_eta/Makefile | 8 ++-- proofs/cbmc/polyveck_unpack_t0/Makefile | 8 ++-- proofs/cbmc/polyveck_use_hint/Makefile | 6 +-- proofs/cbmc/polyvecl_add/Makefile | 6 +-- proofs/cbmc/polyvecl_chknorm/Makefile | 6 +-- proofs/cbmc/polyvecl_invntt_tomont/Makefile | 6 +-- proofs/cbmc/polyvecl_ntt/Makefile | 6 +-- proofs/cbmc/polyvecl_pack_eta/Makefile | 6 +-- proofs/cbmc/polyvecl_pack_z/Makefile | 6 +-- .../Makefile | 4 +- .../Makefile | 6 +-- proofs/cbmc/polyvecl_reduce/Makefile | 6 +-- proofs/cbmc/polyvecl_uniform_gamma1/Makefile | 8 ++-- proofs/cbmc/polyvecl_unpack_eta/Makefile | 8 ++-- proofs/cbmc/polyvecl_unpack_z/Makefile | 8 ++-- proofs/cbmc/polyw1_pack/Makefile | 4 +- proofs/cbmc/polyz_pack/Makefile | 4 +- proofs/cbmc/polyz_unpack/Makefile | 4 +- proofs/cbmc/unpack_pk/Makefile | 8 ++-- proofs/cbmc/unpack_sig/Makefile | 6 +-- proofs/cbmc/unpack_sk/Makefile | 6 +-- 95 files changed, 266 insertions(+), 251 deletions(-) diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common index 2e531548..157fe2ed 100644 --- a/proofs/cbmc/Makefile.common +++ b/proofs/cbmc/Makefile.common @@ -536,6 +536,8 @@ ifndef MLDSA_MODE endif DEFINES += -DMLDSA_MODE=$(MLDSA_MODE) +DEFINES += -DMLD_CONFIG_NAMESPACE_PREFIX=mld +DEFINES += -DMLD_CONFIG_PARAMETER_SET=$(MLD_CONFIG_PARAMETER_SET) # Give visibility to all static functions DEFINES += -Dstatic= diff --git a/proofs/cbmc/Makefile_params.common b/proofs/cbmc/Makefile_params.common index c5ce40a4..3f8817e1 100644 --- a/proofs/cbmc/Makefile_params.common +++ b/proofs/cbmc/Makefile_params.common @@ -6,17 +6,19 @@ ifndef MLDSA_MODE endif MLDSA_MODE ?= 3 -FIPS202_NAMESPACE = mldsa_fips202_ref_ ifeq ($(MLDSA_MODE),2) - MLD_NAMESPACETOP=MLD_44_ref - MLD_NAMESPACE=MLD_44_ref_ + MLD_CONFIG_PARAMETER_SET=44 else ifeq ($(MLDSA_MODE),3) - MLD_NAMESPACETOP=MLD_65_ref - MLD_NAMESPACE=MLD_65_ref_ + MLD_CONFIG_PARAMETER_SET=65 else ifeq ($(MLDSA_MODE),5) - MLD_NAMESPACETOP=MLD_87_ref - MLD_NAMESPACE=MLD_87_ref_ + MLD_CONFIG_PARAMETER_SET=87 else $(error Invalid value of MLDSA_MODE) endif + +# Add parameter set configuration to build +DEFINES += -DMLD_CONFIG_PARAMETER_SET=$(MLD_CONFIG_PARAMETER_SET) + +# FIPS202 namespace for CBMC proofs +FIPS202_NAMESPACE = mldsa_fips202_ref_ diff --git a/proofs/cbmc/check_pct/Makefile b/proofs/cbmc/check_pct/Makefile index c56e168d..17223043 100644 --- a/proofs/cbmc/check_pct/Makefile +++ b/proofs/cbmc/check_pct/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c CHECK_FUNCTION_CONTRACTS=mld_check_pct -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature $(MLD_NAMESPACE)verify +USE_FUNCTION_CONTRACTS=mld_signature mld_verify USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/check_pct/check_pct_harness.c b/proofs/cbmc/check_pct/check_pct_harness.c index 8d3af4e4..5db988d4 100644 --- a/proofs/cbmc/check_pct/check_pct_harness.c +++ b/proofs/cbmc/check_pct/check_pct_harness.c @@ -2,6 +2,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: MIT-0 +#include "api.h" #include "sign.h" int mld_check_pct(uint8_t const pk[CRYPTO_PUBLICKEYBYTES], diff --git a/proofs/cbmc/crypto_sign/Makefile b/proofs/cbmc/crypto_sign/Makefile index dd9e2c32..21468495 100644 --- a/proofs/cbmc/crypto_sign/Makefile +++ b/proofs/cbmc/crypto_sign/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACETOP) -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature +USE_FUNCTION_CONTRACTS=mld_signature APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -30,7 +30,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign +FUNCTION_NAME = mld_crypto_sign # 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_sign/crypto_sign_harness.c b/proofs/cbmc/crypto_sign/crypto_sign_harness.c index 96593905..6d731236 100644 --- a/proofs/cbmc/crypto_sign/crypto_sign_harness.c +++ b/proofs/cbmc/crypto_sign/crypto_sign_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/crypto_sign_keypair/Makefile b/proofs/cbmc/crypto_sign_keypair/Makefile index b52622c7..2c267d63 100644 --- a/proofs/cbmc/crypto_sign_keypair/Makefile +++ b/proofs/cbmc/crypto_sign_keypair/Makefile @@ -19,9 +19,9 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)keypair +CHECK_FUNCTION_CONTRACTS=mld_keypair USE_FUNCTION_CONTRACTS=randombytes -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)keypair_internal +USE_FUNCTION_CONTRACTS+=mld_keypair_internal USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on @@ -32,7 +32,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign_keypair +FUNCTION_NAME = mld_crypto_sign_keypair # 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_sign_keypair/crypto_sign_keypair_harness.c b/proofs/cbmc/crypto_sign_keypair/crypto_sign_keypair_harness.c index 571f1abe..b824b715 100644 --- a/proofs/cbmc/crypto_sign_keypair/crypto_sign_keypair_harness.c +++ b/proofs/cbmc/crypto_sign_keypair/crypto_sign_keypair_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/crypto_sign_keypair_internal/Makefile b/proofs/cbmc/crypto_sign_keypair_internal/Makefile index f54e7637..2d3fc350 100644 --- a/proofs/cbmc/crypto_sign_keypair_internal/Makefile +++ b/proofs/cbmc/crypto_sign_keypair_internal/Makefile @@ -19,19 +19,19 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)keypair_internal +CHECK_FUNCTION_CONTRACTS=mld_keypair_internal USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256 -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_expand +USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_expand USE_FUNCTION_CONTRACTS+=mld_sample_s1_s2 -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_ntt -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_reduce -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_invntt_tomont -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_add -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_power2round -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_pk -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_sk +USE_FUNCTION_CONTRACTS+=mld_polyvecl_ntt +USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_pointwise_montgomery +USE_FUNCTION_CONTRACTS+=mld_polyveck_reduce +USE_FUNCTION_CONTRACTS+=mld_polyveck_invntt_tomont +USE_FUNCTION_CONTRACTS+=mld_polyveck_add +USE_FUNCTION_CONTRACTS+=mld_polyveck_caddq +USE_FUNCTION_CONTRACTS+=mld_polyveck_power2round +USE_FUNCTION_CONTRACTS+=mld_pack_pk +USE_FUNCTION_CONTRACTS+=mld_pack_sk USE_FUNCTION_CONTRACTS+=mld_zeroize USE_FUNCTION_CONTRACTS+=mld_check_pct @@ -43,7 +43,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign_keypair_internal +FUNCTION_NAME = mld_crypto_sign_keypair_internal # 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_sign_keypair_internal/crypto_sign_keypair_internal_harness.c b/proofs/cbmc/crypto_sign_keypair_internal/crypto_sign_keypair_internal_harness.c index e36c7ae4..09f70230 100644 --- a/proofs/cbmc/crypto_sign_keypair_internal/crypto_sign_keypair_internal_harness.c +++ b/proofs/cbmc/crypto_sign_keypair_internal/crypto_sign_keypair_internal_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/crypto_sign_open/Makefile b/proofs/cbmc/crypto_sign_open/Makefile index ee5544fa..ac61f3d9 100644 --- a/proofs/cbmc/crypto_sign_open/Makefile +++ b/proofs/cbmc/crypto_sign_open/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)open -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify +CHECK_FUNCTION_CONTRACTS=mld_open +USE_FUNCTION_CONTRACTS=mld_verify APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -30,7 +30,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign_open +FUNCTION_NAME = mld_crypto_sign_open # 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_sign_open/crypto_sign_open_harness.c b/proofs/cbmc/crypto_sign_open/crypto_sign_open_harness.c index 3f21957f..c464baaa 100644 --- a/proofs/cbmc/crypto_sign_open/crypto_sign_open_harness.c +++ b/proofs/cbmc/crypto_sign_open/crypto_sign_open_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/crypto_sign_signature/Makefile b/proofs/cbmc/crypto_sign_signature/Makefile index e9779cd1..c14befff 100644 --- a/proofs/cbmc/crypto_sign_signature/Makefile +++ b/proofs/cbmc/crypto_sign_signature/Makefile @@ -19,9 +19,9 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature +CHECK_FUNCTION_CONTRACTS=mld_signature USE_FUNCTION_CONTRACTS=mld_randombytes \ - $(MLD_NAMESPACE)signature_internal + mld_signature_internal APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -31,7 +31,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign_signature +FUNCTION_NAME = mld_crypto_sign_signature # 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_sign_signature/crypto_sign_signature_harness.c b/proofs/cbmc/crypto_sign_signature/crypto_sign_signature_harness.c index 545226e0..63026ae8 100644 --- a/proofs/cbmc/crypto_sign_signature/crypto_sign_signature_harness.c +++ b/proofs/cbmc/crypto_sign_signature/crypto_sign_signature_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/crypto_sign_signature_extmu/Makefile b/proofs/cbmc/crypto_sign_signature_extmu/Makefile index c31c1b19..d37cd2ae 100644 --- a/proofs/cbmc/crypto_sign_signature_extmu/Makefile +++ b/proofs/cbmc/crypto_sign_signature_extmu/Makefile @@ -19,9 +19,9 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_extmu +CHECK_FUNCTION_CONTRACTS=mld_signature_extmu USE_FUNCTION_CONTRACTS=mld_randombytes \ - $(MLD_NAMESPACE)signature_internal + mld_signature_internal APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -31,7 +31,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign_signature_extmu +FUNCTION_NAME = mld_crypto_sign_signature_extmu # 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_sign_signature_extmu/crypto_sign_signature_extmu_harness.c b/proofs/cbmc/crypto_sign_signature_extmu/crypto_sign_signature_extmu_harness.c index 3e8b164c..a69288ef 100644 --- a/proofs/cbmc/crypto_sign_signature_extmu/crypto_sign_signature_extmu_harness.c +++ b/proofs/cbmc/crypto_sign_signature_extmu/crypto_sign_signature_extmu_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/crypto_sign_signature_internal/Makefile b/proofs/cbmc/crypto_sign_signature_internal/Makefile index d7610765..78f23c11 100644 --- a/proofs/cbmc/crypto_sign_signature_internal/Makefile +++ b/proofs/cbmc/crypto_sign_signature_internal/Makefile @@ -19,12 +19,12 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_internal -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sk \ +CHECK_FUNCTION_CONTRACTS=mld_signature_internal +USE_FUNCTION_CONTRACTS=mld_unpack_sk \ mld_H \ - $(MLD_NAMESPACE)polyvec_matrix_expand \ - $(MLD_NAMESPACE)polyvecl_ntt \ - $(MLD_NAMESPACE)polyveck_ntt \ + mld_polyvec_matrix_expand \ + mld_polyvecl_ntt \ + mld_polyveck_ntt \ mld_attempt_signature_generation USE_FUNCTION_CONTRACTS+=mld_zeroize @@ -37,7 +37,7 @@ CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula CBMCFLAGS += --no-array-field-sensitivity -FUNCTION_NAME = crypto_sign_signature_internal +FUNCTION_NAME = mld_crypto_sign_signature_internal # 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_sign_signature_internal/crypto_sign_signature_internal_harness.c b/proofs/cbmc/crypto_sign_signature_internal/crypto_sign_signature_internal_harness.c index 8115f3b0..b8f6a2f7 100644 --- a/proofs/cbmc/crypto_sign_signature_internal/crypto_sign_signature_internal_harness.c +++ b/proofs/cbmc/crypto_sign_signature_internal/crypto_sign_signature_internal_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/crypto_sign_verify/Makefile b/proofs/cbmc/crypto_sign_verify/Makefile index 3ce46884..3b79283c 100644 --- a/proofs/cbmc/crypto_sign_verify/Makefile +++ b/proofs/cbmc/crypto_sign_verify/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal +CHECK_FUNCTION_CONTRACTS=mld_verify +USE_FUNCTION_CONTRACTS=mld_verify_internal USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on @@ -31,7 +31,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign_verify +FUNCTION_NAME = mld_crypto_sign_verify # 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_sign_verify/crypto_sign_verify_harness.c b/proofs/cbmc/crypto_sign_verify/crypto_sign_verify_harness.c index ddf10a0e..d6551eb1 100644 --- a/proofs/cbmc/crypto_sign_verify/crypto_sign_verify_harness.c +++ b/proofs/cbmc/crypto_sign_verify/crypto_sign_verify_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/crypto_sign_verify_extmu/Makefile b/proofs/cbmc/crypto_sign_verify_extmu/Makefile index 4b57aa8c..64283a5b 100644 --- a/proofs/cbmc/crypto_sign_verify_extmu/Makefile +++ b/proofs/cbmc/crypto_sign_verify_extmu/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_extmu -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal +CHECK_FUNCTION_CONTRACTS=mld_verify_extmu +USE_FUNCTION_CONTRACTS=mld_verify_internal APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -30,7 +30,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign_verify_extmu +FUNCTION_NAME = mld_crypto_sign_verify_extmu # 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_sign_verify_extmu/crypto_sign_verify_extmu_harness.c b/proofs/cbmc/crypto_sign_verify_extmu/crypto_sign_verify_extmu_harness.c index 5e80390f..463bdcac 100644 --- a/proofs/cbmc/crypto_sign_verify_extmu/crypto_sign_verify_extmu_harness.c +++ b/proofs/cbmc/crypto_sign_verify_extmu/crypto_sign_verify_extmu_harness.c @@ -1,10 +1,9 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" - - void harness(void) { uint8_t *sig; diff --git a/proofs/cbmc/crypto_sign_verify_internal/Makefile b/proofs/cbmc/crypto_sign_verify_internal/Makefile index 46fedfb7..7f0a22cf 100644 --- a/proofs/cbmc/crypto_sign_verify_internal/Makefile +++ b/proofs/cbmc/crypto_sign_verify_internal/Makefile @@ -19,25 +19,25 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_pk -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)unpack_sig -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_chknorm +CHECK_FUNCTION_CONTRACTS=mld_verify_internal +USE_FUNCTION_CONTRACTS=mld_unpack_pk +USE_FUNCTION_CONTRACTS+=mld_unpack_sig +USE_FUNCTION_CONTRACTS+=mld_polyvecl_chknorm USE_FUNCTION_CONTRACTS+=mld_H -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_challenge -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_expand -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_ntt -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_ntt -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_shiftl -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_ntt -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_pointwise_poly_montgomery -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_sub -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_reduce -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_invntt_tomont -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_use_hint -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_pack_w1 +USE_FUNCTION_CONTRACTS+=mld_poly_challenge +USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_expand +USE_FUNCTION_CONTRACTS+=mld_polyvecl_ntt +USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_pointwise_montgomery +USE_FUNCTION_CONTRACTS+=mld_poly_ntt +USE_FUNCTION_CONTRACTS+=mld_polyveck_shiftl +USE_FUNCTION_CONTRACTS+=mld_polyveck_ntt +USE_FUNCTION_CONTRACTS+=mld_polyveck_pointwise_poly_montgomery +USE_FUNCTION_CONTRACTS+=mld_polyveck_sub +USE_FUNCTION_CONTRACTS+=mld_polyveck_reduce +USE_FUNCTION_CONTRACTS+=mld_polyveck_invntt_tomont +USE_FUNCTION_CONTRACTS+=mld_polyveck_caddq +USE_FUNCTION_CONTRACTS+=mld_polyveck_use_hint +USE_FUNCTION_CONTRACTS+=mld_polyveck_pack_w1 USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on @@ -48,7 +48,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = crypto_sign_verify_internal +FUNCTION_NAME = mld_crypto_sign_verify_internal # 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_sign_verify_internal/crypto_sign_verify_internal_harness.c b/proofs/cbmc/crypto_sign_verify_internal/crypto_sign_verify_internal_harness.c index 186cc1bc..3ec8836f 100644 --- a/proofs/cbmc/crypto_sign_verify_internal/crypto_sign_verify_internal_harness.c +++ b/proofs/cbmc/crypto_sign_verify_internal/crypto_sign_verify_internal_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void harness(void) diff --git a/proofs/cbmc/invntt_tomont/Makefile b/proofs/cbmc/invntt_tomont/Makefile index 0e86bc56..9a2c6548 100644 --- a/proofs/cbmc/invntt_tomont/Makefile +++ b/proofs/cbmc/invntt_tomont/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/ntt.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)invntt_tomont +CHECK_FUNCTION_CONTRACTS=mld_invntt_tomont USE_FUNCTION_CONTRACTS=mld_invntt_layer mld_fqscale APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = invntt_tomont +FUNCTION_NAME = mld_invntt_tomont # 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/mld_h/mld_h_harness.c b/proofs/cbmc/mld_h/mld_h_harness.c index 8cbbb48a..8edec32d 100644 --- a/proofs/cbmc/mld_h/mld_h_harness.c +++ b/proofs/cbmc/mld_h/mld_h_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" void mld_H(uint8_t *out, size_t outlen, const uint8_t *in1, size_t in1len, diff --git a/proofs/cbmc/mld_sample_s1_s2/Makefile b/proofs/cbmc/mld_sample_s1_s2/Makefile index b14fc153..6371381e 100644 --- a/proofs/cbmc/mld_sample_s1_s2/Makefile +++ b/proofs/cbmc/mld_sample_s1_s2/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c CHECK_FUNCTION_CONTRACTS=mld_sample_s1_s2 -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta_4x +USE_FUNCTION_CONTRACTS=mld_poly_uniform_eta_4x APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/mld_sample_s1_s2/mld_sample_s1_s2_harness.c b/proofs/cbmc/mld_sample_s1_s2/mld_sample_s1_s2_harness.c index 84a392a0..ed4372e5 100644 --- a/proofs/cbmc/mld_sample_s1_s2/mld_sample_s1_s2_harness.c +++ b/proofs/cbmc/mld_sample_s1_s2/mld_sample_s1_s2_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2, diff --git a/proofs/cbmc/ntt/Makefile b/proofs/cbmc/ntt/Makefile index 345a4a35..d96de164 100644 --- a/proofs/cbmc/ntt/Makefile +++ b/proofs/cbmc/ntt/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/ntt.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)ntt +CHECK_FUNCTION_CONTRACTS=mld_ntt USE_FUNCTION_CONTRACTS=mld_ntt_layer APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = ntt +FUNCTION_NAME = mld_ntt # 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/pack_pk/Makefile b/proofs/cbmc/pack_pk/Makefile index 65d723e3..5e8a9708 100644 --- a/proofs/cbmc/pack_pk/Makefile +++ b/proofs/cbmc/pack_pk/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/packing.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_pk -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyt1_pack +CHECK_FUNCTION_CONTRACTS=mld_pack_pk +USE_FUNCTION_CONTRACTS=mld_polyt1_pack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = pack_pk +FUNCTION_NAME = mld_pack_pk # 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/pack_sig/Makefile b/proofs/cbmc/pack_sig/Makefile index f21e85c2..9e70078a 100644 --- a/proofs/cbmc/pack_sig/Makefile +++ b/proofs/cbmc/pack_sig/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/packing.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sig -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pack_z +CHECK_FUNCTION_CONTRACTS=mld_pack_sig +USE_FUNCTION_CONTRACTS=mld_polyvecl_pack_z APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS+=--slice-formula -FUNCTION_NAME = pack_sig +FUNCTION_NAME = mld_pack_sig # 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/pack_sk/Makefile b/proofs/cbmc/pack_sk/Makefile index 1c7903d9..de3946f1 100644 --- a/proofs/cbmc/pack_sk/Makefile +++ b/proofs/cbmc/pack_sk/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/packing.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sk -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pack_eta $(MLD_NAMESPACE)polyveck_pack_eta $(MLD_NAMESPACE)polyveck_pack_t0 +CHECK_FUNCTION_CONTRACTS=mld_pack_sk +USE_FUNCTION_CONTRACTS=mld_polyvecl_pack_eta mld_polyveck_pack_eta mld_polyveck_pack_t0 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = pack_sk +FUNCTION_NAME = mld_pack_sk # 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_add/Makefile b/proofs/cbmc/poly_add/Makefile index 1f35e231..06fcb44d 100644 --- a/proofs/cbmc/poly_add/Makefile +++ b/proofs/cbmc/poly_add/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_add +CHECK_FUNCTION_CONTRACTS=mld_poly_add USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula -FUNCTION_NAME = poly_add +FUNCTION_NAME = mld_poly_add # 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_caddq/Makefile b/proofs/cbmc/poly_caddq/Makefile index c4f2f2f9..fcc8d706 100644 --- a/proofs/cbmc/poly_caddq/Makefile +++ b/proofs/cbmc/poly_caddq/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_caddq +CHECK_FUNCTION_CONTRACTS=mld_poly_caddq USE_FUNCTION_CONTRACTS=mld_caddq APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_caddq +FUNCTION_NAME = mld_poly_caddq # 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_challenge/Makefile b/proofs/cbmc/poly_challenge/Makefile index 9c9edd0d..a28a130e 100644 --- a/proofs/cbmc/poly_challenge/Makefile +++ b/proofs/cbmc/poly_challenge/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_challenge +CHECK_FUNCTION_CONTRACTS=mld_poly_challenge USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_finalize $(FIPS202_NAMESPACE)shake256_squeezeblocks USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on @@ -30,7 +30,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = poly_challenge +FUNCTION_NAME = mld_poly_challenge # 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_chknorm/Makefile b/proofs/cbmc/poly_chknorm/Makefile index a0544ad2..c44701d8 100644 --- a/proofs/cbmc/poly_chknorm/Makefile +++ b/proofs/cbmc/poly_chknorm/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm +CHECK_FUNCTION_CONTRACTS=mld_poly_chknorm USE_FUNCTION_CONTRACTS=mld_ct_abs_i32 mld_ct_cmask_neg_i32 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_chknorm +FUNCTION_NAME = mld_poly_chknorm # 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_decompose/Makefile b/proofs/cbmc/poly_decompose/Makefile index 5b50ef87..c92bda88 100644 --- a/proofs/cbmc/poly_decompose/Makefile +++ b/proofs/cbmc/poly_decompose/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_decompose +CHECK_FUNCTION_CONTRACTS=mld_poly_decompose USE_FUNCTION_CONTRACTS=mld_decompose APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_decompose +FUNCTION_NAME = mld_poly_decompose # 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_invntt_tomont/Makefile b/proofs/cbmc/poly_invntt_tomont/Makefile index 7d0dcdde..3ee4dc08 100644 --- a/proofs/cbmc/poly_invntt_tomont/Makefile +++ b/proofs/cbmc/poly_invntt_tomont/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_invntt_tomont -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)invntt_tomont +CHECK_FUNCTION_CONTRACTS=mld_poly_invntt_tomont +USE_FUNCTION_CONTRACTS=mld_invntt_tomont APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_invntt_tomont +FUNCTION_NAME = mld_poly_invntt_tomont # 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_make_hint/Makefile b/proofs/cbmc/poly_make_hint/Makefile index 22386569..e9f0926c 100644 --- a/proofs/cbmc/poly_make_hint/Makefile +++ b/proofs/cbmc/poly_make_hint/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_make_hint +CHECK_FUNCTION_CONTRACTS=mld_poly_make_hint USE_FUNCTION_CONTRACTS=mld_make_hint APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_make_hint +FUNCTION_NAME = mld_poly_make_hint # 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_ntt/Makefile b/proofs/cbmc/poly_ntt/Makefile index 5994e40f..8517787f 100644 --- a/proofs/cbmc/poly_ntt/Makefile +++ b/proofs/cbmc/poly_ntt/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_ntt -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)ntt +CHECK_FUNCTION_CONTRACTS=mld_poly_ntt +USE_FUNCTION_CONTRACTS=mld_ntt APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_ntt +FUNCTION_NAME = mld_poly_ntt # 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_pointwise_montgomery/Makefile b/proofs/cbmc/poly_pointwise_montgomery/Makefile index 7740445d..55497dde 100644 --- a/proofs/cbmc/poly_pointwise_montgomery/Makefile +++ b/proofs/cbmc/poly_pointwise_montgomery/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery +CHECK_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery USE_FUNCTION_CONTRACTS=mld_montgomery_reduce APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_pointwise_montgomery +FUNCTION_NAME = mld_poly_pointwise_montgomery # 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_power2round/Makefile b/proofs/cbmc/poly_power2round/Makefile index bc6d9eb0..45570cd1 100644 --- a/proofs/cbmc/poly_power2round/Makefile +++ b/proofs/cbmc/poly_power2round/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_power2round +CHECK_FUNCTION_CONTRACTS=mld_poly_power2round USE_FUNCTION_CONTRACTS=mld_power2round APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_power2round +FUNCTION_NAME = mld_poly_power2round # 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_reduce/Makefile b/proofs/cbmc/poly_reduce/Makefile index f76ce6e8..f0877d3e 100644 --- a/proofs/cbmc/poly_reduce/Makefile +++ b/proofs/cbmc/poly_reduce/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_reduce +CHECK_FUNCTION_CONTRACTS=mld_poly_reduce USE_FUNCTION_CONTRACTS=mld_reduce32 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_reduce +FUNCTION_NAME = mld_poly_reduce # 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_shiftl/Makefile b/proofs/cbmc/poly_shiftl/Makefile index 9948674f..152ddbba 100644 --- a/proofs/cbmc/poly_shiftl/Makefile +++ b/proofs/cbmc/poly_shiftl/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_shiftl +CHECK_FUNCTION_CONTRACTS=mld_poly_shiftl USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_shiftl +FUNCTION_NAME = mld_poly_shiftl # 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_sub/Makefile b/proofs/cbmc/poly_sub/Makefile index e4a2037e..fe252c25 100644 --- a/proofs/cbmc/poly_sub/Makefile +++ b/proofs/cbmc/poly_sub/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_sub +CHECK_FUNCTION_CONTRACTS=mld_poly_sub USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_sub +FUNCTION_NAME = mld_poly_sub # 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_uniform/Makefile b/proofs/cbmc/poly_uniform/Makefile index a22f6bee..7c9a078a 100644 --- a/proofs/cbmc/poly_uniform/Makefile +++ b/proofs/cbmc/poly_uniform/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform +CHECK_FUNCTION_CONTRACTS=mld_poly_uniform USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128_init $(FIPS202_NAMESPACE)shake128_absorb $(FIPS202_NAMESPACE)shake128_finalize $(FIPS202_NAMESPACE)shake128_squeezeblocks mld_rej_uniform USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on @@ -30,7 +30,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = poly_uniform +FUNCTION_NAME = mld_poly_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/poly_uniform_4x/Makefile b/proofs/cbmc/poly_uniform_4x/Makefile index fb0abbb1..93f92efb 100644 --- a/proofs/cbmc/poly_uniform_4x/Makefile +++ b/proofs/cbmc/poly_uniform_4x/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_4x +CHECK_FUNCTION_CONTRACTS=mld_poly_uniform_4x USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake128x4_absorb_once $(FIPS202_NAMESPACE)shake128x4_squeezeblocks mld_rej_uniform USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on @@ -29,7 +29,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_uniform_4x +FUNCTION_NAME = mld_poly_uniform_4x # 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_uniform_eta_4x/Makefile b/proofs/cbmc/poly_uniform_eta_4x/Makefile index c36e03f6..38f26875 100644 --- a/proofs/cbmc/poly_uniform_eta_4x/Makefile +++ b/proofs/cbmc/poly_uniform_eta_4x/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta_4x +CHECK_FUNCTION_CONTRACTS=mld_poly_uniform_eta_4x USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256x4_absorb_once $(FIPS202_NAMESPACE)shake256x4_squeezeblocks mld_rej_eta USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on @@ -29,7 +29,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_uniform_eta_4x +FUNCTION_NAME = mld_poly_uniform_eta_4x # 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_uniform_gamma1/Makefile b/proofs/cbmc/poly_uniform_gamma1/Makefile index 66ca915e..19d0c908 100644 --- a/proofs/cbmc/poly_uniform_gamma1/Makefile +++ b/proofs/cbmc/poly_uniform_gamma1/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_gamma1 -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_finalize $(FIPS202_NAMESPACE)shake256_squeezeblocks $(MLD_NAMESPACE)polyz_unpack +CHECK_FUNCTION_CONTRACTS=mld_poly_uniform_gamma1 +USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_finalize $(FIPS202_NAMESPACE)shake256_squeezeblocks mld_polyz_unpack USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,7 +29,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_uniform_gamma1 +FUNCTION_NAME = mld_poly_uniform_gamma1 # 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_uniform_gamma1_4x/Makefile b/proofs/cbmc/poly_uniform_gamma1_4x/Makefile index e3e497bf..5d9dcff6 100644 --- a/proofs/cbmc/poly_uniform_gamma1_4x/Makefile +++ b/proofs/cbmc/poly_uniform_gamma1_4x/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202x4.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_gamma1_4x -USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256x4_absorb_once $(FIPS202_NAMESPACE)shake256x4_squeezeblocks $(MLD_NAMESPACE)polyz_unpack +CHECK_FUNCTION_CONTRACTS=mld_poly_uniform_gamma1_4x +USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256x4_absorb_once $(FIPS202_NAMESPACE)shake256x4_squeezeblocks mld_polyz_unpack USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -30,7 +30,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = poly_uniform_gamma1_4x +FUNCTION_NAME = mld_poly_uniform_gamma1_4x # 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_use_hint/Makefile b/proofs/cbmc/poly_use_hint/Makefile index 883fefa4..847763f3 100644 --- a/proofs/cbmc/poly_use_hint/Makefile +++ b/proofs/cbmc/poly_use_hint/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_use_hint +CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint USE_FUNCTION_CONTRACTS=mld_use_hint APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = poly_use_hint +FUNCTION_NAME = mld_poly_use_hint # 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/polyeta_pack/Makefile b/proofs/cbmc/polyeta_pack/Makefile index e0341e2a..7aa81d2e 100644 --- a/proofs/cbmc/polyeta_pack/Makefile +++ b/proofs/cbmc/polyeta_pack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_pack +CHECK_FUNCTION_CONTRACTS=mld_polyeta_pack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyeta_pack +FUNCTION_NAME = mld_polyeta_pack # 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/polyeta_unpack/Makefile b/proofs/cbmc/polyeta_unpack/Makefile index 1ed697af..04e5c461 100644 --- a/proofs/cbmc/polyeta_unpack/Makefile +++ b/proofs/cbmc/polyeta_unpack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_unpack +CHECK_FUNCTION_CONTRACTS=mld_polyeta_unpack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyeta_unpack +FUNCTION_NAME = mld_polyeta_unpack # 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/polyt0_pack/Makefile b/proofs/cbmc/polyt0_pack/Makefile index bfe95ba3..40f85b72 100644 --- a/proofs/cbmc/polyt0_pack/Makefile +++ b/proofs/cbmc/polyt0_pack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyt0_pack +CHECK_FUNCTION_CONTRACTS=mld_polyt0_pack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyt0_pack +FUNCTION_NAME = mld_polyt0_pack # 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/polyt0_unpack/Makefile b/proofs/cbmc/polyt0_unpack/Makefile index d44ef77f..62a6cb98 100644 --- a/proofs/cbmc/polyt0_unpack/Makefile +++ b/proofs/cbmc/polyt0_unpack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyt0_unpack +CHECK_FUNCTION_CONTRACTS=mld_polyt0_unpack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyt0_unpack +FUNCTION_NAME = mld_polyt0_unpack # 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/polyt1_pack/Makefile b/proofs/cbmc/polyt1_pack/Makefile index 61048520..647678af 100644 --- a/proofs/cbmc/polyt1_pack/Makefile +++ b/proofs/cbmc/polyt1_pack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyt1_pack +CHECK_FUNCTION_CONTRACTS=mld_polyt1_pack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyt1_pack +FUNCTION_NAME = mld_polyt1_pack # 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/polyt1_unpack/Makefile b/proofs/cbmc/polyt1_unpack/Makefile index cda77280..66a67ad8 100644 --- a/proofs/cbmc/polyt1_unpack/Makefile +++ b/proofs/cbmc/polyt1_unpack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyt1_unpack +CHECK_FUNCTION_CONTRACTS=mld_polyt1_unpack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyt1_unpack +FUNCTION_NAME = mld_polyt1_unpack # 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/polyvec_matrix_expand/Makefile b/proofs/cbmc/polyvec_matrix_expand/Makefile index 83a8248c..77a62bc4 100644 --- a/proofs/cbmc/polyvec_matrix_expand/Makefile +++ b/proofs/cbmc/polyvec_matrix_expand/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvec_matrix_expand -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_4x $(MLD_NAMESPACE)poly_uniform +CHECK_FUNCTION_CONTRACTS=mld_polyvec_matrix_expand +USE_FUNCTION_CONTRACTS=mld_poly_uniform_4x mld_poly_uniform APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula -FUNCTION_NAME = polyvec_matrix_expand +FUNCTION_NAME = mld_polyvec_matrix_expand # 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/polyvec_matrix_pointwise_montgomery/Makefile b/proofs/cbmc/polyvec_matrix_pointwise_montgomery/Makefile index 8e899ee9..e9a4c76a 100644 --- a/proofs/cbmc/polyvec_matrix_pointwise_montgomery/Makefile +++ b/proofs/cbmc/polyvec_matrix_pointwise_montgomery/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_acc_montgomery +CHECK_FUNCTION_CONTRACTS=mld_polyvec_matrix_pointwise_montgomery +USE_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula -FUNCTION_NAME = polyvec_matrix_pointwise_montgomery +FUNCTION_NAME = mld_polyvec_matrix_pointwise_montgomery # 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/polyveck_add/Makefile b/proofs/cbmc/polyveck_add/Makefile index 26ec7945..73a55179 100644 --- a/proofs/cbmc/polyveck_add/Makefile +++ b/proofs/cbmc/polyveck_add/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_add -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_add +CHECK_FUNCTION_CONTRACTS=mld_polyveck_add +USE_FUNCTION_CONTRACTS=mld_poly_add APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula -FUNCTION_NAME = polyveck_add +FUNCTION_NAME = mld_polyveck_add # 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/polyveck_caddq/Makefile b/proofs/cbmc/polyveck_caddq/Makefile index c4b055a4..80dbe6e6 100644 --- a/proofs/cbmc/polyveck_caddq/Makefile +++ b/proofs/cbmc/polyveck_caddq/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_caddq -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_caddq +CHECK_FUNCTION_CONTRACTS=mld_polyveck_caddq +USE_FUNCTION_CONTRACTS=mld_poly_caddq APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_caddq +FUNCTION_NAME = mld_polyveck_caddq # 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/polyveck_chknorm/Makefile b/proofs/cbmc/polyveck_chknorm/Makefile index d15366ed..05f58607 100644 --- a/proofs/cbmc/polyveck_chknorm/Makefile +++ b/proofs/cbmc/polyveck_chknorm/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_chknorm -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm +CHECK_FUNCTION_CONTRACTS=mld_polyveck_chknorm +USE_FUNCTION_CONTRACTS=mld_poly_chknorm APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -30,7 +30,7 @@ CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula CBMCFLAGS += --no-array-field-sensitivity -FUNCTION_NAME = polyveck_chknorm +FUNCTION_NAME = mld_polyveck_chknorm # 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/polyveck_decompose/Makefile b/proofs/cbmc/polyveck_decompose/Makefile index 2014a65c..55213501 100644 --- a/proofs/cbmc/polyveck_decompose/Makefile +++ b/proofs/cbmc/polyveck_decompose/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_decompose -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_decompose +CHECK_FUNCTION_CONTRACTS=mld_polyveck_decompose +USE_FUNCTION_CONTRACTS=mld_poly_decompose APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,7 +29,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = polyveck_decompose +FUNCTION_NAME = mld_polyveck_decompose # 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/polyveck_invntt_tomont/Makefile b/proofs/cbmc/polyveck_invntt_tomont/Makefile index 22b8e566..46edf68c 100644 --- a/proofs/cbmc/polyveck_invntt_tomont/Makefile +++ b/proofs/cbmc/polyveck_invntt_tomont/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_invntt_tomont -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_invntt_tomont +CHECK_FUNCTION_CONTRACTS=mld_polyveck_invntt_tomont +USE_FUNCTION_CONTRACTS=mld_poly_invntt_tomont APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_invntt_tomont +FUNCTION_NAME = mld_polyveck_invntt_tomont # 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/polyveck_make_hint/Makefile b/proofs/cbmc/polyveck_make_hint/Makefile index 8028b0b2..451b71a6 100644 --- a/proofs/cbmc/polyveck_make_hint/Makefile +++ b/proofs/cbmc/polyveck_make_hint/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_make_hint -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_make_hint +CHECK_FUNCTION_CONTRACTS=mld_polyveck_make_hint +USE_FUNCTION_CONTRACTS=mld_poly_make_hint APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --slice-formula -FUNCTION_NAME = polyveck_make_hint +FUNCTION_NAME = mld_polyveck_make_hint # 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/polyveck_ntt/Makefile b/proofs/cbmc/polyveck_ntt/Makefile index c9a0e65e..57bc0602 100644 --- a/proofs/cbmc/polyveck_ntt/Makefile +++ b/proofs/cbmc/polyveck_ntt/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_ntt -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_ntt +CHECK_FUNCTION_CONTRACTS=mld_polyveck_ntt +USE_FUNCTION_CONTRACTS=mld_poly_ntt APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_ntt +FUNCTION_NAME = mld_polyveck_ntt # 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/polyveck_pack_eta/Makefile b/proofs/cbmc/polyveck_pack_eta/Makefile index e8dc00a4..2ae427d5 100644 --- a/proofs/cbmc/polyveck_pack_eta/Makefile +++ b/proofs/cbmc/polyveck_pack_eta/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_pack_eta -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_pack +CHECK_FUNCTION_CONTRACTS=mld_polyveck_pack_eta +USE_FUNCTION_CONTRACTS=mld_polyeta_pack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = polyveck_pack_eta +FUNCTION_NAME = mld_polyveck_pack_eta # 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/polyveck_pack_t0/Makefile b/proofs/cbmc/polyveck_pack_t0/Makefile index 63d9b46f..e2139e67 100644 --- a/proofs/cbmc/polyveck_pack_t0/Makefile +++ b/proofs/cbmc/polyveck_pack_t0/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_pack_t0 -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyt0_pack +CHECK_FUNCTION_CONTRACTS=mld_polyveck_pack_t0 +USE_FUNCTION_CONTRACTS=mld_polyt0_pack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,7 +29,7 @@ CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula CBMCFLAGS += --no-array-field-sensitivity -FUNCTION_NAME = polyveck_pack_t0 +FUNCTION_NAME = mld_polyveck_pack_t0 # 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/polyveck_pack_w1/Makefile b/proofs/cbmc/polyveck_pack_w1/Makefile index a0e8dd1d..0b283a0f 100644 --- a/proofs/cbmc/polyveck_pack_w1/Makefile +++ b/proofs/cbmc/polyveck_pack_w1/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_pack_w1 -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyw1_pack +CHECK_FUNCTION_CONTRACTS=mld_polyveck_pack_w1 +USE_FUNCTION_CONTRACTS=mld_polyw1_pack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --no-array-field-sensitivity -FUNCTION_NAME = polyveck_pack_w1 +FUNCTION_NAME = mld_polyveck_pack_w1 # 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/polyveck_pointwise_poly_montgomery/Makefile b/proofs/cbmc/polyveck_pointwise_poly_montgomery/Makefile index 3fcfe848..102c5096 100644 --- a/proofs/cbmc/polyveck_pointwise_poly_montgomery/Makefile +++ b/proofs/cbmc/polyveck_pointwise_poly_montgomery/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_pointwise_poly_montgomery -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery +CHECK_FUNCTION_CONTRACTS=mld_polyveck_pointwise_poly_montgomery +USE_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --slice-formula -FUNCTION_NAME = polyveck_pointwise_poly_montgomery +FUNCTION_NAME = mld_polyveck_pointwise_poly_montgomery # 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/polyveck_power2round/Makefile b/proofs/cbmc/polyveck_power2round/Makefile index 56f78ada..0849b077 100644 --- a/proofs/cbmc/polyveck_power2round/Makefile +++ b/proofs/cbmc/polyveck_power2round/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_power2round -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_power2round +CHECK_FUNCTION_CONTRACTS=mld_polyveck_power2round +USE_FUNCTION_CONTRACTS=mld_poly_power2round APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_power2round +FUNCTION_NAME = mld_polyveck_power2round # 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/polyveck_reduce/Makefile b/proofs/cbmc/polyveck_reduce/Makefile index f5e49a50..71ab12d7 100644 --- a/proofs/cbmc/polyveck_reduce/Makefile +++ b/proofs/cbmc/polyveck_reduce/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_reduce -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_reduce +CHECK_FUNCTION_CONTRACTS=mld_polyveck_reduce +USE_FUNCTION_CONTRACTS=mld_poly_reduce APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_reduce +FUNCTION_NAME = mld_polyveck_reduce # 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/polyveck_shiftl/Makefile b/proofs/cbmc/polyveck_shiftl/Makefile index 7e1189e8..7800a3fc 100644 --- a/proofs/cbmc/polyveck_shiftl/Makefile +++ b/proofs/cbmc/polyveck_shiftl/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_shiftl -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_shiftl +CHECK_FUNCTION_CONTRACTS=mld_polyveck_shiftl +USE_FUNCTION_CONTRACTS=mld_poly_shiftl APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_shiftl +FUNCTION_NAME = mld_polyveck_shiftl # 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/polyveck_sub/Makefile b/proofs/cbmc/polyveck_sub/Makefile index 081e21a5..e64bfee2 100644 --- a/proofs/cbmc/polyveck_sub/Makefile +++ b/proofs/cbmc/polyveck_sub/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_sub -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_sub +CHECK_FUNCTION_CONTRACTS=mld_polyveck_sub +USE_FUNCTION_CONTRACTS=mld_poly_sub APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_sub +FUNCTION_NAME = mld_polyveck_sub # 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/polyveck_unpack_eta/Makefile b/proofs/cbmc/polyveck_unpack_eta/Makefile index f18b50a5..c72a9644 100644 --- a/proofs/cbmc/polyveck_unpack_eta/Makefile +++ b/proofs/cbmc/polyveck_unpack_eta/Makefile @@ -14,13 +14,13 @@ DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += $(MLD_NAMESPACE)polyveck_unpack_eta.0:8 # Largest value of MLDSA_K +UNWINDSET += mld_polyveck_unpack_eta.0:8 # Largest value of MLDSA_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_unpack_eta -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_unpack +CHECK_FUNCTION_CONTRACTS=mld_polyveck_unpack_eta +USE_FUNCTION_CONTRACTS=mld_polyeta_unpack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_unpack_eta +FUNCTION_NAME = mld_polyveck_unpack_eta # 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/polyveck_unpack_t0/Makefile b/proofs/cbmc/polyveck_unpack_t0/Makefile index d9080517..252060f8 100644 --- a/proofs/cbmc/polyveck_unpack_t0/Makefile +++ b/proofs/cbmc/polyveck_unpack_t0/Makefile @@ -14,13 +14,13 @@ DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += $(MLD_NAMESPACE)polyveck_unpack_t0.0:8 # Largest value of MLDSA_K +UNWINDSET += mld_polyveck_unpack_t0.0:8 # Largest value of MLDSA_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_unpack_t0 -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyt0_unpack +CHECK_FUNCTION_CONTRACTS=mld_polyveck_unpack_t0 +USE_FUNCTION_CONTRACTS=mld_polyt0_unpack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_unpack_t0 +FUNCTION_NAME = mld_polyveck_unpack_t0 # 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/polyveck_use_hint/Makefile b/proofs/cbmc/polyveck_use_hint/Makefile index cee10a87..09562a7d 100644 --- a/proofs/cbmc/polyveck_use_hint/Makefile +++ b/proofs/cbmc/polyveck_use_hint/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_use_hint -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_use_hint +CHECK_FUNCTION_CONTRACTS=mld_polyveck_use_hint +USE_FUNCTION_CONTRACTS=mld_poly_use_hint APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyveck_use_hint +FUNCTION_NAME = mld_polyveck_use_hint # 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/polyvecl_add/Makefile b/proofs/cbmc/polyvecl_add/Makefile index 300b9db8..ce954076 100644 --- a/proofs/cbmc/polyvecl_add/Makefile +++ b/proofs/cbmc/polyvecl_add/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_add -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_add +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_add +USE_FUNCTION_CONTRACTS=mld_poly_add APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --arrays-uf-always --slice-formula -FUNCTION_NAME = polyvecl_add +FUNCTION_NAME = mld_polyvecl_add # 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/polyvecl_chknorm/Makefile b/proofs/cbmc/polyvecl_chknorm/Makefile index 9382e881..e53e7f4c 100644 --- a/proofs/cbmc/polyvecl_chknorm/Makefile +++ b/proofs/cbmc/polyvecl_chknorm/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_chknorm -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_chknorm +USE_FUNCTION_CONTRACTS=mld_poly_chknorm APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -30,7 +30,7 @@ CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula CBMCFLAGS += --no-array-field-sensitivity -FUNCTION_NAME = polyvecl_chknorm +FUNCTION_NAME = mld_polyvecl_chknorm # 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/polyvecl_invntt_tomont/Makefile b/proofs/cbmc/polyvecl_invntt_tomont/Makefile index 39adb47a..888bd1e2 100644 --- a/proofs/cbmc/polyvecl_invntt_tomont/Makefile +++ b/proofs/cbmc/polyvecl_invntt_tomont/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_invntt_tomont -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_invntt_tomont +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_invntt_tomont +USE_FUNCTION_CONTRACTS=mld_poly_invntt_tomont APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyvecl_invntt_tomont +FUNCTION_NAME = mld_polyvecl_invntt_tomont # 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/polyvecl_ntt/Makefile b/proofs/cbmc/polyvecl_ntt/Makefile index 351285f5..bf5fa2e9 100644 --- a/proofs/cbmc/polyvecl_ntt/Makefile +++ b/proofs/cbmc/polyvecl_ntt/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_ntt -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_ntt +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_ntt +USE_FUNCTION_CONTRACTS=mld_poly_ntt APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyvecl_ntt +FUNCTION_NAME = mld_polyvecl_ntt # 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/polyvecl_pack_eta/Makefile b/proofs/cbmc/polyvecl_pack_eta/Makefile index 85051a9c..707c2a8f 100644 --- a/proofs/cbmc/polyvecl_pack_eta/Makefile +++ b/proofs/cbmc/polyvecl_pack_eta/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pack_eta -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_pack +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pack_eta +USE_FUNCTION_CONTRACTS=mld_polyeta_pack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = polyvecl_pack_eta +FUNCTION_NAME = mld_polyvecl_pack_eta # 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/polyvecl_pack_z/Makefile b/proofs/cbmc/polyvecl_pack_z/Makefile index 6f1a523b..08396938 100644 --- a/proofs/cbmc/polyvecl_pack_z/Makefile +++ b/proofs/cbmc/polyvecl_pack_z/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pack_z -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_pack +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pack_z +USE_FUNCTION_CONTRACTS=mld_polyz_pack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS += --slice-formula -FUNCTION_NAME = polyvecl_pack_z +FUNCTION_NAME = mld_polyvecl_pack_z # 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/polyvecl_pointwise_acc_montgomery/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile index a191e504..944bd8f1 100644 --- a/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_acc_montgomery +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery USE_FUNCTION_CONTRACTS=mld_montgomery_reduce APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --slice-formula --no-array-field-sensitivity -FUNCTION_NAME = polyvecl_pointwise_acc_montgomery +FUNCTION_NAME = mld_polyvecl_pointwise_acc_montgomery # 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/polyvecl_pointwise_poly_montgomery/Makefile b/proofs/cbmc/polyvecl_pointwise_poly_montgomery/Makefile index b1cbb297..58aae061 100644 --- a/proofs/cbmc/polyvecl_pointwise_poly_montgomery/Makefile +++ b/proofs/cbmc/polyvecl_pointwise_poly_montgomery/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_poly_montgomery -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_poly_montgomery +USE_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --slice-formula -FUNCTION_NAME = polyvecl_pointwise_poly_montgomery +FUNCTION_NAME = mld_polyvecl_pointwise_poly_montgomery # 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/polyvecl_reduce/Makefile b/proofs/cbmc/polyvecl_reduce/Makefile index f58df7a6..7edb6b93 100644 --- a/proofs/cbmc/polyvecl_reduce/Makefile +++ b/proofs/cbmc/polyvecl_reduce/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_reduce -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_reduce +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_reduce +USE_FUNCTION_CONTRACTS=mld_poly_reduce APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyvecl_reduce +FUNCTION_NAME = mld_polyvecl_reduce # 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/polyvecl_uniform_gamma1/Makefile b/proofs/cbmc/polyvecl_uniform_gamma1/Makefile index 79e3908b..00a2dc3b 100644 --- a/proofs/cbmc/polyvecl_uniform_gamma1/Makefile +++ b/proofs/cbmc/polyvecl_uniform_gamma1/Makefile @@ -19,10 +19,10 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1 -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_gamma1_4x +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_uniform_gamma1 +USE_FUNCTION_CONTRACTS=mld_poly_uniform_gamma1_4x ifeq ($(MLDSA_MODE),3) -USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_uniform_gamma1 +USE_FUNCTION_CONTRACTS+=mld_poly_uniform_gamma1 endif APPLY_LOOP_CONTRACTS=on @@ -32,7 +32,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyvecl_uniform_gamma1 +FUNCTION_NAME = mld_polyvecl_uniform_gamma1 # 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/polyvecl_unpack_eta/Makefile b/proofs/cbmc/polyvecl_unpack_eta/Makefile index 19186dab..4cb17163 100644 --- a/proofs/cbmc/polyvecl_unpack_eta/Makefile +++ b/proofs/cbmc/polyvecl_unpack_eta/Makefile @@ -14,13 +14,13 @@ DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += $(MLD_NAMESPACE)polyvecl_unpack_eta.0:7 # Largest value of MLDSA_L +UNWINDSET += mld_polyvecl_unpack_eta.0:7 # Largest value of MLDSA_L PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_unpack_eta -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_unpack +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_unpack_eta +USE_FUNCTION_CONTRACTS=mld_polyeta_unpack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyvecl_unpack_eta +FUNCTION_NAME = mld_polyvecl_unpack_eta # 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/polyvecl_unpack_z/Makefile b/proofs/cbmc/polyvecl_unpack_z/Makefile index 6d6025d3..1853f215 100644 --- a/proofs/cbmc/polyvecl_unpack_z/Makefile +++ b/proofs/cbmc/polyvecl_unpack_z/Makefile @@ -14,13 +14,13 @@ DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += $(MLD_NAMESPACE)polyvecl_unpack_z.0:7 # Largest value of MLDSA_L +UNWINDSET += mld_polyvecl_unpack_z.0:7 # Largest value of MLDSA_L PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_unpack_z -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_unpack +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_unpack_z +USE_FUNCTION_CONTRACTS=mld_polyz_unpack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyvecl_unpack_z +FUNCTION_NAME = mld_polyvecl_unpack_z # 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/polyw1_pack/Makefile b/proofs/cbmc/polyw1_pack/Makefile index 807daf60..20478417 100644 --- a/proofs/cbmc/polyw1_pack/Makefile +++ b/proofs/cbmc/polyw1_pack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyw1_pack +CHECK_FUNCTION_CONTRACTS=mld_polyw1_pack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyw1_pack +FUNCTION_NAME = mld_polyw1_pack # 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/polyz_pack/Makefile b/proofs/cbmc/polyz_pack/Makefile index ef47c44d..d3fddb13 100644 --- a/proofs/cbmc/polyz_pack/Makefile +++ b/proofs/cbmc/polyz_pack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_pack +CHECK_FUNCTION_CONTRACTS=mld_polyz_pack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyz_pack +FUNCTION_NAME = mld_polyz_pack # 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/polyz_unpack/Makefile b/proofs/cbmc/polyz_unpack/Makefile index be3e4aa0..6b473175 100644 --- a/proofs/cbmc/polyz_unpack/Makefile +++ b/proofs/cbmc/polyz_unpack/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_unpack +CHECK_FUNCTION_CONTRACTS=mld_polyz_unpack USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = polyz_unpack +FUNCTION_NAME = mld_polyz_unpack # 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/unpack_pk/Makefile b/proofs/cbmc/unpack_pk/Makefile index 53156cb8..1319ec04 100644 --- a/proofs/cbmc/unpack_pk/Makefile +++ b/proofs/cbmc/unpack_pk/Makefile @@ -14,13 +14,13 @@ DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += $(MLD_NAMESPACE)unpack_pk.0:8 # Largest value of MLDSA_K +UNWINDSET += mld_unpack_pk.0:8 # Largest value of MLDSA_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/packing.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_pk -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyt1_unpack +CHECK_FUNCTION_CONTRACTS=mld_unpack_pk +USE_FUNCTION_CONTRACTS=mld_polyt1_unpack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = unpack_pk +FUNCTION_NAME = mld_unpack_pk # 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/unpack_sig/Makefile b/proofs/cbmc/unpack_sig/Makefile index 43900878..b1032eb1 100644 --- a/proofs/cbmc/unpack_sig/Makefile +++ b/proofs/cbmc/unpack_sig/Makefile @@ -18,8 +18,8 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/packing.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sig -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_unpack_z mld_unpack_hints +CHECK_FUNCTION_CONTRACTS=mld_unpack_sig +USE_FUNCTION_CONTRACTS=mld_polyvecl_unpack_z mld_unpack_hints APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 CBMCFLAGS+=--slice-formula -FUNCTION_NAME = unpack_sig +FUNCTION_NAME = mld_unpack_sig # 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/unpack_sk/Makefile b/proofs/cbmc/unpack_sk/Makefile index 86b57434..28376ee3 100644 --- a/proofs/cbmc/unpack_sk/Makefile +++ b/proofs/cbmc/unpack_sk/Makefile @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/packing.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)unpack_sk -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_unpack_eta $(MLD_NAMESPACE)polyveck_unpack_eta $(MLD_NAMESPACE)polyveck_unpack_t0 +CHECK_FUNCTION_CONTRACTS=mld_unpack_sk +USE_FUNCTION_CONTRACTS=mld_polyvecl_unpack_eta mld_polyveck_unpack_eta mld_polyveck_unpack_t0 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = unpack_sk +FUNCTION_NAME = mld_unpack_sk # 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 From 8d03d627a6c7704a81763a2d9e0cd04d0b93f1de Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 13:37:18 -0700 Subject: [PATCH 03/18] update api definitions Signed-off-by: Jake Massimo --- mldsa/api.h | 17 ----------------- test/test_mldsa.c | 1 + 2 files changed, 1 insertion(+), 17 deletions(-) diff --git a/mldsa/api.h b/mldsa/api.h index c3584747..9a242542 100644 --- a/mldsa/api.h +++ b/mldsa/api.h @@ -21,23 +21,6 @@ #define MLD_87_SECRETKEYBYTES 4896 #define MLD_87_BYTES 4627 -int MLD_NAMESPACE_K(keypair)(uint8_t *pk, uint8_t *sk); - -int MLD_NAMESPACE_K(signature)(uint8_t *sig, size_t *siglen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *sk); - -int MLD_NAMESPACE_K(sign)(uint8_t *sm, size_t *smlen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *sk); - -int MLD_NAMESPACE_K(verify)(const uint8_t *sig, size_t siglen, const uint8_t *m, - size_t mlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *pk); - -int MLD_NAMESPACE_K(open)(uint8_t *m, size_t *mlen, const uint8_t *sm, - size_t smlen, const uint8_t *ctx, size_t ctxlen, - const uint8_t *pk); #if MLD_CONFIG_PARAMETER_SET == 44 #define CRYPTO_PUBLICKEYBYTES MLD_44_PUBLICKEYBYTES diff --git a/test/test_mldsa.c b/test/test_mldsa.c index dd0a4705..5af0a7b4 100644 --- a/test/test_mldsa.c +++ b/test/test_mldsa.c @@ -7,6 +7,7 @@ #include #include #include "../mldsa/api.h" +#include "../mldsa/sign.h" #include "../mldsa/sys.h" #include "notrandombytes/notrandombytes.h" From 7b68d43bb90e06a268e38435e07445cc099960c7 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 13:43:20 -0700 Subject: [PATCH 04/18] add api.h to bench_mldsa.c Signed-off-by: Jake Massimo --- test/bench_mldsa.c | 1 + 1 file changed, 1 insertion(+) diff --git a/test/bench_mldsa.c b/test/bench_mldsa.c index 1eb3bc52..d70f6332 100644 --- a/test/bench_mldsa.c +++ b/test/bench_mldsa.c @@ -8,6 +8,7 @@ #include #include #include +#include "../mldsa/api.h" #include "../mldsa/randombytes.h" #include "../mldsa/sign.h" #include "hal.h" From feb4c4fd336ba0d352b0e6eabf7c2248d447a57d Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 13:59:31 -0700 Subject: [PATCH 05/18] fix PCT config Signed-off-by: Jake Massimo --- test/break_pct_config.h | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/test/break_pct_config.h b/test/break_pct_config.h index f3618110..606c5385 100644 --- a/test/break_pct_config.h +++ b/test/break_pct_config.h @@ -7,19 +7,12 @@ #define MLD_RANDOMIZED_SIGNING -#ifndef MLDSA_MODE -#define MLDSA_MODE 2 +#ifndef MLD_CONFIG_PARAMETER_SET +#define MLD_CONFIG_PARAMETER_SET 44 #endif -#if MLDSA_MODE == 2 -#define MLD_NAMESPACETOP MLD_44_ref -#define MLD_NAMESPACE(s) MLD_44_ref_##s -#elif MLDSA_MODE == 3 -#define MLD_NAMESPACETOP MLD_65_ref -#define MLD_NAMESPACE(s) MLD_65_ref_##s -#elif MLDSA_MODE == 5 -#define MLD_NAMESPACETOP MLD_87_ref -#define MLD_NAMESPACE(s) MLD_87_ref_##s +#ifndef MLD_CONFIG_NAMESPACE_PREFIX +#define MLD_CONFIG_NAMESPACE_PREFIX mld #endif From 0d3a40aaefd9cb3708a19d53ddc9b3fb7e328ab3 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 14:16:51 -0700 Subject: [PATCH 06/18] remove setting 44 param set Signed-off-by: Jake Massimo --- test/break_pct_config.h | 4 ---- 1 file changed, 4 deletions(-) diff --git a/test/break_pct_config.h b/test/break_pct_config.h index 606c5385..0495e158 100644 --- a/test/break_pct_config.h +++ b/test/break_pct_config.h @@ -7,10 +7,6 @@ #define MLD_RANDOMIZED_SIGNING -#ifndef MLD_CONFIG_PARAMETER_SET -#define MLD_CONFIG_PARAMETER_SET 44 -#endif - #ifndef MLD_CONFIG_NAMESPACE_PREFIX #define MLD_CONFIG_NAMESPACE_PREFIX mld #endif From eca69a87ee487db5a6d92013bf944e24a59535cb Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 14:31:58 -0700 Subject: [PATCH 07/18] break pct config change Signed-off-by: Jake Massimo --- test/break_pct_config.h | 67 +++++++++++++++++++++++++++++++++++++++-- 1 file changed, 65 insertions(+), 2 deletions(-) diff --git a/test/break_pct_config.h b/test/break_pct_config.h index 0495e158..62d5bb14 100644 --- a/test/break_pct_config.h +++ b/test/break_pct_config.h @@ -7,8 +7,50 @@ #define MLD_RANDOMIZED_SIGNING -#ifndef MLD_CONFIG_NAMESPACE_PREFIX -#define MLD_CONFIG_NAMESPACE_PREFIX mld +/****************************************************************************** + * Name: MLD_CONFIG_PARAMETER_SET + * + * Description: Specifies the parameter set for ML-DSA + * - MLD_CONFIG_PARAMETER_SET=44 corresponds to ML-DSA-44 + * - MLD_CONFIG_PARAMETER_SET=65 corresponds to ML-DSA-65 + * - MLD_CONFIG_PARAMETER_SET=87 corresponds to ML-DSA-87 + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +#ifndef MLD_CONFIG_PARAMETER_SET +/* Map legacy MLDSA_MODE to new parameter set for backward compatibility */ +#ifndef MLDSA_MODE +#define MLDSA_MODE 2 +#endif + +#if MLDSA_MODE == 2 +#define MLD_CONFIG_PARAMETER_SET 44 +#elif MLDSA_MODE == 3 +#define MLD_CONFIG_PARAMETER_SET 65 +#elif MLDSA_MODE == 5 +#define MLD_CONFIG_PARAMETER_SET 87 +#else +#define MLD_CONFIG_PARAMETER_SET 44 /* Default to ML-DSA-44 */ +#endif +#endif /* !MLD_CONFIG_PARAMETER_SET */ + +/****************************************************************************** + * Name: MLD_CONFIG_NAMESPACE_PREFIX + * + * Description: The prefix to use to namespace global symbols from mldsa/. + * + * In a multi-level build (that is, if either + * - MLD_CONFIG_MULTILEVEL_WITH_SHARED, or + * - MLD_CONFIG_MULTILEVEL_NO_SHARED, + * are set, level-dependent symbols will additionally be prefixed + * with the parameter set (44/65/87). + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +#if !defined(MLD_CONFIG_NAMESPACE_PREFIX) +#define MLD_CONFIG_NAMESPACE_PREFIX MLD_DEFAULT_NAMESPACE_PREFIX #endif @@ -186,6 +228,27 @@ static MLD_INLINE int mld_break_pct(void) *****************************************************************************/ /* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */ +/************************* Config internals ********************************/ + +/* Default namespace + * + * Don't change this. If you need a different namespace, re-define + * MLD_CONFIG_NAMESPACE_PREFIX above instead, and remove the following. + * + * The default MLDSA namespace is + * + * PQCP_MLDSA_NATIVE_MLDSA_ + * + * e.g., PQCP_MLDSA_NATIVE_MLDSA44_ + */ + +#if MLD_CONFIG_PARAMETER_SET == 44 +#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA44 +#elif MLD_CONFIG_PARAMETER_SET == 65 +#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA65 +#elif MLD_CONFIG_PARAMETER_SET == 87 +#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA87 +#endif #endif /* !MLD_CONFIG_H */ From 2f6e248230b0381ea2bcc715f44e70cdd2c90649 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 14:53:23 -0700 Subject: [PATCH 08/18] fix custom zeroize congif Signed-off-by: Jake Massimo --- test/custom_zeroize_config.h | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/test/custom_zeroize_config.h b/test/custom_zeroize_config.h index ee4750af..3c97d9d1 100644 --- a/test/custom_zeroize_config.h +++ b/test/custom_zeroize_config.h @@ -7,19 +7,32 @@ #define MLD_RANDOMIZED_SIGNING +#ifndef MLD_CONFIG_PARAMETER_SET #ifndef MLDSA_MODE #define MLDSA_MODE 2 #endif #if MLDSA_MODE == 2 -#define MLD_NAMESPACETOP MLD_44_ref -#define MLD_NAMESPACE(s) MLD_44_ref_##s +#define MLD_CONFIG_PARAMETER_SET 44 #elif MLDSA_MODE == 3 -#define MLD_NAMESPACETOP MLD_65_ref -#define MLD_NAMESPACE(s) MLD_65_ref_##s +#define MLD_CONFIG_PARAMETER_SET 65 #elif MLDSA_MODE == 5 -#define MLD_NAMESPACETOP MLD_87_ref -#define MLD_NAMESPACE(s) MLD_87_ref_##s +#define MLD_CONFIG_PARAMETER_SET 87 +#else +#define MLD_CONFIG_PARAMETER_SET 44 +#endif +#endif + +#ifndef MLD_CONFIG_NAMESPACE_PREFIX +#if MLD_CONFIG_PARAMETER_SET == 44 +#define MLD_CONFIG_NAMESPACE_PREFIX MLD_44_ref_ +#elif MLD_CONFIG_PARAMETER_SET == 65 +#define MLD_CONFIG_NAMESPACE_PREFIX MLD_65_ref_ +#elif MLD_CONFIG_PARAMETER_SET == 87 +#define MLD_CONFIG_NAMESPACE_PREFIX MLD_87_ref_ +#else +#define MLD_CONFIG_NAMESPACE_PREFIX MLD_44_ref_ +#endif #endif From 8077609b085c836a64247945ac6be00e6894fcc7 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 15:02:35 -0700 Subject: [PATCH 09/18] fix cmbc proof for attempt_signature Signed-off-by: Jake Massimo --- .../mld_attempt_signature_generation/Makefile | 44 +++++++++---------- ...mld_attempt_signature_generation_harness.c | 1 + 2 files changed, 23 insertions(+), 22 deletions(-) diff --git a/proofs/cbmc/mld_attempt_signature_generation/Makefile b/proofs/cbmc/mld_attempt_signature_generation/Makefile index dbc4fc51..baea328b 100644 --- a/proofs/cbmc/mld_attempt_signature_generation/Makefile +++ b/proofs/cbmc/mld_attempt_signature_generation/Makefile @@ -20,29 +20,29 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c CHECK_FUNCTION_CONTRACTS=mld_attempt_signature_generation -USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1 \ - $(MLD_NAMESPACE)polyvecl_ntt \ - $(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery \ - $(MLD_NAMESPACE)polyveck_reduce \ - $(MLD_NAMESPACE)polyveck_invntt_tomont \ - $(MLD_NAMESPACE)polyveck_caddq \ - $(MLD_NAMESPACE)polyveck_decompose \ - $(MLD_NAMESPACE)polyveck_pack_w1 \ +USE_FUNCTION_CONTRACTS=mld_polyvecl_uniform_gamma1 \ + mld_polyvecl_ntt \ + mld_polyvec_matrix_pointwise_montgomery \ + mld_polyveck_reduce \ + mld_polyveck_invntt_tomont \ + mld_polyveck_caddq \ + mld_polyveck_decompose \ + mld_polyveck_pack_w1 \ mld_H \ - $(MLD_NAMESPACE)poly_challenge \ - $(MLD_NAMESPACE)poly_ntt \ - $(MLD_NAMESPACE)polyvecl_pointwise_poly_montgomery \ - $(MLD_NAMESPACE)polyvecl_invntt_tomont \ - $(MLD_NAMESPACE)polyvecl_add \ - $(MLD_NAMESPACE)polyvecl_reduce \ - $(MLD_NAMESPACE)polyvecl_chknorm \ - $(MLD_NAMESPACE)polyveck_pointwise_poly_montgomery \ - $(MLD_NAMESPACE)polyveck_sub \ - $(MLD_NAMESPACE)polyveck_reduce \ - $(MLD_NAMESPACE)polyveck_chknorm \ - $(MLD_NAMESPACE)polyveck_add \ - $(MLD_NAMESPACE)polyveck_make_hint \ - $(MLD_NAMESPACE)pack_sig + mld_poly_challenge \ + mld_poly_ntt \ + mld_polyvecl_pointwise_poly_montgomery \ + mld_polyvecl_invntt_tomont \ + mld_polyvecl_add \ + mld_polyvecl_reduce \ + mld_polyvecl_chknorm \ + mld_polyveck_pointwise_poly_montgomery \ + mld_polyveck_sub \ + mld_polyveck_reduce \ + mld_polyveck_chknorm \ + mld_polyveck_add \ + mld_polyveck_make_hint \ + mld_pack_sig USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on diff --git a/proofs/cbmc/mld_attempt_signature_generation/mld_attempt_signature_generation_harness.c b/proofs/cbmc/mld_attempt_signature_generation/mld_attempt_signature_generation_harness.c index ffe6a3b7..e896609d 100644 --- a/proofs/cbmc/mld_attempt_signature_generation/mld_attempt_signature_generation_harness.c +++ b/proofs/cbmc/mld_attempt_signature_generation/mld_attempt_signature_generation_harness.c @@ -1,6 +1,7 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT +#include "api.h" #include "sign.h" int mld_attempt_signature_generation( From 7219178dccfd341cd9cd2b456e4420d96e18a979 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 15:36:39 -0700 Subject: [PATCH 10/18] remove namespacing Signed-off-by: Jake Massimo --- proofs/cbmc/crypto_sign/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/cbmc/crypto_sign/Makefile b/proofs/cbmc/crypto_sign/Makefile index 21468495..7f05e5dc 100644 --- a/proofs/cbmc/crypto_sign/Makefile +++ b/proofs/cbmc/crypto_sign/Makefile @@ -19,7 +19,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACETOP) +CHECK_FUNCTION_CONTRACTS=mld_sign USE_FUNCTION_CONTRACTS=mld_signature APPLY_LOOP_CONTRACTS=on From 95f058287388b9af87d5d88319a3dfeba117fc0b Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 15:40:20 -0700 Subject: [PATCH 11/18] include new apis in stack test Signed-off-by: Jake Massimo --- test/test_stack.c | 1 + 1 file changed, 1 insertion(+) diff --git a/test/test_stack.c b/test/test_stack.c index 95867d8f..5cfd3325 100644 --- a/test/test_stack.c +++ b/test/test_stack.c @@ -7,6 +7,7 @@ #include #include "api.h" +#include "../mldsa/sign.h" static void test_keygen_only(void) { From 7c7f787a02f38df2849fe2446c7f92b7b72baaaa Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 15:45:13 -0700 Subject: [PATCH 12/18] linting Signed-off-by: Jake Massimo --- test/test_stack.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/test_stack.c b/test/test_stack.c index 5cfd3325..e50fc997 100644 --- a/test/test_stack.c +++ b/test/test_stack.c @@ -6,8 +6,8 @@ #include #include -#include "api.h" #include "../mldsa/sign.h" +#include "api.h" static void test_keygen_only(void) { From ba1fff81f1628df28e41cd1df3ecf26405d77d10 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 16:24:27 -0700 Subject: [PATCH 13/18] fix no asm config Signed-off-by: Jake Massimo --- test/no_asm_config.h | 50 +++++++++++++++++++++++++++++++++++--------- 1 file changed, 40 insertions(+), 10 deletions(-) diff --git a/test/no_asm_config.h b/test/no_asm_config.h index b8cc80b6..7c6fa2c0 100644 --- a/test/no_asm_config.h +++ b/test/no_asm_config.h @@ -7,19 +7,49 @@ #define MLD_RANDOMIZED_SIGNING +/****************************************************************************** + * Name: MLD_CONFIG_PARAMETER_SET + * + * Description: Parameter set to use for ML-DSA. + * + * This must be one of: + * - MLD_PARAMETER_SET_44 (ML-DSA-44) + * - MLD_PARAMETER_SET_65 (ML-DSA-65) + * - MLD_PARAMETER_SET_87 (ML-DSA-87) + * + *****************************************************************************/ +#ifndef MLD_CONFIG_PARAMETER_SET +#define MLD_CONFIG_PARAMETER_SET MLD_PARAMETER_SET_44 +#endif + +/****************************************************************************** + * Name: MLD_CONFIG_NAMESPACE + * + * Description: Namespace to use for ML-DSA symbols. + * + * If this is undefined, a default namespace based on the + * parameter set will be used. + * + *****************************************************************************/ +#ifndef MLD_CONFIG_NAMESPACE +#if MLD_CONFIG_PARAMETER_SET == MLD_PARAMETER_SET_44 +#define MLD_CONFIG_NAMESPACE MLD_44_ref +#elif MLD_CONFIG_PARAMETER_SET == MLD_PARAMETER_SET_65 +#define MLD_CONFIG_NAMESPACE MLD_65_ref +#elif MLD_CONFIG_PARAMETER_SET == MLD_PARAMETER_SET_87 +#define MLD_CONFIG_NAMESPACE MLD_87_ref +#endif +#endif + +/* Backward compatibility */ #ifndef MLDSA_MODE +#if MLD_CONFIG_PARAMETER_SET == MLD_PARAMETER_SET_44 #define MLDSA_MODE 2 +#elif MLD_CONFIG_PARAMETER_SET == MLD_PARAMETER_SET_65 +#define MLDSA_MODE 3 +#elif MLD_CONFIG_PARAMETER_SET == MLD_PARAMETER_SET_87 +#define MLDSA_MODE 5 #endif - -#if MLDSA_MODE == 2 -#define MLD_NAMESPACETOP MLD_44_ref -#define MLD_NAMESPACE(s) MLD_44_ref_##s -#elif MLDSA_MODE == 3 -#define MLD_NAMESPACETOP MLD_65_ref -#define MLD_NAMESPACE(s) MLD_65_ref_##s -#elif MLDSA_MODE == 5 -#define MLD_NAMESPACETOP MLD_87_ref -#define MLD_NAMESPACE(s) MLD_87_ref_##s #endif /****************************************************************************** From c15909e9e82f87d469f802f97117796126bc9883 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 17:18:27 -0700 Subject: [PATCH 14/18] include common.h to provide namespace macro Signed-off-by: Jake Massimo --- mldsa/ntt.c | 1 + 1 file changed, 1 insertion(+) diff --git a/mldsa/ntt.c b/mldsa/ntt.c index b754cf5d..3006423e 100644 --- a/mldsa/ntt.c +++ b/mldsa/ntt.c @@ -6,6 +6,7 @@ #include "ntt.h" #include "reduce.h" +#include "common.h" static int32_t mld_fqmul(int32_t a, int32_t b) __contract__( From e7761522629074c64894de3b6f5ba6b4ff86ad56 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 17:24:21 -0700 Subject: [PATCH 15/18] alphabetical ordering Signed-off-by: Jake Massimo --- mldsa/ntt.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mldsa/ntt.c b/mldsa/ntt.c index 3006423e..2d2e6e0e 100644 --- a/mldsa/ntt.c +++ b/mldsa/ntt.c @@ -4,9 +4,9 @@ */ #include +#include "common.h" #include "ntt.h" #include "reduce.h" -#include "common.h" static int32_t mld_fqmul(int32_t a, int32_t b) __contract__( From 72087ffb11e012f954692fdd0d8397bbfbc339f0 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 18:09:03 -0700 Subject: [PATCH 16/18] change all mldsa_mode to config_param_set Signed-off-by: Jake Massimo --- mldsa/poly.c | 18 +++++++++--------- mldsa/rounding.h | 12 ++++++------ mldsa/sign.c | 8 ++++---- test/mk/components.mk | 12 ++++++------ 4 files changed, 25 insertions(+), 25 deletions(-) diff --git a/mldsa/poly.c b/mldsa/poly.c index 90092a8f..9e0f40f5 100644 --- a/mldsa/poly.c +++ b/mldsa/poly.c @@ -1042,7 +1042,7 @@ void mld_polyz_pack(uint8_t *r, const mld_poly *a) mld_assert_bound(a->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); -#if MLDSA_MODE == 2 +#if MLD_CONFIG_PARAMETER_SET == 44 for (i = 0; i < MLDSA_N / 4; ++i) __loop__( invariant(i <= MLDSA_N/4)) @@ -1065,7 +1065,7 @@ void mld_polyz_pack(uint8_t *r, const mld_poly *a) r[9 * i + 7] = (t[3] >> 2) & 0xFF; r[9 * i + 8] = (t[3] >> 10) & 0xFF; } -#else /* MLDSA_MODE == 2 */ +#else /* MLD_CONFIG_PARAMETER_SET == 44 */ for (i = 0; i < MLDSA_N / 2; ++i) __loop__( invariant(i <= MLDSA_N/2)) @@ -1080,14 +1080,14 @@ void mld_polyz_pack(uint8_t *r, const mld_poly *a) r[5 * i + 3] = (t[1] >> 4) & 0xFF; r[5 * i + 4] = (t[1] >> 12) & 0xFF; } -#endif /* MLDSA_MODE != 2 */ +#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ } void mld_polyz_unpack(mld_poly *r, const uint8_t *a) { unsigned int i; -#if MLDSA_MODE == 2 +#if MLD_CONFIG_PARAMETER_SET == 44 for (i = 0; i < MLDSA_N / 4; ++i) __loop__( invariant(i <= MLDSA_N/4) @@ -1118,7 +1118,7 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t *a) r->coeffs[4 * i + 2] = MLDSA_GAMMA1 - r->coeffs[4 * i + 2]; r->coeffs[4 * i + 3] = MLDSA_GAMMA1 - r->coeffs[4 * i + 3]; } -#else /* MLDSA_MODE == 2 */ +#else /* MLD_CONFIG_PARAMETER_SET == 44 */ for (i = 0; i < MLDSA_N / 2; ++i) __loop__( invariant(i <= MLDSA_N/2) @@ -1138,7 +1138,7 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t *a) r->coeffs[2 * i + 0] = MLDSA_GAMMA1 - r->coeffs[2 * i + 0]; r->coeffs[2 * i + 1] = MLDSA_GAMMA1 - r->coeffs[2 * i + 1]; } -#endif /* MLDSA_MODE != 2 */ +#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); } @@ -1149,7 +1149,7 @@ void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); -#if MLDSA_MODE == 2 +#if MLD_CONFIG_PARAMETER_SET == 44 for (i = 0; i < MLDSA_N / 4; ++i) __loop__( invariant(i <= MLDSA_N/4)) @@ -1161,12 +1161,12 @@ void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) r[3 * i + 2] = (a->coeffs[4 * i + 2] >> 4) & 0xFF; r[3 * i + 2] |= (a->coeffs[4 * i + 3] << 2) & 0xFF; } -#else /* MLDSA_MODE == 2 */ +#else /* MLD_CONFIG_PARAMETER_SET == 44 */ for (i = 0; i < MLDSA_N / 2; ++i) __loop__( invariant(i <= MLDSA_N/2)) { r[i] = a->coeffs[2 * i + 0] | (a->coeffs[2 * i + 1] << 4); } -#endif /* MLDSA_MODE != 2 */ +#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ } diff --git a/mldsa/rounding.h b/mldsa/rounding.h index d410bf47..c2a6666e 100644 --- a/mldsa/rounding.h +++ b/mldsa/rounding.h @@ -76,20 +76,20 @@ __contract__( /* We know a >= 0 and a < MLDSA_Q, so... */ cassert(*a1 >= 0 && *a1 <= 65472); -#if MLDSA_MODE == 2 +#if MLD_CONFIG_PARAMETER_SET == 44 *a1 = (*a1 * 11275 + (1 << 23)) >> 24; cassert(*a1 >= 0 && *a1 <= 44); *a1 = mld_ct_sel_int32(0, *a1, mld_ct_cmask_neg_i32(43 - *a1)); cassert(*a1 >= 0 && *a1 <= 43); -#else /* MLDSA_MODE == 2 */ +#else /* MLD_CONFIG_PARAMETER_SET == 44 */ *a1 = (*a1 * 1025 + (1 << 21)) >> 22; cassert(*a1 >= 0 && *a1 <= 16); *a1 &= 15; cassert(*a1 >= 0 && *a1 <= 15); -#endif /* MLDSA_MODE != 2 */ +#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ *a0 = a - *a1 * 2 * MLDSA_GAMMA2; *a0 = mld_ct_sel_int32(*a0 - MLDSA_Q, *a0, @@ -146,7 +146,7 @@ __contract__( return a1; } -#if MLDSA_MODE == 2 +#if MLD_CONFIG_PARAMETER_SET == 44 if (a0 > 0) { return (a1 == 43) ? 0 : a1 + 1; @@ -155,7 +155,7 @@ __contract__( { return (a1 == 0) ? 43 : a1 - 1; } -#else /* MLDSA_MODE == 2 */ +#else /* MLD_CONFIG_PARAMETER_SET == 44 */ if (a0 > 0) { return (a1 + 1) & 15; @@ -164,7 +164,7 @@ __contract__( { return (a1 - 1) & 15; } -#endif /* MLDSA_MODE != 2 */ +#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ } diff --git a/mldsa/sign.c b/mldsa/sign.c index f2047a20..ce230415 100644 --- a/mldsa/sign.c +++ b/mldsa/sign.c @@ -97,12 +97,12 @@ __contract__( ) { /* Sample short vectors s1 and s2 */ -#if MLDSA_MODE == 2 +#if MLD_CONFIG_PARAMETER_SET == 44 mld_poly_uniform_eta_4x(&s1->vec[0], &s1->vec[1], &s1->vec[2], &s1->vec[3], seed, 0, 1, 2, 3); mld_poly_uniform_eta_4x(&s2->vec[0], &s2->vec[1], &s2->vec[2], &s2->vec[3], seed, 4, 5, 6, 7); -#elif MLDSA_MODE == 3 +#elif MLD_CONFIG_PARAMETER_SET == 65 mld_poly_uniform_eta_4x(&s1->vec[0], &s1->vec[1], &s1->vec[2], &s1->vec[3], seed, 0, 1, 2, 3); mld_poly_uniform_eta_4x(&s1->vec[4], &s2->vec[0], &s2->vec[1], @@ -110,7 +110,7 @@ __contract__( 0xFF /* irrelevant */); mld_poly_uniform_eta_4x(&s2->vec[2], &s2->vec[3], &s2->vec[4], &s2->vec[5], seed, 7, 8, 9, 10); -#elif MLDSA_MODE == 5 +#elif MLD_CONFIG_PARAMETER_SET == 87 mld_poly_uniform_eta_4x(&s1->vec[0], &s1->vec[1], &s1->vec[2], &s1->vec[3], seed, 0, 1, 2, 3); mld_poly_uniform_eta_4x(&s1->vec[4], &s1->vec[5], &s1->vec[6], @@ -120,7 +120,7 @@ __contract__( seed, 7, 8, 9, 10); mld_poly_uniform_eta_4x(&s2->vec[4], &s2->vec[5], &s2->vec[6], &s2->vec[7], seed, 11, 12, 13, 14); -#endif /* MLDSA_MODE == 5 */ +#endif /* MLD_CONFIG_PARAMETER_SET == 87 */ } MLD_MUST_CHECK_RETURN_VALUE diff --git a/test/mk/components.mk b/test/mk/components.mk index 6553f885..72f8485e 100644 --- a/test/mk/components.mk +++ b/test/mk/components.mk @@ -21,11 +21,11 @@ MLDSA65_DIR = $(BUILD_DIR)/mldsa65 MLDSA87_DIR = $(BUILD_DIR)/mldsa87 MLDSA44_OBJS = $(call MAKE_OBJS,$(MLDSA44_DIR),$(SOURCES) $(FIPS202_SRCS)) -$(MLDSA44_OBJS): CFLAGS += -DMLDSA_MODE=2 +$(MLDSA44_OBJS): CFLAGS += -DMLD_CONFIG_PARAMETER_SET=44 MLDSA65_OBJS = $(call MAKE_OBJS,$(MLDSA65_DIR),$(SOURCES) $(FIPS202_SRCS)) -$(MLDSA65_OBJS): CFLAGS += -DMLDSA_MODE=3 +$(MLDSA65_OBJS): CFLAGS += -DMLD_CONFIG_PARAMETER_SET=65 MLDSA87_OBJS = $(call MAKE_OBJS,$(MLDSA87_DIR),$(SOURCES) $(FIPS202_SRCS)) -$(MLDSA87_OBJS): CFLAGS += -DMLDSA_MODE=5 +$(MLDSA87_OBJS): CFLAGS += -DMLD_CONFIG_PARAMETER_SET=87 $(BUILD_DIR)/libmldsa44.a: $(MLDSA44_OBJS) $(BUILD_DIR)/libmldsa65.a: $(MLDSA65_OBJS) @@ -51,9 +51,9 @@ $(MLDSA44_DIR)/bin/bench_components_mldsa44: $(MLDSA44_DIR)/test/hal/hal.c.o $(MLDSA65_DIR)/bin/bench_components_mldsa65: $(MLDSA65_DIR)/test/hal/hal.c.o $(MLDSA87_DIR)/bin/bench_components_mldsa87: $(MLDSA87_DIR)/test/hal/hal.c.o -$(MLDSA44_DIR)/bin/%: CFLAGS += -DMLDSA_MODE=2 -$(MLDSA65_DIR)/bin/%: CFLAGS += -DMLDSA_MODE=3 -$(MLDSA87_DIR)/bin/%: CFLAGS += -DMLDSA_MODE=5 +$(MLDSA44_DIR)/bin/%: CFLAGS += -DMLD_CONFIG_PARAMETER_SET=44 +$(MLDSA65_DIR)/bin/%: CFLAGS += -DMLD_CONFIG_PARAMETER_SET=65 +$(MLDSA87_DIR)/bin/%: CFLAGS += -DMLD_CONFIG_PARAMETER_SET=87 # Link tests with respective library define ADD_SOURCE From d67d215f5cbfc636c1533b9cd836411adcb405c9 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Thu, 11 Sep 2025 23:54:32 -0700 Subject: [PATCH 17/18] provide config param set provided as in mlkem-native Signed-off-by: Jake Massimo --- Makefile.Microsoft_nmake | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/Makefile.Microsoft_nmake b/Makefile.Microsoft_nmake index 382217ba..ea998f0b 100644 --- a/Makefile.Microsoft_nmake +++ b/Makefile.Microsoft_nmake @@ -31,57 +31,57 @@ OPT = 0 # compilation for mldsa44 {mldsa}.c{$(MLDSA44_BUILD_DIR)\mldsa}.obj:: @if NOT EXIST $(MLDSA44_BUILD_DIR)\mldsa mkdir $(MLDSA44_BUILD_DIR)\mldsa - $(CC) $(CFLAGS) /D MLDSA_MODE=2 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\ $< {mldsa\fips202}.c{$(MLDSA44_BUILD_DIR)\mldsa\fips202}.obj:: @if NOT EXIST $(MLDSA44_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA44_BUILD_DIR)\mldsa\fips202 - $(CC) $(CFLAGS) /D MLDSA_MODE=2 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\fips202\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\mldsa\fips202\ $< {test}.c{$(MLDSA44_BUILD_DIR)\test}.obj:: @if NOT EXIST $(MLDSA44_BUILD_DIR)\test mkdir $(MLDSA44_BUILD_DIR)\test - $(CC) $(CFLAGS) /D MLDSA_MODE=2 /c /Fo$(MLDSA44_BUILD_DIR)\test\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /c /Fo$(MLDSA44_BUILD_DIR)\test\ $< # compilation for mldsa65 {mldsa}.c{$(MLDSA65_BUILD_DIR)\mldsa}.obj:: @if NOT EXIST $(MLDSA65_BUILD_DIR)\mldsa mkdir $(MLDSA65_BUILD_DIR)\mldsa - $(CC) $(CFLAGS) /D MLDSA_MODE=3 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\ $< {mldsa\fips202}.c{$(MLDSA65_BUILD_DIR)\mldsa\fips202}.obj:: @if NOT EXIST $(MLDSA65_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA65_BUILD_DIR)\mldsa\fips202 - $(CC) $(CFLAGS) /D MLDSA_MODE=3 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\fips202\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\mldsa\fips202\ $< {test}.c{$(MLDSA65_BUILD_DIR)\test}.obj:: @if NOT EXIST $(MLDSA65_BUILD_DIR)\test mkdir $(MLDSA65_BUILD_DIR)\test - $(CC) $(CFLAGS) /D MLDSA_MODE=3 /c /Fo$(MLDSA65_BUILD_DIR)\test\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /c /Fo$(MLDSA65_BUILD_DIR)\test\ $< # compilation for mldsa87 {mldsa}.c{$(MLDSA87_BUILD_DIR)\mldsa}.obj:: @if NOT EXIST $(MLDSA87_BUILD_DIR)\mldsa mkdir $(MLDSA87_BUILD_DIR)\mldsa - $(CC) $(CFLAGS) /D MLDSA_MODE=5 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\ $< {mldsa\fips202}.c{$(MLDSA87_BUILD_DIR)\mldsa\fips202}.obj:: @if NOT EXIST $(MLDSA87_BUILD_DIR)\mldsa\fips202 mkdir $(MLDSA87_BUILD_DIR)\mldsa\fips202 - $(CC) $(CFLAGS) /D MLDSA_MODE=5 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\fips202\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\mldsa\fips202\ $< {test}.c{$(MLDSA87_BUILD_DIR)\test}.obj:: @if NOT EXIST $(MLDSA87_BUILD_DIR)\test mkdir $(MLDSA87_BUILD_DIR)\test - $(CC) $(CFLAGS) /D MLDSA_MODE=5 /c /Fo$(MLDSA87_BUILD_DIR)\test\ $< + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /c /Fo$(MLDSA87_BUILD_DIR)\test\ $< # compile functional test for mldsa44 test_mldsa44: $(OBJ_FILES_44) $(MLDSA44_BUILD_DIR)\test\test_mldsa.obj $(BUILD_DIR)\randombytes\notrandombytes.obj @if NOT EXIST $(MLDSA44_BUILD_DIR)\bin mkdir $(MLDSA44_BUILD_DIR)\bin - $(CC) $(CFLAGS) /D MLDSA_MODE=2 /Fe$(MLDSA44_BUILD_DIR)\bin\test_mldsa44 $** /link + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=44 /Fe$(MLDSA44_BUILD_DIR)\bin\test_mldsa44 $** /link # compile functional test for mldsa65 test_mldsa65: $(OBJ_FILES_65) $(MLDSA65_BUILD_DIR)\test\test_mldsa.obj $(BUILD_DIR)\randombytes\notrandombytes.obj @if NOT EXIST $(MLDSA65_BUILD_DIR)\bin mkdir $(MLDSA65_BUILD_DIR)\bin - $(CC) $(CFLAGS) /D MLDSA_MODE=3 /Fe$(MLDSA65_BUILD_DIR)\bin\test_mldsa65 $** /link + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=65 /Fe$(MLDSA65_BUILD_DIR)\bin\test_mldsa65 $** /link # compile functional test for mldsa87 test_mldsa87: $(OBJ_FILES_87) $(MLDSA87_BUILD_DIR)\test\test_mldsa.obj $(BUILD_DIR)\randombytes\notrandombytes.obj @if NOT EXIST $(MLDSA87_BUILD_DIR)\bin mkdir $(MLDSA87_BUILD_DIR)\bin - $(CC) $(CFLAGS) /D MLDSA_MODE=5 /Fe$(MLDSA87_BUILD_DIR)\bin\test_mldsa87 $** /link + $(CC) $(CFLAGS) /D MLD_CONFIG_PARAMETER_SET=87 /Fe$(MLDSA87_BUILD_DIR)\bin\test_mldsa87 $** /link quickcheck: test_mldsa44 test_mldsa65 test_mldsa87 $(MLDSA44_BUILD_DIR)\bin\test_mldsa44.exe From f0f86eeaba2ef50365253689ae3f45c573edf7ac Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Fri, 12 Sep 2025 01:09:09 -0700 Subject: [PATCH 18/18] testing failing proof Signed-off-by: Jake Massimo --- proofs/cbmc/polyvec_matrix_expand/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/proofs/cbmc/polyvec_matrix_expand/Makefile b/proofs/cbmc/polyvec_matrix_expand/Makefile index 77a62bc4..557a1084 100644 --- a/proofs/cbmc/polyvec_matrix_expand/Makefile +++ b/proofs/cbmc/polyvec_matrix_expand/Makefile @@ -18,6 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c CHECK_FUNCTION_CONTRACTS=mld_polyvec_matrix_expand USE_FUNCTION_CONTRACTS=mld_poly_uniform_4x mld_poly_uniform