Add ASSIGN elimination pass correctness proof#19

Open

charles-cooper wants to merge 22 commits intomainfrom

Commits on Dec 10, 2025

Add documentation for step_inst_operand_invariant proof strategy

charles-cooper
and
claude
committed
Add SSA disjointness for all_assigns_equiv preservation

charles-cooper
and
claude
committed
Add documentation for transform_block_correct proof strategy

charles-cooper
and
claude
committed
Merge branch 'main' into assign-elim
charles-cooper
committed
Merge branch 'main' into assign-elim
charles-cooper
committed
Merge branch 'main' into assign-elim
charles-cooper
committed
Merge branch 'main' into assign-elim
charles-cooper
committed
Prove exec_binop/unop/modop_operand_invariant helper lemmas

charles-cooper
and
claude
committed
Improve step_inst_operand_invariant proof documentation

charles-cooper
and
claude
committed
Prove all_assigns_equiv_preserved theorem

charles-cooper
and
claude
committed
Fix LENGTH_MAP reference in transform_inst_non_elim_correct

charles-cooper
and
claude
committed
Add amap_covers_block precondition for transform_block theorems

charles-cooper
and
claude
committed
Add helper lemmas for all_assigns_equiv preservation

charles-cooper
and
claude
committed
Prove resolve_phi_replace_operands and validate step_inst_replace_operands

charles-cooper
and
claude
committed
Develop step_in_block_transform_ok proof and add terminator_not_eliminable

charles-cooper
and
claude
committed
Document cheat dependencies in transform_block_result_equiv

charles-cooper
and
claude
committed
Add Halt/Revert/Error lemmas for transform_block

charles-cooper
and
claude
committed