Add ASSIGN elimination pass correctness proof #19
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
- assignDefs: Transformation definitions (build_assign_map, transform_inst) - assignWellFormed: Well-formedness predicates and replace_var_correct - assignBlock: Block-level correctness (cheated) - assignFunction: Function-level correctness (cheated) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- transform_inst_elim_correct: Full proof for eliminable ASSIGN instructions - transform_inst_non_elim_correct: Uses step_inst_operand_invariant helper - step_inst_operand_invariant: Helper lemma (cheated - needs opcode case split) - Simplified step_in_block_transform theorems 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- all_assigns_equiv_preserved: SSA invariant preservation (cheated) - transform_block_correct: Block OK case (cheated) - transform_block_result_equiv: Structured by result type 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Add LENGTH equality premise to step_inst_operand_invariant to ensure pattern matching on operand lists works correctly. Update transform_inst_non_elim_correct to provide the LENGTH_MAP evidence. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Documented the approach for proving the operand invariance lemma: - Requires case analysis on ~93 opcodes - Helper lemmas for exec_binop/exec_unop/exec_modop were proved interactively - Main insight: eval_operands equality implies individual eval_operand equality when the overall result is SOME 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- Add inst_output_disjoint_amap_def: SSA property that outputs not in amap - Prove update_var_preserves_all_assigns_equiv: key helper for preservation - Add SSA assumption to all_assigns_equiv_preserved, transform_block_correct - Document proof strategy for 93 opcode case analysis 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Document the induction structure and key helper lemmas needed for the block-level correctness proof. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Add three helper lemmas proving that exec_binop, exec_unop, and exec_modop results depend only on operand evaluation values, not operand structure. Each uses EVERY_CASE_TAC with case analysis on list structures. These helpers are the foundation for step_inst_operand_invariant, which remains cheated due to exponential case explosion in complex opcodes like JNZ (proof validated interactively but takes >4 minutes). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Updated documentation with validated proof strategy from interactive exploration: - 32 subgoals after case split on inst.inst_opcode - Helper lemmas (exec_binop/unop/modop_operand_invariant) solve ~22 goals - Remaining ~10 non-exec cases need list structure case analysis - Case explosion on complex opcodes causes >4 min build time - Proof is valid but left as cheat for performance 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Replace cheat with actual proof for all_assigns_equiv_preserved, which shows that SSA disjointness property ensures all_assigns_equiv is preserved through instruction execution. The proof: - Case splits on 93 opcodes via Cases_on `inst.inst_opcode` - For arithmetic ops (exec_binop/unop/modop): uses update_var_preserves - For store ops (MSTORE/SSTORE/TSTORE): shows vs_vars unchanged - For control ops (JMP/JNZ): shows vs_vars unchanged via jump_to_def Also update transform_block_correct documentation with validated proof strategy explored interactively. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Use listTheory.LENGTH_MAP instead of bare LENGTH_MAP for proper scoping. The proof is complete but depends on step_inst_operand_invariant which is cheated, causing transitive cheat marking. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
The transform_inst function eliminates ALL eliminable assigns (those with assign_var_source inst = SOME (out, src)), but the correctness theorem transform_inst_elim_correct requires FLOOKUP amap out = SOME src. This means for correctness, amap must contain entries for all eliminable assigns in the block. This is satisfied when amap is built by build_assign_map, but needs to be explicit in the theorem statement. Added: - amap_covers_block definition: amap contains mappings for all eliminable assigns - Updated transform_block_correct and transform_block_result_equiv preconditions 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- next_inst_preserves_all_assigns_equiv: trivial since next_inst only changes vs_inst_idx - step_in_block_preserves_all_assigns_equiv: uses all_assigns_equiv_preserved and next_inst helper to show step_in_block preserves the property These helpers are key for proving transform_block_correct via induction. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
…rands Key changes: - resolve_phi_replace_operands: fully proven using measureInduct_on - step_inst_replace_operands: validated interactively, documented proof (cheated due to ~3min build time with 93 opcode cases) - transform_inst_non_elim_correct: now uses step_inst_replace_operands 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
…nable - Add terminator_not_eliminable theorem: terminators are not eliminable assigns - Replace cheat in step_in_block_transform_ok with full proof: * Terminator case: use terminator_not_eliminable + transform_inst_non_elim_correct * Non-terminator eliminable: use amap_covers_block + transform_inst_elim_correct * Non-terminator non-eliminable: use transform_inst_non_elim_correct - Simplify step_inst_replace_operands comment (proof validated but slow) Remaining cheats: step_inst_replace_operands (93 opcode cases), transform_block_result_equiv Halt/Revert/Error cases 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Add detailed comments explaining what lemmas are needed to complete the Halt/Revert/Error cases in transform_block_result_equiv: - Halt case needs step_in_block_transform_halt lemma - Revert case needs step_in_block_transform_revert lemma - Error case needs step_in_block_transform_error lemma These lemmas would show that transformation preserves non-OK results with state_equiv, similar to how step_in_block_transform_ok handles the OK case. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- Add amap_operands_defined definition: ensures eliminable assigns have defined operands, preventing behavior change from Error to OK - Add step_in_block_transform_halt: transform preserves Halt results - Add step_in_block_transform_revert: transform preserves Revert results - Add step_in_block_transform_error: transform preserves Error results (requires amap_operands_defined precondition) - Update transform_block_result_equiv to include amap_operands_defined Key insight: For Error case, an eliminable assign with undefined operand would error in original but the transformed NOP would succeed. The amap_operands_defined precondition prevents this semantic difference. 🤖 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
transform_inst_elim_correct- core lemma showing eliminated ASSIGNs preserve semanticsFiles
assignDefsScript.sml- Transformation definitions (build_assign_map, transform_inst, etc.)assignWellFormedScript.sml- Well-formedness predicates and helper lemmasassignBlockScript.sml- Block-level correctness proofsassignFunctionScript.sml- Function-level correctness theoremTest plan
Holmake --qoftransform_inst_elim_correctfully proven🤖 Generated with Claude Code