Context Navigation

labelSimulation.ma @ 2019

Last change on this file since 2019 was 2019, checked in by campbell, 9 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
2	include "Clight/label.ma".
3	include "Clight/Cexec.ma".
4	include "Clight/CexecInd.ma".
5
6	(* TODO: make something general that can live in common/Globalenvs.ma. *)
7	record 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 *)
19	axiom 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
23	whd in match (transform_program ?????);
24	whd in match (transf_program ????);
25	elim 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. *)
38	lemma 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 * //
41	qed.
42
43
44	(* Similarly, lemma to break up label_expr, label_exprs and label_statement in
45	the labelling functions *)
46	lemma 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
50	cases (L syn u)
51	#syn' #u' #H @H
52	qed.
53
54	lemma 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 ??);
58	cases (fresh ??) #l #u' @H
59	qed.
60
61
62	lemma label_expr_type : ∀e,u.
63	typeof (\fst (label_expr e u)) = typeof e.
64	* #e #ty #u >shift_fst //
65	qed.
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. *)
69	inductive 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
74	lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
75	#tr elim tr /2/
76	qed.
77
78	lemma 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/
83	qed.
84
85	theorem 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
275	lemma 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. *)
298	inductive 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
317	lemma 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/
321	qed.
322
323	(* Now define almost all of the simulation relation... *)
324	inductive 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. *)
344	inductive 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. *)
352	inductive 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. *)
357	lemma label_function_return : ∀f.
358	fn_return (label_function f) = fn_return f.
359	* #rty #params #vars #body
360	whd in ⊢ (??(?%)?);
361	cases (label_statement ??) #body' #u'
362	whd in ⊢ (??(?%)?);
363	cases (add_cost_before ??) #body'' #u''
364	//
365	qed.
366
367	lemma 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
370	qed.
371
372	lemma label_fundef_typeof_fundef : ∀fd.
373	type_of_fundef (label_fundef fd) = type_of_fundef fd.
374	* //
375	* #rty #args #vars #body
376	normalize cases (label_statement ??) #body' #u
377	normalize cases (fresh ??) //
378	qed.
379
380	lemma label_fn_params : ∀f.
381	fn_params (label_function f) = fn_params f.
382	* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
383	qed.
384
385	lemma label_fn_vars : ∀f.
386	fn_vars (label_function f) = fn_vars f.
387	* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
388	qed.
389
390	(* Some annoying rewrite rules *)
391	lemma 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
395	whd in ⊢ (??(????(???%))?); >shift_fst @refl
396	qed.
397
398	lemma 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
403	lapply (rg_find_funct … RG … vf fd)
404	cases (find_funct … vf)
405	[ #_ #E normalize in E; destruct
406	\| #fd' #H #E normalize in E; destruct >(H (refl ??)) //
407	] qed.
408
409	lemma 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
422	lemma labelled_is_not_skip : ∀s,u.
423	s ≠ Sskip →
424	∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf.
425	#s #u #NE
426	cases (is_Sskip ?)
427	[ #E @⊥ @(absurd ? E) @labelled_not_skip //
428	\| /2/
429	] qed.
430
431	lemma 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. *)
467	lemma blindly_label : ∀u,s. ∀P:statement → Prop.
468	match 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. *)
500	lemma 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/
509	qed.
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. *)
513	lemma 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
666	lemma 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
673	whd in match (label_function ?);
674	@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
675	lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?)
676	[ /2/ ]
677	>FIND //
678	qed.
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. *)
685	lemma 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
1066	theorem 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 *)
1097	axiom 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
1101	lemma 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
1105	whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1106	cases (bind_inversion ????? EX) -EX #m * #Em #EX
1107	cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1108	cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1109	whd in EX:(??%%); destruct
1110	whd in match (make_initial_state ?);
1111	letin ge' ≝ (make_global ?)
1112	cut (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 ]
1123	qed.
1124
1125
1126

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format