1 | include "Clight/switchRemoval.ma". |
---|
2 | include "Clight/labelSimulation.ma". |
---|
3 | |
---|
4 | |
---|
5 | lemma after_aux_result : ∀avs,n,s,tr,P. |
---|
6 | after_aux avs n s tr P → |
---|
7 | ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉). |
---|
8 | #avs #n elim n |
---|
9 | [ #s #tr #P #A whd in A; %{tr} %{s} % [ @A | % ] |
---|
10 | | #n' #IH #s #tr #P |
---|
11 | whd in ⊢ (% → ?); |
---|
12 | lapply (refl ? (is_final … s)) |
---|
13 | cases (is_final … s) in ⊢ (???% → %); |
---|
14 | [ #F whd in ⊢ (% → ?); |
---|
15 | lapply (refl ? (step … s)) |
---|
16 | cases (step … s) in ⊢ (???% → %); |
---|
17 | [ #o #k #_ * |
---|
18 | | * #tr1 #s1 #ST whd in ⊢ (% → ?); |
---|
19 | cases n' in IH ⊢ %; |
---|
20 | [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd % | skip ] | skip ] |
---|
21 | | #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %); |
---|
22 | [ #INV #AF |
---|
23 | cases (IH … AF) #tr' * #s' * #p #AF' |
---|
24 | % [2: % [2: %{p} whd >F whd >ST whd >INV @AF' | skip ] | skip ] |
---|
25 | | #_ * |
---|
26 | ] |
---|
27 | ] |
---|
28 | | #m #_ * |
---|
29 | ] |
---|
30 | | #r #F * |
---|
31 | ] |
---|
32 | ] qed. |
---|
33 | |
---|
34 | lemma after_n_result : ∀n,O,I,exec,g,s,P,inv. |
---|
35 | after_n_steps n O I exec g s inv P → |
---|
36 | ∃tr',s'. |
---|
37 | P tr' s' ∧ |
---|
38 | after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉). |
---|
39 | #n #O #I #exec #g #s #P #inv #A |
---|
40 | cases (after_aux_result … A) #tr * #s' * #p #A' |
---|
41 | %{tr} %{s'} %{p} @A' |
---|
42 | qed. |
---|
43 | |
---|
44 | |
---|
45 | lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s. |
---|
46 | after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) → |
---|
47 | ∃tr1,tr2,s1. |
---|
48 | is_final … exec g s = None ? ∧ |
---|
49 | step … exec g s = Value … 〈tr1,s1〉 ∧ |
---|
50 | tr = tr1⧺tr2 ∧ |
---|
51 | after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉). |
---|
52 | #n #O #I #exec #g #tr #s' #s #A |
---|
53 | cases (after_1_of_n_steps … A) |
---|
54 | #tr1 * #s1 * * * #F #ST #_ #A' |
---|
55 | cases (after_n_result … A') |
---|
56 | #tr'' * #s'' * #E #A'' destruct |
---|
57 | % [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ] |
---|
58 | qed. |
---|
59 | |
---|
60 | theorem steps_with_labels : ∀ge,ge'. |
---|
61 | related_globals_gen … label_fundef ge ge' → |
---|
62 | ∀n,s1,s1',tr,s2. |
---|
63 | state_with_labels s1 s1' → |
---|
64 | after_n_steps (S n) … clight_exec ge s1 (λ_.true) (λtr',s'.〈tr',s'〉 = 〈tr,s2〉) → |
---|
65 | ∃m. after_n_steps (S m) … clight_exec ge' s1' (λ_.true) |
---|
66 | (λtr',s2'. trace_with_extra_labels tr tr' ∧ |
---|
67 | state_with_labels s2 s2'). |
---|
68 | #ge #ge' #RG |
---|
69 | #n elim n |
---|
70 | [ #s1 #s1' #tr #s2 #SWL #AFTER |
---|
71 | cases (after_1_step … AFTER) #tr' * #s' * * #F1 #ST1 #E destruct |
---|
72 | @(step_with_labels … RG … ST1) // |
---|
73 | | #n #IH #s1 #s1' #tr #s2 #SWL #AFTER |
---|
74 | cases (after_1_of_n_steps' … AFTER) #tr1 * #tr2 * #s' * * * #F1 #ST1 #E #AFTER' |
---|
75 | destruct |
---|
76 | cases (step_with_labels … RG … SWL ST1) #m1 #AF1 |
---|
77 | cases (after_n_result … AF1) #tr2 * #s2' * * #TWEL #SWL' #AF'' |
---|
78 | cases (IH … SWL' AFTER') |
---|
79 | #m2 #AF2 |
---|
80 | %{(m1+S m2)} |
---|
81 | @(after_n_m (S m1) (S m2) … AF2) // |
---|
82 | @(after_n_covariant … AF'') |
---|
83 | |
---|
84 | #tr #s #E destruct %{(refl ??)} |
---|
85 | #tr'' #s'' * #TWEL #SWL % /2/ |
---|
86 | ] qed. |
---|
87 | |
---|
88 | lemma interactive_switch_step : ∀ge,ge'. |
---|
89 | related_globals … fundef_switch_removal ge ge' → |
---|
90 | ∀s1,s1',o,k. |
---|
91 | exec_step ge s1 = Interact … o k → |
---|
92 | switch_state_sim ge s1 s1' → |
---|
93 | ∃k'. |
---|
94 | exec_step ge' s1' = Interact … o k' ∧ |
---|
95 | ∀i. ∃tr,s2. |
---|
96 | k i = Value … 〈tr,s2〉 ∧ |
---|
97 | ∃s2'. |
---|
98 | k' i = Value … 〈tr,s2'〉 ∧ |
---|
99 | switch_state_sim ge s2 s2'. |
---|
100 | #ge #ge' #RG #s1 #s1' #o #k #EX |
---|
101 | cases (exec_step_interaction … EX) |
---|
102 | #vf * #fn * #argtys * #retty * #vargs * #k' * #m #E |
---|
103 | destruct |
---|
104 | #S inversion S |
---|
105 | [1,3,4: #H1 #H2 #H3 #H4 destruct |
---|
106 | #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct |
---|
107 | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 destruct |
---|
108 | ] |
---|
109 | #s_vf #s_fd #s_args #s_k #s_k_ext #s_m #s_m_ext #s_writeable #s_me #s_H |
---|
110 | #E1 #E2 #E3 destruct |
---|
111 | whd in EX:(??%?); |
---|
112 | @(bindIO_res_interact ?????????? EX) -EX |
---|
113 | #vs #CHECK #EX whd in EX:(??%?); destruct |
---|
114 | % [2: % |
---|
115 | [ whd in ⊢ (??%?); |
---|
116 | >CHECK in ⊢ (??%?); |
---|
117 | whd in ⊢ (??%?); |
---|
118 | @refl |
---|
119 | | #i |
---|
120 | % [2: % [2: % |
---|
121 | [ @refl |
---|
122 | | % [2: % |
---|
123 | [ @refl |
---|
124 | | @(sws_returnstate … s_me) // ] |
---|
125 | | skip ] ] | skip ] |
---|
126 | ] ]| skip |
---|
127 | ] qed. |
---|
128 | |
---|
129 | lemma Value_eq_l : ∀tr,s,tr',s'. |
---|
130 | Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 → |
---|
131 | tr = tr'. |
---|
132 | #tr #s #tr' #s' #E destruct % |
---|
133 | qed. |
---|
134 | |
---|
135 | lemma Value_eq_r : ∀tr,s,tr',s'. |
---|
136 | Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 → |
---|
137 | s = s'. |
---|
138 | #tr #s #tr' #s' #E destruct % |
---|
139 | qed. |
---|
140 | |
---|
141 | let corec build_exec |
---|
142 | (ge1,ge2,ge3:genv) |
---|
143 | (SRG:related_globals … fundef_switch_removal ge1 ge2) |
---|
144 | (RG:related_globals_gen … label_fundef ge2 ge3) |
---|
145 | (s1,s2,s3:state) |
---|
146 | (S1:switch_state_sim ge1 s1 s2) |
---|
147 | (S2:state_with_labels s2 s3) |
---|
148 | (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))) |
---|
149 | : sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge3 (exec_step ge3 s3)) ≝ |
---|
150 | match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with |
---|
151 | [ nw_stop tr i s ⇒ ? |
---|
152 | | nw_step tr1 s1' e1 NW1 ⇒ ? |
---|
153 | | nw_interact o k NWk ⇒ ? |
---|
154 | ] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))). |
---|
155 | [ #E1 |
---|
156 | cases (exec_inf_stops_at_final ?? clight_fullexec … E1) |
---|
157 | #EX1 #F1 |
---|
158 | cases (switch_removal_correction … SRG … S1 EX1) |
---|
159 | #n1 #A1 |
---|
160 | cases (after_n_result … A1) #tr1' * #s1' * * #E destruct #S1' #A1' |
---|
161 | cases (steps_with_labels … RG … S2 A1') |
---|
162 | #n2 #A2 cases (after_inv clight_fullexec ????? A2) #tr' * #s' * * #TWL #S' |
---|
163 | lapply F1 whd in ⊢ (??%? → ?); >(switch_final_related … S1') >(final_related … S') #F3 |
---|
164 | whd in match (is_final … s'); >F3 * |
---|
165 | #tr2' #S2 |
---|
166 | @(swl_stop … S2 TWL) |
---|
167 | | #E1 |
---|
168 | cases (extract_step ?? clight_fullexec … E1) |
---|
169 | #EX1 #E1' |
---|
170 | cases (switch_removal_correction … SRG … S1 EX1) |
---|
171 | #n1 #A1 |
---|
172 | cases (after_n_result … A1) #tr1' * #s2' * * #E @(match E with [refl ⇒ ?]) #S1' #A1' |
---|
173 | cases (steps_with_labels … RG … S2 A1') |
---|
174 | #n #AF cases (after_inv clight_fullexec ????? AF) #tr' * #s' * * #TWL #S' |
---|
175 | whd in match (is_final … s'); lapply (refl ? (is_final s')) |
---|
176 | cases (is_final s') in ⊢ (???% → %); |
---|
177 | [ #NF #H whd in H; @(swl_steps … H) // |
---|
178 | @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?]) |
---|
179 | @(build_exec … SRG RG … S1' S') >E1' in NW1; // |
---|
180 | | #r <(final_related … S') <(switch_final_related … S1') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?); |
---|
181 | >(exec_e_step_not_final ?? clight_fullexec … E1) #E' destruct |
---|
182 | ] |
---|
183 | | #E1 |
---|
184 | cases (extract_interact ?? clight_fullexec … E1) |
---|
185 | #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk |
---|
186 | cases (interactive_switch_step … SRG … EX1 S1) #k2' * #EX2 #H2 |
---|
187 | cases (interactive_step_with_labels … RG … EX2 S2) |
---|
188 | #k3' * #EX3 #H3 @(match sym_eq … EX3 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%); |
---|
189 | @swl_interact |
---|
190 | #i cases (H3 i) #tr2 * #s2' * #K2 * #tr3 * #s3' * * #K3 #TR2 #S2' |
---|
191 | cases (H2 i) #tr1 * #s1' * #K1 * #s2x' * @(match sym_eq … K2 with [refl ⇒ ?]) #Ex |
---|
192 | @(match (Value_eq_r … Ex) with [refl ⇒ ?]) #S1' |
---|
193 | lapply (NWk i) |
---|
194 | @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); |
---|
195 | @(match sym_eq … (switch_final_related … S1') with [refl ⇒ ?]) @(match sym_eq … (final_related … S2') with [refl ⇒ ?]) |
---|
196 | @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge3 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); |
---|
197 | @(match sym_eq … K3 with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????); |
---|
198 | cases (is_final s3') |
---|
199 | [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) |
---|
200 | [ destruct // |
---|
201 | | @build_exec // |
---|
202 | inversion NW' |
---|
203 | [ #H1 #H2 #H3 #H4 #H5 destruct |
---|
204 | | #H7 #H8 #H9 #H10 #H11 #H12 destruct // |
---|
205 | | #H14 #H15 #H16 #H17 #H18 destruct |
---|
206 | ] |
---|
207 | ] |
---|
208 | | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) destruct // |
---|
209 | ] |
---|
210 | ] qed. |
---|
211 | |
---|
212 | theorem switch_and_labelling_sim : ∀p. |
---|
213 | let e1 ≝ exec_inf … clight_fullexec p in |
---|
214 | let e2 ≝ exec_inf … clight_fullexec (\fst (clight_label (program_switch_removal p))) in |
---|
215 | not_wrong state e1 → |
---|
216 | sim_with_labels e1 e2. |
---|
217 | #p letin p' ≝ (program_switch_removal p) |
---|
218 | #NW |
---|
219 | cases (not_wrong_init clight_fullexec p NW) |
---|
220 | whd in ⊢ (% → ??%? → ?); #s1 #I1 |
---|
221 | cases (initial_state_in_switch_simulation … I1) |
---|
222 | #s' * * change with p' in match (program_switch_removal p); #I' #RG' #S' |
---|
223 | cases (initial_state_in_simulation … I') |
---|
224 | #s2 * #I2 |
---|
225 | |
---|
226 | whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %; |
---|
227 | letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %; |
---|
228 | change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p); |
---|
229 | >I1 |
---|
230 | |
---|
231 | whd in match (exec_inf ????); |
---|
232 | letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p'))) |
---|
233 | change with (make_initial_state (\fst (clight_label p'))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p'))); |
---|
234 | >I2 |
---|
235 | |
---|
236 | whd in ⊢ (??% → ? → ?%%); |
---|
237 | >exec_inf_aux_unfold |
---|
238 | >exec_inf_aux_unfold |
---|
239 | whd in ⊢ (??% → ? → ?%%); |
---|
240 | whd in match (is_final ?????); |
---|
241 | >(initial_state_is_not_final … I1) |
---|
242 | whd in match (is_final ?????); |
---|
243 | >(initial_state_is_not_final … I2) |
---|
244 | whd in ⊢ (??% → ? → ?%%); |
---|
245 | |
---|
246 | #NW #S |
---|
247 | @(swl_steps E0 E0) |
---|
248 | [ 2: @steps_step | skip | // | @(build_exec … RG' … S' S) |
---|
249 | [ whd in match ge2; >unfold_clight_label |
---|
250 | @transform_program_gen_related |
---|
251 | | inversion NW |
---|
252 | [ #tr #i #s #E1 #E2 destruct |
---|
253 | | #trX #sX #eX #NWX #E1X #E2X destruct // |
---|
254 | | #H1 #H2 #H3 #H4 #H5 destruct |
---|
255 | ] |
---|
256 | ] |
---|
257 | ] qed. |
---|
258 | |
---|
259 | |
---|