foundry_evm_symbolic/runtime/solver/
monotonic_product.rs

1use super::{normalize::mul_cannot_overflow_256, *};
2
3/// Returns whether monotonic product facts make these constraints unsatisfiable.
4#[cfg(test)]
5pub(crate) fn product_monotonic_unsat(constraints: &[BoolExpr]) -> bool {
6    let constraints = normalize_constraints_for_solver(constraints);
7    product_monotonic_unsat_normalized(&constraints)
8}
9
10/// Returns whether normalized monotonic product facts make constraints unsatisfiable.
11pub(crate) fn product_monotonic_unsat_normalized(constraints: &[BoolExpr]) -> bool {
12    let mut less_than = BTreeSet::new();
13    let mut positive = BTreeSet::new();
14    for constraint in constraints {
15        collect_order_facts(constraint, &mut less_than, &mut positive);
16    }
17
18    constraints.iter().any(|constraint| {
19        product_less_than_negation(constraint).is_some_and(|(left_a, left_b, right_a, right_b)| {
20            product_less_than_known(left_a, left_b, right_a, right_b, &less_than, &positive)
21        })
22    })
23}
24
25/// Collects simple unsigned ordering facts from normalized constraints.
26pub(crate) fn collect_order_facts(
27    expr: &BoolExpr,
28    less_than: &mut BTreeSet<(Expr, Expr)>,
29    positive: &mut BTreeSet<Expr>,
30) {
31    match expr {
32        BoolExpr::And(values) => {
33            for value in values {
34                collect_order_facts(value, less_than, positive);
35            }
36        }
37        BoolExpr::Cmp(BoolExprOp::Ult, left, right) => {
38            less_than.insert((left.clone(), right.clone()));
39            if matches!(left, Expr::Const(value) if value.is_zero()) {
40                positive.insert(right.clone());
41            }
42        }
43        BoolExpr::Cmp(BoolExprOp::Ugt, left, right) => {
44            less_than.insert((right.clone(), left.clone()));
45            if matches!(right, Expr::Const(value) if value.is_zero()) {
46                positive.insert(left.clone());
47            }
48        }
49        BoolExpr::Const(_) | BoolExpr::Not(_) | BoolExpr::Eq(_, _) | BoolExpr::Cmp(_, _, _) => {}
50    }
51}
52
53/// Extracts `!(a * b < c * d)` as product operands.
54pub(crate) fn product_less_than_negation(expr: &BoolExpr) -> Option<(&Expr, &Expr, &Expr, &Expr)> {
55    let BoolExpr::Not(value) = expr else { return None };
56    let BoolExpr::Cmp(BoolExprOp::Ult, left, right) = value.as_ref() else { return None };
57    let (left_a, left_b) = mul_operands(left)?;
58    let (right_a, right_b) = mul_operands(right)?;
59    Some((left_a, left_b, right_a, right_b))
60}
61
62/// Returns whether known facts imply `left_a * left_b < right_a * right_b`.
63pub(crate) fn product_less_than_known(
64    left_a: &Expr,
65    left_b: &Expr,
66    right_a: &Expr,
67    right_b: &Expr,
68    less_than: &BTreeSet<(Expr, Expr)>,
69    positive: &BTreeSet<Expr>,
70) -> bool {
71    product_less_than_known_ordered(left_a, left_b, right_a, right_b, less_than, positive)
72        || product_less_than_known_ordered(left_b, left_a, right_a, right_b, less_than, positive)
73        || product_less_than_known_ordered(left_a, left_b, right_b, right_a, less_than, positive)
74        || product_less_than_known_ordered(left_b, left_a, right_b, right_a, less_than, positive)
75}
76
77/// Checks the ordered monotonicity case `0 < a < c && 0 < b < d`.
78pub(crate) fn product_less_than_known_ordered(
79    left_a: &Expr,
80    left_b: &Expr,
81    right_a: &Expr,
82    right_b: &Expr,
83    less_than: &BTreeSet<(Expr, Expr)>,
84    positive: &BTreeSet<Expr>,
85) -> bool {
86    positive.contains(left_a)
87        && positive.contains(left_b)
88        && less_than.contains(&(left_a.clone(), right_a.clone()))
89        && less_than.contains(&(left_b.clone(), right_b.clone()))
90        && mul_cannot_overflow_256(left_a, left_b)
91        && mul_cannot_overflow_256(right_a, right_b)
92}
93
94/// Returns the operands for an unsigned multiplication expression.
95pub(crate) fn mul_operands(expr: &Expr) -> Option<(&Expr, &Expr)> {
96    match expr {
97        Expr::Op(ExprOp::Mul, left, right) => Some((left, right)),
98        _ => None,
99    }
100}
foundry_evm_symbolic/runtime/solver/monotonic_product.rs

foundry_evm_symbolic/runtime/solver/
monotonic_product.rs
