fix: distinguish static-mode violations from INVALID (HaltKind.staticViolation) - #37
Merged
Merged
Conversation
…tion) State-modifying built-ins attempted in a static frame previously halted with `HaltKind.invalid`, conflating them with the INVALID opcode. The EVM raises a dedicated `StaticModeViolation` exception on this path, so a Yul→EVM compiler proved against this semantics could not match the exact exception for static-context writes. Add a distinct `HaltKind.staticViolation` and route every static write-protection halt to it (`guardStatic` for sstore/tstore/log0-4/selfdestruct; the value-`call`/`callcode` and `create`/`create2` branches of `builtinWithExternal`). Classify it non-committing in `HaltKind.commits`. The genuine INVALID opcode is unchanged. Guards, examples, and docs updated. lake build green (8576 jobs); runLinter clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A value-bearing `callcode` transfers value from the executing account to itself (callcode runs the target's code in the current account's context), which is a no-op on world state. Per EIP-214 and the EVM (geth has no static gate on CALLCODE; the pinned evm-semantics likewise has no `callcodeStatic` rule), it is NOT rejected in a static frame — unlike a value-bearing `call`. The previous static guard on `callcode` was an over-restriction: it made the Yul semantics diverge from the EVM (a Yul→EVM compiler cannot match a nonexistent target rejection). Remove it so `callcode` behaves like `delegatecall`/`staticcall` under static context. `call` (which transfers to another account) stays rejected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
leonardoalt
marked this pull request as ready for review
July 16, 2026 12:34
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
1 participant
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.
Why
State-modifying built-ins attempted in a static frame (
env.static = true) halted withHaltKind.invalid, conflating them with theINVALIDopcode. The EVM raises a dedicatedStaticModeViolationexception on this path, so a Yul→EVM compiler proved against this semantics cannot match the exact exception for static-context writes — it blocks extending compiler correctness to static (STATICCALL) frames.What
HaltKind.staticViolation, distinct frominvalid.guardStatic(coverssstore/tstore/log0–log4/selfdestruct) and the value-bearingcall/callcodeandcreate/create2branches ofbuiltinWithExternal.HaltKind.commits(a static violation reverts the frame).INVALIDopcode is unchanged;opName/parse/effectsuntouched.DESIGN.md,Observation.lean) updated.Checks
lake buildgreen (8576 jobs);lake exe runLinter YulSemanticsclean. This is a prerequisite for full static-context support in theyul-compilercorrectness theorem (a companion PR pins this commit).🤖 Generated with Claude Code