source: src/Clight/labelSimulation.ma @ 2011

Last change on this file since 2011 was 2011, checked in by garnier, 7 years ago

Minor cleanup.

File size: 52.1 KB
Line 
1
2include "Clight/label.ma".
3include "Clight/Cexec.ma".
4
5(* for the induction principle *)
6include "Clight/CexecSound.ma".
7
8(* TODO: make something general that can live in common/Globalenvs.ma. *)
9record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
10  rg_find_symbol: ∀s.
11    find_symbol … ge s = find_symbol … ge' s;
12  rg_find_funct: ∀v,f.
13    find_funct … ge v = Some ? f →
14    find_funct … ge' v = Some ? (t f);
15  rg_find_funct_ptr: ∀b,f.
16    find_funct_ptr … ge b = Some ? f →
17    find_funct_ptr … ge' b = Some ? (t f)
18}.
19
20(* FIXME with a more general result *)
21axiom transform_program_related : ∀F,V,init,t,p.
22  related_globals F t (globalenv (λ_.F) V init p) (globalenv (λ_.F) V init (transform_program … p t)).
23(*
24#F #V #init #t * #vars #fns #main
25whd in match (transform_program ?????);
26whd in match (transf_program ????);
27elim fns
28[ % [ // | * [ | #sz #i | #f | #r | #ptr ] #f #F1 whd in F1:(??%?); destruct
29             cases (eq_offset ??) in F1; #F1 whd in F1:(??%?);
30             whd in match (globalenv ?????) in F1;
31             whd in match (globalenv_allocmem ????) in F1;
32             elim
33%
34[ #s
35*)
36
37(* Useful for breaking up the labeling functions, because we don't care about
38   *which* cost labels are added here and so can throw away the resulting name
39   generator. *)
40lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D.
41  \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) =  F (\fst e).
42#A #B #C #D * //
43qed.
44
45
46(* Similarly, lemma to break up label_expr, label_exprs and label_statement in
47   the labelling functions *)
48lemma 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].
49  (∀u'. P (F (\fst (L syn u)) u')) →
50  P (let 〈syn',u'〉 ≝ L syn u in F syn' u').
51#Syn #syn #u #T #L #F #P
52cases (L syn u)
53#syn' #u' #H @H
54qed.
55
56lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
57  (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) →
58  P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u').
59#e #u #T #F #P #H whd in match (add_cost_expr ??);
60cases (fresh ??) #l #u' @H
61qed.
62
63
64lemma label_expr_type : ∀e,u.
65  typeof (\fst (label_expr e u)) = typeof e.
66* #e #ty #u >shift_fst //
67qed.
68
69(* Formalise the notion of a trace with extra cost labels added.  Note that
70   we don't require the left trace to be cost free.  *)
71inductive trace_with_extra_labels : trace → trace → Prop ≝
72| twel_0 : trace_with_extra_labels E0 E0
73| twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2)
74| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
75
76lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
77#tr elim tr /2/
78qed.
79
80lemma twel_app : ∀tr1,tr2,tr1',tr2'.
81  trace_with_extra_labels tr1 tr1' →
82  trace_with_extra_labels tr2 tr2' →
83  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
84#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
85qed. 
86
87definition expr_lvalue_ind_combined ≝
88λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
89conj ??
90 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
91 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
92
93theorem label_expr_ok : ∀ge,ge',en,m.
94  related_globals ? label_fundef ge ge' →
95  (∀e,v,tr.
96   exec_expr ge en m e = OK … 〈v,tr〉 →
97   ∀u. ∃tr'. exec_expr ge' en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧
98             trace_with_extra_labels tr tr') ∧
99  (∀e,ty,b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
100          ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
101                    trace_with_extra_labels tr tr').
102(* Proof goes by breaking up the execution in the hypothesis, breaking up the
103   labelling function to get a new term and executing it by rewriting what we
104   learned from the hypothesis. *)
105#ge #ge' #en #m #RG @expr_lvalue_ind_combined
106[ 1,2: normalize /3 by ex_intro, conj/
107| * //
108 [ #id #ty #IH #v #tr #EX #u
109   cases (bind_inversion ????? EX) -EX * * #b #o #tr1 * #EX1 #EX
110   cases (bind_inversion ????? EX) -EX #v2 * #EX2 #EX
111   normalize in EX; destruct
112   cases (IH … EX1 u) #tr1' * #EX1' #T1
113   %{(tr1')} % [ whd in ⊢ (??%?); >EX1' whd in ⊢ (??%?); >EX2 @refl | // ]
114 | #e1 #ty #IH #v #tr #EX #u
115   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
116   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
117   normalize in EXrem; destruct
118   cases (IH … EX1 u) #tr1' * #EX1' #twel1
119   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1'
120   whd in ⊢ (?(??%?)?); >EXl /2/
121 | #e1 #id #ty #IH #v #tr #EX #u
122   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
123   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
124   normalize in EXrem; destruct
125   cases (IH … EX1 u) #tr1' * #EX1' #twel1
126   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1'
127   whd in ⊢ (??%?); >EXl @refl
128 ]
129| #v #ty #b #o #tr #EX #u %{tr} % [
130    whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
131    [ whd in ⊢ (??%? → ??%?); >(rg_find_symbol … RG) //
132    | #b // ]
133  | // ]
134| #e1 #ty #IH #b #o #tr #EX #u
135  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
136  cases (IH … EX1 u) #tr1' * #EX1' #twel1
137  %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1'
138  whd in ⊢ (?(??%?)?);
139  cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/
140| #ty' #e1 #ty #IH #v #tr #EX #u
141  cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
142  cases (IH … EX1 u) #tr1' * #EX1' #twel1
143  %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?);
144  whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1'
145  whd in ⊢ (?(??%?)?);
146  cases ty' in EX1rem ⊢ %;
147  [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r)
148       #pc normalize #E destruct /2/
149  | *: normalize #A try #B try #C try #D destruct
150  ]
151| #ty #op #e1 #IH #v #tr #EX #u
152  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
153  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem
154  normalize in EXrem; destruct
155  cases (IH … EX1 u) #tr1' * #EX1' #twel1
156  %{tr1'} % // >shift_fst
157  whd in ⊢ (??(????(?(???%)?))?);
158  @label_gen_elim #u2
159  whd in ⊢ (??%?); >EX1'
160  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
161| #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX
162  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
163  cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem
164  cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop'
165  #u
166  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
167  >shift_fst
168  whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
169  @label_gen_elim #u2
170  cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
171  @label_gen_elim #u3 %{(tr1'⧺tr2')}
172  whd in ⊢ (?(??%?)?); >EX1'
173  whd in ⊢ (?(??%?)?); >EX2'
174  whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop
175  normalize in EXop'; destruct % /2/
176| #ty #ty' #e1 #IH #v #tr #EX #u
177  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
178  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem
179  normalize in EX2rem; destruct
180  cases (IH … EX1 u) #tr1' * #EX1' #twel1
181  %{tr1'} % // >shift_fst >shift_fst
182  whd in ⊢ (??%?); >EX1'
183  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
184| #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u
185  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
186  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
187  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
188  normalize in EX2rem; destruct
189  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
190  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
191  @label_gen_elim #u2
192  @label_gen_elim #u3
193  @add_cost_expr_elim #u4 #l4
194  @label_gen_elim #u5
195  @add_cost_expr_elim #u6 #l6
196  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
197  [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
198  whd in ⊢ (?(??%?)?); >EX1'
199  whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
200  whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx'
201  normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
202| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
203  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
204  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
205  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
206  @label_gen_elim #u2
207  @label_gen_elim #u3
208  @add_cost_expr_elim #u4 #l4
209  @add_cost_expr_elim #u5 #l5
210  [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
211    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
212    -EX1rem -EXguardrem -EX2rem
213    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
214    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
215    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
216    whd in ⊢ (?(??%?)?); >EX1'
217    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
218    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
219    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
220    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
221    normalize in EX3rem ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
222  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
223    %{(tr1'⧺E0⧺Echarge l5)}
224    whd in ⊢ (?(??%?)?); >EX1'
225    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
226    normalize in EXguardrem; destruct % // <(E0_right tr) @twel_app /2/
227  ]
228| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
229  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
230  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
231  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
232  @label_gen_elim #u2
233  @add_cost_expr_elim #u4 #l4
234  @label_gen_elim #u3
235  @add_cost_expr_elim #u5 #l5
236  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
237    %{(tr1'⧺Echarge l4)}
238    whd in ⊢ (?(??%?)?); >EX1'
239    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
240    normalize in EXguardrem ⊢ %; destruct % // <(E0_right tr) /3/
241  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
242    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
243    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
244    cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2
245    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
246    whd in ⊢ (?(??%?)?); >EX1'
247    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
248    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
249    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
250    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
251    normalize in EX3rem ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
252  ]
253| #ty #ty' #v #tr normalize /3/
254| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
255  [ 7: #id #fl #IH #EX
256    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
257    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
258    whd in EXoffrem:(???%); destruct >shift_fst >shift_fst
259    cases (IH … EX1 u) #tr1' * #EX1' #twel1
260    %{tr1'} % //
261    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
262    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
263  | 8: #id #fl #IH #EX
264    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
265    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
266    cases (IH … EX1 u) #tr1' * #EX1' #twel1
267    %{tr1'} % //
268    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
269    whd in ⊢ (??%?); @refl
270  | *: normalize #A #B try #C try #D try #F destruct
271  ]
272| #ty #l #e1 #IH #v #tr #EX #u
273  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
274  whd in EX1rem:(???%); destruct
275  cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)}
276  >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1'
277  whd in ⊢ (?(??%?)?); /3/
278| #e1 #ty #NLV #b #o #tr #EX @⊥
279  cases e1 in NLV EX; normalize //
280  #A #B #C try #D try #F destruct
281] qed.
282
283lemma label_exprs_ok : ∀ge,ge'.
284   related_globals ? label_fundef ge ge' →
285   ∀en,m,es,vs,tr.
286   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
287   ∀u. ∃tr'. exec_exprlist ge' en m (\fst (label_exprs es u)) = OK … 〈vs,tr'〉 ∧
288             trace_with_extra_labels tr tr'.
289#ge #ge' #RG #en #m #es elim es
290[ #vs #tr #EX whd in EX:(??%?); destruct #u %{E0} /2/
291| #e #tl #IH #vs #tr #EX
292  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
293  cases (bind_inversion ????? EX) -EX * #tl' #tr' * #EX2 #EX
294  whd in EX:(??%%); destruct
295  #u whd in match (label_exprs ??); @label_gen_elim #u' >shift_fst
296  cases (proj1 ?? (label_expr_ok ge ge' en m RG) ??? EX1 u) #tr1' * #EX1' #T1
297  cases (IH … EX2 u') #tr'' * #EX2' #T2
298  % [2: % [ whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
299    whd in ⊢ (??%?); >EX2' in ⊢ (??%?); @refl
300  | /2/ ] | skip ]
301] qed.
302
303
304(* Now we move on to describe the simulation relation.  First, relate the
305   continuations. *)
306inductive cont_with_labels : cont → cont → Prop ≝
307| cwl_stop : cont_with_labels Kstop Kstop
308| cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
309| cwl_while : ∀ue,e,us,s,cs,cpost,k,k'.
310    cont_with_labels k k' →
311    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'))
312| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
313    cont_with_labels k k' →
314    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'))
315| cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
316    cont_with_labels k k' →
317    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'))
318| 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'))
319| 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'))
320| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
321| 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')
322| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
323    cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k').
324
325lemma call_cont_with_labels : ∀k,k'.
326  cont_with_labels k k' →
327  cont_with_labels (call_cont k) (call_cont k').
328#k0 #k0' #K elim K /2/
329qed.
330
331(* Now define almost all of the simulation relation... *)
332inductive state_with_labels_partial : state → state → Prop ≝
333| 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)
334(* Extra matching states that we can reach that don't quite correspond to the
335   labelling function *)
336| swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
337    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)
338| swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
339    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)
340| swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
341    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)
342(* and the rest *)
343| 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)
344| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
345| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
346.
347
348(* ... and add the states where the cases from switch statements are expanded.
349   We do these separately because in the LSdefault case we have to execute a
350   cost label alongside an arbitrary statement, and we want to reuse the result
351   on arbitrary statements we get for state_with_labels_partial. *)
352inductive state_with_labels : state → state → Prop ≝
353| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
354| swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' →
355    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
356                      (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
357.
358
359(* TODO: this (or something like it) ought to be elsewhere. *)
360inductive plus (ge:genv) : state → trace → state → Prop ≝
361| plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2
362| plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.
363
364(* Some details are invariant under labelling. *)
365lemma label_function_return : ∀f.
366  fn_return (label_function f) = fn_return f.
367* #rty #params #vars #body
368whd in ⊢ (??(?%)?);
369cases (label_statement ??) #body' #u'
370whd in ⊢ (??(?%)?);
371cases (add_cost_before ??) #body'' #u''
372//
373qed.
374
375lemma label_expr_fun_typeof : ∀a,u.
376  fun_typeof (\fst (label_expr a u)) = fun_typeof a.
377#a #u whd in ⊢ (??%?); >label_expr_type @refl
378qed.
379
380lemma label_fundef_typeof_fundef : ∀fd.
381  type_of_fundef (label_fundef fd) = type_of_fundef fd.
382* //
383* #rty #args #vars #body
384normalize cases (label_statement ??) #body' #u
385normalize cases (fresh ??) //
386qed.
387
388lemma label_fn_params : ∀f.
389  fn_params (label_function f) = fn_params f.
390* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
391qed.
392
393lemma label_fn_vars : ∀f.
394  fn_vars (label_function f) = fn_vars f.
395* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
396qed.
397
398(* Some annoying rewrite rules *)
399lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
400  exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
401  exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
402#ge #e #m #a #ty #u
403whd in ⊢ (??(????(???%))?); >shift_fst @refl
404qed.
405
406lemma opt_find_funct : ∀ge,ge',m,vf,fd.
407  related_globals ? label_fundef ge ge' →
408  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
409  opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd).
410#ge #ge' #m #vf #fd #RG
411lapply (rg_find_funct … RG … vf fd)
412cases (find_funct … vf)
413[ #_ #E normalize in E; destruct
414| #fd' #H #E normalize in E; destruct >(H (refl ??)) //
415] qed.
416
417lemma labelled_not_skip : ∀s,u.
418  s ≠ Sskip →
419  (\fst (label_statement s u)) ≠ Sskip.
420* #u
421[ * #H cases (H (refl ??))
422| *: #a try #b try #c try #d try #e
423     (* Use the state-monad-like structure of the labelling function to break
424        it up *)
425     whd in match (label_statement ??);
426     repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
427     % #E destruct
428] qed.
429
430lemma labelled_is_not_skip : ∀s,u.
431  s ≠ Sskip →
432  ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf.
433#s #u #NE
434cases (is_Sskip ?)
435[ #E @⊥ @(absurd ? E) @labelled_not_skip //
436| /2/
437] qed.
438
439lemma label_select_ls : ∀sz,i,ls,u.
440  ∃u'.
441    select_switch sz i (\fst (label_lstatements ls u)) =
442    \fst (label_lstatements (select_switch sz i ls) u').
443#sz #i #ls @(labeled_statements_ind … ls)
444[ #s #u % [2: whd in match (label_lstatements ??);
445  @label_gen_elim #u1 >shift_fst @refl | skip ]
446| #sz' #i' #s #tl #IH #u
447  whd in match (label_lstatements ??);
448  whd in match (select_switch ?? (LScase ????));
449  @intsize_eq_elim_elim
450  [ #NE
451    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
452    cases (IH u2)
453    #u4 #E %{u4} whd in ⊢ (??%?);
454    >intsize_eq_elim_false //
455  | #E <E in i' ⊢ %; #i' whd
456    @eq_bv_elim
457    [ #Ei >Ei
458      %{u}
459      whd in match (label_lstatements (if ? then ? else ?) ?);
460      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
461      whd in ⊢ (??%?);
462      >intsize_eq_elim_true
463      >eq_bv_true
464      @refl
465    | #NEi
466      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
467       whd in ⊢ (??(λ_.??%?));
468       >intsize_eq_elim_true
469       >eq_bv_false //
470    ]
471  ]
472] qed.
473
474(* Break up labelling function in one go for statements. *)
475lemma blindly_label : ∀u,s. ∀P:statement → Prop.
476match s with
477[ Sskip ⇒ P Sskip
478| Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2)))
479| 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)))
480| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
481| 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))))
482| 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))
483| 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))
484| 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))
485| Sbreak ⇒ P Sbreak
486| Scontinue ⇒ P Scontinue
487| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
488| Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2)))
489| Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1))))
490| Sgoto l ⇒ P (Sgoto l)
491| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
492] → P (\fst (label_statement s u)). 
493#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
494@label_gen_elim #u1 //
495@label_gen_elim #u2 //
496[ 6: >shift_fst //
497| *: @label_gen_elim #u3 //
498     @label_gen_elim #u4
499     [ @label_gen_elim #u5 >shift_fst >shift_fst //
500     | 2,3: >shift_fst >shift_fst //
501     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
502     ]
503] qed.
504
505(* Apply induction hypothesis in label_find_label proof below while getting
506   Matita to infer the continuations k0 and k0', and the universe u0, rather
507   than having to give them explicitly. *)
508lemma lfl_IH : ∀s0,lbl.
509  ∀C:option (statement×cont) → option (statement×cont) → Prop.
510  ∀IH:cont → cont → universe CostTag → Prop.
511  (∀k,k',u. cont_with_labels k k' → IH k k' u) →
512  ∀k0,k0',u0. cont_with_labels k0 k0' →
513   (IH k0 k0' u0 →
514    C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) →
515   C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0').
516/3/
517qed.
518
519(* Finding a goto label in a cost-labelled program gives a labelled version of
520   the statement and continuation found by the original function, if any. *)
521lemma label_find_label : ∀lbl,s,k,k',u.
522  cont_with_labels k k' →
523  match find_label lbl s k with
524  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
525    ∃u',cs,k1'.
526    find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
527    cont_with_labels k1 k1'
528  | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ?
529  ].
530#lbl #s @(statement_ind2 ? (λls.
531  ∀k,k',u.
532  cont_with_labels k k' →
533  match find_label_ls lbl ls k with
534  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
535    ∃u',cs,k1'.
536    find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
537    cont_with_labels k1 k1'
538  | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ?
539  ])
540 … s)
541[ #k #k' #u #F @refl
542| #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl
543| #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl
544| #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???);
545  whd in match (find_label ?? k');
546  @(lfl_IH sA … IH1) [ /2/ ]
547  cases (find_label ???)
548  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
549    @(lfl_IH … IH2) [ // ]
550    cases (find_label ???)
551    [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl
552    | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1'
553      % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ]
554    ]
555  | * #sA' #kA' whd in ⊢ (% → %);
556    * #u1' * #cs * #k1' * #FA' #K'
557         % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip]
558  ]
559| #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K
560  whd in match (find_label ?? k); whd in match (find_label ?? k');
561  whd in match (find_label ?? k');
562  @(lfl_IH  … IH1) [ // ] cases (find_label ???)
563  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
564    lapply (IH2 k k' u3 K) cases (find_label ???)
565    [ whd in ⊢ (% → %); #FIND2'
566      whd in match (find_label ???); >FIND1'
567      whd in match (find_label ???); >FIND2' @refl
568    | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2'
569      % [2: % [2: % [2: % [ whd in ⊢ (??%?);
570      whd in match (find_label ???); >FIND1' in ⊢ (??%?);
571      whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl
572      | // ]|skip]|skip]|skip]
573    ]
574  | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1'
575    % [2: % [2: % [2: % [
576      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
577      @refl | // ] |skip ]| skip ]| skip ]
578  ]
579| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
580  whd in match (find_label ?? k); normalize in match (find_label ?? k');
581  @(lfl_IH s0 … IH) [ /2/ ]
582  cases (find_label ???)
583  [ whd in ⊢ (% → %); #FIND1'
584    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
585  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
586    % [2: % [2: % [2: % [
587      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
588      @refl | // ]| skip ]| skip ]| skip ]
589  ]
590| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
591  whd in match (find_label ?? k); normalize in match (find_label ?? k');
592  @(lfl_IH s0 … IH) [ /2/ ]
593  cases (find_label ???)
594  [ whd in ⊢ (% → %); #FIND1'
595    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
596  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
597    % [2: % [2: % [2: % [
598      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
599      @refl | // ]| skip ]| skip ]| skip ]
600  ]
601| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
602  whd in match (find_label ???); normalize in match (find_label ?? k');
603  @(lfl_IH s1 … IH1) [ /2/ ]
604  cases (find_label ???)
605  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1'
606    @(lfl_IH s3 … IH3) [ /2/ ]
607    cases (find_label ???)
608    [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3'
609      @(lfl_IH s2 … IH2) [ /2/ ]
610      cases (find_label ???)
611      [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl
612      | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2'
613        % [2: % [2: % [2: % [
614         whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl
615        | // ]| skip ]| skip ]| skip ]
616      ]
617    | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3'
618        % [2: % [2: % [2: % [
619        >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl
620        | // ]| skip ]| skip ]| skip ]
621    ]
622  | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1'
623        % [2: % [2: % [2: % [
624        >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl
625        | // ]| skip ]| skip ]| skip ]
626  ]
627| //
628| //
629| #eo #k #k' #u @blindly_label #u1 //
630| #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2
631  normalize in match (find_label ???); normalize in match (find_label ???);
632  lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???)
633  [ whd in ⊢ (% → %); //
634  | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K'
635    % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip]
636  ]
637| #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs
638  whd in match (find_label ???); whd in match (find_label ?? k');
639  cases (ident_eq lbl l)
640  [ #E destruct whd
641    % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ]
642  | #NE whd in ⊢ (match % with [_⇒?|_⇒?]);
643    normalize in match (find_label ?? k');
644    @(lfl_IH s0 … IH) [ // ]
645    cases (find_label ???)
646    [ //
647    | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0
648      % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip]
649    ]
650  ]
651| //
652| #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/
653| #s0 #IH #k #k' #u whd in match (label_lstatements ??);
654  @label_gen_elim #u1 >shift_fst >shift_fst
655  whd in match (find_label_ls ???); whd in match (find_label_ls ???);
656  @IH
657| #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K
658  whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
659  @label_gen_elim #u3 >shift_fst
660  whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k');
661  @(lfl_IH s0 … IH1) [ /2/ ]
662  cases (find_label ???)
663  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0
664    lapply (IH2 k k' u2 K) cases (find_label_ls ???)
665    [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl
666    | * #stl #ktl //
667    ]
668  | * #s0' #k0' whd in ⊢ (% → %);
669    * #u' * #cs * #k1' * #FIND0 #K0 >FIND0
670    % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ]
671  ]
672] qed.
673
674lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1.
675  cont_with_labels k k' →
676  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
677  ∃u',cs,k1'.
678    find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
679    cont_with_labels k1 k1'.
680#lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
681whd in match (label_function ?);
682@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
683lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?)
684[ /2/ ]
685>FIND //
686qed.
687
688
689(* We show the main simulation in two stages.  First, we show it for all states
690   in the relation *except* those for labeled_statements, then we'll show the
691   whole thing.  This is so that we can appeal to the other cases in the proof
692   for labeled_statements. *)
693lemma step_with_labels_partial : ∀ge,ge'.
694  related_globals ? label_fundef ge ge' →
695  ∀s1,s1',tr,s2.
696  state_with_labels_partial s1 s1' →
697  exec_step ge s1 = Value … 〈tr,s2〉 →
698   ∃tr',s2'. plus ge' s1' tr' s2' ∧
699             trace_with_extra_labels tr tr' ∧
700             state_with_labels s2 s2'.
701
702(* General plan is like the expressions result, except that we do case analysis
703   on the simulation first, then:  break up the original execution, break up the
704   cost labelling, use the earlier results to deal with expressions, then
705   run the labelled version for enough steps.  We try to avoid having to write
706   out the final trace and state and "skip" them afterwards. *)
707#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
708[ #f #us #s #k #k' #e #m #KL cases s
709  [ #EX inversion KL
710    [ #E1 #E2 #_ destruct %{tr}
711      whd in EX:(??%?);
712      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
713      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}
714        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
715        | // ] | /3/ ]
716      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
717      ]
718    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
719      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
720      whd in EX:(??%%); destruct
721      % [ % [ @plus_one @refl | // ] | /3/ ]
722    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
723      whd in EX:(??%%); destruct
724      % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
725    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
726      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
727      cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem
728      normalize in EXbrem; destruct
729      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
730      [ % [ 2: % [ 2: % [ % [ @plus_one
731        whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
732        whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
733        whd in ⊢ (??%?); @refl
734        | // ]
735        | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
736      | % [ 2: % [ 2: % [ % [ @plus_succ [
737        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
738           whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
739           whd in ⊢ (??%?); @refl
740        | skip | skip
741        | 5: @plus_succ [ 4: @refl | skip | skip
742        | 5: @plus_one @refl | skip ] | skip ]
743        | <(E0_right tr) @twel_app /2/ ]
744        | /3/ ] | skip ] | skip ]
745      ]
746    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
747      whd in EX:(??%?); destruct
748      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
749    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
750      whd in EX:(??%?); destruct
751      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
752    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
753      whd in EX:(??%?); destruct
754      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
755    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
756      whd in EX:(??%?); destruct
757      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
758    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
759      whd in EX:(??%?);
760      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
761      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
762        %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
763        @refl | // ] | /4/ ] | skip ]
764      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
765      ]
766    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
767      % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ]
768    ]
769  | * #a1 #ty1 #a2 #EX
770    cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX
771    cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX
772    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
773    whd in EX:(??%%); destruct
774    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1
775    whd in match (label_statement ??);
776    @label_gen_elim #ua1 @label_gen_elim #ua2
777    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
778    % [2: % [2: % [ % [
779      @plus_one whd in ⊢ (??%?);     
780      >exec_lvalue_labelled >EX1' in ⊢ (??%?);
781      whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
782      whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?);
783      @refl
784    | @twel_app // ] | /3/ ] | skip ] | skip ]
785  | * [2: * #er #tyr ] #ef #args #EX
786    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
787    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
788    cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
789    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
790    whd in EX:(??%%);
791    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
792    destruct
793    whd in match (label_statement ??);
794    whd in match (label_opt_expr ??);
795    [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ]
796    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1
797    @label_gen_elim #u1
798    @label_gen_elim #u2
799    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2
800    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
801    % [2,4: % [2,4: % [1,3: % [1,3:
802      @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
803      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
804      whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
805      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
806      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
807      @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
808  | #st1 #st2 #EX
809    whd in EX:(??%%); destruct
810    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
811    %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
812  | #a #st1 #st2 #EX
813    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
814    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
815    normalize in EX; destruct
816    whd in match (label_statement ??); @label_gen_elim #u1
817    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
818    @label_gen_elim #u5
819    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
820    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
821    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
822    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9:
823      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
824      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
825      whd in ⊢ (??%?); @refl
826    | 1,2,6,7: skip
827    | 5,10: @plus_one @refl
828    | *: skip
829    ]
830    | 2,4: <(E0_right tr) @twel_app /2/
831    ]| 2,4: /3/ ] | *: skip ] | *: skip ]
832  | #a #st #EX
833    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
834    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
835    normalize in EX; destruct
836    whd in match (label_statement ??); @label_gen_elim #u1
837    @label_gen_elim #u2
838    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
839    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
840    >shift_fst
841    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
842    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
843      | 5,10: @plus_succ [ 4,9:
844      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
845      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
846      whd in ⊢ (??%?); @refl
847    | 1,2,6,7: skip
848    | 5: @plus_one @refl
849    | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
850    | *: skip
851    ]
852    | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
853    ]| 2,4: /4/ ] | *: skip ] | *: skip ]
854  | #a #st #EX
855    normalize in EX; destruct
856    whd in match (label_statement ??); @label_gen_elim #u1
857    @label_gen_elim #u2
858    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
859    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
860    % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip
861      | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]
862      | /2/ ] | /4/ ] | skip ] | skip ]
863  | #st1 #a #st2 #st #EX
864    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
865    whd in EX:(??%?); >Eskip in EX; #EX
866    whd in match (label_statement ??); @label_gen_elim #u1
867    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
868    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
869    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
870    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
871      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
872      normalize in EX; destruct
873      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
874      % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
875      | 5,10: @plus_succ [ 4,9:
876      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
877      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
878      whd in ⊢ (??%?); @refl
879      | 1,2,6,7: skip
880      | 5: @plus_one @refl
881      | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
882      | *: skip
883      ]
884      | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
885      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
886    | whd in EX:(??%%); destruct
887      % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one
888        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
889        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
890      | skip ] | skip ]
891    ]
892  | #EX inversion KL
893    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
894    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
895    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
896    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
897    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
898    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
899    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
900    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
901    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
902    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
903    ]
904    whd in match (label_statement ??);
905    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
906    [1,11,13: @plus_one @refl | 2,12,14: //
907    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
908    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
909    | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/
910    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
911    ]| *: /3/ ]|*: skip]|*: skip ]
912  | #EX inversion KL
913    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
914    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
915    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
916    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
917    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
918    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
919    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
920    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
921    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
922    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
923    ]
924    whd in match (label_statement ??);
925    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
926      [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]
927      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
928    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
929      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
930      normalize in EX; destruct
931      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
932      % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5:
933        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
934      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
935      whd in ⊢ (??%?); @refl
936      | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
937      | // | <(E0_right tr) @twel_app /2/
938      ]
939      | /3/ | /3/ ] | *: skip ] | *: skip ]
940    ]
941  | * [2: #a ] #EX
942    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
943    #Ety #EX whd in EX:(??%?);
944    [ destruct
945    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
946      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
947    | >Ety in EX; #EX
948    | @⊥ cases (fn_return f) in Ety EX;
949      [ * #H cases (H (refl ??))
950      | *: normalize #a #b #c try #d try #e destruct
951      ]
952    ]
953    whd in match (label_statement ??);
954    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
955    whd in EX:(??%%); destruct
956    % [2,4: % [2,4: % [1,3: %[1,3: @plus_one
957      whd in ⊢ (??%?);
958      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
959        whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
960      | >label_function_return >Ety in ⊢ (??%?);
961      ] whd in ⊢ (??%?); @refl
962      | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip]
963  | #a #ls #EX
964    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
965    cases v1 in EX1 EX;
966    [ 2: #sz #i #EX1 #EX
967    | *: normalize #A #B try #C destruct
968    ]
969    whd in EX:(??%%); destruct
970    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
971    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
972    % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
973      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
974      ]|skip ]| skip ]
975  | #l #st #EX
976    whd in EX:(??%?); destruct
977    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
978    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
979    %[2: %[2: %[ %[ @plus_succ
980      [ 4: @refl | 5: @plus_one @refl | *: skip ]
981      | /2/ ] | /3/ ] |skip ]| skip ]
982  | #l #EX
983    whd in EX:(??%?);
984    @blindly_label whd
985    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
986    cases (find_label ???) in ⊢ (???% → ?);
987    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
988    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
989      cases (label_find_label_fn … KL F)
990      #u' * #cs * #k1' * #F' #K'
991      % [2: %[2: %[ %[ @plus_succ
992        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ]
993        | /2/ ] | /3/ ] | skip ] | skip ]
994    ]
995  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
996    % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ]
997  ]
998| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
999  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
1000  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
1001  whd in EX:(??%%); destruct
1002  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
1003  [ % [2: % [2: % [ % [
1004    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1005                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
1006               |5: @plus_one @refl | *: skip ]
1007    | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ]
1008  | % [2: % [2: % [ % [
1009    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1010                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
1011    | 5: @plus_succ [4: @refl
1012    | 5: @plus_one @refl | *: skip ] | *: skip ]
1013    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
1014  ]
1015| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
1016  whd in EX:(??%%); destruct
1017  % [2: % [2: % [ % [
1018    @plus_succ [4: % | 5: @plus_one % | *: skip ]
1019    | /2/ ]| /4/ ]| skip ]| skip ]
1020| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
1021  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
1022  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
1023  whd in EX:(??%%); destruct
1024  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
1025  [ % [2: % [2: % [ % [
1026    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1027                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
1028    | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl
1029    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
1030  | % [2: % [2: % [ % [
1031    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1032                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
1033    | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl
1034    | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
1035    ]
1036  ]
1037| *
1038  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
1039    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
1040    whd in EX:(??%%); destruct
1041    whd in match (label_fundef ?);
1042    whd in match (label_function ?);
1043    lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
1044    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
1045    % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
1046      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
1047    | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
1048  | #id #tys #ty #args #k #k' #m #K #EX
1049    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
1050    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
1051    whd in EX2:(??%%); destruct
1052  ]
1053| #res #k #k' #m #K #EX inversion K
1054  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
1055    [ 2: * #i #EX whd in EX:(??%?); destruct
1056    | *: normalize #A try #B try #C destruct
1057    ]
1058    % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ]
1059  | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
1060    [ #EX whd in EX:(??%?); destruct
1061      % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ]
1062    | * * #b #o #ty #EX
1063      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
1064      whd in EX:(??%%); destruct
1065      % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
1066    ]
1067  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
1068       destruct whd in EX:(??%?); destruct
1069  ]
1070| #r #EX whd in EX:(??%%); destruct
1071] qed.
1072
1073
1074theorem step_with_labels : ∀ge,ge'.
1075  related_globals ? label_fundef ge ge' →
1076  ∀s1,s1',tr,s2.
1077  state_with_labels s1 s1' →
1078  (exec_step ge s1 = Value … 〈tr,s2〉 →
1079   ∃tr',s2'. plus ge' s1' tr' s2' ∧
1080             trace_with_extra_labels tr tr' ∧
1081             state_with_labels s2 s2').
1082#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
1083[ #s1 #s1' @step_with_labels_partial //
1084| #f #u *
1085(* If we have LSdefault we need to smuggle the execution of the cost label in
1086   before the actual statement. *)
1087  [ #s #k #k' #e #m #K #EX
1088    whd in EX:(??(??(??%???))?);
1089    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1090    >shift_fst whd in match (seq_of_labeled_statement ?);
1091    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)
1092    #tr' * #s2' * * #P #T #S
1093    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
1094(* but for LScase it's just like the cases in step_with_labels_partial *)
1095  | #sz #i #s #ls #k #k' #e #m #K #EX
1096    whd in EX:(??(??(??%???))?);
1097    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1098    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
1099    whd in EX:(??%?); destruct
1100    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
1101  ]   
1102] qed.
1103
1104(* FIXME: to globalenvs and prove *)
1105axiom transform_program_init_mem : ∀A,B,V,p,f,init.
1106  init_mem ?? init p = init_mem ?? init (transform_program A B V p f).
1107
1108
1109lemma initial_state_in_simulation : ∀p,s.
1110  make_initial_state p = OK ? s →
1111  ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'.
1112* #vars #fns #main #s
1113whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1114cases (bind_inversion ????? EX) -EX #m * #Em #EX
1115cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1116cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1117whd in EX:(??%%); destruct
1118whd in match (make_initial_state ?);
1119letin ge' ≝ (make_global ?)
1120cut (related_globals ? label_fundef ge ge')
1121[ // ] #RG
1122% [2: %
1123[ whd in ⊢ (??%?);
1124  change with (transform_program ??? (mk_program …) label_fundef) in match (mk_program ??? (transf_program ????) ?);
1125  <transform_program_init_mem >Em in ⊢ (??%?);
1126  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
1127  whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')
1128  whd in ⊢ (??%?); @refl
1129| /3/
1130] | skip ]
1131qed.
1132 
1133
1134
Note: See TracBrowser for help on using the repository browser.