Skip to content

Commit 55af130

Browse files
charles-coopercharles-cooper
committed
simulation framework: parameterized by state relation R
- lift_result: lifts state relation R through exec_result - inst_simulates R f / block_simulates R bt: simulation predicates - block_map_transform / function_map_transform: 1:1 mapping transforms - valid_state_rel: closure conditions for step_inst_preserves_R - Instantiations: state_equiv and state_equiv_except satisfy valid_state_rel - analysis_pass_correct: end-to-end composition theorem All proofs cheated (stubs for proving later).
1 parent ef6fda5 commit 55af130

12 files changed

+486
-0
lines changed

‎venom/simulation/Holmakefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
# Pass simulation and composition: public API
2+
INCLUDES = defs proofs

‎venom/simulation/README.md‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# Pass Simulation & Composition Framework
2+
3+
Generic infrastructure for proving compiler pass correctness.
4+
5+
## Structure
6+
7+
```
8+
defs/
9+
passSimulationDefsScript.sml — block_map_transform, function_map_transform,
10+
inst_simulates, block_simulates
11+
proofs/
12+
passSimulationProofsScript.sml — inst_sim_block_sim, block_sim_function,
13+
conditional_inst_sim, block_sim_compose,
14+
result_equiv_trans, lookup_block_map
15+
passCompositionProofsScript.sml — analysis_pass_correct
16+
passSimulationPropsScript.sml — re-exports simulation proofs via ACCEPT_TAC
17+
passCompositionPropsScript.sml — re-exports composition proof via ACCEPT_TAC
18+
```
19+
20+
## Usage
21+
22+
For a 1:1 instruction-mapping pass:
23+
1. Define transform function `f : instruction → instruction`
24+
2. Prove `inst_simulates f` (or use `conditional_inst_sim` for partial transforms)
25+
3. Get block and function correctness for free via `inst_sim_block_sim` + `block_sim_function`
26+
27+
For an analysis-driven pass:
28+
1. Prove dataflow framework conditions (lattice, worklist convergence)
29+
2. Prove analysis fixpoint implies soundness
30+
3. Prove soundness implies block simulation
31+
4. Get function correctness via `analysis_pass_correct`
32+
33+
## Dependencies
34+
35+
Uses `stateEquiv`/`execEquiv` from `venom/` for state and result equivalence.
36+
Uses `worklistProps` from `analysis/dataflow/` for convergence.

‎venom/simulation/defs/Holmakefile‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
# Pass simulation definitions
2+
# From simulation/defs/ relative paths:
3+
# ../.. = venom/
4+
# ../../.. = project root
5+
INCLUDES = $(VFMDIR)/util $(VFMDIR)/spec ../.. ../../../syntax ../../../semantics

‎venom/simulation/defs/execEquivParamDefsScript.sml‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
(*
2+
* Parameterized Execution Equivalence — Definitions
3+
*
4+
* Closure conditions on a state relation R that enable
5+
* step_inst_preserves_R (the master theorem).
6+
*
7+
* Both state_equiv and state_equiv_except satisfy valid_state_rel.
8+
* This eliminates per-pass boilerplate (~800 LOC each for RTA, phi-elim, etc.)
9+
*
10+
* TOP-LEVEL:
11+
* valid_state_rel — closure conditions on R for execution preservation
12+
*)
13+
14+
Theory execEquivParamDefs
15+
Ancestors
16+
stateEquiv venomSem venomState venomInst
17+
18+
(* Closure conditions on a state relation R.
19+
Any R satisfying these supports step_inst_preserves_R.
20+
21+
Conservative: requires all non-var fields equal.
22+
Can be weakened later if a pass only needs partial field equality. *)
23+
Definition valid_state_rel_def:
24+
valid_state_rel (R : venom_state -> venom_state -> bool) <=>
25+
(* R preserves execution-relevant state fields *)
26+
(!s1 s2. R s1 s2 ==>
27+
s1.vs_call_ctx = s2.vs_call_ctx /\
28+
s1.vs_tx_ctx = s2.vs_tx_ctx /\
29+
s1.vs_block_ctx = s2.vs_block_ctx /\
30+
s1.vs_accounts = s2.vs_accounts /\
31+
s1.vs_memory = s2.vs_memory /\
32+
s1.vs_storage = s2.vs_storage /\
33+
s1.vs_transient = s2.vs_transient /\
34+
s1.vs_returndata = s2.vs_returndata /\
35+
s1.vs_halted = s2.vs_halted /\
36+
s1.vs_prev_bb = s2.vs_prev_bb /\
37+
s1.vs_current_bb = s2.vs_current_bb /\
38+
s1.vs_inst_idx = s2.vs_inst_idx) /\
39+
(* R closed under var update *)
40+
(!s1 s2 x v. R s1 s2 ==> R (update_var x v s1) (update_var x v s2)) /\
41+
(* R preserves eval_operand when operand var agrees *)
42+
(!s1 s2 op. R s1 s2 /\
43+
(!x. op = Var x ==> lookup_var x s1 = lookup_var x s2) ==>
44+
eval_operand op s1 = eval_operand op s2) /\
45+
(* R reflexive *)
46+
(!s. R s s)
47+
End

‎venom/simulation/defs/passSimulationDefsScript.sml‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
(*
2+
* Pass Simulation Framework — Definitions
3+
*
4+
* Generic block→function lifting for pass correctness proofs,
5+
* parameterized by state relation R.
6+
*
7+
* TOP-LEVEL:
8+
* lift_result — lift state relation R through exec_result
9+
* block_map_transform — MAP f over block instructions
10+
* function_map_transform — MAP bt over function blocks
11+
* inst_simulates — per-instruction simulation predicate (param by R)
12+
* block_simulates — whole-block simulation predicate (param by R)
13+
*)
14+
15+
Theory passSimulationDefs
16+
Ancestors
17+
stateEquiv execEquiv venomSem venomInst
18+
19+
(* ===== Result relation ===== *)
20+
21+
(* Lift state relation R through exec_result.
22+
result_equiv = lift_result state_equiv
23+
result_equiv_except fresh = lift_result (state_equiv_except fresh) *)
24+
Definition lift_result_def:
25+
lift_result R (OK s1) (OK s2) = R s1 s2 /\
26+
lift_result R (Halt s1) (Halt s2) = R s1 s2 /\
27+
lift_result R (Revert s1) (Revert s2) = R s1 s2 /\
28+
lift_result R (Error e1) (Error e2) = T /\
29+
lift_result R _ _ = F
30+
End
31+
32+
(* ===== Transform definitions ===== *)
33+
34+
(* Level 1: 1:1 instruction mapping *)
35+
Definition block_map_transform_def:
36+
block_map_transform f bb =
37+
bb with bb_instructions := MAP f bb.bb_instructions
38+
End
39+
40+
(* Function transform: apply block transform to all blocks *)
41+
Definition function_map_transform_def:
42+
function_map_transform bt fn =
43+
fn with fn_blocks := MAP bt fn.fn_blocks
44+
End
45+
46+
(* ===== Simulation predicates (parameterized by R) ===== *)
47+
48+
(* Level 1: per-instruction simulation.
49+
f preserves lift_result R for every instruction and state,
50+
and preserves the is_terminator property. *)
51+
Definition inst_simulates_def:
52+
inst_simulates R f <=>
53+
(!inst s. lift_result R (step_inst inst s) (step_inst (f inst) s)) /\
54+
(!inst. is_terminator inst.inst_opcode =
55+
is_terminator (f inst).inst_opcode)
56+
End
57+
58+
(* Level 2: whole-block simulation.
59+
Running the transformed block gives an R-related result. *)
60+
Definition block_simulates_def:
61+
block_simulates R bt <=>
62+
!bb s. lift_result R (run_block bb s) (run_block (bt bb) s)
63+
End

‎venom/simulation/execEquivParamPropsScript.sml‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
(*
2+
* Parameterized Execution Equivalence — Properties (Statements Only)
3+
*
4+
* Re-exports from proofs/execEquivParamProofsScript.sml via ACCEPT_TAC.
5+
*)
6+
7+
Theory execEquivParamProps
8+
Ancestors
9+
execEquivParamProofs
10+
11+
Theorem step_inst_preserves_R:
12+
!(R : venom_state -> venom_state -> bool) inst s1 s2.
13+
valid_state_rel R /\ R s1 s2 /\
14+
(!x. MEM (Var x) inst.inst_operands ==>
15+
lookup_var x s1 = lookup_var x s2) ==>
16+
lift_result R (step_inst inst s1) (step_inst inst s2)
17+
Proof
18+
ACCEPT_TAC step_inst_preserves_R_proof
19+
QED
20+
21+
Theorem state_equiv_valid_state_rel:
22+
valid_state_rel state_equiv
23+
Proof
24+
ACCEPT_TAC state_equiv_valid_state_rel_proof
25+
QED
26+
27+
Theorem state_equiv_except_valid_state_rel:
28+
!fresh. valid_state_rel (state_equiv_except fresh)
29+
Proof
30+
ACCEPT_TAC state_equiv_except_valid_state_rel_proof
31+
QED

‎venom/simulation/passCompositionPropsScript.sml‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
(*
2+
* Analysis-Driven Pass Composition — Correctness (Statement Only)
3+
*
4+
* Re-exports from proofs/passCompositionProofsScript.sml via ACCEPT_TAC.
5+
*)
6+
7+
Theory passCompositionProps
8+
Ancestors
9+
passCompositionProofs passSimulationProps
10+
11+
Theorem analysis_pass_correct:
12+
!(R : venom_state -> venom_state -> bool)
13+
(leq : 'a -> 'a -> bool) m b
14+
(process : 'c -> 'a -> 'a)
15+
(deps : 'c -> 'c list)
16+
(wl0 : 'c list) (st0 : 'a)
17+
(all_lbls : 'c list)
18+
(P : 'a -> bool)
19+
(sound : 'a -> bool)
20+
(transform : 'a -> basic_block -> basic_block).
21+
(!lbl st. P st ==> leq st (process lbl st)) /\
22+
(!lbl st. P st ==> P (process lbl st)) /\
23+
P st0 /\
24+
bounded_measure P leq m b /\
25+
wl_deps_complete process deps /\
26+
(!lbl. MEM lbl all_lbls ==> MEM lbl wl0) /\
27+
(!st. is_fixpoint process all_lbls st ==> sound st) /\
28+
(!analysis. sound analysis ==>
29+
block_simulates R (transform analysis)) /\
30+
(!analysis bb. (transform analysis bb).bb_label = bb.bb_label)
31+
==>
32+
let analysis = SND (wl_iterate process deps wl0 st0) in
33+
!fuel fn s.
34+
lift_result R (run_function fuel fn s)
35+
(run_function fuel
36+
(function_map_transform (transform analysis) fn) s)
37+
Proof
38+
ACCEPT_TAC analysis_pass_correct_proof
39+
QED

‎venom/simulation/passSimulationPropsScript.sml‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
(*
2+
* Pass Simulation Framework — Correctness (Statements Only)
3+
*
4+
* Re-exports from proofs/passSimulationProofsScript.sml via ACCEPT_TAC.
5+
*)
6+
7+
Theory passSimulationProps
8+
Ancestors
9+
passSimulationProofs
10+
11+
Theorem lookup_block_map:
12+
!lbl bbs bt.
13+
(!bb. (bt bb).bb_label = bb.bb_label) ==>
14+
lookup_block lbl (MAP bt bbs) =
15+
OPTION_MAP bt (lookup_block lbl bbs)
16+
Proof
17+
ACCEPT_TAC lookup_block_map_proof
18+
QED
19+
20+
Theorem lift_result_refl:
21+
!(R : venom_state -> venom_state -> bool).
22+
(!s. R s s) ==>
23+
!r. lift_result R r r
24+
Proof
25+
ACCEPT_TAC lift_result_refl_proof
26+
QED
27+
28+
Theorem lift_result_trans:
29+
!(R : venom_state -> venom_state -> bool).
30+
(!s1 s2 s3. R s1 s2 /\ R s2 s3 ==> R s1 s3) ==>
31+
!r1 r2 r3. lift_result R r1 r2 /\ lift_result R r2 r3 ==>
32+
lift_result R r1 r3
33+
Proof
34+
ACCEPT_TAC lift_result_trans_proof
35+
QED
36+
37+
Theorem inst_sim_block_sim:
38+
!(R : venom_state -> venom_state -> bool) f.
39+
inst_simulates R f ==>
40+
block_simulates R (block_map_transform f)
41+
Proof
42+
ACCEPT_TAC inst_sim_block_sim_proof
43+
QED
44+
45+
Theorem block_sim_function:
46+
!(R : venom_state -> venom_state -> bool) bt.
47+
block_simulates R bt /\
48+
(!bb. (bt bb).bb_label = bb.bb_label) ==>
49+
!fuel fn s.
50+
lift_result R (run_function fuel fn s)
51+
(run_function fuel (function_map_transform bt fn) s)
52+
Proof
53+
ACCEPT_TAC block_sim_function_proof
54+
QED
55+
56+
Theorem conditional_inst_sim:
57+
!(R : venom_state -> venom_state -> bool) f P.
58+
(!s. R s s) /\
59+
(!inst s. P inst ==>
60+
lift_result R (step_inst inst s) (step_inst (f inst) s)) /\
61+
(!inst. P inst ==>
62+
is_terminator inst.inst_opcode =
63+
is_terminator (f inst).inst_opcode) /\
64+
(!inst. ~P inst ==> f inst = inst) ==>
65+
inst_simulates R f
66+
Proof
67+
ACCEPT_TAC conditional_inst_sim_proof
68+
QED
69+
70+
Theorem block_sim_compose:
71+
!(R : venom_state -> venom_state -> bool) bt1 bt2.
72+
(!s1 s2 s3. R s1 s2 /\ R s2 s3 ==> R s1 s3) /\
73+
block_simulates R bt1 /\ block_simulates R bt2 ==>
74+
block_simulates R (bt2 o bt1)
75+
Proof
76+
ACCEPT_TAC block_sim_compose_proof
77+
QED

‎venom/simulation/proofs/Holmakefile‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# Pass simulation and composition proofs
2+
INCLUDES = ../defs \
3+
../../analysis/dataflow/defs ../../analysis/dataflow/proofs ../../analysis/dataflow

‎venom/simulation/proofs/execEquivParamProofsScript.sml‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
(*
2+
* Parameterized Execution Equivalence — Proofs
3+
*
4+
* Master theorem: step_inst preserves any valid_state_rel R
5+
* when operand variables agree.
6+
*
7+
* Instantiations: state_equiv and state_equiv_except both satisfy valid_state_rel.
8+
*
9+
* TOP-LEVEL:
10+
* step_inst_preserves_R — master theorem
11+
* state_equiv_valid_state_rel — state_equiv satisfies valid_state_rel
12+
* state_equiv_except_valid_state_rel — state_equiv_except satisfies valid_state_rel
13+
*)
14+
15+
Theory execEquivParamProofs
16+
Ancestors
17+
execEquivParamDefs passSimulationDefs
18+
19+
(* Master theorem: step_inst on R-related states with agreeing operand
20+
vars produces lift_result R related results. *)
21+
Theorem step_inst_preserves_R_proof:
22+
!(R : venom_state -> venom_state -> bool) inst s1 s2.
23+
valid_state_rel R /\ R s1 s2 /\
24+
(!x. MEM (Var x) inst.inst_operands ==>
25+
lookup_var x s1 = lookup_var x s2) ==>
26+
lift_result R (step_inst inst s1) (step_inst inst s2)
27+
Proof
28+
cheat
29+
QED
30+
31+
(* state_equiv satisfies valid_state_rel *)
32+
Theorem state_equiv_valid_state_rel_proof:
33+
valid_state_rel state_equiv
34+
Proof
35+
cheat
36+
QED
37+
38+
(* state_equiv_except satisfies valid_state_rel for any fresh set *)
39+
Theorem state_equiv_except_valid_state_rel_proof:
40+
!fresh. valid_state_rel (state_equiv_except fresh)
41+
Proof
42+
cheat
43+
QED

0 commit comments

Comments
 (0)