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 | (* And similarly for after_n_steps *) |
---|
46 | |
---|
47 | lemma after_inv : ∀FE:fullexec io_out io_in. |
---|
48 | ∀n,g,inv,P,s. |
---|
49 | after_n_steps (S n) … FE g s inv P → |
---|
50 | ∃tr,s'. |
---|
51 | P tr s' ∧ |
---|
52 | match is_final ?? FE g s' with |
---|
53 | [ Some r ⇒ ∃tr'. |
---|
54 | steps ? tr (exec_inf_aux … FE g (step … FE g s)) |
---|
55 | (e_stop ??? tr' r s') |
---|
56 | | None ⇒ |
---|
57 | steps ? tr (exec_inf_aux … FE g (step … FE g s)) |
---|
58 | (exec_inf_aux … FE g (step … FE g s')) |
---|
59 | ]. |
---|
60 | #FE #n #g #inv #P |
---|
61 | (* Rather nasty generalisation *) |
---|
62 | #s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW |
---|
63 | cut (∃tr,s'. P (E0⧺tr) s' ∧ ?) [3: #H @H | skip ] |
---|
64 | generalize in match E0 in AW ⊢ %; generalize in match s; -s |
---|
65 | elim n |
---|
66 | [ #s #tr whd in ⊢ (% → %); |
---|
67 | cases (step … s) [ #o #K * | 3: #m * ] |
---|
68 | * #tr' #s' |
---|
69 | whd in ⊢ (% → ?); cases (inv s') [2: *] |
---|
70 | #AW %{tr'} %{s'} %{AW} |
---|
71 | lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %); |
---|
72 | [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step |
---|
73 | | #r #F whd %{tr'} >exec_inf_aux_unfold whd in ⊢ (???%?); >F whd in ⊢ (???%?); @steps_stop |
---|
74 | ] |
---|
75 | | #n' #IH #s #tr whd in ⊢ (% → ?); |
---|
76 | cases (step … s) [ #o #K * | 3: #m * ] * #tr1 #s1 |
---|
77 | whd in ⊢ (% → ?); cases (inv s1) [2: *] |
---|
78 | whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %); |
---|
79 | [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1 |
---|
80 | cases (IH s1 ? AW1) |
---|
81 | #tr' * #s' * #p #H1 %{(tr1⧺tr')} %{s'} |
---|
82 | lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %); |
---|
83 | [ #NF <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF1 |
---|
84 | @steps_steps >NF in H1; // |
---|
85 | | #r #F <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (??(λ_.???%?)); >NF1 |
---|
86 | >F in H1; whd in ⊢ (% → ?); * #tr1 #H1 %{tr1} |
---|
87 | @steps_steps @H1 |
---|
88 | ] |
---|
89 | ] qed. |
---|
90 | |
---|
91 | (* In some places we do not consider wrong executions. *) |
---|
92 | |
---|
93 | coinductive not_wrong (state:Type[0]) : execution state io_out io_in → Prop ≝ |
---|
94 | | nw_stop : ∀tr,i,s. not_wrong state (e_stop … tr i s) |
---|
95 | | nw_step : ∀tr,s,e. not_wrong state e → not_wrong state (e_step … tr s e) |
---|
96 | | nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k). |
---|
97 | |
---|
98 | lemma not_wrong_not_wrong : ∀state,m. |
---|
99 | ¬ (not_wrong state (e_wrong … m)). |
---|
100 | #state #m % #NW inversion NW |
---|
101 | #A #B #C #D #E destruct |
---|
102 | qed. |
---|
103 | |
---|
104 | lemma not_wrong_steps : ∀state,e,e',tr. |
---|
105 | steps state tr e e' → |
---|
106 | not_wrong state e → |
---|
107 | not_wrong state e'. |
---|
108 | #state #e0 #e0' #tr0 #S elim S |
---|
109 | [ // |
---|
110 | | #tr #s #e #NW inversion NW |
---|
111 | #A #B #C #D #E try #F destruct // |
---|
112 | | #tr #s #e #tr' #e' #S' #IH #NW @IH |
---|
113 | inversion NW |
---|
114 | #A #B #C #D #E try #F destruct // |
---|
115 | ] qed. |
---|
116 | |
---|
117 | lemma not_wrong_init : ∀FE,p. |
---|
118 | not_wrong ? (exec_inf … FE p) → |
---|
119 | ∃s. make_initial_state … p = OK ? s. |
---|
120 | #FE #p whd in ⊢ (??% → ?); |
---|
121 | cases (make_initial_state ??? p) |
---|
122 | [ /2/ |
---|
123 | | normalize #m #NW @⊥ |
---|
124 | inversion NW #H1 #H2 #H3 #H4 try #H5 destruct |
---|
125 | ] qed. |
---|
126 | |
---|
127 | |
---|
128 | (* One execution is simulated by another, but possibly using a different number |
---|
129 | of steps. Note that we have to allow for several steps at the end to make |
---|
130 | the trace match up. |
---|
131 | |
---|
132 | This assumes that the overall traces are exactly the same; this may not be |
---|
133 | the case everywhere and we might have to add a cost label map. (There is |
---|
134 | a separate definition for the cost labelling stage, see |
---|
135 | Clight/labelSpecification.ma.) |
---|
136 | *) |
---|
137 | |
---|
138 | coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝ |
---|
139 | | sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2. |
---|
140 | steps S1 tr e1 (e_stop … tr1 r s1) → |
---|
141 | steps S2 tr e2 (e_stop … tr2 r s2) → |
---|
142 | simulates S1 S2 e1 e2 |
---|
143 | | sim_steps : ∀tr,e1,e1',e2,e2'. |
---|
144 | steps S1 tr e1 e1' → |
---|
145 | steps S2 tr e2 e2' → |
---|
146 | simulates S1 S2 e1' e2' → |
---|
147 | simulates S1 S2 e1 e2 |
---|
148 | | sim_interact : ∀o,k1,k2. |
---|
149 | (∀i. simulates S1 S2 (k1 i) (k2 i)) → |
---|
150 | simulates S1 S2 (e_interact … o k1) (e_interact … o k2). |
---|
151 | |
---|
152 | |
---|
153 | (* Result for lifting simulations on states to simulations on execution traces. |
---|
154 | At the time of writing this hasn't been used in anger yet... |
---|
155 | |
---|
156 | This probably isn't the best route for the stages of the compiler that have |
---|
157 | results in terms of structured traces, but it should be good for the |
---|
158 | front-end. |
---|
159 | *) |
---|
160 | |
---|
161 | let corec build_cofix_simulation |
---|
162 | (FS1,FS2:fullexec io_out io_in) |
---|
163 | (g1:global … FS1) (g2:global … FS2) |
---|
164 | (SIM:state … g1 → state … g2 → Prop) |
---|
165 | (s1:state … g1) (s2:state … g2) |
---|
166 | (NF:is_final … FS1 g1 s1 = None ?) |
---|
167 | (S:SIM s1 s2) |
---|
168 | (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y) |
---|
169 | (SIM_GOOD: ∀x,y. SIM x y → |
---|
170 | not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) → |
---|
171 | is_final … FS1 g1 x = None ? → |
---|
172 | ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) ) |
---|
173 | (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1))) |
---|
174 | : simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?. |
---|
175 | lapply (SIM_GOOD … S NW NF) |
---|
176 | * #tr * #s1' * #s2' * #P1 * #P2 #S' |
---|
177 | lapply (refl ? (is_final … FS1 g1 s1')) |
---|
178 | cases (is_final … s1') in ⊢ (???% → ?); |
---|
179 | [ #NF1 |
---|
180 | @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?)) |
---|
181 | [ @(plus_exec … P1) // |
---|
182 | | @(plus_exec … P2) <SIM_FINAL // |
---|
183 | | @(not_wrong_steps … (plus_exec … P1 …)) // |
---|
184 | | // |
---|
185 | ] |
---|
186 | | #r #F1 |
---|
187 | cases (plus_final … P1 F1) #tr1' #S1 |
---|
188 | cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2 |
---|
189 | @(sim_stop … S1 S2) |
---|
190 | ] qed. |
---|
191 | |
---|
192 | theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in. |
---|
193 | ∀p1:program … FE1. ∀p2:program … FE2. |
---|
194 | let g1 ≝ make_global … p1 in |
---|
195 | let g2 ≝ make_global … p2 in |
---|
196 | ∀SIM: state … g1 → state … g2 → Prop. |
---|
197 | ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 → |
---|
198 | ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2). |
---|
199 | ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y. |
---|
200 | ∀SIM_GOOD: ∀x,y. SIM x y → |
---|
201 | not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) → |
---|
202 | is_final … FE1 g1 x = None ? → |
---|
203 | ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')). |
---|
204 | let e1 ≝ exec_inf … FE1 p1 in |
---|
205 | let e2 ≝ exec_inf … FE2 p2 in |
---|
206 | not_wrong … e1 → |
---|
207 | simulates … e1 e2. |
---|
208 | |
---|
209 | #FE1 #FE2 #p1 #p2 |
---|
210 | letin g1 ≝ (make_global … p1) |
---|
211 | letin g2 ≝ (make_global … p2) |
---|
212 | #SIM #SIM_INIT #SIM_FINAL #SIM_GOOD |
---|
213 | #NW |
---|
214 | cases (not_wrong_init … p1 NW) |
---|
215 | #s1 #I1 |
---|
216 | cases (SIM_INIT … I1) #s2 * #I2 #S |
---|
217 | whd in NW:(??%) ⊢ (???%%); |
---|
218 | >I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%); |
---|
219 | change with g1 in match (make_global … p1); |
---|
220 | change with g2 in match (make_global … p2); |
---|
221 | |
---|
222 | >exec_inf_aux_unfold whd in ⊢ (??% → ???%?); |
---|
223 | lapply (SIM_FINAL … S) |
---|
224 | lapply (refl ? (is_final … s1)) |
---|
225 | cases (is_final … s1) in ⊢ (???% → %); |
---|
226 | [ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%); |
---|
227 | <F2 whd in ⊢ (? → ???%%); #NW |
---|
228 | @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption |
---|
229 | [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ] |
---|
230 | | #r #F1 #F2 #NW whd in ⊢ (???%%); |
---|
231 | >exec_inf_aux_unfold whd in ⊢ (???%%); |
---|
232 | <F2 whd in ⊢ (???%%); |
---|
233 | @(sim_stop … (steps_stop …) (steps_stop …)) |
---|
234 | ] qed. |
---|
235 | |
---|