Repository navigation
Recover folded mapping slots in keccak assumptions - #1104
Merged
Merged
Conversation
gustavo-grieco
changed the title
msooseth
force-pushed
the
fix/keccak-literal-slots-1103
branch
from
October 19, 2026 09:11
08bd4c0 to
4c85a80
Compare
…ions Recovery of compiler-folded slots now also finds array preimages, follows parent slots through known and recovered hashes, and targets hashes written as parent slots into keccak inputs. Keccak results are bounded from above so field offsets cannot wrap to small slots. Add properties that write storage slots in one keccak representation and read them in another, checking for spurious counterexamples and false proofs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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
2 participants
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
Fixes #1103.
Compiler-folded mapping slots reach the solver as literals without keccak assumptions, allowing symbolic accesses to alias unrelated mappings. Recover these preimages in
concreteKeccaksso the existing assumption generation handles them. This proves thatb[k]stays zero after writinga[3], while preserving the validated counterexample at key3when readinga[k].Recovery uses a shared table for keys below 256 and also tries query literals, with mapping slots and field offsets below 256. Unrecoverable literals retain their existing behavior.
The storage-key fuzzer now emits folded mapping hashes. A new property compares symbolic reads against the expected value across concrete stores and explicit writes, including field offsets. Coverage checks require both same-mapping and different-mapping cases.
Validation: all 846 selected tests passed using Stack with GHC 9.10.3,
-Werror=name-shadowing, Z3, and Bitwuzla (seed1103). Both folded-slot fuzz groups passed 200 cases each, with 51.5% same-mapping and 48.5% different-mapping coverage. The Solidity regression preserved the validated counterexample at key3. The local run excluded CVC5, geth differential tests, and the external Yul corpus.The branch includes current
main, including theabstractArithAPI required by Echidna's compatibility build.Checklist