fix(symbolic): explore stateful invariant paths (#15591)

* fix(symbolic): explore multicall invariants

* fix(symbolic): replay setup arbitrary storage

Import setup-time vm.setArbitraryStorage targets into symbolic invariant execution and carry model values for concrete storage slots into replay. This lets invariant counterexamples that depend on symbolic storage behind deployed setup dependencies replay against Forge's concrete executor.

* fix(symbolic): complete hard arithmetic support models

* fix(symbolic): satisfy workspace clippy

* fix(symbolic): continue invariant fuzz after safe symex

* docs(symbolic): document arbitrary storage targets

* test(symbolic): assert invariant fuzz keeps symex metadata

* fix(symbolic): import copied arbitrary storage targets

* fix(symbolic): cache copied arbitrary storage replay values

* fix(symbolic): fall back after invariant symex gaps

* fix(symbolic): preserve invariant counterexample origin

* fix(symbolic): persist invariant replay metadata

* test(symbolic): cover invariant storage rerun

* fix(symbolic): satisfy nightly clippy

* fix(symbolic): replay handler storage reruns

* fix(symbolic): preserve storage key aliases

* fix(symbolic): keep sequence minimization metadata

* fix(symbolic): simplify replay storage key models

* fix(symbolic): tighten invariant replay semantics

* fix(symbolic): tighten invariant replay soundness

* fix(symbolic): align invariant replay semantics

* fix(symbolic): verify replay failure sites

* test(symbolic): cover reverted cheatcode effects

* fix(symbolic): bind handler storage to sequence

Keep symbolic replay storage paired with the exact handler call sequence that produced it. If fuzzing later selects a different reproducer at the same failure site, persist that concrete sequence without stale symbolic storage.

Author: figtracer

crates/cheatcodes/src/evm.rs

@@ -288,7 +288,10 @@ impl Cheatcode for loadCall {
             if ccx.state.has_arbitrary_storage(&target) {
                 // If storage slot is untouched and load from a target with arbitrary storage,
                 // then set random value for current slot.
-                let rand_value = ccx.state.rng().random();
+                let rand_value = ccx
+                    .state
+                    .cached_arbitrary_storage_value(target, slot.into())
+                    .unwrap_or_else(|| ccx.state.rng().random());
                 ccx.state.arbitrary_storage.as_mut().unwrap().save(
                     ccx.ecx,
                     target,

crates/cheatcodes/src/inspector.rs

@@ -403,11 +403,11 @@ pub struct ArbitraryStorage {
     /// Mapping of arbitrary storage addresses to generated values (slot, arbitrary value).
     /// (SLOADs return random value if storage slot wasn't accessed).
     /// Changed values are recorded and used to copy storage to different addresses.
-    pub values: HashMap<Address, HashMap<U256, U256>>,
+    values: HashMap<Address, HashMap<U256, U256>>,
     /// Mapping of address with storage copied to arbitrary storage address source.
-    pub copies: HashMap<Address, Address>,
+    copies: HashMap<Address, Address>,
     /// Address with storage slots that should be overwritten even if previously set.
-    pub overwrites: HashSet<Address>,
+    overwrites: HashSet<Address>,
 }
 
 impl ArbitraryStorage {
@@ -428,6 +428,47 @@ impl ArbitraryStorage {
         }
     }
 
+    /// Returns addresses explicitly marked with arbitrary storage.
+    fn targets(&self) -> impl Iterator<Item = Address> + '_ {
+        self.values.keys().copied()
+    }
+
+    /// Returns addresses explicitly marked with arbitrary storage and whether nonzero slots are
+    /// overwritten.
+    fn target_overwrite_modes(&self) -> impl Iterator<Item = (Address, bool)> + '_ {
+        self.values.keys().map(|address| (*address, self.overwrites.contains(address)))
+    }
+
+    /// Returns addresses that copy storage from arbitrary-storage targets.
+    fn copied_targets(&self) -> impl Iterator<Item = Address> + '_ {
+        self.copies.keys().copied()
+    }
+
+    /// Returns copied arbitrary-storage targets and their source address.
+    fn copied_target_sources(&self) -> impl Iterator<Item = (Address, Address)> + '_ {
+        self.copies.iter().map(|(target, source)| (*target, *source))
+    }
+
+    /// Caches a concrete value for a slot on an arbitrary-storage address or copied target.
+    fn cache_value(&mut self, address: Address, slot: U256, data: U256) {
+        if let Some(values) = self.values.get_mut(&address) {
+            values.insert(slot, data);
+            return;
+        }
+
+        let Some(source) = self.copies.get(&address).copied() else {
+            return;
+        };
+        if let Some(values) = self.values.get_mut(&source) {
+            values.insert(slot, data);
+        }
+    }
+
+    /// Returns a cached arbitrary value for a slot.
+    fn cached_value(&self, address: Address, slot: U256) -> Option<U256> {
+        self.values.get(&address).and_then(|values| values.get(&slot)).copied()
+    }
+
     /// Saves arbitrary storage value for a given address:
     /// - store value in changed values cache.
     /// - update account's storage with given value.
@@ -1298,6 +1339,49 @@ impl<FEN: FoundryEvmNetwork> Cheatcodes<FEN> {
         self.arbitrary_storage.get_or_insert_with(ArbitraryStorage::default)
     }
 
+    /// Returns addresses explicitly marked with arbitrary storage.
+    pub fn arbitrary_storage_targets(&self) -> impl Iterator<Item = Address> + '_ {
+        self.arbitrary_storage.as_ref().into_iter().flat_map(ArbitraryStorage::targets)
+    }
+
+    /// Returns addresses explicitly marked with arbitrary storage and whether nonzero slots are
+    /// overwritten.
+    pub fn arbitrary_storage_target_overwrite_modes(
+        &self,
+    ) -> impl Iterator<Item = (Address, bool)> + '_ {
+        self.arbitrary_storage
+            .as_ref()
+            .into_iter()
+            .flat_map(ArbitraryStorage::target_overwrite_modes)
+    }
+
+    /// Returns addresses that copy storage from arbitrary-storage targets.
+    pub fn arbitrary_storage_copied_targets(&self) -> impl Iterator<Item = Address> + '_ {
+        self.arbitrary_storage.as_ref().into_iter().flat_map(ArbitraryStorage::copied_targets)
+    }
+
+    /// Returns copied arbitrary-storage targets and their source address.
+    pub fn arbitrary_storage_copied_target_sources(
+        &self,
+    ) -> impl Iterator<Item = (Address, Address)> + '_ {
+        self.arbitrary_storage
+            .as_ref()
+            .into_iter()
+            .flat_map(ArbitraryStorage::copied_target_sources)
+    }
+
+    /// Caches a concrete replay value for a slot on an arbitrary-storage address or copied target.
+    pub fn cache_arbitrary_storage_value(&mut self, address: Address, slot: U256, value: U256) {
+        if let Some(storage) = &mut self.arbitrary_storage {
+            storage.cache_value(address, slot, value);
+        }
+    }
+
+    /// Returns a cached arbitrary-storage replay value for a slot.
+    pub fn cached_arbitrary_storage_value(&self, address: Address, slot: U256) -> Option<U256> {
+        self.arbitrary_storage.as_ref().and_then(|storage| storage.cached_value(address, slot))
+    }
+
     /// Whether the given address has arbitrary storage.
     pub fn has_arbitrary_storage(&self, address: &Address) -> bool {
         match &self.arbitrary_storage {
@@ -2535,7 +2619,9 @@ impl<FEN: FoundryEvmNetwork> Cheatcodes<FEN> {
             || self.should_overwrite_arbitrary_storage(&target_address, key)
         {
             if self.has_arbitrary_storage(&target_address) {
-                let arbitrary_value = self.rng().random();
+                let arbitrary_value = self
+                    .cached_arbitrary_storage_value(target_address, key)
+                    .unwrap_or_else(|| self.rng().random());
                 self.arbitrary_storage.as_mut().unwrap().save(
                     ecx,
                     target_address,
@@ -3218,4 +3304,18 @@ mod tests {
         ));
         assert!(cheats.has_log_hooks());
     }
+
+    #[test]
+    fn arbitrary_storage_cache_value_routes_copied_targets_to_source() {
+        let mut storage = ArbitraryStorage::default();
+        let source = Address::repeat_byte(0x11);
+        let copied = Address::repeat_byte(0x22);
+        let slot = U256::from(7);
+
+        storage.mark_arbitrary(&source, false);
+        storage.mark_copy(&source, &copied);
+        storage.cache_value(copied, slot, U256::ZERO);
+
+        assert_eq!(storage.cached_value(source, slot), Some(U256::ZERO));
+    }
 }

crates/config/src/symbolic.rs

@@ -59,7 +59,8 @@ pub struct SymbolicConfig {
     /// Solver names or exact commands to race in parallel. Ignored when `solver_command` is set.
     #[serde(default, skip_serializing_if = "Vec::is_empty")]
     pub solver_portfolio: Vec<String>,
-    /// Optional timeout in seconds for solver-backed symbolic execution.
+    /// Optional SMT solver timeout in seconds. Also bounds wall-clock symbolic invariant
+    /// exploration before falling back to invariant fuzzing.
     pub timeout: Option<u32>,
     /// Halmos-compatible loop bound accepted by config and annotations.
     #[serde(default, rename = "loop", skip_serializing_if = "Option::is_none")]

crates/evm/evm/src/executors/invariant/error.rs

@@ -36,19 +36,17 @@ pub struct HandlerAssertionFailure {
 
 impl HandlerAssertionFailure {
     /// Builds a failure from a replayed sequence whose last call asserted.
-    pub fn from_replayed_sequence(
+    pub const fn from_replayed_sequence(
         call_sequence: Vec<BasicTxDetails>,
+        reverter: Address,
+        selector: Selector,
         edge_fingerprint: B256,
         revert_reason: String,
     ) -> Self {
-        let last = call_sequence.last().expect("replayed sequence is non-empty");
-        let reverter = last.call_details.target;
-        let selector_bytes: [u8; 4] =
-            last.call_details.calldata.get(..4).and_then(|s| s.try_into().ok()).unwrap_or_default();
         let original_sequence_len = call_sequence.len();
         Self {
             reverter,
-            selector: Selector::from(selector_bytes),
+            selector,
             call_sequence,
             original_sequence_len,
             revert_reason,

crates/evm/evm/src/executors/invariant/shrink.rs

@@ -213,6 +213,9 @@ pub struct CheckSequenceOutcome {
     pub calls_count: usize,
     pub reverts: usize,
     pub failure_site: Option<CheckSequenceFailureSite>,
+    /// Whether replay stopped on an assertion in a sequence call rather than a plain revert or
+    /// terminal invariant check.
+    pub sequence_assertion_failure: bool,
 }
 
 pub struct ShrunkSequence {
@@ -225,6 +228,8 @@ pub struct ShrunkSequence {
 #[derive(Debug)]
 pub struct HandlerReplayOutcome {
     pub anchor_asserted: bool,
+    pub reverter: Address,
+    pub selector: Selector,
     pub revert_reason: Option<String>,
     /// Normalized via `handler_edge_fingerprint` so callers can compare directly.
     pub anchor_fingerprint: B256,
@@ -711,6 +716,7 @@ pub fn check_sequence<FEN: FoundryEvmNetwork>(
                     calls_count: calls_executed,
                     reverts,
                     failure_site: Some(site),
+                    sequence_assertion_failure: true,
                 }));
             }
             if call_result.reverted && options.fail_on_revert {
@@ -722,6 +728,7 @@ pub fn check_sequence<FEN: FoundryEvmNetwork>(
                         calls_count: calls_executed,
                         reverts,
                         failure_site: None,
+                        sequence_assertion_failure: false,
                     }));
                 }
                 let site = sequence_call_failure_site(&calls[idx], &call_result);
@@ -732,6 +739,7 @@ pub fn check_sequence<FEN: FoundryEvmNetwork>(
                     calls_count: calls_executed,
                     reverts,
                     failure_site: Some(site),
+                    sequence_assertion_failure: false,
                 }));
             }
             Ok(ReplayDecision::Continue(call_result))
@@ -752,6 +760,7 @@ pub fn check_sequence<FEN: FoundryEvmNetwork>(
         calls_count: calls_executed,
         reverts,
         failure_site,
+        sequence_assertion_failure: false,
     })
 }
 
@@ -951,6 +960,8 @@ pub fn replay_handler_failure_sequence<FEN: FoundryEvmNetwork>(
     let Some(&anchor_idx) = sequence.last() else {
         return Ok(HandlerReplayOutcome {
             anchor_asserted: false,
+            reverter: Address::ZERO,
+            selector: Selector::ZERO,
             revert_reason: None,
             anchor_fingerprint: B256::ZERO,
         });
@@ -966,7 +977,7 @@ pub fn replay_handler_failure_sequence<FEN: FoundryEvmNetwork>(
             if idx == anchor_idx {
                 let snapshot = snapshot_edge_fingerprint(&call_result);
                 let anchor = &calls[anchor_idx];
-                let reverter = anchor.call_details.target;
+                let reverter = call_result.reverter.unwrap_or(anchor.call_details.target);
                 let selector_bytes: [u8; 4] = anchor
                     .call_details
                     .calldata
@@ -979,6 +990,8 @@ pub fn replay_handler_failure_sequence<FEN: FoundryEvmNetwork>(
                     if asserted { assertion_failure_reason(call_result, rd) } else { None };
                 return Ok(ReplayDecision::Stop(HandlerReplayOutcome {
                     anchor_asserted: asserted,
+                    reverter,
+                    selector,
                     revert_reason: reason,
                     anchor_fingerprint: fingerprint,
                 }));
@@ -987,6 +1000,8 @@ pub fn replay_handler_failure_sequence<FEN: FoundryEvmNetwork>(
                 // Pre-anchor assertion = different bug; reject.
                 return Ok(ReplayDecision::Stop(HandlerReplayOutcome {
                     anchor_asserted: false,
+                    reverter: Address::ZERO,
+                    selector: Selector::ZERO,
                     revert_reason: None,
                     anchor_fingerprint: B256::ZERO,
                 }));
@@ -997,6 +1012,8 @@ pub fn replay_handler_failure_sequence<FEN: FoundryEvmNetwork>(
 
     Ok(outcome.unwrap_or(HandlerReplayOutcome {
         anchor_asserted: false,
+        reverter: Address::ZERO,
+        selector: Selector::ZERO,
         revert_reason: None,
         anchor_fingerprint: B256::ZERO,
     }))

crates/evm/symbolic/README.md

@@ -315,6 +315,45 @@ set, generates symbolic arguments with the same ABI model used for stateless
 tests, preserves symbolic world state between calls, and replays a concrete
 sequence before reporting a counterexample.
 
+Some invariant harnesses deploy dependency contracts in `setUp`, then rely on
+those dependencies having satisfiable environment state during the campaign. For
+example, a lending invariant may call an ERC20 mock for balances and allowances,
+or an oracle mock for a price, without exposing target functions that write
+those values first. In that case the dependency storage remains the concrete
+state produced by `setUp`, and symbolic execution can only explore paths
+reachable from that concrete dependency state.
+
+Use Foundry's existing `vm.setArbitraryStorage(address)` cheatcode to mark those
+environment dependency contracts as symbolic storage targets:
+
+```solidity
+function setUp() public {
+    loanToken = new ERC20Mock();
+    collateralToken = new ERC20Mock();
+    oracle = new OracleMock();
+
+    vm.setArbitraryStorage(address(loanToken));
+    vm.setArbitraryStorage(address(collateralToken));
+    vm.setArbitraryStorage(address(oracle));
+
+    targetContract(address(this));
+}
+```
+
+If the harness imports a smaller Hevm interface that does not expose this
+cheatcode, declare a local interface with `setArbitraryStorage(address)` and
+cast it to `address(vm)`.
+
+Keep this scoped to external dependencies that model the environment, such as
+token balances, token allowances, and oracle prices. Do not blanket-mark the
+invariant harness or protocol state as arbitrary; that can create unreachable
+states and counterexamples that concrete replay rejects.
+
+Replay currently materializes only concrete storage slots observed during
+symbolic execution. Dependency storage keyed by symbolic calldata is still
+explored symbolically, but it can replay-filter to `Incomplete` or `mismatch`
+instead of a confirmed counterexample if the required slot is not concrete.
+
 ## Configuration
 
 The primary configuration path is native Foundry config.