fix(symbolic): explore stateful invariant paths

[figtracer]

Description

This improves symbolic invariant execution for stateful Morpho-style paths. It lets bounded symbolic invariant exploration continue through multi-call sequences, replays setup-time arbitrary-storage values for explicit symbolic-storage targets, and completes hard-arithmetic fallback models with the supporting storage values needed by checked ERC20-style arithmetic guards.

• The Morpho canary needs a supply -> supplyCollateral -> borrow sequence. On GalloDaSballo/morpho-foundry-fv@example-concrete-fallback, the clean harness pins the market/token/oracle addresses, but it does not provide a concrete target path that funds/approves tokens or sets an oracle price. Normal invariant fuzzing confirms that boundary: invariant_hasBorrowed passed after 256 runs with all 128000 target calls reverting.
• Plain forge test --symbolic on the same repro reaches the relevant shape but stops incomplete after 26 paths with hard arithmetic heuristic witness used; no replayed counterexample found.
• With the dependency boundary made explicit by marking loanToken, collateralToken, and oracle as arbitrary storage, this PR finds and replays the 3-call supply -> supplyCollateral -> borrow counterexample (paths: 177, models: 1, hard-arith: 84 in a fresh run).

Current workaround: explicit dependency storage boundary:

• Use the existing Foundry vm.setArbitraryStorage(address) when a symbolic invariant depends on setup-deployed dependency contracts whose storage must be satisfiable, but no target call in the invariant campaign writes that storage. In the Morpho repro, that means the ERC20 token mocks and oracle mock:

interface ArbitraryStorageVm {
    function setArbitraryStorage(address target) external;
}

ArbitraryStorageVm(address(vm)).setArbitraryStorage(address(loanToken));
ArbitraryStorageVm(address(vm)).setArbitraryStorage(address(collateralToken));
ArbitraryStorageVm(address(vm)).setArbitraryStorage(address(oracle));

• Keep this scoped to external dependencies that model the environment, such as token balances/allowances and oracle prices. Do not blanket-mark the invariant harness or protocol state as arbitrary; that can produce unreachable counterexamples that do not replay.
• This cheatcode annotation is the current workaround for dependency/environment storage. The desired UX is hybrid invariant exploration that learns reachable frontier states without requiring users to add these annotations.

What this intentionally does not do:

• It does not make all setup storage arbitrary. On the same repro, --symbolic-storage-layout generic produces a 2-path counterexample that does not replay because it also makes harness/protocol state arbitrary. That is too broad for this class of invariant test.
• It does not add another user-facing modeling cheatcode. The longer-term UX should be an Echidna-style hybrid worker: normal invariant fuzzing builds or loads reachable corpus/frontier states, symbolic execution extends those states, and confirmed counterexamples feed back into the corpus/replay flow.

Status quo

• Halmos has the same explicit symbolic-storage boundary (svm.enableSymbolicStorage / Foundry vm.setArbitraryStorage), so it is not a better no-annotation UX for this case.
• Echidna symExec is the product direction to pursue: symbolic execution is an additional exploration worker over the same campaign/tests. A local Echidna run on this repo did not get to the property because HEVM rejected a Foundry deployment cheatcode in the harness, but the model is still the right UX shape.
• Certora Morpho specs also make the boundary explicit: they use a dedicated MorphoHarness, require assumptions, extSloads => NONDET, _.price() => CONSTANT, and envfree getters instead of asking the prover to infer arbitrary dependency storage.

[mablr]

Looks good, just one question

[grandizzy]

Found three remaining soundness gaps that can report confirmed symbolic invariant failures outside the concrete campaign semantics. Details and suggested changes inline.

[mablr]

This restores the pre-call PathState, but concrete top-level reverts retain non-journaled effects such as vm.mockCall and vm.warp. A reverting handler can therefore affect the next concrete call while symbolic execution drops that effect and may report Safe.

[mablr]

This storage is keyed only by handler site, but the following fuzz campaign can replace the seeded symbolic failure with a shorter sequence at the same site. We then attach stale storage to a different sequence and persist it as replay-confirmed.

[grandizzy]

One replay-integrity issue remains after the latest fix: fresh symbolic artifacts now record an exact SymbolicInvariantFailureSite, but artifacts with site: None still use broad matching, and the persisted-failure replay path drops failure_site and emits new site: None artifacts.

That means a stale artifact can still be accepted when the original predicate no longer fails but the same sequence fails in afterInvariant, at another invariant edge, or through fail_on_revert.

The persisted replay should validate and preserve the concrete failure site, and artifact replay should reject missing site metadata as unverifiable. Proposed diff: #15591 (comment)

[grandizzy]

lgtm

[mablr]

I think these previous comments are not fully addressed:

#15591 (comment)
#15591 (comment)
#15591 (comment)

Unsure we need to block on them, but i wanted to pin them at least for follow-up.

[mablr]

LGTM

[grandizzy]

lgtm