feat: full static-call-context support in compiler correctness - #39
Merged
Conversation
Bump the yul-semantics pin to the HaltKind.staticViolation commit and handle the new halt kind in HaltMatch / resultOf (→ EVM Exception .StaticModeViolation) and the compile_correct_eval halt-kind analysis. Keeps the compiler building and axiom-clean against the updated source semantics; static-frame correctness proofs follow in the next commit. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
FrameOK no longer fixes permitStateMutation = true, so the correctness theorems now cover static (STATICCALL) frames in addition to ordinary ones. In a static frame every state-modifying built-in the source forbids halts with Exception .StaticModeViolation, matching the source's HaltKind.staticViolation. Local guarded ops (sstore, tstore, log0-log4, selfdestruct): opStep now cases on yst.env.static. The non-static branch reuses the existing normal step (deriving permitStateMutation = true from EnvMatch.static); the static branch fires the target's generic StepRunning.staticModeViolation gate via the new staticViolationStep / staticHaltStepGen helpers. Open-world ops: externalStaticHaltStep discharges the external static-halt branch of ahalt_sim. Value-bearing call / create / create2 halt via the dedicated StepRunning.callStatic / createStatic / create2Static rules; delegatecall / staticcall / gas never produce a relational halt. CALLCODE is the one genuine source/target mismatch: the source halts a value-bearing CALLCODE in a static frame with .staticViolation, but the target EVM semantics deliberately has no callcodeStatic rule (a self-transfer is a world-state no-op). FrameOK.perm is therefore weakened to `permitStateMutation = true ∨ CALLCODE byte ∉ code` — free (Or.inl rfl) for every ordinary frame, and only constraining a static frame to be CALLCODE-free. This strictly generalises the previous non-static-only theorem; ordinary-frame CALLCODE is unaffected. Theorem statements (compile_correct, compile_correct_withPayload, compile_correct_eval, compileObject_correct) are unchanged and still pin axioms [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Upstream yul-semantics (db5e072) no longer rejects a value-bearing CALLCODE in a static frame — the self-transfer is a world-state no-op, so it now matches EIP-214 / evm-semantics (which has no callcodeStatic rule). With the source/target mismatch gone, static CALLCODE simply proceeds like delegatecall/staticcall and never produces a relational halt. This removes the temporary carve-out entirely: - Bump yul-semantics rev to db5e072d4e5067b5f4f0d9833a811e71da984f57. - Drop the `perm` field from FrameOK (it no longer constrains permitStateMutation at all), and delete the `hf.perm` slot from the 36 tuple reconstructions in OpStep. - Route static CALLCODE through externalStaticHaltStep's never-halts group (contradiction from the impossible halt), alongside delegatecall/ staticcall/gas, instead of the FrameOK byte-exclusion. FrameOK now says nothing about permitStateMutation, so compile_correct and friends cover ordinary and static frames uniformly with no exception. Every built-in the source halts under static (sstore/tstore/log0-4/selfdestruct, value-call, create/create2) maps to a matching evm-semantics StaticModeViolation rule. Theorem statements unchanged; axioms stay [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Repoint from the PR #37 branch commit to the merged yul-semantics main (0b1a2c0), which contains HaltKind.staticViolation and the CALLCODE static-frame correction. Build green (8663 jobs); Checks.lean axiom guard unchanged ([propext, Classical.choice, Quot.sound]). 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:36
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.
Extends
compile_correct(and the object/eval variants) to cover static (STATICCALL) frames, closing the audit's finding #2 (the theorem previously requiredFrameOK.perm = permitStateMutation = true, i.e. non-static frames only).Stacked on powdr-labs/yul-semantics#37 (adds
HaltKind.staticViolationso static writes match the EVM'sStaticModeViolationinstead of being conflated withINVALID). The lakefile pins that branch commit; update the pin to the merged SHA before merging this.Increment 1 (this commit — landed, green)
staticViolationcommit.HaltKind.staticViolation → EVM Exception .StaticModeViolationinHaltMatch/resultOfand thecompile_correct_evalhalt analysis.Checks.leanaxiom guard unchanged (3 standard axioms).Increment 2 (in progress)
FrameOK.perm; derivepermitStateMutationper-op fromStateMatchand the source's static branch.static → StaticModeViolationhalt branch for each state-modifying op (sstore/tstore/log0–log4/selfdestruct, value-call/callcode,create/create2).compile_correct/compile_correct_withPayload/compile_correct_eval/compileObject_correctto both static parities.🤖 Generated with Claude Code