source: src/Clight/SwitchAndLabel.ma @ 3081

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

Tidy up recent work a little.

File size: 8.1 KB
Line 
1include "Clight/switchRemoval.ma".
2include "Clight/labelSimulation.ma".
3
4(* Combine the results about switch removal and labelling to provide a single
5   result linking the input Clight program with the cost labelled Clight
6   program. *)
7
8(* First lift the step result for labelling to a finite run of steps. *)
9
10lemma steps_with_labels : ∀ge,ge'.
11  related_globals_gen … label_fundef ge ge' →
12  ∀n,s1,s1',tr,s2.
13  state_with_labels s1 s1' →
14  after_n_steps (S n) … clight_exec ge s1 (λ_.true) (λtr',s'.〈tr',s'〉 = 〈tr,s2〉) →
15   ∃m. after_n_steps (S m) … clight_exec ge' s1' (λ_.true)
16   (λtr',s2'. trace_with_extra_labels tr tr' ∧
17              state_with_labels s2 s2').
18#ge #ge' #RG
19#n elim n
20[ #s1 #s1' #tr #s2 #SWL #AFTER
21  cases (after_1_step … AFTER) #tr' * #s' * * #F1 #ST1 #E destruct
22  @(step_with_labels … RG … ST1) //
23| #n #IH #s1 #s1' #tr #s2 #SWL #AFTER
24  cases (after_1_of_n_steps' … AFTER) #tr1 * #tr2 * #s' * * * #F1 #ST1 #E #AFTER'
25  destruct
26  cases (step_with_labels … RG … SWL ST1) #m1 #AF1
27  cases (after_n_result … AF1) #tr2 * #s2' * * #TWEL #SWL' #AF''
28  cases (IH … SWL' AFTER')
29  #m2 #AF2
30  %{(m1+S m2)}
31  @(after_n_m (S m1) (S m2) … AF2) //
32  @(after_n_covariant … AF'')
33 
34  #tr #s #E destruct %{(refl ??)}
35  #tr'' #s'' * #TWEL #SWL % /2/
36] qed.
37
38lemma interactive_switch_step : ∀ge,ge'.
39  related_globals … fundef_switch_removal ge ge' →
40  ∀s1,s1',o,k.
41  exec_step ge s1 = Interact … o k →
42  switch_state_sim ge s1 s1' →
43  ∃k'.
44      exec_step ge' s1' = Interact … o k' ∧
45  ∀i. ∃tr,s2.
46    k i = Value … 〈tr,s2〉 ∧
47    ∃s2'.
48      k' i = Value … 〈tr,s2'〉 ∧
49      switch_state_sim ge s2 s2'.
50#ge #ge' #RG #s1 #s1' #o #k #EX
51cases (exec_step_interaction … EX)
52#vf * #fn * #argtys * #retty * #vargs * #k' * #m #E
53destruct
54#S inversion S
55[1,3,4: #H1 #H2 #H3 #H4 destruct
56  #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
57  #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 destruct
58]
59#s_vf #s_fd #s_args #s_k #s_k_ext #s_m #s_m_ext #s_writeable #s_me #s_H
60#E1 #E2 #E3 destruct
61whd in EX:(??%?);
62@(bindIO_res_interact ?????????? EX) -EX
63#vs #CHECK #EX whd in EX:(??%?); destruct
64% [2: %
65[ whd in ⊢ (??%?);
66  >CHECK in ⊢ (??%?);
67  whd in ⊢ (??%?);
68  @refl
69| #i
70  % [2: % [2: %
71  [ @refl
72  | % [2: %
73    [ @refl
74    | @(sws_returnstate … s_me) // ]
75    | skip ] ] | skip ]
76  ] ]| skip
77] qed.
78
79lemma Value_eq_l : ∀tr,s,tr',s'.
80  Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 →
81  tr = tr'.
82#tr #s #tr' #s' #E destruct %
83qed.
84
85lemma Value_eq_r : ∀tr,s,tr',s'.
86  Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 →
87  s = s'.
88#tr #s #tr' #s' #E destruct %
89qed.
90
91(* Now build the coinduction simulation, taking one step to many after switch
92   removal, then use steps_with_labels to take those to the cost labelled
93   version. *)
94
95let corec build_exec
96  (ge1,ge2,ge3:genv)
97  (SRG:related_globals … fundef_switch_removal ge1 ge2)
98  (RG:related_globals_gen … label_fundef ge2 ge3)
99  (s1,s2,s3:state)
100  (S1:switch_state_sim ge1 s1 s2)
101  (S2:state_with_labels s2 s3)
102  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
103: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge3 (exec_step ge3 s3)) ≝
104match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
105[ nw_stop tr i s ⇒ ?
106| nw_step tr1 s1' e1 NW1 ⇒ ?
107| nw_interact o k NWk ⇒ ?
108] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
109[ #E1
110  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
111  #EX1 #F1
112  cases (switch_removal_correction … SRG … S1 EX1)
113  #n1 #A1
114  cases (after_n_result … A1) #tr1' * #s1' * * #E destruct #S1' #A1'
115  cases (steps_with_labels … RG … S2 A1')
116  #n2 #A2 cases (after_inv clight_fullexec ????? A2) #tr' * #s' * * #TWL #S'
117  lapply F1 whd in ⊢ (??%? → ?); >(switch_final_related … S1') >(final_related … S') #F3
118    whd in match (is_final … s'); >F3 *
119    #tr2' #S2
120    @(swl_stop … S2 TWL)
121| #E1
122  cases (extract_step ?? clight_fullexec … E1)
123  #EX1 #E1'
124  cases (switch_removal_correction … SRG … S1 EX1)
125  #n1 #A1
126  cases (after_n_result … A1) #tr1' * #s2' * * #E @(match E with [refl ⇒ ?]) #S1' #A1'
127  cases (steps_with_labels … RG … S2 A1')
128  #n #AF cases (after_inv clight_fullexec ????? AF) #tr' * #s' * * #TWL #S'
129  whd in match (is_final … s'); lapply (refl ? (is_final s'))
130  cases (is_final s') in ⊢ (???% → %);
131  [ #NF #H whd in H; @(swl_steps … H) //
132    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
133    @(build_exec … SRG RG … S1' S') >E1' in NW1; //
134  | #r <(final_related … S') <(switch_final_related … S1') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?);
135    >(exec_e_step_not_final ?? clight_fullexec … E1) #E' destruct
136  ]
137| #E1
138  cases (extract_interact ?? clight_fullexec … E1)
139  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
140  cases (interactive_switch_step … SRG … EX1 S1) #k2' * #EX2 #H2
141  cases (interactive_step_with_labels … RG … EX2 S2)
142  #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 ⊢ (??%);
143  @swl_interact
144  #i cases (H3 i) #tr2 * #s2' * #K2 * #tr3 * #s3' * * #K3 #TR2 #S2'
145  cases (H2 i) #tr1 * #s1' * #K1 * #s2x' * @(match sym_eq … K2 with [refl ⇒ ?]) #Ex
146  @(match (Value_eq_r … Ex) with [refl ⇒ ?]) #S1'
147  lapply (NWk i)
148  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????);
149  @(match sym_eq … (switch_final_related … S1') with [refl ⇒ ?]) @(match sym_eq … (final_related … S2') with [refl ⇒ ?])
150  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge3 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%);
151  @(match sym_eq … K3 with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
152  cases (is_final s3')
153  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …))
154    [ destruct //
155    | @build_exec //
156      inversion NW'
157      [ #H1 #H2 #H3 #H4 #H5 destruct
158      | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
159      | #H14 #H15 #H16 #H17 #H18 destruct
160      ]
161    ]
162  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) destruct //
163  ]
164] qed.
165
166(* And deal with the start of the program to tie up everything nicely. *)
167
168theorem switch_and_labelling_sim : ∀p.
169  let e1 ≝ exec_inf … clight_fullexec p in
170  let e2 ≝ exec_inf … clight_fullexec (\fst (clight_label (program_switch_removal p))) in
171  not_wrong state e1 →
172  sim_with_labels e1 e2.
173#p letin p' ≝ (program_switch_removal p)
174#NW
175cases (not_wrong_init clight_fullexec p NW)
176whd in ⊢ (% → ??%? → ?); #s1 #I1
177cases (initial_state_in_switch_simulation … I1)
178#s' * * change with p' in match (program_switch_removal p); #I' #RG' #S'
179cases (initial_state_in_simulation … I')
180#s2 * #I2
181
182whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
183letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
184change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
185>I1
186
187whd in match (exec_inf ????);
188letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p')))
189change with (make_initial_state (\fst (clight_label p'))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p')));
190>I2
191
192whd in ⊢ (??% → ? → ?%%);
193>exec_inf_aux_unfold
194>exec_inf_aux_unfold
195whd in ⊢ (??% → ? → ?%%);
196whd in match (is_final ?????);
197>(initial_state_is_not_final … I1)
198whd in match (is_final ?????);
199>(initial_state_is_not_final … I2)
200whd in ⊢ (??% → ? → ?%%);
201
202#NW #S
203@(swl_steps E0 E0)
204[ 2: @steps_step | skip | // | @(build_exec … RG' … S' S)
205  [ whd in match ge2; >unfold_clight_label
206    @transform_program_gen_related
207  | inversion NW
208    [ #tr #i #s #E1 #E2 destruct
209    | #trX #sX #eX #NWX #E1X #E2X destruct //
210    | #H1 #H2 #H3 #H4 #H5 destruct
211    ]
212  ]
213] qed.
214
215
Note: See TracBrowser for help on using the repository browser.