source: src/Clight/labelSimulation.ma @ 2300

Last change on this file since 2300 was 2203, checked in by campbell, 9 years ago

A general result about simulations of executions.
File size: 58.8 KB
Line 
1
2include "Clight/labelSpecification.ma".
3include "Clight/CexecInd.ma".
4
5(* Useful for breaking up the labeling functions, because we don't care about
6   *which* cost labels are added here and so can throw away the resulting name
7   generator. *)
8lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D.
9  \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) =  F (\fst e).
10#A #B #C #D * //
11qed.
12
13
14(* Similarly, lemma to break up label_expr, label_exprs and label_statement in
15   the labelling functions *)
16lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0].
17  (∀u'. P (F (\fst (L syn u)) u')) →
18  P (let 〈syn',u'〉 ≝ L syn u in F syn' u').
19#Syn #syn #u #T #L #F #P
20cases (L syn u)
21#syn' #u' #H @H
22qed.
23
24lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
25  (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) →
26  P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u').
27#e #u #T #F #P #H whd in match (add_cost_expr ??);
28cases (fresh ??) #l #u' @H
29qed.
30
31
32lemma label_expr_type : ∀e,u.
33  typeof (\fst (label_expr e u)) = typeof e.
34* #e #ty #u >shift_fst //
35qed.
36
37(* Lemmas about trace_with_extra_labels *)
38
39lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
40#tr elim tr /2/
41qed.
42
43lemma twel_app : ∀tr1,tr2,tr1',tr2'.
44  trace_with_extra_labels tr1 tr1' →
45  trace_with_extra_labels tr2 tr2' →
46  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
47#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
48qed. 
49
50
51theorem label_expr_ok : ∀ge,ge',en,m.
52  related_globals … label_fundef ge ge' →
53  (∀e,v,tr.
54   exec_expr ge en m e = OK … 〈v,tr〉 →
55   ∀u. ∃tr'. exec_expr ge' en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧
56             trace_with_extra_labels tr tr') ∧
57  (∀e,ty,b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
58          ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
59                    trace_with_extra_labels tr tr').
60(* Proof goes by breaking up the execution in the hypothesis, breaking up the
61   labelling function to get a new term and executing it by rewriting what we
62   learned from the hypothesis. *)
63#ge #ge' #en #m #RG @expr_lvalue_ind_combined
64[ 1,2: normalize /3 by ex_intro, conj/
65| * //
66 [ #id #ty #IH #v #tr #EX #u
67   cases (bind_inversion ????? EX) -EX * * #b #o #tr1 * #EX1 #EX
68   cases (bind_inversion ????? EX) -EX #v2 * #EX2 #EX
69   normalize in EX; destruct
70   cases (IH … EX1 u) #tr1' * #EX1' #T1
71   %{(tr1')} % [ whd in ⊢ (??%?); >EX1' whd in ⊢ (??%?); >EX2 @refl | // ]
72 | #e1 #ty #IH #v #tr #EX #u
73   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
74   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
75   normalize in EXrem; destruct
76   cases (IH … EX1 u) #tr1' * #EX1' #twel1
77   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1'
78   whd in ⊢ (?(??%?)?); >EXl /2/
79 | #e1 #id #ty #IH #v #tr #EX #u
80   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
81   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
82   normalize in EXrem; destruct
83   cases (IH … EX1 u) #tr1' * #EX1' #twel1
84   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1'
85   whd in ⊢ (??%?); >EXl @refl
86 ]
87| #v #ty #b #o #tr #EX #u %{tr} % [
88    whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
89    [ whd in ⊢ (??%? → ??%?); >(rg_find_symbol … RG) //
90    | #b // ]
91  | // ]
92| #e1 #ty #IH #b #o #tr #EX #u
93  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
94  cases (IH … EX1 u) #tr1' * #EX1' #twel1
95  %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1'
96  whd in ⊢ (?(??%?)?);
97  cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/
98| #ty' #e1 #ty #IH #v #tr #EX #u
99  cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
100  cases (IH … EX1 u) #tr1' * #EX1' #twel1
101  %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?);
102  whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1'
103  whd in ⊢ (?(??%?)?);
104  cases ty' in EX1rem ⊢ %;
105  [ 4: #ty' normalize #E destruct /2/
106  | *: normalize #A try #B try #C try #D destruct
107  ]
108| #ty #op #e1 #IH #v #tr #EX #u
109  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
110  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem
111  normalize in EXrem; destruct
112  cases (IH … EX1 u) #tr1' * #EX1' #twel1
113  %{tr1'} % // >shift_fst
114  whd in ⊢ (??(????(?(???%)?))?);
115  @label_gen_elim #u2
116  whd in ⊢ (??%?); >EX1'
117  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
118| #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX
119  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
120  cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem
121  cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop'
122  #u
123  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
124  >shift_fst
125  whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
126  @label_gen_elim #u2
127  cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
128  @label_gen_elim #u3 %{(tr1'⧺tr2')}
129  whd in ⊢ (?(??%?)?); >EX1'
130  whd in ⊢ (?(??%?)?); >EX2'
131  whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop
132  normalize in EXop'; destruct % /2/
133| #ty #ty' #e1 #IH #v #tr #EX #u
134  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
135  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem
136  normalize in EX2rem; destruct
137  cases (IH … EX1 u) #tr1' * #EX1' #twel1
138  %{tr1'} % // >shift_fst >shift_fst
139  whd in ⊢ (??%?); >EX1'
140  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
141| #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u
142  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
143  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
144  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
145  normalize in EX2rem; destruct
146  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
147  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
148  @label_gen_elim #u2
149  @label_gen_elim #u3
150  @add_cost_expr_elim #u4 #l4
151  @label_gen_elim #u5
152  @add_cost_expr_elim #u6 #l6
153  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
154  [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
155  whd in ⊢ (?(??%?)?); >EX1'
156  whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
157  whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx'
158  normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
159| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
160  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
161  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
162  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
163  @label_gen_elim #u2
164  @label_gen_elim #u3
165  @add_cost_expr_elim #u4 #l4
166  @add_cost_expr_elim #u5 #l5
167  [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
168    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
169    -EX1rem -EXguardrem -EX2rem
170    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
171    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
172    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
173    whd in ⊢ (?(??%?)?); >EX1'
174    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
175    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
176    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
177    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
178    whd in EX3rem:(??%%) ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
179  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
180    %{(tr1'⧺E0⧺Echarge l5)}
181    whd in ⊢ (?(??%?)?); >EX1'
182    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
183    whd in EXguardrem:(??%%); destruct % // <(E0_right tr) @twel_app /2/
184  ]
185| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
186  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
187  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
188  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
189  @label_gen_elim #u2
190  @add_cost_expr_elim #u4 #l4
191  @label_gen_elim #u3
192  @add_cost_expr_elim #u5 #l5
193  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
194    %{(tr1'⧺Echarge l4)}
195    whd in ⊢ (?(??%?)?); >EX1'
196    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
197    whd in EXguardrem:(??%%) ⊢ %; destruct % // <(E0_right tr) /3/
198  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
199    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
200    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
201    cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2
202    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
203    whd in ⊢ (?(??%?)?); >EX1'
204    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
205    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
206    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
207    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
208    whd in EX3rem:(??%%) ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
209  ]
210| #ty #ty' #v #tr normalize /3/
211| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
212  [ 7: #id #fl #IH #EX
213    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
214    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
215    whd in EXoffrem:(???%); destruct >shift_fst >shift_fst
216    cases (IH … EX1 u) #tr1' * #EX1' #twel1
217    %{tr1'} % //
218    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
219    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
220  | 8: #id #fl #IH #EX
221    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
222    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
223    cases (IH … EX1 u) #tr1' * #EX1' #twel1
224    %{tr1'} % //
225    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
226    whd in ⊢ (??%?); @refl
227  | *: normalize #A #B try #C try #D try #F destruct
228  ]
229| #ty #l #e1 #IH #v #tr #EX #u
230  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
231  whd in EX1rem:(???%); destruct
232  cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)}
233  >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1'
234  whd in ⊢ (?(??%?)?); /3/
235| #e1 #ty #NLV #b #o #tr #EX @⊥
236  cases e1 in NLV EX; normalize //
237  #A #B #C try #D try #F destruct
238] qed.
239
240lemma label_exprs_ok : ∀ge,ge'.
241   related_globals … label_fundef ge ge' →
242   ∀en,m,es,vs,tr.
243   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
244   ∀u. ∃tr'. exec_exprlist ge' en m (\fst (label_exprs es u)) = OK … 〈vs,tr'〉 ∧
245             trace_with_extra_labels tr tr'.
246#ge #ge' #RG #en #m #es elim es
247[ #vs #tr #EX whd in EX:(??%?); destruct #u %{E0} /2/
248| #e #tl #IH #vs #tr #EX
249  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
250  cases (bind_inversion ????? EX) -EX * #tl' #tr' * #EX2 #EX
251  whd in EX:(??%%); destruct
252  #u whd in match (label_exprs ??); @label_gen_elim #u' >shift_fst
253  cases (proj1 ?? (label_expr_ok ge ge' en m RG) ??? EX1 u) #tr1' * #EX1' #T1
254  cases (IH … EX2 u') #tr'' * #EX2' #T2
255  % [2: % [ whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
256    whd in ⊢ (??%?); >EX2' in ⊢ (??%?); @refl
257  | /2/ ] | skip ]
258] qed.
259
260
261(* Now we move on to describe the simulation relation.  First, relate the
262   continuations. *)
263inductive cont_with_labels : cont → cont → Prop ≝
264| cwl_stop : cont_with_labels Kstop Kstop
265| cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
266| cwl_while : ∀ue,e,us,s,cs,cpost,k,k'.
267    cont_with_labels k k' →
268    cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
269| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
270    cont_with_labels k k' →
271    cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
272| cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
273    cont_with_labels k k' →
274    cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k'))
275| cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
276| cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
277| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
278| cwl_call : ∀r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (label_function f) en k')
279| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
280    cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k').
281
282lemma call_cont_with_labels : ∀k,k'.
283  cont_with_labels k k' →
284  cont_with_labels (call_cont k) (call_cont k').
285#k0 #k0' #K elim K /2/
286qed.
287
288(* Now define almost all of the simulation relation... *)
289inductive state_with_labels_partial : state → state → Prop ≝
290| swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
291(* Extra matching states that we can reach that don't quite correspond to the
292   labelling function *)
293| swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
294    state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
295| swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
296    state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
297| swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
298    state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
299(* and the rest *)
300| swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)
301| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
302| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
303.
304
305(* ... and add the states where the cases from switch statements are expanded.
306   We do these separately because in the LSdefault case we have to execute a
307   cost label alongside an arbitrary statement, and we want to reuse the result
308   on arbitrary statements we get for state_with_labels_partial. *)
309inductive state_with_labels : state → state → Prop ≝
310| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
311| swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' →
312    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
313                      (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
314.
315
316(* Some details are invariant under labelling. *)
317lemma label_function_return : ∀f.
318  fn_return (label_function f) = fn_return f.
319* #rty #params #vars #body
320whd in ⊢ (??(?%)?);
321cases (label_statement ??) #body' #u'
322whd in ⊢ (??(?%)?);
323cases (add_cost_before ??) #body'' #u''
324//
325qed.
326
327lemma label_expr_fun_typeof : ∀a,u.
328  fun_typeof (\fst (label_expr a u)) = fun_typeof a.
329#a #u whd in ⊢ (??%?); >label_expr_type @refl
330qed.
331
332lemma label_fundef_typeof_fundef : ∀fd.
333  type_of_fundef (label_fundef fd) = type_of_fundef fd.
334* //
335* #rty #args #vars #body
336normalize cases (label_statement ??) #body' #u
337normalize cases (fresh ??) //
338qed.
339
340lemma label_fn_params : ∀f.
341  fn_params (label_function f) = fn_params f.
342* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
343qed.
344
345lemma label_fn_vars : ∀f.
346  fn_vars (label_function f) = fn_vars f.
347* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
348qed.
349
350(* Some annoying rewrite rules *)
351lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
352  exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
353  exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
354#ge #e #m #a #ty #u
355whd in ⊢ (??(????(???%))?); >shift_fst @refl
356qed.
357
358lemma opt_find_funct : ∀ge,ge',m,vf,fd.
359  related_globals … label_fundef ge ge' →
360  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
361  opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd).
362#ge #ge' #m #vf #fd #RG
363lapply (rg_find_funct … RG … vf fd)
364cases (find_funct … vf)
365[ #_ #E normalize in E; destruct
366| #fd' #H #E normalize in E; destruct >(H (refl ??)) //
367] qed.
368
369lemma labelled_not_skip : ∀s,u.
370  s ≠ Sskip →
371  (\fst (label_statement s u)) ≠ Sskip.
372* #u
373[ * #H cases (H (refl ??))
374| *: #a try #b try #c try #d try #e
375     (* Use the state-monad-like structure of the labelling function to break
376        it up *)
377     whd in match (label_statement ??);
378     repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
379     % #E destruct
380] qed.
381
382lemma labelled_is_not_skip : ∀s,u.
383  s ≠ Sskip →
384  ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf.
385#s #u #NE
386cases (is_Sskip ?)
387[ #E @⊥ @(absurd ? E) @labelled_not_skip //
388| /2/
389] qed.
390
391lemma label_select_ls : ∀sz,i,ls,u.
392  ∃u'.
393    select_switch sz i (\fst (label_lstatements ls u)) =
394    \fst (label_lstatements (select_switch sz i ls) u').
395#sz #i #ls @(labeled_statements_ind … ls)
396[ #s #u % [2: whd in match (label_lstatements ??);
397  @label_gen_elim #u1 >shift_fst @refl | skip ]
398| #sz' #i' #s #tl #IH #u
399  whd in match (label_lstatements ??);
400  whd in match (select_switch ?? (LScase ????));
401  @intsize_eq_elim_elim
402  [ #NE
403    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
404    cases (IH u2)
405    #u4 #E %{u4} whd in ⊢ (??%?);
406    >intsize_eq_elim_false //
407  | #E <E in i' ⊢ %; #i' whd
408    @eq_bv_elim
409    [ #Ei >Ei
410      %{u}
411      whd in match (label_lstatements (if ? then ? else ?) ?);
412      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
413      whd in ⊢ (??%?);
414      >intsize_eq_elim_true
415      >eq_bv_true
416      @refl
417    | #NEi
418      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
419       whd in ⊢ (??(λ_.??%?));
420       >intsize_eq_elim_true
421       >eq_bv_false //
422    ]
423  ]
424] qed.
425
426(* Break up labelling function in one go for statements. *)
427lemma blindly_label : ∀u,s. ∀P:statement → Prop.
428match s with
429[ Sskip ⇒ P Sskip
430| Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2)))
431| Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3)))
432| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
433| Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3))))
434| Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
435| Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
436| Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip))
437| Sbreak ⇒ P Sbreak
438| Scontinue ⇒ P Scontinue
439| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
440| Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2)))
441| Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1))))
442| Sgoto l ⇒ P (Sgoto l)
443| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
444] → P (\fst (label_statement s u)). 
445#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
446@label_gen_elim #u1 //
447@label_gen_elim #u2 //
448[ 6: >shift_fst //
449| *: @label_gen_elim #u3 //
450     @label_gen_elim #u4
451     [ @label_gen_elim #u5 >shift_fst >shift_fst //
452     | 2,3: >shift_fst >shift_fst //
453     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
454     ]
455] qed.
456
457(* Apply induction hypothesis in label_find_label proof below while getting
458   Matita to infer the continuations k0 and k0', and the universe u0, rather
459   than having to give them explicitly. *)
460lemma lfl_IH : ∀s0,lbl.
461  ∀C:option (statement×cont) → option (statement×cont) → Prop.
462  ∀IH:cont → cont → universe CostTag → Prop.
463  (∀k,k',u. cont_with_labels k k' → IH k k' u) →
464  ∀k0,k0',u0. cont_with_labels k0 k0' →
465   (IH k0 k0' u0 →
466    C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) →
467   C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0').
468/3/
469qed.
470
471(* Finding a goto label in a cost-labelled program gives a labelled version of
472   the statement and continuation found by the original function, if any. *)
473lemma label_find_label : ∀lbl,s,k,k',u.
474  cont_with_labels k k' →
475  match find_label lbl s k with
476  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
477    ∃u',cs,k1'.
478    find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
479    cont_with_labels k1 k1'
480  | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ?
481  ].
482#lbl #s @(statement_ind2 ? (λls.
483  ∀k,k',u.
484  cont_with_labels k k' →
485  match find_label_ls lbl ls k with
486  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
487    ∃u',cs,k1'.
488    find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
489    cont_with_labels k1 k1'
490  | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ?
491  ])
492 … s)
493[ #k #k' #u #F @refl
494| #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl
495| #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl
496| #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???);
497  whd in match (find_label ?? k');
498  @(lfl_IH sA … IH1) [ /2/ ]
499  cases (find_label ???)
500  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
501    @(lfl_IH … IH2) [ // ]
502    cases (find_label ???)
503    [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl
504    | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1'
505      % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ]
506    ]
507  | * #sA' #kA' whd in ⊢ (% → %);
508    * #u1' * #cs * #k1' * #FA' #K'
509         % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip]
510  ]
511| #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K
512  whd in match (find_label ?? k); whd in match (find_label ?? k');
513  whd in match (find_label ?? k');
514  @(lfl_IH  … IH1) [ // ] cases (find_label ???)
515  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
516    lapply (IH2 k k' u3 K) cases (find_label ???)
517    [ whd in ⊢ (% → %); #FIND2'
518      whd in match (find_label ???); >FIND1'
519      whd in match (find_label ???); >FIND2' @refl
520    | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2'
521      % [2: % [2: % [2: % [ whd in ⊢ (??%?);
522      whd in match (find_label ???); >FIND1' in ⊢ (??%?);
523      whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl
524      | // ]|skip]|skip]|skip]
525    ]
526  | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1'
527    % [2: % [2: % [2: % [
528      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
529      @refl | // ] |skip ]| skip ]| skip ]
530  ]
531| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
532  whd in match (find_label ?? k); normalize in match (find_label ?? k');
533  @(lfl_IH s0 … IH) [ /2/ ]
534  cases (find_label ???)
535  [ whd in ⊢ (% → %); #FIND1'
536    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
537  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
538    % [2: % [2: % [2: % [
539      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
540      @refl | // ]| skip ]| skip ]| skip ]
541  ]
542| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
543  whd in match (find_label ?? k); normalize in match (find_label ?? k');
544  @(lfl_IH s0 … IH) [ /2/ ]
545  cases (find_label ???)
546  [ whd in ⊢ (% → %); #FIND1'
547    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
548  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
549    % [2: % [2: % [2: % [
550      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
551      @refl | // ]| skip ]| skip ]| skip ]
552  ]
553| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
554  whd in match (find_label ???); normalize in match (find_label ?? k');
555  @(lfl_IH s1 … IH1) [ /2/ ]
556  cases (find_label ???)
557  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1'
558    @(lfl_IH s3 … IH3) [ /2/ ]
559    cases (find_label ???)
560    [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3'
561      @(lfl_IH s2 … IH2) [ /2/ ]
562      cases (find_label ???)
563      [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl
564      | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2'
565        % [2: % [2: % [2: % [
566         whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl
567        | // ]| skip ]| skip ]| skip ]
568      ]
569    | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3'
570        % [2: % [2: % [2: % [
571        >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl
572        | // ]| skip ]| skip ]| skip ]
573    ]
574  | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1'
575        % [2: % [2: % [2: % [
576        >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl
577        | // ]| skip ]| skip ]| skip ]
578  ]
579| //
580| //
581| #eo #k #k' #u @blindly_label #u1 //
582| #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2
583  normalize in match (find_label ???); normalize in match (find_label ???);
584  lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???)
585  [ whd in ⊢ (% → %); //
586  | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K'
587    % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip]
588  ]
589| #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs
590  whd in match (find_label ???); whd in match (find_label ?? k');
591  cases (ident_eq lbl l)
592  [ #E destruct whd
593    % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ]
594  | #NE whd in ⊢ (match % with [_⇒?|_⇒?]);
595    normalize in match (find_label ?? k');
596    @(lfl_IH s0 … IH) [ // ]
597    cases (find_label ???)
598    [ //
599    | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0
600      % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip]
601    ]
602  ]
603| //
604| #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/
605| #s0 #IH #k #k' #u whd in match (label_lstatements ??);
606  @label_gen_elim #u1 >shift_fst >shift_fst
607  whd in match (find_label_ls ???); whd in match (find_label_ls ???);
608  @IH
609| #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K
610  whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
611  @label_gen_elim #u3 >shift_fst
612  whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k');
613  @(lfl_IH s0 … IH1) [ /2/ ]
614  cases (find_label ???)
615  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0
616    lapply (IH2 k k' u2 K) cases (find_label_ls ???)
617    [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl
618    | * #stl #ktl //
619    ]
620  | * #s0' #k0' whd in ⊢ (% → %);
621    * #u' * #cs * #k1' * #FIND0 #K0 >FIND0
622    % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ]
623  ]
624] qed.
625
626lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1.
627  cont_with_labels k k' →
628  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
629  ∃u',cs,k1'.
630    find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
631    cont_with_labels k1 k1'.
632#lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
633whd in match (label_function ?);
634@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
635lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?)
636[ /2/ ]
637>FIND //
638qed.
639
640
641(* We show the main simulation in two stages.  First, we show it for all states
642   in the relation *except* those for labeled_statements, then we'll show the
643   whole thing.  This is so that we can appeal to the other cases in the proof
644   for labeled_statements. *)
645lemma step_with_labels_partial : ∀ge,ge'.
646  related_globals … label_fundef ge ge' →
647  ∀s1,s1',tr,s2.
648  state_with_labels_partial s1 s1' →
649  exec_step ge s1 = Value … 〈tr,s2〉 →
650   ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
651             trace_with_extra_labels tr tr' ∧
652             state_with_labels s2 s2'.
653
654(* General plan is like the expressions result, except that we do case analysis
655   on the simulation first, then:  break up the original execution, break up the
656   cost labelling, use the earlier results to deal with expressions, then
657   run the labelled version for enough steps.  We try to avoid having to write
658   out the final trace and state and "skip" them afterwards. *)
659#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
660[ #f #us #s #k #k' #e #m #KL cases s
661  [ #EX inversion KL
662    [ #E1 #E2 #_ destruct %{tr}
663      whd in EX:(??%?);
664      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
665      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}
666        % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E @refl
667        | // ] | /3/ ]
668      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
669      ]
670    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
671      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
672      whd in EX:(??%%); destruct
673      % [ % [ @cl_plus_one @refl | // ] | /3/ ]
674    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
675      whd in EX:(??%%); destruct
676      % [ 2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
677    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
678      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
679      cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem
680      normalize in EXbrem; destruct
681      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
682      [ % [ 2: % [ 2: % [ % [ @cl_plus_one
683        whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
684        whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
685        whd in ⊢ (??%?); @refl
686        | // ]
687        | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
688      | % [ 2: % [ 2: % [ % [ @cl_plus_succ [
689        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
690           whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
691           whd in ⊢ (??%?); @refl
692        | skip | skip
693        | 5: @cl_plus_succ [ 4: @refl | skip | skip
694        | 5: @cl_plus_one @refl | skip ] | skip ]
695        | <(E0_right tr) @twel_app /2/ ]
696        | /3/ ] | skip ] | skip ]
697      ]
698    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
699      whd in EX:(??%?); destruct
700      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]
701    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
702      whd in EX:(??%?); destruct
703      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
704    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
705      whd in EX:(??%?); destruct
706      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
707    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
708      whd in EX:(??%?); destruct
709      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
710    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
711      whd in EX:(??%?);
712      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
713      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
714        %{E0} % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
715        @refl | // ] | /4/ ] | skip ]
716      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
717      ]
718    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
719      % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ]| skip ]| skip ]
720    ]
721  | * #a1 #ty1 #a2 #EX
722    cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX
723    cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX
724    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
725    whd in EX:(??%%); destruct
726    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1
727    whd in match (label_statement ??);
728    @label_gen_elim #ua1 @label_gen_elim #ua2
729    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
730    % [2: % [2: % [ % [
731      @cl_plus_one whd in ⊢ (??%?);     
732      >exec_lvalue_labelled >EX1' in ⊢ (??%?);
733      whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
734      whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?);
735      @refl
736    | @twel_app // ] | /3/ ] | skip ] | skip ]
737  | * [2: * #er #tyr ] #ef #args #EX
738    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
739    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
740    cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
741    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
742    whd in EX:(??%%);
743    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
744    destruct
745    whd in match (label_statement ??);
746    whd in match (label_opt_expr ??);
747    [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ]
748    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1
749    @label_gen_elim #u1
750    @label_gen_elim #u2
751    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2
752    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
753    % [2,4: % [2,4: % [1,3: % [1,3:
754      @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
755      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
756      whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
757      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
758      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
759      @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
760  | #st1 #st2 #EX
761    whd in EX:(??%%); destruct
762    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
763    %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
764  | #a #st1 #st2 #EX
765    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
766    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
767    normalize in EX; destruct
768    whd in match (label_statement ??); @label_gen_elim #u1
769    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
770    @label_gen_elim #u5
771    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
772    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
773    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
774    % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9:
775      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
776      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
777      whd in ⊢ (??%?); @refl
778    | 1,2,6,7: skip
779    | 5,10: @cl_plus_one @refl
780    | *: skip
781    ]
782    | 2,4: <(E0_right tr) @twel_app /2/
783    ]| 2,4: /3/ ] | *: skip ] | *: skip ]
784  | #a #st #EX
785    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
786    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
787    normalize in EX; destruct
788    whd in match (label_statement ??); @label_gen_elim #u1
789    @label_gen_elim #u2
790    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
791    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
792    >shift_fst
793    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
794    % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
795      | 5,10: @cl_plus_succ [ 4,9:
796      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
797      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
798      whd in ⊢ (??%?); @refl
799    | 1,2,6,7: skip
800    | 5: @cl_plus_one @refl
801    | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
802    | *: skip
803    ]
804    | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
805    ]| 2,4: /4/ ] | *: skip ] | *: skip ]
806  | #a #st #EX
807    normalize in EX; destruct
808    whd in match (label_statement ??); @label_gen_elim #u1
809    @label_gen_elim #u2
810    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
811    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
812    % [2: % [2: % [ % [ @cl_plus_succ [ 4: @refl | 1,2: skip
813      | 5: @cl_plus_succ [ 4: @refl | 1,2: skip | 5: @cl_plus_one // | skip ] | skip ]
814      | /2/ ] | /4/ ] | skip ] | skip ]
815  | #st1 #a #st2 #st #EX
816    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
817    whd in EX:(??%?); >Eskip in EX; #EX
818    whd in match (label_statement ??); @label_gen_elim #u1
819    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
820    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
821    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
822    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
823      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
824      normalize in EX; destruct
825      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
826      % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
827      | 5,10: @cl_plus_succ [ 4,9:
828      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
829      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
830      whd in ⊢ (??%?); @refl
831      | 1,2,6,7: skip
832      | 5: @cl_plus_one @refl
833      | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
834      | *: skip
835      ]
836      | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
837      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
838    | whd in EX:(??%%); destruct
839      % [2: % [2: %[ %[ @cl_plus_succ [ 4: @refl | 5: @cl_plus_one
840        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
841        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
842      | skip ] | skip ]
843    ]
844  | #EX inversion KL
845    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
846    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
847    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
848    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
849    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
850    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
851    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
852    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
853    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
854    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
855    ]
856    whd in match (label_statement ??);
857    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
858    [1,11,13: @cl_plus_one @refl | 2,12,14: //
859    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
860    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
861    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip] | /2/
862    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
863    ]| *: /3 by swl_partial, swl_state/ ]|*: skip]|*: skip ]
864  | #EX inversion KL
865    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
866    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
867    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
868    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
869    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
870    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
871    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
872    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
873    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
874    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
875    ]
876    whd in match (label_statement ??);
877    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
878      [1,3,7,9,11: @cl_plus_one @refl | 5: @cl_plus_succ [4:@refl | 5:@cl_plus_one @refl | *: skip ]
879      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
880    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
881      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
882      normalize in EX; destruct
883      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
884      % [2,4: % [2,4: % [1,3: % [1,3: [ @cl_plus_one | @cl_plus_succ ] [ 1,5:
885        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
886      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
887      whd in ⊢ (??%?); @refl
888      | 6: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
889      | // | <(E0_right tr) @twel_app /2/
890      ]
891      | /3/ | /3/ ] | *: skip ] | *: skip ]
892    ]
893  | * [2: #a ] #EX
894    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
895    #Ety #EX whd in EX:(??%?);
896    [ destruct
897    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
898      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
899    | >Ety in EX; #EX
900    | @⊥ cases (fn_return f) in Ety EX;
901      [ * #H cases (H (refl ??))
902      | *: normalize #a #b #c try #d try #e destruct
903      ]
904    ]
905    whd in match (label_statement ??);
906    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
907    whd in EX:(??%%); destruct
908    % [2,4: % [2,4: % [1,3: %[1,3: @cl_plus_one
909      whd in ⊢ (??%?);
910      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
911        whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
912      | >label_function_return >Ety in ⊢ (??%?);
913      ] whd in ⊢ (??%?); @refl
914      | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip]
915  | #a #ls #EX
916    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
917    cases v1 in EX1 EX;
918    [ 2: #sz #i #EX1 #EX
919    | *: normalize #A #B try #C destruct
920    ]
921    whd in EX:(??%%); destruct
922    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
923    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
924    % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
925      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
926      ]|skip ]| skip ]
927  | #l #st #EX
928    whd in EX:(??%?); destruct
929    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
930    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
931    %[2: %[2: %[ %[ @cl_plus_succ
932      [ 4: @refl | 5: @cl_plus_one @refl | *: skip ]
933      | /2/ ] | /3/ ] |skip ]| skip ]
934  | #l #EX
935    whd in EX:(??%?);
936    @blindly_label whd
937    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
938    cases (find_label ???) in ⊢ (???% → ?);
939    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
940    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
941      cases (label_find_label_fn … KL F)
942      #u' * #cs * #k1' * #F' #K'
943      % [2: %[2: %[ %[ @cl_plus_succ
944        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @cl_plus_one @refl | *: skip ]
945        | /2/ ] | /3/ ] | skip ] | skip ]
946    ]
947  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
948    % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]| skip ]
949  ]
950| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
951  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
952  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
953  whd in EX:(??%%); destruct
954  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
955  [ % [2: % [2: % [ % [
956    @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
957                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
958               |5: @cl_plus_one @refl | *: skip ]
959    | <(E0_right tr) /3/ ]| /4 by swl_partial, swl_state, cwl_while/ ]| skip ]| skip ]
960  | % [2: % [2: % [ % [
961    @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
962                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
963    | 5: @cl_plus_succ [4: @refl
964    | 5: @cl_plus_one @refl | *: skip ] | *: skip ]
965    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
966  ]
967| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
968  whd in EX:(??%%); destruct
969  % [2: % [2: % [ % [
970    @cl_plus_succ [4: % | 5: @cl_plus_one % | *: skip ]
971    | /2/ ]| /4/ ]| skip ]| skip ]
972| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
973  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
974  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
975  whd in EX:(??%%); destruct
976  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
977  [ % [2: % [2: % [ % [
978    @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
979                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
980    | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_one @refl
981    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
982  | % [2: % [2: % [ % [
983    @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
984                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
985    | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_succ [4: @refl
986    | 5: @cl_plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
987    ]
988  ]
989| *
990  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
991    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
992    whd in EX:(??%%); destruct
993    whd in match (label_fundef ?);
994    whd in match (label_function ?);
995    lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
996    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
997    % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
998      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
999    | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
1000  | #id #tys #ty #args #k #k' #m #K #EX
1001    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
1002    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
1003    whd in EX2:(??%%); destruct
1004  ]
1005| #res #k #k' #m #K #EX inversion K
1006  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
1007    [ 2: * #i #EX whd in EX:(??%?); destruct
1008    | *: normalize #A try #B try #C destruct
1009    ]
1010    % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /2/ ]| skip ]| skip ]
1011  | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
1012    [ #EX whd in EX:(??%?); destruct
1013      % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /3/ ]| skip ]| skip ]
1014    | * * #b #o #ty #EX
1015      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
1016      whd in EX:(??%%); destruct
1017      % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
1018    ]
1019  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
1020       destruct whd in EX:(??%?); destruct
1021  ]
1022| #r #EX whd in EX:(??%%); destruct
1023] qed.
1024
1025
1026theorem step_with_labels : ∀ge,ge'.
1027  related_globals … label_fundef ge ge' →
1028  ∀s1,s1',tr,s2.
1029  state_with_labels s1 s1' →
1030  (exec_step ge s1 = Value … 〈tr,s2〉 →
1031   ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
1032             trace_with_extra_labels tr tr' ∧
1033             state_with_labels s2 s2').
1034#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
1035[ #s1 #s1' @step_with_labels_partial //
1036| #f #u *
1037(* If we have LSdefault we need to smuggle the execution of the cost label in
1038   before the actual statement. *)
1039  [ #s #k #k' #e #m #K #EX
1040    whd in EX:(??(??(??%???))?);
1041    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1042    >shift_fst whd in match (seq_of_labeled_statement ?);
1043    cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
1044    #tr' * #s2' * * #P #T #S
1045    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
1046(* but for LScase it's just like the cases in step_with_labels_partial *)
1047  | #sz #i #s #ls #k #k' #e #m #K #EX
1048    whd in EX:(??(??(??%???))?);
1049    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1050    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
1051    whd in EX:(??%?); destruct
1052    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
1053  ]   
1054] qed.
1055
1056
1057lemma exec_step_interaction:
1058  ∀ge,s,o,k. exec_step ge s = Interact … o k  →
1059  ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
1060#ge #s cases s
1061[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
1062  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
1063  whd in ⊢ (??%? → ?);
1064  [ 4,6,8,9: #EX destruct ]
1065  [ cases a
1066    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
1067    | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
1068      #x whd in ⊢ (??%? → ?); [2: cases (exec_expr ????) #y ] #EX whd in EX:(??%?); destruct
1069    ]
1070  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
1071  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
1072  | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
1073  | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
1074  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
1075      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
1076  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
1077  | cases kk [ 1,8: cases (fn_return f) normalize #A try #B try #C try #D try #E try #F try #G try #H destruct
1078    | 2,3,5,6,7: normalize #A #B try #C try #D try #E destruct
1079    | #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
1080  | cases kk normalize #A try #B try #C try #D try #E destruct
1081  | cases kk [ 4: #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
1082    | *: normalize #A try #B try #C try #D try #E destruct
1083    ]
1084  ]
1085| #f #args #kk #m #o #k cases f
1086  [ #f' whd in ⊢ (??%? → ?); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
1087    #x1 #x2 @bindIO_res_interact #m #Em #EX whd in EX:(??%?); destruct
1088  (* This is the only case that actually matters! *)
1089  | #fn #argtys #rty whd in ⊢ (??%? → ?);
1090    @bindIO_res_interact #vs #Evs
1091    #EX whd in EX:(??%?); destruct
1092    %{fn} %{argtys} %{rty} %{args} %{kk} %{m} %
1093  ]
1094| #v #kk #m #o #k whd in ⊢ (??%? → ?); cases kk
1095    [ cases v [2: * ] normalize #A try #B destruct
1096    | 8: #x1 #x2 #x3 #x4 cases x1
1097      [ whd in ⊢ (??%? → ?); #EX destruct | #x5 whd in ⊢ (??%? → ?); cases x5
1098          #x6 #x7 @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct ]
1099    | *: normalize #A try #B try #C try #D try #E destruct ]
1100| #r #o #k #EX whd in EX:(??%?); destruct
1101] qed.
1102
1103lemma state_with_labels_call : ∀f,a,k,m,s1.
1104 state_with_labels (Callstate f a k m) s1 →
1105 ∃k'. cont_with_labels k k' ∧ s1 = Callstate (label_fundef f) a k' m.
1106#f #a #k #m #s1 #S inversion S
1107[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
1108  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1109  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct
1110  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
1111  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
1112  | #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % //
1113  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1114  | #H72 #H73 #H74 #H75 destruct
1115  ]
1116| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 destruct
1117] qed.
1118
1119lemma interactive_step_with_labels : ∀ge,ge'.
1120  related_globals … label_fundef ge ge' →
1121  ∀s1,s1',o,k.
1122  exec_step ge s1 = Interact … o k →
1123  state_with_labels s1 s1' →
1124  ∃k'.
1125      exec_step ge' s1' = Interact … o k' ∧
1126  ∀i. ∃tr,s2.
1127    k i = Value … 〈tr,s2〉 ∧
1128    ∃tr',s2'.
1129      k' i = Value … 〈tr',s2'〉 ∧
1130      trace_with_extra_labels tr tr' ∧
1131      state_with_labels s2 s2'.
1132#ge #ge' #RG #s1 #s1' #o #k #EX
1133cases (exec_step_interaction … EX)
1134#fn * #argtys * #retty * #vargs * #k' * #m #E
1135destruct
1136#S cases (state_with_labels_call … S)
1137#k'' * #K #E2 destruct
1138whd in EX:(??%?);
1139@(bindIO_res_interact ?????????? EX) -EX
1140#vs #CHECK #EX whd in EX:(??%?); destruct
1141% [2: %
1142[ whd in ⊢ (??%?);
1143  >CHECK in ⊢ (??%?);
1144  whd in ⊢ (??%?);
1145  @refl
1146| #i
1147  % [2: % [2: %
1148  [ @refl
1149  | % [2: % [ 2: % [ %
1150    [ @refl
1151    | // ]
1152    | /3/ ]
1153    | skip ]| skip ]
1154  ]| skip ]| skip ]
1155]| skip
1156] qed.
1157
1158
1159lemma initial_state_in_simulation : ∀p,s.
1160  make_initial_state p = OK ? s →
1161  ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'.
1162* #vars #fns #main #s
1163whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1164cases (bind_inversion ????? EX) -EX #m * #Em #EX
1165cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1166cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1167whd in EX:(??%%); destruct
1168whd in match (make_initial_state ?);
1169letin ge' ≝ (make_global ?)
1170cut (related_globals … label_fundef ge ge')
1171[ // ] #RG
1172% [2: %
1173[ whd in ⊢ (??%?);
1174  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
1175  >init_mem_transf >Em in ⊢ (??%?);
1176  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
1177  whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')
1178  whd in ⊢ (??%?); @refl
1179| /3/
1180] | skip ]
1181qed.
1182 
1183
1184
1185
1186lemma final_related : ∀s1,s2.
1187  state_with_labels s1 s2 →
1188  is_final s1 = is_final s2.
1189#s1x #s2x *
1190[ #s1y #s2y * //
1191| //
1192] qed.
1193
1194let corec build_exec
1195  (ge1,ge2:genv)
1196  (RG:related_globals … label_fundef ge1 ge2)
1197  (s1,s2:state)
1198  (S:state_with_labels s1 s2)
1199  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
1200: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝
1201match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
1202[ nw_stop tr i s ⇒ ?
1203| nw_step tr1 s1' e1 NW1 ⇒ ?
1204| nw_interact o k NWk ⇒ ?
1205] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
1206[ #E1
1207  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
1208  #EX1 #F1
1209  cases (step_with_labels … RG … S EX1)
1210  #tr2 * #s2' * * #PL #TWL #S'
1211  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
1212  cases (plus_final … clight_fullexec … PL F2)
1213  #tr2' #S2
1214  @(swl_stop … S2 TWL)
1215| #E1
1216  cases (extract_step ?? clight_fullexec … E1)
1217  #EX1 #E1'
1218  cases (step_with_labels … RG … S EX1)
1219  #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
1220  @(swl_steps … (plus_exec … clight_fullexec … EX2 ?))
1221  [ whd in ⊢ (??%?); <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
1222  | //
1223  | (* Manual rewrite to prevent guardedness condition getting upset. *)
1224    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
1225    @build_exec // >E1' in NW1; //
1226  ]
1227| #E1
1228  cases (extract_interact ?? clight_fullexec … E1)
1229  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
1230  cases (interactive_step_with_labels … RG … EX1 S)
1231  #k2' * #EX2 #H2 @(match sym_eq … EX2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%);
1232  @swl_interact
1233  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
1234  lapply (NWk i)
1235  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
1236  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
1237  cases (is_final s2')
1238  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
1239    inversion NW'
1240    [ #H1 #H2 #H3 #H4 #H5 destruct
1241    | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
1242    | #H14 #H15 #H16 #H17 #H18 destruct
1243    ]
1244  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
1245  ]
1246] qed.
1247
1248lemma initial_state_is_not_final : ∀p,s.
1249  make_initial_state p = OK ? s →
1250  is_final s = None ?.
1251* #vars #fns #main #s
1252whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1253cases (bind_inversion ????? EX) -EX #m * #Em #EX
1254cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1255cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1256whd in EX:(??%%); destruct //
1257qed.
1258
1259
1260theorem labelling_sim : labelled_exec_is_equiv.
1261whd (* let's remind ourselves of the spec *)
1262#p
1263#NW
1264cases (not_wrong_init clight_fullexec p NW)
1265whd in ⊢ (% → ??%? → ?); #s1 #I1
1266cases (initial_state_in_simulation … I1)
1267#s2 * #I2
1268
1269whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
1270letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
1271change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
1272>I1
1273
1274whd in match (exec_inf ????);
1275letin ge2 ≝ (make_global ?? clight_fullexec (clight_label p))
1276change with (make_initial_state (clight_label p)) in match (make_initial_state ?? clight_fullexec (clight_label p));
1277>I2
1278
1279whd in ⊢ (??% → ? → ?%%);
1280>exec_inf_aux_unfold
1281>exec_inf_aux_unfold
1282whd in ⊢ (??% → ? → ?%%);
1283whd in match (is_final ?????);
1284>(initial_state_is_not_final … I1)
1285whd in match (is_final ?????);
1286>(initial_state_is_not_final … I2)
1287whd in ⊢ (??% → ? → ?%%);
1288
1289#NW #S
1290@(swl_steps E0 E0)
1291[ 2: @steps_step | skip | // | @build_exec
1292  [ @transform_program_related | // | inversion NW
1293    [ #tr #i #s #E1 #E2 destruct
1294    | #trX #sX #eX #NWX #E1X #E2X destruct //
1295    | #H1 #H2 #H3 #H4 #H5 destruct
1296    ]
1297  ]
1298] qed.
1299
1300
1301
Note: See TracBrowser for help on using the repository browser.