Simulation framework: parameterized by state relation R

[charles-cooper]

co-authored by claude opus 4.6

Pass simulation framework parameterized by state relation R, with cheated proofs as placeholders.

Components

Simulation Framework (venom/simulation/)

• lift_result (defs/passSimulationDefsScript.sml): Lifts state relation R through exec_result — generalizes result_equiv (which is lift_result state_equiv)
• inst_simulates R f: Per-instruction simulation — f preserves lift_result R and is_terminator
• block_simulates R bt: Whole-block simulation via run_block
• block_map_transform / function_map_transform: 1:1 instruction/block mapping

Parameterized Execution Equivalence (venom/simulation/defs/execEquivParamDefsScript.sml)

• valid_state_rel R: Closure conditions on R enabling the master theorem (preserves non-var fields, closed under update_var, preserves eval_operand when operand vars agree, reflexive)
• step_inst_preserves_R: Master theorem — valid_state_rel R ∧ R s1 s2 ∧ operand vars agree ⟹ lift_result R (step_inst inst s1) (step_inst inst s2)
• Instantiations: state_equiv and state_equiv_except both satisfy valid_state_rel

Composition (venom/simulation/proofs/passCompositionProofsScript.sml)

• analysis_pass_correct: End-to-end theorem connecting dataflow convergence → soundness → simulation → function correctness, parameterized by R

Lifting Theorems

• inst_sim_block_sim — instruction sim → block sim
• block_sim_function — block sim → function correctness
• conditional_inst_sim — partial + identity → full inst_simulates
• block_sim_compose — composition preserves block_simulates
• lift_result_refl / lift_result_trans — R properties lift through results

Motivation

Eliminates per-pass boilerplate (~800 LOC each) for execution preservation proofs. Current RTA has 839 LOC of opcode-by-opcode helpers that step_inst_preserves_R replaces with one master theorem + one valid_state_rel satisfaction proof.

Stats

• 10 cheated theorems across 3 proof files
• 3 new files (execEquivParam defs/proofs/props), 5 modified
• All compile cleanly

Depends on

• PR Analysis infrastructure: lattice + worklist + dataflow helpers #157 (pass-infrastructure) — this branch includes the dataflow framework