feat(symbolic): persist replayable counterexample artifacts

[mablr]

Description

Closes OSS-349

Adds symbolic counterexample artifacts that can be replayed independently from the original symbolic run. When forge test --symbolic confirms a counterexample, Forge writes a schema-versioned JSON artifact under the project cache and surfaces its path in JSON output and non-JSON test output.

Artifacts can be replayed with:

forge test --replay-symbolic-artifact <path>

Replay supports both single-call symbolic counterexamples and invariant/stateful sequence counterexamples.

What changed

• Persist confirmed symbolic counterexamples as foundry:symbolic.counterexample@v1 artifacts.
• Add --replay-symbolic-artifact <PATH> to reconstruct the target contract/test/path and replay the stored calls.
• Add normalized JSON references via counterexample_artifacts.
• Surface artifact paths in human output as warnings.
• Validate replay artifacts before execution, including schema header, empty calls, target/function matching, and single-call value constraints.
• Make replay CI-friendly:
  • still-reproducing counterexample fails
  • fixed counterexample passes
  • stale or ambiguous target fails
• Cover single-call, invariant sequence, replay skip, stale target, fixed bug, and schema behavior in tests.

PR Checklist

• Added Tests
• Added Documentation
• Breaking changes

[figtracer]

reviewed the replay paths and reproduced one config-drift edge case locally.

[grandizzy]

Please check findings below

[grandizzy]

🟡 non-blocking: sequence replay needs no solver, yet this enables symbolic mode globally for all replays. If enabling symbolic has side effects (solver validation, test discovery), prefer an explicit replay execution mode over flipping this flag.

[grandizzy]

🟡 non-blocking: run_tests now needs #[allow(clippy::too_many_arguments)] (also at L1296/L1335). Since replay_symbolic_artifact already lives in TestRunnerConfig, consider a RunTestsOptions struct instead of threading another positional arg.

[grandizzy]

🟡 non-blocking: the schema requires compact 0x hex for warp/roll/value, but the loader doesn't validate against the schema and Alloy's U256 deserializer may accept other forms — a schema-contract mismatch on input. Add a producer test that Some(U256::ZERO) serializes to "0x0" (schema allows 0x0, forbids leading-zero forms). Also note the external HTTPS $refs mean the offline test only checks ref existence, not real validation.

Re-reviewed after latest commits (2d56330): blockers 1, 2, and 4 are fixed and blocker 3 is mitigated. Dismissing in favor of an approval.

[grandizzy]

Re-reviewed after the latest commits. All four earlier blockers are resolved or mitigated:

• Single-call replay semantics (a3ffefe): now gates on replay.status == Confirmed, rejects warp/roll, uses call_raw + is_raw_call_success to mirror the original symbolic path, decodes the live revert reason (falling back to the artifact reason only when empty), and routes EvmError::Skip to single_skip. ✅
• check_sequence executed-call counts (96ea2e7): independent calls_executed counter replaces idx + 1/sequence.len(). ✅
• Artifact filename identity (415d8b5): 16-byte keccak over the full contract\0value\0kind identity, with a collision test. ✅
• Double replay_persisted_call_sequence: still executes twice, but the second pass now recomputes metrics for the (possibly changed) sequence returned by replay_error, so it's a minor efficiency follow-up rather than a correctness issue. ✅ (mitigated)

Most non-blocking items were also addressed: #[serde(deny_unknown_fields)] on the artifact structs, loader rejecting non-confirmed artifacts, a U256::ZERO compact-hex test, doc-comments scoping execute_tx/execute_tx_and_register_created to invariant replay, and the legacy singular counterexample_artifact field documented in favor of the plural.

Remaining nits are optional follow-ups: config.symbolic.enabled = true for sequence replay, the run_tests argument count, and true offline schema validation for the external $refs.

LGTM, nice work.