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}
foundry_evm_symbolic/runtime/solver/normalize/rounding.rs

foundry_evm_symbolic/runtime/solver/normalize/
rounding.rs
