WIP: SSA construction block-level proofs #17
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
Create proof structure for SSA construction pass following phi_elimination pattern: - ssaDefsScript.sml: Basic SSA definitions (variable naming, version maps) - ssaTransformScript.sml: Transformation definitions (renaming, PHI placement) - ssaStateEquivScript.sml: State equivalence relating non-SSA to SSA states - ssaWellFormedScript.sml: Well-formedness conditions - ssaBlockScript.sml: Block-level correctness (with some cheat placeholders) - ssaFunctionScript.sml: Function-level correctness (with some cheat placeholders) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
- Add step_inst_halt_ssa_equiv and step_inst_revert_ssa_equiv theorems - Complete step_in_block_ssa_result_equiv for Halt/Revert cases - Complete run_block_ssa_equiv induction case - Add valid_ssa_transform_compatible helper theorem - Complete run_function_ssa_equiv and ssa_construction_correct The proof structure is now complete. Some proof steps require domain-specific reasoning about how the SSA transformation preserves instruction compatibility. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Progress on proving SSA construction correctness: - step_inst_non_phi_ssa_equiv: proven (non-PHI instruction preserves equiv) - exec_binop/unop/modop_result_ssa_equiv: helper theorems (have cheats for multi-output) - step_inst_result_ssa_equiv: WIP with >~ tactical approach - Added ssa_state_equiv_update_same_vm theorem for same-vm preservation Still have cheats remaining - work in progress. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
The proof was attempted with tactical approach but >~ pattern matching didn't work with HOL4's MATCH_MP_TAC. Document the working proof strategy discovered through interactive testing: - binop/unop/modop cases work with exec_*_result_ssa_equiv helper theorems - After case split, need to split on inst.inst_outputs and FLOOKUP vm h - Memory ops need case splits and load/store equiv theorems - Error cases use ssa_result_equiv_def directly 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Use documented cheat approach for JNZ proof due to batch/interactive mode discrepancy. Interactive proof verified working but batch mode fails due to TRY/NO_TAC interaction with rename1 tactic. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Added proven helper theorems for store and assign operations: - mstore_result_ssa_equiv, sstore_result_ssa_equiv, tstore_result_ssa_equiv - assign_result_ssa_equiv These theorems are fully proven but irule matching in step_inst_result_ssa_equiv fails due to gvs[AllCaseEqs()] expanding case structures to a form that doesn't match the theorem conclusions. Using cheat with documented workaround. Updated PLAN.md with current status and analysis of pattern matching issue. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
…issue Key findings: - ADD case proof works interactively: irule exec_binop_result_ssa_equiv + case splits on outputs + FLOOKUP - Batch mode issue: simp[] expands tuple case expressions to nested cases, breaking irule matching against helper theorems - All helper theorems proven without cheats: exec_*_result_ssa_equiv, *load_result_ssa_equiv, *store_result_ssa_equiv, assign_result_ssa_equiv - 4 cheats remain in ssaBlockTheory, all due to batch mode technical issues Updated PLAN.md with detailed documentation of proof approach and remaining work. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Replace cheats with working proofs: - jnz_result_ssa_equiv: Use CASE_TAC sequence with eval_operand_ssa_equiv - step_inst_result_ssa_equiv: Per-opcode tactics with explicit case handling - run_block_ssa_equiv: Explicit >- tacticals for base cases All ssaBlockTheory theorems now proven without cheats. 🤖 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
step_inst_non_phi_ssa_equivtheorem (proven)step_inst_result_ssa_equivand block-level proofsStatus
Work in progress - still has cheats that need to be removed:
Test plan
VFMDIR=/home/ubuntu/verifereum Holmake --qof🤖 Generated with Claude Code