foundry_evm_symbolic/runtime/solver/normalize/
polynomial.rs

1//! Bounded sparse-polynomial identity reasoning over EVM words.
2
3use super::*;
4
5pub(super) fn polynomial_identity(left: &SymExpr, right: &SymExpr) -> bool {
6    if !polynomial_normalization_can_help(left) && !polynomial_normalization_can_help(right) {
7        return false;
8    }
9    matches!(
10        (Polynomial::from_expr(left), Polynomial::from_expr(right)),
11        (Some(left), Some(right)) if left == right
12    )
13}
14
15fn polynomial_normalization_can_help(expr: &SymExpr) -> bool {
16    let crosses_sum_product_boundary = match expr.kind() {
17        SymExprKind::BinOp(SymBinOp::Mul, left, right) => {
18            matches!(left.kind(), SymExprKind::BinOp(SymBinOp::Add | SymBinOp::Sub, ..))
19                || matches!(right.kind(), SymExprKind::BinOp(SymBinOp::Add | SymBinOp::Sub, ..))
20        }
21        SymExprKind::BinOp(SymBinOp::Add | SymBinOp::Sub, left, right) => {
22            matches!(left.kind(), SymExprKind::BinOp(SymBinOp::Mul, ..))
23                || matches!(right.kind(), SymExprKind::BinOp(SymBinOp::Mul, ..))
24                || matches!(
25                    left.kind(),
26                    SymExprKind::BinOp(SymBinOp::Shl, _, shift)
27                        if shift.as_const().is_some_and(|shift| shift < U256::from(256))
28                )
29                || matches!(
30                    right.kind(),
31                    SymExprKind::BinOp(SymBinOp::Shl, _, shift)
32                        if shift.as_const().is_some_and(|shift| shift < U256::from(256))
33                )
34        }
35        _ => false,
36    };
37    if !crosses_sum_product_boundary {
38        return false;
39    }
40
41    fn ring_shape(
42        expr: &SymExpr,
43        shapes: &mut HashMap<SymExpr, Option<(usize, usize)>>,
44        remaining: &mut usize,
45    ) -> Option<(usize, usize)> {
46        if let Some(shape) = shapes.get(expr) {
47            return *shape;
48        }
49        if *remaining == 0 {
50            return None;
51        }
52        *remaining -= 1;
53        let shape = (|| match expr.kind() {
54            SymExprKind::Const(_) | SymExprKind::Var(_) => Some((0, 0)),
55            SymExprKind::BinOp(
56                op @ (SymBinOp::Add | SymBinOp::Sub | SymBinOp::Mul),
57                left,
58                right,
59            ) => {
60                let left = ring_shape(left, shapes, remaining)?;
61                let right = ring_shape(right, shapes, remaining)?;
62                let operations = left.0.saturating_add(right.0).saturating_add(1);
63                let multiplications = left
64                    .1
65                    .saturating_add(right.1)
66                    .saturating_add(usize::from(*op == SymBinOp::Mul));
67                Some((operations, multiplications))
68            }
69            SymExprKind::BinOp(SymBinOp::Shl, value, shift)
70                if shift.as_const().is_some_and(|shift| shift < U256::from(256)) =>
71            {
72                let shape = ring_shape(value, shapes, remaining)?;
73                Some((shape.0.saturating_add(1), shape.1.saturating_add(1)))
74            }
75            _ => None,
76        })();
77        shapes.insert(expr.clone(), shape);
78        shape
79    }
80
81    let mut shapes = HashMap::default();
82    let mut remaining = MAX_LOCAL_ANALYSIS_NODES;
83    ring_shape(expr, &mut shapes, &mut remaining)
84        .is_some_and(|(operations, multiplications)| operations > 1 && multiplications > 0)
85}
86
87// Keep distributive expansion predictably bounded. The motivating accounting identity needs two
88// terms with two factors; these limits leave ample room for ordinary identities without allowing
89// adversarial expressions to explode.
90const MAX_POLYNOMIAL_TERMS: usize = 32;
91const MAX_MONOMIAL_FACTORS: usize = 8;
92const MAX_POLYNOMIAL_PRODUCTS: usize = 256;
93
94type Monomial = Vec<SymExpr>;
95
96/// A sparse polynomial over the EVM word ring Z/(2^256).
97///
98/// Addition, subtraction, and multiplication of EVM words obey the ring laws even when they
99/// wrap. Canonicalizing small expressions here lets the solver recognize nonlinear algebraic
100/// identities without replacing bit-vector semantics with unbounded integer arithmetic.
101#[derive(Clone, PartialEq, Eq)]
102struct Polynomial {
103    terms: HashMap<Monomial, U256>,
104}
105
106impl Polynomial {
107    fn from_expr(expr: &SymExpr) -> Option<Self> {
108        let mut remaining = MAX_LOCAL_ANALYSIS_NODES;
109        Self::from_expr_cached(expr, &mut HashMap::default(), &mut remaining)
110    }
111
112    fn from_expr_cached(
113        expr: &SymExpr,
114        polynomials: &mut HashMap<SymExpr, Option<Self>>,
115        remaining: &mut usize,
116    ) -> Option<Self> {
117        if let Some(polynomial) = polynomials.get(expr) {
118            return polynomial.clone();
119        }
120        if *remaining == 0 {
121            polynomials.insert(expr.clone(), None);
122            return None;
123        }
124        *remaining -= 1;
125        let polynomial =
126            (|| match expr.kind() {
127                SymExprKind::Const(value) => Some(Self::constant(*value)),
128                SymExprKind::BinOp(SymBinOp::Add, left, right) => {
129                    Self::from_expr_cached(left, polynomials, remaining)?
130                        .add(Self::from_expr_cached(right, polynomials, remaining)?)
131                }
132                SymExprKind::BinOp(SymBinOp::Sub, left, right) => {
133                    Self::from_expr_cached(left, polynomials, remaining)?
134                        .sub(Self::from_expr_cached(right, polynomials, remaining)?)
135                }
136                SymExprKind::BinOp(SymBinOp::Mul, left, right) => {
137                    Self::from_expr_cached(left, polynomials, remaining)?
138                        .mul(Self::from_expr_cached(right, polynomials, remaining)?)
139                }
140                SymExprKind::BinOp(SymBinOp::Shl, value, shift)
141                    if let Some(shift) = shift.as_const()
142                        && shift < U256::from(256) =>
143                {
144                    let coefficient = U256::ONE << usize::try_from(shift).ok()?;
145                    Self::from_expr_cached(value, polynomials, remaining)?
146                        .mul(Self::constant(coefficient))
147                }
148                _ => {
149                    let terms = HashMap::from_iter([(vec![expr.clone()], U256::ONE)]);
150                    Some(Self { terms })
151                }
152            })();
153        polynomials.insert(expr.clone(), polynomial.clone());
154        polynomial
155    }
156
157    fn constant(value: U256) -> Self {
158        let mut terms = HashMap::default();
159        if !value.is_zero() {
160            terms.insert(Vec::new(), value);
161        }
162        Self { terms }
163    }
164
165    fn add(mut self, right: Self) -> Option<Self> {
166        for (monomial, coefficient) in right.terms {
167            self.add_term(monomial, coefficient);
168            if self.terms.len() > MAX_POLYNOMIAL_TERMS {
169                return None;
170            }
171        }
172        Some(self)
173    }
174
175    fn sub(mut self, right: Self) -> Option<Self> {
176        for (monomial, coefficient) in right.terms {
177            self.add_term(monomial, U256::ZERO.wrapping_sub(coefficient));
178            if self.terms.len() > MAX_POLYNOMIAL_TERMS {
179                return None;
180            }
181        }
182        Some(self)
183    }
184
185    fn mul(self, right: Self) -> Option<Self> {
186        let products = self.terms.len().checked_mul(right.terms.len())?;
187        if products > MAX_POLYNOMIAL_PRODUCTS {
188            return None;
189        }
190
191        let mut out = Self { terms: HashMap::default() };
192        for (left_monomial, left_coefficient) in &self.terms {
193            for (right_monomial, right_coefficient) in &right.terms {
194                let factor_count = left_monomial.len().checked_add(right_monomial.len())?;
195                if factor_count > MAX_MONOMIAL_FACTORS {
196                    return None;
197                }
198                let mut monomial = Vec::with_capacity(factor_count);
199                monomial.extend(left_monomial.iter().cloned());
200                monomial.extend(right_monomial.iter().cloned());
201                SymExpr::sort_interned_factors(&mut monomial);
202                out.add_term(monomial, left_coefficient.wrapping_mul(*right_coefficient));
203                if out.terms.len() > MAX_POLYNOMIAL_TERMS {
204                    return None;
205                }
206            }
207        }
208        Some(out)
209    }
210
211    fn add_term(&mut self, monomial: Monomial, coefficient: U256) {
212        if coefficient.is_zero() {
213            return;
214        }
215        let coefficient =
216            self.terms.get(&monomial).copied().unwrap_or_default().wrapping_add(coefficient);
217        if coefficient.is_zero() {
218            self.terms.remove(&monomial);
219        } else {
220            self.terms.insert(monomial, coefficient);
221        }
222    }
223}
foundry_evm_symbolic/runtime/solver/normalize/polynomial.rs

foundry_evm_symbolic/runtime/solver/normalize/
polynomial.rs
