foundry_evm_symbolic/runtime/solver/reasoning/
xor.rs

1//! A checked specialist for affine systems of EVM word XOR equalities.
2//!
3//! Gaussian elimination proposes either a model or a set of source equations whose XOR is
4//! contradictory. Neither answer is trusted: models are evaluated against the entire original
5//! query, and the certificate checker cancels terms in the original source equations without
6//! consulting the elimination rows. Unsupported queries and exhausted work budgets fall through.
7
8use super::*;
9
10// A word-sized bitset tracks both columns and source equations. Bound expression unfolding too:
11// a small hash-consed DAG can represent an exponentially large unfolded XOR tree.
12const MAX_XOR_ROWS: usize = 256;
13const MAX_XOR_ATOMS: usize = 256;
14const MAX_XOR_VISITS: usize = 8192;
15
16pub(in super::super) enum CheckedXorResult {
17    Unsat,
18    Model(SymbolicModel),
19}
20
21#[derive(Clone, Copy)]
22struct Row {
23    columns: U256,
24    value: U256,
25    sources: U256,
26}
27
28struct Relation<'a> {
29    left: &'a SymExpr,
30    right: &'a SymExpr,
31    negated: bool,
32}
33
34/// Returns only independently checked answers, using the original, unnormalized constraints.
35pub(in super::super) fn checked_xor_result(
36    constraints: &[SymBoolExpr],
37) -> Option<CheckedXorResult> {
38    let relations = asserted_relations(constraints)?;
39    // Most EVM queries are not XOR workloads. Do not run elimination for ordinary equalities.
40    if !relations
41        .iter()
42        .any(|relation| affine_terms(relation).0.into_iter().flatten().any(is_affine_op))
43    {
44        return None;
45    }
46
47    let mut atoms = HashMap::<&SymExpr, usize>::default();
48    let mut basis = [None::<Row>; MAX_XOR_ATOMS];
49    let mut visits = MAX_XOR_VISITS;
50    let mut rows = Vec::with_capacity(relations.len());
51    for (index, relation) in relations.iter().enumerate() {
52        let (terms, constant) = affine_terms(relation);
53        let mut row = Row { columns: U256::ZERO, value: constant, sources: U256::ONE << index };
54        let mut pending = terms.into_iter().flatten().collect::<Vec<_>>();
55        while let Some(expr) = pending.pop() {
56            visits = visits.checked_sub(1)?;
57            match expr.kind() {
58                SymExprKind::Const(value) => row.value ^= *value,
59                SymExprKind::BinOp(SymBinOp::Xor, left, right) => {
60                    pending.extend([left, right]);
61                }
62                SymExprKind::Not(value) => {
63                    row.value ^= U256::MAX;
64                    pending.push(value);
65                }
66                _ => {
67                    let next = atoms.len();
68                    let column = *atoms.entry(expr).or_insert(next);
69                    if column >= MAX_XOR_ATOMS {
70                        return None;
71                    }
72                    row.columns ^= U256::ONE << column;
73                }
74            }
75        }
76        rows.push(row);
77    }
78    for (relation, mut row) in relations.iter().zip(rows.iter().copied()) {
79        if relation.negated {
80            continue;
81        }
82        while !row.columns.is_zero() {
83            let pivot = row.columns.trailing_zeros();
84            if let Some(previous) = basis[pivot] {
85                row.columns ^= previous.columns;
86                row.value ^= previous.value;
87                row.sources ^= previous.sources;
88            } else {
89                basis[pivot] = Some(row);
90                break;
91            }
92        }
93        if row.columns.is_zero() && !row.value.is_zero() {
94            return check_certificate(&relations, row.sources, None)
95                .then_some(CheckedXorResult::Unsat);
96        }
97    }
98    // A disequality is impossible when its equality follows from the asserted equalities.
99    // Disequalities never become basis rows: combining them as equations would be unsound.
100    for (index, (relation, mut row)) in relations.iter().zip(rows).enumerate() {
101        if !relation.negated {
102            continue;
103        }
104        row.sources = U256::ZERO;
105        while !row.columns.is_zero() {
106            let pivot = row.columns.trailing_zeros();
107            let Some(previous) = basis[pivot] else { break };
108            row.columns ^= previous.columns;
109            row.value ^= previous.value;
110            row.sources ^= previous.sources;
111        }
112        if row.columns.is_zero() && row.value.is_zero() {
113            return check_certificate(&relations, row.sources, Some(index))
114                .then_some(CheckedXorResult::Unsat);
115        }
116    }
117
118    // Free columns are zero. Back-substitution assigns pivot columns; opaque expressions are
119    // never independently assignable, so only variable columns enter the candidate model.
120    if constraints.iter().any(SymBoolExpr::contains_gasleft) {
121        return None;
122    }
123    let mut values = [U256::ZERO; MAX_XOR_ATOMS];
124    for (pivot, row) in basis.iter().enumerate().rev() {
125        if let Some(row) = row {
126            let mut value = row.value;
127            for (column, assigned) in values.iter().enumerate().skip(pivot + 1) {
128                if row.columns.bit(column) {
129                    value ^= *assigned;
130                }
131            }
132            values[pivot] = value;
133        }
134    }
135    let model = atoms
136        .into_iter()
137        .filter_map(|(expr, column)| match expr.kind() {
138            SymExprKind::Var(symbol) => Some((*symbol, values[column])),
139            _ => None,
140        })
141        .collect();
142    eval_model_constraints(constraints, &model).then_some(CheckedXorResult::Model(model))
143}
144
145/// Collects asserted equalities and disequalities. Negated conjunctions cannot supply relations.
146fn asserted_relations(constraints: &[SymBoolExpr]) -> Option<Vec<Relation<'_>>> {
147    if constraints.len() > MAX_XOR_VISITS {
148        return None;
149    }
150    let mut relations = Vec::new();
151    let mut pending = constraints.iter().collect::<Vec<_>>();
152    let mut visits = MAX_XOR_VISITS;
153    while let Some(constraint) = pending.pop() {
154        visits = visits.checked_sub(1)?;
155        if let SymBoolExprKind::And(values) = constraint.kind() {
156            if pending.len() + values.len() > visits {
157                return None;
158            }
159            pending.extend(values.iter());
160            continue;
161        }
162        let (value, negated) = match constraint.kind() {
163            SymBoolExprKind::Not(value) => (value, true),
164            _ => (constraint, false),
165        };
166        if let SymBoolExprKind::Cmp(SymCmpOp::Eq, left, right) = value.kind() {
167            if relations.len() == MAX_XOR_ROWS {
168                return None;
169            }
170            relations.push(Relation { left, right, negated });
171        }
172    }
173    Some(relations)
174}
175
176fn is_affine_op(expr: &SymExpr) -> bool {
177    matches!(expr.kind(), SymExprKind::BinOp(SymBinOp::Xor, _, _) | SymExprKind::Not(_))
178}
179
180/// Recovers equalities compiled as `ISZERO(ADD(word, constant))` or `ISZERO(SUB(a, b))`.
181/// Only the equality boundary admits these rewrites: addition inside an XOR remains opaque
182/// because carries are not linear over GF(2). Every constant operation wraps at EVM word width.
183fn affine_terms<'a>(relation: &Relation<'a>) -> ([Option<&'a SymExpr>; 2], U256) {
184    let Some(mut target) = relation.right.as_const() else {
185        return ([Some(relation.left), Some(relation.right)], U256::ZERO);
186    };
187    let mut word = relation.left;
188    for _ in 0..32 {
189        match word.kind() {
190            SymExprKind::BinOp(SymBinOp::Add, left, right)
191                if let Some(value) = right.as_const() =>
192            {
193                target = target.wrapping_sub(value);
194                word = left;
195            }
196            SymExprKind::BinOp(SymBinOp::Sub, left, right) => {
197                if let Some(value) = right.as_const() {
198                    target = target.wrapping_add(value);
199                    word = left;
200                } else if let Some(value) = left.as_const() {
201                    target = value.wrapping_sub(target);
202                    word = right;
203                } else if target.is_zero() {
204                    return ([Some(left), Some(right)], U256::ZERO);
205                } else {
206                    break;
207                }
208            }
209            _ => break,
210        }
211    }
212    ([Some(word), None], target)
213}
214
215/// Checks a contradiction certificate by XORing selected source equalities directly. All opaque
216/// terms must cancel, leaving `0 = nonzero`, or `0 != 0` for a disequality certificate. This is a
217/// necessary contradiction even when atoms are related (e.g. `x` and `x & mask`); no independence
218/// assumption is used to establish UNSAT.
219fn check_certificate(
220    relations: &[Relation<'_>],
221    sources: U256,
222    disequality: Option<usize>,
223) -> bool {
224    if relations.len() < MAX_XOR_ROWS && !(sources >> relations.len()).is_zero() {
225        return false;
226    }
227    if disequality
228        .is_some_and(|index| !relations.get(index).is_some_and(|relation| relation.negated))
229    {
230        return false;
231    }
232    let mut terms = HashSet::<&SymExpr>::default();
233    let mut constant = U256::ZERO;
234    let mut visits = MAX_XOR_VISITS;
235    for (index, relation) in relations.iter().enumerate() {
236        if sources.bit(index) && relation.negated {
237            return false;
238        }
239        if !sources.bit(index) && disequality != Some(index) {
240            continue;
241        }
242        let (words, offset) = affine_terms(relation);
243        constant ^= offset;
244        let mut pending = words.into_iter().flatten().collect::<Vec<_>>();
245        while let Some(expr) = pending.pop() {
246            let Some(remaining) = visits.checked_sub(1) else { return false };
247            visits = remaining;
248            match expr.kind() {
249                SymExprKind::Const(value) => constant ^= *value,
250                SymExprKind::BinOp(SymBinOp::Xor, left, right) => {
251                    pending.extend([left, right]);
252                }
253                SymExprKind::Not(value) => {
254                    constant ^= U256::MAX;
255                    pending.push(value);
256                }
257                _ => {
258                    if !terms.remove(expr) {
259                        terms.insert(expr);
260                    }
261                }
262            }
263        }
264    }
265    terms.is_empty() && constant.is_zero() == disequality.is_some()
266}
foundry_evm_symbolic/runtime/solver/reasoning/xor.rs

foundry_evm_symbolic/runtime/solver/reasoning/
xor.rs
