From 8bc366e73e88aa80e7923c3f7977821269222333 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Sun, 7 Jun 2026 10:52:17 +0800 Subject: [PATCH] poly: Deduplicate poly_decompose and poly_use_hint poly_decompose and poly_use_hint depend only on GAMMA2, so ML-DSA-65 and -87 use identical code. Move them into the shared poly.c as mld_poly_decompose_{88,32} and mld_poly_use_hint_{88,32}, compiled once, with thin dispatchers in poly_kl.h, so a multilevel build shares a single copy instead of emitting one per parameter set. The native backend dispatch moves into the value-specialized variants, dropping the parameter-set checks. The underlying rounding.h helpers mld_decompose and mld_use_hint are likewise split into value-specialized variants written against the parameter-set independent constants MLDSA_GAMMA2_{88,32}; the original dispatching forms are removed as they have no remaining users. Split the CBMC proofs into per-variant proofs plus dispatcher proofs. - Towards #536 Signed-off-by: Matthias J. Kannwischer --- mldsa/mldsa_native.c | 10 +- mldsa/mldsa_native_asm.S | 10 +- mldsa/src/poly.c | 212 ++++++++++++++++++ mldsa/src/poly.h | 120 ++++++++++ mldsa/src/poly_kl.c | 129 ----------- mldsa/src/poly_kl.h | 28 ++- mldsa/src/rounding.h | 129 ++++++++--- proofs/cbmc/decompose/Makefile | 56 ----- proofs/cbmc/decompose_32/Makefile | 41 ++++ .../decompose_32_harness.c} | 5 +- proofs/cbmc/decompose_88/Makefile | 41 ++++ .../cbmc/decompose_88/decompose_88_harness.c | 13 ++ proofs/cbmc/poly_decompose/Makefile | 8 +- proofs/cbmc/poly_decompose_32/Makefile | 41 ++++ .../poly_decompose_32_harness.c | 12 + proofs/cbmc/poly_decompose_32_c/Makefile | 41 ++++ .../poly_decompose_32_c_harness.c} | 9 +- .../poly_decompose_32_native_aarch64/Makefile | 6 +- proofs/cbmc/poly_decompose_88/Makefile | 41 ++++ .../poly_decompose_88_harness.c | 12 + proofs/cbmc/poly_decompose_88_c/Makefile | 41 ++++ .../poly_decompose_88_c_harness.c | 15 ++ .../poly_decompose_88_native_aarch64/Makefile | 6 +- proofs/cbmc/poly_decompose_c/Makefile | 55 ----- proofs/cbmc/poly_decompose_native/Makefile | 16 +- .../poly_decompose_native_harness.c | 8 +- proofs/cbmc/poly_use_hint/Makefile | 8 +- proofs/cbmc/poly_use_hint_32/Makefile | 41 ++++ .../poly_use_hint_32_harness.c | 12 + proofs/cbmc/poly_use_hint_32_c/Makefile | 41 ++++ .../poly_use_hint_32_c_harness.c} | 10 +- proofs/cbmc/poly_use_hint_88/Makefile | 41 ++++ .../poly_use_hint_88_harness.c | 12 + proofs/cbmc/poly_use_hint_88_c/Makefile | 41 ++++ .../poly_use_hint_88_c_harness.c | 15 ++ proofs/cbmc/poly_use_hint_c/Makefile | 55 ----- proofs/cbmc/poly_use_hint_native/Makefile | 16 +- .../poly_use_hint_native_harness.c | 8 +- .../poly_use_hint_native_aarch64/Makefile | 2 +- proofs/cbmc/use_hint/Makefile | 55 ----- proofs/cbmc/use_hint_32/Makefile | 40 ++++ .../use_hint_32_harness.c} | 4 +- proofs/cbmc/use_hint_88/Makefile | 40 ++++ proofs/cbmc/use_hint_88/use_hint_88_harness.c | 12 + test/src/test_unit.c | 24 +- 45 files changed, 1146 insertions(+), 436 deletions(-) delete mode 100644 proofs/cbmc/decompose/Makefile create mode 100644 proofs/cbmc/decompose_32/Makefile rename proofs/cbmc/{decompose/decompose_harness.c => decompose_32/decompose_32_harness.c} (71%) create mode 100644 proofs/cbmc/decompose_88/Makefile create mode 100644 proofs/cbmc/decompose_88/decompose_88_harness.c create mode 100644 proofs/cbmc/poly_decompose_32/Makefile create mode 100644 proofs/cbmc/poly_decompose_32/poly_decompose_32_harness.c create mode 100644 proofs/cbmc/poly_decompose_32_c/Makefile rename proofs/cbmc/{poly_decompose_c/poly_decompose_c_harness.c => poly_decompose_32_c/poly_decompose_32_c_harness.c} (51%) create mode 100644 proofs/cbmc/poly_decompose_88/Makefile create mode 100644 proofs/cbmc/poly_decompose_88/poly_decompose_88_harness.c create mode 100644 proofs/cbmc/poly_decompose_88_c/Makefile create mode 100644 proofs/cbmc/poly_decompose_88_c/poly_decompose_88_c_harness.c delete mode 100644 proofs/cbmc/poly_decompose_c/Makefile create mode 100644 proofs/cbmc/poly_use_hint_32/Makefile create mode 100644 proofs/cbmc/poly_use_hint_32/poly_use_hint_32_harness.c create mode 100644 proofs/cbmc/poly_use_hint_32_c/Makefile rename proofs/cbmc/{poly_use_hint_c/poly_use_hint_c_harness.c => poly_use_hint_32_c/poly_use_hint_32_c_harness.c} (52%) create mode 100644 proofs/cbmc/poly_use_hint_88/Makefile create mode 100644 proofs/cbmc/poly_use_hint_88/poly_use_hint_88_harness.c create mode 100644 proofs/cbmc/poly_use_hint_88_c/Makefile create mode 100644 proofs/cbmc/poly_use_hint_88_c/poly_use_hint_88_c_harness.c delete mode 100644 proofs/cbmc/poly_use_hint_c/Makefile delete mode 100644 proofs/cbmc/use_hint/Makefile create mode 100644 proofs/cbmc/use_hint_32/Makefile rename proofs/cbmc/{use_hint/use_hint_harness.c => use_hint_32/use_hint_32_harness.c} (69%) create mode 100644 proofs/cbmc/use_hint_88/Makefile create mode 100644 proofs/cbmc/use_hint_88/use_hint_88_harness.c diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 4d5f9d9a5..e01a2a80a 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -416,10 +416,12 @@ /* mldsa/src/rounding.h */ #undef MLD_2_POW_D #undef MLD_ROUNDING_H -#undef mld_decompose +#undef mld_decompose_32 +#undef mld_decompose_88 #undef mld_make_hint #undef mld_power2round -#undef mld_use_hint +#undef mld_use_hint_32 +#undef mld_use_hint_88 /* mldsa/src/sign.h */ #undef MLD_DOMAIN_SEPARATION_MAX_BYTES #undef MLD_PREHASH_NONE @@ -478,6 +480,8 @@ #undef mld_poly_add #undef mld_poly_caddq #undef mld_poly_chknorm +#undef mld_poly_decompose_32 +#undef mld_poly_decompose_88 #undef mld_poly_invntt_tomont #undef mld_poly_ntt #undef mld_poly_pointwise_montgomery @@ -487,6 +491,8 @@ #undef mld_poly_sub #undef mld_poly_uniform #undef mld_poly_uniform_4x +#undef mld_poly_use_hint_32 +#undef mld_poly_use_hint_88 #undef mld_polyt0_pack #undef mld_polyt0_unpack #undef mld_polyt1_pack diff --git a/mldsa/mldsa_native_asm.S b/mldsa/mldsa_native_asm.S index 57518c8cd..3c81d8070 100644 --- a/mldsa/mldsa_native_asm.S +++ b/mldsa/mldsa_native_asm.S @@ -423,10 +423,12 @@ /* mldsa/src/rounding.h */ #undef MLD_2_POW_D #undef MLD_ROUNDING_H -#undef mld_decompose +#undef mld_decompose_32 +#undef mld_decompose_88 #undef mld_make_hint #undef mld_power2round -#undef mld_use_hint +#undef mld_use_hint_32 +#undef mld_use_hint_88 /* mldsa/src/sign.h */ #undef MLD_DOMAIN_SEPARATION_MAX_BYTES #undef MLD_PREHASH_NONE @@ -485,6 +487,8 @@ #undef mld_poly_add #undef mld_poly_caddq #undef mld_poly_chknorm +#undef mld_poly_decompose_32 +#undef mld_poly_decompose_88 #undef mld_poly_invntt_tomont #undef mld_poly_ntt #undef mld_poly_pointwise_montgomery @@ -494,6 +498,8 @@ #undef mld_poly_sub #undef mld_poly_uniform #undef mld_poly_uniform_4x +#undef mld_poly_use_hint_32 +#undef mld_poly_use_hint_88 #undef mld_polyt0_pack #undef mld_polyt0_unpack #undef mld_polyt1_pack diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index 12ed2cf8d..3c7038141 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -1057,6 +1057,218 @@ void mld_polyw1_pack_32(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_32], || MLD_CONFIG_PARAMETER_SET == 87 */ #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */ +#if !defined(MLD_CONFIG_NO_SIGN_API) +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44 +MLD_STATIC_TESTABLE +void mld_poly_decompose_88_c(mld_poly *a1, mld_poly *a0) +__contract__( + requires(memory_no_alias(a1, sizeof(mld_poly))) + requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(mld_poly))) + assigns(memory_slice(a0, sizeof(mld_poly))) + ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88))) + ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2_88+1)) +) +{ + unsigned int i; + mld_assert_bound(a0->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(a0->coeffs, i, MLDSA_N, 0, MLDSA_Q)) + invariant(array_bound(a1->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88))) + invariant(array_abs_bound(a0->coeffs, 0, i, MLDSA_GAMMA2_88+1)) + decreases(MLDSA_N - i) + ) + { + mld_decompose_88(&a0->coeffs[i], &a1->coeffs[i], a0->coeffs[i]); + } + + mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2_88 + 1); + mld_assert_bound(a1->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_88)); +} + +MLD_INTERNAL_API +void mld_poly_decompose_88(mld_poly *a1, mld_poly *a0) +{ +#if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) + int ret; + mld_assert_bound(a0->coeffs, MLDSA_N, 0, MLDSA_Q); + ret = mld_poly_decompose_88_native(a1->coeffs, a0->coeffs); + if (ret == MLD_NATIVE_FUNC_SUCCESS) + { + mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2_88 + 1); + mld_assert_bound(a1->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_88)); + return; + } +#endif /* MLD_USE_NATIVE_POLY_DECOMPOSE_88 */ + mld_poly_decompose_88_c(a1, a0); +} +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \ + */ + +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \ + (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) +MLD_STATIC_TESTABLE +void mld_poly_decompose_32_c(mld_poly *a1, mld_poly *a0) +__contract__( + requires(memory_no_alias(a1, sizeof(mld_poly))) + requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(mld_poly))) + assigns(memory_slice(a0, sizeof(mld_poly))) + ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32))) + ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2_32+1)) +) +{ + unsigned int i; + mld_assert_bound(a0->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(a0->coeffs, i, MLDSA_N, 0, MLDSA_Q)) + invariant(array_bound(a1->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32))) + invariant(array_abs_bound(a0->coeffs, 0, i, MLDSA_GAMMA2_32+1)) + decreases(MLDSA_N - i) + ) + { + mld_decompose_32(&a0->coeffs[i], &a1->coeffs[i], a0->coeffs[i]); + } + + mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2_32 + 1); + mld_assert_bound(a1->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_32)); +} + +MLD_INTERNAL_API +void mld_poly_decompose_32(mld_poly *a1, mld_poly *a0) +{ +#if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_32) + int ret; + mld_assert_bound(a0->coeffs, MLDSA_N, 0, MLDSA_Q); + ret = mld_poly_decompose_32_native(a1->coeffs, a0->coeffs); + if (ret == MLD_NATIVE_FUNC_SUCCESS) + { + mld_assert_abs_bound(a0->coeffs, MLDSA_N, MLDSA_GAMMA2_32 + 1); + mld_assert_bound(a1->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_32)); + return; + } +#endif /* MLD_USE_NATIVE_POLY_DECOMPOSE_32 */ + mld_poly_decompose_32_c(a1, a0); +} +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ + || MLD_CONFIG_PARAMETER_SET == 87 */ +#endif /* !MLD_CONFIG_NO_SIGN_API */ + +#if !defined(MLD_CONFIG_NO_VERIFY_API) +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44 +MLD_STATIC_TESTABLE +void mld_poly_use_hint_88_c(mld_poly *a, const mld_poly *h) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(memory_no_alias(h, sizeof(mld_poly))) + requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(a, sizeof(mld_poly))) + ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88))) +) +{ + 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(a->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88))) + invariant(array_bound(a->coeffs, i, MLDSA_N, 0, MLDSA_Q)) + decreases(MLDSA_N - i) + ) + { + a->coeffs[i] = mld_use_hint_88(a->coeffs[i], h->coeffs[i]); + } + mld_assert_bound(a->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_88)); +} + +MLD_INTERNAL_API +void mld_poly_use_hint_88(mld_poly *a, const mld_poly *h) +{ +#if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) + int ret; + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); + ret = mld_poly_use_hint_88_native(a->coeffs, h->coeffs); + if (ret == MLD_NATIVE_FUNC_SUCCESS) + { + mld_assert_bound(a->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_88)); + return; + } +#endif /* MLD_USE_NATIVE_POLY_USE_HINT_88 */ + mld_poly_use_hint_88_c(a, h); +} +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \ + */ + +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \ + (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) +MLD_STATIC_TESTABLE +void mld_poly_use_hint_32_c(mld_poly *a, const mld_poly *h) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(memory_no_alias(h, sizeof(mld_poly))) + requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(a, sizeof(mld_poly))) + ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32))) +) +{ + 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(a->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32))) + invariant(array_bound(a->coeffs, i, MLDSA_N, 0, MLDSA_Q)) + decreases(MLDSA_N - i) + ) + { + a->coeffs[i] = mld_use_hint_32(a->coeffs[i], h->coeffs[i]); + } + mld_assert_bound(a->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_32)); +} + +MLD_INTERNAL_API +void mld_poly_use_hint_32(mld_poly *a, const mld_poly *h) +{ +#if defined(MLD_USE_NATIVE_POLY_USE_HINT_32) + int ret; + mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); + mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); + ret = mld_poly_use_hint_32_native(a->coeffs, h->coeffs); + if (ret == MLD_NATIVE_FUNC_SUCCESS) + { + mld_assert_bound(a->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_32)); + return; + } +#endif /* MLD_USE_NATIVE_POLY_USE_HINT_32 */ + mld_poly_use_hint_32_c(a, h); +} +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ + || MLD_CONFIG_PARAMETER_SET == 87 */ +#endif /* !MLD_CONFIG_NO_VERIFY_API */ + #else /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */ MLD_EMPTY_CU(mld_poly) #endif /* MLD_CONFIG_MULTILEVEL_NO_SHARED */ diff --git a/mldsa/src/poly.h b/mldsa/src/poly.h index e7d4871b1..ad31733f5 100644 --- a/mldsa/src/poly.h +++ b/mldsa/src/poly.h @@ -425,4 +425,124 @@ __contract__( || MLD_CONFIG_PARAMETER_SET == 87 */ #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */ +#if !defined(MLD_CONFIG_NO_SIGN_API) +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44 +#define mld_poly_decompose_88 MLD_NAMESPACE(poly_decompose_88) +/** + * For all coefficients c of the input polynomial, compute high and low bits + * c0, c1 such c mod MLDSA_Q = c1*ALPHA + c0 with -ALPHA/2 < c0 <= ALPHA/2 + * except c1 = (MLDSA_Q-1)/ALPHA where we set c1 = 0 and + * -ALPHA/2 <= c0 = c mod MLDSA_Q - MLDSA_Q < 0, where + * ALPHA = 2*MLDSA_GAMMA2_88. Assumes coefficients to be standard + * representatives. + * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/88 + * (ML-DSA-44). + * + * @reference{The reference implementation has the input polynomial as a + * separate argument that may be aliased with either of the outputs. Removing + * the aliasing eases CBMC proofs.} + * + * @param[out] a1 Pointer to output polynomial with coefficients c1. + * @param[in,out] a0 Pointer to input/output polynomial. Output polynomial has + * coefficients c0. + */ +MLD_INTERNAL_API +void mld_poly_decompose_88(mld_poly *a1, mld_poly *a0) +__contract__( + requires(memory_no_alias(a1, sizeof(mld_poly))) + requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(mld_poly))) + assigns(memory_slice(a0, sizeof(mld_poly))) + ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88))) + ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2_88+1)) +); +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \ + */ + +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \ + (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) +#define mld_poly_decompose_32 MLD_NAMESPACE(poly_decompose_32) +/** + * For all coefficients c of the input polynomial, compute high and low bits + * c0, c1 such c mod MLDSA_Q = c1*ALPHA + c0 with -ALPHA/2 < c0 <= ALPHA/2 + * except c1 = (MLDSA_Q-1)/ALPHA where we set c1 = 0 and + * -ALPHA/2 <= c0 = c mod MLDSA_Q - MLDSA_Q < 0, where + * ALPHA = 2*MLDSA_GAMMA2_32. Assumes coefficients to be standard + * representatives. + * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/32 + * (ML-DSA-65 and ML-DSA-87). + * + * @reference{The reference implementation has the input polynomial as a + * separate argument that may be aliased with either of the outputs. Removing + * the aliasing eases CBMC proofs.} + * + * @param[out] a1 Pointer to output polynomial with coefficients c1. + * @param[in,out] a0 Pointer to input/output polynomial. Output polynomial has + * coefficients c0. + */ +MLD_INTERNAL_API +void mld_poly_decompose_32(mld_poly *a1, mld_poly *a0) +__contract__( + requires(memory_no_alias(a1, sizeof(mld_poly))) + requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(mld_poly))) + assigns(memory_slice(a0, sizeof(mld_poly))) + ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32))) + ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2_32+1)) +); +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ + || MLD_CONFIG_PARAMETER_SET == 87 */ +#endif /* !MLD_CONFIG_NO_SIGN_API */ + +#if !defined(MLD_CONFIG_NO_VERIFY_API) +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44 +#define mld_poly_use_hint_88 MLD_NAMESPACE(poly_use_hint_88) +/** + * Use hint polynomial h to correct the high bits of a in-place. + * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/88 + * (ML-DSA-44). + * + * @param[in,out] a Input/output polynomial. + * @param[in] h Hint polynomial. + */ +MLD_INTERNAL_API +void mld_poly_use_hint_88(mld_poly *a, const mld_poly *h) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(memory_no_alias(h, sizeof(mld_poly))) + requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(a, sizeof(mld_poly))) + ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88))) +); +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \ + */ + +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \ + (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) +#define mld_poly_use_hint_32 MLD_NAMESPACE(poly_use_hint_32) +/** + * Use hint polynomial h to correct the high bits of a in-place. + * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/32 + * (ML-DSA-65 and ML-DSA-87). + * + * @param[in,out] a Input/output polynomial. + * @param[in] h Hint polynomial. + */ +MLD_INTERNAL_API +void mld_poly_use_hint_32(mld_poly *a, const mld_poly *h) +__contract__( + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(memory_no_alias(h, sizeof(mld_poly))) + requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(a, sizeof(mld_poly))) + ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32))) +); +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ + || MLD_CONFIG_PARAMETER_SET == 87 */ +#endif /* !MLD_CONFIG_NO_VERIFY_API */ + #endif /* !MLD_POLY_H */ diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index 5be537d46..d632dbefe 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -31,137 +31,10 @@ * within a single compilation unit. */ #define mld_rej_eta MLD_ADD_PARAM_SET(mld_rej_eta) #define mld_rej_eta_c MLD_ADD_PARAM_SET(mld_rej_eta_c) -#define mld_poly_decompose_c MLD_ADD_PARAM_SET(mld_poly_decompose_c) -#define mld_poly_use_hint_c MLD_ADD_PARAM_SET(mld_poly_use_hint_c) #define mld_polyz_unpack_c MLD_ADD_PARAM_SET(mld_polyz_unpack_c) /* End of parameter set namespacing */ -#if !defined(MLD_CONFIG_NO_SIGN_API) -MLD_STATIC_TESTABLE -void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0) -__contract__( - requires(memory_no_alias(a1, sizeof(mld_poly))) - requires(memory_no_alias(a0, sizeof(mld_poly))) - requires(array_bound(a0->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) - assigns(memory_slice(a1, sizeof(mld_poly))) - assigns(memory_slice(a0, sizeof(mld_poly))) - ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) - ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)) -) -{ - unsigned int i; - mld_assert_bound(a0->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(a0->coeffs, i, MLDSA_N, 0, MLDSA_Q)) - 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)) - decreases(MLDSA_N - i) - ) - { - mld_decompose(&a0->coeffs[i], &a1->coeffs[i], a0->coeffs[i]); - } - - 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 -void mld_poly_decompose(mld_poly *a1, mld_poly *a0) -{ -#if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) && MLD_CONFIG_PARAMETER_SET == 44 - int ret; - mld_assert_bound(a0->coeffs, MLDSA_N, 0, MLDSA_Q); - ret = mld_poly_decompose_88_native(a1->coeffs, a0->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - 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)); - return; - } -#elif defined(MLD_USE_NATIVE_POLY_DECOMPOSE_32) && \ - (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) - int ret; - mld_assert_bound(a0->coeffs, MLDSA_N, 0, MLDSA_Q); - ret = mld_poly_decompose_32_native(a1->coeffs, a0->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - 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)); - return; - } -#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_poly_decompose_c(a1, a0); -} - -#endif /* !MLD_CONFIG_NO_SIGN_API */ - -#if !defined(MLD_CONFIG_NO_VERIFY_API) -MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *a, const mld_poly *h) -__contract__( - requires(memory_no_alias(a, sizeof(mld_poly))) - requires(memory_no_alias(h, sizeof(mld_poly))) - requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q)) - requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) - assigns(memory_slice(a, sizeof(mld_poly))) - ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) -) -{ - 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(a->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) - invariant(array_bound(a->coeffs, i, MLDSA_N, 0, MLDSA_Q)) - decreases(MLDSA_N - i) - ) - { - a->coeffs[i] = mld_use_hint(a->coeffs[i], h->coeffs[i]); - } - mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); -} - -MLD_INTERNAL_API -void mld_poly_use_hint(mld_poly *a, const mld_poly *h) -{ -#if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) && MLD_CONFIG_PARAMETER_SET == 44 - int ret; - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - ret = mld_poly_use_hint_88_native(a->coeffs, h->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); - return; - } -#elif defined(MLD_USE_NATIVE_POLY_USE_HINT_32) && \ - (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) - int ret; - mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - ret = mld_poly_use_hint_32_native(a->coeffs, h->coeffs); - if (ret == MLD_NATIVE_FUNC_SUCCESS) - { - mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2)); - return; - } -#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_poly_use_hint_c(a, h); -} -#endif /* !MLD_CONFIG_NO_VERIFY_API */ - #if !defined(MLD_CONFIG_NO_KEYPAIR_API) /** * Sample uniformly random coefficients in [-MLDSA_ETA, MLDSA_ETA] by @@ -901,8 +774,6 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) * Don't modify by hand -- this is auto-generated by scripts/autogen. */ #undef mld_rej_eta #undef mld_rej_eta_c -#undef mld_poly_decompose_c -#undef mld_poly_use_hint_c #undef mld_polyz_unpack_c #undef MLD_POLY_UNIFORM_ETA_NBLOCKS #undef MLD_POLY_UNIFORM_ETA_NBLOCKS diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h index 341cd987a..83acd7e14 100644 --- a/mldsa/src/poly_kl.h +++ b/mldsa/src/poly_kl.h @@ -16,7 +16,8 @@ * c0, c1 such c mod MLDSA_Q = c1*ALPHA + c0 with -ALPHA/2 < c0 <= ALPHA/2 * except c1 = (MLDSA_Q-1)/ALPHA where we set c1 = 0 and * -ALPHA/2 <= c0 = c mod MLDSA_Q - MLDSA_Q < 0. Assumes coefficients to be - * standard representatives. + * standard representatives. Dispatches to the value-specialized variant for + * the selected parameter set. * * @reference{The reference implementation has the input polynomial as a * separate argument that may be aliased with either of the outputs. Removing @@ -26,8 +27,7 @@ * @param[in,out] a0 Pointer to input/output polynomial. Output polynomial has * coefficients c0. */ -MLD_INTERNAL_API -void mld_poly_decompose(mld_poly *a1, mld_poly *a0) +static MLD_INLINE void mld_poly_decompose(mld_poly *a1, mld_poly *a0) __contract__( requires(memory_no_alias(a1, sizeof(mld_poly))) requires(memory_no_alias(a0, sizeof(mld_poly))) @@ -36,7 +36,14 @@ __contract__( assigns(memory_slice(a0, sizeof(mld_poly))) ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)) -); +) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly_decompose_88(a1, a0); +#else + mld_poly_decompose_32(a1, a0); +#endif +} #endif /* !MLD_CONFIG_NO_SIGN_API */ @@ -44,12 +51,12 @@ __contract__( #define mld_poly_use_hint MLD_NAMESPACE_KL(poly_use_hint) /** * Use hint polynomial h to correct the high bits of a in-place. + * Dispatches to the value-specialized variant for the selected parameter set. * * @param[in,out] a Input/output polynomial. * @param[in] h Hint polynomial. */ -MLD_INTERNAL_API -void mld_poly_use_hint(mld_poly *a, const mld_poly *h) +static MLD_INLINE void mld_poly_use_hint(mld_poly *a, const mld_poly *h) __contract__( requires(memory_no_alias(a, sizeof(mld_poly))) requires(memory_no_alias(h, sizeof(mld_poly))) @@ -57,7 +64,14 @@ __contract__( requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) assigns(memory_slice(a, sizeof(mld_poly))) ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) -); +) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly_use_hint_88(a, h); +#else + mld_poly_use_hint_32(a, h); +#endif +} #endif /* !MLD_CONFIG_NO_VERIFY_API */ #if !defined(MLD_CONFIG_NO_KEYPAIR_API) diff --git a/mldsa/src/rounding.h b/mldsa/src/rounding.h index 21fae3c98..b7b93f7cd 100644 --- a/mldsa/src/rounding.h +++ b/mldsa/src/rounding.h @@ -25,9 +25,11 @@ * of mldsa-native (e.g. with varying parameter sets) * within a single compilation unit. */ #define mld_power2round MLD_ADD_PARAM_SET(mld_power2round) -#define mld_decompose MLD_ADD_PARAM_SET(mld_decompose) +#define mld_decompose_88 MLD_ADD_PARAM_SET(mld_decompose_88) +#define mld_decompose_32 MLD_ADD_PARAM_SET(mld_decompose_32) #define mld_make_hint MLD_ADD_PARAM_SET(mld_make_hint) -#define mld_use_hint MLD_ADD_PARAM_SET(mld_use_hint) +#define mld_use_hint_88 MLD_ADD_PARAM_SET(mld_use_hint_88) +#define mld_use_hint_32 MLD_ADD_PARAM_SET(mld_use_hint_32) /* End of parameter set namespacing */ #define MLD_2_POW_D (1 << MLDSA_D) @@ -63,12 +65,15 @@ __contract__( /** * For finite field element a, compute high and low bits a0, a1 such that - * a mod^+ MLDSA_Q = a1 * 2 * MLDSA_GAMMA2 + a0 with - * -MLDSA_GAMMA2 < a0 <= MLDSA_GAMMA2 except if - * a1 = (MLDSA_Q-1)/(MLDSA_GAMMA2*2) where we set a1 = 0 and - * -MLDSA_GAMMA2 <= a0 = a mod^+ MLDSA_Q - MLDSA_Q < 0. Assumes a to be + * a mod^+ MLDSA_Q = a1 * 2 * MLDSA_GAMMA2_88 + a0 with + * -MLDSA_GAMMA2_88 < a0 <= MLDSA_GAMMA2_88 except if + * a1 = (MLDSA_Q-1)/(MLDSA_GAMMA2_88*2) where we set a1 = 0 and + * -MLDSA_GAMMA2_88 <= a0 = a mod^+ MLDSA_Q - MLDSA_Q < 0. Assumes a to be * standard representative. * + * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/88 + * (ML-DSA-44). + * * @reference{In the reference implementation, a1 is passed as a return value * instead.} * @@ -76,18 +81,18 @@ __contract__( * @param[out] a1 Pointer to output element a1. * @param a Input element. */ -static MLD_INLINE void mld_decompose(int32_t *a0, int32_t *a1, int32_t a) +static MLD_INLINE void mld_decompose_88(int32_t *a0, int32_t *a1, int32_t a) __contract__( requires(memory_no_alias(a0, sizeof(int32_t))) requires(memory_no_alias(a1, sizeof(int32_t))) requires(a >= 0 && a < MLDSA_Q) assigns(memory_slice(a0, sizeof(int32_t))) assigns(memory_slice(a1, sizeof(int32_t))) - /* a0 = -MLDSA_GAMMA2 can only occur when (q-1) = a - (a mod MLDSA_GAMMA2), - * then a1=1; and a0 = a - (a mod MLDSA_GAMMA2) - 1 (@[FIPS204, Algorithm 36 (Decompose)]) */ - ensures(*a0 >= -MLDSA_GAMMA2 && *a0 <= MLDSA_GAMMA2) - ensures(*a1 >= 0 && *a1 < (MLDSA_Q-1)/(2*MLDSA_GAMMA2)) - ensures((*a1 * 2 * MLDSA_GAMMA2 + *a0 - a) % MLDSA_Q == 0) + /* a0 = -MLDSA_GAMMA2_88 can only occur when (q-1) = a - (a mod MLDSA_GAMMA2_88), + * then a1=1; and a0 = a - (a mod MLDSA_GAMMA2_88) - 1 (@[FIPS204, Algorithm 36 (Decompose)]) */ + ensures(*a0 >= -MLDSA_GAMMA2_88 && *a0 <= MLDSA_GAMMA2_88) + ensures(*a1 >= 0 && *a1 < (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88)) + ensures((*a1 * 2 * MLDSA_GAMMA2_88 + *a0 - a) % MLDSA_Q == 0) ) { /* @@ -109,7 +114,6 @@ __contract__( /* check-magic: 65472 == round((MLDSA_Q-1)/128) */ mld_assert(*a1 >= 0 && *a1 <= 65472); -#if MLD_CONFIG_PARAMETER_SET == 44 /* check-magic: 1488 == 2 * intdiv(intdiv(MLDSA_Q - 1, 88), 128) */ /* check-magic: 11275 == floor(2**24 / 1488) */ /* check-magic: 1560281088 == 1 / (1 / 1488 - 11275 / 2**24) */ @@ -146,16 +150,59 @@ __contract__( *a1 = mld_ct_sel_int32(0, *a1, mld_ct_cmask_neg_i32(43 - *a1)); mld_assert(*a1 >= 0 && *a1 <= 43); -#else /* MLD_CONFIG_PARAMETER_SET == 44 */ + + *a0 = a - *a1 * 2 * MLDSA_GAMMA2_88; + *a0 = mld_ct_sel_int32(*a0 - MLDSA_Q, *a0, + mld_ct_cmask_neg_i32((MLDSA_Q - 1) / 2 - *a0)); +} + +/** + * For finite field element a, compute high and low bits a0, a1 such that + * a mod^+ MLDSA_Q = a1 * 2 * MLDSA_GAMMA2_32 + a0 with + * -MLDSA_GAMMA2_32 < a0 <= MLDSA_GAMMA2_32 except if + * a1 = (MLDSA_Q-1)/(MLDSA_GAMMA2_32*2) where we set a1 = 0 and + * -MLDSA_GAMMA2_32 <= a0 = a mod^+ MLDSA_Q - MLDSA_Q < 0. Assumes a to be + * standard representative. + * + * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/32 + * (ML-DSA-65 and ML-DSA-87). + * + * @reference{In the reference implementation, a1 is passed as a return value + * instead.} + * + * @param[out] a0 Pointer to output element a0. + * @param[out] a1 Pointer to output element a1. + * @param a Input element. + */ +static MLD_INLINE void mld_decompose_32(int32_t *a0, int32_t *a1, int32_t a) +__contract__( + requires(memory_no_alias(a0, sizeof(int32_t))) + requires(memory_no_alias(a1, sizeof(int32_t))) + requires(a >= 0 && a < MLDSA_Q) + assigns(memory_slice(a0, sizeof(int32_t))) + assigns(memory_slice(a1, sizeof(int32_t))) + /* a0 = -MLDSA_GAMMA2_32 can only occur when (q-1) = a - (a mod MLDSA_GAMMA2_32), + * then a1=1; and a0 = a - (a mod MLDSA_GAMMA2_32) - 1 (@[FIPS204, Algorithm 36 (Decompose)]) */ + ensures(*a0 >= -MLDSA_GAMMA2_32 && *a0 <= MLDSA_GAMMA2_32) + ensures(*a1 >= 0 && *a1 < (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32)) + ensures((*a1 * 2 * MLDSA_GAMMA2_32 + *a0 - a) % MLDSA_Q == 0) +) +{ + /* See mld_decompose_88 for the derivation of the computation of f1. */ + *a1 = (a + 127) >> 7; + /* We know a >= 0 and a < MLDSA_Q, so... */ + /* check-magic: 65472 == round((MLDSA_Q-1)/128) */ + mld_assert(*a1 >= 0 && *a1 <= 65472); + /* check-magic: 4092 == 2 * intdiv(intdiv(MLDSA_Q - 1, 32), 128) */ /* check-magic: 1025 == floor(2**22 / 4092) */ /* check-magic: 4290772992 == 1 / (1 / 4092 - 1025 / 2**22) */ /* * Compute f1 = round-(f1' / B) ≈ round(f1' * 1025 / 2^22). This is exact for - * 0 <= f1' < 2^16. Following the same argument above, it suffices to show - * that f1' * eps < 1 / B, where eps := 1 / B - 1025 / 2^22. Indeed, we have - * eps = 1 / 4290772992 ≈ 2^(-31.99) < 2^(-31), therefore f1' * eps < - * 2^16 * 2^(-31) = 1 / 2^15 < 1 / 2^12 < 1 / B. + * 0 <= f1' < 2^16. Following the same argument as in mld_decompose_88, it + * suffices to show that f1' * eps < 1 / B, where eps := 1 / B - 1025 / 2^22. + * Indeed, we have eps = 1 / 4290772992 ≈ 2^(-31.99) < 2^(-31), therefore + * f1' * eps < 2^16 * 2^(-31) = 1 / 2^15 < 1 / 2^12 < 1 / B. */ *a1 = (*a1 * 1025 + (1 << 21)) >> 22; mld_assert(*a1 >= 0 && *a1 <= 16); @@ -163,9 +210,7 @@ __contract__( *a1 &= 15; mld_assert(*a1 >= 0 && *a1 <= 15); -#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ - - *a0 = a - *a1 * 2 * MLDSA_GAMMA2; + *a0 = a - *a1 * 2 * MLDSA_GAMMA2_32; *a0 = mld_ct_sel_int32(*a0 - MLDSA_Q, *a0, mld_ct_cmask_neg_i32((MLDSA_Q - 1) / 2 - *a0)); } @@ -197,28 +242,30 @@ __contract__( /** * Correct high bits according to hint. * + * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/88 + * (ML-DSA-44). + * * @param a Input element. * @param hint Hint bit. * * @return Corrected high bits. */ MLD_MUST_CHECK_RETURN_VALUE -static MLD_INLINE int32_t mld_use_hint(int32_t a, int32_t hint) +static MLD_INLINE int32_t mld_use_hint_88(int32_t a, int32_t hint) __contract__( requires(hint >= 0 && hint <= 1) requires(a >= 0 && a < MLDSA_Q) - ensures(return_value >= 0 && return_value < (MLDSA_Q-1)/(2*MLDSA_GAMMA2)) + ensures(return_value >= 0 && return_value < (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88)) ) { int32_t a0, a1; - mld_decompose(&a0, &a1, a); + mld_decompose_88(&a0, &a1, a); if (hint == 0) { return a1; } -#if MLD_CONFIG_PARAMETER_SET == 44 if (a0 > 0) { return (a1 == 43) ? 0 : a1 + 1; @@ -227,7 +274,35 @@ __contract__( { return (a1 == 0) ? 43 : a1 - 1; } -#else /* MLD_CONFIG_PARAMETER_SET == 44 */ +} + +/** + * Correct high bits according to hint. + * + * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/32 + * (ML-DSA-65 and ML-DSA-87). + * + * @param a Input element. + * @param hint Hint bit. + * + * @return Corrected high bits. + */ +MLD_MUST_CHECK_RETURN_VALUE +static MLD_INLINE int32_t mld_use_hint_32(int32_t a, int32_t hint) +__contract__( + requires(hint >= 0 && hint <= 1) + requires(a >= 0 && a < MLDSA_Q) + ensures(return_value >= 0 && return_value < (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32)) +) +{ + int32_t a0, a1; + + mld_decompose_32(&a0, &a1, a); + if (hint == 0) + { + return a1; + } + if (a0 > 0) { return (a1 + 1) & 15; @@ -236,8 +311,6 @@ __contract__( { return (a1 - 1) & 15; } -#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ } - #endif /* !MLD_ROUNDING_H */ diff --git a/proofs/cbmc/decompose/Makefile b/proofs/cbmc/decompose/Makefile deleted file mode 100644 index c8c290201..000000000 --- a/proofs/cbmc/decompose/Makefile +++ /dev/null @@ -1,56 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = decompose_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = decompose - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c - -CHECK_FUNCTION_CONTRACTS=mld_decompose -USE_FUNCTION_CONTRACTS=mld_ct_sel_int32 -USE_FUNCTION_CONTRACTS+=mld_ct_cmask_neg_i32 -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 - -FUNCTION_NAME = decompose - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 8 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/decompose_32/Makefile b/proofs/cbmc/decompose_32/Makefile new file mode 100644 index 000000000..dd81fce95 --- /dev/null +++ b/proofs/cbmc/decompose_32/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = decompose_32_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = decompose_32 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS= +else +CHECK_FUNCTION_CONTRACTS=mld_decompose_32 +endif +USE_FUNCTION_CONTRACTS=mld_ct_sel_int32 +USE_FUNCTION_CONTRACTS+=mld_ct_cmask_neg_i32 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = decompose_32 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/decompose/decompose_harness.c b/proofs/cbmc/decompose_32/decompose_32_harness.c similarity index 71% rename from proofs/cbmc/decompose/decompose_harness.c rename to proofs/cbmc/decompose_32/decompose_32_harness.c index c8a7c5adb..ea1de4752 100644 --- a/proofs/cbmc/decompose/decompose_harness.c +++ b/proofs/cbmc/decompose_32/decompose_32_harness.c @@ -3,10 +3,11 @@ #include "rounding.h" - void harness(void) { +#if MLD_CONFIG_PARAMETER_SET != 44 int32_t *a0, *a1; int32_t a; - mld_decompose(a0, a1, a); + mld_decompose_32(a0, a1, a); +#endif } diff --git a/proofs/cbmc/decompose_88/Makefile b/proofs/cbmc/decompose_88/Makefile new file mode 100644 index 000000000..33f3f1166 --- /dev/null +++ b/proofs/cbmc/decompose_88/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = decompose_88_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = decompose_88 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS=mld_decompose_88 +else +CHECK_FUNCTION_CONTRACTS= +endif +USE_FUNCTION_CONTRACTS=mld_ct_sel_int32 +USE_FUNCTION_CONTRACTS+=mld_ct_cmask_neg_i32 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = decompose_88 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/decompose_88/decompose_88_harness.c b/proofs/cbmc/decompose_88/decompose_88_harness.c new file mode 100644 index 000000000..ef61c41f8 --- /dev/null +++ b/proofs/cbmc/decompose_88/decompose_88_harness.c @@ -0,0 +1,13 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "rounding.h" + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + int32_t *a0, *a1; + int32_t a; + mld_decompose_88(a0, a1, a); +#endif +} diff --git a/proofs/cbmc/poly_decompose/Makefile b/proofs/cbmc/poly_decompose/Makefile index 106a35b45..48376cba9 100644 --- a/proofs/cbmc/poly_decompose/Makefile +++ b/proofs/cbmc/poly_decompose/Makefile @@ -17,10 +17,14 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=mld_poly_decompose -USE_FUNCTION_CONTRACTS= mld_poly_decompose_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +USE_FUNCTION_CONTRACTS=mld_poly_decompose_88 +else +USE_FUNCTION_CONTRACTS=mld_poly_decompose_32 +endif APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_decompose_32/Makefile b/proofs/cbmc/poly_decompose_32/Makefile new file mode 100644 index 000000000..216d549a4 --- /dev/null +++ b/proofs/cbmc/poly_decompose_32/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_decompose_32_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_decompose_32 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +else +CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_32 +USE_FUNCTION_CONTRACTS=mld_poly_decompose_32_c +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_decompose_32 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/poly_decompose_32/poly_decompose_32_harness.c b/proofs/cbmc/poly_decompose_32/poly_decompose_32_harness.c new file mode 100644 index 000000000..3c9290c88 --- /dev/null +++ b/proofs/cbmc/poly_decompose_32/poly_decompose_32_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET != 44 + mld_poly *a0, *a1; + mld_poly_decompose_32(a1, a0); +#endif +} diff --git a/proofs/cbmc/poly_decompose_32_c/Makefile b/proofs/cbmc/poly_decompose_32_c/Makefile new file mode 100644 index 000000000..9a1acd1d2 --- /dev/null +++ b/proofs/cbmc/poly_decompose_32_c/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_decompose_32_c_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_decompose_32_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +else +CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_32_c +USE_FUNCTION_CONTRACTS=mld_decompose_32 +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mld_poly_decompose_32_c + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +include ../Makefile.common diff --git a/proofs/cbmc/poly_decompose_c/poly_decompose_c_harness.c b/proofs/cbmc/poly_decompose_32_c/poly_decompose_32_c_harness.c similarity index 51% rename from proofs/cbmc/poly_decompose_c/poly_decompose_c_harness.c rename to proofs/cbmc/poly_decompose_32_c/poly_decompose_32_c_harness.c index d5f71205e..5ce8ae94b 100644 --- a/proofs/cbmc/poly_decompose_c/poly_decompose_c_harness.c +++ b/proofs/cbmc/poly_decompose_32_c/poly_decompose_32_c_harness.c @@ -1,14 +1,15 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -#include "poly_kl.h" +#include "poly.h" // Prototype for the function under test -#define mld_poly_decompose_c MLD_ADD_PARAM_SET(mld_poly_decompose_c) -void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0); +void mld_poly_decompose_32_c(mld_poly *a1, mld_poly *a0); void harness(void) { +#if MLD_CONFIG_PARAMETER_SET != 44 mld_poly *a0, *a1; - mld_poly_decompose_c(a1, a0); + mld_poly_decompose_32_c(a1, a0); +#endif } diff --git a/proofs/cbmc/poly_decompose_32_native_aarch64/Makefile b/proofs/cbmc/poly_decompose_32_native_aarch64/Makefile index 3b78a88b5..d97dd0f58 100644 --- a/proofs/cbmc/poly_decompose_32_native_aarch64/Makefile +++ b/proofs/cbmc/poly_decompose_32_native_aarch64/Makefile @@ -19,7 +19,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c # poly_decompose_32 is only used with ML-DSA-65 and ML-DSA-87 ifeq ($(MLD_CONFIG_PARAMETER_SET),65) @@ -52,10 +52,10 @@ CBMC_OBJECT_BITS = 8 # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file -# ("mldsa/poly_kl.c") in PROJECT_SOURCES). +# ("mldsa/poly.c") in PROJECT_SOURCES). # REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i # include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly_kl.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c # $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar # $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz # Care is required with variables on the left-hand side: REWRITTEN_SOURCES must diff --git a/proofs/cbmc/poly_decompose_88/Makefile b/proofs/cbmc/poly_decompose_88/Makefile new file mode 100644 index 000000000..22bb8804a --- /dev/null +++ b/proofs/cbmc/poly_decompose_88/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_decompose_88_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_decompose_88 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_88 +USE_FUNCTION_CONTRACTS=mld_poly_decompose_88_c +else +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_decompose_88 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/poly_decompose_88/poly_decompose_88_harness.c b/proofs/cbmc/poly_decompose_88/poly_decompose_88_harness.c new file mode 100644 index 000000000..d7e457747 --- /dev/null +++ b/proofs/cbmc/poly_decompose_88/poly_decompose_88_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly *a0, *a1; + mld_poly_decompose_88(a1, a0); +#endif +} diff --git a/proofs/cbmc/poly_decompose_88_c/Makefile b/proofs/cbmc/poly_decompose_88_c/Makefile new file mode 100644 index 000000000..aec11d190 --- /dev/null +++ b/proofs/cbmc/poly_decompose_88_c/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_decompose_88_c_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_decompose_88_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_88_c +USE_FUNCTION_CONTRACTS=mld_decompose_88 +else +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mld_poly_decompose_88_c + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +include ../Makefile.common diff --git a/proofs/cbmc/poly_decompose_88_c/poly_decompose_88_c_harness.c b/proofs/cbmc/poly_decompose_88_c/poly_decompose_88_c_harness.c new file mode 100644 index 000000000..15212611c --- /dev/null +++ b/proofs/cbmc/poly_decompose_88_c/poly_decompose_88_c_harness.c @@ -0,0 +1,15 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +// Prototype for the function under test +void mld_poly_decompose_88_c(mld_poly *a1, mld_poly *a0); + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly *a0, *a1; + mld_poly_decompose_88_c(a1, a0); +#endif +} diff --git a/proofs/cbmc/poly_decompose_88_native_aarch64/Makefile b/proofs/cbmc/poly_decompose_88_native_aarch64/Makefile index 0bdff0dad..2403b8199 100644 --- a/proofs/cbmc/poly_decompose_88_native_aarch64/Makefile +++ b/proofs/cbmc/poly_decompose_88_native_aarch64/Makefile @@ -19,7 +19,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c # poly_decompose_88 is only used with ML-DSA-44 ifeq ($(MLD_CONFIG_PARAMETER_SET),44) @@ -49,10 +49,10 @@ CBMC_OBJECT_BITS = 8 # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file -# ("mldsa/poly_kl.c") in PROJECT_SOURCES). +# ("mldsa/poly.c") in PROJECT_SOURCES). # REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i # include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly_kl.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c # $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar # $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz # Care is required with variables on the left-hand side: REWRITTEN_SOURCES must diff --git a/proofs/cbmc/poly_decompose_c/Makefile b/proofs/cbmc/poly_decompose_c/Makefile deleted file mode 100644 index 92a10d6e0..000000000 --- a/proofs/cbmc/poly_decompose_c/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = poly_decompose_c_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = poly_decompose_c - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c - -CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_c -USE_FUNCTION_CONTRACTS=mld_decompose -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 - -FUNCTION_NAME = mld_poly_decompose_c - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 10 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/poly_decompose_native/Makefile b/proofs/cbmc/poly_decompose_native/Makefile index 8bfb251cf..0f307a468 100644 --- a/proofs/cbmc/poly_decompose_native/Makefile +++ b/proofs/cbmc/poly_decompose_native/Makefile @@ -17,16 +17,16 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c -CHECK_FUNCTION_CONTRACTS=mld_poly_decompose -USE_FUNCTION_CONTRACTS= mld_poly_decompose_c ifeq ($(MLD_CONFIG_PARAMETER_SET),44) - USE_FUNCTION_CONTRACTS+=mld_poly_decompose_88_native -else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) - USE_FUNCTION_CONTRACTS+=mld_poly_decompose_32_native -else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) - USE_FUNCTION_CONTRACTS+=mld_poly_decompose_32_native +CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_88 +USE_FUNCTION_CONTRACTS=mld_poly_decompose_88_c +USE_FUNCTION_CONTRACTS+=mld_poly_decompose_88_native +else +CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_32 +USE_FUNCTION_CONTRACTS=mld_poly_decompose_32_c +USE_FUNCTION_CONTRACTS+=mld_poly_decompose_32_native endif APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c b/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c index bd08c2090..2e3d6e03d 100644 --- a/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c +++ b/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c @@ -1,11 +1,15 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -#include "poly_kl.h" +#include "poly.h" void harness(void) { mld_poly *a0, *a1; - mld_poly_decompose(a1, a0); +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly_decompose_88(a1, a0); +#else + mld_poly_decompose_32(a1, a0); +#endif } diff --git a/proofs/cbmc/poly_use_hint/Makefile b/proofs/cbmc/poly_use_hint/Makefile index 1fe11a03d..a7bcf415b 100644 --- a/proofs/cbmc/poly_use_hint/Makefile +++ b/proofs/cbmc/poly_use_hint/Makefile @@ -17,10 +17,14 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint -USE_FUNCTION_CONTRACTS=mld_poly_use_hint_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_88 +else +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_32 +endif APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_use_hint_32/Makefile b/proofs/cbmc/poly_use_hint_32/Makefile new file mode 100644 index 000000000..f2c85cb36 --- /dev/null +++ b/proofs/cbmc/poly_use_hint_32/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_use_hint_32_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_use_hint_32 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +else +CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_32 +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_32_c +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_use_hint_32 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/poly_use_hint_32/poly_use_hint_32_harness.c b/proofs/cbmc/poly_use_hint_32/poly_use_hint_32_harness.c new file mode 100644 index 000000000..7414eda7a --- /dev/null +++ b/proofs/cbmc/poly_use_hint_32/poly_use_hint_32_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET != 44 + mld_poly *a, *h; + mld_poly_use_hint_32(a, h); +#endif +} diff --git a/proofs/cbmc/poly_use_hint_32_c/Makefile b/proofs/cbmc/poly_use_hint_32_c/Makefile new file mode 100644 index 000000000..aa2e27b4b --- /dev/null +++ b/proofs/cbmc/poly_use_hint_32_c/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_use_hint_32_c_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_use_hint_32_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +else +CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_32_c +USE_FUNCTION_CONTRACTS=mld_use_hint_32 +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mld_poly_use_hint_32_c + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c b/proofs/cbmc/poly_use_hint_32_c/poly_use_hint_32_c_harness.c similarity index 52% rename from proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c rename to proofs/cbmc/poly_use_hint_32_c/poly_use_hint_32_c_harness.c index e358e2aab..ea8d04542 100644 --- a/proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c +++ b/proofs/cbmc/poly_use_hint_32_c/poly_use_hint_32_c_harness.c @@ -1,15 +1,15 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -#include "poly_kl.h" +#include "poly.h" // Prototype for the function under test -#define mld_poly_use_hint_c MLD_ADD_PARAM_SET(mld_poly_use_hint_c) -void mld_poly_use_hint_c(mld_poly *a, mld_poly *h); - +void mld_poly_use_hint_32_c(mld_poly *a, const mld_poly *h); void harness(void) { +#if MLD_CONFIG_PARAMETER_SET != 44 mld_poly *a, *h; - mld_poly_use_hint_c(a, h); + mld_poly_use_hint_32_c(a, h); +#endif } diff --git a/proofs/cbmc/poly_use_hint_88/Makefile b/proofs/cbmc/poly_use_hint_88/Makefile new file mode 100644 index 000000000..daa2e9c76 --- /dev/null +++ b/proofs/cbmc/poly_use_hint_88/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_use_hint_88_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_use_hint_88 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_88 +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_88_c +else +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_use_hint_88 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/poly_use_hint_88/poly_use_hint_88_harness.c b/proofs/cbmc/poly_use_hint_88/poly_use_hint_88_harness.c new file mode 100644 index 000000000..d598728a1 --- /dev/null +++ b/proofs/cbmc/poly_use_hint_88/poly_use_hint_88_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly *a, *h; + mld_poly_use_hint_88(a, h); +#endif +} diff --git a/proofs/cbmc/poly_use_hint_88_c/Makefile b/proofs/cbmc/poly_use_hint_88_c/Makefile new file mode 100644 index 000000000..d21eee7f8 --- /dev/null +++ b/proofs/cbmc/poly_use_hint_88_c/Makefile @@ -0,0 +1,41 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_use_hint_88_c_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_use_hint_88_c + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_88_c +USE_FUNCTION_CONTRACTS=mld_use_hint_88 +else +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = mld_poly_use_hint_88_c + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/poly_use_hint_88_c/poly_use_hint_88_c_harness.c b/proofs/cbmc/poly_use_hint_88_c/poly_use_hint_88_c_harness.c new file mode 100644 index 000000000..4fd2ee5ac --- /dev/null +++ b/proofs/cbmc/poly_use_hint_88_c/poly_use_hint_88_c_harness.c @@ -0,0 +1,15 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +// Prototype for the function under test +void mld_poly_use_hint_88_c(mld_poly *a, const mld_poly *h); + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly *a, *h; + mld_poly_use_hint_88_c(a, h); +#endif +} diff --git a/proofs/cbmc/poly_use_hint_c/Makefile b/proofs/cbmc/poly_use_hint_c/Makefile deleted file mode 100644 index 188b8e705..000000000 --- a/proofs/cbmc/poly_use_hint_c/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = poly_use_hint_c_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = poly_use_hint_c - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c - -CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_c -USE_FUNCTION_CONTRACTS=mld_use_hint -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 - -FUNCTION_NAME = mld_poly_use_hint_c - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 8 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/poly_use_hint_native/Makefile b/proofs/cbmc/poly_use_hint_native/Makefile index b4438cc33..3e58c0770 100644 --- a/proofs/cbmc/poly_use_hint_native/Makefile +++ b/proofs/cbmc/poly_use_hint_native/Makefile @@ -17,16 +17,16 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c -CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint -USE_FUNCTION_CONTRACTS=mld_poly_use_hint_c ifeq ($(MLD_CONFIG_PARAMETER_SET),44) - USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_88_native -else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) - USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_32_native -else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) - USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_32_native +CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_88 +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_88_c +USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_88_native +else +CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_32 +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_32_c +USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_32_native endif APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c b/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c index bf3e43b4f..5633cf7fb 100644 --- a/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c +++ b/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c @@ -1,11 +1,15 @@ // Copyright (c) The mldsa-native project authors // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -#include "poly_kl.h" +#include "poly.h" void harness(void) { mld_poly *a, *h; - mld_poly_use_hint(a, h); +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly_use_hint_88(a, h); +#else + mld_poly_use_hint_32(a, h); +#endif } diff --git a/proofs/cbmc/poly_use_hint_native_aarch64/Makefile b/proofs/cbmc/poly_use_hint_native_aarch64/Makefile index 4a5da443c..76b206f1d 100644 --- a/proofs/cbmc/poly_use_hint_native_aarch64/Makefile +++ b/proofs/cbmc/poly_use_hint_native_aarch64/Makefile @@ -19,7 +19,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c ifeq ($(MLD_CONFIG_PARAMETER_SET),44) CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_88_native diff --git a/proofs/cbmc/use_hint/Makefile b/proofs/cbmc/use_hint/Makefile deleted file mode 100644 index 5f01b0c1e..000000000 --- a/proofs/cbmc/use_hint/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = use_hint_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = use_hint - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c - -CHECK_FUNCTION_CONTRACTS=mld_use_hint -USE_FUNCTION_CONTRACTS=mld_decompose -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 - -FUNCTION_NAME = use_hint - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 8 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/use_hint_32/Makefile b/proofs/cbmc/use_hint_32/Makefile new file mode 100644 index 000000000..6c9870c5c --- /dev/null +++ b/proofs/cbmc/use_hint_32/Makefile @@ -0,0 +1,40 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = use_hint_32_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = use_hint_32 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS= +else +CHECK_FUNCTION_CONTRACTS=mld_use_hint_32 +endif +USE_FUNCTION_CONTRACTS=mld_decompose_32 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = use_hint_32 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/use_hint/use_hint_harness.c b/proofs/cbmc/use_hint_32/use_hint_32_harness.c similarity index 69% rename from proofs/cbmc/use_hint/use_hint_harness.c rename to proofs/cbmc/use_hint_32/use_hint_32_harness.c index 0fe55f929..60996b654 100644 --- a/proofs/cbmc/use_hint/use_hint_harness.c +++ b/proofs/cbmc/use_hint_32/use_hint_32_harness.c @@ -5,6 +5,8 @@ void harness(void) { +#if MLD_CONFIG_PARAMETER_SET != 44 int32_t a, r, hint; - r = mld_use_hint(a, hint); + r = mld_use_hint_32(a, hint); +#endif } diff --git a/proofs/cbmc/use_hint_88/Makefile b/proofs/cbmc/use_hint_88/Makefile new file mode 100644 index 000000000..5fe35a7a0 --- /dev/null +++ b/proofs/cbmc/use_hint_88/Makefile @@ -0,0 +1,40 @@ +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = use_hint_88_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = use_hint_88 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +CHECK_FUNCTION_CONTRACTS=mld_use_hint_88 +else +CHECK_FUNCTION_CONTRACTS= +endif +USE_FUNCTION_CONTRACTS=mld_decompose_88 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = use_hint_88 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/use_hint_88/use_hint_88_harness.c b/proofs/cbmc/use_hint_88/use_hint_88_harness.c new file mode 100644 index 000000000..34fee1a85 --- /dev/null +++ b/proofs/cbmc/use_hint_88/use_hint_88_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "rounding.h" + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + int32_t a, r, hint; + r = mld_use_hint_88(a, hint); +#endif +} diff --git a/test/src/test_unit.c b/test/src/test_unit.c index e7a6a5cb2..43604d9ef 100644 --- a/test/src/test_unit.c +++ b/test/src/test_unit.c @@ -41,11 +41,19 @@ void mld_poly_ntt_c(mld_poly *a); void mld_poly_invntt_tomont_c(mld_poly *a); void mld_poly_caddq_c(mld_poly *a); #if !defined(MLD_CONFIG_NO_SIGN_API) -void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0); +#if MLD_CONFIG_PARAMETER_SET == 44 +void mld_poly_decompose_88_c(mld_poly *a1, mld_poly *a0); +#else +void mld_poly_decompose_32_c(mld_poly *a1, mld_poly *a0); #endif +#endif /* !MLD_CONFIG_NO_SIGN_API */ #if !defined(MLD_CONFIG_NO_VERIFY_API) -void mld_poly_use_hint_c(mld_poly *a, const mld_poly *h); +#if MLD_CONFIG_PARAMETER_SET == 44 +void mld_poly_use_hint_88_c(mld_poly *a, const mld_poly *h); +#else +void mld_poly_use_hint_32_c(mld_poly *a, const mld_poly *h); #endif +#endif /* !MLD_CONFIG_NO_VERIFY_API */ uint32_t mld_poly_chknorm_c(const mld_poly *a, int32_t B); #if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API) void mld_poly_pointwise_montgomery_c(mld_poly *a, const mld_poly *b); @@ -444,7 +452,11 @@ static int test_poly_decompose_core(const mld_poly *input_poly, mld_memcpy(ref_a0, input_poly, sizeof(mld_poly)); mld_poly_decompose(test_a1, test_a0); - mld_poly_decompose_c(ref_a1, ref_a0); +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly_decompose_88_c(ref_a1, ref_a0); +#else + mld_poly_decompose_32_c(ref_a1, ref_a0); +#endif CHECK(compare_i32_arrays(test_a1->coeffs, ref_a1->coeffs, MLDSA_N, test_name, input_poly->coeffs)); @@ -568,7 +580,11 @@ static int test_poly_use_hint_core(const mld_poly *poly_a, *test_a = *poly_a; *ref_a = *poly_a; mld_poly_use_hint(test_a, poly_h); - mld_poly_use_hint_c(ref_a, poly_h); +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly_use_hint_88_c(ref_a, poly_h); +#else + mld_poly_use_hint_32_c(ref_a, poly_h); +#endif CHECK(compare_i32_arrays(test_a->coeffs, ref_a->coeffs, MLDSA_N, test_name, poly_a->coeffs));