Repository navigation
Conversation
A division whose operands the path bounds to a few bits was still sent as a 256-bit `bvudiv`, which z3 could not bit-blast in time. Emit it over the proven width with zero extension, keeping the all-ones result of a zero divisor. The CSE writer is now the single emission path.
mattsse
left a comment
mattsse
left a comment
There was a problem hiding this comment.
Please address the inline SMT emission regression.
| ) { | ||
| if op == SymBinOp::UDiv { | ||
| out.push_str("(ite (= "); | ||
| self.write_expr(out, right, None, None); |
There was a problem hiding this comment.
This emits right both in the zero check and again in the division, but SmtCsePlan counts uses before this duplication. After normalization removes provably nonzero EVM guards, single-use nested divisors therefore expand exponentially instead of receiving bindings. Repro: in a pure check with uint8 x, uint8 d, initialize assembly q := add(d, 1), unroll N steps of q := add(1, div(x, q)), finish with q := div(x, q), and assert q <= x. At N = 8/12/16, the reviewed head emits 122,929/1,966,129/31,457,329 bytes of SMT with no CSE definitions. Each extra level doubles the query, so small additional nesting leads to excessive memory use during query construction, before the solver timeout applies. Please bind the reused divisor or account for these synthesized uses in the CSE plan.
Narrow UDIV writes its divisor twice, but the CSE planner counted only the source use. Count the extra emitted use so nested divisors receive bindings. On a 12-step uint8 chain, the SMT query falls from 1,966,129 to 3,925 bytes with the same proof result.
Why
Before: Z3 could not prove a property with bounded 8-bit divisions when the query used 256-bit division. The initial narrow-width change also expanded shared nested divisors into a large SMT query.
After: The same property is proven, and nested divisors stay shared in the emitted query.
Change
Emit bounded
UDIVandUREMat the proved width while preserving EVM division-by-zero behavior. Count the extra divisor use in narrowUDIVbefore the existing CSE planner assigns bindings.Results
uint8contractDownstream
Symbolic proof completeness improves for this bounded-division case; no API, configuration, or persisted-data format changes. AI assistance was used.