CBMC: Use constant quantifier ranges in some loop invariants

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                                                             \
   {                                                                            \

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)
   )
   {

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)))

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)

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

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

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

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

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

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

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

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

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