source: src/Clight/labelSimulation.ma @ 2324

Last change on this file since 2324 was 2319, checked in by campbell, 8 years ago

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

File size: 59.4 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_gen … 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 ⊢ (??%? → ??%?); >(rgg_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_gen … 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 : ∀g,r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (\fst (label_function g 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 : ∀g,f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (\fst (label_function g 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 : ∀g,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 (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
295| swl_dowhilestate : ∀g,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 (\fst (label_function g f)) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
297| swl_forstate : ∀g,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 (\fst (label_function g 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 : ∀g,fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (\fst (label_fundef g 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 : ∀g,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 (\fst (label_function g 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 : ∀g,f.
318  fn_return (\fst (label_function g f)) = fn_return f.
319#g * #rty #params #vars #body
320whd in match (label_function ??);
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 : ∀g,fd.
333  type_of_fundef (\fst (label_fundef g fd)) = type_of_fundef fd.
334#g * //
335* #rty #args #vars #body
336normalize cases (label_statement ??) #body' #u
337normalize cases (fresh ??) //
338qed.
339
340lemma label_fn_params : ∀g,f.
341  fn_params (\fst (label_function g f)) = fn_params f.
342#g * #rty #params #vars #s whd in ⊢ (??(?(???%))?); @breakup_pair @breakup_pair //
343qed.
344
345lemma label_fn_vars : ∀g,f.
346  fn_vars (\fst (label_function g f)) = fn_vars f.
347#g * #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_gen … label_fundef ge ge' →
360  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
361  ∃u. opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (\fst (label_fundef u fd)).
362#ge #ge' #m #vf #fd #RG
363lapply (rgg_find_funct … RG … vf fd)
364cases (find_funct … vf)
365[ #_ #E normalize in E; destruct
366| #fd' #H #E normalize in E; destruct cases (H (refl ??)) #u #FF %{u} >FF //
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 : ∀g,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 (\fst (label_function g f))) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
631    cont_with_labels k1 k1'.
632#g #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') g ?)
636[ /2/ ]
637>FIND whd in ⊢ (% → ?); //
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_gen … 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[ #g #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 (\fst (label_function g 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    | #u0 #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      cases (opt_find_funct … RG … EX3) #ux #EFF
754      % [2,4: % [2,4: % [1,3: % [1,3:
755      @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
756      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
757      whd in ⊢ (??%?); [ >EFF in ⊢ (??%?); | >EFF in ⊢ (??%?); ]
758      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
759      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
760      whd in ⊢ (??%?);
761      @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
762  | #st1 #st2 #EX
763    whd in EX:(??%%); destruct
764    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
765    %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
766  | #a #st1 #st2 #EX
767    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
768    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
769    normalize in EX; destruct
770    whd in match (label_statement ??); @label_gen_elim #u1
771    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
772    @label_gen_elim #u5
773    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
774    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
775    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
776    % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9:
777      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
778      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
779      whd in ⊢ (??%?); @refl
780    | 1,2,6,7: skip
781    | 5,10: @cl_plus_one @refl
782    | *: skip
783    ]
784    | 2,4: <(E0_right tr) @twel_app /2/
785    ]| 2,4: /3/ ] | *: skip ] | *: skip ]
786  | #a #st #EX
787    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
788    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
789    normalize in EX; destruct
790    whd in match (label_statement ??); @label_gen_elim #u1
791    @label_gen_elim #u2
792    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
793    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
794    >shift_fst
795    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
796    % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
797      | 5,10: @cl_plus_succ [ 4,9:
798      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
799      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
800      whd in ⊢ (??%?); @refl
801    | 1,2,6,7: skip
802    | 5: @cl_plus_one @refl
803    | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
804    | *: skip
805    ]
806    | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
807    ]| 2,4: /4/ ] | *: skip ] | *: skip ]
808  | #a #st #EX
809    normalize in EX; destruct
810    whd in match (label_statement ??); @label_gen_elim #u1
811    @label_gen_elim #u2
812    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
813    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
814    % [2: % [2: % [ % [ @cl_plus_succ [ 4: @refl | 1,2: skip
815      | 5: @cl_plus_succ [ 4: @refl | 1,2: skip | 5: @cl_plus_one // | skip ] | skip ]
816      | /2/ ] | /4/ ] | skip ] | skip ]
817  | #st1 #a #st2 #st #EX
818    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
819    whd in EX:(??%?); >Eskip in EX; #EX
820    whd in match (label_statement ??); @label_gen_elim #u1
821    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
822    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
823    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
824    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
825      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
826      normalize in EX; destruct
827      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
828      % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
829      | 5,10: @cl_plus_succ [ 4,9:
830      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
831      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
832      whd in ⊢ (??%?); @refl
833      | 1,2,6,7: skip
834      | 5: @cl_plus_one @refl
835      | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
836      | *: skip
837      ]
838      | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
839      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
840    | whd in EX:(??%%); destruct
841      % [2: % [2: %[ %[ @cl_plus_succ [ 4: @refl | 5: @cl_plus_one
842        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
843        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
844      | skip ] | skip ]
845    ]
846  | #EX inversion KL
847    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
848    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
849    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
850    | #ue #e0 #us0 #s0 #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    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
853    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
854    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
855    | #ux #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
856    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
857    ]
858    whd in match (label_statement ??);
859    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
860    [1,11,13: @cl_plus_one @refl | 2,12,14: //
861    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
862    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
863    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip] | /2/
864    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
865    ]| *: /3 by swl_partial, swl_state/ ]|*: skip]|*: skip ]
866  | #EX inversion KL
867    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
868    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
869    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
870    | #ue #e0 #us0 #s0 #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    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
873    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
874    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
875    | #g #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
876    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
877    ]
878    whd in match (label_statement ??);
879    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
880      [1,3,7,9,11: @cl_plus_one @refl | 5: @cl_plus_succ [4:@refl | 5:@cl_plus_one @refl | *: skip ]
881      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
882    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
883      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
884      normalize in EX; destruct
885      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
886      % [2,4: % [2,4: % [1,3: % [1,3: [ @cl_plus_one | @cl_plus_succ ] [ 1,5:
887        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
888      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
889      whd in ⊢ (??%?); @refl
890      | 6: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
891      | // | <(E0_right tr) @twel_app /2/
892      ]
893      | /3/ | /3/ ] | *: skip ] | *: skip ]
894    ]
895  | * [2: #a ] #EX
896    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
897    #Ety #EX whd in EX:(??%?);
898    [ destruct
899    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
900      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
901    | >Ety in EX; #EX
902    | @⊥ cases (fn_return f) in Ety EX;
903      [ * #H cases (H (refl ??))
904      | *: normalize #a #b #c try #d try #e destruct
905      ]
906    ]
907    whd in match (label_statement ??);
908    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
909    whd in EX:(??%%); destruct
910    % [2,4: % [2,4: % [1,3: %[1,3: @cl_plus_one
911      whd in ⊢ (??%?);
912      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
913        whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
914      | >label_function_return >Ety in ⊢ (??%?);
915      ] whd in ⊢ (??%?); @refl
916      | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip]
917  | #a #ls #EX
918    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
919    cases v1 in EX1 EX;
920    [ 2: #sz #i #EX1 #EX
921    | *: normalize #A #B try #C destruct
922    ]
923    whd in EX:(??%%); destruct
924    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
925    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
926    % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
927      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
928      ]|skip ]| skip ]
929  | #l #st #EX
930    whd in EX:(??%?); destruct
931    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
932    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
933    %[2: %[2: %[ %[ @cl_plus_succ
934      [ 4: @refl | 5: @cl_plus_one @refl | *: skip ]
935      | /2/ ] | /3/ ] |skip ]| skip ]
936  | #l #EX
937    whd in EX:(??%?);
938    @blindly_label whd
939    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
940    cases (find_label ???) in ⊢ (???% → ?);
941    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
942    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
943      cases (label_find_label_fn g … KL F)
944      #u' * #cs * #k1' * #F' #K'
945      % [2: %[2: %[ %[ @cl_plus_succ
946        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @cl_plus_one @refl | *: skip ]
947        | /2/ ] | /3/ ] | skip ] | skip ]
948    ]
949  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
950    % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]| skip ]
951  ]
952| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
953  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
954  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
955  whd in EX:(??%%); destruct
956  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
957  [ % [2: % [2: % [ % [
958    @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
959                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
960               |5: @cl_plus_one @refl | *: skip ]
961    | <(E0_right tr) /3/ ]| /4 by swl_partial, swl_state, cwl_while/ ]| skip ]| skip ]
962  | % [2: % [2: % [ % [
963    @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
964                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
965    | 5: @cl_plus_succ [4: @refl
966    | 5: @cl_plus_one @refl | *: skip ] | *: skip ]
967    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
968  ]
969| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
970  whd in EX:(??%%); destruct
971  % [2: % [2: % [ % [
972    @cl_plus_succ [4: % | 5: @cl_plus_one % | *: skip ]
973    | /2/ ]| /4/ ]| skip ]| skip ]
974| #u0 #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
975  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
976  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
977  whd in EX:(??%%); destruct
978  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
979  [ % [2: % [2: % [ % [
980    @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
981                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
982    | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_one @refl
983    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
984  | % [2: % [2: % [ % [
985    @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
986                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
987    | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_succ [4: @refl
988    | 5: @cl_plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
989    ]
990  ]
991| #u0 *
992  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
993    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
994    whd in EX:(??%%); destruct
995    whd in match (label_fundef ??);
996    whd in match (label_function ??);
997    lapply (refl ? (\fst (label_function u0 f))) whd in ⊢ (???(???%) → ?);
998    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
999    % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
1000      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
1001    | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
1002  | #id #tys #ty #args #k #k' #m #K #EX
1003    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
1004    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
1005    whd in EX2:(??%%); destruct
1006  ]
1007| #res #k #k' #m #K #EX inversion K
1008  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
1009    [ 2: * #i #EX whd in EX:(??%?); destruct
1010    | *: normalize #A try #B try #C destruct
1011    ]
1012    % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /2/ ]| skip ]| skip ]
1013  | 9: #u0 #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
1014    [ #EX whd in EX:(??%?); destruct
1015      % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /3/ ]| skip ]| skip ]
1016    | * * #b #o #ty #EX
1017      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
1018      whd in EX:(??%%); destruct
1019      % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
1020    ]
1021  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
1022       destruct whd in EX:(??%?); destruct
1023  ]
1024| #r #EX whd in EX:(??%%); destruct
1025] qed.
1026
1027
1028theorem step_with_labels : ∀ge,ge'.
1029  related_globals_gen … label_fundef ge ge' →
1030  ∀s1,s1',tr,s2.
1031  state_with_labels s1 s1' →
1032  (exec_step ge s1 = Value … 〈tr,s2〉 →
1033   ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
1034             trace_with_extra_labels tr tr' ∧
1035             state_with_labels s2 s2').
1036#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
1037[ #s1 #s1' @step_with_labels_partial //
1038| #u0 #f #u *
1039(* If we have LSdefault we need to smuggle the execution of the cost label in
1040   before the actual statement. *)
1041  [ #s #k #k' #e #m #K #EX
1042    whd in EX:(??(??(??%???))?);
1043    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1044    >shift_fst whd in match (seq_of_labeled_statement ?);
1045    cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
1046    #tr' * #s2' * * #P #T #S
1047    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
1048(* but for LScase it's just like the cases in step_with_labels_partial *)
1049  | #sz #i #s #ls #k #k' #e #m #K #EX
1050    whd in EX:(??(??(??%???))?);
1051    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1052    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
1053    whd in EX:(??%?); destruct
1054    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
1055  ]   
1056] qed.
1057
1058
1059lemma exec_step_interaction:
1060  ∀ge,s,o,k. exec_step ge s = Interact … o k  →
1061  ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
1062#ge #s cases s
1063[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
1064  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
1065  whd in ⊢ (??%? → ?);
1066  [ 4,6,8,9: #EX destruct ]
1067  [ cases a
1068    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
1069    | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
1070      #x whd in ⊢ (??%? → ?); [2: cases (exec_expr ????) #y ] #EX whd in EX:(??%?); destruct
1071    ]
1072  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
1073  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
1074  | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
1075  | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
1076  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
1077      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
1078  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
1079  | 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
1080    | 2,3,5,6,7: normalize #A #B try #C try #D try #E destruct
1081    | #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
1082  | cases kk normalize #A try #B try #C try #D try #E destruct
1083  | cases kk [ 4: #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
1084    | *: normalize #A try #B try #C try #D try #E destruct
1085    ]
1086  ]
1087| #f #args #kk #m #o #k cases f
1088  [ #f' whd in ⊢ (??%? → ?); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
1089    #x1 #x2 @bindIO_res_interact #m #Em #EX whd in EX:(??%?); destruct
1090  (* This is the only case that actually matters! *)
1091  | #fn #argtys #rty whd in ⊢ (??%? → ?);
1092    @bindIO_res_interact #vs #Evs
1093    #EX whd in EX:(??%?); destruct
1094    %{fn} %{argtys} %{rty} %{args} %{kk} %{m} %
1095  ]
1096| #v #kk #m #o #k whd in ⊢ (??%? → ?); cases kk
1097    [ cases v [2: * ] normalize #A try #B destruct
1098    | 8: #x1 #x2 #x3 #x4 cases x1
1099      [ whd in ⊢ (??%? → ?); #EX destruct | #x5 whd in ⊢ (??%? → ?); cases x5
1100          #x6 #x7 @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct ]
1101    | *: normalize #A try #B try #C try #D try #E destruct ]
1102| #r #o #k #EX whd in EX:(??%?); destruct
1103] qed.
1104
1105lemma state_with_labels_call : ∀f,a,k,m,s1.
1106 state_with_labels (Callstate f a k m) s1 →
1107 ∃k'. cont_with_labels k k' ∧ ∃u0. s1 = Callstate (\fst (label_fundef u0 f)) a k' m.
1108#f #a #k #m #s1 #S inversion S
1109[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
1110  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1111  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct
1112  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
1113  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
1114  | #u0 #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % /2/
1115  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1116  | #H72 #H73 #H74 #H75 destruct
1117  ]
1118| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 destruct
1119] qed.
1120
1121lemma interactive_step_with_labels : ∀ge,ge'.
1122  related_globals_gen … label_fundef ge ge' →
1123  ∀s1,s1',o,k.
1124  exec_step ge s1 = Interact … o k →
1125  state_with_labels s1 s1' →
1126  ∃k'.
1127      exec_step ge' s1' = Interact … o k' ∧
1128  ∀i. ∃tr,s2.
1129    k i = Value … 〈tr,s2〉 ∧
1130    ∃tr',s2'.
1131      k' i = Value … 〈tr',s2'〉 ∧
1132      trace_with_extra_labels tr tr' ∧
1133      state_with_labels s2 s2'.
1134#ge #ge' #RG #s1 #s1' #o #k #EX
1135cases (exec_step_interaction … EX)
1136#fn * #argtys * #retty * #vargs * #k' * #m #E
1137destruct
1138#S cases (state_with_labels_call … S)
1139#k'' * #K * #u0 #E2 destruct
1140whd in EX:(??%?);
1141@(bindIO_res_interact ?????????? EX) -EX
1142#vs #CHECK #EX whd in EX:(??%?); destruct
1143% [2: %
1144[ whd in ⊢ (??%?);
1145  >CHECK in ⊢ (??%?);
1146  whd in ⊢ (??%?);
1147  @refl
1148| #i
1149  % [2: % [2: %
1150  [ @refl
1151  | % [2: % [ 2: % [ %
1152    [ @refl
1153    | // ]
1154    | /3/ ]
1155    | skip ]| skip ]
1156  ]| skip ]| skip ]
1157]| skip
1158] qed.
1159
1160
1161lemma initial_state_in_simulation : ∀p,s.
1162  make_initial_state p = OK ? s →
1163  ∃s'. make_initial_state (\fst (clight_label p)) = OK ? s' ∧ state_with_labels s s'.
1164* #vars #fns #main #s
1165whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1166cases (bind_inversion ????? EX) -EX #m * #Em #EX
1167cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1168cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1169whd in EX:(??%%); destruct
1170whd in match (make_initial_state ?);
1171letin ge' ≝ (make_global ?)
1172cut (related_globals_gen … label_fundef ge ge')
1173[ // ] #RG
1174cases (rgg_find_funct_ptr … RG … Emain') #u' #FFP
1175% [2: %
1176[ whd in ⊢ (??%?);
1177  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
1178  >(init_mem_transf_gen … (mk_program ?? vars fns main)) >Em in ⊢ (??%?);
1179  whd in ⊢ (??%?); <(rgg_find_symbol … RG) >Emain in ⊢ (??%?);
1180  whd in ⊢ (??%?); >FFP in ⊢ (??%?);
1181  whd in ⊢ (??%?); @refl
1182| /3/
1183] | skip ]
1184qed.
1185 
1186
1187
1188
1189lemma final_related : ∀s1,s2.
1190  state_with_labels s1 s2 →
1191  is_final s1 = is_final s2.
1192#s1x #s2x *
1193[ #s1y #s2y * //
1194| //
1195] qed.
1196
1197let corec build_exec
1198  (ge1,ge2:genv)
1199  (RG:related_globals_gen … label_fundef ge1 ge2)
1200  (s1,s2:state)
1201  (S:state_with_labels s1 s2)
1202  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
1203: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝
1204match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
1205[ nw_stop tr i s ⇒ ?
1206| nw_step tr1 s1' e1 NW1 ⇒ ?
1207| nw_interact o k NWk ⇒ ?
1208] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
1209[ #E1
1210  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
1211  #EX1 #F1
1212  cases (step_with_labels … RG … S EX1)
1213  #tr2 * #s2' * * #PL #TWL #S'
1214  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
1215  cases (plus_final … clight_fullexec … PL F2)
1216  #tr2' #S2
1217  @(swl_stop … S2 TWL)
1218| #E1
1219  cases (extract_step ?? clight_fullexec … E1)
1220  #EX1 #E1'
1221  cases (step_with_labels … RG … S EX1)
1222  #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
1223  @(swl_steps … (plus_exec … clight_fullexec … EX2 ?))
1224  [ whd in ⊢ (??%?); <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
1225  | //
1226  | (* Manual rewrite to prevent guardedness condition getting upset. *)
1227    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
1228    @build_exec // >E1' in NW1; //
1229  ]
1230| #E1
1231  cases (extract_interact ?? clight_fullexec … E1)
1232  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
1233  cases (interactive_step_with_labels … RG … EX1 S)
1234  #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 ⊢ (??%);
1235  @swl_interact
1236  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
1237  lapply (NWk i)
1238  @(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 ⇒ ?])
1239  @(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 ?????);
1240  cases (is_final s2')
1241  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
1242    inversion NW'
1243    [ #H1 #H2 #H3 #H4 #H5 destruct
1244    | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
1245    | #H14 #H15 #H16 #H17 #H18 destruct
1246    ]
1247  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
1248  ]
1249] qed.
1250
1251lemma initial_state_is_not_final : ∀p,s.
1252  make_initial_state p = OK ? s →
1253  is_final s = None ?.
1254* #vars #fns #main #s
1255whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1256cases (bind_inversion ????? EX) -EX #m * #Em #EX
1257cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1258cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1259whd in EX:(??%%); destruct //
1260qed.
1261
1262
1263theorem labelling_sim : labelled_exec_is_equiv.
1264whd (* let's remind ourselves of the spec *)
1265#p
1266#NW
1267cases (not_wrong_init clight_fullexec p NW)
1268whd in ⊢ (% → ??%? → ?); #s1 #I1
1269cases (initial_state_in_simulation … I1)
1270#s2 * #I2
1271
1272whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
1273letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
1274change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
1275>I1
1276
1277whd in match (exec_inf ????);
1278letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p)))
1279change with (make_initial_state (\fst (clight_label p))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p)));
1280>I2
1281
1282whd in ⊢ (??% → ? → ?%%);
1283>exec_inf_aux_unfold
1284>exec_inf_aux_unfold
1285whd in ⊢ (??% → ? → ?%%);
1286whd in match (is_final ?????);
1287>(initial_state_is_not_final … I1)
1288whd in match (is_final ?????);
1289>(initial_state_is_not_final … I2)
1290whd in ⊢ (??% → ? → ?%%);
1291
1292#NW #S
1293@(swl_steps E0 E0)
1294[ 2: @steps_step | skip | // | @build_exec
1295  [ @transform_program_gen_related | // | inversion NW
1296    [ #tr #i #s #E1 #E2 destruct
1297    | #trX #sX #eX #NWX #E1X #E2X destruct //
1298    | #H1 #H2 #H3 #H4 #H5 destruct
1299    ]
1300  ]
1301] qed.
1302
1303
1304
Note: See TracBrowser for help on using the repository browser.