source: src/Clight/SwitchAndLabel.ma @ 3047

Last change on this file since 3047 was 3047, checked in by campbell, 7 years ago

Switch removal and labelling combined.

File size: 9.5 KB
Line 
1include "Clight/switchRemoval.ma".
2include "Clight/labelSimulation.ma".
3
4
5lemma 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
34lemma 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
40cases (after_aux_result … A) #tr * #s' * #p #A'
41%{tr} %{s'} %{p} @A'
42qed.
43
44
45lemma 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
53cases (after_1_of_n_steps … A)
54#tr1 * #s1 * * * #F #ST #_ #A'
55cases (after_n_result … A')
56#tr'' * #s'' * #E #A'' destruct
57% [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ]
58qed.
59
60theorem 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
88lemma 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
101cases (exec_step_interaction … EX)
102#vf * #fn * #argtys * #retty * #vargs * #k' * #m #E
103destruct
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
111whd 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
129lemma 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 %
133qed.
134
135lemma 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 %
139qed.
140
141let 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)) ≝
150match 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
212theorem 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
219cases (not_wrong_init clight_fullexec p NW)
220whd in ⊢ (% → ??%? → ?); #s1 #I1
221cases (initial_state_in_switch_simulation … I1)
222#s' * * change with p' in match (program_switch_removal p); #I' #RG' #S'
223cases (initial_state_in_simulation … I')
224#s2 * #I2
225
226whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
227letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
228change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
229>I1
230
231whd in match (exec_inf ????);
232letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p')))
233change with (make_initial_state (\fst (clight_label p'))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p')));
234>I2
235
236whd in ⊢ (??% → ? → ?%%);
237>exec_inf_aux_unfold
238>exec_inf_aux_unfold
239whd in ⊢ (??% → ? → ?%%);
240whd in match (is_final ?????);
241>(initial_state_is_not_final … I1)
242whd in match (is_final ?????);
243>(initial_state_is_not_final … I2)
244whd 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
Note: See TracBrowser for help on using the repository browser.