Repository navigation
Conversation
msooseth
force-pushed
the
stack/5-perf
branch
from
November 13, 2026 14:24
927f1a7 to
cce246d
Compare
msooseth
force-pushed
the
stack/5-perf
branch
from
November 13, 2026 14:34
cce246d to
72ac4c4
Compare
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
staticBranch simplified all path conditions from scratch, twice, at every symbolic jump, which dominated long invariant paths. The simplified conditions are now cached in the VM and only the props added since are simplified on top. The branch condition is also tried alone first, which decides some branches the full simplification cannot. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Common subexpression elimination and the collectors run before a query is encoded (keccak values and literals, storage reads, buffer accesses, referenced variables, buffers and contexts, counterexample defaults) walked the props as trees, exponential in the depth of their sharing. CSE memoizes its rewrite per node id, and the collectors, whose monoids ignore repeats, use the new foldTermOnce. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
CSE names repeated buffers and stores, but words were written out at every use, so a term shared as a DAG, e.g. a merged least-significant-bit search, became exponentially large query text. shareWords counts the uses of each word node after CSE and replaces those used more than once by names, defined with define-fun after the buffer and store definitions. Declarations still come from the unshared props. CSE hash-conses the nodes it rebuilds so they keep ids. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Naming a shared product hid it from the encoder's structural matching: checkedMul no longer saw x == (x * d) / d, and checked-mul-div-cancel turned unknown. Mul, Div, Mod and the other arithmetic nodes stay in place; their operands can still be shared, and the abstract encoding names arithmetic terms itself. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
With --check-static-branches, a branch kept both ways whose one side the solver finds unsatisfiable is a static-missed event, with the condition, its simplified form and the path conditions when expressions are logged. The summary counts them per location, a worklist of missing rules. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
msooseth
force-pushed
the
stack/5-perf
branch
from
November 13, 2026 14:36
72ac4c4 to
cca0da7
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
Query preprocessing visits shared nodes once, repeated word subterms are shared with
define-funin solver queries, and static branch decisions reuse the simplified path conditions. Pending paths are explored depth-first, and the Solidity ASTs are no longer kept.--check-static-branchesalso logs branches that simplification keeps but the solver decides, to find missing simplifier rules.Part 5 of 7 of splitting #1248.
Checklist