feat: add native symbolic testing#14796
Draft
mattsse wants to merge 11 commits into
Draft
Conversation
* test(symbolic): add fuzzer/standard-lib parity tests Adds 23 CI-bounded symbolic-execution parity tests against canonical benchmark corpora (Echidna, Medusa, ItyFuzz, devdacian, crytic/properties, Halmos examples, OpenZeppelin patterns) plus engine-capability checks for new opcodes. All tests gated on z3_available(); total wall ~43s in parallel. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): convert parity tests to snapbox snapshots Replaces `stdout_lossy() + contains()` assertions with `stdout_eq(str![[...]])` snapshots for all 23 symbolic parity tests. - Adds two helpers in the test module: - `assert_symbolic` redacts `[METRICS]` (paths/queries counts) and `[SENDER]` (symbolic invariant sender addresses). - `assert_symbolic_witness` adds `[CALLDATA]` and `[ARGS]` (with one level of nested scientific-notation brackets) for tests whose counterexample witnesses Z3 chooses freely. - Uses `sh_eprintln` in `skip_unless_z3!` to satisfy the disallowed-macro clippy lint. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): trim parity snapshots with ellipsis wildcards Replaces the repeated compile-header and pre-"Failing tests:" duplicated counterexample line in each snapshot with a single `...` multi-line wildcard from snapbox. Passing tests keep just `Ran 1 test for ...` and the `[PASS] ...` line; failing tests keep from `Failing tests:` to the `forge test --rerun` tip. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): split parity corpora * test(symbolic): align kevm snapshot with trim convention The split-out kevm test ended the snapshot at `Suite result: ok. ...; finished in [..]`, but the global `[ELAPSED]` redaction rewrites `finished in <n>s` to literal `[ELAPSED]`, so the assertion never matched. Replace the trailing line with the same `...` multi-line wildcard the other parity snapshots use. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): consolidate parity tests under symbolic_parity/ mod - Move the 12 `symbolic_parity_*.rs` files into a `symbolic_parity/` subdirectory with a single `mod symbolic_parity` registration. Mirrors the existing `invariant/` layout. - Re-export `assert_symbolic` and `assert_symbolic_witness` from `symbolic_parity::mod` so corpus submodules can `use super::*` instead of reaching into `crate::test_cmd::symbolic_helpers`. - Add the missing snapshot assertions for hevm, manticore, scribble, and swc. These were checking only the failure exit code; now they assert the trimmed snapbox snapshot the rest of the corpus uses. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): make manticore parity test actually exercise the engine The previous snapshot showed: [FAIL: failed to set up invariant testing environment: No contracts to fuzz.] That's a wiring bug, not a real `Manticore`-style multi-tx exploration: the test contract held both `arm()` and `invariant_neverArmed()` in the same contract, didn't inherit `forge-std/Test`, and had no `setUp` / `targetContract` call, so the invariant runner had no fuzzable target. Split the target out into a separate `ArmTarget` contract and register it via `targetContract`. The engine now actually shrinks the symbolic sequence to a single `arm(0xfeed)` call. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): align parity tests with upstream challenges - devdacian rarely-false: port to canonical (n + 1234) % 2**80 == 0 - halmos minivat: rename trivial test to linear_smoke_parity and add canonical Fundamental Equation of DAI invariant as ignored regression (engine gap: nonlinear bv-mul symbolic*symbolic) - erc20 approve race: tighten comment to reflect hardcoded sequence Co-authored-by: grandizzy <38490174+grandizzy@users.noreply.github.com> Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * Update crates/forge/tests/cli/test_cmd/symbolic_parity/halmos.rs Co-authored-by: figtracer <me@figtracer.com> --------- Co-authored-by: Amp <amp@ampcode.com> Co-authored-by: Derek <256792747+decofe@users.noreply.github.com> Co-authored-by: figtracer <me@figtracer.com>
Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com>
* feat(symbolic): support SMT solver selection * fix: address grandizzy's comments * fix: improve symbolic solver portfolio performance * fix(symbolic): validate portfolio solver choices Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): avoid impossible mapping storage aliases Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * chore(symbolic): remove local solver version aliases Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * chore(symbolic): drop versioned solver aliases Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): snapshot erc20 storage regression Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> --------- Co-authored-by: Amp <amp@ampcode.com>
* chore(symbolic): share builtin solver registry Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): report portfolio solver outcomes Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): warn on degraded solver portfolios Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * chore(symbolic): fix portfolio diagnostics clippy Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * docs(symbolic): document solver portfolio helpers --------- Co-authored-by: Amp <amp@ampcode.com>
Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What changed
Adds Foundry-owned native symbolic testing behind
forge test --symbolic.This introduces a new
foundry-evm-symboliccrate with a standalone symbolic EVM, Z3-backed solving, symbolic ABI input generation, byte-precise calldata/memory/returndata, symbolic storage and keccak support, multi-frame calls, creation, cheatcode handling, invariant sequence execution, and concrete replay before counterexamples are reported.The Forge runner now discovers
check*/prove*tests for stateless symbolic execution andinvariant*/statefulFuzz*tests for bounded symbolic sequence execution when symbolic mode is enabled. Symbolic configuration is available through[profile.*.symbolic], CLI/env overrides, and nativeforge-config:inline settings, with compatibility translation for@custom:halmosannotations.Why
This gives Forge a native path for symbolic testing without requiring a separate external runner, while still preserving normal Forge setup, compilation, test selection, result formatting, and replay semantics.
Impact
Users can write ordinary Forge-style Solidity tests and run them symbolically with
forge test --symbolic. Dynamic ABI bounds, solver limits, invariant depth, symbolic call targeting, SMT dumping, and storage layout mode are configurable through Foundry config. Unsupported symbolic constructs are reported as incomplete/stuck rather than silently treated as proven.