diff --git a/mldsa/src/cbmc.h b/mldsa/src/cbmc.h index 272acf66bb..fb03ef91f6 100644 --- a/mldsa/src/cbmc.h +++ b/mldsa/src/cbmc.h @@ -105,6 +105,16 @@ * 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. + * This form is false if qvar_lb or qvar_ub exceeds qvar_max. + * * 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 +132,30 @@ * 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) \ + ((uint32_t)(qvar_lb) <= (uint32_t)(qvar_max) && \ + (uint32_t)(qvar_ub) <= (uint32_t)(qvar_max) && \ + __CPROVER_forall \ + { \ + uint32_t qvar; \ + (qvar) < (uint32_t)(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/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 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