fix(symbolic): register folded mapping slots as keccak preimages

crates/evm/symbolic/Cargo.toml

@@ -17,6 +17,7 @@ workspace = true
 foundry-common.workspace = true
 foundry-config.workspace = true
 foundry-cheatcodes-spec.workspace = true
+foundry-compilers.workspace = true
 foundry-evm.workspace = true
 
 evm2.workspace = true

crates/evm/symbolic/README.md

@@ -881,7 +881,7 @@ Known incomplete, bounded, or approximate surfaces include:
 | Dynamic memory and copy bounds | Many symbolic memory, calldata, returndata, and `MCOPY`/`RETURNDATACOPY` sizes are supported when bounded by configuration or solver-proved limits. Accesses beyond the configured `memory_limit`, and `RETURNDATACOPY` ranges beyond the return data, halt exceptionally as in concrete execution. Symbolic sizes that stay within memory but exceed the configured copy bounds report incomplete. |
 | Opcode activation | Implemented opcodes follow the active EVM version. An opcode used before its activation fork causes an exceptional halt, matching concrete execution. |
 | Concrete-required operands and bytecode | Symbolic data can flow through calldata, memory, storage, logs, and returndata, but some control/metadata values must resolve to concrete or solver-constrained values: `JUMP`/`JUMPI` destinations, `BLOBHASH` indices, cheatcode selectors, many cheatcode ABI decodes, fork IDs/block numbers, nonces, and created runtime bytecode opcodes. Symbolic bytecode opcodes, symbolic runtime sizes, or unconstrained control operands report incomplete. |
-| Symbolic hashing and `KECCAK256` | Concrete hashes are computed exactly. Symbolic `KECCAK256` is represented by deterministic opaque terms plus Solidity-storage-layout heuristics for common mapping and dynamic-array keys. For storage keys `keccak(...) + offset`, offsets below `2^64` are assumed not to alias fixed slots or other hash bases; larger offsets are compared exactly, so an index bounded only by an abstract array length may report incomplete. A constant slot only counts as `keccak(...) + offset` when that hash was computed concretely during the run; other constants are fixed slots. A symbolic hash of constant input length compared with a 32- or 64-byte hash computed concretely during the run, or with a symbolic hash over a different constant input length, is decided by comparing inputs, assuming no collisions. Proof obligations that depend on cryptographic facts such as non-zero hashes, collision resistance, or preimage resistance are not proof-grade and may report incomplete or produce replay-filtered candidates. |
+| Symbolic hashing and `KECCAK256` | Concrete hashes are computed exactly. Symbolic `KECCAK256` is represented by deterministic opaque terms plus Solidity-storage-layout heuristics for common mapping and dynamic-array keys. For storage keys `keccak(...) + offset`, offsets below `2^64` are assumed not to alias fixed slots or other hash bases; larger offsets are compared exactly, so an index bounded only by an abstract array length may report incomplete. A constant slot only counts as `keccak(...) + offset` when the run computed that hash concretely or when it is a mapping root from a deployed contract's storage layout hashed with a source literal or bytecode constant, which covers slots the optimizer folds for constant keys (one nested level); other constants are fixed slots. A symbolic hash of constant input length compared with a 32- or 64-byte hash computed concretely during the run, or with a symbolic hash over a different constant input length, is decided by comparing inputs, assuming no collisions. Proof obligations that depend on cryptographic facts such as non-zero hashes, collision resistance, or preimage resistance are not proof-grade and may report incomplete or produce replay-filtered candidates. |
 | Symbolic storage base values | Writes and later reads through symbolic keys are modeled, with Solidity-layout heuristics for common mapping/dynamic-array keys. Reads of previously-unwritten symbolic keys are abstract storage variables by default, or zero under the zero-init storage layout; the engine does not enumerate arbitrary concrete backend storage slots for a symbolic key. Proofs involving unknown existing storage are scoped to the selected `symbolic.storage_layout`. |
 | Precompiles | Canonical precompiles are recognized according to the active EVM version, including the Prague BLS12-381 precompiles `0x0b`-`0x11` and Osaka P256VERIFY `0x100`; an address that is not a precompile on the active hardfork, such as KZG `0x0a` before Cancun, falls back to normal empty-account behavior. Precompile addresses use normal account emptiness checks for `EXTCODEHASH`. Concrete inputs for every active precompile execute the corresponding revm precompile for the active hardfork with effectively unlimited gas. Symbolic identity is byte-precise; symbolic hash/modexp outputs are deterministic opaque terms or fixed-length symbolic outputs, not full cryptographic/algebraic models. Symbolic ecrecover returns empty data for invalid recovery IDs and models both empty and 32-byte returndata when recovery is uncertain; the recovered address remains an opaque term. Symbolic BN254 inputs and symbolic BLAKE2f final flags report incomplete because precompile success depends on validity checks the symbolic model does not prove. KZG `0x0a` concrete inputs execute the revm KZG precompile exactly. Symbolic KZG calls model broad exact failures such as invalid input length and version/hash mismatches where known, plus selected replayable success/failure witnesses. Any remaining feasible symbolic KZG space reports incomplete rather than being treated as proved safe. Symbolic inputs to BLS12-381 and P256VERIFY report incomplete. Symbolic length headers, symbolic modexp output lengths, out-of-bounds symbolic inputs, future/custom precompiles, and precompile gas/OOG behavior are not fully modeled. |
 | Hard arithmetic | Bit-vector arithmetic is modeled through SMT. Forge canonicalizes small polynomial equalities over the exact 256-bit EVM word ring, including identities that wrap, and proves unsigned monotonic product and same-divisor quotient comparisons when path bounds show that every product fits in 256 bits. It first explores branches decided by those local checks and bounded concrete witnesses, then sends the remaining hard-arithmetic branches to the configured SMT solver. Expansion and fallback time are deliberately bounded; division, unsupported `EXP` base/exponent shapes, larger polynomials, and other solver-intractable nonlinear expressions can report incomplete or timeout. |

crates/evm/symbolic/src/executor/invariant.rs

@@ -117,6 +117,7 @@ impl SymbolicExecutor {
         );
         initial_state.apply_executor_env(&mut self.cx, &input.executor);
         initial_state.world.set_storage_layout(self.config.storage_layout);
+        register_folded_mapping_slots(&mut self.cx, &input.executor);
 
         let calldatas = SymbolicCalldata::variants_with_prefix(
             &input.target.function,

crates/evm/symbolic/src/executor/run.rs

@@ -367,6 +367,7 @@ impl SymbolicExecutor {
             .ok_or(SymbolicError::MissingAccount(input.target))?;
         let bytecode = account.code.ok_or(SymbolicError::MissingCode(input.target))?;
         let code = SymCode::from_bytecode(&mut self.cx, &bytecode);
+        register_folded_mapping_slots(&mut self.cx, &input.executor);
         let mut roots = Vec::new();
         for calldata in SymbolicCalldata::variants(input.function, &self.config, &mut self.cx)? {
             let corpus_seed_models = input
@@ -616,6 +617,7 @@ impl SymbolicExecutor {
         );
         initial_state.apply_executor_env(&mut self.cx, &input.executor);
         initial_state.world.set_storage_layout(self.config.storage_layout);
+        register_folded_mapping_slots(&mut self.cx, &input.executor);
         let initial = SequencePath { state: initial_state, steps: Vec::new() };
 
         if symbolic_invariant_should_check(0, input.depth, input.check_interval) {

crates/evm/symbolic/src/runtime.rs

@@ -8,6 +8,7 @@ mod control;
 mod evm;
 mod executor_view;
 mod expr;
+mod folded_slots;
 mod memory;
 mod precompiles;
 mod solver;
@@ -22,6 +23,7 @@ pub(crate) use control::*;
 pub(crate) use evm::*;
 pub use executor_view::ExecutorView;
 pub(crate) use expr::*;
+pub(crate) use folded_slots::*;
 pub(crate) use memory::*;
 pub(crate) use precompiles::*;
 pub(crate) use solver::{BranchFeasibility, SmtLibSubprocessSolver};

crates/evm/symbolic/src/runtime/executor_view.rs

@@ -1,6 +1,7 @@
 use super::*;
 use evm2::evm::{AccountInfo, DbResult};
-use foundry_evm::core::backend::Backend;
+use foundry_common::contracts::ContractsByArtifact;
+use foundry_evm::{core::backend::Backend, fuzz::strategies::LiteralsDictionary};
 
 /// Reads of a backend's accepted state, independent of its network.
 pub(crate) trait AcceptedState {
@@ -52,6 +53,10 @@ pub struct ExecutorView<'a> {
     pub(crate) storage_load_hooks: Vec<(Address, SymbolicStorageHook)>,
     pub(crate) storage_store_hooks: Vec<(Address, SymbolicStorageHook)>,
     pub(crate) mapping_storage_store_hooks: Vec<((Address, U256), SymbolicStorageHook)>,
+    /// Project artifacts, used to find the storage layouts of deployed contracts.
+    pub(crate) known_contracts: Option<&'a ContractsByArtifact>,
+    /// Source literals, used as candidate keys of constant-folded mapping slots.
+    pub(crate) literals: Option<&'a LiteralsDictionary>,
 }
 
 /// Block environment values exposed to symbolic execution.
@@ -172,6 +177,20 @@ impl<'a> ExecutorView<'a> {
                     )
                 })
                 .collect(),
+            known_contracts: None,
+            literals: None,
         }
     }
+
+    /// Attaches the project artifacts and source literals that register the constant-folded
+    /// mapping slots of deployed contracts before a run.
+    pub const fn with_project(
+        mut self,
+        known_contracts: &'a ContractsByArtifact,
+        literals: &'a LiteralsDictionary,
+    ) -> Self {
+        self.known_contracts = Some(known_contracts);
+        self.literals = Some(literals);
+        self
+    }
 }

crates/evm/symbolic/src/runtime/expr/cx.rs

@@ -94,7 +94,7 @@ impl SymCx {
         self.replayable_inputs.contains(&symbol)
     }
 
-    pub(in crate::runtime::expr) fn record_concrete_keccak_preimage(
+    pub(in crate::runtime) fn record_concrete_keccak_preimage(
         &mut self,
         hash: U256,
         bytes: Arc<[SymExpr]>,

crates/evm/symbolic/src/runtime/folded_slots.rs

@@ -0,0 +1,143 @@
+//! Registration of constant-folded mapping slots as concrete Keccak preimages.
+//!
+//! With the optimizer on, solc folds the slot of a mapping entry at a constant key,
+//! `keccak256(abi.encode(key, slot))`, into one `PUSH32`. The engine treats a constant slot as a
+//! hash only when it knows a preimage, so the folded slot would otherwise count as a fixed slot
+//! that a write through a symbolic key never reaches. Before a run, the mapping roots in the
+//! storage layout of each deployed contract are hashed with every candidate key: the source
+//! literals and the contract's `PUSH` immediates. Nested mappings get one more level. A registered
+//! preimage is a real one, so this adds no unsoundness; constants that no candidate produces, such
+//! as ERC-1967 and ERC-7201 roots, stay fixed slots.
+
+use super::*;
+use foundry_common::slot_identifier::{ENCODING_INPLACE, ENCODING_MAPPING};
+use foundry_compilers::artifacts::{Storage, StorageLayout, StorageType};
+
+/// Mapping levels hashed below a storage layout root: the mapping itself and one nested mapping.
+const FOLDED_MAPPING_LEVELS: usize = 2;
+
+/// Records the folded mapping slots of every deployed contract with a known storage layout.
+pub(crate) fn register_folded_mapping_slots(cx: &mut SymCx, executor: &ExecutorView<'_>) {
+    let Some(known_contracts) = executor.known_contracts else { return };
+    let literals = executor
+        .literals
+        .map(|literals| {
+            literals
+                .get()
+                .words
+                .values()
+                .flatten()
+                .map(|word| (*word).into())
+                .collect::<HashSet<U256>>()
+        })
+        .unwrap_or_default();
+    for &address in &executor.account_addresses {
+        if let Ok(Some(account)) = executor.backend.basic(address)
+            && let Some(code) = &account.code
+            && !code.is_empty()
+            && let Some((_, contract)) =
+                known_contracts.find_by_deployed_code_exact(code.original_byte_slice())
+            && let Some(layout) = &contract.storage_layout
+        {
+            let mut keys = literals.clone();
+            keys.extend(push_immediates(code.original_byte_slice()));
+            let keys = keys.into_iter().collect::<Vec<_>>();
+            for entry in &layout.storage {
+                if let Ok(slot) = entry.slot.parse::<U256>() {
+                    register_mapping_slots(
+                        cx,
+                        layout,
+                        slot,
+                        &entry.storage_type,
+                        &keys,
+                        FOLDED_MAPPING_LEVELS,
+                    );
+                }
+            }
+        }
+    }
+}
+
+/// Returns the right-aligned values of the `PUSH` immediates in `code`.
+fn push_immediates(code: &[u8]) -> impl Iterator<Item = U256> {
+    let mut pc = 0;
+    std::iter::from_fn(move || {
+        while let Some(&op) = code.get(pc) {
+            pc += 1;
+            if let opcode::PUSH1..=opcode::PUSH32 = op {
+                let len = usize::from(op - opcode::PUSH1 + 1);
+                let data = &code[pc..code.len().min(pc + len)];
+                pc += len;
+                return Some(U256::from_be_slice(data));
+            }
+        }
+        None
+    })
+}
+
+/// Hashes every candidate key that fits the key type of the mapping at `slot`, descending into
+/// struct members and `levels - 1` nested mapping levels.
+fn register_mapping_slots(
+    cx: &mut SymCx,
+    layout: &StorageLayout,
+    slot: U256,
+    type_id: &str,
+    keys: &[U256],
+    levels: usize,
+) {
+    let Some(ty) = layout.types.get(type_id) else { return };
+    if levels == 0 {
+        return;
+    }
+    if ty.encoding == ENCODING_MAPPING {
+        let Some((key_ty, value_id)) =
+            ty.key.as_deref().and_then(|key| layout.types.get(key)).zip(ty.value.as_deref())
+        else {
+            return;
+        };
+        for &key in keys.iter().filter(|&&key| key_fits(key_ty, key)) {
+            let hash = record_mapping_preimage(cx, key, slot);
+            register_mapping_slots(cx, layout, hash, value_id, keys, levels - 1);
+        }
+    } else if ty.encoding == ENCODING_INPLACE
+        && let Some(members) = ty
+            .other
+            .get("members")
+            .and_then(|members| serde_json::from_value::<Vec<Storage>>(members.clone()).ok())
+    {
+        for member in &members {
+            if let Ok(offset) = member.slot.parse::<U256>() {
+                let slot = slot.wrapping_add(offset);
+                register_mapping_slots(cx, layout, slot, &member.storage_type, keys, levels);
+            }
+        }
+    }
+}
+
+/// Returns whether `key` is a value of the mapping key type `ty` as `abi.encode` pads it.
+fn key_fits(ty: &StorageType, key: U256) -> bool {
+    let Ok(bytes) = ty.number_of_bytes.parse::<usize>() else { return false };
+    let bits = bytes * 8;
+    if bits == 0 || bits > 256 || ty.label == "string" || ty.label == "bytes" {
+        // Dynamic keys are hashed from their bytes, not from a padded word.
+        false
+    } else if ty.label.starts_with("int") {
+        let magnitude = U256::ONE << (bits - 1);
+        key < magnitude || key >= U256::ZERO.wrapping_sub(magnitude)
+    } else if ty.label.starts_with("bytes") {
+        key.trailing_zeros() >= 256 - bits
+    } else {
+        bits == 256 || key < U256::ONE << bits
+    }
+}
+
+/// Records `keccak(key . slot)` with its 64-byte preimage and returns the hash.
+fn record_mapping_preimage(cx: &mut SymCx, key: U256, slot: U256) -> U256 {
+    let mut bytes = [0u8; 64];
+    bytes[..32].copy_from_slice(B256::from(key).as_slice());
+    bytes[32..].copy_from_slice(B256::from(slot).as_slice());
+    let hash = keccak256(bytes).into();
+    let preimage = bytes.iter().map(|&byte| SymExpr::constant(cx, U256::from(byte))).collect();
+    cx.record_concrete_keccak_preimage(hash, preimage);
+    hash
+}

crates/forge/src/cmd/test/mod.rs

@@ -1241,10 +1241,14 @@ impl TestArgs {
                 None => config.cache_path.join(AUTO_FUZZ_FAILURE_DIR).join(AUTO_CORPUS_DIR),
             });
         }
+        // The debugger labels slots from the layout, and symbolic execution learns the mapping
+        // roots behind constant-folded slots from it.
+        if (self.debug || config.symbolic.enabled)
+            && !config.extra_output.contains(&ContractOutputSelection::StorageLayout)
+        {
+            config.extra_output.push(ContractOutputSelection::StorageLayout);
+        }
         if self.debug {
-            if !config.extra_output.contains(&ContractOutputSelection::StorageLayout) {
-                config.extra_output.push(ContractOutputSelection::StorageLayout);
-            }
             // Full build infos keep the sources the compiler saw, which dynamic test linking
             // rewrites in test files.
             if let Err(error) = config.enable_debug_build_info() {

crates/forge/src/runner.rs

@@ -1997,7 +1997,8 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
         branch_target: Option<SymbolicBranchTarget>,
     ) -> SymbolicRunInput<'f> {
         SymbolicRunInput {
-            executor: ExecutorView::new(self.executor.as_ref()),
+            executor: ExecutorView::new(self.executor.as_ref())
+                .with_project(&self.cr.mcr.known_contracts, &self.cr.mcr.fuzz_literals),
             target: self.address,
             sender,
             function: func,
@@ -3249,7 +3250,8 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
             .collect::<Vec<_>>();
         let mut symbolic = SymbolicExecutor::new(self.config.symbolic.clone());
         let result = symbolic.search_invariant_candidates(SymbolicInvariantCandidateInput {
-            executor: ExecutorView::new(prefix_executor),
+            executor: ExecutorView::new(prefix_executor)
+                .with_project(&self.cr.mcr.known_contracts, &self.cr.mcr.invariant_literals),
             invariant_address: invariant_contract.address,
             invariants: &invariants,
             after_invariant,
@@ -3513,7 +3515,8 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
                 frontier.operands.result,
             );
             let search = symbolic.search_branch_target(SymbolicRunInput {
-                executor: ExecutorView::new(&prefix_executor),
+                executor: ExecutorView::new(&prefix_executor)
+                    .with_project(&self.cr.mcr.known_contracts, &self.cr.mcr.invariant_literals),
                 target: call.call_details.target,
                 sender: call.sender,
                 function,
@@ -4377,7 +4380,8 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
             };
             let mut symbolic = SymbolicExecutor::new(symbolic_config.clone());
             match symbolic.run_invariant(SymbolicInvariantRunInput {
-                executor: ExecutorView::new(&evm.executor),
+                executor: ExecutorView::new(&evm.executor)
+                    .with_project(&self.cr.mcr.known_contracts, &self.cr.mcr.invariant_literals),
                 invariant_address: self.address,
                 sender: self.sender,
                 invariant: anchor,