[figtracer]

Why

With the optimizer on, solc folds keccak256(abi.encode(K, slot)) for a constant key into a PUSH32. Under forge test --symbolic that constant counts as a fixed slot that never aliases a write through a symbolic key, so m[o] = 5; assert(m[K] == 0) passes although o == K breaks it. Found by symdiff (Tempo, OPT-01); the check_/test_ twins disagree before and agree after.

function check_const_key(address o) public {
    m[o] = 5;
    assert(m[0xD00D] == 0);
}
function test_const_key() public { check_const_key(address(0xD00D)); }

[PASS] check_const_key(address)          // optimizer runs 200
[FAIL: panic: assertion failed (0x01)] test_const_key()

Change

New runtime/folded_slots.rs: before a run, for every cached account whose code matches a known artifact with a storage layout, hash each mapping root (also inside structs, one nested level) with every candidate key of a fitting type and record the preimage in concrete_keccak_preimages. Candidate keys are the contract's PUSH immediates plus source literals from the fuzz literals dictionary, so constants solc folded away still count. ExecutorView::with_project wires the known contracts and literals at the four runner call sites; forge test adds storageLayout to extra_output when symbolic mode is on. Cases folded into symbolic_keccak_known_preimage_bases_do_not_alias.

Downstream

Base mablr/evm2-migration. Adds a foundry-compilers dependency to the symbolic crate for the layout types and requests storageLayout output in symbolic runs. A registered preimage is a real one, so this adds no unsoundness; ERC-1967 and ERC-7201 constant slots stay fixed slots. Limits: a key that appears in neither the literals nor the bytecode, and a root reached only through assembly (keccak("ns.slot")), are still missed. Cost is keys times roots keccaks per deployed contract per run, not measured on a large project.

[mattsse]

Please address the inline finding.

[mattsse]

Please avoid eagerly materializing every candidate-key pair for nested mappings. For mapping(uint256 => mapping(uint256 => uint256)), this iterates all keys again for each outer key and retains N² preimages on every symbolic run, even if the property never accesses the mapping. In a local dev build of this head, a pure assert(x == x) test with that unused mapping and 2,000 unused integer constants took 7.74s and 3.06 GB peak RSS; with 400 constants it took 0.28s and 213 MB. Discovery also has no deadline/cancellation check, so larger projects can exhaust memory or overrun frontier-search budgets. Please avoid retaining the full Cartesian product and honor the deadline while scanning.