Add revert_to_assert pass #16
Draft
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
Implements the revert-to-assert optimization for Venom IR: - Transforms jnz cond @revert @else into iszero+assert+jmp - Transforms jnz cond @then @revert into assert+jmp Adds ASSERT and ASSERT_UNREACHABLE semantics to venomSemScript.sml. Key correctness theorems are cheated for now; full proofs to follow. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- Prove transform_blocks_length, transform_blocks_labels, lookup_block_transform_blocks in rtaFunction - Add and prove run_then_transform_block and run_else_transform_block helpers in rtaBlock showing transformed instruction sequences produce correct results - Fix rta_then_produces_assert and rta_else_produces_assert proofs - Remaining cheats: rta_then_block_equiv, rta_else_block_equiv, transform_function_correct 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
…ence - Add step_inst_preserves_inst_idx: step_inst doesn't change vs_inst_idx for non-terminator instructions - Add step_in_block_prefix_same: step_in_block is identical for blocks with same prefix when executing within the prefix - Document proof structure for rta_then_block_equiv_general using complete induction on remaining instructions - Update rtaFunctionScript with detailed proof status documentation The generalized theorems handle blocks with arbitrary prefix instructions before the JNZ terminator, extending the simple case theorems. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- Add rta_then_terminator_else: handles terminator position for else branch - Add rta_then_terminator_then: handles terminator position for then branch - Add then_lbl <> else_lbl precondition to general theorems - Add s.vs_inst_idx = 0 and ~s.vs_halted preconditions These terminator case theorems are fully proved (no cheats). The general theorems still use cheats for the prefix-handling case. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- Add s.vs_inst_idx = 0 and ~s.vs_halted preconditions to transform_block_run_*
- Structure proofs with case analysis separating no-transformation from transformation cases
- Update documentation with clear dependency chain between block and function level theorems
- Simplify block-level general theorems to single cheat (interactively verified base cases)
The dependency chain is now:
rta_*_block_equiv_general (prefix case cheated)
-> transform_block_run_* (structured, inner cheats)
-> transform_function_correct
-> transform_preserves_halts/reverts
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.5 <[email protected]>
Verified interactively that the FRONT = [] base cases for rta_then_block_equiv_general work: - else_lbl (cond=0): iszero gives 1, assert(1) passes, jmp to else_lbl - then_lbl (cond!=0): iszero gives 0, assert(0) Reverts The FRONT = h::t prefix cases require complete induction on the measure (LENGTH bb.bb_instructions - s.vs_inst_idx) and are still cheated. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
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
jnz cond @revert @elseintoiszero cond; assert; jmp @elsejnz cond @then @revertintoassert cond; jmp @thenFiles
venom/venomSemScript.sml- Added ASSERT/ASSERT_UNREACHABLE semanticsvenom/passes/revert_to_assert/rtaTransformScript.sml- Transformation definitionsvenom/passes/revert_to_assert/rtaWellFormedScript.sml- Applicability predicatesvenom/passes/revert_to_assert/rtaBlockScript.sml- Block-level correctnessvenom/passes/revert_to_assert/rtaFunctionScript.sml- Function-level correctnessStatus
Key correctness theorems are cheated; full proofs in progress.
🤖 Generated with Claude Code