Repository navigation
Support of OPCODE BLOBBASEFEE , BLOBHASH and CLZ - #583
Open
HugoDowsers wants to merge 46 commits into
Open
HugoDowsers wants to merge 46 commits into
HugoDowsers wants to merge 46 commits into
Conversation
Contributor
|
Thank you so much for this! In the meantime, could you add some tests for these new opcode instructions, similar to the existing ones here: |
Author
|
I've added some regression tests about the new opcodes. I needed to change the evm version in the foundry.toml |
halmos assigned CREATE addresses from a counter (magic_address + n) and did not model account nonces at all. A contract that predicts its own deployment address therefore disagreed with the executor, which breaks every CREATE3 library: the proxy deploys somewhere the caller cannot find, the `codesize != 0` check fails and all paths revert (paths: 0). Exec now tracks nonces (1 for a newly created account per EIP-161, incremented by both CREATE and CREATE2 even when the creation fails), and new_address() routes the rlp encoding of [sender, nonce] through sha3_data(), which maps it to a magic address exactly like the 0xff-prefixed 85-byte preimage of CREATE2. Both sides of the prediction then land on the same address, whatever the order in which they are computed. Closes a16z#217
Now that nonces are modeled, expose foundry's nonce cheatcodes. Selectors taken from foundry's crates/cheatcodes/assets/cheatcodes.json. setNonce() refuses to lower a nonce, as in foundry, and points at setNonceUnsafe(); resetNonce() sets 0 for EOAs and 1 for accounts with code.
Covers the CREATE3 deployment pattern reported in a16z#217, direct prediction of `new C()` at nonces 1 and 2, and the four nonce cheatcodes.
Second console script pointing at the same entry point, so `halmos` keeps working. `--help` now shows the name the command was invoked with, and dolmos.toml is read before halmos.toml in the project root. Dowsers-only: never propose upstream.
Only `dolmos` is installed now. The python package keeps its upstream name `halmos`, so imports and rebases on upstream are unaffected; only the command disappears. Note: the docker smoke tests in .github/workflows still run `halmos --version` and will fail on this fork until they are updated.
pip list, pip uninstall and importlib.metadata now see `dolmos`, and --version reads the version from that distribution. Homepage points at the fork, with the upstream repository kept as a separate URL. The importable package stays src/halmos: `import halmos` is unchanged and rebases on upstream do not conflict over a renamed directory.
The precompile input size was passed to BitVecSorts in bytes instead of bits, so any symbolic call to SHA256, RIPEMD160 or MODEXP raised a z3 sort mismatch. - move the hashing and MODEXP models to a new precompiles module - evaluate concrete inputs exactly (hashlib, pow) - MODEXP: EIP-198 layout with zero-padded input, output on len(M) bytes, EIP-7823 input length cap; symbolic results are modeled with an uninterpreted function constrained by result < M, with exact handling of M == 0, E == 0, E == 1 and bases 0/1 - add tests/regression/test/Precompiles.t.sol
Both cheatcodes used to fail with "Unsupported cheat code". - new expectations module: per-frame expectations stored in CallContext, decoding of the 26 overloads, symbolic matching of revert data and logs - an expectation applies to the next call or creation of the frame (cheatcode and console calls are ignored); a call that reverts as expected is reported as successful with dummy return data, like foundry - expectRevert: raw data or Error(string) payload match, partial match, reverter address, count (0 = must not revert) - expectEmit: ordered match anywhere in the call tree, topic/data checks, emitter address, anonymous events, count - a frame that returns with a pending expectation fails the test - failing expectations fork a FailCheatcode path, so symbolic inputs yield counterexamples - add tests/regression/test/Expect.t.sol (35 tests); use expectCall as the example of an unsupported cheatcode in SvmCheatCode.t.sol
setUp() with more than one feasible successful path used to abort with "Multiple paths were found in setUp()". - setup() now returns every path that is not provably infeasible - all of them become the initial frontier states, so each regular test and each invariant test sequence is explored from every setup state; counterexamples include the symbolic values selecting the setup state - the invariant testing context (targets, senders, selectors) is read from the first setup state - the number of setup states is reported with -v - add tests/regression/test/SetupMulti.t.sol (regular, setUpSymbolic and invariant tests)
The optimizer (notably via-IR) may constant-fold keccak256(k . p) into a PUSH32 literal, e.g. in a constructor writing m[k] = v, while runtime code computes the same slot with SHA3. A concrete slot is decoded as (p, k) only once its keccak preimage is known, so the first write was stored under the raw slot and the later read under (p, k): the value was lost and a false counterexample reported. When a structured access is resolved from a concrete slot, a value stored under the raw slot is now moved to the structured location first (solidity layout), or copied once (generic layout). StorageSlot.t.sol::check_keccak_slot_2_fail, which documented this limitation, now passes and is renamed accordingly.
- the whole balance is sent to the beneficiary, and the frame halts successfully with empty return data; - WriteInStaticContext in a static context; - the account (code, storage, balance, nonce) is deleted at the end of the transaction only if it was created in that transaction; the deletions are propagated through CallOutput.accounts_to_delete on success and dropped on revert. Accounts created in the current transaction are tracked in Exec.created_in_tx, reset by SEVM.run(). UnsupportedOpcode.t.sol now relies on an undefined opcode (0x0c) instead of selfdestruct, and StaticContexts.t.sol::check_selfdestruct_fails is enabled.
keccak256 is modeled as uninterpreted functions, so a model may assign to a symbolic preimage a hash that differs from the real keccak256, yielding counterexamples that do not replay (e.g. amt = 0 hashing to a storage key written in setUp). When the query is sat, the preimages of the symbolic keccak terms are read from the model (through definitional sha3arg_* constants, neutral for unsat cores), and the facts f_sha3_N(v) == keccak256(v) are added before solving again. These facts hold for the real hash function, so no real counterexample is lost, and unsat proves that none exists under the usual keccak assumptions. After --keccak-refinement-rounds rounds (default 3), a model that still disagrees is reported as potentially invalid. Unsat cores of refined queries are not cached, as they may depend on the unnamed facts.
The EVM version (hard fork) determines: - the available opcodes: an opcode introduced after the selected fork halts the current frame with InvalidOpcode, as on a node running that fork (DELEGATECALL, REVERT/RETURNDATA*/STATICCALL, shifts/CREATE2/ EXTCODEHASH, CHAINID/SELFBALANCE, BASEFEE, PUSH0, TLOAD/TSTORE/MCOPY/ BLOBHASH/BLOBBASEFEE, CLZ); - the semantics of SELFDESTRUCT: before Cancun, the account is deleted at the end of the transaction even if it was not created in it (EIP-6780 from Cancun). The option can be given on the command line, in dolmos.toml, or in @Custom:dolmos annotations. When not given, the evmVersion found in the compiler metadata of the test contract (foundry's evm_version) is used, or the latest supported fork (osaka). With the latest fork, the opcode check is skipped entirely, so the default behavior and performance are unchanged. Not modeled yet: fork-dependent precompiles and gas rules.
…terexample when refinement is undecided
…s (halmos#280, a16z#369, a16z#398, a16z#419) With -pcex, counterexamples are printed so that they can be acted upon: - test arguments decoded with the ABI of the test: lengths of dynamic arrays, bytes and strings applied, values rendered by type (decimal with hints such as 1e18 or 2**255, checksummed addresses with the contract and test variable behind them, strings) - bytes holding calldata decoded with the ABIs of the compiled contracts, and calls made with calldata built by svm.createCalldata listed (halmos#369) - bytes4 values rendered as selectors, 0x00000000 as the empty selector of plain ether transfers (halmos#419) - invariant call sequences with concrete senders, values, arguments and timestamps - a forge test replaying each counterexample: typed calls through `this` and through the state variables of the test holding the targets, low-level calls otherwise - duplicate counterexamples hidden and counted (halmos#398) - potentially invalid counterexamples relying on the EXP abstraction checked against the real exponentiation: constant exponents expanded by square and multiply, constant bases tabulated, real values added at the operands of the model, up to 3 rounds (keccak values checked in the same loop). The counterexample is then valid, proven spurious (unsat), or reported with the reason (halmos#280) Also fixes --early-exit, which reported the queries cancelled after the first counterexample as solver errors and saved them as failed queries (halmos#398). Without the option, the output is unchanged. Verdicts and model counts are the same with and without it on tests/regression, except for counterexamples proven spurious. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FT71T6kg8kz9yamjguBUb8
… storage layout, CRLF fixtures on Windows
- test(fs): portable absolute paths in test_fs (Windows CI) - fs: case-insensitive fs_permissions matching on Windows (normcase) - ci: checkout v6, setup-python v6, setup-uv v7, login-action v4, upload-artifact v6, download-artifact v7 - ci: run pre-commit directly (pre-commit/action uses actions/cache@v4, node20)
…nfig output; ci: annotate failed tests - config: split_command does not treat backslashes as escapes on Windows (shlex.split mangled C:\...\yices-smt2.exe), with tests - test_pcex: pass the yices command with shlex.join - fs: decode forge config output as utf-8 (the locale encoding is not utf-8 on Windows) - ci: report failed tests as annotations on the run page, summary with -rfE - changelog
- only install geas for sys-asm-halmos (the only project using it) - pin geas to v0.3.3 - force HTTP/1.1, fall back to direct fetch on any proxy error, retry 3x
`uv run --with pytest-github-actions-annotate-failures` runs pytest in an overlay environment (VIRTUAL_ENV and sys.prefix point to it), so on Windows dolmos no longer finds z3.exe, installed by z3-solver in .venv\bin (not on PATH, unlike .venv\Scripts): --solver z3 failed with "No download URL for solver.name='z3'" (test_solver_resolution_precedence, and the z3-annotated StdAssert tests in test_main[tests/regression]). pytest-github-actions-annotate-failures moves to the dev extras, and pytest runs with a plain `uv run`, as before ce0a4c3. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MAM31oUC1SLbTkc6DYWCio
|
Review the following changes in direct dependencies. Learn more about Socket for GitHub.
|
This branch has not been deployed
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
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.
This PR adds symbolic execution support for three EVM opcodes that were previously unhandled by Halmos, causing verification failures on contracts that use them.