From c060d6dc6f5fcc1151fce0b1118cd82d7a9f99ea Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 2 Jun 2026 16:00:00 +0800 Subject: [PATCH 1/2] poly: Value-specialize polyw1_pack to deduplicate multilevel builds polyw1_pack depends only on GAMMA2, so ML-DSA-65 and -87 use identical code. Move it into the shared poly.c as mld_polyw1_pack_{88,32}, compiled once, with a thin dispatcher in poly_kl.h, so a multilevel build shares a single copy instead of emitting one per parameter set. Split the CBMC proof into per-variant proofs plus a dispatcher proof. - Towards #536 Signed-off-by: Matthias J. Kannwischer --- mldsa/mldsa_native.c | 6 +++ mldsa/mldsa_native_asm.S | 6 +++ mldsa/src/params.h | 17 +++--- mldsa/src/poly.c | 52 +++++++++++++++++++ mldsa/src/poly.h | 45 ++++++++++++++++ mldsa/src/poly_kl.c | 32 ------------ mldsa/src/poly_kl.h | 16 ++++-- proofs/cbmc/polyw1_pack/Makefile | 8 ++- proofs/cbmc/polyw1_pack_32/Makefile | 40 ++++++++++++++ .../polyw1_pack_32/polyw1_pack_32_harness.c | 13 +++++ proofs/cbmc/polyw1_pack_88/Makefile | 40 ++++++++++++++ .../polyw1_pack_88/polyw1_pack_88_harness.c | 13 +++++ 12 files changed, 244 insertions(+), 44 deletions(-) create mode 100644 proofs/cbmc/polyw1_pack_32/Makefile create mode 100644 proofs/cbmc/polyw1_pack_32/polyw1_pack_32_harness.c create mode 100644 proofs/cbmc/polyw1_pack_88/Makefile create mode 100644 proofs/cbmc/polyw1_pack_88/polyw1_pack_88_harness.c diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index fd5e3006b..4d5f9d9a5 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -280,6 +280,8 @@ #undef MLDSA_ETA #undef MLDSA_GAMMA1 #undef MLDSA_GAMMA2 +#undef MLDSA_GAMMA2_32 +#undef MLDSA_GAMMA2_88 #undef MLDSA_K #undef MLDSA_L #undef MLDSA_N @@ -294,6 +296,8 @@ #undef MLDSA_POLYT1_PACKEDBYTES #undef MLDSA_POLYVECH_PACKEDBYTES #undef MLDSA_POLYW1_PACKEDBYTES +#undef MLDSA_POLYW1_PACKEDBYTES_32 +#undef MLDSA_POLYW1_PACKEDBYTES_88 #undef MLDSA_POLYZ_PACKEDBYTES #undef MLDSA_Q #undef MLDSA_Q_HALF @@ -487,6 +491,8 @@ #undef mld_polyt0_unpack #undef mld_polyt1_pack #undef mld_polyt1_unpack +#undef mld_polyw1_pack_32 +#undef mld_polyw1_pack_88 /* mldsa/src/randombytes.h */ #undef MLD_RANDOMBYTES_H /* mldsa/src/reduce.h */ diff --git a/mldsa/mldsa_native_asm.S b/mldsa/mldsa_native_asm.S index df3c4d22d..57518c8cd 100644 --- a/mldsa/mldsa_native_asm.S +++ b/mldsa/mldsa_native_asm.S @@ -287,6 +287,8 @@ #undef MLDSA_ETA #undef MLDSA_GAMMA1 #undef MLDSA_GAMMA2 +#undef MLDSA_GAMMA2_32 +#undef MLDSA_GAMMA2_88 #undef MLDSA_K #undef MLDSA_L #undef MLDSA_N @@ -301,6 +303,8 @@ #undef MLDSA_POLYT1_PACKEDBYTES #undef MLDSA_POLYVECH_PACKEDBYTES #undef MLDSA_POLYW1_PACKEDBYTES +#undef MLDSA_POLYW1_PACKEDBYTES_32 +#undef MLDSA_POLYW1_PACKEDBYTES_88 #undef MLDSA_POLYZ_PACKEDBYTES #undef MLDSA_Q #undef MLDSA_Q_HALF @@ -494,6 +498,8 @@ #undef mld_polyt0_unpack #undef mld_polyt1_pack #undef mld_polyt1_unpack +#undef mld_polyw1_pack_32 +#undef mld_polyw1_pack_88 /* mldsa/src/randombytes.h */ #undef MLD_RANDOMBYTES_H /* mldsa/src/reduce.h */ diff --git a/mldsa/src/params.h b/mldsa/src/params.h index 94960a5c2..acc9a1a0e 100644 --- a/mldsa/src/params.h +++ b/mldsa/src/params.h @@ -14,6 +14,11 @@ #define MLDSA_Q_HALF ((MLDSA_Q + 1) / 2) #define MLDSA_D 13 +#define MLDSA_GAMMA2_88 ((MLDSA_Q - 1) / 88) +#define MLDSA_GAMMA2_32 ((MLDSA_Q - 1) / 32) +#define MLDSA_POLYW1_PACKEDBYTES_88 192 +#define MLDSA_POLYW1_PACKEDBYTES_32 128 + #if MLD_CONFIG_PARAMETER_SET == 44 #define MLDSA_K 4 @@ -22,11 +27,11 @@ #define MLDSA_TAU 39 #define MLDSA_BETA 78 #define MLDSA_GAMMA1 (1 << 17) -#define MLDSA_GAMMA2 ((MLDSA_Q - 1) / 88) +#define MLDSA_GAMMA2 MLDSA_GAMMA2_88 #define MLDSA_OMEGA 80 #define MLDSA_CTILDEBYTES 32 #define MLDSA_POLYZ_PACKEDBYTES 576 -#define MLDSA_POLYW1_PACKEDBYTES 192 +#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_88 #define MLDSA_POLYETA_PACKEDBYTES 96 #elif MLD_CONFIG_PARAMETER_SET == 65 @@ -37,11 +42,11 @@ #define MLDSA_TAU 49 #define MLDSA_BETA 196 #define MLDSA_GAMMA1 (1 << 19) -#define MLDSA_GAMMA2 ((MLDSA_Q - 1) / 32) +#define MLDSA_GAMMA2 MLDSA_GAMMA2_32 #define MLDSA_OMEGA 55 #define MLDSA_CTILDEBYTES 48 #define MLDSA_POLYZ_PACKEDBYTES 640 -#define MLDSA_POLYW1_PACKEDBYTES 128 +#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_32 #define MLDSA_POLYETA_PACKEDBYTES 128 #elif MLD_CONFIG_PARAMETER_SET == 87 @@ -52,11 +57,11 @@ #define MLDSA_TAU 60 #define MLDSA_BETA 120 #define MLDSA_GAMMA1 (1 << 19) -#define MLDSA_GAMMA2 ((MLDSA_Q - 1) / 32) +#define MLDSA_GAMMA2 MLDSA_GAMMA2_32 #define MLDSA_OMEGA 75 #define MLDSA_CTILDEBYTES 64 #define MLDSA_POLYZ_PACKEDBYTES 640 -#define MLDSA_POLYW1_PACKEDBYTES 128 +#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_32 #define MLDSA_POLYETA_PACKEDBYTES 96 #endif /* MLD_CONFIG_PARAMETER_SET == 87 */ diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index 3408c41a0..12ed2cf8d 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -1005,6 +1005,58 @@ uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) return mld_poly_chknorm_c(a, B); } +#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \ + MLD_CONFIG_PARAMETER_SET == 44 +MLD_INTERNAL_API +void mld_polyw1_pack_88(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_88], + const mld_poly *a) +{ + unsigned int i; + + mld_assert_bound(a->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_88)); + + for (i = 0; i < MLDSA_N / 4; ++i) + __loop__( + invariant(i <= MLDSA_N/4) + decreases(MLDSA_N / 4 - i)) + { + r[3 * i + 0] = (uint8_t)((a->coeffs[4 * i + 0]) & 0xFF); + r[3 * i + 0] |= (uint8_t)((a->coeffs[4 * i + 1] << 6) & 0xFF); + r[3 * i + 1] = (uint8_t)((a->coeffs[4 * i + 1] >> 2) & 0xFF); + r[3 * i + 1] |= (uint8_t)((a->coeffs[4 * i + 2] << 4) & 0xFF); + r[3 * i + 2] = (uint8_t)((a->coeffs[4 * i + 2] >> 4) & 0xFF); + r[3 * i + 2] |= (uint8_t)((a->coeffs[4 * i + 3] << 2) & 0xFF); + } +} +#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_INTERNAL_API +void mld_polyw1_pack_32(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_32], + const mld_poly *a) +{ + unsigned int i; + + mld_assert_bound(a->coeffs, MLDSA_N, 0, + (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_32)); + + for (i = 0; i < MLDSA_N / 2; ++i) + __loop__( + invariant(i <= MLDSA_N/2) + decreases(MLDSA_N / 2 - i)) + { + r[i] = + (uint8_t)((a->coeffs[2 * i + 0] | (a->coeffs[2 * i + 1] << 4)) & 0xFF); + } +} +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ + || MLD_CONFIG_PARAMETER_SET == 87 */ +#endif /* !MLD_CONFIG_NO_SIGN_API || !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 bb0e45251..d22f1b037 100644 --- a/mldsa/src/poly.h +++ b/mldsa/src/poly.h @@ -378,4 +378,49 @@ __contract__( ensures((return_value == 0) == array_abs_bound(a->coeffs, 0, MLDSA_N, B)) ); +#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44 +#define mld_polyw1_pack_88 MLD_NAMESPACE(polyw1_pack_88) +/** + * Bit-pack polynomial w1 for GAMMA2 = (MLDSA_Q-1)/88 (coefficients in [0, 43]). + * Input coefficients are assumed to be standard representatives. + * + * @param[out] r Pointer to output byte array (MLDSA_POLYW1_PACKEDBYTES_88). + * @param[in] a Pointer to input polynomial. + */ +MLD_INTERNAL_API +void mld_polyw1_pack_88(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_88], + const mld_poly *a) +__contract__( + requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES_88)) + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88))) + assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES_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_polyw1_pack_32 MLD_NAMESPACE(polyw1_pack_32) +/** + * Bit-pack polynomial w1 for GAMMA2 = (MLDSA_Q-1)/32 (coefficients in [0, 15]). + * Input coefficients are assumed to be standard representatives. + * + * @param[out] r Pointer to output byte array (MLDSA_POLYW1_PACKEDBYTES_32). + * @param[in] a Pointer to input polynomial. + */ +MLD_INTERNAL_API +void mld_polyw1_pack_32(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_32], + const mld_poly *a) +__contract__( + requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES_32)) + requires(memory_no_alias(a, sizeof(mld_poly))) + requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32))) + assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES_32)) +); +#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \ + || MLD_CONFIG_PARAMETER_SET == 87 */ +#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */ + #endif /* !MLD_POLY_H */ diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index 4ce6ac7a6..5be537d46 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -893,38 +893,6 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) mld_polyz_unpack_c(r, a); } - -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) - decreases(MLDSA_N / 4 - i)) - { - r[3 * i + 0] = (uint8_t)((a->coeffs[4 * i + 0]) & 0xFF); - r[3 * i + 0] |= (uint8_t)((a->coeffs[4 * i + 1] << 6) & 0xFF); - r[3 * i + 1] = (uint8_t)((a->coeffs[4 * i + 1] >> 2) & 0xFF); - r[3 * i + 1] |= (uint8_t)((a->coeffs[4 * i + 2] << 4) & 0xFF); - r[3 * i + 2] = (uint8_t)((a->coeffs[4 * i + 2] >> 4) & 0xFF); - r[3 * i + 2] |= (uint8_t)((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) - decreases(MLDSA_N / 2 - i)) - { - r[i] = - (uint8_t)((a->coeffs[2 * i + 0] | (a->coeffs[2 * i + 1] << 4)) & 0xFF); - } -#endif /* MLD_CONFIG_PARAMETER_SET != 44 */ -} #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */ /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. */ diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h index 2e5163ce1..363fa4929 100644 --- a/mldsa/src/poly_kl.h +++ b/mldsa/src/poly_kl.h @@ -306,20 +306,28 @@ __contract__( #define mld_polyw1_pack MLD_NAMESPACE_KL(polyw1_pack) /** * Bit-pack polynomial w1 with coefficients in [0, 15] or [0, 43]. Input - * coefficients are assumed to be standard representatives. + * coefficients are assumed to be standard representatives. Dispatches to the + * value-specialized variant for the selected parameter set. * * @param[out] r Pointer to output byte array with at least * MLDSA_POLYW1_PACKEDBYTES bytes. * @param[in] a Pointer to input polynomial. */ -MLD_INTERNAL_API -void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a) +static MLD_INLINE void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], + const mld_poly *a) __contract__( requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES)) requires(memory_no_alias(a, sizeof(mld_poly))) requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES)) -); +) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_polyw1_pack_88(r, a); +#else + mld_polyw1_pack_32(r, a); +#endif +} #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */ #endif /* !MLD_POLY_KL_H */ diff --git a/proofs/cbmc/polyw1_pack/Makefile b/proofs/cbmc/polyw1_pack/Makefile index 658175e75..6215fae0d 100644 --- a/proofs/cbmc/polyw1_pack/Makefile +++ b/proofs/cbmc/polyw1_pack/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_polyw1_pack -USE_FUNCTION_CONTRACTS= +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) +USE_FUNCTION_CONTRACTS=mld_polyw1_pack_88 +else +USE_FUNCTION_CONTRACTS=mld_polyw1_pack_32 +endif APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/polyw1_pack_32/Makefile b/proofs/cbmc/polyw1_pack_32/Makefile new file mode 100644 index 000000000..e452d6d24 --- /dev/null +++ b/proofs/cbmc/polyw1_pack_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 = polyw1_pack_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 = polyw1_pack_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_polyw1_pack_32 +endif +USE_FUNCTION_CONTRACTS= +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 = polyw1_pack_32 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/polyw1_pack_32/polyw1_pack_32_harness.c b/proofs/cbmc/polyw1_pack_32/polyw1_pack_32_harness.c new file mode 100644 index 000000000..365800515 --- /dev/null +++ b/proofs/cbmc/polyw1_pack_32/polyw1_pack_32_harness.c @@ -0,0 +1,13 @@ +// 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; + uint8_t *r; + mld_polyw1_pack_32(r, a); +#endif +} diff --git a/proofs/cbmc/polyw1_pack_88/Makefile b/proofs/cbmc/polyw1_pack_88/Makefile new file mode 100644 index 000000000..4adf45808 --- /dev/null +++ b/proofs/cbmc/polyw1_pack_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 = polyw1_pack_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 = polyw1_pack_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_polyw1_pack_88 +else +CHECK_FUNCTION_CONTRACTS= +endif +USE_FUNCTION_CONTRACTS= +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 = polyw1_pack_88 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +include ../Makefile.common diff --git a/proofs/cbmc/polyw1_pack_88/polyw1_pack_88_harness.c b/proofs/cbmc/polyw1_pack_88/polyw1_pack_88_harness.c new file mode 100644 index 000000000..405e1690b --- /dev/null +++ b/proofs/cbmc/polyw1_pack_88/polyw1_pack_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 "poly.h" + +void harness(void) +{ +#if MLD_CONFIG_PARAMETER_SET == 44 + mld_poly *a; + uint8_t *r; + mld_polyw1_pack_88(r, a); +#endif +} From a828efe00d2e8ad53992760a244675acb2db85d6 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 3 Jun 2026 15:31:27 +0800 Subject: [PATCH 2/2] CBMC: Use bitwuzla backend for poly_ntt_c proof On aarch64 (the CBMC CI runner) z3 is not stable for this proof: the individual proofs (for reduce_ram mode) runs for over 20 minutes and times out when run in parallel with other proofs. The proof completes in seconds on x86_64, and it also works in non-reduced-ram mode even though this code is indepdendent of it. Alternatives measured on aarch64 (ML-DSA-44, reduce-ram): z3 4.15.3 / 4.16.0 > 20 min bump OBJECT_BITS no effect (still > 20 min) SAT backend ~25 s bitwuzla ~2 min Both SAT and bitwuzla resolve the timeout; use bitwuzla. Signed-off-by: Matthias J. Kannwischer --- proofs/cbmc/poly_ntt_c/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/cbmc/poly_ntt_c/Makefile b/proofs/cbmc/poly_ntt_c/Makefile index 26fca0df9..18323a754 100644 --- a/proofs/cbmc/poly_ntt_c/Makefile +++ b/proofs/cbmc/poly_ntt_c/Makefile @@ -26,7 +26,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--bitwuzla FUNCTION_NAME = mld_poly_ntt_c