From f04386d3d57198d78b353c606bf7be2328127be6 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Sun, 25 Oct 2026 22:38:20 +0800 Subject: [PATCH 1/2] CBMC: Add optional constant ranges to `forall` CBMC's propositional backend needs a constant upper limit to expand a quantifier. An invariant such as `forall(k, 0, i, P)` uses a variable upper bound, so the backend replaces it with an unconstrained literal and warns "ignoring forall". This can cause spurious failures with CaDiCaL. Keep `forall(k, lb, ub, P)` and add `forall(k, lb, ub, max, P)`. Implement the five-argument form with `CBMC_FORALL` over `[0, max)`, guarding the predicate with `lb <= k && k < ub`. `max` must be a compile-time constant, and callers must ensure `ub <= max`. The macro does not check that bound. Dispatch between the forms by argument count using C99 variadic macros. Supply a trailing selector argument so the four-argument call also leaves a nonempty variadic tail. The four-argument form still handles a variable lower bound when the upper bound is constant. Use the new form only for variable upper bounds in `poly_add`, `polyveck_caddq`, `polyveck_decompose_pack_w1`, `polyveck_invntt_tomont`, `polyveck_ntt`, `polyveck_reduce`, `polyvecl_ntt` and `unpack_sk_t0hat`, and add CaDiCaL as their second solver. Other calls retain the four-argument form. Signed-off-by: Matthias J. Kannwischer Signed-off-by: Hanno Becker --- mldsa/src/cbmc.h | 22 ++++++++++++++++++- mldsa/src/poly.c | 6 ++--- mldsa/src/polyvec.c | 12 +++++----- mldsa/src/polyvec_lazy.h | 2 +- proofs/cbmc/poly_add/Makefile | 4 +++- proofs/cbmc/polyveck_caddq/Makefile | 4 +++- .../cbmc/polyveck_decompose_pack_w1/Makefile | 4 +++- proofs/cbmc/polyveck_invntt_tomont/Makefile | 4 +++- proofs/cbmc/polyveck_ntt/Makefile | 4 +++- proofs/cbmc/polyveck_reduce/Makefile | 4 +++- proofs/cbmc/polyvecl_ntt/Makefile | 4 +++- proofs/cbmc/unpack_sk_t0hat/Makefile | 4 +++- 12 files changed, 55 insertions(+), 19 deletions(-) diff --git a/mldsa/src/cbmc.h b/mldsa/src/cbmc.h index 272acf66bb..0996fd3a3d 100644 --- a/mldsa/src/cbmc.h +++ b/mldsa/src/cbmc.h @@ -105,6 +105,15 @@ * Note that the range on qvar is _exclusive_ between qvar_lb .. qvar_ub * https://diffblue.github.io/cbmc/contracts-quantifiers.html * + * forall(qvar, qvar_lb, qvar_ub, predicate) quantifies directly over + * [qvar_lb, qvar_ub). + * + * forall(qvar, qvar_lb, qvar_ub, qvar_max, predicate) additionally takes a + * compile-time constant qvar_max. It quantifies over [0, qvar_max) and + * restricts to [qvar_lb, qvar_ub) via an implication. Use this form when + * qvar_ub is variable, so the propositional backend can expand a constant + * range. A variable qvar_lb alone does not require this form. + * * The quantified variable is declared as uint32_t, so these macros * quantify only over indices in [0, UINT32_MAX). Bounds larger than * UINT32_MAX (4 GiB) are NOT supported: the explicit (uint32_t) casts @@ -122,13 +131,24 @@ * Prevent clang-format from corrupting CBMC's special ==> operator */ /* clang-format off */ -#define forall(qvar, qvar_lb, qvar_ub, predicate) \ +#define CBMC_FORALL(qvar, qvar_lb, qvar_ub, predicate) \ __CPROVER_forall \ { \ uint32_t qvar; \ ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> (predicate) \ } +#define CBMC_FORALL_BOUNDED(qvar, qvar_lb, qvar_ub, qvar_max, predicate) \ + CBMC_FORALL(qvar, 0, qvar_max, \ + ((uint32_t)(qvar_lb) <= (qvar) && \ + (qvar) < (uint32_t)(qvar_ub)) ==> (predicate)) + +/* The final argument keeps the selector's variadic tail nonempty in C99. */ +#define CBMC_FORALL_SELECT(_1, _2, _3, _4, _5, NAME, ...) NAME +#define forall(...) \ + CBMC_FORALL_SELECT(__VA_ARGS__, CBMC_FORALL_BOUNDED, CBMC_FORALL, \ + unused)(__VA_ARGS__) + #define exists(qvar, qvar_lb, qvar_ub, predicate) \ __CPROVER_exists \ { \ diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index 4153d80b8d..c1e7a5e19a 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -104,9 +104,9 @@ void mld_poly_add(mld_poly *r, const mld_poly *b) assigns(i, memory_slice(r, sizeof(mld_poly))) invariant(i <= MLDSA_N) invariant(forall(k0, i, MLDSA_N, r->coeffs[k0] == loop_entry(*r).coeffs[k0])) - invariant(forall(k1, 0, i, r->coeffs[k1] == loop_entry(*r).coeffs[k1] + b->coeffs[k1])) - invariant(forall(k2, 0, i, r->coeffs[k2] < MLD_REDUCE32_DOMAIN_MAX)) - invariant(forall(k2, 0, i, r->coeffs[k2] >= INT32_MIN)) + invariant(forall(k1, 0, i, MLDSA_N, r->coeffs[k1] == loop_entry(*r).coeffs[k1] + b->coeffs[k1])) + invariant(forall(k2, 0, i, MLDSA_N, r->coeffs[k2] < MLD_REDUCE32_DOMAIN_MAX)) + invariant(forall(k2, 0, i, MLDSA_N, r->coeffs[k2] >= INT32_MIN)) decreases(MLDSA_N - i) ) { diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index be13ae3f91..da2eec1cbf 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -86,7 +86,7 @@ void mld_polyvecl_ntt(mld_polyvecl *v) assigns(i, memory_slice(v, sizeof(mld_polyvecl))) invariant(i <= MLDSA_L) invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) - invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) + invariant(forall(k1, 0, i, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) decreases(MLDSA_L - i)) { mld_poly_ntt(&v->vec[i]); @@ -253,7 +253,7 @@ void mld_polyveck_reduce(mld_polyveck *v) assigns(i, memory_slice(v, sizeof(mld_polyveck))) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) - invariant(forall(k2, 0, i, + invariant(forall(k2, 0, i, MLDSA_K, array_bound(v->vec[k2].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))) decreases(MLDSA_K - i) ) @@ -279,7 +279,7 @@ void mld_polyveck_caddq(mld_polyveck *v) assigns(i, memory_slice(v, sizeof(mld_polyveck))) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) - invariant(forall(k1, 0, i, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) + invariant(forall(k1, 0, i, MLDSA_K, array_bound(v->vec[k1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) decreases(MLDSA_K - i)) { mld_poly_caddq(&v->vec[i]); @@ -302,7 +302,7 @@ void mld_polyveck_ntt(mld_polyveck *v) assigns(i, memory_slice(v, sizeof(mld_polyveck))) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) - invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) + invariant(forall(k1, 0, i, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) decreases(MLDSA_K - i)) { mld_poly_ntt(&v->vec[i]); @@ -324,7 +324,7 @@ void mld_polyveck_invntt_tomont(mld_polyveck *v) assigns(i, memory_slice(v, sizeof(mld_polyveck))) invariant(i <= MLDSA_K) invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1]))) - invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) + invariant(forall(k1, 0, i, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) decreases(MLDSA_K - i)) { mld_poly_invntt_tomont(&v->vec[i]); @@ -379,7 +379,7 @@ void mld_polyveck_decompose_pack_w1( memory_slice(scratch, sizeof(mld_poly)), memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES)) invariant(i <= MLDSA_K) - invariant(forall(k1, 0, i, + invariant(forall(k1, 0, i, MLDSA_K, array_abs_bound(v0->vec[k1].coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1))) invariant(forall(k2, i, MLDSA_K, array_bound(v0->vec[k2].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) diff --git a/mldsa/src/polyvec_lazy.h b/mldsa/src/polyvec_lazy.h index 7f5de4a4e9..e865f39dc7 100644 --- a/mldsa/src/polyvec_lazy.h +++ b/mldsa/src/polyvec_lazy.h @@ -288,7 +288,7 @@ __contract__( __loop__( assigns(i, memory_slice(t0, sizeof(mld_sk_t0hat_eager))) invariant(i <= MLDSA_K) - invariant(forall(k0, 0, i, + invariant(forall(k0, 0, i, MLDSA_K, array_bound(t0->vec.vec[k0].coeffs, 0, MLDSA_N, -(1 << (MLDSA_D - 1)) + 1, (1 << (MLDSA_D - 1)) + 1))) decreases(MLDSA_K - i) diff --git a/proofs/cbmc/poly_add/Makefile b/proofs/cbmc/poly_add/Makefile index 7b7396f919..7197131258 100644 --- a/proofs/cbmc/poly_add/Makefile +++ b/proofs/cbmc/poly_add/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cadical CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = poly_add diff --git a/proofs/cbmc/polyveck_caddq/Makefile b/proofs/cbmc/polyveck_caddq/Makefile index a86e61f075..572f6cc5b6 100644 --- a/proofs/cbmc/polyveck_caddq/Makefile +++ b/proofs/cbmc/polyveck_caddq/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cadical CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyveck_caddq diff --git a/proofs/cbmc/polyveck_decompose_pack_w1/Makefile b/proofs/cbmc/polyveck_decompose_pack_w1/Makefile index 7e3d1238ed..255f2d70c9 100644 --- a/proofs/cbmc/polyveck_decompose_pack_w1/Makefile +++ b/proofs/cbmc/polyveck_decompose_pack_w1/Makefile @@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cadical CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyveck_decompose_pack_w1 diff --git a/proofs/cbmc/polyveck_invntt_tomont/Makefile b/proofs/cbmc/polyveck_invntt_tomont/Makefile index 7cb933c7ee..dfa57af0bd 100644 --- a/proofs/cbmc/polyveck_invntt_tomont/Makefile +++ b/proofs/cbmc/polyveck_invntt_tomont/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cadical CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyveck_invntt_tomont diff --git a/proofs/cbmc/polyveck_ntt/Makefile b/proofs/cbmc/polyveck_ntt/Makefile index 50dcc855de..502e75407d 100644 --- a/proofs/cbmc/polyveck_ntt/Makefile +++ b/proofs/cbmc/polyveck_ntt/Makefile @@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cadical CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyveck_ntt diff --git a/proofs/cbmc/polyveck_reduce/Makefile b/proofs/cbmc/polyveck_reduce/Makefile index f2b914bdab..b3fb96ba9c 100644 --- a/proofs/cbmc/polyveck_reduce/Makefile +++ b/proofs/cbmc/polyveck_reduce/Makefile @@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cadical CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyveck_reduce diff --git a/proofs/cbmc/polyvecl_ntt/Makefile b/proofs/cbmc/polyvecl_ntt/Makefile index 5283f03be1..65b692b55f 100644 --- a/proofs/cbmc/polyvecl_ntt/Makefile +++ b/proofs/cbmc/polyvecl_ntt/Makefile @@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cadical CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = polyvecl_ntt diff --git a/proofs/cbmc/unpack_sk_t0hat/Makefile b/proofs/cbmc/unpack_sk_t0hat/Makefile index da376e2395..9136353b33 100644 --- a/proofs/cbmc/unpack_sk_t0hat/Makefile +++ b/proofs/cbmc/unpack_sk_t0hat/Makefile @@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Supported CBMC configurations -CBMC_SUPPORTED_CONFIGS = LP64:z3 +CBMC_SUPPORTED_CONFIGS = \ + LP64:z3 \ + LP64:cadical CBMC_DEFAULT_CONFIG = LP64:z3 FUNCTION_NAME = unpack_sk_t0hat From e052dc946491387eda0ce1fbd62f1a397cceb42f Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Mon, 26 Oct 2026 20:50:02 +0800 Subject: [PATCH 2/2] CBMC: Run CaDiCaL proofs in the expensive job pool Mark the cadical solver profile as expensive so that CaDiCaL configurations run in the existing expensive job pool. This limits concurrent SAT array expansion and reduces memory pressure. Other proofs retain their existing scheduling, and disabling pools still permits unrestricted execution. Signed-off-by: Matthias J. Kannwischer --- proofs/cbmc/Makefile.common | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common index 7cf25d8806..46c01a64ae 100644 --- a/proofs/cbmc/Makefile.common +++ b/proofs/cbmc/Makefile.common @@ -234,6 +234,8 @@ CBMC_PROFILE_cadical_BACKEND := CBMC_PROFILE_cadical_PROVER_NAME := CaDiCaL CBMC_PROFILE_cadical_SMT_FORMAT := CBMC_PROFILE_cadical_FLAGS := --sat-solver cadical +# SAT array expansion can consume many GiB before solving starts. +CBMC_PROFILE_cadical_EXPENSIVE := true # Make evaluates the configuration checks below before running target recipes. # The runner queries these metadata targets before selecting CBMC_DM/CBMC_SOLVER. @@ -303,7 +305,7 @@ endif # CBMC_SKIP_CONFIG_RESOLUTION # Job pools # For version of Litani that are new enough (where `litani print-capabilities` -# prints "pools"), proofs for which `EXPENSIVE = true` is set can be added to a +# prints "pools"), proofs or solver profiles marked EXPENSIVE can be added to a # "job pool" that restricts how many expensive proofs are run at a time. All # other proofs will be built in parallel as usual. # @@ -330,7 +332,7 @@ endif # CBMC_SKIP_CONFIG_RESOLUTION ifeq ($(strip $(ENABLE_POOLS)),) POOL = INIT_POOLS = -else ifeq ($(strip $(EXPENSIVE)),) +else ifeq ($(strip $(EXPENSIVE) $(CBMC_PROFILE_$(CBMC_SOLVER)_EXPENSIVE)),) POOL = INIT_POOLS = else