foundry_evm_symbolic/runtime/solver/normalize/
rounding.rs

1//! Rounding relations between a rounded multiple and its original dividend.
2//!
3//! These bounds describe mathematical differences, not wrapping EVM subtractions.
4//! They are consumed only where the sign or a non-wrapping product is established.
5
6use super::{
7    ConstraintContext, HashMap, MAX_LOCAL_ANALYSIS_NODES, SymBinOp, SymBoolExpr, SymBoolExprKind,
8    SymCmpOp, SymExpr, SymExprKind, U256, WordInterval,
9};
10
11/// `anchor - below <= rounded <= anchor + above` over mathematical integers.
12struct RoundingBounds<'a> {
13    anchor: &'a SymExpr,
14    below: U256,
15    above: U256,
16}
17
18impl ConstraintContext {
19    /// Matches `(dividend / d) * d` for a positive constant `d`.
20    pub(super) fn rounded_product_operands(expr: &SymExpr) -> Option<(&SymExpr, U256)> {
21        let (quotient, factor) = Self::constant_mul_operands(expr)?;
22        let (dividend, divisor) = quotient.udiv_operands()?;
23        (divisor.as_const() == Some(factor) && !factor.is_zero()).then_some((dividend, factor))
24    }
25
26    // Requesting an anchor preserves the raw dividend relation even when a safe
27    // offset also exposes a relation to the pre-offset value. With no requested
28    // anchor, prefer the shifted relation for quotient cancellation.
29    fn rounding_bounds<'a>(
30        &self,
31        expr: &'a SymExpr,
32        anchor: Option<&SymExpr>,
33    ) -> Option<RoundingBounds<'a>> {
34        let mut remaining = MAX_LOCAL_ANALYSIS_NODES;
35        self.rounding_bounds_cached(expr, anchor, &mut HashMap::default(), &mut remaining)
36    }
37
38    fn rounding_bounds_cached<'a>(
39        &self,
40        expr: &'a SymExpr,
41        anchor: Option<&SymExpr>,
42        intervals: &mut HashMap<SymExpr, Option<WordInterval>>,
43        remaining: &mut usize,
44    ) -> Option<RoundingBounds<'a>> {
45        let (dividend, divisor) = Self::rounded_product_operands(expr)?;
46        // Euclidean division: q*d = dividend - remainder, 0 <= remainder < d.
47        // In particular, q*d <= dividend <= MAX, so the rescaling cannot wrap.
48        let width = divisor - U256::ONE;
49        let raw = RoundingBounds { anchor: dividend, below: width, above: U256::ZERO };
50        if anchor == Some(dividend) {
51            return Some(raw);
52        }
53        let offset = match dividend.kind() {
54            SymExprKind::BinOp(SymBinOp::Add, anchor, bias)
55                if let Some(bias) = bias.as_const()
56                    && bias <= width =>
57            {
58                Some((anchor, bias, bias))
59            }
60            SymExprKind::BinOp(SymBinOp::Sub, sum, one)
61                if one.as_const() == Some(U256::ONE)
62                    && let SymExprKind::BinOp(SymBinOp::Add, anchor, bias) = sum.kind()
63                    && bias.as_const() == Some(divisor) =>
64            {
65                // Preserve the intermediate addition in `(anchor + d) - 1`.
66                Some((anchor, width, divisor))
67            }
68            _ => None,
69        };
70        if let Some((anchor, bias, addition)) = offset
71            && self
72                .interval_cached(anchor, intervals, remaining)
73                .is_some_and(|range| range.max.checked_add(addition).is_some())
74        {
75            // For dividend = anchor + bias, the error is bias - remainder.
76            return Some(RoundingBounds { anchor, below: width - bias, above: bias });
77        }
78        // An unproved offset remains opaque. A bound on a wrapped sum cannot
79        // justify removing that sum from the relation.
80        Some(raw)
81    }
82
83    /// A nonnegative rounding error smaller than a divisor preserves its quotient.
84    pub(super) fn quotient_of_rounded_product<'a>(&self, expr: &'a SymExpr) -> Option<&'a SymExpr> {
85        let (numerator, divisor) = expr.udiv_operands()?;
86        let bounds = self.rounding_bounds(numerator, None)?;
87        let minimum =
88            divisor.as_const().or_else(|| self.unsigned_lower_bounds.get(divisor).copied())?;
89        if !bounds.below.is_zero() || bounds.above >= minimum {
90            return None;
91        }
92        let SymExprKind::BinOp(SymBinOp::Mul, left, right) = bounds.anchor.kind() else {
93            return None;
94        };
95        let value = if left == divisor {
96            right
97        } else if right == divisor {
98            left
99        } else {
100            return None;
101        };
102        // The anchor is an EVM word. Cancelling a factor requires independent
103        // evidence that its mathematical product did not wrap.
104        self.mul_cannot_overflow_256(value, divisor).then_some(value)
105    }
106
107    pub(super) fn rounding_comparison_value(&self, expr: &SymBoolExpr) -> Option<bool> {
108        if let SymBoolExprKind::Not(inner) = expr.kind() {
109            return self.rounding_comparison_value(inner).map(|value| !value);
110        }
111        let SymBoolExprKind::Cmp(op, left, right) = expr.kind() else { return None };
112        for (rounded, anchor, op) in [
113            (left, right, *op),
114            (
115                right,
116                left,
117                match op {
118                    SymCmpOp::Ult => SymCmpOp::Ugt,
119                    SymCmpOp::Ule => SymCmpOp::Uge,
120                    SymCmpOp::Ugt => SymCmpOp::Ult,
121                    SymCmpOp::Uge => SymCmpOp::Ule,
122                    other => *other,
123                },
124            ),
125        ] {
126            if let Some(bounds) = self.rounding_bounds(rounded, Some(anchor))
127                && bounds.anchor == anchor
128            {
129                match op {
130                    SymCmpOp::Uge if bounds.below.is_zero() => return Some(true),
131                    SymCmpOp::Ult if bounds.below.is_zero() => return Some(false),
132                    SymCmpOp::Ule if bounds.above.is_zero() => return Some(true),
133                    SymCmpOp::Ugt if bounds.above.is_zero() => return Some(false),
134                    _ => {}
135                }
136            }
137        }
138        None
139    }
140
141    /// Bounds a subtraction only when the relation proves it cannot underflow.
142    pub(super) fn rounding_error_interval(
143        &self,
144        left: &SymExpr,
145        right: &SymExpr,
146        intervals: &mut HashMap<SymExpr, Option<WordInterval>>,
147        remaining: &mut usize,
148    ) -> Option<WordInterval> {
149        if let Some(bounds) = self.rounding_bounds_cached(left, Some(right), intervals, remaining)
150            && bounds.anchor == right
151            && bounds.below.is_zero()
152        {
153            return Some(WordInterval { min: U256::ZERO, max: bounds.above });
154        }
155        if let Some(bounds) = self.rounding_bounds_cached(right, Some(left), intervals, remaining)
156            && bounds.anchor == left
157            && bounds.above.is_zero()
158        {
159            return Some(WordInterval { min: U256::ZERO, max: bounds.below });
160        }
161        None
162    }
163}
164
165#[cfg(test)]
166mod tests {
167    use super::{
168        super::{
169            SymCx, SymbolicModel, normalize_constraints_for_solver,
170            normalize_constraints_for_solver_cached,
171        },
172        *,
173    };
174
175    fn rounded(cx: &mut SymCx, value: &SymExpr, divisor: U256, bias: U256, split: bool) -> SymExpr {
176        let divisor_expr = SymExpr::constant(cx, divisor);
177        let bias_expr = SymExpr::constant(cx, if split { bias + U256::ONE } else { bias });
178        let dividend = SymExpr::binop(cx, SymBinOp::Add, value.clone(), bias_expr);
179        let dividend = if split {
180            let one = SymExpr::one(cx);
181            SymExpr::binop(cx, SymBinOp::Sub, dividend, one)
182        } else {
183            dividend
184        };
185        let quotient = SymExpr::binop(cx, SymBinOp::UDiv, dividend, divisor_expr.clone());
186        SymExpr::binop(cx, SymBinOp::Mul, quotient, divisor_expr)
187    }
188
189    #[test]
190    fn ceiling_rounding_proves_order_and_error_for_both_addition_forms() {
191        let mut cx = SymCx::new();
192        let value = SymExpr::var(&mut cx, "value");
193        let bound =
194            SymBoolExpr::cmp_word_const(&mut cx, SymCmpOp::Ule, &value, U256::MAX - U256::from(37));
195        let complement = SymExpr::not(&mut cx, value.clone());
196        let complement_bound =
197            SymBoolExpr::cmp_word_const(&mut cx, SymCmpOp::Uge, &complement, U256::from(37));
198        for bound in [bound, complement_bound] {
199            for split in [false, true] {
200                let rounded = rounded(&mut cx, &value, U256::from(37), U256::from(36), split);
201                let error = SymExpr::binop(&mut cx, SymBinOp::Sub, rounded.clone(), value.clone());
202                let order = SymBoolExpr::cmp(&mut cx, SymCmpOp::Uge, rounded, value.clone());
203                let error_bound =
204                    SymBoolExpr::cmp_word_const(&mut cx, SymCmpOp::Ult, &error, U256::from(37));
205                for property in [order, error_bound] {
206                    let failure = property.not(&mut cx);
207                    let normalized =
208                        normalize_constraints_for_solver(&mut cx, &[bound.clone(), failure]);
209                    assert_eq!(normalized, vec![SymBoolExpr::constant(&mut cx, false)]);
210                }
211            }
212        }
213    }
214
215    #[test]
216    fn safe_offsets_preserve_dividend_order_and_remainder() {
217        let mut cx = SymCx::new();
218        let value = SymExpr::var(&mut cx, "value");
219        let safe =
220            SymBoolExpr::cmp_word_const(&mut cx, SymCmpOp::Ule, &value, U256::MAX - U256::from(37));
221        let mut cache = HashMap::default();
222        for bias in [U256::ZERO, U256::from(18), U256::from(36)] {
223            for split in [false, true] {
224                let rounded = rounded(&mut cx, &value, U256::from(37), bias, split);
225                let (dividend, _) = ConstraintContext::rounded_product_operands(&rounded).unwrap();
226                let error =
227                    SymExpr::binop(&mut cx, SymBinOp::Sub, dividend.clone(), rounded.clone());
228                let order =
229                    SymBoolExpr::cmp(&mut cx, SymCmpOp::Ule, rounded.clone(), dividend.clone());
230                let remainder =
231                    SymBoolExpr::cmp_word_const(&mut cx, SymCmpOp::Ult, &error, U256::from(37));
232                for property in [order, remainder] {
233                    for bounded in [true, false, true] {
234                        let mut constraints = vec![property.clone().not(&mut cx)];
235                        if bounded {
236                            constraints.push(safe.clone());
237                        }
238                        for _ in 0..2 {
239                            let normalized = normalize_constraints_for_solver_cached(
240                                &mut cx,
241                                &constraints,
242                                &mut cache,
243                            );
244                            assert_eq!(
245                                normalized,
246                                vec![SymBoolExpr::constant(&mut cx, false)],
247                                "bias={bias}, split={split}, bounded={bounded}"
248                            );
249                            constraints.reverse();
250                        }
251                    }
252                }
253            }
254        }
255    }
256
257    #[test]
258    fn rounding_relations_bound_biased_dividends_at_word_boundaries() {
259        let mut cx = SymCx::new();
260        let value = SymExpr::var(&mut cx, "value");
261        for divisor in [U256::from(3), U256::from(37), (U256::ONE << 255) - U256::ONE, U256::MAX] {
262            for bias in [U256::ZERO, divisor / U256::from(2), divisor - U256::ONE] {
263                let bound =
264                    SymBoolExpr::cmp_word_const(&mut cx, SymCmpOp::Ule, &value, U256::MAX - bias);
265                let context = ConstraintContext::new(&[bound]);
266                let rounded = rounded(&mut cx, &value, divisor, bias, false);
267                let relation = context.rounding_bounds(&rounded, None).unwrap_or_else(|| {
268                    panic!(
269                        "missing relation: divisor={divisor}, bias={bias}, expression={rounded:?}"
270                    )
271                });
272                assert_eq!(relation.anchor, &value);
273                let samples = (0..=255).map(U256::from).chain([
274                    U256::ONE << 255,
275                    U256::MAX - bias,
276                    U256::MAX,
277                ]);
278                for input in samples.filter(|input| *input <= U256::MAX - bias) {
279                    let mut model = SymbolicModel::default();
280                    assert!(value.assign_model_value(&mut model, input));
281                    let output = rounded.eval_model(&model).unwrap();
282                    if output >= input {
283                        assert!(output - input <= relation.above);
284                    } else {
285                        assert!(input - output <= relation.below);
286                    }
287                }
288            }
289        }
290    }
291
292    #[test]
293    fn rounding_normalization_preserves_wrapping_and_signed_comparisons() {
294        let mut cx = SymCx::new();
295        let value = SymExpr::var(&mut cx, "value");
296        let mut cache = HashMap::default();
297        let safe =
298            SymBoolExpr::cmp_word_const(&mut cx, SymCmpOp::Ule, &value, U256::MAX - U256::from(37));
299        for bias in [U256::ZERO, U256::from(36)] {
300            for split in [false, true] {
301                let rounded = rounded(&mut cx, &value, U256::from(37), bias, split);
302                let error = SymExpr::binop(&mut cx, SymBinOp::Sub, rounded.clone(), value.clone());
303                for op in [
304                    SymCmpOp::Eq,
305                    SymCmpOp::Ult,
306                    SymCmpOp::Ule,
307                    SymCmpOp::Ugt,
308                    SymCmpOp::Uge,
309                    SymCmpOp::Slt,
310                    SymCmpOp::Sgt,
311                ] {
312                    let comparison = SymBoolExpr::cmp(&mut cx, op, rounded.clone(), value.clone());
313                    let error_bound =
314                        SymBoolExpr::cmp_word_const(&mut cx, op, &error, U256::from(37));
315                    for predicate in [comparison, error_bound] {
316                        for predicate in [predicate.clone(), predicate.not(&mut cx)] {
317                            for bounded in [true, false, true] {
318                                let mut constraints = vec![predicate.clone()];
319                                if bounded {
320                                    constraints.push(safe.clone());
321                                }
322                                for _ in 0..2 {
323                                    let normalized = normalize_constraints_for_solver_cached(
324                                        &mut cx,
325                                        &constraints,
326                                        &mut cache,
327                                    );
328                                    for input in [
329                                        U256::ZERO,
330                                        U256::ONE,
331                                        U256::from(36),
332                                        U256::from(37),
333                                        (U256::ONE << 255) - U256::ONE,
334                                        U256::ONE << 255,
335                                        U256::MAX - U256::from(37),
336                                        U256::MAX - U256::ONE,
337                                        U256::MAX,
338                                    ] {
339                                        let mut model = SymbolicModel::default();
340                                        assert!(value.assign_model_value(&mut model, input));
341                                        assert_eq!(
342                                            constraints
343                                                .iter()
344                                                .all(|c| c.eval_model(&model).unwrap()),
345                                            normalized
346                                                .iter()
347                                                .all(|c| c.eval_model(&model).unwrap()),
348                                            "bias={bias}, split={split}, op={op:?}, bounded={bounded}, input={input}"
349                                        );
350                                    }
351                                    constraints.reverse();
352                                }
353                            }
354                        }
355                    }
356                }
357            }
358        }
359    }
360
361    #[test]
362    fn wrapped_dividend_bound_does_not_establish_rounding_safety() {
363        let mut cx = SymCx::new();
364        let value = SymExpr::var(&mut cx, "value");
365        let rounded = rounded(&mut cx, &value, U256::from(37), U256::from(36), false);
366        let (dividend, _) = ConstraintContext::rounded_product_operands(&rounded).unwrap();
367        let bound = SymBoolExpr::cmp_word_const(&mut cx, SymCmpOp::Ule, dividend, U256::from(36));
368        let order = SymBoolExpr::cmp(&mut cx, SymCmpOp::Ult, rounded, value.clone());
369        let constraints = vec![bound, order];
370        let normalized = normalize_constraints_for_solver(&mut cx, &constraints);
371        let mut model = SymbolicModel::default();
372        assert!(value.assign_model_value(&mut model, U256::MAX));
373        assert!(constraints.iter().all(|c| c.eval_model(&model).unwrap()));
374        assert!(normalized.iter().all(|c| c.eval_model(&model).unwrap()));
375    }
376}
foundry_evm_symbolic/runtime/solver/normalize/rounding.rs

foundry_evm_symbolic/runtime/solver/normalize/
rounding.rs
