source: src/Clight/labelSimulation.ma @ 2022

Last change on this file since 2022 was 2019, checked in by campbell, 8 years ago

Split out special induction principle for Clight from soundness file.
Put cast simplification into compiler.ma.

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