diff --git a/BIBLIOGRAPHY.md b/BIBLIOGRAPHY.md index 4cc0a0472..f19a89b40 100644 --- a/BIBLIOGRAPHY.md +++ b/BIBLIOGRAPHY.md @@ -50,6 +50,7 @@ source code and documentation. - [mldsa/fips202/fips202x4.c](mldsa/fips202/fips202x4.c) - [mldsa/ntt.h](mldsa/ntt.h) - [mldsa/poly.c](mldsa/poly.c) + - [mldsa/poly_kl.c](mldsa/poly_kl.c) - [mldsa/polyvec.c](mldsa/polyvec.c) - [mldsa/rounding.h](mldsa/rounding.h) - [mldsa/sign.c](mldsa/sign.c) @@ -127,6 +128,7 @@ source code and documentation. - [README.md](README.md) - [mldsa/ntt.c](mldsa/ntt.c) - [mldsa/poly.c](mldsa/poly.c) + - [mldsa/poly_kl.c](mldsa/poly_kl.c) ### `REF_AVX2` diff --git a/integration/liboqs/ML-DSA-44_META.yml b/integration/liboqs/ML-DSA-44_META.yml index 24ae1156b..9209f9fd6 100644 --- a/integration/liboqs/ML-DSA-44_META.yml +++ b/integration/liboqs/ML-DSA-44_META.yml @@ -31,8 +31,9 @@ implementations: sources: integration/liboqs/config_c.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c mldsa/packing.h mldsa/params.h mldsa/poly.c - mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h - mldsa/rounding.h mldsa/sign.c mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc + mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c mldsa/polyvec.h mldsa/randombytes.h + mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h mldsa/symmetric.h mldsa/sys.h + mldsa/zetas.inc - name: x86_64 version: FIPS204 folder_name: . @@ -44,9 +45,9 @@ implementations: sources: integration/liboqs/config_x86_64.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/native/api.h mldsa/native/meta.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c - mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h - mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h - mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/x86_64 + mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c + mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c + mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/x86_64 supported_platforms: - architecture: x86_64 operating_systems: @@ -67,9 +68,9 @@ implementations: sources: integration/liboqs/config_aarch64.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/native/api.h mldsa/native/meta.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c - mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h - mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h - mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/aarch64 + mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c + mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c + mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/aarch64 supported_platforms: - architecture: arm_8 operating_systems: diff --git a/integration/liboqs/ML-DSA-65_META.yml b/integration/liboqs/ML-DSA-65_META.yml index c09815c67..8b5a68fe3 100644 --- a/integration/liboqs/ML-DSA-65_META.yml +++ b/integration/liboqs/ML-DSA-65_META.yml @@ -31,8 +31,9 @@ implementations: sources: integration/liboqs/config_c.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c mldsa/packing.h mldsa/params.h mldsa/poly.c - mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h - mldsa/rounding.h mldsa/sign.c mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc + mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c mldsa/polyvec.h mldsa/randombytes.h + mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h mldsa/symmetric.h mldsa/sys.h + mldsa/zetas.inc - name: x86_64 version: FIPS204 folder_name: . @@ -44,9 +45,9 @@ implementations: sources: integration/liboqs/config_x86_64.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/native/api.h mldsa/native/meta.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c - mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h - mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h - mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/x86_64 + mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c + mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c + mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/x86_64 supported_platforms: - architecture: x86_64 operating_systems: @@ -67,9 +68,9 @@ implementations: sources: integration/liboqs/config_aarch64.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/native/api.h mldsa/native/meta.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c - mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h - mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h - mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/aarch64 + mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c + mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c + mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/aarch64 supported_platforms: - architecture: arm_8 operating_systems: diff --git a/integration/liboqs/ML-DSA-87_META.yml b/integration/liboqs/ML-DSA-87_META.yml index a990119d0..b4b3805a6 100644 --- a/integration/liboqs/ML-DSA-87_META.yml +++ b/integration/liboqs/ML-DSA-87_META.yml @@ -31,8 +31,9 @@ implementations: sources: integration/liboqs/config_c.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c mldsa/packing.h mldsa/params.h mldsa/poly.c - mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h - mldsa/rounding.h mldsa/sign.c mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc + mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c mldsa/polyvec.h mldsa/randombytes.h + mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h mldsa/symmetric.h mldsa/sys.h + mldsa/zetas.inc - name: x86_64 version: FIPS204 folder_name: . @@ -44,9 +45,9 @@ implementations: sources: integration/liboqs/config_x86_64.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/native/api.h mldsa/native/meta.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c - mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h - mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h - mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/x86_64 + mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c + mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c + mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/x86_64 supported_platforms: - architecture: x86_64 operating_systems: @@ -66,9 +67,9 @@ implementations: sources: integration/liboqs/config_aarch64.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h mldsa/cbmc.h mldsa/common.h mldsa/ct.c mldsa/ct.h mldsa/debug.c mldsa/debug.h mldsa/native/api.h mldsa/native/meta.h mldsa/ntt.c mldsa/ntt.h mldsa/packing.c - mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/polyvec.c mldsa/polyvec.h - mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c mldsa/sign.h - mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/aarch64 + mldsa/packing.h mldsa/params.h mldsa/poly.c mldsa/poly.h mldsa/poly_kl.c mldsa/polyvec.c + mldsa/polyvec.h mldsa/randombytes.h mldsa/reduce.h mldsa/rounding.h mldsa/sign.c + mldsa/sign.h mldsa/symmetric.h mldsa/sys.h mldsa/zetas.inc mldsa/native/aarch64 supported_platforms: - architecture: arm_8 operating_systems: diff --git a/mldsa/common.h b/mldsa/common.h index 360a90fca..9cfcf7b4c 100644 --- a/mldsa/common.h +++ b/mldsa/common.h @@ -49,15 +49,32 @@ #define MLD_CONCAT_(x1, x2) x1##x2 #define MLD_CONCAT(x1, x2) MLD_CONCAT_(x1, x2) +#if defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) || \ + defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) +#define MLD_MULTILEVEL_BUILD +#endif + +#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_KL \ + MLD_CONCAT(MLD_ADD_PARAM_SET(MLD_CONFIG_NAMESPACE_PREFIX), _) /* Functions are prefixed by MLD_CONFIG_NAMESPACE_PREFIX. * - * Example: If MLD_CONFIG_NAMESPACE_PREFIX is PQCP_MLDSA_NATIVE_MLDSA44, then - * MLD_NAMESPACE(sign) becomes PQCP_MLDSA_NATIVE_MLDSA44_sign. + * 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, then + * MLD_NAMESPACE_KL(keypair) becomes PQCP_MLDSA_NATIVE44_keypair/ + * PQCP_MLDSA_NATIVE65_keypair/PQCP_MLDSA_NATIVE87_keypair. */ #define MLD_NAMESPACE(s) MLD_CONCAT(MLD_NAMESPACE_PREFIX, s) -#define MLD_NAMESPACETOP MLD_CONFIG_NAMESPACE_PREFIX +#define MLD_NAMESPACE_KL(s) MLD_CONCAT(MLD_NAMESPACE_PREFIX_KL, s) #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) #include MLD_CONFIG_ARITH_BACKEND_FILE diff --git a/mldsa/config.h b/mldsa/config.h index 0cb8f4320..fc86fb284 100644 --- a/mldsa/config.h +++ b/mldsa/config.h @@ -43,6 +43,12 @@ * * 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. * *****************************************************************************/ @@ -50,6 +56,51 @@ #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. + * + * Example: TODO: add example + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ + /****************************************************************************** * Name: MLD_CONFIG_FILE * diff --git a/mldsa/debug.c b/mldsa/debug.c index 200d33fcf..a55d51e8b 100644 --- a/mldsa/debug.c +++ b/mldsa/debug.c @@ -8,6 +8,8 @@ #include "common.h" +#if !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) + #if defined(MLDSA_DEBUG) #include @@ -60,6 +62,12 @@ MLD_EMPTY_CU(debug) #endif /* !MLDSA_DEBUG */ +#else /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */ + +MLD_EMPTY_CU(debug) + +#endif /* MLD_CONFIG_MULTILEVEL_NO_SHARED */ + /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ #undef MLD_DEBUG_ERROR_HEADER diff --git a/mldsa/ntt.c b/mldsa/ntt.c index e38930225..73f02b79c 100644 --- a/mldsa/ntt.c +++ b/mldsa/ntt.c @@ -12,6 +12,10 @@ * https://github.com/pq-crystals/dilithium/tree/master/ref */ +#include "common.h" + +#if !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) + #include #include "ntt.h" @@ -244,3 +248,7 @@ void mld_invntt_tomont(int32_t a[MLDSA_N]) a[j] = mld_fqscale(a[j]); } } + +#else /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */ +MLD_EMPTY_CU(mld_ntt) +#endif /* MLD_CONFIG_MULTILEVEL_NO_SHARED */ diff --git a/mldsa/packing.h b/mldsa/packing.h index 407b736cf..a5102a0dd 100644 --- a/mldsa/packing.h +++ b/mldsa/packing.h @@ -8,7 +8,7 @@ #include #include "polyvec.h" -#define mld_pack_pk MLD_NAMESPACE(pack_pk) +#define mld_pack_pk MLD_NAMESPACE_KL(pack_pk) /************************************************* * Name: mld_pack_pk * @@ -31,7 +31,7 @@ __contract__( ); -#define mld_pack_sk MLD_NAMESPACE(pack_sk) +#define mld_pack_sk MLD_NAMESPACE_KL(pack_sk) /************************************************* * Name: mld_pack_sk * @@ -69,7 +69,7 @@ __contract__( ); -#define mld_pack_sig MLD_NAMESPACE(pack_sig) +#define mld_pack_sig MLD_NAMESPACE_KL(pack_sig) /************************************************* * Name: mld_pack_sig * @@ -104,7 +104,7 @@ __contract__( assigns(memory_slice(sig, CRYPTO_BYTES)) ); -#define mld_unpack_pk MLD_NAMESPACE(unpack_pk) +#define mld_unpack_pk MLD_NAMESPACE_KL(unpack_pk) /************************************************* * Name: mld_unpack_pk * @@ -128,7 +128,7 @@ __contract__( ); -#define mld_unpack_sk MLD_NAMESPACE(unpack_sk) +#define mld_unpack_sk MLD_NAMESPACE_KL(unpack_sk) /************************************************* * Name: mld_unpack_sk * @@ -169,7 +169,7 @@ __contract__( array_bound(s2->vec[k2].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) ); -#define mld_unpack_sig MLD_NAMESPACE(unpack_sig) +#define mld_unpack_sig MLD_NAMESPACE_KL(unpack_sig) /************************************************* * Name: mld_unpack_sig * diff --git a/mldsa/poly.c b/mldsa/poly.c index eadc6b18a..dc1ee8096 100644 --- a/mldsa/poly.c +++ b/mldsa/poly.c @@ -21,6 +21,7 @@ #include #include +#include "common.h" #include "ct.h" #include "debug.h" #include "ntt.h" @@ -29,6 +30,8 @@ #include "rounding.h" #include "symmetric.h" +#if !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) + MLD_INTERNAL_API void mld_poly_reduce(mld_poly *a) { @@ -218,154 +221,6 @@ void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a) mld_assert_bound(a1->coeffs, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1); } -MLD_INTERNAL_API -void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) -{ -#if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) && MLD_CONFIG_PARAMETER_SET == 44 - /* TODO: proof */ - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - mld_poly_decompose_88_native(a1->coeffs, a0->coeffs, a->coeffs); -#elif defined(MLD_USE_NATIVE_POLY_DECOMPOSE_32) && \ - (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) - /* TODO: proof */ - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - mld_poly_decompose_32_native(a1->coeffs, a0->coeffs, a->coeffs); -#else /* !(MLD_USE_NATIVE_POLY_DECOMPOSE_88 && MLD_CONFIG_PARAMETER_SET == 44) \ - && MLD_USE_NATIVE_POLY_DECOMPOSE_32 && (MLD_CONFIG_PARAMETER_SET == \ - 65 || MLD_CONFIG_PARAMETER_SET == 87) */ - unsigned int i; - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - for (i = 0; i < MLDSA_N; ++i) - __loop__( - assigns(i, memory_slice(a0, sizeof(mld_poly)), memory_slice(a1, sizeof(mld_poly))) - invariant(i <= MLDSA_N) - invariant(array_bound(a1->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) - invariant(array_abs_bound(a0->coeffs, 0, i, MLDSA_GAMMA2+1)) - ) - { - mld_decompose(&a0->coeffs[i], &a1->coeffs[i], a->coeffs[i]); - } -#endif /* !(MLD_USE_NATIVE_POLY_DECOMPOSE_88 && MLD_CONFIG_PARAMETER_SET == \ - 44) && !(MLD_USE_NATIVE_POLY_DECOMPOSE_32 && \ - (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)) \ - */ - - mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2 + 1); - mld_assert_bound(a1->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); -} - -MLD_INTERNAL_API -unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, - const mld_poly *a1) -{ - unsigned int i, s = 0; - - for (i = 0; i < MLDSA_N; ++i) - __loop__( - invariant(i <= MLDSA_N) - invariant(s <= i) - invariant(array_bound(h->coeffs, 0, i, 0, 2)) - ) - { - const unsigned int hint_bit = mld_make_hint(a0->coeffs[i], a1->coeffs[i]); - h->coeffs[i] = hint_bit; - s += hint_bit; - } - - mld_assert(s <= MLDSA_N); - mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - return s; -} - -MLD_INTERNAL_API -void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) -{ -#if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) && MLD_CONFIG_PARAMETER_SET == 44 - /* TODO: proof */ - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - mld_poly_use_hint_88_native(b->coeffs, a->coeffs, h->coeffs); -#elif defined(MLD_USE_NATIVE_POLY_USE_HINT_32) && \ - (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) - /* TODO: proof */ - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - mld_poly_use_hint_32_native(b->coeffs, a->coeffs, h->coeffs); -#else /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \ - && MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET == 65 \ - || MLD_CONFIG_PARAMETER_SET == 87) */ - unsigned int i; - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - - for (i = 0; i < MLDSA_N; ++i) - __loop__( - invariant(i <= MLDSA_N) - invariant(array_bound(b->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) - ) - { - b->coeffs[i] = mld_use_hint(a->coeffs[i], h->coeffs[i]); - } -#endif /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \ - && !(MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET == \ - 65 || MLD_CONFIG_PARAMETER_SET == 87)) */ - - mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); -} - -/* Reference: explicitly checks the bound B to be <= (MLDSA_Q - 1) / 8). - * This is unnecessary as it's always a compile-time constant. - * We instead model it as a precondition. - * Checking the bound is performed using a conditional arguing - * that it is okay to leak which coefficient violates the bound (while the - * coefficient itself must remain secret). - * We instead perform everything in constant-time. - * Also it is sufficient to check that it is smaller than - * MLDSA_Q - REDUCE32_RANGE_MAX > (MLDSA_Q - 1) / 8). - */ -MLD_INTERNAL_API -uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) -{ -#if defined(MLD_USE_NATIVE_POLY_CHKNORM) - /* TODO: proof */ - mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX); - return mld_poly_chknorm_native(a->coeffs, B); -#else - unsigned int i; - uint32_t t = 0; - mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX); - - - for (i = 0; i < MLDSA_N; ++i) - __loop__( - invariant(i <= MLDSA_N) - invariant(t == 0 || t == 0xFFFFFFFF) - invariant((t == 0) == array_abs_bound(a->coeffs, 0, i, B)) - ) - { - /* - * Since we know that -REDUCE32_RANGE_MAX <= a < REDUCE32_RANGE_MAX, - * and B <= MLDSA_Q - REDUCE32_RANGE_MAX, to check if - * -B < (a mod± MLDSA_Q) < B, it suffices to check if -B < a < B. - * - * We prove this to be true using the following CBMC assertions. - * a ==> b expressed as !a || b to also allow run-time assertion. - */ - mld_assert(a->coeffs[i] < B || a->coeffs[i] - MLDSA_Q <= -B); - mld_assert(a->coeffs[i] > -B || a->coeffs[i] + MLDSA_Q >= B); - - /* Reference: Leaks which coefficient violates the bound via a conditional. - * We are more conservative to reduce the number of declassifications in - * constant-time testing. - */ - - /* if (abs(a[i]) >= B) */ - t |= mld_ct_cmask_neg_i32(B - 1 - mld_ct_abs_i32(a->coeffs[i])); - } - - return t; -#endif /* !MLD_USE_NATIVE_POLY_CHKNORM */ -} /************************************************* * Name: mld_rej_uniform @@ -553,476 +408,6 @@ void mld_poly_uniform_4x(mld_poly *vec0, mld_poly *vec1, mld_poly *vec2, mld_zeroize(buf, sizeof(buf)); } -/************************************************* - * Name: mld_rej_eta - * - * Description: Sample uniformly random coefficients in [-MLDSA_ETA, MLDSA_ETA] - *by performing rejection sampling on array of random bytes. - * - * Arguments: - int32_t *a: pointer to output array (allocated) - * - unsigned int target: requested number of coefficients to - *sample - * - unsigned int offset: number of coefficients already sampled - * - const uint8_t *buf: array of random bytes to sample from - * - unsigned int buflen: length of array of random bytes - * - * Returns number of sampled coefficients. Can be smaller than target if not - *enough random bytes were given. - **************************************************/ - -/* Reference: `mld_rej_eta()` in the reference implementation @[REF]. - * - Our signature differs from the reference implementation - * in that it adds the offset and always expects the base of the - * target buffer. This avoids shifting the buffer base in the - * caller, which appears tricky to reason about. */ -#if MLDSA_ETA == 2 -/* - * Sampling 256 coefficients mod 15 using rejection sampling from 4 bits. - * Expected number of required bytes: (256 * (16/15))/2 = 136.5 bytes. - * We sample 1 block (=136 bytes) of SHAKE256_RATE output initially. - * Sampling 2 blocks initially results in slightly worse performance. - */ -#define POLY_UNIFORM_ETA_NBLOCKS 1 -#elif MLDSA_ETA == 4 -/* - * Sampling 256 coefficients mod 9 using rejection sampling from 4 bits. - * Expected number of required bytes: (256 * (16/9))/2 = 227.5 bytes. - * We sample 2 blocks (=272 bytes) of SHAKE256_RATE output initially. - */ -#define POLY_UNIFORM_ETA_NBLOCKS 2 -#else /* MLDSA_ETA == 4 */ -#error "Invalid value of MLDSA_ETA" -#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ -static unsigned int mld_rej_eta(int32_t *a, unsigned int target, - unsigned int offset, const uint8_t *buf, - unsigned int buflen) -__contract__( - requires(offset <= target && target <= MLDSA_N) - requires(buflen <= (POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)) - requires(memory_no_alias(a, sizeof(int32_t) * target)) - requires(memory_no_alias(buf, buflen)) - requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) - assigns(memory_slice(a, sizeof(int32_t) * target)) - ensures(offset <= return_value && return_value <= target) - ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) -) -{ - unsigned int ctr, pos; - int t_valid; - uint32_t t0, t1; - mld_assert_abs_bound(a, offset, MLDSA_ETA + 1); - -/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */ -#if MLDSA_ETA == 2 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) - if (offset == 0) - { - int ret = mld_rej_uniform_eta2_native(a, target, buf, buflen); - if (ret != -1) - { - unsigned res = (unsigned)ret; - mld_assert_abs_bound(a, res, MLDSA_ETA + 1); - return res; - } - } -/* TODO: CBMC proof based on mld_rej_uniform_eta4_native */ -#elif MLDSA_ETA == 4 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) - if (offset == 0) - { - int ret = mld_rej_uniform_eta4_native(a, target, buf, buflen); - if (ret != -1) - { - unsigned res = (unsigned)ret; - mld_assert_abs_bound(a, res, MLDSA_ETA + 1); - return res; - } - } -#endif /* !(MLDSA_ETA == 2 && MLD_USE_NATIVE_REJ_UNIFORM_ETA2) && MLDSA_ETA == \ - 4 && MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */ - - ctr = offset; - pos = 0; - while (ctr < target && pos < buflen) - __loop__( - invariant(offset <= ctr && ctr <= target && pos <= buflen) - invariant(array_abs_bound(a, 0, ctr, MLDSA_ETA + 1)) - ) - { - t0 = buf[pos] & 0x0F; - t1 = buf[pos++] >> 4; - - /* Constant time: The inputs and outputs to the rejection sampling are - * secret. However, it is fine to leak which coefficients have been - * rejected. For constant-time testing, we declassify the result of - * the comparison. - */ -#if MLDSA_ETA == 2 - t_valid = t0 < 15; - MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); - if (t_valid) /* t0 < 15 */ - { - t0 = t0 - (205 * t0 >> 10) * 5; - a[ctr++] = 2 - (int32_t)t0; - } - t_valid = t1 < 15; - MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); - if (t_valid && ctr < target) /* t1 < 15 */ - { - t1 = t1 - (205 * t1 >> 10) * 5; - a[ctr++] = 2 - (int32_t)t1; - } -#elif MLDSA_ETA == 4 - t_valid = t0 < 9; - MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); - if (t_valid) /* t0 < 9 */ - { - a[ctr++] = 4 - (int32_t)t0; - } - t_valid = t1 < 9; /* t1 < 9 */ - MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); - if (t_valid && ctr < target) - { - a[ctr++] = 4 - (int32_t)t1; - } -#else /* MLDSA_ETA == 4 */ -#error "Invalid value of MLDSA_ETA" -#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ - } - - mld_assert_abs_bound(a, ctr, MLDSA_ETA + 1); - - return ctr; -} - -MLD_INTERNAL_API -void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, - mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES], - uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, - uint8_t nonce3) -{ - /* Temporary buffers for XOF output before rejection sampling */ - MLD_ALIGN uint8_t - buf[4][MLD_ALIGN_UP(POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)]; - - MLD_ALIGN uint8_t extseed[4][MLD_ALIGN_UP(MLDSA_CRHBYTES + 2)]; - - /* Tracks the number of coefficients we have already sampled */ - unsigned ctr[4]; - mld_xof256_x4_ctx state; - unsigned buflen; - - mld_memcpy(extseed[0], seed, MLDSA_CRHBYTES); - mld_memcpy(extseed[1], seed, MLDSA_CRHBYTES); - mld_memcpy(extseed[2], seed, MLDSA_CRHBYTES); - mld_memcpy(extseed[3], seed, MLDSA_CRHBYTES); - extseed[0][MLDSA_CRHBYTES] = nonce0; - extseed[1][MLDSA_CRHBYTES] = nonce1; - extseed[2][MLDSA_CRHBYTES] = nonce2; - extseed[3][MLDSA_CRHBYTES] = nonce3; - extseed[0][MLDSA_CRHBYTES + 1] = 0; - extseed[1][MLDSA_CRHBYTES + 1] = 0; - extseed[2][MLDSA_CRHBYTES + 1] = 0; - extseed[3][MLDSA_CRHBYTES + 1] = 0; - - mld_xof256_x4_init(&state); - mld_xof256_x4_absorb(&state, extseed, MLDSA_CRHBYTES + 2); - - /* - * Initially, squeeze heuristic number of POLY_UNIFORM_ETA_NBLOCKS. - * This should generate the coefficients with high probability. - */ - mld_xof256_x4_squeezeblocks(buf, POLY_UNIFORM_ETA_NBLOCKS, &state); - buflen = POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES; - - ctr[0] = mld_rej_eta(r0->coeffs, MLDSA_N, 0, buf[0], buflen); - ctr[1] = mld_rej_eta(r1->coeffs, MLDSA_N, 0, buf[1], buflen); - ctr[2] = mld_rej_eta(r2->coeffs, MLDSA_N, 0, buf[2], buflen); - ctr[3] = mld_rej_eta(r3->coeffs, MLDSA_N, 0, buf[3], buflen); - - /* - * So long as not all entries have been generated, squeeze - * one more block a time until we're done. - */ - buflen = STREAM256_BLOCKBYTES; - while (ctr[0] < MLDSA_N || ctr[1] < MLDSA_N || ctr[2] < MLDSA_N || - ctr[3] < MLDSA_N) - __loop__( - assigns(ctr, state, memory_slice(r0, sizeof(mld_poly)), - memory_slice(r1, sizeof(mld_poly)), memory_slice(r2, sizeof(mld_poly)), - memory_slice(r3, sizeof(mld_poly)), object_whole(buf[0]), - object_whole(buf[1]), object_whole(buf[2]), - object_whole(buf[3])) - invariant(ctr[0] <= MLDSA_N && ctr[1] <= MLDSA_N) - invariant(ctr[2] <= MLDSA_N && ctr[3] <= MLDSA_N) - invariant(array_abs_bound(r0->coeffs, 0, ctr[0], MLDSA_ETA + 1)) - invariant(array_abs_bound(r1->coeffs, 0, ctr[1], MLDSA_ETA + 1)) - invariant(array_abs_bound(r2->coeffs, 0, ctr[2], MLDSA_ETA + 1)) - invariant(array_abs_bound(r3->coeffs, 0, ctr[3], MLDSA_ETA + 1))) - { - mld_xof256_x4_squeezeblocks(buf, 1, &state); - ctr[0] = mld_rej_eta(r0->coeffs, MLDSA_N, ctr[0], buf[0], buflen); - ctr[1] = mld_rej_eta(r1->coeffs, MLDSA_N, ctr[1], buf[1], buflen); - ctr[2] = mld_rej_eta(r2->coeffs, MLDSA_N, ctr[2], buf[2], buflen); - ctr[3] = mld_rej_eta(r3->coeffs, MLDSA_N, ctr[3], buf[3], buflen); - } - - mld_xof256_x4_release(&state); - - mld_assert_abs_bound(r0->coeffs, MLDSA_N, MLDSA_ETA + 1); - mld_assert_abs_bound(r1->coeffs, MLDSA_N, MLDSA_ETA + 1); - mld_assert_abs_bound(r2->coeffs, MLDSA_N, MLDSA_ETA + 1); - mld_assert_abs_bound(r3->coeffs, MLDSA_N, MLDSA_ETA + 1); - - /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ - mld_zeroize(buf, sizeof(buf)); - mld_zeroize(extseed, sizeof(extseed)); -} - - -#define POLY_UNIFORM_GAMMA1_NBLOCKS \ - ((MLDSA_POLYZ_PACKEDBYTES + STREAM256_BLOCKBYTES - 1) / STREAM256_BLOCKBYTES) -MLD_INTERNAL_API -void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES], - uint16_t nonce) -{ - MLD_ALIGN uint8_t buf[POLY_UNIFORM_GAMMA1_NBLOCKS * STREAM256_BLOCKBYTES]; - MLD_ALIGN uint8_t extseed[MLDSA_CRHBYTES + 2]; - mld_xof256_ctx state; - - mld_memcpy(extseed, seed, MLDSA_CRHBYTES); - extseed[MLDSA_CRHBYTES] = nonce & 0xFF; - extseed[MLDSA_CRHBYTES + 1] = nonce >> 8; - - mld_xof256_init(&state); - mld_xof256_absorb_once(&state, extseed, MLDSA_CRHBYTES + 2); - - mld_xof256_squeezeblocks(buf, POLY_UNIFORM_GAMMA1_NBLOCKS, &state); - mld_polyz_unpack(a, buf); - - mld_xof256_release(&state); - - mld_assert_bound(a->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - - /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ - mld_zeroize(buf, sizeof(buf)); - mld_zeroize(extseed, sizeof(extseed)); -} - -MLD_INTERNAL_API -void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, - mld_poly *r3, - const uint8_t seed[MLDSA_CRHBYTES], - uint16_t nonce0, uint16_t nonce1, - uint16_t nonce2, uint16_t nonce3) -{ - /* Temporary buffers for XOF output before rejection sampling */ - MLD_ALIGN uint8_t - buf[4][MLD_ALIGN_UP(POLY_UNIFORM_GAMMA1_NBLOCKS * STREAM256_BLOCKBYTES)]; - - MLD_ALIGN uint8_t extseed[4][MLD_ALIGN_UP(MLDSA_CRHBYTES + 2)]; - - /* Tracks the number of coefficients we have already sampled */ - mld_xof256_x4_ctx state; - - mld_memcpy(extseed[0], seed, MLDSA_CRHBYTES); - mld_memcpy(extseed[1], seed, MLDSA_CRHBYTES); - mld_memcpy(extseed[2], seed, MLDSA_CRHBYTES); - mld_memcpy(extseed[3], seed, MLDSA_CRHBYTES); - extseed[0][MLDSA_CRHBYTES] = nonce0 & 0xFF; - extseed[1][MLDSA_CRHBYTES] = nonce1 & 0xFF; - extseed[2][MLDSA_CRHBYTES] = nonce2 & 0xFF; - extseed[3][MLDSA_CRHBYTES] = nonce3 & 0xFF; - extseed[0][MLDSA_CRHBYTES + 1] = nonce0 >> 8; - extseed[1][MLDSA_CRHBYTES + 1] = nonce1 >> 8; - extseed[2][MLDSA_CRHBYTES + 1] = nonce2 >> 8; - extseed[3][MLDSA_CRHBYTES + 1] = nonce3 >> 8; - - mld_xof256_x4_init(&state); - mld_xof256_x4_absorb(&state, extseed, MLDSA_CRHBYTES + 2); - mld_xof256_x4_squeezeblocks(buf, POLY_UNIFORM_GAMMA1_NBLOCKS, &state); - - mld_polyz_unpack(r0, buf[0]); - mld_polyz_unpack(r1, buf[1]); - mld_polyz_unpack(r2, buf[2]); - mld_polyz_unpack(r3, buf[3]); - mld_xof256_x4_release(&state); - - mld_assert_bound(r0->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - mld_assert_bound(r1->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - mld_assert_bound(r2->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - mld_assert_bound(r3->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - - /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ - mld_zeroize(buf, sizeof(buf)); - mld_zeroize(extseed, sizeof(extseed)); -} - -MLD_INTERNAL_API -void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES]) -{ - unsigned int i, j, pos; - uint64_t signs; - uint64_t offset; - MLD_ALIGN uint8_t buf[SHAKE256_RATE]; - mld_shake256ctx state; - - mld_shake256_init(&state); - mld_shake256_absorb(&state, seed, MLDSA_CTILDEBYTES); - mld_shake256_finalize(&state); - mld_shake256_squeeze(buf, SHAKE256_RATE, &state); - - /* Convert the first 8 bytes of buf[] into an unsigned 64-bit value. */ - /* Each bit of that dictates the sign of the resulting challenge value */ - signs = 0; - for (i = 0; i < 8; ++i) - __loop__( - assigns(i, signs) - invariant(i <= 8) - ) - { - signs |= (uint64_t)buf[i] << 8 * i; - } - pos = 8; - - mld_memset(c, 0, sizeof(mld_poly)); - - for (i = MLDSA_N - MLDSA_TAU; i < MLDSA_N; ++i) - __loop__( - assigns(i, j, object_whole(buf), state, pos, memory_slice(c, sizeof(mld_poly)), signs) - invariant(i >= MLDSA_N - MLDSA_TAU) - invariant(i <= MLDSA_N) - invariant(pos >= 1) - invariant(pos <= SHAKE256_RATE) - invariant(array_bound(c->coeffs, 0, MLDSA_N, -1, 2)) - invariant(state.pos <= SHAKE256_RATE) - ) - { - do - __loop__( - assigns(j, object_whole(buf), state, pos) - invariant(state.pos <= SHAKE256_RATE) - ) - { - if (pos >= SHAKE256_RATE) - { - mld_shake256_squeeze(buf, SHAKE256_RATE, &state); - pos = 0; - } - j = buf[pos++]; - } while (j > i); - - c->coeffs[i] = c->coeffs[j]; - - /* Reference: Compute coefficent value here in two steps to */ - /* mixinf unsigned and signed arithmetic with implicit */ - /* conversions, and so that CBMC can keep track of ranges */ - /* to complete type-safety proof here. */ - - /* The least-significant bit of signs tells us if we want -1 or +1 */ - offset = 2 * (signs & 1); - - /* offset has value 0 or 2 here, so (1 - (int32_t) offset) has - * value -1 or +1 */ - c->coeffs[j] = 1 - (int32_t)offset; - - /* Move to the next bit of signs for next time */ - signs >>= 1; - } - - mld_assert_bound(c->coeffs, MLDSA_N, -1, 2); - mld_shake256_release(&state); - - /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ - mld_zeroize(buf, sizeof(buf)); - mld_zeroize(&signs, sizeof(signs)); -} - -MLD_INTERNAL_API -void mld_polyeta_pack(uint8_t *r, const mld_poly *a) -{ - unsigned int i; - uint8_t t[8]; - - mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_ETA + 1); - -#if MLDSA_ETA == 2 - for (i = 0; i < MLDSA_N / 8; ++i) - __loop__( - invariant(i <= MLDSA_N/8)) - { - t[0] = MLDSA_ETA - a->coeffs[8 * i + 0]; - t[1] = MLDSA_ETA - a->coeffs[8 * i + 1]; - t[2] = MLDSA_ETA - a->coeffs[8 * i + 2]; - t[3] = MLDSA_ETA - a->coeffs[8 * i + 3]; - t[4] = MLDSA_ETA - a->coeffs[8 * i + 4]; - t[5] = MLDSA_ETA - a->coeffs[8 * i + 5]; - t[6] = MLDSA_ETA - a->coeffs[8 * i + 6]; - t[7] = MLDSA_ETA - a->coeffs[8 * i + 7]; - - r[3 * i + 0] = ((t[0] >> 0) | (t[1] << 3) | (t[2] << 6)) & 0xFF; - r[3 * i + 1] = - ((t[2] >> 2) | (t[3] << 1) | (t[4] << 4) | (t[5] << 7)) & 0xFF; - r[3 * i + 2] = ((t[5] >> 1) | (t[6] << 2) | (t[7] << 5)) & 0xFF; - } -#elif MLDSA_ETA == 4 - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2)) - { - t[0] = MLDSA_ETA - a->coeffs[2 * i + 0]; - t[1] = MLDSA_ETA - a->coeffs[2 * i + 1]; - r[i] = t[0] | (t[1] << 4); - } -#else /* MLDSA_ETA == 4 */ -#error "Invalid value of MLDSA_ETA" -#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ -} - -void mld_polyeta_unpack(mld_poly *r, const uint8_t *a) -{ - unsigned int i; - -#if MLDSA_ETA == 2 - for (i = 0; i < MLDSA_N / 8; ++i) - __loop__( - invariant(i <= MLDSA_N/8) - invariant(array_bound(r->coeffs, 0, i*8, -5, MLDSA_ETA + 1))) - { - r->coeffs[8 * i + 0] = (a[3 * i + 0] >> 0) & 7; - r->coeffs[8 * i + 1] = (a[3 * i + 0] >> 3) & 7; - r->coeffs[8 * i + 2] = ((a[3 * i + 0] >> 6) | (a[3 * i + 1] << 2)) & 7; - r->coeffs[8 * i + 3] = (a[3 * i + 1] >> 1) & 7; - r->coeffs[8 * i + 4] = (a[3 * i + 1] >> 4) & 7; - r->coeffs[8 * i + 5] = ((a[3 * i + 1] >> 7) | (a[3 * i + 2] << 1)) & 7; - r->coeffs[8 * i + 6] = (a[3 * i + 2] >> 2) & 7; - r->coeffs[8 * i + 7] = (a[3 * i + 2] >> 5) & 7; - - r->coeffs[8 * i + 0] = MLDSA_ETA - r->coeffs[8 * i + 0]; - r->coeffs[8 * i + 1] = MLDSA_ETA - r->coeffs[8 * i + 1]; - r->coeffs[8 * i + 2] = MLDSA_ETA - r->coeffs[8 * i + 2]; - r->coeffs[8 * i + 3] = MLDSA_ETA - r->coeffs[8 * i + 3]; - r->coeffs[8 * i + 4] = MLDSA_ETA - r->coeffs[8 * i + 4]; - r->coeffs[8 * i + 5] = MLDSA_ETA - r->coeffs[8 * i + 5]; - r->coeffs[8 * i + 6] = MLDSA_ETA - r->coeffs[8 * i + 6]; - r->coeffs[8 * i + 7] = MLDSA_ETA - r->coeffs[8 * i + 7]; - } -#elif MLDSA_ETA == 4 - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2) - invariant(array_bound(r->coeffs, 0, i*2, -11, MLDSA_ETA + 1))) - { - r->coeffs[2 * i + 0] = a[i] & 0x0F; - r->coeffs[2 * i + 1] = a[i] >> 4; - r->coeffs[2 * i + 0] = MLDSA_ETA - r->coeffs[2 * i + 0]; - r->coeffs[2 * i + 1] = MLDSA_ETA - r->coeffs[2 * i + 1]; - } -#else /* MLDSA_ETA == 4 */ -#error "Invalid value of MLDSA_ETA" -#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ - - mld_assert_bound(r->coeffs, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, - MLDSA_ETA + 1); -} MLD_INTERNAL_API void mld_polyt1_pack(uint8_t *r, const mld_poly *a) @@ -1173,141 +558,7 @@ void mld_polyt0_unpack(mld_poly *r, const uint8_t *a) (1 << (MLDSA_D - 1)) + 1); } -MLD_INTERNAL_API -void mld_polyz_pack(uint8_t *r, const mld_poly *a) -{ - unsigned int i; - uint32_t t[4]; - mld_assert_bound(a->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); - -#if MLD_CONFIG_PARAMETER_SET == 44 - for (i = 0; i < MLDSA_N / 4; ++i) - __loop__( - invariant(i <= MLDSA_N/4)) - { - t[0] = MLDSA_GAMMA1 - a->coeffs[4 * i + 0]; - t[1] = MLDSA_GAMMA1 - a->coeffs[4 * i + 1]; - t[2] = MLDSA_GAMMA1 - a->coeffs[4 * i + 2]; - t[3] = MLDSA_GAMMA1 - a->coeffs[4 * i + 3]; - - r[9 * i + 0] = (t[0]) & 0xFF; - r[9 * i + 1] = (t[0] >> 8) & 0xFF; - r[9 * i + 2] = (t[0] >> 16) & 0xFF; - r[9 * i + 2] |= (t[1] << 2) & 0xFF; - r[9 * i + 3] = (t[1] >> 6) & 0xFF; - r[9 * i + 4] = (t[1] >> 14) & 0xFF; - r[9 * i + 4] |= (t[2] << 4) & 0xFF; - r[9 * i + 5] = (t[2] >> 4) & 0xFF; - r[9 * i + 6] = (t[2] >> 12) & 0xFF; - r[9 * i + 6] |= (t[3] << 6) & 0xFF; - r[9 * i + 7] = (t[3] >> 2) & 0xFF; - r[9 * i + 8] = (t[3] >> 10) & 0xFF; - } -#else /* MLD_CONFIG_PARAMETER_SET == 44 */ - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2)) - { - t[0] = MLDSA_GAMMA1 - a->coeffs[2 * i + 0]; - t[1] = MLDSA_GAMMA1 - a->coeffs[2 * i + 1]; - - r[5 * i + 0] = (t[0]) & 0xFF; - r[5 * i + 1] = (t[0] >> 8) & 0xFF; - r[5 * i + 2] = (t[0] >> 16) & 0xFF; - r[5 * i + 2] |= (t[1] << 4) & 0xFF; - r[5 * i + 3] = (t[1] >> 4) & 0xFF; - r[5 * i + 4] = (t[1] >> 12) & 0xFF; - } -#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ -} - -MLD_INTERNAL_API -void mld_polyz_unpack(mld_poly *r, const uint8_t *a) -{ - unsigned int i; - -#if MLD_CONFIG_PARAMETER_SET == 44 - for (i = 0; i < MLDSA_N / 4; ++i) - __loop__( - invariant(i <= MLDSA_N/4) - invariant(array_bound(r->coeffs, 0, i*4, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - { - r->coeffs[4 * i + 0] = a[9 * i + 0]; - r->coeffs[4 * i + 0] |= (uint32_t)a[9 * i + 1] << 8; - r->coeffs[4 * i + 0] |= (uint32_t)a[9 * i + 2] << 16; - r->coeffs[4 * i + 0] &= 0x3FFFF; - - r->coeffs[4 * i + 1] = a[9 * i + 2] >> 2; - r->coeffs[4 * i + 1] |= (uint32_t)a[9 * i + 3] << 6; - r->coeffs[4 * i + 1] |= (uint32_t)a[9 * i + 4] << 14; - r->coeffs[4 * i + 1] &= 0x3FFFF; - - r->coeffs[4 * i + 2] = a[9 * i + 4] >> 4; - r->coeffs[4 * i + 2] |= (uint32_t)a[9 * i + 5] << 4; - r->coeffs[4 * i + 2] |= (uint32_t)a[9 * i + 6] << 12; - r->coeffs[4 * i + 2] &= 0x3FFFF; - - r->coeffs[4 * i + 3] = a[9 * i + 6] >> 6; - r->coeffs[4 * i + 3] |= (uint32_t)a[9 * i + 7] << 2; - r->coeffs[4 * i + 3] |= (uint32_t)a[9 * i + 8] << 10; - r->coeffs[4 * i + 3] &= 0x3FFFF; - - r->coeffs[4 * i + 0] = MLDSA_GAMMA1 - r->coeffs[4 * i + 0]; - r->coeffs[4 * i + 1] = MLDSA_GAMMA1 - r->coeffs[4 * i + 1]; - 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 /* MLD_CONFIG_PARAMETER_SET == 44 */ - for (i = 0; i < MLDSA_N / 2; ++i) - __loop__( - invariant(i <= MLDSA_N/2) - invariant(array_bound(r->coeffs, 0, i*2, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) - { - r->coeffs[2 * i + 0] = a[5 * i + 0]; - r->coeffs[2 * i + 0] |= (uint32_t)a[5 * i + 1] << 8; - r->coeffs[2 * i + 0] |= (uint32_t)a[5 * i + 2] << 16; - r->coeffs[2 * i + 0] &= 0xFFFFF; - - r->coeffs[2 * i + 1] = a[5 * i + 2] >> 4; - r->coeffs[2 * i + 1] |= (uint32_t)a[5 * i + 3] << 4; - r->coeffs[2 * i + 1] |= (uint32_t)a[5 * i + 4] << 12; - /* r->coeffs[2*i+1] &= 0xFFFFF; */ /* No effect, since we're anyway at 20 - bits */ - - 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 /* MLD_CONFIG_PARAMETER_SET != 44 */ - - mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); -} - -MLD_INTERNAL_API -void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) -{ - unsigned int i; - - mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); - -#if MLD_CONFIG_PARAMETER_SET == 44 - for (i = 0; i < MLDSA_N / 4; ++i) - __loop__( - invariant(i <= MLDSA_N/4)) - { - r[3 * i + 0] = (a->coeffs[4 * i + 0]) & 0xFF; - r[3 * i + 0] |= (a->coeffs[4 * i + 1] << 6) & 0xFF; - r[3 * i + 1] = (a->coeffs[4 * i + 1] >> 2) & 0xFF; - r[3 * i + 1] |= (a->coeffs[4 * i + 2] << 4) & 0xFF; - r[3 * i + 2] = (a->coeffs[4 * i + 2] >> 4) & 0xFF; - r[3 * i + 2] |= (a->coeffs[4 * i + 3] << 2) & 0xFF; - } -#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 /* MLD_CONFIG_PARAMETER_SET != 44 */ -} +#else /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */ +MLD_EMPTY_CU(mld_poly) +#endif /* MLD_CONFIG_MULTILEVEL_NO_SHARED */ diff --git a/mldsa/poly.h b/mldsa/poly.h index 71dbeda33..0257309e7 100644 --- a/mldsa/poly.h +++ b/mldsa/poly.h @@ -385,7 +385,7 @@ __contract__( ensures(array_bound(vec3->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) ); -#define mld_poly_uniform_eta_4x MLD_NAMESPACE(poly_uniform_eta_4x) +#define mld_poly_uniform_eta_4x MLD_NAMESPACE_KL(poly_uniform_eta_4x) /************************************************* * Name: mld_poly_uniform_eta * @@ -425,7 +425,7 @@ __contract__( ensures(array_abs_bound(r3->coeffs, 0, MLDSA_N, MLDSA_ETA + 1)) ); -#define mld_poly_uniform_gamma1 MLD_NAMESPACE(poly_uniform_gamma1) +#define mld_poly_uniform_gamma1 MLD_NAMESPACE_KL(poly_uniform_gamma1) /************************************************* * Name: mld_poly_uniform_gamma1 * @@ -449,7 +449,7 @@ __contract__( ); -#define mld_poly_uniform_gamma1_4x MLD_NAMESPACE(poly_uniform_gamma1_4x) +#define mld_poly_uniform_gamma1_4x MLD_NAMESPACE_KL(poly_uniform_gamma1_4x) /************************************************* * Name: mld_poly_uniform_gamma1_4x * @@ -485,7 +485,7 @@ __contract__( ); -#define mld_poly_challenge MLD_NAMESPACE(poly_challenge) +#define mld_poly_challenge MLD_NAMESPACE_KL(poly_challenge) /************************************************* * Name: mld_poly_challenge * @@ -507,7 +507,7 @@ __contract__( ensures(array_bound(c->coeffs, 0, MLDSA_N, -1, 2)) ); -#define mld_polyeta_pack MLD_NAMESPACE(polyeta_pack) +#define mld_polyeta_pack MLD_NAMESPACE_KL(polyeta_pack) /************************************************* * Name: mld_polyeta_pack * @@ -542,7 +542,7 @@ __contract__( #error "Invalid value of MLDSA_ETA" #endif -#define mld_polyeta_unpack MLD_NAMESPACE(polyeta_unpack) +#define mld_polyeta_unpack MLD_NAMESPACE_KL(polyeta_unpack) /************************************************* * Name: mld_polyeta_unpack * @@ -639,7 +639,7 @@ __contract__( ensures(array_bound(r->coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)) ); -#define mld_polyz_pack MLD_NAMESPACE(polyz_pack) +#define mld_polyz_pack MLD_NAMESPACE_KL(polyz_pack) /************************************************* * Name: mld_polyz_pack * @@ -659,7 +659,7 @@ __contract__( assigns(object_whole(r)) ); -#define mld_polyz_unpack MLD_NAMESPACE(polyz_unpack) +#define mld_polyz_unpack MLD_NAMESPACE_KL(polyz_unpack) /************************************************* * Name: mld_polyz_unpack * @@ -679,7 +679,7 @@ __contract__( ); -#define mld_polyw1_pack MLD_NAMESPACE(polyw1_pack) +#define mld_polyw1_pack MLD_NAMESPACE_KL(polyw1_pack) /************************************************* * Name: mld_polyw1_pack * diff --git a/mldsa/poly_kl.c b/mldsa/poly_kl.c new file mode 100644 index 000000000..1c28cf469 --- /dev/null +++ b/mldsa/poly_kl.c @@ -0,0 +1,790 @@ +/* + * Copyright (c) The mldsa-native project authors + * Copyright (c) The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ + +/* References + * ========== + * + * - [FIPS204] + * FIPS 204 Module-Lattice-Based Digital Signature Standard + * National Institute of Standards and Technology + * https://csrc.nist.gov/pubs/fips/204/final + * + * - [REF] + * CRYSTALS-Dilithium reference implementation + * Bai, Ducas, Kiltz, Lepoint, Lyubashevsky, Schwabe, Seiler, Stehlé + * https://github.com/pq-crystals/dilithium/tree/master/ref + */ + +#include +#include + +#include "ct.h" +#include "debug.h" +#include "poly.h" +#include "rounding.h" +#include "symmetric.h" + + +MLD_INTERNAL_API +void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) +{ +#if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) && MLD_CONFIG_PARAMETER_SET == 44 + /* TODO: proof */ + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + mld_poly_decompose_88_native(a1->coeffs, a0->coeffs, a->coeffs); +#elif defined(MLD_USE_NATIVE_POLY_DECOMPOSE_32) && \ + (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) + /* TODO: proof */ + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + mld_poly_decompose_32_native(a1->coeffs, a0->coeffs, a->coeffs); +#else /* !(MLD_USE_NATIVE_POLY_DECOMPOSE_88 && MLD_CONFIG_PARAMETER_SET == 44) \ + && MLD_USE_NATIVE_POLY_DECOMPOSE_32 && (MLD_CONFIG_PARAMETER_SET == \ + 65 || MLD_CONFIG_PARAMETER_SET == 87) */ + unsigned int i; + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + for (i = 0; i < MLDSA_N; ++i) + __loop__( + assigns(i, memory_slice(a0, sizeof(mld_poly)), memory_slice(a1, sizeof(mld_poly))) + invariant(i <= MLDSA_N) + invariant(array_bound(a1->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + invariant(array_abs_bound(a0->coeffs, 0, i, MLDSA_GAMMA2+1)) + ) + { + mld_decompose(&a0->coeffs[i], &a1->coeffs[i], a->coeffs[i]); + } +#endif /* !(MLD_USE_NATIVE_POLY_DECOMPOSE_88 && MLD_CONFIG_PARAMETER_SET == \ + 44) && !(MLD_USE_NATIVE_POLY_DECOMPOSE_32 && \ + (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)) \ + */ + + mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2 + 1); + mld_assert_bound(a1->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); +} + +MLD_INTERNAL_API +unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, + const mld_poly *a1) +{ + unsigned int i, s = 0; + + for (i = 0; i < MLDSA_N; ++i) + __loop__( + invariant(i <= MLDSA_N) + invariant(s <= i) + invariant(array_bound(h->coeffs, 0, i, 0, 2)) + ) + { + const unsigned int hint_bit = mld_make_hint(a0->coeffs[i], a1->coeffs[i]); + h->coeffs[i] = hint_bit; + s += hint_bit; + } + + mld_assert(s <= MLDSA_N); + mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); + return s; +} + +MLD_INTERNAL_API +void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) +{ +#if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) && MLD_CONFIG_PARAMETER_SET == 44 + /* TODO: proof */ + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); + mld_poly_use_hint_88_native(b->coeffs, a->coeffs, h->coeffs); +#elif defined(MLD_USE_NATIVE_POLY_USE_HINT_32) && \ + (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) + /* TODO: proof */ + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); + mld_poly_use_hint_32_native(b->coeffs, a->coeffs, h->coeffs); +#else /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \ + && MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET == 65 \ + || MLD_CONFIG_PARAMETER_SET == 87) */ + unsigned int i; + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); + + for (i = 0; i < MLDSA_N; ++i) + __loop__( + invariant(i <= MLDSA_N) + invariant(array_bound(b->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ) + { + b->coeffs[i] = mld_use_hint(a->coeffs[i], h->coeffs[i]); + } +#endif /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \ + && !(MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET == \ + 65 || MLD_CONFIG_PARAMETER_SET == 87)) */ + + mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); +} + +/* Reference: explicitly checks the bound B to be <= (MLDSA_Q - 1) / 8). + * This is unnecessary as it's always a compile-time constant. + * We instead model it as a precondition. + * Checking the bound is performed using a conditional arguing + * that it is okay to leak which coefficient violates the bound (while the + * coefficient itself must remain secret). + * We instead perform everything in constant-time. + * Also it is sufficient to check that it is smaller than + * MLDSA_Q - REDUCE32_RANGE_MAX > (MLDSA_Q - 1) / 8). + */ +MLD_INTERNAL_API +uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) +{ +#if defined(MLD_USE_NATIVE_POLY_CHKNORM) + /* TODO: proof */ + mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX); + return mld_poly_chknorm_native(a->coeffs, B); +#else + unsigned int i; + uint32_t t = 0; + mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX); + + + for (i = 0; i < MLDSA_N; ++i) + __loop__( + invariant(i <= MLDSA_N) + invariant(t == 0 || t == 0xFFFFFFFF) + invariant((t == 0) == array_abs_bound(a->coeffs, 0, i, B)) + ) + { + /* + * Since we know that -REDUCE32_RANGE_MAX <= a < REDUCE32_RANGE_MAX, + * and B <= MLDSA_Q - REDUCE32_RANGE_MAX, to check if + * -B < (a mod± MLDSA_Q) < B, it suffices to check if -B < a < B. + * + * We prove this to be true using the following CBMC assertions. + * a ==> b expressed as !a || b to also allow run-time assertion. + */ + mld_assert(a->coeffs[i] < B || a->coeffs[i] - MLDSA_Q <= -B); + mld_assert(a->coeffs[i] > -B || a->coeffs[i] + MLDSA_Q >= B); + + /* Reference: Leaks which coefficient violates the bound via a conditional. + * We are more conservative to reduce the number of declassifications in + * constant-time testing. + */ + + /* if (abs(a[i]) >= B) */ + t |= mld_ct_cmask_neg_i32(B - 1 - mld_ct_abs_i32(a->coeffs[i])); + } + + return t; +#endif /* !MLD_USE_NATIVE_POLY_CHKNORM */ +} + + +/************************************************* + * Name: mld_rej_eta + * + * Description: Sample uniformly random coefficients in [-MLDSA_ETA, MLDSA_ETA] + *by performing rejection sampling on array of random bytes. + * + * Arguments: - int32_t *a: pointer to output array (allocated) + * - unsigned int target: requested number of coefficients to + *sample + * - unsigned int offset: number of coefficients already sampled + * - const uint8_t *buf: array of random bytes to sample from + * - unsigned int buflen: length of array of random bytes + * + * Returns number of sampled coefficients. Can be smaller than target if not + *enough random bytes were given. + **************************************************/ + +/* Reference: `mld_rej_eta()` in the reference implementation @[REF]. + * - Our signature differs from the reference implementation + * in that it adds the offset and always expects the base of the + * target buffer. This avoids shifting the buffer base in the + * caller, which appears tricky to reason about. */ +#if MLDSA_ETA == 2 +/* + * Sampling 256 coefficients mod 15 using rejection sampling from 4 bits. + * Expected number of required bytes: (256 * (16/15))/2 = 136.5 bytes. + * We sample 1 block (=136 bytes) of SHAKE256_RATE output initially. + * Sampling 2 blocks initially results in slightly worse performance. + */ +#define POLY_UNIFORM_ETA_NBLOCKS 1 +#elif MLDSA_ETA == 4 +/* + * Sampling 256 coefficients mod 9 using rejection sampling from 4 bits. + * Expected number of required bytes: (256 * (16/9))/2 = 227.5 bytes. + * We sample 2 blocks (=272 bytes) of SHAKE256_RATE output initially. + */ +#define POLY_UNIFORM_ETA_NBLOCKS 2 +#else /* MLDSA_ETA == 4 */ +#error "Invalid value of MLDSA_ETA" +#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ +static unsigned int mld_rej_eta(int32_t *a, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen) +__contract__( + requires(offset <= target && target <= MLDSA_N) + requires(buflen <= (POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)) + requires(memory_no_alias(a, sizeof(int32_t) * target)) + requires(memory_no_alias(buf, buflen)) + requires(array_abs_bound(a, 0, offset, MLDSA_ETA + 1)) + assigns(memory_slice(a, sizeof(int32_t) * target)) + ensures(offset <= return_value && return_value <= target) + ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) +) +{ + unsigned int ctr, pos; + int t_valid; + uint32_t t0, t1; + mld_assert_abs_bound(a, offset, MLDSA_ETA + 1); + +/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */ +#if MLDSA_ETA == 2 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) + if (offset == 0) + { + int ret = mld_rej_uniform_eta2_native(a, target, buf, buflen); + if (ret != -1) + { + unsigned res = (unsigned)ret; + mld_assert_abs_bound(a, res, MLDSA_ETA + 1); + return res; + } + } +/* TODO: CBMC proof based on mld_rej_uniform_eta4_native */ +#elif MLDSA_ETA == 4 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) + if (offset == 0) + { + int ret = mld_rej_uniform_eta4_native(a, target, buf, buflen); + if (ret != -1) + { + unsigned res = (unsigned)ret; + mld_assert_abs_bound(a, res, MLDSA_ETA + 1); + return res; + } + } +#endif /* !(MLDSA_ETA == 2 && MLD_USE_NATIVE_REJ_UNIFORM_ETA2) && MLDSA_ETA == \ + 4 && MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */ + + ctr = offset; + pos = 0; + while (ctr < target && pos < buflen) + __loop__( + invariant(offset <= ctr && ctr <= target && pos <= buflen) + invariant(array_abs_bound(a, 0, ctr, MLDSA_ETA + 1)) + ) + { + t0 = buf[pos] & 0x0F; + t1 = buf[pos++] >> 4; + + /* Constant time: The inputs and outputs to the rejection sampling are + * secret. However, it is fine to leak which coefficients have been + * rejected. For constant-time testing, we declassify the result of + * the comparison. + */ +#if MLDSA_ETA == 2 + t_valid = t0 < 15; + MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); + if (t_valid) /* t0 < 15 */ + { + t0 = t0 - (205 * t0 >> 10) * 5; + a[ctr++] = 2 - (int32_t)t0; + } + t_valid = t1 < 15; + MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); + if (t_valid && ctr < target) /* t1 < 15 */ + { + t1 = t1 - (205 * t1 >> 10) * 5; + a[ctr++] = 2 - (int32_t)t1; + } +#elif MLDSA_ETA == 4 + t_valid = t0 < 9; + MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); + if (t_valid) /* t0 < 9 */ + { + a[ctr++] = 4 - (int32_t)t0; + } + t_valid = t1 < 9; /* t1 < 9 */ + MLD_CT_TESTING_DECLASSIFY(&t_valid, sizeof(int)); + if (t_valid && ctr < target) + { + a[ctr++] = 4 - (int32_t)t1; + } +#else /* MLDSA_ETA == 4 */ +#error "Invalid value of MLDSA_ETA" +#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ + } + + mld_assert_abs_bound(a, ctr, MLDSA_ETA + 1); + + return ctr; +} + +MLD_INTERNAL_API +void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, + mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES], + uint8_t nonce0, uint8_t nonce1, uint8_t nonce2, + uint8_t nonce3) +{ + /* Temporary buffers for XOF output before rejection sampling */ + MLD_ALIGN uint8_t + buf[4][MLD_ALIGN_UP(POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)]; + + MLD_ALIGN uint8_t extseed[4][MLD_ALIGN_UP(MLDSA_CRHBYTES + 2)]; + + /* Tracks the number of coefficients we have already sampled */ + unsigned ctr[4]; + mld_xof256_x4_ctx state; + unsigned buflen; + + mld_memcpy(extseed[0], seed, MLDSA_CRHBYTES); + mld_memcpy(extseed[1], seed, MLDSA_CRHBYTES); + mld_memcpy(extseed[2], seed, MLDSA_CRHBYTES); + mld_memcpy(extseed[3], seed, MLDSA_CRHBYTES); + extseed[0][MLDSA_CRHBYTES] = nonce0; + extseed[1][MLDSA_CRHBYTES] = nonce1; + extseed[2][MLDSA_CRHBYTES] = nonce2; + extseed[3][MLDSA_CRHBYTES] = nonce3; + extseed[0][MLDSA_CRHBYTES + 1] = 0; + extseed[1][MLDSA_CRHBYTES + 1] = 0; + extseed[2][MLDSA_CRHBYTES + 1] = 0; + extseed[3][MLDSA_CRHBYTES + 1] = 0; + + mld_xof256_x4_init(&state); + mld_xof256_x4_absorb(&state, extseed, MLDSA_CRHBYTES + 2); + + /* + * Initially, squeeze heuristic number of POLY_UNIFORM_ETA_NBLOCKS. + * This should generate the coefficients with high probability. + */ + mld_xof256_x4_squeezeblocks(buf, POLY_UNIFORM_ETA_NBLOCKS, &state); + buflen = POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES; + + ctr[0] = mld_rej_eta(r0->coeffs, MLDSA_N, 0, buf[0], buflen); + ctr[1] = mld_rej_eta(r1->coeffs, MLDSA_N, 0, buf[1], buflen); + ctr[2] = mld_rej_eta(r2->coeffs, MLDSA_N, 0, buf[2], buflen); + ctr[3] = mld_rej_eta(r3->coeffs, MLDSA_N, 0, buf[3], buflen); + + /* + * So long as not all entries have been generated, squeeze + * one more block a time until we're done. + */ + buflen = STREAM256_BLOCKBYTES; + while (ctr[0] < MLDSA_N || ctr[1] < MLDSA_N || ctr[2] < MLDSA_N || + ctr[3] < MLDSA_N) + __loop__( + assigns(ctr, state, memory_slice(r0, sizeof(mld_poly)), + memory_slice(r1, sizeof(mld_poly)), memory_slice(r2, sizeof(mld_poly)), + memory_slice(r3, sizeof(mld_poly)), object_whole(buf[0]), + object_whole(buf[1]), object_whole(buf[2]), + object_whole(buf[3])) + invariant(ctr[0] <= MLDSA_N && ctr[1] <= MLDSA_N) + invariant(ctr[2] <= MLDSA_N && ctr[3] <= MLDSA_N) + invariant(array_abs_bound(r0->coeffs, 0, ctr[0], MLDSA_ETA + 1)) + invariant(array_abs_bound(r1->coeffs, 0, ctr[1], MLDSA_ETA + 1)) + invariant(array_abs_bound(r2->coeffs, 0, ctr[2], MLDSA_ETA + 1)) + invariant(array_abs_bound(r3->coeffs, 0, ctr[3], MLDSA_ETA + 1))) + { + mld_xof256_x4_squeezeblocks(buf, 1, &state); + ctr[0] = mld_rej_eta(r0->coeffs, MLDSA_N, ctr[0], buf[0], buflen); + ctr[1] = mld_rej_eta(r1->coeffs, MLDSA_N, ctr[1], buf[1], buflen); + ctr[2] = mld_rej_eta(r2->coeffs, MLDSA_N, ctr[2], buf[2], buflen); + ctr[3] = mld_rej_eta(r3->coeffs, MLDSA_N, ctr[3], buf[3], buflen); + } + + mld_xof256_x4_release(&state); + + mld_assert_abs_bound(r0->coeffs, MLDSA_N, MLDSA_ETA + 1); + mld_assert_abs_bound(r1->coeffs, MLDSA_N, MLDSA_ETA + 1); + mld_assert_abs_bound(r2->coeffs, MLDSA_N, MLDSA_ETA + 1); + mld_assert_abs_bound(r3->coeffs, MLDSA_N, MLDSA_ETA + 1); + + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(buf, sizeof(buf)); + mld_zeroize(extseed, sizeof(extseed)); +} + + +#define POLY_UNIFORM_GAMMA1_NBLOCKS \ + ((MLDSA_POLYZ_PACKEDBYTES + STREAM256_BLOCKBYTES - 1) / STREAM256_BLOCKBYTES) +MLD_INTERNAL_API +void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES], + uint16_t nonce) +{ + MLD_ALIGN uint8_t buf[POLY_UNIFORM_GAMMA1_NBLOCKS * STREAM256_BLOCKBYTES]; + MLD_ALIGN uint8_t extseed[MLDSA_CRHBYTES + 2]; + mld_xof256_ctx state; + + mld_memcpy(extseed, seed, MLDSA_CRHBYTES); + extseed[MLDSA_CRHBYTES] = nonce & 0xFF; + extseed[MLDSA_CRHBYTES + 1] = nonce >> 8; + + mld_xof256_init(&state); + mld_xof256_absorb_once(&state, extseed, MLDSA_CRHBYTES + 2); + + mld_xof256_squeezeblocks(buf, POLY_UNIFORM_GAMMA1_NBLOCKS, &state); + mld_polyz_unpack(a, buf); + + mld_xof256_release(&state); + + mld_assert_bound(a->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(buf, sizeof(buf)); + mld_zeroize(extseed, sizeof(extseed)); +} + +MLD_INTERNAL_API +void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2, + mld_poly *r3, + const uint8_t seed[MLDSA_CRHBYTES], + uint16_t nonce0, uint16_t nonce1, + uint16_t nonce2, uint16_t nonce3) +{ + /* Temporary buffers for XOF output before rejection sampling */ + MLD_ALIGN uint8_t + buf[4][MLD_ALIGN_UP(POLY_UNIFORM_GAMMA1_NBLOCKS * STREAM256_BLOCKBYTES)]; + + MLD_ALIGN uint8_t extseed[4][MLD_ALIGN_UP(MLDSA_CRHBYTES + 2)]; + + /* Tracks the number of coefficients we have already sampled */ + mld_xof256_x4_ctx state; + + mld_memcpy(extseed[0], seed, MLDSA_CRHBYTES); + mld_memcpy(extseed[1], seed, MLDSA_CRHBYTES); + mld_memcpy(extseed[2], seed, MLDSA_CRHBYTES); + mld_memcpy(extseed[3], seed, MLDSA_CRHBYTES); + extseed[0][MLDSA_CRHBYTES] = nonce0 & 0xFF; + extseed[1][MLDSA_CRHBYTES] = nonce1 & 0xFF; + extseed[2][MLDSA_CRHBYTES] = nonce2 & 0xFF; + extseed[3][MLDSA_CRHBYTES] = nonce3 & 0xFF; + extseed[0][MLDSA_CRHBYTES + 1] = nonce0 >> 8; + extseed[1][MLDSA_CRHBYTES + 1] = nonce1 >> 8; + extseed[2][MLDSA_CRHBYTES + 1] = nonce2 >> 8; + extseed[3][MLDSA_CRHBYTES + 1] = nonce3 >> 8; + + mld_xof256_x4_init(&state); + mld_xof256_x4_absorb(&state, extseed, MLDSA_CRHBYTES + 2); + mld_xof256_x4_squeezeblocks(buf, POLY_UNIFORM_GAMMA1_NBLOCKS, &state); + + mld_polyz_unpack(r0, buf[0]); + mld_polyz_unpack(r1, buf[1]); + mld_polyz_unpack(r2, buf[2]); + mld_polyz_unpack(r3, buf[3]); + mld_xof256_x4_release(&state); + + mld_assert_bound(r0->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + mld_assert_bound(r1->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + mld_assert_bound(r2->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + mld_assert_bound(r3->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(buf, sizeof(buf)); + mld_zeroize(extseed, sizeof(extseed)); +} + +MLD_INTERNAL_API +void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES]) +{ + unsigned int i, j, pos; + uint64_t signs; + uint64_t offset; + MLD_ALIGN uint8_t buf[SHAKE256_RATE]; + mld_shake256ctx state; + + mld_shake256_init(&state); + mld_shake256_absorb(&state, seed, MLDSA_CTILDEBYTES); + mld_shake256_finalize(&state); + mld_shake256_squeeze(buf, SHAKE256_RATE, &state); + + /* Convert the first 8 bytes of buf[] into an unsigned 64-bit value. */ + /* Each bit of that dictates the sign of the resulting challenge value */ + signs = 0; + for (i = 0; i < 8; ++i) + __loop__( + assigns(i, signs) + invariant(i <= 8) + ) + { + signs |= (uint64_t)buf[i] << 8 * i; + } + pos = 8; + + mld_memset(c, 0, sizeof(mld_poly)); + + for (i = MLDSA_N - MLDSA_TAU; i < MLDSA_N; ++i) + __loop__( + assigns(i, j, object_whole(buf), state, pos, memory_slice(c, sizeof(mld_poly)), signs) + invariant(i >= MLDSA_N - MLDSA_TAU) + invariant(i <= MLDSA_N) + invariant(pos >= 1) + invariant(pos <= SHAKE256_RATE) + invariant(array_bound(c->coeffs, 0, MLDSA_N, -1, 2)) + invariant(state.pos <= SHAKE256_RATE) + ) + { + do + __loop__( + assigns(j, object_whole(buf), state, pos) + invariant(state.pos <= SHAKE256_RATE) + ) + { + if (pos >= SHAKE256_RATE) + { + mld_shake256_squeeze(buf, SHAKE256_RATE, &state); + pos = 0; + } + j = buf[pos++]; + } while (j > i); + + c->coeffs[i] = c->coeffs[j]; + + /* Reference: Compute coefficent value here in two steps to */ + /* mixinf unsigned and signed arithmetic with implicit */ + /* conversions, and so that CBMC can keep track of ranges */ + /* to complete type-safety proof here. */ + + /* The least-significant bit of signs tells us if we want -1 or +1 */ + offset = 2 * (signs & 1); + + /* offset has value 0 or 2 here, so (1 - (int32_t) offset) has + * value -1 or +1 */ + c->coeffs[j] = 1 - (int32_t)offset; + + /* Move to the next bit of signs for next time */ + signs >>= 1; + } + + mld_assert_bound(c->coeffs, MLDSA_N, -1, 2); + mld_shake256_release(&state); + + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(buf, sizeof(buf)); + mld_zeroize(&signs, sizeof(signs)); +} + +MLD_INTERNAL_API +void mld_polyeta_pack(uint8_t *r, const mld_poly *a) +{ + unsigned int i; + uint8_t t[8]; + + mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_ETA + 1); + +#if MLDSA_ETA == 2 + for (i = 0; i < MLDSA_N / 8; ++i) + __loop__( + invariant(i <= MLDSA_N/8)) + { + t[0] = MLDSA_ETA - a->coeffs[8 * i + 0]; + t[1] = MLDSA_ETA - a->coeffs[8 * i + 1]; + t[2] = MLDSA_ETA - a->coeffs[8 * i + 2]; + t[3] = MLDSA_ETA - a->coeffs[8 * i + 3]; + t[4] = MLDSA_ETA - a->coeffs[8 * i + 4]; + t[5] = MLDSA_ETA - a->coeffs[8 * i + 5]; + t[6] = MLDSA_ETA - a->coeffs[8 * i + 6]; + t[7] = MLDSA_ETA - a->coeffs[8 * i + 7]; + + r[3 * i + 0] = ((t[0] >> 0) | (t[1] << 3) | (t[2] << 6)) & 0xFF; + r[3 * i + 1] = + ((t[2] >> 2) | (t[3] << 1) | (t[4] << 4) | (t[5] << 7)) & 0xFF; + r[3 * i + 2] = ((t[5] >> 1) | (t[6] << 2) | (t[7] << 5)) & 0xFF; + } +#elif MLDSA_ETA == 4 + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2)) + { + t[0] = MLDSA_ETA - a->coeffs[2 * i + 0]; + t[1] = MLDSA_ETA - a->coeffs[2 * i + 1]; + r[i] = t[0] | (t[1] << 4); + } +#else /* MLDSA_ETA == 4 */ +#error "Invalid value of MLDSA_ETA" +#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ +} + +void mld_polyeta_unpack(mld_poly *r, const uint8_t *a) +{ + unsigned int i; + +#if MLDSA_ETA == 2 + for (i = 0; i < MLDSA_N / 8; ++i) + __loop__( + invariant(i <= MLDSA_N/8) + invariant(array_bound(r->coeffs, 0, i*8, -5, MLDSA_ETA + 1))) + { + r->coeffs[8 * i + 0] = (a[3 * i + 0] >> 0) & 7; + r->coeffs[8 * i + 1] = (a[3 * i + 0] >> 3) & 7; + r->coeffs[8 * i + 2] = ((a[3 * i + 0] >> 6) | (a[3 * i + 1] << 2)) & 7; + r->coeffs[8 * i + 3] = (a[3 * i + 1] >> 1) & 7; + r->coeffs[8 * i + 4] = (a[3 * i + 1] >> 4) & 7; + r->coeffs[8 * i + 5] = ((a[3 * i + 1] >> 7) | (a[3 * i + 2] << 1)) & 7; + r->coeffs[8 * i + 6] = (a[3 * i + 2] >> 2) & 7; + r->coeffs[8 * i + 7] = (a[3 * i + 2] >> 5) & 7; + + r->coeffs[8 * i + 0] = MLDSA_ETA - r->coeffs[8 * i + 0]; + r->coeffs[8 * i + 1] = MLDSA_ETA - r->coeffs[8 * i + 1]; + r->coeffs[8 * i + 2] = MLDSA_ETA - r->coeffs[8 * i + 2]; + r->coeffs[8 * i + 3] = MLDSA_ETA - r->coeffs[8 * i + 3]; + r->coeffs[8 * i + 4] = MLDSA_ETA - r->coeffs[8 * i + 4]; + r->coeffs[8 * i + 5] = MLDSA_ETA - r->coeffs[8 * i + 5]; + r->coeffs[8 * i + 6] = MLDSA_ETA - r->coeffs[8 * i + 6]; + r->coeffs[8 * i + 7] = MLDSA_ETA - r->coeffs[8 * i + 7]; + } +#elif MLDSA_ETA == 4 + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2) + invariant(array_bound(r->coeffs, 0, i*2, -11, MLDSA_ETA + 1))) + { + r->coeffs[2 * i + 0] = a[i] & 0x0F; + r->coeffs[2 * i + 1] = a[i] >> 4; + r->coeffs[2 * i + 0] = MLDSA_ETA - r->coeffs[2 * i + 0]; + r->coeffs[2 * i + 1] = MLDSA_ETA - r->coeffs[2 * i + 1]; + } +#else /* MLDSA_ETA == 4 */ +#error "Invalid value of MLDSA_ETA" +#endif /* MLDSA_ETA != 2 && MLDSA_ETA != 4 */ + + mld_assert_bound(r->coeffs, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, + MLDSA_ETA + 1); +} + + +MLD_INTERNAL_API +void mld_polyz_pack(uint8_t *r, const mld_poly *a) +{ + unsigned int i; + uint32_t t[4]; + + mld_assert_bound(a->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); + +#if MLD_CONFIG_PARAMETER_SET == 44 + for (i = 0; i < MLDSA_N / 4; ++i) + __loop__( + invariant(i <= MLDSA_N/4)) + { + t[0] = MLDSA_GAMMA1 - a->coeffs[4 * i + 0]; + t[1] = MLDSA_GAMMA1 - a->coeffs[4 * i + 1]; + t[2] = MLDSA_GAMMA1 - a->coeffs[4 * i + 2]; + t[3] = MLDSA_GAMMA1 - a->coeffs[4 * i + 3]; + + r[9 * i + 0] = (t[0]) & 0xFF; + r[9 * i + 1] = (t[0] >> 8) & 0xFF; + r[9 * i + 2] = (t[0] >> 16) & 0xFF; + r[9 * i + 2] |= (t[1] << 2) & 0xFF; + r[9 * i + 3] = (t[1] >> 6) & 0xFF; + r[9 * i + 4] = (t[1] >> 14) & 0xFF; + r[9 * i + 4] |= (t[2] << 4) & 0xFF; + r[9 * i + 5] = (t[2] >> 4) & 0xFF; + r[9 * i + 6] = (t[2] >> 12) & 0xFF; + r[9 * i + 6] |= (t[3] << 6) & 0xFF; + r[9 * i + 7] = (t[3] >> 2) & 0xFF; + r[9 * i + 8] = (t[3] >> 10) & 0xFF; + } +#else /* MLD_CONFIG_PARAMETER_SET == 44 */ + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2)) + { + t[0] = MLDSA_GAMMA1 - a->coeffs[2 * i + 0]; + t[1] = MLDSA_GAMMA1 - a->coeffs[2 * i + 1]; + + r[5 * i + 0] = (t[0]) & 0xFF; + r[5 * i + 1] = (t[0] >> 8) & 0xFF; + r[5 * i + 2] = (t[0] >> 16) & 0xFF; + r[5 * i + 2] |= (t[1] << 4) & 0xFF; + r[5 * i + 3] = (t[1] >> 4) & 0xFF; + r[5 * i + 4] = (t[1] >> 12) & 0xFF; + } +#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ +} + +MLD_INTERNAL_API +void mld_polyz_unpack(mld_poly *r, const uint8_t *a) +{ + unsigned int i; + +#if MLD_CONFIG_PARAMETER_SET == 44 + for (i = 0; i < MLDSA_N / 4; ++i) + __loop__( + invariant(i <= MLDSA_N/4) + invariant(array_bound(r->coeffs, 0, i*4, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) + { + r->coeffs[4 * i + 0] = a[9 * i + 0]; + r->coeffs[4 * i + 0] |= (uint32_t)a[9 * i + 1] << 8; + r->coeffs[4 * i + 0] |= (uint32_t)a[9 * i + 2] << 16; + r->coeffs[4 * i + 0] &= 0x3FFFF; + + r->coeffs[4 * i + 1] = a[9 * i + 2] >> 2; + r->coeffs[4 * i + 1] |= (uint32_t)a[9 * i + 3] << 6; + r->coeffs[4 * i + 1] |= (uint32_t)a[9 * i + 4] << 14; + r->coeffs[4 * i + 1] &= 0x3FFFF; + + r->coeffs[4 * i + 2] = a[9 * i + 4] >> 4; + r->coeffs[4 * i + 2] |= (uint32_t)a[9 * i + 5] << 4; + r->coeffs[4 * i + 2] |= (uint32_t)a[9 * i + 6] << 12; + r->coeffs[4 * i + 2] &= 0x3FFFF; + + r->coeffs[4 * i + 3] = a[9 * i + 6] >> 6; + r->coeffs[4 * i + 3] |= (uint32_t)a[9 * i + 7] << 2; + r->coeffs[4 * i + 3] |= (uint32_t)a[9 * i + 8] << 10; + r->coeffs[4 * i + 3] &= 0x3FFFF; + + r->coeffs[4 * i + 0] = MLDSA_GAMMA1 - r->coeffs[4 * i + 0]; + r->coeffs[4 * i + 1] = MLDSA_GAMMA1 - r->coeffs[4 * i + 1]; + 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 /* MLD_CONFIG_PARAMETER_SET == 44 */ + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2) + invariant(array_bound(r->coeffs, 0, i*2, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) + { + r->coeffs[2 * i + 0] = a[5 * i + 0]; + r->coeffs[2 * i + 0] |= (uint32_t)a[5 * i + 1] << 8; + r->coeffs[2 * i + 0] |= (uint32_t)a[5 * i + 2] << 16; + r->coeffs[2 * i + 0] &= 0xFFFFF; + + r->coeffs[2 * i + 1] = a[5 * i + 2] >> 4; + r->coeffs[2 * i + 1] |= (uint32_t)a[5 * i + 3] << 4; + r->coeffs[2 * i + 1] |= (uint32_t)a[5 * i + 4] << 12; + /* r->coeffs[2*i+1] &= 0xFFFFF; */ /* No effect, since we're anyway at 20 + bits */ + + 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 /* MLD_CONFIG_PARAMETER_SET != 44 */ + + mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); +} + +MLD_INTERNAL_API +void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) +{ + unsigned int i; + + mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); + +#if MLD_CONFIG_PARAMETER_SET == 44 + for (i = 0; i < MLDSA_N / 4; ++i) + __loop__( + invariant(i <= MLDSA_N/4)) + { + r[3 * i + 0] = (a->coeffs[4 * i + 0]) & 0xFF; + r[3 * i + 0] |= (a->coeffs[4 * i + 1] << 6) & 0xFF; + r[3 * i + 1] = (a->coeffs[4 * i + 1] >> 2) & 0xFF; + r[3 * i + 1] |= (a->coeffs[4 * i + 2] << 4) & 0xFF; + r[3 * i + 2] = (a->coeffs[4 * i + 2] >> 4) & 0xFF; + r[3 * i + 2] |= (a->coeffs[4 * i + 3] << 2) & 0xFF; + } +#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 /* MLD_CONFIG_PARAMETER_SET != 44 */ +} diff --git a/mldsa/polyvec.h b/mldsa/polyvec.h index 563759b70..2ab048f2f 100644 --- a/mldsa/polyvec.h +++ b/mldsa/polyvec.h @@ -16,7 +16,9 @@ typedef struct mld_poly vec[MLDSA_L]; } mld_polyvecl; -#define mld_polyvecl_uniform_gamma1 MLD_NAMESPACE(polyvecl_uniform_gamma1) +#define mld_polyvecl MLD_ADD_PARAM_SET(mld_polyvecl) + +#define mld_polyvecl_uniform_gamma1 MLD_NAMESPACE_KL(polyvecl_uniform_gamma1) /************************************************* * Name: mld_polyvecl_uniform_gamma1 * @@ -42,7 +44,7 @@ __contract__( array_bound(v->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ); -#define mld_polyvecl_reduce MLD_NAMESPACE(polyvecl_reduce) +#define mld_polyvecl_reduce MLD_NAMESPACE_KL(polyvecl_reduce) /************************************************* * Name: mld_polyvecl_reduce * @@ -63,7 +65,7 @@ __contract__( array_bound(v->vec[k1].coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX))) ); -#define mld_polyvecl_add MLD_NAMESPACE(polyvecl_add) +#define mld_polyvecl_add MLD_NAMESPACE_KL(polyvecl_add) /************************************************* * Name: mld_polyvecl_add * @@ -88,7 +90,7 @@ __contract__( array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) ); -#define mld_polyvecl_ntt MLD_NAMESPACE(polyvecl_ntt) +#define mld_polyvecl_ntt MLD_NAMESPACE_KL(polyvecl_ntt) /************************************************* * Name: mld_polyvecl_ntt * @@ -106,7 +108,7 @@ __contract__( ensures(forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ); -#define mld_polyvecl_invntt_tomont MLD_NAMESPACE(polyvecl_invntt_tomont) +#define mld_polyvecl_invntt_tomont MLD_NAMESPACE_KL(polyvecl_invntt_tomont) /************************************************* * Name: mld_polyvecl_invntt_tomont * @@ -127,7 +129,7 @@ __contract__( ); #define mld_polyvecl_pointwise_poly_montgomery \ - MLD_NAMESPACE(polyvecl_pointwise_poly_montgomery) + MLD_NAMESPACE_KL(polyvecl_pointwise_poly_montgomery) /************************************************* * Name: mld_polyvecl_pointwise_poly_montgomery * @@ -153,7 +155,7 @@ __contract__( ); #define mld_polyvecl_pointwise_acc_montgomery \ - MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery) + MLD_NAMESPACE_KL(polyvecl_pointwise_acc_montgomery) /************************************************* * Name: mld_polyvecl_pointwise_acc_montgomery * @@ -191,7 +193,7 @@ __contract__( ); -#define mld_polyvecl_chknorm MLD_NAMESPACE(polyvecl_chknorm) +#define mld_polyvecl_chknorm MLD_NAMESPACE_KL(polyvecl_chknorm) /************************************************* * Name: mld_polyvecl_chknorm * @@ -221,7 +223,9 @@ typedef struct mld_poly vec[MLDSA_K]; } mld_polyveck; -#define mld_polyveck_reduce MLD_NAMESPACE(polyveck_reduce) +#define mld_polyveck MLD_ADD_PARAM_SET(mld_polyveck) + +#define mld_polyveck_reduce MLD_NAMESPACE_KL(polyveck_reduce) /************************************************* * Name: polyveck_reduce * @@ -241,7 +245,7 @@ __contract__( array_bound(v->vec[k1].coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX))) ); -#define mld_polyveck_caddq MLD_NAMESPACE(polyveck_caddq) +#define mld_polyveck_caddq MLD_NAMESPACE_KL(polyveck_caddq) /************************************************* * Name: mld_polyveck_caddq * @@ -261,7 +265,7 @@ __contract__( array_bound(v->vec[k1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) ); -#define mld_polyveck_add MLD_NAMESPACE(polyveck_add) +#define mld_polyveck_add MLD_NAMESPACE_KL(polyveck_add) /************************************************* * Name: mld_polyveck_add * @@ -286,7 +290,7 @@ __contract__( array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) ); -#define mld_polyveck_sub MLD_NAMESPACE(polyveck_sub) +#define mld_polyveck_sub MLD_NAMESPACE_KL(polyveck_sub) /************************************************* * Name: mld_polyveck_sub * @@ -309,7 +313,7 @@ __contract__( array_bound(u->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE32_DOMAIN_MAX))) ); -#define mld_polyveck_shiftl MLD_NAMESPACE(polyveck_shiftl) +#define mld_polyveck_shiftl MLD_NAMESPACE_KL(polyveck_shiftl) /************************************************* * Name: mld_polyveck_shiftl * @@ -328,7 +332,7 @@ __contract__( ensures(forall(k1, 0, MLDSA_K, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) ); -#define mld_polyveck_ntt MLD_NAMESPACE(polyveck_ntt) +#define mld_polyveck_ntt MLD_NAMESPACE_KL(polyveck_ntt) /************************************************* * Name: mld_polyveck_ntt * @@ -346,7 +350,7 @@ __contract__( ensures(forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ); -#define mld_polyveck_invntt_tomont MLD_NAMESPACE(polyveck_invntt_tomont) +#define mld_polyveck_invntt_tomont MLD_NAMESPACE_KL(polyveck_invntt_tomont) /************************************************* * Name: mld_polyveck_invntt_tomont * @@ -366,7 +370,7 @@ __contract__( ); #define mld_polyveck_pointwise_poly_montgomery \ - MLD_NAMESPACE(polyveck_pointwise_poly_montgomery) + MLD_NAMESPACE_KL(polyveck_pointwise_poly_montgomery) /************************************************* * Name: mld_polyveck_pointwise_poly_montgomery * @@ -391,7 +395,7 @@ __contract__( ensures(forall(k1, 0, MLDSA_K, array_abs_bound(r->vec[k1].coeffs, 0, MLDSA_N, MLDSA_Q))) ); -#define mld_polyveck_chknorm MLD_NAMESPACE(polyveck_chknorm) +#define mld_polyveck_chknorm MLD_NAMESPACE_KL(polyveck_chknorm) /************************************************* * Name: mld_polyveck_chknorm * @@ -416,7 +420,7 @@ __contract__( ensures((return_value == 0) == forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, B))) ); -#define mld_polyveck_power2round MLD_NAMESPACE(polyveck_power2round) +#define mld_polyveck_power2round MLD_NAMESPACE_KL(polyveck_power2round) /************************************************* * Name: mld_polyveck_power2round * @@ -445,7 +449,7 @@ __contract__( ensures(forall(k2, 0, MLDSA_K, array_bound(v1->vec[k2].coeffs, 0, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1))) ); -#define mld_polyveck_decompose MLD_NAMESPACE(polyveck_decompose) +#define mld_polyveck_decompose MLD_NAMESPACE_KL(polyveck_decompose) /************************************************* * Name: mld_polyveck_decompose * @@ -478,7 +482,7 @@ __contract__( array_abs_bound(v0->vec[k2].coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1))) ); -#define mld_polyveck_make_hint MLD_NAMESPACE(polyveck_make_hint) +#define mld_polyveck_make_hint MLD_NAMESPACE_KL(polyveck_make_hint) /************************************************* * Name: mld_polyveck_make_hint * @@ -502,7 +506,7 @@ __contract__( ensures(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) ); -#define mld_polyveck_use_hint MLD_NAMESPACE(polyveck_use_hint) +#define mld_polyveck_use_hint MLD_NAMESPACE_KL(polyveck_use_hint) /************************************************* * Name: mld_polyveck_use_hint * @@ -529,7 +533,7 @@ __contract__( array_bound(w->vec[k2].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))) ); -#define mld_polyveck_pack_w1 MLD_NAMESPACE(polyveck_pack_w1) +#define mld_polyveck_pack_w1 MLD_NAMESPACE_KL(polyveck_pack_w1) /************************************************* * Name: mld_polyveck_pack_w1 * @@ -552,7 +556,7 @@ __contract__( assigns(object_whole(r)) ); -#define mld_polyveck_pack_eta MLD_NAMESPACE(polyveck_pack_eta) +#define mld_polyveck_pack_eta MLD_NAMESPACE_KL(polyveck_pack_eta) /************************************************* * Name: mld_polyveck_pack_eta * @@ -574,7 +578,7 @@ __contract__( assigns(object_whole(r)) ); -#define mld_polyvecl_pack_eta MLD_NAMESPACE(polyvecl_pack_eta) +#define mld_polyvecl_pack_eta MLD_NAMESPACE_KL(polyvecl_pack_eta) /************************************************* * Name: mld_polyvecl_pack_eta * @@ -596,7 +600,7 @@ __contract__( assigns(object_whole(r)) ); -#define mld_polyvecl_pack_z MLD_NAMESPACE(polyvecl_pack_z) +#define mld_polyvecl_pack_z MLD_NAMESPACE_KL(polyvecl_pack_z) /************************************************* * Name: mld_polyvecl_pack_z * @@ -618,7 +622,7 @@ __contract__( assigns(object_whole(r)) ); -#define mld_polyveck_pack_t0 MLD_NAMESPACE(polyveck_pack_t0) +#define mld_polyveck_pack_t0 MLD_NAMESPACE_KL(polyveck_pack_t0) /************************************************* * Name: mld_polyveck_pack_t0 * @@ -640,7 +644,7 @@ __contract__( assigns(object_whole(r)) ); -#define mld_polyvecl_unpack_eta MLD_NAMESPACE(polyvecl_unpack_eta) +#define mld_polyvecl_unpack_eta MLD_NAMESPACE_KL(polyvecl_unpack_eta) /************************************************* * Name: mld_polyvecl_unpack_eta * @@ -662,7 +666,7 @@ __contract__( array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) ); -#define mld_polyvecl_unpack_z MLD_NAMESPACE(polyvecl_unpack_z) +#define mld_polyvecl_unpack_z MLD_NAMESPACE_KL(polyvecl_unpack_z) /************************************************* * Name: mld_polyvecl_unpack_z * @@ -684,7 +688,7 @@ __contract__( array_bound(z->vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ); -#define mld_polyveck_unpack_eta MLD_NAMESPACE(polyveck_unpack_eta) +#define mld_polyveck_unpack_eta MLD_NAMESPACE_KL(polyveck_unpack_eta) /************************************************* * Name: mld_polyveck_unpack_eta * @@ -706,7 +710,7 @@ __contract__( array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))) ); -#define mld_polyveck_unpack_t0 MLD_NAMESPACE(polyveck_unpack_t0) +#define mld_polyveck_unpack_t0 MLD_NAMESPACE_KL(polyveck_unpack_t0) /************************************************* * Name: mld_polyveck_unpack_t0 * @@ -728,7 +732,7 @@ __contract__( array_bound(p->vec[k1].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))) ); -#define mld_polyvec_matrix_expand MLD_NAMESPACE(polyvec_matrix_expand) +#define mld_polyvec_matrix_expand MLD_NAMESPACE_KL(polyvec_matrix_expand) /************************************************* * Name: mld_polyvec_matrix_expand * @@ -753,7 +757,7 @@ __contract__( #define mld_polyvec_matrix_pointwise_montgomery \ - MLD_NAMESPACE(polyvec_matrix_pointwise_montgomery) + MLD_NAMESPACE_KL(polyvec_matrix_pointwise_montgomery) /************************************************* * Name: mld_polyvec_matrix_pointwise_montgomery * diff --git a/mldsa/sign.h b/mldsa/sign.h index 0024afca7..abdb8ad6a 100644 --- a/mldsa/sign.h +++ b/mldsa/sign.h @@ -23,7 +23,17 @@ #include "polyvec.h" #include "sys.h" -#define crypto_sign_keypair_internal MLD_NAMESPACE(keypair_internal) +#define crypto_sign_keypair_internal MLD_NAMESPACE_KL(keypair_internal) +#define crypto_sign_keypair MLD_NAMESPACE_KL(keypair) +#define crypto_sign_signature_internal MLD_NAMESPACE_KL(signature_internal) +#define crypto_sign_signature MLD_NAMESPACE_KL(signature) +#define crypto_sign_signature_extmu MLD_NAMESPACE_KL(signature_extmu) +#define crypto_sign MLD_NAMESPACE_KL(crypto_sign) +#define crypto_sign_verify_internal MLD_NAMESPACE_KL(verify_internal) +#define crypto_sign_verify MLD_NAMESPACE_KL(verify) +#define crypto_sign_verify_extmu MLD_NAMESPACE_KL(verify_extmu) +#define crypto_sign_open MLD_NAMESPACE_KL(open) + /************************************************* * Name: crypto_sign_keypair_internal * @@ -56,7 +66,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_keypair MLD_NAMESPACE(keypair) /************************************************* * Name: crypto_sign_keypair * @@ -85,7 +94,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_signature_internal MLD_NAMESPACE(signature_internal) /************************************************* * Name: crypto_sign_signature_internal * @@ -134,7 +142,6 @@ __contract__( (return_value == -1 && *siglen == 0)) ); -#define crypto_sign_signature MLD_NAMESPACE(signature) /************************************************* * Name: crypto_sign_signature * @@ -174,7 +181,6 @@ __contract__( (return_value == -1 && *siglen == 0)) ); -#define crypto_sign_signature_extmu MLD_NAMESPACE(signature_extmu) /************************************************* * Name: crypto_sign_signature_extmu * @@ -208,7 +214,6 @@ __contract__( (return_value == -1 && *siglen == 0)) ); -#define crypto_sign MLD_NAMESPACETOP /************************************************* * Name: crypto_sign * @@ -245,7 +250,6 @@ __contract__( (return_value == -1)) ); -#define crypto_sign_verify_internal MLD_NAMESPACE(verify_internal) /************************************************* * Name: crypto_sign_verify_internal * @@ -282,7 +286,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_verify MLD_NAMESPACE(verify) /************************************************* * Name: crypto_sign_verify * @@ -318,7 +321,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_verify_extmu MLD_NAMESPACE(verify_extmu) /************************************************* * Name: crypto_sign_verify_extmu * @@ -348,7 +350,6 @@ __contract__( ensures(return_value == 0 || return_value == -1) ); -#define crypto_sign_open MLD_NAMESPACE(open) /************************************************* * Name: crypto_sign_open * diff --git a/proofs/cbmc/Makefile_params.common b/proofs/cbmc/Makefile_params.common index 4ac0f339a..791b8f5bf 100644 --- a/proofs/cbmc/Makefile_params.common +++ b/proofs/cbmc/Makefile_params.common @@ -9,13 +9,13 @@ MLD_CONFIG_PARAMETER_SET ?= 65 FIPS202_NAMESPACE = mldsa_fips202_ref_ ifeq ($(MLD_CONFIG_PARAMETER_SET),44) - MLD_NAMESPACETOP=PQCP_MLDSA_NATIVE_MLDSA44 + MLD_NAMESPACE_KL=PQCP_MLDSA_NATIVE_MLDSA44_ MLD_NAMESPACE=PQCP_MLDSA_NATIVE_MLDSA44_ else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) - MLD_NAMESPACETOP=PQCP_MLDSA_NATIVE_MLDSA65 + MLD_NAMESPACE_KL=PQCP_MLDSA_NATIVE_MLDSA65_ MLD_NAMESPACE=PQCP_MLDSA_NATIVE_MLDSA65_ else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) - MLD_NAMESPACETOP=PQCP_MLDSA_NATIVE_MLDSA87 + MLD_NAMESPACE_KL=PQCP_MLDSA_NATIVE_MLDSA87_ MLD_NAMESPACE=PQCP_MLDSA_NATIVE_MLDSA87_ else $(error Invalid value of MLD_CONFIG_PARAMETER_SET) diff --git a/proofs/cbmc/crypto_sign/Makefile b/proofs/cbmc/crypto_sign/Makefile index dd9e2c32d..438e3dbf0 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_NAMESPACE)crypto_sign USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature APPLY_LOOP_CONTRACTS=on diff --git a/proofs/cbmc/poly_challenge/Makefile b/proofs/cbmc/poly_challenge/Makefile index c972eb2b8..c8a704926 100644 --- a/proofs/cbmc/poly_challenge/Makefile +++ b/proofs/cbmc/poly_challenge/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_challenge USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_finalize $(FIPS202_NAMESPACE)shake256_squeeze $(FIPS202_NAMESPACE)shake256_release diff --git a/proofs/cbmc/poly_chknorm/Makefile b/proofs/cbmc/poly_chknorm/Makefile index a0544ad2f..c17279c77 100644 --- a/proofs/cbmc/poly_chknorm/Makefile +++ b/proofs/cbmc/poly_chknorm/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm USE_FUNCTION_CONTRACTS=mld_ct_abs_i32 mld_ct_cmask_neg_i32 diff --git a/proofs/cbmc/poly_decompose/Makefile b/proofs/cbmc/poly_decompose/Makefile index 5b50ef873..ecc35ffde 100644 --- a/proofs/cbmc/poly_decompose/Makefile +++ b/proofs/cbmc/poly_decompose/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_decompose USE_FUNCTION_CONTRACTS=mld_decompose diff --git a/proofs/cbmc/poly_make_hint/Makefile b/proofs/cbmc/poly_make_hint/Makefile index 223865692..ecd0218ba 100644 --- a/proofs/cbmc/poly_make_hint/Makefile +++ b/proofs/cbmc/poly_make_hint/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_make_hint USE_FUNCTION_CONTRACTS=mld_make_hint diff --git a/proofs/cbmc/poly_uniform_eta_4x/Makefile b/proofs/cbmc/poly_uniform_eta_4x/Makefile index c36e03f62..df5a87421 100644 --- a/proofs/cbmc/poly_uniform_eta_4x/Makefile +++ b/proofs/cbmc/poly_uniform_eta_4x/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202x4.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c $(SRCDIR)/mldsa/fips202/fips202x4.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta_4x USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256x4_absorb_once $(FIPS202_NAMESPACE)shake256x4_squeezeblocks mld_rej_eta diff --git a/proofs/cbmc/poly_uniform_gamma1/Makefile b/proofs/cbmc/poly_uniform_gamma1/Makefile index 973d9156c..26055c9e2 100644 --- a/proofs/cbmc/poly_uniform_gamma1/Makefile +++ b/proofs/cbmc/poly_uniform_gamma1/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.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_squeeze $(FIPS202_NAMESPACE)shake256_release $(MLD_NAMESPACE)polyz_unpack diff --git a/proofs/cbmc/poly_uniform_gamma1_4x/Makefile b/proofs/cbmc/poly_uniform_gamma1_4x/Makefile index e3e497bfd..15cf4c4a0 100644 --- a/proofs/cbmc/poly_uniform_gamma1_4x/Makefile +++ b/proofs/cbmc/poly_uniform_gamma1_4x/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c $(SRCDIR)/mldsa/fips202/fips202x4.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.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 diff --git a/proofs/cbmc/poly_use_hint/Makefile b/proofs/cbmc/poly_use_hint/Makefile index 883fefa4c..6a20e66ed 100644 --- a/proofs/cbmc/poly_use_hint/Makefile +++ b/proofs/cbmc/poly_use_hint/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_use_hint USE_FUNCTION_CONTRACTS=mld_use_hint diff --git a/proofs/cbmc/polyeta_pack/Makefile b/proofs/cbmc/polyeta_pack/Makefile index e0341e2af..c4b2eee68 100644 --- a/proofs/cbmc/polyeta_pack/Makefile +++ b/proofs/cbmc/polyeta_pack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_pack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/polyeta_unpack/Makefile b/proofs/cbmc/polyeta_unpack/Makefile index 1ed697af7..9067765fe 100644 --- a/proofs/cbmc/polyeta_unpack/Makefile +++ b/proofs/cbmc/polyeta_unpack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyeta_unpack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/polyw1_pack/Makefile b/proofs/cbmc/polyw1_pack/Makefile index 807daf603..12f871df8 100644 --- a/proofs/cbmc/polyw1_pack/Makefile +++ b/proofs/cbmc/polyw1_pack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyw1_pack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/polyz_pack/Makefile b/proofs/cbmc/polyz_pack/Makefile index ef47c44de..6e4237af7 100644 --- a/proofs/cbmc/polyz_pack/Makefile +++ b/proofs/cbmc/polyz_pack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_pack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/polyz_unpack/Makefile b/proofs/cbmc/polyz_unpack/Makefile index be3e4aa04..63b346b69 100644 --- a/proofs/cbmc/polyz_unpack/Makefile +++ b/proofs/cbmc/polyz_unpack/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_unpack USE_FUNCTION_CONTRACTS= diff --git a/proofs/cbmc/rej_eta/Makefile b/proofs/cbmc/rej_eta/Makefile index eaadab2b7..e57348045 100644 --- a/proofs/cbmc/rej_eta/Makefile +++ b/proofs/cbmc/rej_eta/Makefile @@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c CHECK_FUNCTION_CONTRACTS=mld_rej_eta USE_FUNCTION_CONTRACTS= diff --git a/test/break_pct_config.h b/test/break_pct_config.h index fc99fe876..1230479d1 100644 --- a/test/break_pct_config.h +++ b/test/break_pct_config.h @@ -43,6 +43,12 @@ * * 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. * *****************************************************************************/ @@ -50,6 +56,50 @@ #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. + * + * Example: TODO: add example + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ /****************************************************************************** * Name: MLD_CONFIG_FILE diff --git a/test/custom_memcpy_config.h b/test/custom_memcpy_config.h index b687f64bb..48572dd1e 100644 --- a/test/custom_memcpy_config.h +++ b/test/custom_memcpy_config.h @@ -43,6 +43,12 @@ * * 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. * *****************************************************************************/ @@ -50,6 +56,50 @@ #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. + * + * Example: TODO: add example + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ /****************************************************************************** * Name: MLD_CONFIG_FILE diff --git a/test/custom_memset_config.h b/test/custom_memset_config.h index e78196488..a7ba161e7 100644 --- a/test/custom_memset_config.h +++ b/test/custom_memset_config.h @@ -43,6 +43,12 @@ * * 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. * *****************************************************************************/ @@ -50,6 +56,51 @@ #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. + * + * Example: TODO: add example + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ + /****************************************************************************** * Name: MLD_CONFIG_FILE diff --git a/test/custom_randombytes_config.h b/test/custom_randombytes_config.h index 212ae1108..2524cf390 100644 --- a/test/custom_randombytes_config.h +++ b/test/custom_randombytes_config.h @@ -43,6 +43,12 @@ * * 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. * *****************************************************************************/ @@ -50,6 +56,50 @@ #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. + * + * Example: TODO: add example + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ /****************************************************************************** * Name: MLD_CONFIG_FILE diff --git a/test/custom_stdlib_config.h b/test/custom_stdlib_config.h index c1eca49f8..7eedc09bd 100644 --- a/test/custom_stdlib_config.h +++ b/test/custom_stdlib_config.h @@ -43,6 +43,12 @@ * * 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. * *****************************************************************************/ @@ -50,6 +56,50 @@ #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. + * + * Example: TODO: add example + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ /****************************************************************************** * Name: MLD_CONFIG_FILE diff --git a/test/custom_zeroize_config.h b/test/custom_zeroize_config.h index ee1356431..2054ff804 100644 --- a/test/custom_zeroize_config.h +++ b/test/custom_zeroize_config.h @@ -43,6 +43,12 @@ * * 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. * *****************************************************************************/ @@ -50,6 +56,50 @@ #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. + * + * Example: TODO: add example + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ /****************************************************************************** * Name: MLD_CONFIG_FILE diff --git a/test/no_asm_config.h b/test/no_asm_config.h index 745db959e..82e94d29b 100644 --- a/test/no_asm_config.h +++ b/test/no_asm_config.h @@ -43,6 +43,12 @@ * * 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. * *****************************************************************************/ @@ -50,6 +56,50 @@ #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. + * + * Example: TODO: add example + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * 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. + * + * See examples/multilevel_build_mldsa for an example. + * + * This can also be set using CFLAGS. + * + *****************************************************************************/ +/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */ /****************************************************************************** * Name: MLD_CONFIG_ARITH_BACKEND_FILE