Add branch optimization pass for Venom IR #20
+618
−4
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
Bash tool already provides timing info and has timeout parameter. Using time/timeout wrappers breaks permission pattern matching. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
This pass optimizes conditional branches by removing redundant ISZERO instructions. It transforms the pattern: %t = iszero %x jnz %t, @label_a, @label_b Into: nop jnz %x, @label_b, @label_a The key insight is that jnz (iszero x), A, B is semantically equivalent to jnz x, B, A since the condition is negated and targets swapped. Files: - branchOptTransformScript.sml: Transformation definitions (149 LOC) - branchOptCorrectScript.sml: Correctness proofs (239 LOC) Key theorems: - iszero_jnz_swap_equiv: The fundamental semantic equivalence - transform_block_execution_equiv: Main correctness theorem 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Use simp[Once step_inst_def] instead of fully unfolding step_inst_def to avoid exponential blowup from the ~50 opcode case expression. Build time reduced from ~59s to ~8s. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
xrchz
reviewed
Dec 10, 2025
| Cases_on `v = 0w` >> simp[bool_to_word_def, jump_to_def] | ||
| QED | ||
|
|
||
| val _ = export_theory(); |
Member
There was a problem hiding this comment.
export theory shouldn't be used explicitly when using modern Theory syntax
xrchz
reviewed
Dec 10, 2025
| QED | ||
|
|
||
| (* Main correctness theorem: transform preserves execution semantics *) | ||
| Theorem transform_block_execution_equiv: |
Member
There was a problem hiding this comment.
I expect to see a top level correctness theorem that has a short statement and actually calls the compiler pass. This one looks like a lemma that has the pass inlined.
Member
|
When adding new theories like this, we also need to add a leaf dependency to the root theory (vyperHol) so that the build CI exercises the new theories. I'd be happy to see additions for all the missing theories in this PR. |
- Remove explicit export_theory() calls from both script files - Add transform_block_correct theorem with run_block formulation - Add branchOptCorrect to vyperHol root theory for CI builds - Add venom/passes/branch_opt to Holmakefile INCLUDES - Add step_inst_preserves_current_bb helper lemma - Add get_instruction_transform_prefix prefix preservation lemma - Add rich_list to ancestors for list lemmas The transform_block_correct proof has a cheat for the non-trivial case (when transformation applies). The trivial case (transform_block bb = bb) is fully proven. Full proof requires block simulation infrastructure to track execution through prefix and apply local equivalence theorem. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
xrchz
reviewed
Dec 12, 2025
| 2. iszero_jnz_swap_equiv shows the last two instructions produce same target | ||
|
|
||
| Full infrastructure for this simulation argument is TODO. *) | ||
| cheat |
Member
There was a problem hiding this comment.
Doesn't transform_block_execution_equiv do a lot of the work for this?
- transform_applies_structure: extracts block structure when transform applies - transform_block_length: proves transform preserves instruction count - Document gt/etq goaltree workflow in AGENTS.md Main transform_block_correct still has cheat pending completion. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
…ution_equiv Re: PR comment asking if transform_block_execution_equiv does the work: transform_block_execution_equiv does the semantic heavy lifting - it proves that ISZERO+JNZ and NOP+swapped_JNZ produce the same vs_current_bb at the step_inst level. The remaining work in transform_block_correct is: 1. Prefix case (completed): For idx < n-2, both blocks step identically via step_in_block_transform_prefix, then recurse with the IH 2. Transformation point (remaining cheat): For idx = n-2, need to unfold run_block twice and connect to transform_block_execution_equiv. This requires extracting the full instruction structure from is_iszero_inst and jnz_uses_var. The proof structure now clearly shows how transform_block_execution_equiv fits into the overall correctness argument. 🤖 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
iszero x; jnz t, A, Bintonop; jnz x, B, AFiles
venom/passes/branch_opt/branchOptTransformScript.sml- Transformation definitions (149 LOC)venom/passes/branch_opt/branchOptCorrectScript.sml- Correctness proofs (239 LOC)Key Theorems
iszero_jnz_swap_equiv: The fundamental semantic equivalencetransform_block_execution_equiv: Main correctness theorem proving both paths lead to the same branch targetTest plan
🤖 Generated with Claude Code