1 | include "common/SmallstepExec.ma". |
---|
2 | include "common/IO.ma". |
---|
3 | |
---|
4 | (* Equivalences of execution traces. *) |
---|
5 | |
---|
6 | (* A finite trace is produced by some prefix of an execution. *) |
---|
7 | |
---|
8 | inductive steps (state:Type[0]) : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝ |
---|
9 | | steps_stop : ∀tr,s,r. steps state tr (e_stop … tr s r) (e_stop … tr s r) |
---|
10 | | steps_step : ∀tr,s,e. steps state tr (e_step … tr s e) e |
---|
11 | | steps_steps : ∀tr,s,e,tr',e'. steps state tr e e' → steps state (tr'⧺tr) (e_step … tr' s e) e'. |
---|
12 | |
---|
13 | (* Go from individual steps to part of an execution trace. *) |
---|
14 | lemma plus_exec : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s'. |
---|
15 | plus … FE gl s tr s' → |
---|
16 | is_final … FE gl s' = None ? → |
---|
17 | steps (state … gl) tr |
---|
18 | (exec_inf_aux … FE gl (step … FE gl s)) |
---|
19 | (exec_inf_aux … FE gl (step … FE gl s')). |
---|
20 | #FE #gl #s0 #tr0 #s0' #P elim P |
---|
21 | [ #s1 #tr #s2 #NF1 #EX #NF2 >EX >exec_inf_aux_unfold |
---|
22 | whd in ⊢ (???%?); >NF2 |
---|
23 | %2 |
---|
24 | | #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #NF3 |
---|
25 | >EX1 >exec_inf_aux_unfold |
---|
26 | whd in ⊢ (???%?); >(plus_not_final … P2) /3/ |
---|
27 | ] qed. |
---|
28 | |
---|
29 | lemma plus_final : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s',r. |
---|
30 | plus … FE gl s tr s' → |
---|
31 | is_final … FE gl s' = Some ? r → |
---|
32 | ∃tr'. steps (state … gl) tr |
---|
33 | (exec_inf_aux … FE gl (step … FE gl s)) |
---|
34 | (e_stop … tr' r s'). |
---|
35 | #FE #gl #s0 #tr0 #s0' #r #P elim P |
---|
36 | [ #s1 #tr #s2 #NF1 #EX #F2 >EX >exec_inf_aux_unfold |
---|
37 | whd in ⊢ (??(λ_.???%?)); >F2 |
---|
38 | %{tr} %1 |
---|
39 | | #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #F3 |
---|
40 | >EX1 >exec_inf_aux_unfold |
---|
41 | whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2) |
---|
42 | cases (IH F3) #tr'' #S' %{tr''} /2/ |
---|
43 | ] qed. |
---|
44 | |
---|
45 | (* In some places we do not consider wrong executions. *) |
---|
46 | |
---|
47 | coinductive not_wrong (state:Type[0]) : execution state io_out io_in → Prop ≝ |
---|
48 | | nw_stop : ∀tr,i,s. not_wrong state (e_stop … tr i s) |
---|
49 | | nw_step : ∀tr,s,e. not_wrong state e → not_wrong state (e_step … tr s e) |
---|
50 | | nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k). |
---|
51 | |
---|
52 | lemma not_wrong_not_wrong : ∀state,m. |
---|
53 | ¬ (not_wrong state (e_wrong … m)). |
---|
54 | #state #m % #NW inversion NW |
---|
55 | #A #B #C #D #E destruct |
---|
56 | qed. |
---|
57 | |
---|
58 | lemma not_wrong_steps : ∀state,e,e',tr. |
---|
59 | steps state tr e e' → |
---|
60 | not_wrong state e → |
---|
61 | not_wrong state e'. |
---|
62 | #state #e0 #e0' #tr0 #S elim S |
---|
63 | [ // |
---|
64 | | #tr #s #e #NW inversion NW |
---|
65 | #A #B #C #D #E try #F destruct // |
---|
66 | | #tr #s #e #tr' #e' #S' #IH #NW @IH |
---|
67 | inversion NW |
---|
68 | #A #B #C #D #E try #F destruct // |
---|
69 | ] qed. |
---|
70 | |
---|
71 | lemma not_wrong_init : ∀FE,p. |
---|
72 | not_wrong ? (exec_inf … FE p) → |
---|
73 | ∃s. make_initial_state … p = OK ? s. |
---|
74 | #FE #p whd in ⊢ (??% → ?); |
---|
75 | cases (make_initial_state ??? p) |
---|
76 | [ /2/ |
---|
77 | | normalize #m #NW @⊥ |
---|
78 | inversion NW #H1 #H2 #H3 #H4 try #H5 destruct |
---|
79 | ] qed. |
---|
80 | |
---|
81 | |
---|
82 | (* One execution is simulated by another, but possibly using a different number |
---|
83 | of steps. Note that we have to allow for several steps at the end to make |
---|
84 | the trace match up. |
---|
85 | |
---|
86 | This assumes that the overall traces are exactly the same; this may not be |
---|
87 | the case everywhere and we might have to add a cost label map. (There is |
---|
88 | a separate definition for the cost labelling stage, see |
---|
89 | Clight/labelSpecification.ma.) |
---|
90 | *) |
---|
91 | |
---|
92 | coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝ |
---|
93 | | sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2. |
---|
94 | steps S1 tr e1 (e_stop … tr1 r s1) → |
---|
95 | steps S2 tr e2 (e_stop … tr2 r s2) → |
---|
96 | simulates S1 S2 e1 e2 |
---|
97 | | sim_steps : ∀tr,e1,e1',e2,e2'. |
---|
98 | steps S1 tr e1 e1' → |
---|
99 | steps S2 tr e2 e2' → |
---|
100 | simulates S1 S2 e1' e2' → |
---|
101 | simulates S1 S2 e1 e2 |
---|
102 | | sim_interact : ∀o,k1,k2. |
---|
103 | (∀i. simulates S1 S2 (k1 i) (k2 i)) → |
---|
104 | simulates S1 S2 (e_interact … o k1) (e_interact … o k2). |
---|
105 | |
---|
106 | |
---|
107 | (* Result for lifting simulations on states to simulations on execution traces. |
---|
108 | At the time of writing this hasn't been used in anger yet... |
---|
109 | |
---|
110 | This probably isn't the best route for the stages of the compiler that have |
---|
111 | results in terms of structured traces, but it should be good for the |
---|
112 | front-end. |
---|
113 | *) |
---|
114 | |
---|
115 | let corec build_cofix_simulation |
---|
116 | (FS1,FS2:fullexec io_out io_in) |
---|
117 | (g1:global … FS1) (g2:global … FS2) |
---|
118 | (SIM:state … g1 → state … g2 → Prop) |
---|
119 | (s1:state … g1) (s2:state … g2) |
---|
120 | (NF:is_final … FS1 g1 s1 = None ?) |
---|
121 | (S:SIM s1 s2) |
---|
122 | (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y) |
---|
123 | (SIM_GOOD: ∀x,y. SIM x y → |
---|
124 | not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) → |
---|
125 | is_final … FS1 g1 x = None ? → |
---|
126 | ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) ) |
---|
127 | (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1))) |
---|
128 | : simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?. |
---|
129 | lapply (SIM_GOOD … S NW NF) |
---|
130 | * #tr * #s1' * #s2' * #P1 * #P2 #S' |
---|
131 | lapply (refl ? (is_final … FS1 g1 s1')) |
---|
132 | cases (is_final … s1') in ⊢ (???% → ?); |
---|
133 | [ #NF1 |
---|
134 | @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?)) |
---|
135 | [ @(plus_exec … P1) // |
---|
136 | | @(plus_exec … P2) <SIM_FINAL // |
---|
137 | | @(not_wrong_steps … (plus_exec … P1 …)) // |
---|
138 | | // |
---|
139 | ] |
---|
140 | | #r #F1 |
---|
141 | cases (plus_final … P1 F1) #tr1' #S1 |
---|
142 | cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2 |
---|
143 | @(sim_stop … S1 S2) |
---|
144 | ] qed. |
---|
145 | |
---|
146 | theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in. |
---|
147 | ∀p1:program … FE1. ∀p2:program … FE2. |
---|
148 | let g1 ≝ make_global … p1 in |
---|
149 | let g2 ≝ make_global … p2 in |
---|
150 | ∀SIM: state … g1 → state … g2 → Prop. |
---|
151 | ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 → |
---|
152 | ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2). |
---|
153 | ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y. |
---|
154 | ∀SIM_GOOD: ∀x,y. SIM x y → |
---|
155 | not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) → |
---|
156 | is_final … FE1 g1 x = None ? → |
---|
157 | ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')). |
---|
158 | let e1 ≝ exec_inf … FE1 p1 in |
---|
159 | let e2 ≝ exec_inf … FE2 p2 in |
---|
160 | not_wrong … e1 → |
---|
161 | simulates … e1 e2. |
---|
162 | |
---|
163 | #FE1 #FE2 #p1 #p2 |
---|
164 | letin g1 ≝ (make_global … p1) |
---|
165 | letin g2 ≝ (make_global … p2) |
---|
166 | #SIM #SIM_INIT #SIM_FINAL #SIM_GOOD |
---|
167 | #NW |
---|
168 | cases (not_wrong_init … p1 NW) |
---|
169 | #s1 #I1 |
---|
170 | cases (SIM_INIT … I1) #s2 * #I2 #S |
---|
171 | whd in NW:(??%) ⊢ (???%%); |
---|
172 | >I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%); |
---|
173 | change with g1 in match (make_global … p1); |
---|
174 | change with g2 in match (make_global … p2); |
---|
175 | |
---|
176 | >exec_inf_aux_unfold whd in ⊢ (??% → ???%?); |
---|
177 | lapply (SIM_FINAL … S) |
---|
178 | lapply (refl ? (is_final … s1)) |
---|
179 | cases (is_final … s1) in ⊢ (???% → %); |
---|
180 | [ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%); |
---|
181 | <F2 whd in ⊢ (? → ???%%); #NW |
---|
182 | @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption |
---|
183 | [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ] |
---|
184 | | #r #F1 #F2 #NW whd in ⊢ (???%%); |
---|
185 | >exec_inf_aux_unfold whd in ⊢ (???%%); |
---|
186 | <F2 whd in ⊢ (???%%); |
---|
187 | @(sim_stop … (steps_stop …) (steps_stop …)) |
---|
188 | ] qed. |
---|
189 | |
---|