fix(symbolic): prove memory-backed arrays - #16747
Draft
figtracer wants to merge 5 commits into
Draft
Conversation
The model evaluator only lives for the expression roots it evaluates, so its scratch maps can borrow hash-consed nodes instead of cloning handles. This removes reference-count churn without changing evaluation or cache lifetime. On Solady v0.1.26, the focused symbolic suite was neutral at 211.1 ms on master and 211.6 ms on this change. A repeated model-heavy FLS check was also neutral at 243.0 ms and 242.6 ms over 25 runs.
Contributor
✅ Changelog foundThe deterministic check will validate the changed entry. |
Borrowing evaluator cache keys only avoided reference-counted handle churn and produced neutral results on both ordinary Solady and the model-heavy control. Restore the simpler existing representation before retargeting this draft toward measured symbolic-memory work.
Preserve correlated symbolic memory offsets through full-word array assertions and retain conservative bounds needed to prune disjoint writes. This turns an OpenZeppelin Arrays.slice property from incomplete at 50 queries into Safe in 17 while a corrupted variant still produces and concretely replays a counterexample.
figtracer
changed the title
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
1 participant
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.
Preserves correlated symbolic memory offsets through full-word array assertions. The fallback is limited to no-reason
uint256[],int256[], andbytes32[]equality assertions, proves that every feasible CALL size contains the decoded arrays, and accepts the same non-strict ABI tail layouts as the ordinary decoder. This lets symbolic execution finish properties whose array values are assembled through dynamic memory offsets without changing concrete fuzzing.Results
bbf3600dArrays.slicepropertyA deliberately corrupted variant produces
args=[[0], 0, 0], and the persisted artifact reproduces the same assertion failure under concrete replay. The longer candidate wall time is not presented as a speedup: master stops early without proving the property. AI assistance was used for implementation, review, and benchmark analysis.