Repository navigation
Conversation
msooseth
force-pushed
the
stack/3-simplifier
branch
2 times, most recently
from
November 13, 2026 14:34
0edb0c1 to
7776e08
Compare
…tant propagation; immutables in Foundry source lookup Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…erflow checks Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…on reduction and remainders a <= c*x bounds a/c by x, and c*x <= a bounds it below; ceilDiv(c1*x, c2) is x/(c2/c1) or one less when c1 divides c2; a%b <= a and a%b < b. They close the PSM swap round trip and previewSwapExactOut proofs that timed out. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A merged short-circuit overflow check leaves ITE y (x*y) 0, which is x*y. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
x < x - x % c is never true (x % 0 is 0). Solidity's uintN version masks both sides, x = t & m and (t - x % c) & m with m = 2^n - 1, and the masked difference is still x - x % c. Drips compares the current timestamp with the start of its cycle this way (now < now - now % cycleSecs); left alone, the condition stays symbolic and, through the packed array offset it selects, reaches SMT as a symbolic exponent. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Merging branches nests ITEs with literal leaves, e.g. a value scaled by a constant per set bit. Lift operations into all leaves, up to 16, instead of only into one level of literal branches. The rewrite fuzzer generates such trees and merged chains. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
mapExpr and foldExpr walked shared nodes once per path to them, which is exponential in the depth of sharing: a merged x' = ITE (c x) x (f x) chain, as Solidity's least-significant-bit search becomes, refers to each x three times. mapExpr now memoizes per call by node id. foldExprOnce/foldPropOnce visit each node once, for idempotent monoids; containsNode, the logical store, small-subterm and literal-ITE searches, and boundedScaling use them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Bounds on c + x, c - x and ~x carry to x, keeping the side of a wrapping interval the other bounds allow, as in Solidity's signed range checks. A wrap-aware interval of Mod, Add/Sub of a literal and SEx tightens upperWithBounds, and props with contradicting bounds are false. The new boundedMasks pass then decides tests such as absTick & 0x800 for a tick bounded to [-100, 100]. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Narrowing m & x to a smaller mask hid it from the rules that match a mask, e.g. of an address, and split eq-divergent-overapprox-call into seven counterexamples. Rewrite m & x only to 0, when the bound of x leaves none of the bits of m, or to x, when it leaves only bits of m. The rewrite fuzzer generates signed range-check words and bit tests of them under range bounds, and bounds-fuzz checks the bounds of such words. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A price picked by seven tick bits is an ITE tree of 128 literals, so the checked-multiplication guard dividing by it folds only with a limit of 128 leaves. A sign-extended word always lies in its signed range, and props whose bounds leave a term no value in its range are false, which prunes branches of bound() that a signed tick cannot take. The rewrite fuzzer generates trees past the leaf limit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Bounds moved through c + x, c - x and ~x give many more terms a small range, and enumerating them forked loop branches into up to maxWidth paths each, which exhausted memory on spot-clob's Market tests. The shifted bounds now only feed rewriting and pruning (chainedBounds and the contradiction check); propBounds, which the enumeration uses, is the direct bounds again. bounds-fuzz checks the shifted bounds. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
msooseth
force-pushed
the
stack/3-simplifier
branch
from
November 13, 2026 14:36
7776e08 to
c245847
Compare
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
New simplifier rules: Solidity's multiplication overflow checks become bounds, path-condition bounds clear impossible mask bits and refute out-of-range props, operations fold through ITE trees of literals, and constant propagation substitutes any term fixed to a constant. New abstract arithmetic lemmas cover
ceilDiv, division by a constant and remainders.mapExprand the simplifier's subterm searches visit each hash-consed node once instead of once per path to it, which the bound rules rely on to stay fast on merged states.Part 3 of 7 of splitting #1248.
Checklist