Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
1a94882
Add ASSIGN elimination pass correctness proof structure
charles-cooper Dec 9, 2025
b92baf2
Prove transform_inst_elim_correct, refactor block-level proofs
charles-cooper Dec 9, 2025
6b6fce9
Add helper lemmas for block-level correctness
charles-cooper Dec 9, 2025
0af73b6
Merge branch 'main' into assign-elim
charles-cooper Dec 9, 2025
aecde0f
Strengthen step_inst_operand_invariant with LENGTH condition
charles-cooper Dec 9, 2025
0c4c4fc
Add documentation for step_inst_operand_invariant proof strategy
charles-cooper Dec 10, 2025
89fce3e
Add SSA disjointness for all_assigns_equiv preservation
charles-cooper Dec 10, 2025
dca92be
Add documentation for transform_block_correct proof strategy
charles-cooper Dec 10, 2025
0d094a5
Merge branch 'main' into assign-elim
charles-cooper Dec 10, 2025
f1e0d7a
Merge branch 'main' into assign-elim
charles-cooper Dec 10, 2025
10db43f
Merge branch 'main' into assign-elim
charles-cooper Dec 10, 2025
0b78f4f
Merge branch 'main' into assign-elim
charles-cooper Dec 10, 2025
079f8d4
Prove exec_binop/unop/modop_operand_invariant helper lemmas
charles-cooper Dec 10, 2025
13ac886
Improve step_inst_operand_invariant proof documentation
charles-cooper Dec 10, 2025
ce9d1f9
Prove all_assigns_equiv_preserved theorem
charles-cooper Dec 10, 2025
ca681bc
Fix LENGTH_MAP reference in transform_inst_non_elim_correct
charles-cooper Dec 10, 2025
6da8ca7
Add amap_covers_block precondition for transform_block theorems
charles-cooper Dec 10, 2025
adddbb1
Add helper lemmas for all_assigns_equiv preservation
charles-cooper Dec 10, 2025
4ee1deb
Prove resolve_phi_replace_operands and validate step_inst_replace_ope…
charles-cooper Dec 10, 2025
0479b68
Develop step_in_block_transform_ok proof and add terminator_not_elimi…
charles-cooper Dec 10, 2025
f96f31b
Document cheat dependencies in transform_block_result_equiv
charles-cooper Dec 10, 2025
18975cf
Add Halt/Revert/Error lemmas for transform_block
charles-cooper Dec 10, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions venom/passes/assign_elimination/Holmakefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
# ASSIGN elimination pass for Venom IR
# Includes venom semantics and verifereum theories
INCLUDES = $(VFMDIR)/util $(VFMDIR)/spec ../.. ../phi_elimination
Loading