Move common theories to venom/ for shared use across passes #27
+228
−110
Conversation
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
Refactors state equivalence and semantic properties into common location so they can be reused by phi_elimination, revert_to_assert, and future optimization passes. Changes: - Move stateEquivScript.sml to venom/ (extended for all state fields) - Move execEquivScript.sml to venom/ (updated for new opcodes) - Add venomSemPropsScript.sml with general semantic lemmas - Update phi_elimination to use common theories - Update revert_to_assert to use venomSemProps instead of duplicating Note: New cases added to execEquiv proofs for environment opcodes and ASSERT_UNREACHABLE introduced in 3f969d7. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
xrchz
approved these changes
Dec 28, 2025
Member
xrchz
left a comment
xrchz
left a comment
There was a problem hiding this comment.
Seems good. Only thing to note is that something like state_equiv is not in general gonna be the same for every compiler pass proof - it's good to have a generic one like this, but some passes might need to define a more specialised one that allows more differences or something.
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.
Summary
stateEquivScript.smlandexecEquivScript.smlfromphi_elimination/tovenom/for shared usevenomSemPropsScript.smlwith general semantic lemmas (bool_to_word, step_iszero, step_assert, step_jnz, step_jmp)state_equivto include all state fields (returndata, accounts, call_ctx, tx_ctx, block_ctx)execEquivfor environment opcodes and ASSERT_UNREACHABLE (introduced in 3f969d7)revert_to_assertto use common lemmas instead of duplicatingTest plan
venom/builds successfullyphi_elimination/builds successfullyrevert_to_assert/builds successfully (with expected CHEATs)🤖 Generated with Claude Code