feat(symbolic): support symbolic vm.deal values#14952
Merged
figtracer merged 1 commit intoMay 28, 2026
Merged
Conversation
figtracer
requested review from
0xrusowsky,
DaniPopes,
grandizzy,
mablr,
mattsse and
stevencartavia
as code owners
Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d
figtracer
force-pushed
the
fig/symbolic-deal-value
branch
from
0628250 to
d140227
Compare
figtracer
changed the title
vm.deal values
grandizzy
added a commit
that referenced
this pull request
Jun 8, 2026
* feat: add native symbolic testing * fix: satisfy symbolic clippy lints * fix: set symbolic counterexample value * fix: narrow symbolic test classification * test(symbolic): add fuzzer/standard-lib parity tests (#14809) * 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> * refactor(symbolic): split executor into modules (#14825) Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): add named dynamic ABI bounds (#14814) * feat(symbolic): add solver selection plumbing (#14835) * 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> * feat(symbolic): add portfolio solver diagnostics (#14846) * 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> * feat(symbolic): stage portfolio solver launches (#14847) Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): summarize portfolio diagnostics (#14849) * feat(symbolic): summarize portfolio diagnostics Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * Address symbolic portfolio diagnostics review Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Fix transaction request clippy warning Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Revert "Fix transaction request clippy warning" This reverts commit 884799d. * Allow transaction request enum size lint Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Disambiguate portfolio diagnostics re-export Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Use enum for solver outcomes Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> --------- Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): defer diagnostics during progress output (#14861) Defer symbolic diagnostics during progress output Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): show query progress (#14862) Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): adapt portfolio scheduling (#14864) * feat(symbolic): adapt portfolio scheduling Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): tighten adaptive portfolio scoring Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * refactor(symbolic): name portfolio scheduler signals Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): clarify query progress limit Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 --------- Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): configure exploration order (#14869) * feat(symbolic): configure exploration order Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): default exploration order when omitted Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): apply exploration order to local batches Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> --------- Co-authored-by: Amp <amp@ampcode.com> * refactor(symbolic): consolidate constants into a `consts` module (#14880) Promotes scattered magic numbers and named constants spread across executor.rs, solver.rs, evm.rs, memory.rs, state.rs and precompiles.rs into a single `crates/evm/symbolic/src/consts.rs` module. All previous call-sites pick the constants up through the existing use `super::*` / `pub(crate) use consts::*` re-export chain, so no public API changes. * refactor(symbolic): split symbolic test file by feature (#14881) * refactor(symbolic): consolidate constants into a `consts` module Promotes scattered magic numbers and named constants spread across executor.rs, solver.rs, evm.rs, memory.rs, state.rs and precompiles.rs into a single `crates/evm/symbolic/src/consts.rs` module. All previous call-sites pick the constants up through the existing use `super::*` / `pub(crate) use consts::*` re-export chain, so no public API changes. * refactor(symbolic): split symbolic test file by feature Splits the monolithic symbolic.rs (~7800 lines, ~150 tests) into focused files grouped by the EVM feature they exercise: - symbolic.rs: basic flags, core behavior, arrays, invariants - symbolic_opcodes.rs: byte/signextend, shift, exp - symbolic_memory.rs: mload/mstore/sha3/log/returndatacopy/mcopy - symbolic_calls.rs: calldataload/copy, external/static/delegate/callcode - symbolic_creates.rs: create, create2, nonce, vm.expectCreate - symbolic_storage.rs: mapping, packed, ERC-20 storage, svm helpers - symbolic_precompiles.rs: hash, identity, advanced precompile coverage - symbolic_cheatcodes.rs: all vm.* cheatcode tests No test logic changes; all symbolic CLI tests are preserved. --------- Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): harden soundness fallbacks (#14877) Co-authored-by: Amp <amp@ampcode.com> Co-authored-by: Mablr <59505383+mablr@users.noreply.github.com> * refactor(symbolic): split executor into modules (#14879) * refactor(symbolic): split executor into modules Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * ci: skip tempo network checks without rpc secrets Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Revert "ci: skip tempo network checks without rpc secrets" This reverts commit af8e942. --------- Co-authored-by: Amp <amp@ampcode.com> * refactor(symbolic): replace `String` errors in solver config with `enum` (#14898) Introduces `SolverConfigError` with `EmptyCommand` and `UnterminatedQuote(char)` variants, replacing all `Result<T, String>` in the solver command-building path. Also tightens `split_quoted_args` to return the offending `char` directly instead of a pre-formatted string, letting callers own the message context. * fix: stabilize symbolic CI tests (#14900) * test: snapshot symbolic CLI output checks (#14903) * test: snapshot symbolic CLI output checks * fix: satisfy clippy on symbolic test branch * Update crates/forge/tests/cli/test_cmd/symbolic_helpers.rs Co-authored-by: Mablr <59505383+mablr@users.noreply.github.com> --------- Co-authored-by: grandizzy <38490174+grandizzy@users.noreply.github.com> Co-authored-by: Mablr <59505383+mablr@users.noreply.github.com> * feat(symbolic): add tracing to executor and solver (#14904) * feat(symbolic): add tracing to executor and solver Spans added: - `symbolic_path` (`completed_paths`, `worklist_size`): wraps each worklist iteration in `run.rs` - `symbolic_step` (`pc`, `op`): wraps each `step()` call, nested under `symbolic_path` - `jumpi_branch` (`pc`, `dest`): wraps the symbolic `JUMPI` fork block in `opcodes.rs` - `solver_query` (`query_id`, `constraint_count`, `kind`): wraps `is_sat`/`model` calls in `solver.rs` Events added: - trace per path pop and per solver query entry - debug at path/depth limit exhaustion and final safe/revert-all outcome - debug before counterexample model materialization - debug (with `constraint_count`) on invalid solver model * fix: add missing tracing spans to `execute_sequence_call` * refactor(common): extract wallet helpers (#14906) * refactor(common): extract wallet helpers Move `derive_key_path`, `derive_private_key<W>`, `derive_private_key_with_language`, and `private_key_from_u256` from `foundry-evm-symbolic` into `foundry-common` so that both `foundry-cheatcodes` and `foundry-evm-symbolic` share a single impl. * fix: enable `mnemonic-all-languages` * test(symbolic): stabilize cheatcode expectations (#14910) Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): normalize hard arithmetic queries (#14901) * feat(symbolic): normalize hard arithmetic queries Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 * fix(symbolic): address hard arithmetic review Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * style(symbolic): fix nightly rustfmt import order Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): stabilize fake portfolio solvers Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> --------- Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): cache satisfiability queries (#14917) Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): cache solver models (#14921) feat(symbolic): expose solver telemetry Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): avoid cache hits in scheduler tests (#14935) Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): add soundness regression tests (#14936) * test(symbolic): regress default-layout unwritten mapping SLOAD Pins that a symbolic-key read of an unwritten mapping yields a fresh symbolic value under the default storage layout, complementing the existing generic-layout coverage. * test(symbolic): regress transient storage clear between invariant steps Pins that EIP-1153 transient storage is cleared at the boundary of every top-level symbolic invariant sequence step, so a prior step's TSTORE is not observable from the next step. * test(symbolic): regress revert-branch exploration under fail_on_revert Pins that with fail_on_revert=false, the symbolic invariant runner keeps exploring non-reverting symbolic branches of a target whose other branches revert, instead of silently under-approximating and missing bugs. * test(symbolic): regress GAS/gasleft bound and pin Unsupported gap Pins that the GAS opcode is bounded by the transaction gas limit rather than silently returning U256::MAX, and records an ignored regression that gasleft-dependent branches should fail closed as Unsupported instead of emitting phantom non-replaying counterexamples. * test(symbolic): regress dynamic memory read epoch ordering Pins that a symbolic-offset MLOAD respects write-epoch ordering: when a later concrete MSTORE has written to an offset, a subsequent dynamic read that aliases that offset must see the later concrete value, not the stale earlier symbolic write. * test(symbolic): regress overlay code lookup across invariant steps Pins that top-level invariant sequence calls resolve account code through the symbolic world overlay so prior-step vm.etch effects are visible at the next step, instead of bypassing to the backend and silently missing the mutation. * test(symbolic): regress CREATE with symbolic runtime size fails closed Pins that a constructor returning a symbolic-length runtime image is reported as unsupported symbolic execution rather than silently installed as max-length padded bytecode, which would corrupt EXTCODESIZE and later selector dispatch. * test(symbolic): regress vm.prank delegatecall overload fails closed Pins that the vm.prank(address,bool) and vm.prank(address,address,bool) overloads with delegateCall=true are reported as unsupported symbolic execution instead of silently behaving like the plain address-only overloads. * test(symbolic): pin Keccak-heuristic surfacing gap Adds an ignored regression that pins the plan goal: results that depend on heuristic Keccak modeling must surface explicit Keccak/SHA3 vocabulary (Incomplete or warning), instead of either passing silently or surfacing a generic solver-error Incomplete with no Keccak attribution. * style(symbolic): rustfmt * fix(symbolic): report non-replaying counterexamples as incomplete (#14937) Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): fail closed on gasleft (#14939) Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): surface Keccak heuristic in incomplete results (#14940) Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * docs(symbolic): document preview result semantics (#14941) Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): allow GAS as call operand (#14942) feat(symbolic): allow gas as call operand Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): support symbolic `vm.deal` values (#14952) feat(symbolic): support symbolic vm.deal values Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * docs(symbolic): document known incomplete surfaces Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * docs(symbolic): clarify bounded preview gaps Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): fail closed on false-pass surfaces Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): fail closed on validity-sensitive helpers (#15024) Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com> * test: update default config snapshot * fix: make clippy happy * perf(symbolic): improve solver query handling (#15065) * try validated hard-arithmetic fallback before SMT for satisfiable is_sat queries Result: {"status":"keep","metric":1208,"build_ms":3751,"counterexample_lines":8,"run1_ms":4219,"run2_ms":1208,"run3_ms":1196,"total_wall_ms":6677,"total_ms":1208} * fold constant BoolExpr comparisons during construction Result: {"status":"keep","metric":1187,"build_ms":3527,"counterexample_lines":8,"run1_ms":4476,"run2_ms":1187,"run3_ms":1182,"total_wall_ms":6894,"total_ms":1187} * preallocate SMT query buffer based on constraint count Result: {"status":"keep","metric":1178,"build_ms":3255,"counterexample_lines":8,"run1_ms":4767,"run2_ms":1178,"run3_ms":1171,"total_wall_ms":7166,"total_ms":1178} * preallocate normalized solver cache-key vector Result: {"status":"keep","metric":1175,"build_ms":4637,"counterexample_lines":8,"run1_ms":4918,"run2_ms":1174,"run3_ms":1175,"total_wall_ms":7317,"total_ms":1175} * normalize solver constraint batches by flattening and deduplicating top-level conjuncts Result: {"status":"keep","total_ms":1190,"build_ms":8581,"counterexample_lines":8,"run1_ms":4718,"run2_ms":1180,"run3_ms":1190,"total_wall_ms":7140,"min_ms":1180,"mean_ms":2363,"max_ms":4718,"symbolic_paths":31,"symbolic_queries":48,"symbolic_smt_queries":48,"symbolic_sat_queries":50,"symbolic_sat_cache_hits":6,"symbolic_model_queries":4,"symbolic_model_cache_hits":0,"symbolic_hard_arith_witnesses":0,"symbolic_solver_ms":714} * Simplify repeated symbolic AND masks * fix(forge): run symbolic-only check tests * short-circuit direct symbolic contradictions before SMT * reuse validated symbolic solver cache results * fix symbolic solver fallback review issues * perf(symbolic): reduce solver work for guarded division checks (#15074) perf(symbolic): normalize guarded self-division checks * perf(symbolic): reduce solver work with path-bounded arithmetic guards (#15079) perf(symbolic): use path bounds for checked mul guards * perf(symbolic): reduce solver queries with witnesses and exact folds (#15082) * perf(symbolic): try hard-arithmetic sat witnesses before SMT * perf(symbolic): fold exact comparison identities --------- Co-authored-by: grandizzy <38490174+grandizzy@users.noreply.github.com> Co-authored-by: Derek <256792747+decofe@users.noreply.github.com> Co-authored-by: Amp <amp@ampcode.com> Co-authored-by: figtracer <me@figtracer.com> Co-authored-by: Mablr <59505383+mablr@users.noreply.github.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
2 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.
Summary
vm.deal(address,uint256)to store symbolic balance values instead of requiring the amount to be concrete/constrainedGAScannot leak into world-state balancesWhy
vm.dealis balance assignment, and the symbolic world already supports symbolicBALANCEreads, symbolic transfer arithmetic, and solver-backed value-transfer solvency checks. Requiring the deal amount to be concrete was overly conservative and blocked useful tests before they reached the property under test.This keeps the model bounded: it supports symbolic balance/value-transfer semantics, but does not claim full account-existence path splitting for
amount == 0vsamount != 0or gas-derived balance semantics.Generic coverage
This is not special-cased for a bug-suite contract. The regressions cover the general balance semantics:
vm.dealbalance can be read back throughBALANCEgasleft()and derivedgasleft() + 1deal values fail closedBug-suite check
Against
grandizzy/symbolic-bug-suite, the previous remaining targeted blocker after #14942 was TheDAO stopping onsymbolic vm.deal value. With this PR:So the test now reaches a real counterexample instead of an unsupported symbolic
vm.dealvalue.