foundry_evm_symbolic/runtime/solver/reasoning/
monotonic_product.rs

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

foundry_evm_symbolic/runtime/solver/reasoning/
monotonic_product.rs
