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

[mablr]

Looks good overall.

I left 3 non-blocking suggestions, but can be handled later in follow-up as the PR is already big.