Repository navigation
Conversation
…nt tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…l forge builds Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…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>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…erflow checks Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…leaks in symbolic execution Success leaves are checked by the solver and deduplicated as they are reached. Traces, memory size and loop visit counters no longer keep earlier VMs alive, and memory snapshots at forks drop the unused zeros. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ions The end states of one call with the same accounts, block and environment become one state constrained by the disjunction of their path conditions, so the next call explores it once. Logs of earlier calls are dropped. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Two parts that differ only in a condition and its negation become one without it, and parts implied by others are dropped, so the branches of an assertion leave no disjunction behind. 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>
The two sides of a JUMPI may meet after the jump target, as in if/else and ternaries. Inside a merged side, a branch its own condition decides is followed. A JUMPI reached again from the same call site is in a loop and forks, so the loop bound applies even when the loop condition is concrete. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The run log shows which tests are still running, which the console hides behind the first unfinished one. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
msooseth
changed the title
hevm test on spark-psm: symbolic pranks, simplifications, ceilDiv lemmashevm test on spark-psm: invariant state merging, diamond merges, lemmas, memory fixes
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>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Solidity writes an element of a packed array (uint32[] etc.) at 256 ** offset, and when the element index depends on a condition the offset is ITE c (Lit x) (Lit y). SMT cannot encode a symbolic exponent, so the query failed with "Cannot encode symbolic exponent". With a literal base, rewrite to ITE c (base ** x) (base ** y), which folds to two constants. Co-Authored-By: Claude Opus 5.5 (1M context) <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>
A merged ternary leaves a two-valued term, e.g. LT 0 x for `b ? 1 : 0`. Used as an array length, it made the free memory pointer and every later memory access symbolic. Memory instructions now fork on such a term in an offset or size, and run again with each value. Co-Authored-By: Claude Opus 5.5 <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>
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>
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>
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>
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>
The size was checked against the maximum with the structural Ord on Expr, so every symbolic size, e.g. end - start of the init code after a symbolic-length memory allocation, failed as too large and the path was silently dropped. Simplify it and compare the literal; a size that stays symbolic ends the path as partial. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A T[] argument with a static T gets a symbolic length of at most --max-dyn-size elements, whose elements are the calldata words after the length word, as bytes and string get theirs. The bound is reported with the same caveat, so such a run is never a clean pass. They used to stop the run with an internal error. The invariant test of an uncallable target now uses bytes[], which is still unsupported. 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>
splitMergedMemArg forked on a merged memory offset before the op ran, even when the stack held fewer items than the op takes: a RETURN with a single symbolic item forked instead of halting with StackUnderrun, and symbolic-lockstep found the symbolic run going on where the concrete one had halted. The split now requires the op's full arity on the stack. 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>
When a memory offset or size is not a literal or a merged ITE, but becomes one for each value of a subterm with at most --max-mem-arg-split values (default 8), e.g. the symbolic length of a short array argument, the path forks on those values and substitutes each one into the stacks, memory, buffers and contract storage and balances. The pushed equality keeps it sound wherever the substitution does not reach. Memory then stays concrete, e.g. for a CREATE after allocating such an array. 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>
The atom enumerateViaSmallSubterm returns is a subterm of the argument simplified, which the stack may not hold as is: substituting it changed nothing, the op ran into the same split again, and a CALL with an input size of mod(x, 8) forked forever (eq-all-yul-optimization-tests timed out). Each branch now also sets the argument to its value. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Memory staying concrete is of no use to an op that ends the frame, and forking there made the lockstep fuzzers find the symbolic run going on where the concrete one had halted, e.g. RETURN at an offset calldataload(0x24) & 1. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
accountEmpty compared the balance with Lit 0 structurally, so a balance
that is a term equal to 0, e.g. after a CALL sending x & 0, made the
account non-empty: EXTCODEHASH returned keccak("") instead of 0, and
the account survived the end-of-transaction cleanup of empty touched
accounts. Found by symbolic-lockstep.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
DynArgBounded records whether bytes/string and whether array arguments were bounded, and the message names only those. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
|
Maybe we could separate the actual stateful invariant code from the other fixes? |
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
Improvements found running
hevm teston the spark-psm repo:prank/startPrankwith a symbolic address (e.g. picked from an actor list) branches over its values instead of failing; invariant tests print partially explored paths grouped by source location instead of their expressionsforge builds and for contracts with immutables; the progress log shows themceilDivby a symbolic divisor,a <= c*xboundinga/cbyx,ceilDiv(c1*x, c2)againstx/(c2/c1)whenc1 | c2, and remainder bounds; allprove_tests of spark-psm now passITE c t ksimplifies totwhentiskwherecis 0--run-log FILE(a START/DONE line per test) and--yul-verbosity N, and tests time out after 10 minutes by defaultChecklist