refactor: extract IRState.withTx and YulTransaction.ofIR helpers#1733
Merged
refactor: extract IRState.withTx and YulTransaction.ofIR helpers#1733
Conversation
Replace 37 inline occurrences of the 9-line transaction-context record update pattern with two @[reducible] helpers: - IRState.withTx: copies transaction fields into an IR state - YulTransaction.ofIR: converts IR transactions to Yul transactions Both helpers include @[simp] lemmas (sender, storage, events) so existing proofs work unchanged. Net reduction: 153 lines. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Th0rgal
pushed a commit
that referenced
this pull request
Apr 16, 2026
Pick up YulTransaction.ofIR_sender/ofIR_args from #1733. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Th0rgal
pushed a commit
that referenced
this pull request
Apr 16, 2026
…bridge Merge origin/main to pick up: - refactor: extract IRState.withTx and YulTransaction.ofIR helpers (#1733) - fix: link to the paper Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.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
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.
Summary
IRState.withTxhelper that applies transaction context fields (sender, msgValue, etc.) to an IR state, replacing 37 inline occurrences of the 9-line record update patternYulTransaction.ofIRhelper that converts IR transactions to Yul transactions, eliminating duplicate field-copying boilerplate@[reducible]with@[simp]lemmas so existing proofs work unchangedMotivation
The paper listings for EthRes 2026 include theorem signatures from these files. The inline record updates made the theorems difficult to read both in code and in the paper. These helpers make the proof signatures self-documenting.
Test plan
lake build Compiler.Proofs.YulGeneration.Equivalencepasseslake build Compiler.Proofs.YulGeneration.Preservationpasses (pre-existing simp warnings only)lake build Compiler.Proofs.EndToEndpasses🤖 Generated with Claude Code
Note
Low Risk
Mechanical refactor of proof/semantic glue code; main risk is unintended rewriting/simp changes that could subtly affect proof obligations, but runtime semantics are unchanged.
Overview
Refactors the IR→Yul proof stack to eliminate repeated transaction-field record construction by introducing
IRState.withTx(applyIRTransactioncontext onto anIRState) andYulTransaction.ofIR(convertIRTransactiontoYulTransaction) with supportingsimplemmas.Updates end-to-end and preservation/equivalence proofs (
EndToEnd.lean,YulGeneration/{Equivalence,Preservation}.lean) to use these helpers in hypotheses and runtime calls, simplifying theorem signatures without changing proof intent.Reviewed by Cursor Bugbot for commit 8c58fb2. Bugbot is set up for automated code reviews on this repo. Configure here.