feat(symbolic): prove bounded mul-div monotonicity (#15696)

Author: figtracer

crates/evm/symbolic/README.md

@@ -588,7 +588,7 @@ Known incomplete, bounded, or approximate surfaces include:
 | Symbolic hashing and `KECCAK256` | Concrete hashes are computed exactly. Symbolic `KECCAK256` is represented by deterministic opaque terms plus Solidity-storage-layout heuristics for common mapping and dynamic-array keys. Proof obligations that depend on cryptographic facts such as non-zero hashes, collision resistance, or preimage resistance are not proof-grade and may report incomplete or produce replay-filtered candidates. |
 | Symbolic storage base values | Writes and later reads through symbolic keys are modeled, with Solidity-layout heuristics for common mapping/dynamic-array keys. Reads of previously-unwritten symbolic keys are abstract storage variables by default, or zero under the zero-init storage layout; the engine does not enumerate arbitrary concrete backend storage slots for a symbolic key. Proofs involving unknown existing storage are scoped to the selected `symbolic.storage_layout`. |
 | Precompiles | Canonical precompiles are recognized according to the active EVM version; KZG `0x0a` is Cancun+ only and falls back to normal empty-account behavior on earlier hardforks. Concrete inputs for modeled precompiles execute the corresponding revm precompile with effectively unlimited gas. Symbolic identity is byte-precise; symbolic hash/ecrecover/modexp outputs are deterministic opaque terms or fixed-length symbolic outputs, not full cryptographic/algebraic models. Symbolic BN254 inputs and symbolic BLAKE2f final flags report incomplete because precompile success depends on validity checks the symbolic model does not prove. KZG `0x0a` concrete inputs execute the revm KZG precompile exactly. Symbolic KZG calls model broad exact failures such as invalid input length and version/hash mismatches where known, plus selected replayable success/failure witnesses. Any remaining feasible symbolic KZG space reports incomplete rather than being treated as proved safe. Symbolic length headers, symbolic modexp output lengths, out-of-bounds symbolic inputs, future/custom precompiles, and precompile gas/OOG behavior are not fully modeled. |
-| Hard arithmetic | Bit-vector arithmetic is modeled through SMT. Some expensive arithmetic has bounded helpers, but unsupported `EXP` base/exponent shapes and other solver-intractable forms can report incomplete or timeout. |
+| Hard arithmetic | Bit-vector arithmetic is modeled through SMT. Forge proves unsigned monotonic product and same-divisor quotient comparisons when path bounds show that every product fits in 256 bits. Other expensive arithmetic has bounded helpers, but unsupported `EXP` base/exponent shapes and solver-intractable nonlinear identities can report incomplete or timeout. |
 | Cheatcode surface | The common testing cheatcodes listed below are modeled for safe concrete/symbolic forms. Unsupported Foundry/VM compatibility cheatcodes, value-bearing cheatcode calls, delegatecall prank forms, symbolic `expectCall` gas, unsupported symbolic `vm.bound` ranges, and unsupported symbolic `assumeNoRevert` decodes/overlaps report incomplete. |
 | Approximate/no-op cheatcodes | Some recognized Foundry helpers are accepted but not semantically checked under symbolic execution, including non-observable gas metering helpers, access-list/warm/cool helpers, `allowCheatcodes`, `sleep`, and breakpoints. Observable EVM-version helpers, gas snapshot/read helpers, and safe-memory expectation helpers report incomplete instead of fabricating results or silently accepting assertions. |
 | Fork mutation during symbolic execution | Fork-backed setup is allowed before symbolic execution. Creating forks, selecting a different fork, or rolling/mutating fork blocks during symbolic execution is restricted and reports incomplete unless it stays on the already active fork in the supported form. |

crates/evm/symbolic/src/runtime/solver.rs

@@ -12,7 +12,7 @@ pub(crate) use hard_arith_fallback::{
 };
 #[cfg(test)]
 pub(crate) use monotonic_product::product_monotonic_unsat;
-use monotonic_product::product_monotonic_unsat_normalized;
+use monotonic_product::{product_monotonic_unsat_normalized, remove_implied_monotonic_constraints};
 pub(crate) use opt::normalize_constraints_for_solver;
 use opt::{constraints_are_directly_unsat, sorted_bool_exprs_are_subset, write_smt_assertions};
 #[cfg(test)]
@@ -460,7 +460,7 @@ impl SmtLibSubprocessSolver {
         defer_hard_arith_without_witness: bool,
     ) -> Result<bool, SymbolicError> {
         self.sat_queries += 1;
-        let smt_constraints = normalize_constraints_for_solver(cx, constraints);
+        let smt_constraints = normalize_sat_constraints(cx, constraints);
         let cache_key = smt_constraints.clone();
         if let Some(result) = self.sat_cache.get(&cache_key) {
             self.sat_cache_hits += 1;
@@ -476,14 +476,14 @@ impl SmtLibSubprocessSolver {
         if defer_hard_arith_without_witness
             && let Some((condition, base)) = constraints.split_last()
             && {
-                let normalized_base = normalize_constraints_for_solver(cx, base);
+                let normalized_base = normalize_sat_constraints(cx, base);
                 self.sat_cache.get(&normalized_base) == Some(&true)
             }
             && {
                 let mut complement = Vec::with_capacity(constraints.len());
                 complement.extend(base.iter().cloned());
                 complement.push(condition.clone().not(cx));
-                let normalized_complement = normalize_constraints_for_solver(cx, &complement);
+                let normalized_complement = normalize_sat_constraints(cx, &complement);
                 self.has_cached_unsat_subset(&normalized_complement)
             }
         {
@@ -711,6 +711,11 @@ impl SmtLibSubprocessSolver {
     }
 }
 
+/// Normalizes satisfiability constraints and removes soundly implied nonlinear comparisons.
+fn normalize_sat_constraints(cx: &mut SymCx, constraints: &[SymBoolExpr]) -> Vec<SymBoolExpr> {
+    remove_implied_monotonic_constraints(normalize_constraints_for_solver(cx, constraints))
+}
+
 /// Returns a hard-arithmetic fallback model only after validating it against original constraints.
 fn validated_hard_arith_fallback_model(
     cx: &SymCx,

crates/evm/symbolic/src/runtime/solver/monotonic_product.rs

@@ -1,8 +1,16 @@
-use super::*;
+use super::{opt::ConstraintContext, *};
 
 type LessThanFacts<'a> = HashSet<(&'a SymExpr, &'a SymExpr)>;
+type LessOrEqualFacts<'a> = HashSet<(&'a SymExpr, &'a SymExpr)>;
 type PositiveFacts<'a> = HashSet<&'a SymExpr>;
 
+#[derive(Default)]
+struct OrderFacts<'a> {
+    less_than: LessThanFacts<'a>,
+    less_or_equal: LessOrEqualFacts<'a>,
+    positive: PositiveFacts<'a>,
+}
+
 /// Returns whether monotonic product facts make these constraints unsatisfiable.
 #[cfg(test)]
 pub(crate) fn product_monotonic_unsat(cx: &mut SymCx, constraints: &[SymBoolExpr]) -> bool {
@@ -12,51 +20,217 @@ pub(crate) fn product_monotonic_unsat(cx: &mut SymCx, constraints: &[SymBoolExpr
 
 /// Returns whether normalized monotonic product facts make constraints unsatisfiable.
 pub(crate) fn product_monotonic_unsat_normalized(constraints: &[SymBoolExpr]) -> bool {
-    let mut less_than = HashSet::default();
-    let mut positive = HashSet::default();
-    for constraint in constraints {
-        collect_order_facts(constraint, &mut less_than, &mut positive);
-    }
+    let facts = order_facts(constraints.iter());
+    let bounds = ConstraintContext::new(constraints);
 
     constraints.iter().any(|constraint| {
-        product_less_than_negation(constraint).is_some_and(|(left_a, left_b, right_a, right_b)| {
-            product_less_than_known(left_a, left_b, right_a, right_b, &less_than, &positive)
-        })
+        reversed_strict_comparison(constraint)
+            .is_some_and(|(left, right)| expr_less_or_equal(right, left, &facts, &bounds))
+            || product_less_than_negation(constraint).is_some_and(
+                |(left_a, left_b, right_a, right_b)| {
+                    product_less_than_known(
+                        left_a,
+                        left_b,
+                        right_a,
+                        right_b,
+                        &facts.less_than,
+                        &facts.positive,
+                        &bounds,
+                    )
+                },
+            )
     })
 }
 
-fn collect_order_facts<'a>(
-    expr: &'a SymBoolExpr,
-    less_than: &mut LessThanFacts<'a>,
-    positive: &mut PositiveFacts<'a>,
-) {
+/// Removes hard-arithmetic comparisons implied by the remaining path constraints.
+///
+/// This keeps a sound monotonic success path from falling through to the heuristic witness
+/// search, whose satisfiable models are useful for counterexamples but cannot establish a proof.
+pub(super) fn remove_implied_monotonic_constraints(
+    mut constraints: Vec<SymBoolExpr>,
+) -> Vec<SymBoolExpr> {
+    // Remove constraints one at a time so two candidates cannot justify each other and then both
+    // disappear from the final query.
+    let mut index = 0;
+    while index < constraints.len() {
+        if !constraints[index].contains_hard_arith() {
+            index += 1;
+            continue;
+        }
+        let Some((left, right)) = less_or_equal_comparison(&constraints[index]) else {
+            index += 1;
+            continue;
+        };
+        let base = constraints
+            .iter()
+            .enumerate()
+            .filter(|(candidate, _)| *candidate != index)
+            .map(|(_, constraint)| constraint.clone())
+            .collect::<Vec<_>>();
+        let facts = order_facts(base.iter());
+        let bounds = ConstraintContext::new(&base);
+        if expr_less_or_equal(left, right, &facts, &bounds) {
+            constraints.remove(index);
+        } else {
+            index += 1;
+        }
+    }
+    constraints
+}
+
+fn order_facts<'a>(constraints: impl IntoIterator<Item = &'a SymBoolExpr>) -> OrderFacts<'a> {
+    let mut facts = OrderFacts::default();
+    for constraint in constraints {
+        collect_order_facts(constraint, &mut facts);
+    }
+    facts
+}
+
+fn collect_order_facts<'a>(expr: &'a SymBoolExpr, facts: &mut OrderFacts<'a>) {
     match expr.kind() {
         SymBoolExprKind::And(values) => {
             for value in values.iter() {
-                collect_order_facts(value, less_than, positive);
+                collect_order_facts(value, facts);
             }
         }
         SymBoolExprKind::Cmp(SymCmpOp::Ult, left, right) => {
-            less_than.insert((left, right));
+            facts.less_than.insert((left, right));
+            facts.less_or_equal.insert((left, right));
             if left.as_const().is_some_and(|value| value.is_zero()) {
-                positive.insert(right);
+                facts.positive.insert(right);
             }
         }
         SymBoolExprKind::Cmp(SymCmpOp::Ugt, left, right) => {
-            less_than.insert((right, left));
+            facts.less_than.insert((right, left));
+            facts.less_or_equal.insert((right, left));
             if right.as_const().is_some_and(|value| value.is_zero()) {
-                positive.insert(left);
+                facts.positive.insert(left);
             }
         }
+        SymBoolExprKind::Cmp(SymCmpOp::Ule, left, right) => {
+            facts.less_or_equal.insert((left, right));
+        }
+        SymBoolExprKind::Cmp(SymCmpOp::Uge, left, right) => {
+            facts.less_or_equal.insert((right, left));
+        }
+        SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right) => {
+            facts.less_or_equal.insert((left, right));
+            facts.less_or_equal.insert((right, left));
+        }
         SymBoolExprKind::Not(value) => {
             if let Some(expr) = nonzero_expr(value) {
-                positive.insert(expr);
+                facts.positive.insert(expr);
+            }
+            if let SymBoolExprKind::Cmp(op, left, right) = value.kind() {
+                match op {
+                    // !(a < b) => b <= a
+                    SymCmpOp::Ult => {
+                        facts.less_or_equal.insert((right, left));
+                    }
+                    // !(a > b) => a <= b
+                    SymCmpOp::Ugt => {
+                        facts.less_or_equal.insert((left, right));
+                    }
+                    // !(a <= b) => b < a
+                    SymCmpOp::Ule => {
+                        facts.less_than.insert((right, left));
+                        facts.less_or_equal.insert((right, left));
+                    }
+                    // !(a >= b) => a < b
+                    SymCmpOp::Uge => {
+                        facts.less_than.insert((left, right));
+                        facts.less_or_equal.insert((left, right));
+                    }
+                    SymCmpOp::Eq | SymCmpOp::Slt | SymCmpOp::Sgt => {}
+                }
             }
         }
-        SymBoolExprKind::Const(_) | SymBoolExprKind::Cmp(_, _, _) => {}
+        SymBoolExprKind::Const(_) | SymBoolExprKind::Cmp(SymCmpOp::Slt | SymCmpOp::Sgt, _, _) => {}
+    }
+}
+
+/// Returns a strict comparison that contradicts `right <= left`.
+fn reversed_strict_comparison(expr: &SymBoolExpr) -> Option<(&SymExpr, &SymExpr)> {
+    match expr.kind() {
+        SymBoolExprKind::Cmp(SymCmpOp::Ult, left, right) => Some((left, right)),
+        SymBoolExprKind::Cmp(SymCmpOp::Ugt, left, right) => Some((right, left)),
+        SymBoolExprKind::Not(value) => match value.kind() {
+            SymBoolExprKind::Cmp(SymCmpOp::Ule, left, right) => Some((right, left)),
+            SymBoolExprKind::Cmp(SymCmpOp::Uge, left, right) => Some((left, right)),
+            _ => None,
+        },
+        _ => None,
+    }
+}
+
+/// Returns the unsigned weak ordering asserted by this constraint.
+fn less_or_equal_comparison(expr: &SymBoolExpr) -> Option<(&SymExpr, &SymExpr)> {
+    match expr.kind() {
+        SymBoolExprKind::Cmp(SymCmpOp::Ule, left, right) => Some((left, right)),
+        SymBoolExprKind::Cmp(SymCmpOp::Uge, left, right) => Some((right, left)),
+        SymBoolExprKind::Not(value) => match value.kind() {
+            SymBoolExprKind::Cmp(SymCmpOp::Ult, left, right) => Some((right, left)),
+            SymBoolExprKind::Cmp(SymCmpOp::Ugt, left, right) => Some((left, right)),
+            _ => None,
+        },
+        _ => None,
+    }
+}
+
+/// Returns whether the known unsigned order and no-overflow bounds imply `left <= right`.
+fn expr_less_or_equal<'a>(
+    left: &'a SymExpr,
+    right: &'a SymExpr,
+    facts: &OrderFacts<'a>,
+    bounds: &ConstraintContext,
+) -> bool {
+    if left == right || facts.less_or_equal.contains(&(left, right)) {
+        return true;
+    }
+
+    match (left.kind(), right.kind()) {
+        (
+            SymExprKind::BinOp(SymBinOp::UDiv, left_num, left_den),
+            SymExprKind::BinOp(SymBinOp::UDiv, right_num, right_den),
+        ) if left_den == right_den => expr_less_or_equal(left_num, right_num, facts, bounds),
+        (
+            SymExprKind::BinOp(SymBinOp::Mul, left_a, left_b),
+            SymExprKind::BinOp(SymBinOp::Mul, right_a, right_b),
+        ) if bounds.mul_cannot_overflow_256(left_a, left_b)
+            && bounds.mul_cannot_overflow_256(right_a, right_b) =>
+        {
+            product_less_or_equal_known(left_a, left_b, right_a, right_b, facts, bounds)
+        }
+        _ => false,
     }
 }
 
+fn product_less_or_equal_known<'a>(
+    left_a: &'a SymExpr,
+    left_b: &'a SymExpr,
+    right_a: &'a SymExpr,
+    right_b: &'a SymExpr,
+    facts: &OrderFacts<'a>,
+    bounds: &ConstraintContext,
+) -> bool {
+    product_less_or_equal_known_ordered(left_a, left_b, right_a, right_b, facts, bounds)
+        || product_less_or_equal_known_ordered(left_b, left_a, right_a, right_b, facts, bounds)
+        || product_less_or_equal_known_ordered(left_a, left_b, right_b, right_a, facts, bounds)
+        || product_less_or_equal_known_ordered(left_b, left_a, right_b, right_a, facts, bounds)
+}
+
+fn product_less_or_equal_known_ordered<'a>(
+    left_a: &'a SymExpr,
+    left_b: &'a SymExpr,
+    right_a: &'a SymExpr,
+    right_b: &'a SymExpr,
+    facts: &OrderFacts<'a>,
+    bounds: &ConstraintContext,
+) -> bool {
+    expr_less_or_equal(left_a, right_a, facts, bounds)
+        && expr_less_or_equal(left_b, right_b, facts, bounds)
+}
+
 fn nonzero_expr(expr: &SymBoolExpr) -> Option<&SymExpr> {
     let SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right) = expr.kind() else { return None };
     if left.as_const().is_some_and(|value| value.is_zero()) {
@@ -87,11 +261,18 @@ fn product_less_than_known<'a>(
     right_b: &'a SymExpr,
     less_than: &LessThanFacts<'a>,
     positive: &PositiveFacts<'a>,
+    bounds: &ConstraintContext,
 ) -> bool {
-    product_less_than_known_ordered(left_a, left_b, right_a, right_b, less_than, positive)
-        || product_less_than_known_ordered(left_b, left_a, right_a, right_b, less_than, positive)
-        || product_less_than_known_ordered(left_a, left_b, right_b, right_a, less_than, positive)
-        || product_less_than_known_ordered(left_b, left_a, right_b, right_a, less_than, positive)
+    product_less_than_known_ordered(left_a, left_b, right_a, right_b, less_than, positive, bounds)
+        || product_less_than_known_ordered(
+            left_b, left_a, right_a, right_b, less_than, positive, bounds,
+        )
+        || product_less_than_known_ordered(
+            left_a, left_b, right_b, right_a, less_than, positive, bounds,
+        )
+        || product_less_than_known_ordered(
+            left_b, left_a, right_b, right_a, less_than, positive, bounds,
+        )
 }
 
 fn product_less_than_known_ordered<'a>(
@@ -101,13 +282,14 @@ fn product_less_than_known_ordered<'a>(
     right_b: &'a SymExpr,
     less_than: &LessThanFacts<'a>,
     positive: &PositiveFacts<'a>,
+    bounds: &ConstraintContext,
 ) -> bool {
     positive.contains(left_a)
         && positive.contains(left_b)
         && less_than.contains(&(left_a, right_a))
         && less_than.contains(&(left_b, right_b))
-        && left_a.mul_cannot_overflow_256(left_b)
-        && right_a.mul_cannot_overflow_256(right_b)
+        && bounds.mul_cannot_overflow_256(left_a, left_b)
+        && bounds.mul_cannot_overflow_256(right_a, right_b)
 }
 
 fn mul_operands(expr: &SymExpr) -> Option<(&SymExpr, &SymExpr)> {