Fix #1082: resolve symbolic-key SLOAD over a ConcreteStore

[gustavo-grieco]

Fixes #1082.

Problem

readStorage returns an unresolved abstract SLoad for a symbolic slot over a ConcreteStore, even though the store's contents are fully known. The symbolic interpreter then forks on an effectively-known value. Two symptoms:

• Non-termination: observed through echidna's verification mode (concrete deployment populates a ConcreteStore, then a symbolic mapping read never resolves: 0 SMT queries, frozen coverage).
• Blowup on populated stores: standalone hevm test, a symbolic-key read of a never-written mapping over a store holding 600 entries of an unrelated mapping does not complete within 120s. All those entries are dragged into the fork and the SMT encoding even though none of them can alias the read.

Fix

Two pieces. Notably this is not the ITE-over-all-entries fold proposed in the issue: that would inline the whole store into every symbolic read and trades non-termination for OOM on populated stores.

1. An empty ConcreteStore reads 0 at every slot, including symbolic ones. A ConcreteStore is total (unwritten slots are 0), so with no entries every read is 0. This lives in readStorage' (the total variant used by the interpreter's internal-storage path and by expression simplification), not in readStorage: accessStorage relies on readStorage's Nothing/SLoad results to drive lazy RPC slot fetching for external contracts, whose ConcreteStore is a partial cache rather than the full storage. Folding the rule into readStorage would make every first read of an unfetched slot on a forked contract silently return 0 instead of issuing PleaseFetchSlot. A new unit test (readStorage-keeps-nothing-on-concrete-miss) pins that contract.

2. At read time (OpSload), filter the ConcreteStore to entries that can belong to the read's mapping, using the keccak preimages recorded during concrete execution: a concrete key whose known preimage identifies a different mapping slot cannot equal the symbolic read slot, by keccak injectivity — the same assumption family the store simplifier already uses (idsDontMatch, Lit < 256 vs Keccak). A read of an unwritten or unrelated mapping filters to empty → Lit 0, before any fork. Keys with unknown preimage are kept (conservative, sound). The filtered store is only used for the one read expression and is never written back.

This incidentally fulfills the existing word-eq-bug test's TODO: This should be simplified to (Lit 0) — its expectation is updated accordingly.

Tests

• Expr unit tests (test/EVM/Expr/ExprTests.hs): empty-store rule for symbolic slots, preserved Nothing-on-concrete-miss contract of readStorage, write-stripping down to an empty base, and filterStoreByReadSlot drop/keep/ignore cases (using a real keccak' preimage).
• Foundry tests (test/EVM/Test/FoundryTests.hs):
  • pass/symbolicKeySload.sol: the issue's literal empty-store repro, plus a 600-entry populated mapping with a symbolic read of an untouched mapping. Without the fix the latter does not complete (this is the regression signal); with it, ~1s. Both contracts use bool public constant IS_TEST deliberately — a scalar state var would keep a preimage-less slot in the store and route the read through the solver instead of resolving to 0.
  • fail/symbolicKeySload.sol: soundness guard — a symbolic read of the same mapping that holds concrete entries (10, enough to be representative while keeping the SMT query small) must keep them, so the assert is falsifiable. hevm finds and concretely validates the counterexample. If the filter ever unsoundly dropped same-mapping entries, this test would start "passing".

Measurements (arm64 macOS, z3)

Scenario	before	after
issue repro prove_symbolic_key (empty store)	hangs via echidna verification mode	0.08s
unrelated-mapping read, 60 entries	1.44s	0.07s
unrelated-mapping read, 600 entries	>120s (killed)	~1s
same-mapping read (must falsify)	cex validated	same cex, same time

Notes

• keccakPreImgs are only recorded during concrete execution (OpSha3), so the filter benefits exactly the flows that hit this bug: concrete deployment/setUp() followed by symbolic execution (hevm test, echidna verification mode). During pure symbolic execution the preimage map is empty and the filter keeps everything (status quo).
• The filter only applies to a bare ConcreteStore; reads over SStore write-chains are left to the existing simplification/decomposition machinery.
• Entries at scalar slots (no recorded preimage) are always kept. If that ever shows up as a bottleneck, dropping k < 256 keys for keccak-shaped reads would mirror the existing small-lit-vs-keccak assumption; not needed for the cases here.

🤖 Generated with Claude Code

[gustavo-grieco]

CI fix: the Symbolic-Key-SLoad-Fail foundry test made bitwuzla exit with std::bad_alloc (the same-mapping query carried 60 kept entries plus forge-std state, and with the solver dead the runner reported no cex, flipping the result to (True, False)). The query is semantically identical pre- and post-patch — the filter keeps everything for same-mapping reads — so this was test weight, not a regression. Slimmed the soundness canary to a bare contract with 10 entries; locally it finds and concretely validates the counterexample in ~2s with no warnings.

[msooseth]

LGTM