Repository navigation
Move keccak preimage handling into EVM.Keccak.Preimages, end infeasible paths at branch queries - #1163
Merged
Conversation
Preimages are typed (mapping, array, raw), the simplifier and the SMT keccak assumptions share one table of small array slots and one lookup of the field-offset window, and the assumed keccak range is named. 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>
checkBranch took an unsatisfiable branch condition to mean the branch is not taken, also when the path conditions themselves were unsatisfiable, so such paths kept running, e.g. until the loop iteration limit. It now checks the negation too and returns Infeasible when both fail, and the path ends like a failed vm.assume. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A copy with a symbolic size passes the memory access check during execution, and its size can become a huge literal only once keccaks are concretized for the SMT encoding, which then unrolled one store per byte and exhausted memory. The encoder now rejects such sizes, using the limit execution already applies to literal sizes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A parsed W256 or W64 stayed a thunk that held its string until used. In the symbolic-execution fuzzer, a geth trace with deep stacks on every line, read as a String and parsed this way, took several GB. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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.
Description
Keccak preimage handling (tables, the field-offset window lookup, folded-slot recovery, decoding recorded preimages, the assumed keccak range) now lives in one module,
EVM.Keccak.Preimages, shared by the simplifier and the SMT keccak assumptions. This removes the simplifier's separate array preimage table.Behaviour changes:
setUp), as the final queries already did.checkBranchtook an unsatisfiable branch condition to mean the branch is not taken, even when the path conditions themselves were unsatisfiable, so such paths kept running, e.g. until the loop iteration limit. It now checks the negation too, and ends the path when both are unsatisfiable. This costs one extra solver query when a branch condition is unsatisfiable.Checklist