foundry_evm_symbolic/runtime/solver/
monotonic_product.rs

1use super::{opt::ConstraintContext, *};
2
3type LessThanFacts<'a> = HashSet<(&'a SymExpr, &'a SymExpr)>;
4type LessOrEqualFacts<'a> = HashSet<(&'a SymExpr, &'a SymExpr)>;
5type PositiveFacts<'a> = HashSet<&'a SymExpr>;
6
7#[derive(Default)]
8struct OrderFacts<'a> {
9    less_than: LessThanFacts<'a>,
10    less_or_equal: LessOrEqualFacts<'a>,
11    positive: PositiveFacts<'a>,
12}
13
14/// Returns whether monotonic product facts make these constraints unsatisfiable.
15#[cfg(test)]
16pub(crate) fn product_monotonic_unsat(cx: &mut SymCx, constraints: &[SymBoolExpr]) -> bool {
17    let constraints = normalize_constraints_for_solver(cx, constraints);
18    product_monotonic_unsat_normalized(&constraints)
19}
20
21/// Returns whether normalized monotonic product facts make constraints unsatisfiable.
22pub(crate) fn product_monotonic_unsat_normalized(constraints: &[SymBoolExpr]) -> bool {
23    let facts = order_facts(constraints.iter());
24    let bounds = ConstraintContext::new(constraints);
25
26    constraints.iter().any(|constraint| {
27        reversed_strict_comparison(constraint)
28            .is_some_and(|(left, right)| expr_less_or_equal(right, left, &facts, &bounds))
29            || product_less_than_negation(constraint).is_some_and(
30                |(left_a, left_b, right_a, right_b)| {
31                    product_less_than_known(
32                        left_a,
33                        left_b,
34                        right_a,
35                        right_b,
36                        &facts.less_than,
37                        &facts.positive,
38                        &bounds,
39                    )
40                },
41            )
42    })
43}
44
45/// Removes hard-arithmetic comparisons implied by the remaining path constraints.
46///
47/// This keeps a sound monotonic success path from falling through to the heuristic witness
48/// search, whose satisfiable models are useful for counterexamples but cannot establish a proof.
49pub(super) fn remove_implied_monotonic_constraints(
50    mut constraints: Vec<SymBoolExpr>,
51) -> Vec<SymBoolExpr> {
52    // Remove constraints one at a time so two candidates cannot justify each other and then both
53    // disappear from the final query.
54    let mut index = 0;
55    while index < constraints.len() {
56        if !constraints[index].contains_hard_arith() {
57            index += 1;
58            continue;
59        }
60        let Some((left, right)) = less_or_equal_comparison(&constraints[index]) else {
61            index += 1;
62            continue;
63        };
64        let base = constraints
65            .iter()
66            .enumerate()
67            .filter(|(candidate, _)| *candidate != index)
68            .map(|(_, constraint)| constraint.clone())
69            .collect::<Vec<_>>();
70        let facts = order_facts(base.iter());
71        let bounds = ConstraintContext::new(&base);
72        if expr_less_or_equal(left, right, &facts, &bounds) {
73            constraints.remove(index);
74        } else {
75            index += 1;
76        }
77    }
78    constraints
79}
80
81fn order_facts<'a>(constraints: impl IntoIterator<Item = &'a SymBoolExpr>) -> OrderFacts<'a> {
82    let mut facts = OrderFacts::default();
83    for constraint in constraints {
84        collect_order_facts(constraint, &mut facts);
85    }
86    facts
87}
88
89fn collect_order_facts<'a>(expr: &'a SymBoolExpr, facts: &mut OrderFacts<'a>) {
90    match expr.kind() {
91        SymBoolExprKind::And(values) => {
92            for value in values.iter() {
93                collect_order_facts(value, facts);
94            }
95        }
96        SymBoolExprKind::Cmp(SymCmpOp::Ult, left, right) => {
97            facts.less_than.insert((left, right));
98            facts.less_or_equal.insert((left, right));
99            if left.as_const().is_some_and(|value| value.is_zero()) {
100                facts.positive.insert(right);
101            }
102        }
103        SymBoolExprKind::Cmp(SymCmpOp::Ugt, left, right) => {
104            facts.less_than.insert((right, left));
105            facts.less_or_equal.insert((right, left));
106            if right.as_const().is_some_and(|value| value.is_zero()) {
107                facts.positive.insert(left);
108            }
109        }
110        SymBoolExprKind::Cmp(SymCmpOp::Ule, left, right) => {
111            facts.less_or_equal.insert((left, right));
112        }
113        SymBoolExprKind::Cmp(SymCmpOp::Uge, left, right) => {
114            facts.less_or_equal.insert((right, left));
115        }
116        SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right) => {
117            facts.less_or_equal.insert((left, right));
118            facts.less_or_equal.insert((right, left));
119        }
120        SymBoolExprKind::Not(value) => {
121            if let Some(expr) = nonzero_expr(value) {
122                facts.positive.insert(expr);
123            }
124            if let SymBoolExprKind::Cmp(op, left, right) = value.kind() {
125                match op {
126                    // !(a < b) => b <= a
127                    SymCmpOp::Ult => {
128                        facts.less_or_equal.insert((right, left));
129                    }
130                    // !(a > b) => a <= b
131                    SymCmpOp::Ugt => {
132                        facts.less_or_equal.insert((left, right));
133                    }
134                    // !(a <= b) => b < a
135                    SymCmpOp::Ule => {
136                        facts.less_than.insert((right, left));
137                        facts.less_or_equal.insert((right, left));
138                    }
139                    // !(a >= b) => a < b
140                    SymCmpOp::Uge => {
141                        facts.less_than.insert((left, right));
142                        facts.less_or_equal.insert((left, right));
143                    }
144                    SymCmpOp::Eq | SymCmpOp::Slt | SymCmpOp::Sgt => {}
145                }
146            }
147        }
148        SymBoolExprKind::Const(_) | SymBoolExprKind::Cmp(SymCmpOp::Slt | SymCmpOp::Sgt, _, _) => {}
149    }
150}
151
152/// Returns a strict comparison that contradicts `right <= left`.
153fn reversed_strict_comparison(expr: &SymBoolExpr) -> Option<(&SymExpr, &SymExpr)> {
154    match expr.kind() {
155        SymBoolExprKind::Cmp(SymCmpOp::Ult, left, right) => Some((left, right)),
156        SymBoolExprKind::Cmp(SymCmpOp::Ugt, left, right) => Some((right, left)),
157        SymBoolExprKind::Not(value) => match value.kind() {
158            SymBoolExprKind::Cmp(SymCmpOp::Ule, left, right) => Some((right, left)),
159            SymBoolExprKind::Cmp(SymCmpOp::Uge, left, right) => Some((left, right)),
160            _ => None,
161        },
162        _ => None,
163    }
164}
165
166/// Returns the unsigned weak ordering asserted by this constraint.
167fn less_or_equal_comparison(expr: &SymBoolExpr) -> Option<(&SymExpr, &SymExpr)> {
168    match expr.kind() {
169        SymBoolExprKind::Cmp(SymCmpOp::Ule, left, right) => Some((left, right)),
170        SymBoolExprKind::Cmp(SymCmpOp::Uge, left, right) => Some((right, left)),
171        SymBoolExprKind::Not(value) => match value.kind() {
172            SymBoolExprKind::Cmp(SymCmpOp::Ult, left, right) => Some((right, left)),
173            SymBoolExprKind::Cmp(SymCmpOp::Ugt, left, right) => Some((left, right)),
174            _ => None,
175        },
176        _ => None,
177    }
178}
179
180/// Returns whether the known unsigned order and no-overflow bounds imply `left <= right`.
181fn expr_less_or_equal<'a>(
182    left: &'a SymExpr,
183    right: &'a SymExpr,
184    facts: &OrderFacts<'a>,
185    bounds: &ConstraintContext,
186) -> bool {
187    if left == right || facts.less_or_equal.contains(&(left, right)) {
188        return true;
189    }
190
191    match (left.kind(), right.kind()) {
192        (
193            SymExprKind::BinOp(SymBinOp::UDiv, left_num, left_den),
194            SymExprKind::BinOp(SymBinOp::UDiv, right_num, right_den),
195        ) if left_den == right_den => expr_less_or_equal(left_num, right_num, facts, bounds),
196        (
197            SymExprKind::BinOp(SymBinOp::Mul, left_a, left_b),
198            SymExprKind::BinOp(SymBinOp::Mul, right_a, right_b),
199        ) if bounds.mul_cannot_overflow_256(left_a, left_b)
200            && bounds.mul_cannot_overflow_256(right_a, right_b) =>
201        {
202            product_less_or_equal_known(left_a, left_b, right_a, right_b, facts, bounds)
203        }
204        _ => false,
205    }
206}
207
208fn product_less_or_equal_known<'a>(
209    left_a: &'a SymExpr,
210    left_b: &'a SymExpr,
211    right_a: &'a SymExpr,
212    right_b: &'a SymExpr,
213    facts: &OrderFacts<'a>,
214    bounds: &ConstraintContext,
215) -> bool {
216    product_less_or_equal_known_ordered(left_a, left_b, right_a, right_b, facts, bounds)
217        || product_less_or_equal_known_ordered(left_b, left_a, right_a, right_b, facts, bounds)
218        || product_less_or_equal_known_ordered(left_a, left_b, right_b, right_a, facts, bounds)
219        || product_less_or_equal_known_ordered(left_b, left_a, right_b, right_a, facts, bounds)
220}
221
222fn product_less_or_equal_known_ordered<'a>(
223    left_a: &'a SymExpr,
224    left_b: &'a SymExpr,
225    right_a: &'a SymExpr,
226    right_b: &'a SymExpr,
227    facts: &OrderFacts<'a>,
228    bounds: &ConstraintContext,
229) -> bool {
230    expr_less_or_equal(left_a, right_a, facts, bounds)
231        && expr_less_or_equal(left_b, right_b, facts, bounds)
232}
233
234fn nonzero_expr(expr: &SymBoolExpr) -> Option<&SymExpr> {
235    let SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right) = expr.kind() else { return None };
236    if left.as_const().is_some_and(|value| value.is_zero()) {
237        Some(right)
238    } else if right.as_const().is_some_and(|value| value.is_zero()) {
239        Some(left)
240    } else {
241        None
242    }
243}
244
245fn product_less_than_negation(
246    expr: &SymBoolExpr,
247) -> Option<(&SymExpr, &SymExpr, &SymExpr, &SymExpr)> {
248    let SymBoolExprKind::Not(value) = expr.kind() else { return None };
249    let SymBoolExprKind::Cmp(SymCmpOp::Ult, left, right) = value.kind() else {
250        return None;
251    };
252    let (left_a, left_b) = mul_operands(left)?;
253    let (right_a, right_b) = mul_operands(right)?;
254    Some((left_a, left_b, right_a, right_b))
255}
256
257fn product_less_than_known<'a>(
258    left_a: &'a SymExpr,
259    left_b: &'a SymExpr,
260    right_a: &'a SymExpr,
261    right_b: &'a SymExpr,
262    less_than: &LessThanFacts<'a>,
263    positive: &PositiveFacts<'a>,
264    bounds: &ConstraintContext,
265) -> bool {
266    product_less_than_known_ordered(left_a, left_b, right_a, right_b, less_than, positive, bounds)
267        || product_less_than_known_ordered(
268            left_b, left_a, right_a, right_b, less_than, positive, bounds,
269        )
270        || product_less_than_known_ordered(
271            left_a, left_b, right_b, right_a, less_than, positive, bounds,
272        )
273        || product_less_than_known_ordered(
274            left_b, left_a, right_b, right_a, less_than, positive, bounds,
275        )
276}
277
278fn product_less_than_known_ordered<'a>(
279    left_a: &'a SymExpr,
280    left_b: &'a SymExpr,
281    right_a: &'a SymExpr,
282    right_b: &'a SymExpr,
283    less_than: &LessThanFacts<'a>,
284    positive: &PositiveFacts<'a>,
285    bounds: &ConstraintContext,
286) -> bool {
287    positive.contains(left_a)
288        && positive.contains(left_b)
289        && less_than.contains(&(left_a, right_a))
290        && less_than.contains(&(left_b, right_b))
291        && bounds.mul_cannot_overflow_256(left_a, left_b)
292        && bounds.mul_cannot_overflow_256(right_a, right_b)
293}
294
295fn mul_operands(expr: &SymExpr) -> Option<(&SymExpr, &SymExpr)> {
296    match expr.kind() {
297        SymExprKind::BinOp(SymBinOp::Mul, left, right) => Some((left, right)),
298        _ => None,
299    }
300}
foundry_evm_symbolic/runtime/solver/monotonic_product.rs

foundry_evm_symbolic/runtime/solver/
monotonic_product.rs
