Context Navigation

StatusSimulationHelper.ma @ 3261

Last change on this file since 3261 was 3154, checked in by piccolo, 8 years ago
1) changed block_of_call in order to prevent pre-main calls 2) StatusSimulationHelper? in place
File size: 88.9 KB

Line
1	(**************************************************************************)
2	(* ___ *)
3	(* \|\|M\|\| *)
4	(* \|\|A\|\| A project by Andrea Asperti *)
5	(* \|\|T\|\| *)
6	(* \|\|I\|\| Developers: *)
7	(* \|\|T\|\| The HELM team. *)
8	(* \|\|A\|\| http://helm.cs.unibo.it *)
9	(* \ / *)
10	(* \ / This file is distributed under the terms of the *)
11	(* v GNU General Public License Version 2 *)
12	(* *)
13	(**************************************************************************)
14
15	include "joint/StatusSimulationUtils.ma".
16
17	lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
18	∀prog : joint_program P_in.
19	∀stack_sizes.
20	∀ f_lbls,f_regs.∀f_bl_r.∀init.∀st_no_pc_rel,st_rel.
21	∀f,fn,stmt,st1,st2.
22	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
23	st_no_pc_rel st_rel →
24	st_rel st1 st2 →
25	fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
26	return 〈f,fn,stmt〉 →
27	st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2).
28	#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
29	#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
30	cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
31	@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
32	qed.
33
34	lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
35	∀prog : joint_program P_in.
36	∀stack_sizes.
37	∀ f_lbls,f_regs.∀f_bl_r.∀init.
38	∀st_no_pc_rel,st_rel.
39	∀f,fn,stmt,st1,st2.
40	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
41	st_no_pc_rel st_rel→
42	st_rel st1 st2 →
43	fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
44	return 〈f,fn,stmt〉 →
45	pc … st1 = pc … st2.
46	#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
47	#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
48	cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
49	@(fetch_ok_pc_ok … goodR … EQfn) assumption
50	qed.
51
52	lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
53	∀prog : joint_program P_in.
54	∀stack_sizes.
55	∀ f_lbls,f_regs.∀f_bl_r.∀init.
56	∀st_no_pc_rel,st_rel.
57	∀f,fn,stmt,st1,st2.
58	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
59	st_no_pc_rel st_rel →
60	st_rel st1 st2 →
61	fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
62	return 〈f,fn,stmt〉 →
63	(last_pop … st1) =
64	sigma_stored_pc P_in P_out prog stack_sizes init f_bl_r f_lbls
65	f_regs (last_pop … st2).
66	#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
67	#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
68	cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
69	@(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption
70	qed.
71
72	lemma as_label_ok_non_entry : ∀ P_in , P_out: sem_graph_params.
73	∀prog : joint_program P_in.
74	∀stack_sizes.
75	∀ f_lbls,f_regs.∀f_bl_r.∀init.
76	∀st_no_pc_rel,st_rel.
77	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
78	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
79	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
80	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
81	st_no_pc_rel st_rel →
82	∀st1,st2,f,fn,stmt.
83	fetch_statement …
84	(joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
85	block_id … (pc_block (pc … st1)) ≠ -1 →
86	st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
87	as_label (joint_status P_in prog stack_sizes) st1 =
88	as_label (joint_status P_out trans_prog stack_sizes) st2.
89	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
90	#good #st1 #st2 #f #fn #stmt #EQfetch * #Hbl #Rst1st2 * #Hentry
91	whd in ⊢ (??%%); >EQfetch normalize nodelta
92	lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
93	[2: @eqZb_elim [1: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
94	#H cases(H EQfetch) -H \|:] #data #t_fn ** #EQt_fn #Hdata #H
95	whd in match fetch_statement; normalize nodelta
96	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn >EQt_fn
97	>m_return_bind cases stmt in EQfetch H;
98	[ * [ #c \| #id #args #dest \| #r #lb \| #seq] #nxt \| * [ #lb \| \| #has #id #args ] \| * ]
99	#EQfetch normalize nodelta * #bl
100	[1,2,3,4: @eq_identifier_elim
101	[1,3,5,7: #EQ @⊥ @Hentry >EQ %
102	\|: #_ cut(∀b.andb b false = false) [1,3,5,7: %] #EQ >EQ -EQ normalize nodelta
103	]
104	]
105	*
106	[ >(f_step_on_cost … data) whd in ⊢ (% → ?); cases(f_regs ??) [2: # x #y *]
107	normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1
108	whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQcost
109	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
110	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQcost; #EQcost >EQcost %
111	]
112	#Hregs *
113	[1,2,3: * [2,4,6: #hd #tl * #mid1 * #mid2 * #l2 *** #EQmid1 cases(\fst (\fst bl))
114	[1,3,5: whd in ⊢ (% → ?); * #EQ destruct(EQ)] #hd1 #tl1 whd in ⊢ (% → ?);
115	* #mid3 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQ
116	change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_ #_
117	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ % ]
118	* #mid1 * #mid2 * #l2 * #_ cases bl in Hregs;
119	[2,4,6: #x #y #z #w #_ whd in ⊢ (% → ?); * #a * #b ** #EQ destruct(EQ)]
120	#instr #post #Hregs whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) *
121	#nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1)
122	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ #_ >EQ
123	inversion(instr ?)
124	[2,3,4,6,7,8,10,11,12: [1,4,7: #id1 #arg1 #dest1 \|2,5,8: #r1 #lb1 \|*: #seq]
125	#EQ1 >EQ1 %] #c1 #EQc1
126	lapply(bind_new_bind_new_instantiates … Hregs (cost_in_f_step … data … c1) …
127	(jmeq_to_eq ??? EQc1)) #EQ destruct(EQ)
128	\|: [2,4,6: #hd #tl * #mid ** #_ cases (\fst bl) [1,3,5: * #EQ destruct(EQ)]
129	#hd1 #tl1 whd in ⊢ (% → ?); * #mid1 * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?);
130	* #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_
131	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ %
132	\|: #mid ** #_ cases bl in Hregs; * [2,4,6: #x #y #z #_ * #w * #a ** #EQ destruct]
133	#instr #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?);
134	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) #EQ >EQ %
135	]
136	]
137	qed.
138
139
140	lemma eval_goto_ok : ∀ P_in , P_out: sem_graph_params.
141	∀prog : joint_program P_in.
142	∀stack_sizes.
143	∀ f_lbls,f_regs.∀f_bl_r.∀init.
144	∀st_no_pc_rel,st_rel.
145	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
146	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
147	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
148	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
149	st_no_pc_rel st_rel →
150	∀st1,st1' : joint_abstract_status prog_pars_in.
151	∀st2 : joint_abstract_status prog_pars_out.
152	∀f : ident.
153	∀fn : joint_closed_internal_function P_in ?.
154	∀lbl.
155	block_id … (pc_block (pc … st1)) ≠ -1 →
156	st_rel st1 st2 →
157	let goto ≝ (GOTO P_in lbl) in
158	fetch_statement P_in ?
159	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
160	return 〈f, fn, final … goto〉 →
161	eval_state P_in …
162	(joint_globalenv P_in prog stack_sizes) st1 = return st1' →
163	∃ st2'. st_rel st1' st2' ∧
164	∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
165	bool_to_Prop (taaf_non_empty … taf) ∧
166	as_label (joint_abstract_status prog_pars_in) st1' =
167	as_label (joint_abstract_status prog_pars_out) st2'.
168	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
169	#st_rel #good #st1 #st1' #st2 #f #fn #lbl * #Hbl #Rst1st2 #EQfetch
170	whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
171	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
172	whd in match eval_statement_advance; normalize nodelta whd in match goto;
173	normalize nodelta >pc_of_label_eq
174	[2: @(proj1 … (fetch_statement_inv … EQfetch)) \|*: ]
175	>m_return_bind whd in match set_no_pc;
176	whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
177	lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
178	[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
179	#H cases(H EQfetch) -H \|*:]
180	#data * #t_fn #EQt_fn #Hdata normalize nodelta #pre #instr * #Hregs
181	* #l1 * #mid ** #EQmid #EQl1 whd in ⊢ (% → ?); #EQfin
182	cases(bind_new_bind_new_instantiates' … Hregs
183	(bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
184	EQfetch Rst1st2 …)))
185	[2: % assumption
186	\|4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
187	\|3:
188	]
189	#st2_fin ** #EQst2_fin #EQ destruct(EQ) #Hfin_rel
190	%{(mk_state_pc ? st2_fin (pc_of_point p_out (pc_block (pc … st2)) lbl)
191	(last_pop … st2))}
192	cut(? : Prop)
193	[3: #Rst1st2' %{Rst1st2'}
194	\|
195	\| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) @(st_rel_def … good)
196	[3: @(proj1 … (fetch_statement_inv … EQfetch)) \|1,2:
197	\|5: @(fetch_stmt_ok_sigma_last_pop_ok … good … Rst1st2 EQfetch)
198	\| assumption
199	]
200	]
201	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQl1; #EQl1
202	lapply(taaf_to_taa … (produce_trace_any_any_free … st2 … … EQl1 … EQst2_fin) ?)
203	[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
204	whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
205	<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind
206	whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
207	>EQfin %
208	\| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn %
209	]
210	#taa %{(taaf_step … taa …)}
211	[3: %{I}
212	\|*: whd [ whd in ⊢ (??%?); \| whd in match eval_state;] whd in match fetch_statement;
213	normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn
214	>m_return_bind >point_of_pc_of_point >EQfin [%] >m_return_bind
215	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
216	whd in match eval_statement_advance; whd in match goto; normalize nodelta
217	>pc_of_label_eq
218	[2: whd in match (pc_block ?); >EQt_fn in ⊢ (??%?); % \|3:] %
219	]
220	cases(fetch_stmt_ok_succ_ok … lbl … EQfetch) [4: %\|3: % % \|*:]
221	#stmt' #EQstmt'
222	@(as_label_ok_non_entry … good)
223	[4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt'
224	\|1,2,3:
225	\| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) % assumption
226	\| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (?%?); assumption
227	\| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch)
228	cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
229	* whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point #EQ destruct(EQ)
230	@H %
231	]
232	qed.
233
234	lemma eval_goto_premain_ok : ∀ P_in , P_out: sem_graph_params.
235	∀prog : joint_program P_in.
236	∀stack_sizes.
237	∀ f_lbls,f_regs.∀f_bl_r.∀init.
238	∀st_no_pc_rel,st_rel.
239	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
240	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
241	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
242	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
243	st_no_pc_rel st_rel →
244	∀st1,st1' : joint_abstract_status prog_pars_in.
245	∀st2 : joint_abstract_status prog_pars_out.
246	∀f : ident.
247	∀fn : joint_closed_internal_function P_in ?.
248	∀lbl.
249	block_id … (pc_block (pc … st1)) = -1 →
250	st_rel st1 st2 →
251	let goto ≝ (GOTO P_in lbl) in
252	fetch_statement P_in ?
253	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
254	return 〈f, fn, final … goto〉 →
255	eval_state P_in …
256	(joint_globalenv P_in prog stack_sizes) st1 = return st1' →
257	∃ st2'. st_rel st1' st2' ∧
258	∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
259	bool_to_Prop (taaf_non_empty … taf) ∧
260	as_label (joint_abstract_status prog_pars_in) st1' =
261	as_label (joint_abstract_status prog_pars_out) st2'.
262	#p_in #p_out #prog #stack_sizes #f_lbls #f_regs #init_regs #init #st_no_pc_rel
263	#st_rel #good #st1 #st1' #st2 #f #fn #lbl #EQbl #Rst1st2 #EQfetch #EQeval
264	cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2'
265	#EQst2' #Hlab %{st2'} % [assumption] %{(taaf_step … (taa_base …)…)}
266	[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in match joint_classify;
267	normalize nodelta >EQfetch %
268	\| assumption ] %{I} assumption
269	qed.
270
271
272	lemma eval_tailcall_ok : ∀ P_in , P_out: sem_graph_params.
273	∀prog : joint_program P_in.
274	∀stack_sizes.
275	∀ f_lbls,f_regs.∀f_bl_r.∀init.
276	∀st_no_pc_rel,st_rel.
277	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
278	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
279	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
280	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
281	st_no_pc_rel st_rel →
282	∀st1,st1' : joint_abstract_status prog_pars_in.
283	∀st2 : joint_abstract_status prog_pars_out.
284	∀f : ident.
285	∀fn : joint_closed_internal_function P_in ?.
286	∀has_tail,id,arg.
287	block_id … (pc_block (pc … st1)) ≠ -1 →
288	st_rel st1 st2 →
289	fetch_statement P_in ?
290	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
291	return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 →
292	eval_state P_in …
293	(joint_globalenv P_in prog stack_sizes) st1 = return st1' →
294	∃is_tail,st2_pre_call,t_is_tail.
295	as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧
296	∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
297	∃taa2 : trace_any_any … st2 st2_pre_call.
298	∃taa2' : trace_any_any … st2_after_call st2'.
299	eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes)
300	st2_pre_call = return st2_after_call ∧
301	st_rel st1' st2' ∧
302	as_label (joint_abstract_status prog_pars_in) st1' =
303	as_label (joint_abstract_status prog_pars_out) st2_after_call.
304	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
305	#good #st1 #st1' #st2 #f #fn #has_tail #id #arg * #Hbl #Rst1st2 #EQfetch
306	whd in match eval_state in ⊢ (% → ?); normalize nodelta >EQfetch >m_return_bind
307	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
308	whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta
309	>set_no_pc_eta #H @('bind_inversion H) -H #bl #EQbl lapply(err_eq_from_io ????? EQbl)
310	-EQbl #EQbl #H @('bind_inversion H) -H
311	* #id1 * #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
312	[2: #H @('bind_inversion H) -H #x whd in match eval_external_call; normalize nodelta
313	#H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z #_
314	#H @('bind_inversion H) -H #w whd in ⊢ (??%%→ ?); #ABS destruct(ABS) ]
315	whd in match (stack_sizes ????); #H lapply(err_eq_from_io ????? H) -H
316	#H @('bind_inversion H) -H #ssize_f #H lapply(opt_eq_from_res ???? H) -H #EQssize_f
317	#H @('bind_inversion H) -H #st1_fin whd in match eval_internal_call;
318	normalize nodelta whd in match (stack_sizes ????); #H @('bind_inversion H) -H
319	#ssize_f1 #H lapply(opt_eq_from_res ???? H) -H #EQssize_f1 #H @('bind_inversion H) -H
320	#st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
321	% [@hide_prf whd in ⊢ (??%?); >EQfetch %]
322	lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
323	[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
324	#H cases(H EQfetch) -H \|*:]
325	#data * #t_fn #EQt_fn #Hdata normalize nodelta #pre #instr * #Hregs *
326	#l1 * #mid ** #EQmid #EQpre whd in ⊢ (% → ?); #EQmid
327	cut(? : Prop)
328	[3: #EQint_fn1
329	lapply(b_graph_transform_program_fetch_internal_function … good bl id1 fn1)
330	@eqZb_elim [ #ABS cases(block_of_call_no_minus_one … EQbl) >ABS #H @⊥ @H % ]
331	#_ normalize nodelta
332	#H cases(H EQint_fn1) -H #data1 * #t_fn1 ** #EQt_fn1 #Hregs1 #good1
333	cases(bind_new_bind_new_instantiates' … Hregs
334	(bind_new_bind_new_instantiates' ?????? Hdata
335	(tailcall_commutation ?????????? good ???????? EQfetch ? EQbl … EQint_fn1 …
336	EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1))) [2: % assumption]
337	#has_tail' * #id' * #arg' * #EQ destruct(EQ) * #st2_pre ** #EQst2_pre #EQt_bl
338	* #st2_after * #EQst2_after #H cases(bind_new_bind_new_instantiates' … Hregs1 H)
339	-H #st2' * #EQst2' #fin_sem_rel
340	\|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %
341	\|
342	]
343	%{(mk_state_pc ? st2_pre (pc_of_point p_out (pc_block … (pc … st2)) mid) (last_pop … st2))}
344	%
345	[ @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
346	<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind
347	>point_of_pc_of_point >EQmid % ]
348	%
349	[ whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [_ ⇒ ? \| _ ⇒ ?]));
350	whd in match fetch_statement; normalize nodelta
351	<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in
352	⊢ (??(match % with [_ ⇒ ? \| _ ⇒ ?])?);
353	>EQt_fn in ⊢ (??(match % with [_ ⇒ ? \| _ ⇒ ?])?);
354	>m_return_bind in ⊢ (??(match % with [_ ⇒ ? \| _ ⇒ ?])?);
355	>point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? \| _ ⇒ ?])?);
356	>EQmid in ⊢ (??(match % with [_ ⇒ ? \| _ ⇒ ?])?); normalize nodelta
357	>EQbl >EQt_bl >m_return_bind >m_return_bind >EQt_fn1 >EQint_fn1 %
358	]
359	%{(mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after)
360	(pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
361	%{(mk_state_pc ? st2' (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))}
362	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn
363	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre
364	%{(taaf_to_taa … (produce_trace_any_any_free … st2 … EQt_fn … EQpre EQst2_pre) …)}
365	[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
366	whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
367	>point_of_pc_of_point >EQmid % ]
368	cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
369	#nxt1 * #c #EQin #H lapply(H … EQin) -H normalize nodelta >(f_step_on_cost … data1)
370	* #st_bl @eq_identifier_elim [2: * #H @⊥ @H % #_ ] #_
371	cases(added_prologue … data1) in EQst2';
372	[ whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta * whd in ⊢ (% → ?);
373	inversion(f_regs ??) normalize nodelta [2: #x #y #_ #_ *] #EQregs #EQ destruct(EQ)
374	* #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
375	#nxt2 * #EQt_cost change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) *
376	#EQ1 #EQ2 destruct(EQ1 EQ2) #EQentry >EQentry %{(taa_base …)}
377	\| #hd #tl #EQst2' * normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??)
378	[2: #x #y #_ #_ ] #EQregs normalize nodelta #EQ destruct(EQ) #l1 * #mid1 * #mid2
379	* #l2 *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?);
380	* #nxt2 * #EQnop change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
381	* #EQ1 #EQ2 destruct(EQ1 EQ2) * #star * #_ whd in ⊢ (% → ?); * #l3 * #mid3 * #mid4
382	* #l4 *** #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt2 * #EQt_cost
383	change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl4
384	letin trans_prog ≝ (b_graph_transform_program ????)
385	lapply(taaf_to_taa …
386	(produce_trace_any_any_free … (mk_prog_params p_out trans_prog stack_size)
387	(mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after)
388	(pc_of_point p_out bl mid4) (last_pop … st2)) … EQt_fn1 … EQst2') ?)
389	[4: >point_of_pc_of_point in ⊢ (????%???); assumption
390	\| @if_elim #_ [2: @I] % * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement;
391	normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQnop %
392	\|*:]
393	#taa %{(taa_step … taa)}
394	[ % * #H @H whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
395	>EQt_fn1 >m_return_bind >point_of_pc_of_point cases EQl4 #mid5 * #rest **
396	#EQ destruct(EQ) * #nxt3 * #EQ #_ #_ >EQ %
397	\|2,3: whd [ whd in ⊢ (??%?); \| whd in match eval_state; ]
398	whd in match fetch_statement; normalize nodelta >EQt_fn1
399	>m_return_bind >point_of_pc_of_point >EQt_cost [2: %] >m_return_bind %
400	]
401	]
402	%
403	[2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??); whd in match (as_pc_of ??);
404	whd in match fetch_statement; normalize nodelta >EQint_fn1 >EQt_fn1
405	>m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta
406	>point_of_offset_of_point >point_of_offset_of_point >EQin >m_return_bind
407	normalize nodelta >EQt_cost >m_return_bind normalize nodelta [ %]
408	whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%);
409	whd in match (get_first_costlabel_next ???);
410	generalize in match (refl ??);
411	>EQin in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ? \| _ ⇒ ?]?))));
412	#EQcost' normalize nodelta %
413	]
414	%
415	[1,3: whd in match eval_state; whd in match fetch_statement; normalize nodelta
416	>EQt_fn >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
417	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
418	whd in match eval_statement_advance; whd in match eval_tailcall;
419	normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1)
420	* #id2 * #fn2 normalize nodelta #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
421	>EQ -EQ >m_return_bind normalize nodelta whd in match (stack_sizes ????);
422	>EQssize_f >m_return_bind whd in match eval_internal_call; normalize nodelta
423	whd in match (stack_sizes ????); >EQssize_f1 >m_return_bind >EQst2_after
424	>m_return_bind [2: %] whd in match set_no_pc; normalize nodelta >EQentry %
425	\|*: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn1 \|1,2,5,6:]
426	@(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption
427	]
428	qed.
429
430	lemma eval_tailcall_premain_ok : ∀ P_in , P_out: sem_graph_params.
431	∀prog : joint_program P_in.
432	∀stack_sizes.
433	∀ f_lbls,f_regs.∀f_bl_r.∀init.
434	∀st_no_pc_rel,st_rel.
435	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
436	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
437	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
438	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
439	st_no_pc_rel st_rel →
440	∀st1,st1' : joint_abstract_status prog_pars_in.
441	∀st2 : joint_abstract_status prog_pars_out.
442	∀f : ident.
443	∀fn : joint_closed_internal_function P_in ?.
444	∀has_tail,id,arg.
445	block_id … (pc_block (pc … st1)) = -1 →
446	st_rel st1 st2 →
447	fetch_statement P_in ?
448	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
449	return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 →
450	eval_state P_in …
451	(joint_globalenv P_in prog stack_sizes) st1 = return st1' →
452	∃is_tail,st2_pre_call,t_is_tail.
453	as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧
454	∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
455	∃taa2 : trace_any_any … st2 st2_pre_call.
456	∃taa2' : trace_any_any … st2_after_call st2'.
457	eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes)
458	st2_pre_call = return st2_after_call ∧
459	st_rel st1' st2' ∧
460	as_label (joint_abstract_status prog_pars_in) st1' =
461	as_label (joint_abstract_status prog_pars_out) st2_after_call.
462	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
463	#st_rel #good #st1 #st1' #st2 #f #fn #has #id #arg #EQbl #Rst1st2 #EQfetch
464	#EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' **
465	#Rst1st2' #EQst2' #Hlab % [ @hide_prf whd in ⊢ (??%?); >EQfetch %] %{st2}
466	% [ @hide_prf change with (joint_classify ???) in ⊢ (??%?); <Hclass
467	whd in ⊢ (??%?); >EQfetch %]
468	%
469	[ letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog)
470	cut(∃f',fn',has',id',arg'.
471	fetch_statement p_out … (joint_globalenv p_out trans_prog stack_size)
472	(pc … st2) = return 〈f',fn',final ?? (TAILCALL p_out has' id' arg')〉)
473	[ lapply Hclass whd in ⊢ (??%? → ?); >EQfetch whd in match joint_classify_final;
474	normalize nodelta whd in match joint_classify; normalize nodelta
475	inversion (fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct(EQ)]
476	** #f' #fn' *
477	[ * [ #c \| #c_id #arg #dest \| #r #lbl \| #seq ] #nxt \| * [ #lbl \| \| #has' #id' #arg' ] \| *]
478	#EQt_fetch normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ)
479	%{f'} %{fn'} %{has'} %{id'} %{arg'} % ]
480	* #f' * #fn' * #has' * #id' * #arg' #EQt_fetch
481	@('bind_inversion EQeval) #x >EQfetch in ⊢ (% → ?); whd in ⊢ (??%% → ?);
482	#EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
483	whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta
484	#H @('bind_inversion H) -H #bl #H lapply(err_eq_from_io ????? H) -H #EQbl
485	#H @('bind_inversion H) -H * #f1 * #fn1 #H lapply(err_eq_from_io ????? H) -H
486	#EQfn1 normalize nodelta
487	[2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
488	#H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
489	#H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ)
490	]
491	#H lapply(err_eq_from_io ????? H) -H #H@('bind_inversion H) -H #f_ssize
492	#H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf_ssize
493	#H @('bind_inversion H) -H #st1_fin whd in match eval_internal_call; normalize nodelta
494	#H @('bind_inversion H) -H #f1_ssize #H lapply(opt_eq_from_res ???? H) -H
495	whd in match (stack_sizes ????); #EQf1_ssize #H @('bind_inversion H) -H
496	#st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
497	@('bind_inversion EQst2') #x >EQt_fetch in ⊢ (% → ?); whd in ⊢ (??%% → ?);
498	#EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta
499	>m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall;
500	normalize nodelta #H @('bind_inversion H) -H #bl' #H lapply(err_eq_from_io ????? H)
501	-H #EQbl' #H @('bind_inversion H) -H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H)
502	-H #EQfn1' normalize nodelta
503	[2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
504	#H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
505	#H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ)
506	]
507	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #f_ssize'
508	#H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf_ssize'
509	#H @('bind_inversion H) -H #st2_fin whd in match eval_internal_call;
510	normalize nodelta #H @('bind_inversion H) -H #f1_ssize' #H lapply(opt_eq_from_res ???? H)
511	-H whd in match (stack_sizes ????); #EQf1_ssize' #H @('bind_inversion H) -H
512	#st2_setup #EQst2_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
513	whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [ _ ⇒ ? \| _ ⇒ ? ]));
514	normalize nodelta >EQt_fetch in ⊢ (??(match % with [ _ ⇒ ? \| _ ⇒ ? ])?);
515	normalize nodelta >EQbl >EQbl' >m_return_bind >m_return_bind
516	whd in match fetch_internal_function; normalize nodelta
517	lapply(fetch_ok_pc_ok … good … Rst1st2' ?)
518	[ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); %
519	\|*:
520	]
521	whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ)
522	>EQfn1 >EQfn1' >m_return_bind >m_return_bind normalize nodelta
523	lapply EQfn1 whd in match fetch_function; normalize nodelta
524	@eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) #H @H assumption]
525	#Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H)
526	#f2 #EQf2 #H @('bind_inversion H) -H #fn2 #_ whd in ⊢ (??%? → ?); -e0 -EQ
527	#EQ destruct(EQ) -H lapply EQfn1' whd in match fetch_function; normalize nodelta
528	@eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta
529	#H lapply(opt_eq_from_res ???? H) -H
530	whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta
531	whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta
532	whd in match transform_joint_program; normalize nodelta
533	>(symbol_for_block_transf ??? (λx.x) prog
534	(λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?);
535	>EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) -H #fn2' #_
536	whd in ⊢ (??%% → ?); #EQ destruct(EQ) %
537	]
538	%{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [2: assumption] %{EQst2' Rst1st2'}
539	qed.
540
541
542	lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
543	∀prog : joint_program P_in.
544	∀stack_sizes.
545	∀ f_lbls,f_regs.∀f_bl_r.∀init.
546	∀st_no_pc_rel,st_rel.
547	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
548	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
549	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
550	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
551	st_no_pc_rel st_rel →
552	∀st1,st1' : joint_abstract_status prog_pars_in.
553	∀st2 : joint_abstract_status prog_pars_out.
554	∀f : ident.
555	∀fn : joint_closed_internal_function P_in ?.
556	∀a,ltrue,lfalse.
557	block_id … (pc_block (pc … st1)) ≠ -1 →
558	st_rel st1 st2 →
559	let cond ≝ (COND P_in ? a ltrue) in
560	fetch_statement P_in ?
561	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
562	return 〈f, fn, sequential … cond lfalse〉 →
563	eval_state P_in …
564	(joint_globalenv P_in prog stack_sizes) st1 = return st1' →
565	as_costed (joint_abstract_status prog_pars_in) st1' →
566	∃ st2'. st_rel st1' st2' ∧
567	∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
568	bool_to_Prop (taaf_non_empty … taf) ∧
569	as_label (joint_abstract_status prog_pars_in) st1' =
570	as_label (joint_abstract_status prog_pars_out) st2'.
571	#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
572	#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2
573	#EQfetch #EQeval
574	@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
575	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
576	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
577	#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
578	cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
579	[ >(pc_of_label_eq … EQfn)
580	normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
581	\| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
582	]
583	#EQ destruct(EQ) #n_costed
584	lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
585	[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
586	#H cases(H EQfetch) -H \|*:]
587	#init_data * #t_fn1 ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
588	#EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta
589	*** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
590	[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
591	whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
592	#ABS #_ lapply(fetch_statement_inv … EQfetch) * #_
593	>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
594	whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
595	<ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
596	]
597	#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
598	#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
599	* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
600	cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
601	(cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
602	[2,4: % assumption]
603	#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
604	cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
605	normalize nodelta
606	#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v'
607	[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
608	(last_pop … st2))}
609	\| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
610	(last_pop … st2))}
611	]
612	letin st1' ≝ (mk_state_pc P_in ???)
613	letin st2' ≝ (mk_state_pc P_out ???)
614	cut(st_rel st1' st2')
615	[1,3: @(st_rel_def … goodR … f fn ?)
616	[1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
617	\|2,5: assumption
618	\|3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
619	]
620	]
621	#H_fin
622	%
623	[1,3: assumption]
624	>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
625	lapply(taaf_to_taa ???
626	(produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
627	seq_pre_l EQst_pre_mid_no_pc) ?)
628	[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
629	whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
630	whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
631	>point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >EQt_cond *
632	#H @H %
633	]
634	#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???)}
635	[1,5: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
636	[2: @ltrue\|3: %2 % % \|4: % \|6: @lfalse \|7: % % \|8: %] #stmt' #EQstmt'
637	whd <(as_label_ok_non_entry … goodR … EQstmt' ? H_fin)
638	[1,4: assumption
639	\|2,5: cases(entry_unused … (pi2 ?? fn) … EQstmt)
640	[ whd in match stmt_forall_labels; whd in match stmt_labels;
641	normalize nodelta #H cases(append_All … H) #_
642	whd in match stmt_explicit_labels; whd in match step_labels;
643	normalize nodelta * whd in match (point_of_label ????);
644	* #H1 #_ #_ >point_of_pc_of_point % #H2 @H1 >H2 %
645	\| ** whd in match (point_of_label ????); #H1 #_ #_ % whd in match st1';
646	#H2 @H1 <H2 whd in match succ_pc; whd in match point_of_pc;
647	normalize nodelta whd in match pc_of_point; normalize nodelta
648	>point_of_offset_of_point %
649	]
650	\|*: % assumption
651	]
652	\|2,6: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
653	>EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
654	>EQt_cond %
655	\|3,7: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
656	>EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond
657	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
658	whd in match eval_statement_advance; normalize nodelta >EQbv' >m_return_bind
659	>rel_v_v' >m_return_bind normalize nodelta
660	[ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)]
661	>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) %
662	\|*: %{I} cases(fetch_stmt_ok_succ_ok … (pc … st1') … EQfetch)
663	[4,8: %
664	\|3: whd in match stmt_labels; normalize nodelta @Exists_append2
665	whd in match stmt_explicit_labels; whd in match step_labels;
666	normalize nodelta %1 //
667	\|7: @Exists_append1 %1 %
668	\|2,6:
669	]
670	#stmt' #EQstmt' @(as_label_ok_non_entry … goodR)
671	[4,11: @EQstmt'
672	\|1,2,3,8,9,10:
673	\|5,12: % assumption
674	\|6,13: assumption
675	\|*: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
676	[ * #_ ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H <H1
677	>point_of_pc_of_point %
678	\| ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H <H1
679	>point_of_pc_of_point %
680	]
681	]
682	]
683	qed.
684
685	lemma eval_cond_premain_ok : ∀ P_in , P_out: sem_graph_params.
686	∀prog : joint_program P_in.
687	∀stack_sizes.
688	∀ f_lbls,f_regs.∀f_bl_r.∀init.
689	∀st_no_pc_rel,st_rel.
690	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
691	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
692	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
693	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
694	st_no_pc_rel st_rel →
695	∀st1,st1' : joint_abstract_status prog_pars_in.
696	∀st2 : joint_abstract_status prog_pars_out.
697	∀f : ident.
698	∀fn : joint_closed_internal_function P_in ?.
699	∀a,ltrue,lfalse.
700	block_id … (pc_block (pc … st1)) = -1 →
701	st_rel st1 st2 →
702	let cond ≝ (COND P_in ? a ltrue) in
703	fetch_statement P_in ?
704	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
705	return 〈f, fn, sequential … cond lfalse〉 →
706	eval_state P_in …
707	(joint_globalenv P_in prog stack_sizes) st1 = return st1' →
708	as_costed (joint_abstract_status prog_pars_in) st1' →
709	∃ st2'. st_rel st1' st2' ∧
710	∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
711	bool_to_Prop (taaf_non_empty … taf) ∧
712	as_label (joint_abstract_status prog_pars_in) st1' =
713	as_label (joint_abstract_status prog_pars_out) st2'.
714	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
715	#st_rel #good #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #EQbl #Rst1st2 #EQfetch
716	#EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2'
717	** #Rst1st2' #EQst2' #Hlab whd in ⊢ (% → ?); * #ncost %{st2'} %{Rst1st2'}
718	%{(taaf_step_jump … (taa_base …) …)}
719	[ whd <Hlab % assumption
720	\| whd change with (joint_classify ???) in ⊢ (??%?); <Hclass
721	whd in match joint_classify; normalize nodelta >EQfetch %
722	\| assumption
723	]
724	%{I} assumption
725	qed.
726
727
728	lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
729	∀prog : joint_program P_in.
730	∀stack_sizes.
731	∀ f_lbls,f_regs.∀f_bl_r.∀init.
732	∀st_no_pc_rel,st_rel.
733	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
734	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
735	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
736	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
737	st_no_pc_rel st_rel →
738	∀st1,st1' : joint_abstract_status prog_pars_in.
739	∀st2 : joint_abstract_status prog_pars_out.
740	∀f.∀fn : joint_closed_internal_function P_in ?.
741	∀stmt,nxt.
742	block_id … (pc_block (pc … st1)) ≠ -1 →
743	st_rel st1 st2 →
744	let seq ≝ (step_seq P_in ? stmt) in
745	fetch_statement P_in …
746	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
747	return 〈f, fn, sequential ?? seq nxt〉 →
748	eval_state P_in … (joint_globalenv P_in prog stack_sizes)
749	st1 = return st1' →
750	∃st2'. st_rel st1' st2' ∧
751	∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
752	if taaf_non_empty … taf then True else (IT CAN BE SIMPLIFIED )
753	(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
754	¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1') ∧
755	as_label (joint_abstract_status prog_pars_in) st1' =
756	as_label (joint_abstract_status prog_pars_out) st2'.
757	#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel
758	#goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval
759	@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
760	#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
761	#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
762	whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
763	lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
764	[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
765	#H cases(H EQfetch) -H \|*:]
766	#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
767	#EQt_fn #Hinit normalize nodelta * #bl * @if_elim
768	[ @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] whd in match point_of_pc;
769	normalize nodelta whd in match (point_of_offset ??); #ABS #_
770	lapply(fetch_statement_inv … EQfetch) * #_
771	>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
772	normalize nodelta whd in match (point_of_offset ??); <ABS
773	cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
774	]
775	#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
776	>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
777	cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit
778	(seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
779	[2: % assumption]
780	#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
781	%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
782	cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
783	#EQfn #_ cut(? : Prop) [3: #Hfin % [@Hfin] \|1:
784	\| @(st_rel_def ?????????? goodR … f fn)
785	[ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
786	\| <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
787	\| @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
788	]
789	]
790	%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
791	SBiC EQst2_fin_no_pc)}
792	% [ @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch % ]
793	cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4: % \|3: % % \|2:]
794	#stmt' #EQstmt' @(as_label_ok_non_entry … goodR)
795	[4: <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt'
796	\|1,2,3:
797	\| % <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) assumption
798	\| assumption
799	\| cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
800	* whd in match (point_of_label ????); * #H #_ #_ % #H1 @H <H1 whd in match succ_pc;
801	whd in match point_of_pc; whd in match pc_of_point; normalize nodelta
802	>point_of_offset_of_point %
803	]
804	qed.
805
806	lemma general_eval_seq_no_call_premain_ok :∀ P_in , P_out: sem_graph_params.
807	∀prog : joint_program P_in.
808	∀stack_sizes.
809	∀ f_lbls,f_regs.∀f_bl_r.∀init.
810	∀st_no_pc_rel,st_rel.
811	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
812	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
813	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
814	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
815	st_no_pc_rel st_rel →
816	∀st1,st1' : joint_abstract_status prog_pars_in.
817	∀st2 : joint_abstract_status prog_pars_out.
818	∀f.∀fn : joint_closed_internal_function P_in ?.
819	∀stmt,nxt.
820	block_id … (pc_block (pc … st1)) = -1 →
821	st_rel st1 st2 →
822	let seq ≝ (step_seq P_in ? stmt) in
823	fetch_statement P_in …
824	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
825	return 〈f, fn, sequential ?? seq nxt〉 →
826	eval_state P_in … (joint_globalenv P_in prog stack_sizes)
827	st1 = return st1' →
828	∃st2'. st_rel st1' st2' ∧
829	∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
830	bool_to_Prop (taaf_non_empty … taf) ∧
831	as_label (joint_abstract_status prog_pars_in) st1' =
832	as_label (joint_abstract_status prog_pars_out) st2'.
833	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
834	#st_rel #good #st1 #st1' #st2 #f #fn #stmt #nxt #EQbl #Rst1st2 #EQfetch
835	#EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2'
836	** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)}
837	[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in match joint_classify;
838	normalize nodelta >EQfetch %
839	\| assumption
840	]
841	%{I} assumption
842	qed.
843
844	lemma general_eval_cost_ok :
845	∀ P_in , P_out: sem_graph_params.
846	∀prog : joint_program P_in.
847	∀stack_sizes.
848	∀ f_lbls,f_regs.∀f_bl_r.∀init.
849	∀st_no_pc_rel,st_rel.
850	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
851	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
852	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
853	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
854	st_no_pc_rel st_rel →
855	∀st1,st1' : joint_abstract_status prog_pars_in.
856	∀st2 : joint_abstract_status prog_pars_out.
857	∀f.
858	∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
859	block_id … (pc_block (pc … st1)) ≠ -1 →
860	st_rel st1 st2 →
861	let cost ≝ COST_LABEL P_in ? c in
862	fetch_statement P_in …
863	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
864	return 〈f, fn, sequential ?? cost nxt〉 →
865	eval_state P_in … (ev_genv … prog_pars_in)
866	st1 = return st1' →
867	∃ st2'. st_rel st1' st2' ∧
868	∃taf : trace_any_any_free
869	(joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
870	st2 st2'.
871	bool_to_Prop (taaf_non_empty … taf) ∧
872	as_label (joint_abstract_status prog_pars_in) st1' =
873	as_label (joint_abstract_status prog_pars_out) st2'.
874	#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
875	#st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta
876	#EQfetch
877	whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta
878	>EQfetch >m_return_bind normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
879	#EQ destruct(EQ)
880	%{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt)
881	(last_pop … st2))}
882	cut(? : Prop) [3: #Hfin % [@Hfin] \|
883	\| cases(fetch_statement_inv … EQfetch) #EQfn #_
884	<(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
885	whd in match (succ_pc ???); whd in match (point_of_succ ???);
886	>set_no_pc_eta
887	@(st_rel_def … prog … stack_size … goodR
888	(st_no_pc … st1) (st_no_pc … st2)) [3: >EQfn in ⊢ (??%?); %\|1,2:]
889	[ @(cost_commutation … prog … stack_size … goodR … EQfetch) [ % assumption]
890	@(fetch_stmt_ok_sigma_state_ok … goodR … Rst1st2 EQfetch)
891	\| @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch)
892	]
893	]
894	lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
895	[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
896	#H cases(H EQfetch) -H \|*:]
897	#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
898	#EQt_fn #Hinit normalize nodelta * #bl *
899	@if_elim @eq_identifier_elim [2: #_ cases(not_emptyb ??) *]
900	[ #EQentry inversion(not_emptyb ??) [2: #_ *] #non_empty_pre #_ whd in ⊢ (% → ?);
901	inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
902	whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?);
903	* #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
904	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
905	* #EQ1 #EQ2 destruct(EQ1 EQ2)
906	\| #EQentry inversion(not_emptyb ??) [ #_ *] #empty_pre #_
907	>(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *]
908	#EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 *
909	#mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt
910	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
911	\| #EQentry #_ >(f_step_on_cost … init_data) whd in ⊢ (% → ?);
912	inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
913	* #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
914	#nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
915	* #EQ1 #EQ2 destruct(EQ1 EQ2)
916	]
917	%{(taaf_step … (taa_base …) …)}
918	[3,6,9: %{I}
919	\|*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
920	>EQt_fn >m_return_bind >EQt_stmt >m_return_bind %
921	]
922	cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4,8,12: % \|2,6,10: \|3,7,11: % %]
923	#stmt' #EQstmt' @(as_label_ok_non_entry … goodR)
924	[4,11,18: @EQstmt'
925	\|1,2,3,8,9,10,15,16,17:
926	\|5,12,19: % assumption
927	\|6,13,20: assumption
928	\|*: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
929	* whd in match (point_of_label ????); * #H #_ #_ % #H1 @H <H1 whd in match succ_pc;
930	whd in match point_of_pc; whd in match pc_of_point; normalize nodelta
931	>point_of_offset_of_point %
932	]
933	qed.
934
935	lemma general_eval_cost_premain_ok :
936	∀ P_in , P_out: sem_graph_params.
937	∀prog : joint_program P_in.
938	∀stack_sizes.
939	∀ f_lbls,f_regs.∀f_bl_r.∀init.
940	∀st_no_pc_rel,st_rel.
941	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
942	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
943	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
944	good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
945	st_no_pc_rel st_rel →
946	∀st1,st1' : joint_abstract_status prog_pars_in.
947	∀st2 : joint_abstract_status prog_pars_out.
948	∀f.
949	∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
950	block_id … (pc_block (pc … st1)) = -1 →
951	st_rel st1 st2 →
952	let cost ≝ COST_LABEL P_in ? c in
953	fetch_statement P_in …
954	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
955	return 〈f, fn, sequential ?? cost nxt〉 →
956	eval_state P_in … (ev_genv … prog_pars_in)
957	st1 = return st1' →
958	∃ st2'. st_rel st1' st2' ∧
959	∃taf : trace_any_any_free
960	(joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
961	st2 st2'.
962	bool_to_Prop (taaf_non_empty … taf) ∧
963	as_label (joint_abstract_status prog_pars_in) st1' =
964	as_label (joint_abstract_status prog_pars_out) st2'.
965	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
966	#good #st1 #st1' #st2 #f #fn #c #nxt #EQbl #Rst1st2 #EQfetch #EQeval
967	cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2'
968	** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)}
969	[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass
970	whd in match joint_classify; normalize nodelta >EQfetch %
971	\| assumption
972	]
973	%{I} assumption
974	qed.
975
976	lemma next_of_call_pc_inv : ∀pars.∀prog. ∀stack_size.
977	∀pc,nxt.
978	next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size)) pc
979	= return nxt →
980	∃id,fn,c_id,c_args,c_dest.
981	fetch_statement pars
982	… (ev_genv … (mk_prog_params pars prog stack_size)) pc =
983	return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉.
984	#pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta
985	#H @('bind_inversion H) -H ** #id #fn *
986	[ *[ #c \| #c_id #c_arg #c_dest \| #reg #lbl \| #seq ] #prox \| #fin \| #H #r #l #l ]
987	#EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
988	%{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption
989	qed.
990
991	lemma stored_pc_inj :
992	∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
993	sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
994	block_id (pc_block pc) ≠ OZ →
995	sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
996	sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
997	pc = pc'.
998	#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H *#H1
999	whd in match sigma_stored_pc; normalize nodelta
1000	inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1
1001	normalize nodelta inversion(sigma_pc_opt ?????????)
1002	[ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1 whd in match sigma_pc_opt;
1003	normalize nodelta @if_elim
1004	[ #Hbl whd in ⊢ (??%? → ?); #EQ destruct(EQ) lapply(Hbl) -Hbl @eqZb_elim
1005	[whd in ⊢ (??%% → ?); #EQ destruct(EQ)] @eqZb_elim [#ABS >ABS in H1; #H @⊥ @H %]
1006	@⊥ @H1 %]
1007	#Hbl normalize nodelta #H @('bind_inversion H) -H #lbl whd in match sigma_label;
1008	normalize nodelta >code_block_of_block_eq >m_return_bind
1009	>fetch_internal_function_no_zero [ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
1010	>(pc_block_eq … H) whd in match sigma_stored_pc; normalize nodelta >EQpc1 %
1011	]
1012	#pc2 #EQpc2 normalize nodelta #EQ destruct(EQ)
1013	@(sigma_stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs …)
1014	[ assumption] >EQpc1 >EQpc2 %
1015	qed.
1016
1017	lemma eval_return_ok :
1018	∀ P_in , P_out: sem_graph_params.
1019	∀prog : joint_program P_in.
1020	∀stack_sizes.
1021	∀ f_lbls,f_regs.∀f_bl_r.∀init.
1022	∀st_no_pc_rel,st_rel.
1023	let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
1024	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
1025	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
1026	∀good : good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1027	st_no_pc_rel st_rel.
1028	∀st1,st1' : joint_abstract_status prog_pars_in.
1029	∀st2 : joint_abstract_status prog_pars_out.
1030	∀f.
1031	∀fn : joint_closed_internal_function P_in ?.
1032	block_id … (pc_block (pc … st1)) ≠ -1 →
1033	st_rel st1 st2 →
1034	fetch_statement P_in …
1035	(joint_globalenv P_in prog stack_sizes) (pc … st1) =
1036	return 〈f, fn,final P_in ? (RETURN …)〉 →
1037	eval_state P_in … (ev_genv … prog_pars_in)
1038	st1 = return st1' →
1039	∃st2_ret,st2_after_ret,st2' : joint_abstract_status prog_pars_out.
1040	∃taa2 : trace_any_any … st2 st2_ret.
1041	∃taa2' : trace_any_any_free … st2_after_ret st2'.
1042	(if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
1043	as_classifier … st2_ret cl_return ∧
1044	as_execute … st2_ret st2_after_ret ∧ st_rel st1' st2' ∧
1045	ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret ∧
1046	as_label (joint_abstract_status prog_pars_in) st1' =
1047	as_label (joint_abstract_status prog_pars_out) st2'.
1048	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
1049	#st_rel #good #st1 #st1' #st2 #f #fn #Hbl #Rst1st2 #EQfetch
1050	whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
1051	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
1052	whd in match eval_statement_advance; whd in match eval_return; normalize nodelta
1053	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #ssize
1054	#H lapply(opt_eq_from_res ???? H) -H change with (stack_size f) in ⊢ (??%? → ?);
1055	#EQssize #H @('bind_inversion H) -H * #st_pop #pc_pop #EQpop #H @('bind_inversion H)
1056	-H #next_of_call #EQnext_of_call whd in ⊢ (??%% → ?); whd in match next;
1057	whd in match set_last_pop; whd in match set_pc; normalize nodelta #EQ destruct(EQ)
1058	lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
1059	[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta
1060	#H cases(H EQfetch) -H \|*:]
1061	#data * #t_fn ** #EQt_fn >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn;
1062	#EQt_fn #Hinit normalize nodelta ** #pre #fin_s * #Hregs * #pre * #mid
1063	** #EQmid #EQpre whd in ⊢ (% → ?); #EQt_stmt
1064	cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall
1065	<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs
1066	cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' … Hinit
1067	(return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall …
1068	Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
1069	** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta
1070	[ * #sem_rel #EQt_next
1071	%{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))}
1072	%{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop)
1073	(pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)}
1074	%{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop)
1075	(pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)}
1076	%{((taaf_to_taa …
1077	(produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))}
1078	[ @if_elim #_ [2: @I] % * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement;
1079	normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt % ]
1080	%{(taaf_base …)} cut(? : Prop)
1081	[3: #Hfin % [ %
1082	[ % [ % [%{I} ]
1083	whd [whd in ⊢ (??%?); \| whd in match eval_state;] whd in match fetch_statement;
1084	normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt [%]
1085	>m_return_bind whd in match eval_statement_no_pc; normalize nodelta
1086	>m_return_bind whd in match eval_statement_advance; whd in match eval_return;
1087	normalize nodelta whd in match (stack_sizes ????); >EQssize >m_return_bind
1088	>EQt_pop >m_return_bind >EQt_next >m_return_bind %
1089	\| @Hfin
1090	]
1091	\| whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i
1092	#calling * #id1 * #arg1 * #dest1 * #nxt' #EQfetch_call * #s2_pre #s2_call
1093	whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQ destruct(EQ)
1094	whd in ⊢ (??%% → ?); whd in match (point_of_succ ???);
1095	whd in match (point_of_succ ???); #EQ cut(next_of_call =nxt')
1096	[ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) cases next_of_call in e0; #x
1097	normalize nodelta whd in match (offset_of_point ??); cases nxt' #y
1098	normalize nodelta #EQ1 destruct(EQ1) % ]
1099	-EQ #EQ destruct(EQ) whd in ⊢ (% → ?); <EQt_pc_pop #EQ1
1100	lapply(stored_pc_inj … EQ1)
1101	[2: % #ABS cases(fetch_statement_inv … EQcall) <EQt_pc_pop
1102	>fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc;
1103	normalize nodelta >ABS %
1104	\| % #ABS cases(next_of_call_pc_inv … EQt_next) #x * #y * #z * #w * #a
1105	whd in match fetch_statement; normalize nodelta >fetch_internal_function_no_zero
1106	[whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] assumption
1107	] #EQ2 destruct(EQ2) whd
1108	cases(next_of_call_pc_inv … EQt_next) #id'' * #fn'' * #c_id'' * #c_args''
1109	* #c_dest'' #EQ3 >EQ3 normalize nodelta % [%] % ] ]
1110	\|2: whd in match succ_pc; normalize nodelta whd in match (point_of_succ ???);
1111	destruct(EQt_pc_pop) lapply(proj1 ?? (fetch_statement_inv … EQcall))
1112	<pc_block_eq in Hbl_pcpop sem_rel ⊢ %;
1113	[2: % #H cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero
1114	[ #EQ destruct] whd in match sigma_stored_pc; normalize nodelta >H %]
1115	#Hbl_pcpop #sem_rel #EQ @(st_rel_def … good … sem_rel … ) [3: @EQ \|1,2:] %
1116	\|
1117	]
1118	cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % \|3: % % \|2:]
1119	#stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc_pop)) (neg one))
1120	[ #Hbl @(as_label_premain_ok ?????????? good) [assumption \| assumption ]
1121	\| #Hbl_pc_pop @(as_label_ok_non_entry … good)
1122	[4: @EQstmt'
1123	\|1,2,3:
1124	\| assumption
1125	\| assumption
1126	\| cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall)))
1127	* whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point
1128	#H1 @H <H1 %
1129	]
1130	]
1131	]
1132	cases(fetch_statement_sigma_stored_pc … good … Hbl_pcpop … EQcall) #data1 * #Hinit1
1133	normalize nodelta *** #pre_c #instr_c #post_c * #Hregs1 * #pc1 * destruct(EQt_pc_pop)
1134	whd in match sigma_stored_pc in ⊢ (% → ?); normalize nodelta
1135	inversion(sigma_pc_opt ???????? t_pc_pop)
1136	[ #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero [#EQ destruct(EQ)]
1137	whd in match sigma_stored_pc; normalize nodelta >ABS %]
1138	#pc2 #EQpc2 normalize nodelta inversion(sigma_pc_opt ?????????)
1139	[ #_ normalize nodelta #EQ destruct(EQ) cases(fetch_statement_inv … EQcall)
1140	>fetch_internal_function_no_zero [2: whd in match sigma_stored_pc; normalize nodelta >EQpc2 %]
1141	#EQ destruct(EQ) ]
1142	#pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQpc2 in EQpc3; #H lapply(sym_eq ??? H) -H #H
1143	lapply(sigma_stored_pc_inj … H) [ >EQpc2 % #EQ destruct] #EQ destruct(EQ) * #t_fn1 * #nxt1
1144	* #pre * #post @eq_identifier_elim
1145	[ #EQentry cases(entry_is_cost … (pi2 ?? fn1)) #nxt1 * #c <EQentry #ABS
1146	cases(fetch_statement_inv … EQcall) #_ normalize nodelta >ABS #EQ destruct(EQ) ]
1147	#_ cut(∀x : bool.andb x false = false) [* %] #EQ >EQ -EQ normalize nodelta ***
1148	cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1)
1149	(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1)
1150	((call_is_call … good … (proj1 … (fetch_statement_inv … EQcall))) id args dest ?)) (point_of_pc p_in pc1))
1151	#id' * #args' * #dest' #EQ >EQ -EQ #EQt_call #EQpre_c #EQpost_c #EQnxt1 #H
1152	cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1)
1153	(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1) H))
1154	-H #st2' * #EQst2' #fin_sem_rel
1155	%{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))}
1156	%{(next p_out nxt1
1157	(set_last_pop p_out (decrement_stack_usage ? ssize t_st_pop) pc1))}
1158	%{(mk_state_pc ? st2' (pc_of_point p_out (pc_block pc1) next_of_call) pc1)}
1159	%{((taaf_to_taa …
1160	(produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))}
1161	[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); whd in match (as_label ??);
1162	whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
1163	>point_of_pc_of_point >EQt_stmt >m_return_bind normalize nodelta * #H @H % ]
1164	letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog)
1165	lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size) ??????????)
1166	[11: * #taaf * #_ #prf %{taaf}
1167	\|3: change with (pc_block pc1) in match (pc_block ?);
1168	@(proj1 … (fetch_statement_inv … EQt_call))
1169	\|2: whd in match next; whd in match succ_pc; whd in match set_pc;
1170	whd in match point_of_pc; normalize nodelta whd in match pc_of_point;
1171	normalize nodelta >point_of_offset_of_point in ⊢ (????%???);
1172	whd in match (point_of_succ ???); @EQpost_c
1173	\|1: assumption
1174	\|*:
1175	]
1176	cut(? : Prop)
1177	[3: #Hfin %
1178	[ %
1179	[ %
1180	[2: @Hfin
1181	\| %
1182	[ %
1183	[ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *]
1184	#hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) *
1185	#succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ)
1186	#EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??);
1187	whd in match (as_pc_of ??); whd in match (point_of_succ ???);
1188	change with (pc_block pc1) in match (pc_block ?);
1189	whd in match fetch_statement; normalize nodelta
1190	>(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind
1191	whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
1192	>EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt;
1193	normalize nodelta * #H @H % ]
1194	]
1195	whd [ whd in match (as_classify ??); \| whd in match eval_state; normalize nodelta]
1196	whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
1197	>point_of_pc_of_point >EQt_stmt [%] >m_return_bind whd in match eval_statement_no_pc;
1198	normalize nodelta >m_return_bind whd in match eval_statement_advance;
1199	whd in match eval_return; normalize nodelta whd in match (stack_sizes ????);
1200	>EQssize >m_return_bind >EQt_pop >m_return_bind whd in match next_of_call_pc;
1201	normalize nodelta >EQt_call >m_return_bind %
1202	]
1203	]
1204	]
1205	\|
1206	\| whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct]
1207	whd in match (point_of_succ ???); @(st_rel_def … good)
1208	[3: change with (pc_block pc1) in match (pc_block ?);
1209	lapply(proj1 ?? (fetch_statement_inv … EQcall)) <pc_block_eq in ⊢ (% → ?);
1210	[2: >EQpc2 % #EQ destruct] #H @H
1211	\|1,2:
1212	\| <pc_block_eq in fin_sem_rel; [2: >EQpc2 % #EQ destruct] #H @H
1213	\| %
1214	]
1215	]
1216	[ whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i
1217	#calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call
1218	whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQpc1_pc_s1_pre #EQsucc_pc
1219	whd in ⊢ (% → ?); #EQpc_s1_pre >EQpc_s1_pre in EQfetch_call; #EQfetch_call
1220	cases(fetch_statement_sigma_stored_pc … good … EQfetch_call)
1221	[2: <EQpc_s1_pre % #ABS elim Hbl_pcpop #H @H -H >EQpc1_pc_s1_pre assumption ]
1222	#data2 * #EQdata2 normalize nodelta * #bl2 * #EQbl2 * #pc3 * #EQstored
1223	lapply(stored_pc_inj … (sym_eq ??? EQstored))
1224	[2: % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero
1225	[ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS %
1226	\| % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero
1227	[2: <pc_block_eq [assumption] % #ABS1 cases(fetch_statement_inv … EQfetch_call)
1228	whd in match sigma_stored_pc; normalize nodelta >ABS1
1229	>fetch_internal_function_no_zero [2: %] ] whd in ⊢ (??%% → ?); #EQ destruct
1230	]
1231	#EQ destruct(EQ) * #fn' * #nxt'' * #l1 * #l2 @eq_identifier_elim
1232	[ #EQentry cases(fetch_statement_inv … EQfetch_call) #_ >EQentry normalize nodelta
1233	cases(entry_is_cost … (pi2 ?? calling)) #nxt1 * #c #EQ >EQ #EQ1 destruct]
1234	#_ cut(∀b : bool.andb b false = false) [ * //] #EQ >EQ -EQ normalize nodelta
1235	*** #EQt_fetch_call #_ #_ #EQnxt' whd >EQt_fetch_call normalize nodelta
1236	cut(? : Prop)
1237	[3: whd in match (last_pop ??); #H %{H}
1238	\|2: @(stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs … )
1239	[ % #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero
1240	[#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS %
1241	\|3: >EQpc1_pc_s1_pre assumption
1242	\| % #ABS cases(fetch_statement_inv … EQt_call) >fetch_internal_function_no_zero
1243	[2: assumption] #EQ destruct
1244	]
1245	\|]
1246	destruct(H)
1247	cut(nxt'' = nxt1) [2: #EQ destruct whd in ⊢ (??%%); % ]
1248	cut(nxt' = next_of_call)
1249	[ lapply EQsucc_pc whd in match (succ_pc); normalize nodelta
1250	whd in match (point_of_succ ???); whd in match (point_of_succ ???);
1251	whd in ⊢ (??%% → ?); cases next_of_call #x cases nxt' #y
1252	whd in match (offset_of_point ??); whd in match (offset_of_point ??);
1253	#EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) % ]
1254	#EQ destruct(EQ) >EQcall in EQfetch_call; >EQt_call in EQt_fetch_call;
1255	whd in ⊢ (? → ??%? → ?); #EQ1 #EQ2 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) %
1256	]
1257	cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % \|3: % % \|2:]
1258	#stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc1)) (neg one))
1259	[ #Hbl @(as_label_premain_ok ?????????? good)
1260	[ change with (pc_block (sigma_stored_pc ?????????)) in match (pc_block ?);
1261	<pc_block_eq [ assumption] % #ABS cases(fetch_statement_inv … EQstmt')
1262	>fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc;
1263	normalize nodelta >ABS %
1264	\| assumption
1265	]
1266	\| #Hbl_pc_pop @(as_label_ok_non_entry … good)
1267	[4: @EQstmt'
1268	\|1,2,3:
1269	\| assumption
1270	\| assumption
1271	\| cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall)))
1272	* whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point
1273	#H1 @H <H1 %
1274	]
1275	]
1276	qed.
1277
1278	lemma eval_call_ok : ∀ P_in , P_out: sem_graph_params.
1279	∀prog : joint_program P_in.
1280	∀stack_size.
1281	∀ f_lbls,f_regs.∀init_regs.∀init.
1282	∀st_no_pc_rel,st_rel.
1283	let prog_pars_in ≝ mk_prog_params P_in prog stack_size in
1284	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
1285	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in
1286	∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs
1287	st_no_pc_rel st_rel.
1288	∀st1,st1' : joint_abstract_status prog_pars_in.
1289	∀st2 : joint_abstract_status prog_pars_out.
1290	∀f.
1291	∀fn : joint_closed_internal_function P_in ?.
1292	∀id,arg,dest,nxt.
1293	block_id … (pc_block (pc … st1)) ≠ -1 →
1294	st_rel st1 st2 →
1295	fetch_statement P_in …
1296	(joint_globalenv P_in prog stack_size) (pc … st1) =
1297	return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 →
1298	eval_state P_in … (ev_genv … prog_pars_in)
1299	st1 = return st1' →
1300	∃is_call,st2_pre_call,t_is_call.
1301	as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» =
1302	as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧
1303	(pc … st1) = sigma_stored_pc P_in P_out prog stack_size
1304	init init_regs f_lbls f_regs (pc … st2_pre_call) ∧
1305	∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
1306	∃taa2 : trace_any_any … st2 st2_pre_call.
1307	∃taa2' : trace_any_any … st2_after_call st2'.
1308	eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call =
1309	return st2_after_call ∧
1310	st_rel st1' st2' ∧
1311	as_label (joint_abstract_status prog_pars_in) st1' =
1312	as_label (joint_abstract_status prog_pars_out) st2_after_call.
1313	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
1314	#good #st1 #st1' #st2 #f #fn #id #arg #dest #nxt #Hbl #Rst1st2 #EQfetch
1315	whd in match eval_state in ⊢ (% → ?); normalize nodelta >EQfetch >m_return_bind
1316	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
1317	#H @('bind_inversion H) -H #bl >set_no_pc_eta #H lapply(err_eq_from_io ????? H) -H
1318	#EQbl #H @('bind_inversion H) -H * #f1 *
1319	#fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
1320	[2: #H @('bind_inversion H) -H #x whd in match eval_external_call; normalize nodelta
1321	#H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z #_
1322	#H @('bind_inversion H) -H #w whd in ⊢ (??%% → ?); #ABS destruct(ABS) ]
1323	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1_save #EQst1_save
1324	#H @('bind_inversion H) -H #st1_no_pc' whd in match eval_internal_call;
1325	normalize nodelta change with (stack_size ?) in match (stack_sizes ????); #H
1326	@('bind_inversion H) -H #ssize #H lapply(opt_eq_from_res ???? H) -H #EQssize
1327	#H @('bind_inversion H) -H #st1_no_pc'' #EQst1_no_pc'' whd in ⊢ (??%% → ?);
1328	#EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1329	% [@hide_prf whd in ⊢ (??%?); >EQfetch %]
1330	cases(fetch_statement_sigma_stored_pc … good … Hbl EQfetch)
1331	#data * #EQdata normalize nodelta *** #pre #instr #post * #Hregs * #pc' * #EQpc'
1332	* #t_fn * #nxt' * #l1 * #l2 @eq_identifier_elim
1333	[ #EQentry cases(fetch_statement_inv … EQfetch) #_ >EQentry normalize nodelta
1334	cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #ABS destruct(ABS) ]
1335	#_ cut(∀b.andb b false = false) [* %] #EQ ** >EQ -EQ normalize nodelta *
1336	#EQt_call #EQpre #EQpost #_
1337	lapply(b_graph_transform_program_fetch_internal_function … good … bl f1 fn1)
1338	@eqZb_elim [ normalize nodelta #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) >ABS #H @H %]
1339	#_ normalize nodelta #H cut(? : Prop)
1340	[3: #EQint_fn cases(H EQint_fn) -H
1341	\|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %\|*:]
1342	#data1 * #t_fn1 ** #EQt_fn1 #Hdata1 #good1
1343	cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs)
1344	(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
1345	(call_is_call … good … )) … (point_of_pc p_out pc'))
1346	[4: @(proj1 … (fetch_statement_inv … EQfetch)) \|*:]
1347	#id' * #args' * #dest' #EQinstr
1348	cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs)
1349	(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
1350	(call_commutation … good … Hbl EQfetch bl EQbl … EQint_fn … EQst1_save … EQssize …
1351	EQst1_no_pc'' … Rst1st2 … EQt_fn1)) … EQpc' EQt_call EQinstr)
1352	#st2_pre ** #EQst2_pre #EQt_bl * #st2_save * #EQst2_save * #st2_after * #EQst2_after
1353	#Hprologue
1354	%{(mk_state_pc ? st2_pre pc' (last_pop … st2))}
1355	%
1356	[ @hide_prf whd in ⊢ (??%?); >EQt_call >EQinstr %]
1357	%
1358	[ % [2: @sym_eq assumption] whd in ⊢ (??%%);
1359	>EQfetch in ⊢ (??(match % with [ _ ⇒ ? \| _ ⇒ ? ])?);
1360	>EQt_call in ⊢ (???(match % with [ _ ⇒ ? \| _ ⇒ ? ])); normalize nodelta >EQbl
1361	>m_return_bind >EQint_fn normalize nodelta >EQinstr normalize nodelta
1362	>EQt_bl >m_return_bind >EQt_fn1 % ]
1363	%{(mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
1364	(pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
1365	cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue) -Hprologue #st2' * #EQst2'
1366	#fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
1367	#nxt1 * #c #EQcost #H lapply(H … EQcost) -H -good1 normalize nodelta
1368	>(f_step_on_cost … data1) *** #pre1 #instr1 #post1 @eq_identifier_elim [2: * #H @⊥ @H %]
1369	#_ cases(added_prologue … data1) in EQst2'; normalize nodelta
1370	[ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1371	\| #hd #tl #EQst2'
1372	]
1373	* whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [2,4: #x #y #_ #_ *]
1374	#EQf_regs #EQ [2: whd in EQ : (???%);] destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 ***
1375	#EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
1376	#nxt2 * [ #EQnop \| #EQt_cost ] change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ)
1377	whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
1378	[ * #star_lab * #Hstar_lab * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1' whd in ⊢ (% → ?);
1379	* #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt2 * #EQt_cost
1380	change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl2
1381	\| #EQentry
1382	]
1383	whd in EQmid1 : (??%%); destruct(EQmid1)
1384	%{(mk_state_pc ? ? (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))}
1385	[ @st2' \|3: @(increment_stack_usage p_out ssize st2_after)]
1386	>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre
1387	lapply(taaf_to_taa … (produce_trace_any_any_free … st2 f t_fn … EQpre … EQst2_pre) ?)
1388	[3,6: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
1389	[2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
1390	#ABS cases(fetch_statement_inv … EQfetch) <EQpc'
1391	>fetch_internal_function_no_zero [1,3: #EQ destruct]
1392	whd in match sigma_stored_pc; normalize nodelta >ABS %]
1393	>(pc_of_point_of_pc … pc') #taa1 %{taa1}
1394	\|1,4: @if_elim #_ [2,4: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
1395	<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
1396	[2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
1397	#ABS cases(fetch_statement_inv … EQfetch) <EQpc'
1398	>fetch_internal_function_no_zero [1,3: #EQ destruct]
1399	whd in match sigma_stored_pc; normalize nodelta >ABS %]
1400	>(pc_of_point_of_pc … pc') whd in match (as_pc_of ??); >EQt_call
1401	>EQinstr %
1402	\|2,5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
1403	[2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
1404	#ABS cases(fetch_statement_inv … EQfetch) <EQpc'
1405	>fetch_internal_function_no_zero [1,3: #EQ destruct]
1406	whd in match sigma_stored_pc; normalize nodelta >ABS %]
1407	@(proj1 … (fetch_statement_inv … EQt_call))
1408	]
1409	-taa1
1410	[ letin trans_prog ≝ (b_graph_transform_program ????)
1411	lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size)
1412	(mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
1413	(pc_of_point p_out bl mid2) (last_pop … st2)) … EQst2')
1414	[ >point_of_pc_of_point in ⊢ (????%???); @EQl2
1415	\| change with bl in match (pc_block ?); assumption
1416	\|*:
1417	]
1418	#taaf %{(taaf_to_taa … (taa_append_taaf … (taa_step … (taa_base …) …) taaf) ?)}
1419	[1,2: [ @if_elim #_ [2: @I] ] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
1420	whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
1421	>EQt_fn1 >m_return_bind whd in match point_of_pc; normalize nodelta
1422	>point_of_offset_of_point [ >EQnop %] cases EQl2 #mid * #rest **
1423	#EQ destruct(EQ) * #nxt2 * #EQmid2 change with nxt2 in ⊢ (??%? → ?);
1424	#EQ destruct(EQ) #_ >EQmid2 %
1425	\|3,4: whd [ whd in ⊢ (??%?); \| whd in match eval_state; ]
1426	whd in match fetch_statement; normalize nodelta
1427	>EQt_fn1 >m_return_bind >point_of_pc_of_point >EQt_cost [%] >m_return_bind
1428	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind %
1429	]
1430	\| >EQentry %{(taa_base …)}
1431	]
1432	%
1433	[2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??); whd in match (as_pc_of ??);
1434	whd in match fetch_statement; normalize nodelta >EQint_fn >EQt_fn1
1435	>m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta
1436	>point_of_offset_of_point >point_of_offset_of_point >EQcost >m_return_bind
1437	normalize nodelta >EQt_cost >m_return_bind [2: %] normalize nodelta
1438	whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%);
1439	whd in match (get_first_costlabel_next ???);
1440	generalize in match (refl ??);
1441	>EQcost in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ? \| _ ⇒ ?]?))));
1442	#EQcost' normalize nodelta %
1443	]
1444	%
1445	[1,3: whd in match eval_state; normalize nodelta >EQt_call >m_return_bind
1446	whd in match eval_statement_no_pc; normalize nodelta >EQinstr normalize nodelta
1447	>m_return_bind whd in match eval_statement_advance; whd in match eval_call;
1448	normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1)
1449	* #f2 * #fn2 #EQ normalize nodelta whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
1450	>EQ -EQ >m_return_bind normalize nodelta >EQst2_save >m_return_bind
1451	whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????);
1452	>EQssize >m_return_bind >EQst2_after >m_return_bind [%] >EQentry %
1453	\|*: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn \|1,2,5,6:]
1454	@(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption
1455	]
1456	qed.
1457
1458	lemma eval_call_premain_ok : ∀ P_in , P_out: sem_graph_params.
1459	∀prog : joint_program P_in.
1460	∀stack_size.
1461	∀ f_lbls,f_regs.∀init_regs.∀init.
1462	∀st_no_pc_rel,st_rel.
1463	let prog_pars_in ≝ mk_prog_params P_in prog stack_size in
1464	let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
1465	let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in
1466	∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs
1467	st_no_pc_rel st_rel.
1468	∀st1,st1' : joint_abstract_status prog_pars_in.
1469	∀st2 : joint_abstract_status prog_pars_out.
1470	∀f.
1471	∀fn : joint_closed_internal_function P_in ?.
1472	∀id,arg,dest,nxt.
1473	block_id … (pc_block (pc … st1)) = -1 →
1474	st_rel st1 st2 →
1475	fetch_statement P_in …
1476	(joint_globalenv P_in prog stack_size) (pc … st1) =
1477	return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 →
1478	eval_state P_in … (ev_genv … prog_pars_in)
1479	st1 = return st1' →
1480	∃is_call,st2_pre_call,t_is_call.
1481	as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» =
1482	as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧
1483	(pc … st1) = sigma_stored_pc P_in P_out prog stack_size
1484	init init_regs f_lbls f_regs (pc … st2_pre_call) ∧
1485	∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
1486	∃taa2 : trace_any_any … st2 st2_pre_call.
1487	∃taa2' : trace_any_any … st2_after_call st2'.
1488	eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call =
1489	return st2_after_call ∧
1490	st_rel st1' st2' ∧
1491	as_label (joint_abstract_status prog_pars_in) st1' =
1492	as_label (joint_abstract_status prog_pars_out) st2_after_call.
1493	#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
1494	#good #st1 #st1' #st2 #f #fn #id #arg #dest #nxt #EQbl #Rst1st2 #EQfetch #EQeval
1495	% [ whd in ⊢ (??%?); >EQfetch %] %{st2} cases(pre_main_ok … good … EQbl EQeval Rst1st2)
1496	#Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab %
1497	[ change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in ⊢ (??%?); >EQfetch %]
1498	% [ % [2: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
1499	<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQbl % ]
1500	\| %{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [%{EQst2' Rst1st2'}]
1501	assumption
1502	]
1503	whd in ⊢ (??%%); >EQfetch in ⊢ (??(match % with [_ ⇒ ? \| _ ⇒ ?])?); normalize nodelta
1504	lapply Hclass whd in ⊢ (??%% → ?); >EQfetch in ⊢ (% → ?); whd in match joint_classify_step;
1505	normalize nodelta inversion(fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct]
1506	** #f' #fn' *
1507	[ * [ #c \| #id' #arg' #dest' \| #r #lbl \| #seq ] #nxt \| * [ #lb \|\| #h #id' #arg'] \| *]
1508	#EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct normalize nodelta @('bind_inversion EQeval)
1509	#x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc;
1510	normalize nodelta >m_return_bind whd in match eval_statement_advance;
1511	whd in match eval_call; normalize nodelta #H @('bind_inversion H) -H #bl #H
1512	lapply(err_eq_from_io ????? H) -H #EQbl #H @('bind_inversion H) -H * #f1
1513	* #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
1514	[2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
1515	#H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
1516	#H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ]
1517	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1_save
1518	#_ #H @('bind_inversion H) -H #st1_fin #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1519	>EQbl >m_return_bind whd in match fetch_internal_function; normalize nodelta
1520	>EQfn1 >m_return_bind normalize nodelta @('bind_inversion EQst2') #x
1521	>EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc;
1522	normalize nodelta >m_return_bind whd in match eval_statement_advance;
1523	whd in match eval_call; normalize nodelta #H @('bind_inversion H) -H
1524	#bl' >set_no_pc_eta #H lapply(err_eq_from_io ????? H) -H #EQbl'
1525	#H @('bind_inversion H) -H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H) -H
1526	#EQfn1' normalize nodelta
1527	[2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
1528	#H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
1529	#H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ]
1530	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
1531	#st2_save #_ #H @('bind_inversion H) -H #st2_fin #_ whd in ⊢ (??%% → ?);
1532	#EQ destruct(EQ) >EQbl' >m_return_bind >EQfn1' >m_return_bind normalize nodelta
1533	lapply(fetch_ok_pc_ok … good … Rst1st2' ?)
1534	[ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); %
1535	\|*:
1536	]
1537	whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ)
1538	lapply EQfn1 whd in match fetch_function; normalize nodelta
1539	@eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) #H @H assumption]
1540	#Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H)
1541	#f2 #EQf2 #H @('bind_inversion H) -H #fn2 #_ whd in ⊢ (??%? → ?); -e0 -EQ
1542	#EQ destruct(EQ) -H lapply EQfn1' whd in match fetch_function; normalize nodelta
1543	@eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta
1544	#H lapply(opt_eq_from_res ???? H) -H
1545	whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta
1546	whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta
1547	whd in match transform_joint_program; normalize nodelta
1548	>(symbol_for_block_transf ??? (λx.x) prog
1549	(λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?);
1550	>EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) -H #fn2' #_
1551	whd in ⊢ (??%% → ?); #EQ destruct(EQ) %
1552	qed.
1553
1554
1555	lemma pair_dep_match_elim : ∀A,B,C : Type[0].∀P : C → Prop.∀t:A×B.
1556	∀c.
1557	(∀x,y,prf.P (c x y prf)) →
1558	P (let 〈x,y〉 as prf ≝ t in c x y prf).
1559	#A #B #C #P * // qed.
1560
1561	theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
1562	∀prog : joint_program p_in.∀stack_size : ident → option ℕ.
1563	∀init : (∀globals.joint_closed_internal_function p_in globals →
1564	bound_b_graph_translate_data p_in p_out globals).
1565	∀init_regs : block → list register.∀f_lbls : lbl_funct_type.
1566	∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out.
1567	∀st_rel : joint_state_pc_relation p_in p_out.
1568	good_state_relation p_in p_out prog stack_size init init_regs
1569	f_lbls f_regs st_no_pc_rel st_rel →
1570	good_init_relation p_in p_out prog stack_size init st_no_pc_rel →
1571	let trans_prog ≝ b_graph_transform_program … init prog in
1572	∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
1573	∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
1574	∃[1] R.
1575	status_simulation_with_init
1576	(joint_abstract_status (mk_prog_params p_in prog stack_size))
1577	(joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
1578	R init_in init_out.
1579	#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #st_no_pc_rel
1580	#st_rel #good #good_init #init_in whd in match make_initial_state; normalize nodelta
1581	#H @('bind_inversion H) -H #init_m #EQinit_m @pair_dep_match_elim #m #bl #prf
1582	whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1583	letin trans_prog ≝ (b_graph_transform_program ????)
1584	letin globals_size ≝ (globals_stacksize … trans_prog)
1585	letin spp ≝
1586	(«mk_pointer bl (mk_offset (bitvector_of_Z 16 (-S (globals_size)))),
1587	pi2 … bl»)
1588	letin st ≝ (mk_state p_out
1589	(* frames ≝ *)(Some ? (empty_framesT …))
1590	(* internal_stack ≝ *) empty_is
1591	(* carry ≝ *)(BBbit false)
1592	(* regs ≝ *)(empty_regsT … spp)
1593	(* mem ≝ *)m
1594	(* stack_usage ≝ *)0)
1595	%{(mk_state_pc ? (set_sp … spp st) init_pc (null_pc one))} >init_mem_transf
1596	>EQinit_m >m_return_bind @pair_dep_match_elim #m1 #bl1 #prf' lapply prf
1597	lapply prf' lapply prf' <prf in ⊢ (%→?); #EQ destruct(EQ) -prf' #prf' #_
1598	%{(refl …)} %{(JointStatusSimulation … good)} %
1599	[ whd @(st_rel_def … good)
1600	[3: % \|1,2:
1601	\| lapply(good_empty ?????? good_init ? EQinit_m) <prf' normalize nodelta #H @H
1602	\| %
1603	]
1604	\| whd whd in ⊢ (??%%); lapply(good_init_cost_label … good_init) normalize nodelta
1605	cases(fetch_statement ????) normalize nodelta
1606	[2: #e * [ #e' #EQ >EQ % \| #x * #EQ #EQ1 >EQ normalize nodelta >EQ1 % ] ]
1607	#x cases(cost_label_of_stmt ???) normalize nodelta
1608	[ * [ * #e' #EQ >EQ % \| * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 %]
1609	\| #c * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 %
1610	]
1611	]
1612	%
1613	[ #st1 #st1' #st2 whd in ⊢ (% → ?); #EQeval @('bind_inversion EQeval)
1614	** #f #fn #stmt #H lapply(err_eq_from_io ????? H) -H cases stmt -stmt
1615	[ * [ #c \| #id #arg #dest \| #r #lb \| #seq ] #nxt \| #fin \| * ] #EQfetch #_
1616	whd in ⊢ (% → ?); #Rst1st2
1617	change with (joint_classify ???) in
1618	⊢ (match % with [ _ ⇒ ? \| _ ⇒ ? \| _ ⇒ ? \| _ ⇒ ? \| _ ⇒ ? ]);
1619	[ whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
1620	cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
1621	[ cases(general_eval_cost_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1622	\| cases(general_eval_cost_ok … good … Hbl Rst1st2 EQfetch EQeval)
1623	] #st2' * #Rst1st2' * #taaf * #H #H1 %{st2'} %{taaf} >H % [1,3: %{I} assumption]
1624	assumption
1625	\| whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta #prf
1626	cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
1627	[ cases(eval_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1628	\| cases(eval_call_ok … good … Hbl Rst1st2 EQfetch EQeval)
1629	]
1630	#prf' * #st2_pre * #prf'' ** #EQ #EQ1 * #st2_after * #st2' * #taa * #taa1 ** #EQ2 #H #EQ3
1631	%{st2_pre} [1,3: assumption] % [1,3: % [1,3: >EQ % \|*: assumption ] ]
1632	%{st2_after} %{st2'} %{taa} %{taa1} % [1,3: %{EQ2 H}] assumption
1633	\| whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
1634	#ncost cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
1635	[ cases(eval_cond_premain_ok … good … Hbl Rst1st2 EQfetch EQeval ncost)
1636	\| cases(eval_cond_ok … good … Hbl Rst1st2 EQfetch EQeval ncost)
1637	]
1638	#st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I} assumption]
1639	assumption
1640	\| whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
1641	cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
1642	[ cases(general_eval_seq_no_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1643	\| cases(general_eval_seq_no_call_ok … good … Hbl Rst1st2 EQfetch EQeval)
1644	]
1645	#st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} % [ >H1 %{I H} \|3: %{H1 H} ]
1646	assumption
1647	]
1648	\| @(as_result_ok … good)
1649	]
1650	cases fin in EQfetch; -fin
1651	[ #lb #EQfetch whd in match joint_classify; normalize nodelta >EQfetch
1652	normalize nodelta
1653	cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
1654	#Hbl
1655	[ cases(eval_goto_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1656	\| cases(eval_goto_ok … good … Hbl Rst1st2 EQfetch EQeval)
1657	]
1658	#st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I H}] assumption
1659	\| #EQfetch whd in match joint_classify; normalize nodelta >EQfetch
1660	normalize nodelta
1661	cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
1662	#Hbl
1663	[ @⊥ @(pre_main_no_return … good … Hbl … EQfetch) ]
1664	cases(eval_return_ok … good … Hbl Rst1st2 EQfetch EQeval) #st2_pre * #st2_after
1665	* #st2' * #taa * #taaf ***** #H #H1 #H2 #H3 #H4 #H5 %{st2_pre} %{st2_after}
1666	%{st2'} %{taa} %{taaf} % [2: assumption] % [2: assumption] % [2: assumption]
1667	% [2: assumption] %{H H1}
1668	\| #has #id #arg #EQfetch whd in match joint_classify; normalize nodelta
1669	>EQfetch normalize nodelta
1670	cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
1671	#Hbl
1672	[ cases(eval_tailcall_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1673	\| cases(eval_tailcall_ok … good … Hbl Rst1st2 EQfetch EQeval)
1674	]
1675	#prf * #st2_pre * #t_is_call * #H * #st2_after * #st2' * #taa1 * #taa2
1676	** #H1 #H2 #H3 #prf' %{st2_pre} [1,3: assumption] %{H} %{st2_after} %{st2'}
1677	%{taa1} %{taa2} % [2,4: assumption] %{H1 H2}
1678	]
1679	qed.
1680

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

Download in other formats:

Original Format