Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

ERTLtoERTLptrUtils.ma @ 3393

Last change on this file since 3393 was 3018, checked in by sacerdot, 8 years ago

1) some files repaired
2) all stuff related to the aborted pass ERTLptr (now merged with

ERTLToLTL) moved into the ERTLptr directory (no longer used/linked)

File size: 77.1 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 "ERTL/ERTLToERTLptr.ma".
16	include "common/StatusSimulation.ma".
17	include "joint/Traces.ma".
18	include "ERTLptr/ERTLptr_semantics.ma".
19	include "common/ExtraMonads.ma".
20
21
22	definition ERTL_status ≝
23	λprog : ertl_program.λstack_sizes.
24	joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).
25
26	definition ERTLptr_status ≝
27	λprog : ertlptr_program.λstack_sizes.
28	joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
29
30	definition sigma_map ≝ block → label → option label.
31	definition lbl_funct ≝ block → label → (list label).
32	definition regs_funct ≝ block → label → (list register).
33
34	(TO BE MOVED)
35	lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
36	∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
37	(∀ prf : r = Code.P (g prf)) →
38	P ((match r return λx.(r = x → ?) with
39	[XData ⇒ f \| Code ⇒ g])(refl ? r)).
40	#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 \| @H2]
41	qed.
42
43	definition get_sigma :
44	ertl_program → lbl_funct → sigma_map ≝
45	λprog,f_lbls.λbl,searched.
46	let globals ≝ prog_var_names … prog in
47	let ge ≝ globalenv_noinit … prog in
48	! bl ← code_block_of_block bl ;
49	! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
50	!〈res,s〉 ← find ?? (joint_if_code … fn)
51	(λlbl.λ_. match split_on_last … (f_lbls bl lbl) with
52	[None ⇒ eq_identifier … searched lbl
53	\|Some x ⇒ eq_identifier … searched (\snd x)
54	]);
55	return res.
56
57	definition sigma_pc_opt :
58	ertl_program → lbl_funct →
59	program_counter → option program_counter ≝
60	λprog,f_lbls,pc.
61	let sigma ≝ get_sigma prog f_lbls in
62	let ertl_ptr_point ≝ point_of_pc ERTLptr_semantics pc in
63	if eqZb (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
64	return pc
65	else
66	! ertl_point ← sigma (pc_block pc) ertl_ptr_point;
67	return pc_of_point
68	ERTL_semantics (pc_block pc) ertl_point.
69
70	definition sigma_stored_pc ≝
71	λprog,f_lbls,pc. match sigma_pc_opt prog f_lbls pc with
72	[None ⇒ null_pc (pc_offset … pc) \| Some x ⇒ x].
73
74
75	definition sigma_beval : ertl_program → lbl_funct →
76	beval → beval ≝
77	λprog,f_lbls,bv.
78	match bv with
79	[ BVpc pc prt ⇒ match sigma_pc_opt prog f_lbls pc with
80	[None ⇒ BVundef \| Some x ⇒ BVpc x prt]
81	\| _ ⇒ bv
82	].
83
84	definition sigma_is : ertl_program → lbl_funct →
85	internal_stack → internal_stack ≝
86	λprog,f_lbls,is.
87	match is with
88	[ empty_is ⇒ empty_is
89	\| one_is bv ⇒ one_is (sigma_beval prog f_lbls bv)
90	\| both_is bv1 bv2 ⇒
91	both_is (sigma_beval prog f_lbls bv1) (sigma_beval prog f_lbls bv2)
92	].
93
94	lemma sigma_is_empty : ∀prog,sigma.
95	sigma_is prog sigma empty_is = empty_is.
96	#prog #sigma % qed.
97
98	definition sigma_mem : ertl_program → lbl_funct →
99	bemem → bemem ≝
100	λprog,f_lbls,m.
101	mk_mem
102	(λb.
103	If Zltb (block_id b) (nextblock m) then with prf' do
104	let l ≝ low_bound m b in
105	let h ≝ high_bound m b in
106	mk_block_contents l h
107	(λz.If Zleb l z ∧ Zltb z h then with prf'' do
108	sigma_beval prog f_lbls (contents (blocks m b) z)
109	else BVundef)
110	else empty_block OZ OZ)
111	(nextblock m)
112	(nextblock_pos m).
113
114	include "common/ExtraIdentifiers.ma".
115
116
117	definition sigma_register_env :
118	ertl_program → lbl_funct →
119	list register →
120	register_env beval → register_env beval ≝
121	λprog,f_lbls,ids,psd_env.
122	let m' ≝ map ??? psd_env (λbv.sigma_beval prog f_lbls bv) in
123	m' ∖ ids.
124
125
126	definition sigma_frames_opt : ertl_program →
127	lbl_funct → regs_funct →
128	list (register_env beval × (Σb:block.block_region b=Code)) →
129	option (list (register_env beval × (Σb:block.block_region b=Code))) ≝
130	λprog,f_lbls,f_regs,frms.
131	let globals ≝ prog_var_names … prog in
132	let ge ≝ globalenv_noinit … prog in
133	m_list_map ? ? ?
134	(λx.let 〈reg_env,bl〉 ≝ x in
135	! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
136	return 〈sigma_register_env prog f_lbls
137	(added_registers ERTL globals fn (f_regs bl)) reg_env,bl〉) frms.
138
139	definition sigma_frames : ertl_program →
140	lbl_funct → regs_funct →
141	option (list (register_env beval × (Σb:block.block_region b=Code))) →
142	option (list (register_env beval × (Σb:block.block_region b=Code))) ≝
143	λprog,f_lbls,f_regs,frms.
144	! frames ← frms;
145	sigma_frames_opt prog f_lbls f_regs frames.
146
147	include "common/BitVectorTrieMap.ma".
148
149	definition sigma_hw_register_env :ertl_program →
150	lbl_funct → hw_register_env → hw_register_env ≝
151	λprog,f_lbls,h_reg.mk_hw_register_env
152	(map ? ? (sigma_beval prog f_lbls) 6 (reg_env … h_reg)) (other_bit … h_reg).
153
154	definition sigma_regs :ertl_program →
155	lbl_funct → list register →
156	(register_env beval)×hw_register_env→
157	(register_env beval)×hw_register_env ≝
158	λprog,f_lbls,ids,regs.let 〈x,y〉≝ regs in
159	〈sigma_register_env prog f_lbls ids x,
160	sigma_hw_register_env prog f_lbls y〉.
161
162	definition dummy_state : state ERTL_semantics ≝
163	mk_state ERTL_semantics
164	(None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 0 empty.
165
166	definition sigma_state : ertl_program →
167	lbl_funct → regs_funct → list register →
168	state ERTLptr_semantics → state ERTL_semantics ≝
169	λprog,f_lbls,f_regs,restr,st.
170	mk_state ERTL_semantics
171	(sigma_frames prog f_lbls f_regs (st_frms ERTLptr_semantics st))
172	(sigma_is prog f_lbls (istack … st))
173	(carry … st)
174	(sigma_regs prog f_lbls restr (regs … st))
175	(stack_usage … st)
176	(sigma_mem prog f_lbls (m … st)).
177
178	definition dummy_state_pc : state_pc ERTL_semantics ≝
179	mk_state_pc ? dummy_state (null_pc one) (null_pc one).
180
181	definition sigma_state_pc : ertl_program → lbl_funct → regs_funct →
182	state_pc ERTLptr_semantics → state_pc ERTL_semantics ≝
183	λprog,f_lbls,f_regs,st.
184	let ge ≝ globalenv_noinit … prog in
185	let globals ≝ prog_var_names … prog in
186	match fetch_internal_function … ge (pc_block (pc … st)) with
187	[ OK y ⇒ let 〈i,fn〉 ≝ y in
188	let added ≝ added_registers ERTL globals fn
189	(f_regs (pc_block (pc … st))) in
190	mk_state_pc ?
191	(sigma_state prog f_lbls f_regs added st)
192	(pc … st) (sigma_stored_pc prog f_lbls (last_pop … st))
193	\| Error e ⇒ dummy_state_pc
194	].
195
196
197	lemma ps_reg_retrieve_ok : ∀prog : ertl_program.
198	∀f_lbls : lbl_funct. ∀r,restr.
199	preserving1 ?? res_preserve1 …
200	(sigma_regs prog f_lbls restr)
201	(sigma_beval prog f_lbls)
202	(λregs.ps_reg_retrieve regs r)
203	(λregs.ps_reg_retrieve regs r).
204	#prog #f_lbls #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve;
205	whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1
206	whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta
207	>lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in
208	>(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1
209	#bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec %
210	qed.
211
212	lemma hw_reg_retrieve_ok : ∀prog : ertl_program.
213	∀f_lbls : lbl_funct. ∀r,restr.
214	preserving1 ?? res_preserve1 …
215	(sigma_regs prog f_lbls restr)
216	(sigma_beval prog f_lbls)
217	(λregs.hw_reg_retrieve regs r)
218	(λregs.hw_reg_retrieve regs r).
219	#prog #f_lbls #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve;
220	whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs;
221	whd in match sigma_hw_register_env; normalize nodelta
222	change with (sigma_beval prog f_lbls BVundef) in ⊢ (???????(??(?????%))?);
223	#bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct
224	%{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)}
225	% //
226	qed.
227
228
229	lemma ps_reg_store_ok : ∀prog : ertl_program.
230	∀f_lbls : lbl_funct. ∀r,restr.
231	¬(r ∈ (set_from_list RegisterTag restr)) →
232	preserving21 ?? res_preserve1 …
233	(sigma_beval prog f_lbls)
234	(sigma_regs prog f_lbls restr)
235	(sigma_regs prog f_lbls restr)
236	(ps_reg_store r)
237	(ps_reg_store r).
238	#prog #f_lbls #r #restr #Hreg whd in match ps_reg_store; normalize nodelta
239	#bv * #psd_r #hw_r @mfr_return_eq1
240	whd in match reg_store; whd in match sigma_regs; normalize nodelta
241	whd in match sigma_register_env; normalize nodelta >map_add
242	>add_set_minus [% \| assumption]
243	qed.
244	(*
245	lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
246	lapply x_spec -x_spec lapply EQpsd -EQpsd whd in match sigma_register_env;
247	normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %]
248	#id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) -H
249	#x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec
250	whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % //
251	\| #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta
252	whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % //
253	]
254	qed.*)
255
256
257	lemma hw_reg_store_ok : ∀prog : ertl_program.
258	∀f_lbls : lbl_funct. ∀r,restr.
259	preserving21 ?? res_preserve1 …
260	(sigma_beval prog f_lbls)
261	(sigma_regs prog f_lbls restr)
262	(sigma_regs prog f_lbls restr)
263	(hw_reg_store r)
264	(hw_reg_store r).
265	#prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta
266	#bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs;
267	normalize nodelta
268	whd in match sigma_hw_register_env; normalize nodelta <insert_map * #psd_r'
269	* #hw_r' #b' whd in ⊢ (???% → ?); #EQ destruct % [2: % [%] % \|]
270	qed.
271
272	definition move_dst_not_fresh : list register → move_dst → Prop ≝
273	λrestr,mv.match mv with
274	[PSD r ⇒ bool_to_Prop (¬(r ∈ (set_from_list RegisterTag restr)))
275	\| _ ⇒ True
276	].
277
278	lemma ertl_eval_move_ok : ∀prog : ertl_program.
279	∀f_lbls : lbl_funct. ∀ restr,pm.
280	move_dst_not_fresh restr (\fst pm) →
281	preserving1 ?? res_preserve1 …
282	(sigma_regs prog f_lbls restr)
283	(sigma_regs prog f_lbls restr)
284	(λregs.ertl_eval_move regs pm)
285	(λregs.ertl_eval_move regs pm).
286	#prog #sigma #restr * #mv_dst #arg_dst #Hpm #pm whd in match ertl_eval_move;
287	normalize nodelta @mfr_bind1 [@(sigma_beval prog sigma)
288	\| cases arg_dst normalize nodelta
289	[2: #b change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
290	@mfr_return1]
291	* #r normalize nodelta [@ps_reg_retrieve_ok\| @hw_reg_retrieve_ok]
292	\| #bv cases mv_dst in Hpm; #r #Hpm normalize nodelta [@ps_reg_store_ok assumption
293	\| @hw_reg_store_ok
294	]
295	]
296	qed.
297
298	lemma ps_arg_retrieve_ok : ∀prog : ertl_program.
299	∀f_lbls : lbl_funct. ∀a,restr.
300	preserving1 ?? res_preserve1 …
301	(sigma_regs prog f_lbls restr)
302	(sigma_beval prog f_lbls)
303	(λregs.ps_arg_retrieve regs a)
304	(λregs.ps_arg_retrieve regs a).
305	#prog #sigma #a #restr whd in match ps_arg_retrieve; normalize nodelta cases a -a
306	normalize nodelta [#r \| #b ] #regs
307	[ @ps_reg_retrieve_ok
308	\| change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
309	@mfr_return1
310	]
311	qed.
312
313	lemma pop_ok :
314	∀prog : ertl_program.∀f_lbls : lbl_funct.
315	∀f_regs : regs_funct.∀restr.
316	preserving1 ?? res_preserve1 ????
317	(sigma_state prog f_lbls f_regs restr)
318	(λx.let 〈bv,st〉 ≝ x in
319	〈sigma_beval prog f_lbls bv,
320	sigma_state prog f_lbls f_regs restr st〉)
321	(pop ERTL_semantics)
322	(pop ERTLptr_semantics).
323	#prog #f_lbls #f_regs #id whd in match pop; normalize nodelta #st @mfr_bind1
324	[@(λx.let 〈bv,is〉 ≝ x in
325	〈sigma_beval prog f_lbls bv,
326	sigma_is prog f_lbls is 〉)
327	\| whd in match is_pop; normalize nodelta whd in match sigma_state;
328	normalize nodelta cases(istack ? st) normalize nodelta
329	[@res_preserve_error1
330	\|2,3: #bv1 [2: #bv2] * #bv3 #is1 whd in ⊢ (??%% → ?); #EQ destruct
331	% [2,4: % [1,3: %\|: %] \|:]
332	]
333	\| * #bv #is normalize nodelta @mfr_return_eq1 %
334	]
335	qed.
336
337	lemma push_ok :
338	∀prog : ertl_program.
339	∀f_lbls : lbl_funct.
340	∀f_regs : regs_funct.∀restr.
341	preserving21 ?? res_preserve1 …
342	(sigma_state prog f_lbls f_regs restr)
343	(sigma_beval prog f_lbls)
344	(sigma_state prog f_lbls f_regs restr)
345	(push ERTL_semantics)
346	(push ERTLptr_semantics).
347	#prog #f_lbls #f_regs #restr whd in match push; normalize nodelta #st #bv @mfr_bind1
348	[ @(sigma_is prog f_lbls)
349	\| whd in match is_push; normalize nodelta whd in match sigma_state; normalize nodelta
350	cases (istack ? st) [2,3: #bv [2: #bv']] whd in match sigma_is in ⊢ (???????%?);
351	normalize nodelta [@res_preserve_error1] @mfr_return_eq1 %
352	\| #is @mfr_return_eq1 %
353	]
354	qed.
355
356	lemma be_opaccs_ok :
357	∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀ op.
358	preserving21 ?? res_preserve1 ??????
359	(sigma_beval prog f_lbls)
360	(sigma_beval prog f_lbls)
361	(λx.let 〈bv1,bv2〉 ≝ x in
362	〈sigma_beval prog f_lbls bv1,
363	sigma_beval prog f_lbls bv2〉)
364	(be_opaccs op)
365	(be_opaccs op).
366	#prog #sigma #op #bv #bv1
367	whd in match be_opaccs; normalize nodelta @mfr_bind1
368	[ @(λx.x)
369	\| cases bv
370	[ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
371	whd in match Byte_of_val; normalize nodelta
372	try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
373	whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
374	normalize nodelta [2: #pc] @res_preserve_error1
375	\| #by @mfr_bind1
376	[ @(λx.x)
377	\| cases bv1
378	[ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
379	whd in match Byte_of_val; normalize nodelta
380	try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
381	whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
382	normalize nodelta [2: #pc] @res_preserve_error1
383	\| #by1 * #bv2 #bv3 cases(opaccs eval op by by1) #by' #by1' normalize nodelta
384	whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % \|]
385	qed.
386
387	lemma be_op1_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct.
388	∀ op.
389	preserving1 ?? res_preserve1 …
390	(sigma_beval prog f_lbls)
391	(sigma_beval prog f_lbls)
392	(be_op1 op)
393	(be_op1 op).
394	#prog #sigma #o #bv whd in match be_op1; normalize nodelta @mfr_bind1
395	[ @(λx.x)
396	\| cases bv
397	[ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
398	whd in match Byte_of_val; whd in match sigma_beval; normalize nodelta
399	try @res_preserve_error1 [ @mfr_return_eq1 %]
400	cases(sigma_pc_opt prog sigma pc1) [2: #pc2] normalize nodelta
401	@res_preserve_error1
402	\| #by @mfr_return_eq1 %
403	]
404	qed.
405
406
407	lemma be_op2_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct.
408	∀ b,op.
409	preserving21 ?? res_preserve1 …
410	(sigma_beval prog f_lbls)
411	(sigma_beval prog f_lbls)
412	(λx.let 〈bv,b〉≝ x in 〈sigma_beval prog f_lbls bv,b〉)
413	(be_op2 b op)
414	(be_op2 b op).
415	#prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
416	cases daemon
417	qed. (TODO)
418	(*cases bv
419	[ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
420	normalize nodelta [cases op normalize nodelta @res_preserve_error1] whd in match sigma_beval;
421	normalize nodelta
422	cases bv1
423	[1,2,8,9,15,16,22,23,29,30,36,37:
424	\|3,10,17,24,31,38: #ptr1' #ptr2' #p'
425	\|4,11,18,25,32,39: #by'
426	\|5,12,19,26,33,40: #p'
427	\|6,13,20,27,34,41: #ptr' #p'
428	\|7,14,21,28,35,42: #pc1' #p1'
429	]
430	normalize nodelta try @res_preserve_error1
431	[4,5,8,13,16,20,21,22,23,24,25,26 : @res_preserve_error11 %
432	[2,4,6,8,10,12,14,16,18,20,22,24: cases(sigma_pc_opt ???) try % #pc2 %
433	\|*:]
434	\|*: cases op normalize nodelta
435	try @res_preserve_error1 try( @mfr_return_eq1 %)
436	[1,2,12,13,16,17,18: @if_elim #_ try @res_preserve_error1
437	try( @mfr_return_eq1 %)
438	[ @if_elim #_ @mfr_return_eq1 %
439	\| cases(ptype ptr) normalize nodelta
440	[2: @res_preserve_error1] @mfr_bind1
441	[ @(λx.x)
442	\| whd in match Bit_of_val; normalize nodelta
443	cases b [#bo\|\| #bo #ptr'' #p'' #bit_v]
444	normalize nodelta [2,3: @res_preserve_error1]
445	@mfr_return_eq1 %
446	\| #bi cases(op2 ?????) #by #bi1 normalize nodelta
447	@mfr_return_eq1 %
448	]
449	\| cases(ptype ptr) normalize nodelta @res_preserve_error1
450	]
451	\|3,4,5,6,7,8: @mfr_bind1
452	[1,4,7,10,13,16: @(λx.x)
453	\|2,5,8,11,14,17: whd in match Bit_of_val; normalize nodelta
454	cases b [1,4,7,10,13,16: #bo\|
455	\|2,5,8,11,14,17:
456	\|3,6,9,12,15,18: #bo #ptr'' #p'' #bit_v
457	] normalize nodelta try @res_preserve_error1
458	@mfr_return_eq1 %
459	\|3,6,9,12,15,18: #bi try(@mfr_return_eq1 %) cases(op2 ?????) #by #bi1 normalize nodelta
460	@mfr_return_eq1 %
461	]
462	\|*: whd in match be_add_sub_byte; normalize nodelta
463	[1,2,3: cases(ptype ptr) normalize nodelta [2,4,6: @res_preserve_error1]
464	cases p * [2,4,6: #p_no] #prf normalize nodelta
465	[@res_preserve_error1
466	\|2,3: cases b [1,4: #bo\|2,5: \|3,6: #bo #ptr'' #p'' #bit_v]
467	normalize nodelta [1,2,3,4: @res_preserve_error1]
468	@if_elim #_ [2,4: @res_preserve_error1]
469	@If_elim #INUTILE [2,4: @res_preserve_error1]
470	@pair_elim #a1 #a2 #_ normalize nodelta
471	@mfr_return_eq1 %
472	\|*: @mfr_bind1
473	[1,4,7: @(λx.x)
474	\|2,5,8: whd in match Bit_of_val; normalize nodelta
475	[@mfr_return_eq1 %] cases b
476	[1,4: #bo\|2,5: \|3,6: #bo #ptr'' #p'' #bit_v]
477	normalize nodelta [3,4,5,6: @res_preserve_error1]
478	@mfr_return_eq1 %
479	\|3,6,9: * normalize nodelta [1,3,5: @res_preserve_error1]
480	cases(op2 ?????) #a1 #a2 normalize nodelta
481	@mfr_return_eq1 %
482	]
483	]
484	\|*: cases(ptype ptr') normalize nodelta [2,4: @res_preserve_error1]
485	cases p' * [2,4: #part_no] #prf normalize nodelta
486	[ @res_preserve_error1
487	\| cases b [#bo\|\| #bo #ptr'' #p'' #bit_v]
488	normalize nodelta [1,2: @res_preserve_error1] @if_elim #_
489	[2: @res_preserve_error1] @If_elim #INUTILE [2: @res_preserve_error1]
490	@pair_elim #a1 #a2 #_ normalize nodelta @mfr_return_eq1 %
491	\|*: @mfr_bind1
492	[1,4: @(λx.x)
493	\|2,5: whd in match Bit_of_val; normalize nodelta [ @mfr_return_eq1 %]
494	cases b [#bo\|\| #bo #ptr'' #p'' #bit_v] normalize nodelta
495	[2,3: @res_preserve_error1] @mfr_return_eq1 %
496	\|3,6: * normalize nodelta [1,3: @res_preserve_error1]
497	cases(op2 ?????) #a1 #a2 normalize nodelta
498	@mfr_return_eq1 %
499	]
500	]
501	]
502	]
503	]
504	qed.*)
505
506	lemma pointer_of_address_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
507	preserving1 … res_preserve1 …
508	(λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog f_lbls bv1,
509	sigma_beval prog f_lbls bv2〉)
510	(λx.x)
511	pointer_of_address pointer_of_address.
512	#prog #sigma * #bv1 #bv2 whd in match pointer_of_address;
513	whd in match pointer_of_bevals; normalize nodelta
514	cases bv1 normalize nodelta
515	[ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
516	try @res_preserve_error1
517	[ cases bv2 [ \| \| #ptr1' #ptr2' #p' \| #by' \| #p' \| #ptr' #p' \| #pc1' #p1']
518	normalize nodelta
519	[1,2,3,4,5: @res_preserve_error1
520	\| @if_elim #_ [ @mfr_return_eq1 % \| @res_preserve_error1]
521	]
522	] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
523	[2,4: #pc4] normalize nodelta @res_preserve_error1
524	qed.
525
526	lemma beloadv_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct.
527	∀ptr.
528	preserving1 … opt_preserve1 …
529	(sigma_mem prog f_lbls)
530	(sigma_beval prog f_lbls)
531	(λm.beloadv m ptr)
532	(λm.beloadv m ptr).
533	#prog #sigma #ptr #mem whd in match beloadv; whd in match do_if_in_bounds;
534	normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
535	whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
536	@if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?);
537	normalize nodelta @If_elim [2: >Hzlb * #H @⊥ @H %] #_ @andb_elim @if_elim
538	[2: #_ *] #Hzleb #Hzlb' >Hzlb normalize nodelta >Hzlb' normalize nodelta
539	@mfr_return_eq1 whd in match sigma_mem; normalize nodelta >Hzlb
540	@If_elim [2: * #H @⊥ @H %] * >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %]
541	* %
542	qed.
543
544	lemma bestorev_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
545	∀ptr.
546	preserving21 … opt_preserve1 …
547	(sigma_mem prog f_lbls)
548	(sigma_beval prog f_lbls)
549	(sigma_mem prog f_lbls)
550	(λm.bestorev m ptr)
551	(λm.bestorev m ptr).
552	#prog #sigma #ptr #mem #bv whd in match bestorev; whd in match do_if_in_bounds;
553	normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
554	whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
555	@if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *]
556	whd in match sigma_mem in ⊢ (% → % → ?); normalize nodelta >Hzlb
557	@If_elim [2: * #H @⊥ @H %] * #Hzleb #Hzlb' normalize nodelta >Hzleb
558	>Hzlb' normalize nodelta @mfr_return_eq1 whd in ⊢ (???%); @eq_f @mem_ext_eq
559	[ #bl normalize nodelta % [%]
560	[ whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] *
561	whd in match update_block; normalize nodelta @if_elim
562	[ @eq_block_elim [2: #_ ] #EQbl >EQbl >Hzlb @If_elim [2: * #H @⊥ @H %]
563	* whd in match low_bound; normalize nodelta @if_elim [ #_ %]
564	@eq_block_elim #_ * %
565	\| @eq_block_elim [#_ ] #Hbl * @If_elim
566	[ #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
567	normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl
568	assumption
569	\| #Hzlb'' >Hzlb'' @If_elim [*] #_ %
570	]
571	]
572	\| whd in match update_block; whd in match sigma_mem; normalize nodelta
573	@if_elim @eq_block_elim [2,3: #_ * \|4: *] #Hbl #_ @If_elim
574	[3,4: >Hbl >Hzlb * [2: #H @⊥ @H %] @If_elim [2: * #H @⊥ @H %] *
575	whd in match high_bound; normalize nodelta @if_elim [#_ %]
576	@eq_block_elim [ #_ ] #H @⊥ @H %
577	\| #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match high_bound;
578	normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *]
579	#H @⊥ @Hbl assumption
580	\| #Hzlb'' >Hzlb'' @If_elim [*] #_ %
581	]
582	\| #z whd in match update_block; whd in match sigma_mem; normalize nodelta
583	@if_elim @eq_block_elim [2,3: #_ * \|4: *] #Hbl #_
584	[ @If_elim #Hzlb'' >Hzlb'' [2: @If_elim * #_ %] @If_elim @andb_elim
585	@if_elim [2: #_ *] #Hzleb' #Hzlb'''
586	[ @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta
587	@If_elim @andb_elim @if_elim [2: #_ *] @if_elim
588	[1,3,5: @eq_block_elim [2,4,6: #_ ] #H @⊥ @Hbl assumption] #_ >Hzleb'
589	whd in match high_bound; normalize nodelta @if_elim
590	[1,3: @eq_block_elim [2,4: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
591	[ * %] * #H @⊥ @H %
592	\| @If_elim * [2: #H @⊥ @H %] whd in match low_bound; normalize nodelta
593	@if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_
594	>Hzleb' whd in match high_bound; normalize nodelta @if_elim
595	[@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
596	@If_elim [2: #_ %] *
597	\| @If_elim [2: * #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim
598	[@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ #_
599	whd in match low_bound in Hzleb'; normalize nodelta in Hzleb';
600	whd in match high_bound; normalize nodelta @if_elim
601	[@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ @If_elim [2: #_ %]
602	@andb_elim @if_elim [2: #_ ] #H >H in Hzleb';
603	]
604	\| whd in ⊢ (??%?); @if_elim @eqZb_elim [2,3: #_ * \|4: ] #Hz
605	[ >Hzlb @If_elim [2: * #H @⊥ @H %] * @If_elim @andb_elim @if_elim
606	[2: #_ ] #Hzleb' #Hzlb'' >Hbl >Hzlb @If_elim [2,4,6: #H @⊥ @H %] #_
607	whd in match low_bound; normalize nodelta @eq_block_elim
608	[2,4,6: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound;
609	normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %]
610	#_ normalize nodelta
611	[1,2: >Hzleb' >Hzlb'' @If_elim [2,3: * #H @⊥ @H %]
612	#_ [2: %] whd in ⊢ (???(???%)); @if_elim [2: #_ %]
613	@eqZb_elim [2: #_ *] #H @⊥ @Hz assumption
614	\| @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ ] #H >H in Hzleb';
615	]
616	\| >Hbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
617	normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] #_ normalize nodelta
618	whd in match high_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %]
619	normalize nodelta >Hz >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] #_ #_
620	whd in ⊢ (???(???%)); @eqZb_elim [2: * #H @⊥ @H %] #_ %
621	]
622	]
623	]
624	\| %
625	]
626	qed.
627
628
629	lemma sp_ok : ∀prog : ertl_program.
630	∀f_lbls : lbl_funct.
631	∀f_regs : regs_funct.∀restr.
632	preserving1 … res_preserve1 …
633	(λst.sigma_state prog f_lbls f_regs restr st)
634	(λx.x)
635	(sp ERTL_semantics)
636	(sp ERTLptr_semantics).
637	#prog #f_lbls #f_regs #restr #st whd in match sp; normalize nodelta
638	whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state;
639	normalize nodelta whd in match sigma_regs; normalize nodelta
640	cases(regs ? st) #psd_r #hw_r normalize nodelta
641	inversion(pointer_of_address ?) normalize nodelta [2: #e #_ @res_preserve_error1]
642	#pt #EQ lapply(jmeq_to_eq ??? EQ) -EQ whd in match hwreg_retrieve; normalize nodelta
643	whd in match sigma_hw_register_env; normalize nodelta
644	change with (sigma_beval prog f_lbls BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?);
645	>lookup_map >lookup_map
646	cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef)
647	[ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
648	whd in match pointer_of_address; whd in match pointer_of_bevals; normalize nodelta
649	[1,2,3,4,5: #ABS destruct
650	\| cases(lookup beval 6 (bitvector_of_register RegisterSPH) (reg_env hw_r) BVundef)
651	[ \| \| #ptr1' #ptr2' #p' \| #by' \| #p' \| #ptr' #p' \| #pc1' #p1']
652	whd in match sigma_beval; normalize nodelta
653	[1,2,3,4,5: #ABS destruct
654	\| @if_elim [2: #_ #ABS destruct] #H whd in ⊢ (??%? → ?); #EQ destruct
655	normalize nodelta @match_reg_elim #INUTILE
656	[ @mfr_return_eq1 % \| @res_preserve_error1 ]
657	\| cases (sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct
658	]
659	\| whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?)
660	normalize nodelta [2: #x] #EQ destruct
661	]
662	qed.
663
664	lemma set_sp_ok : ∀prog : ertl_program.
665	∀f_lbls : lbl_funct.
666	∀f_regs : regs_funct.∀restr.∀ptr,st.
667	set_sp ? ptr (sigma_state prog f_lbls f_regs restr st) =
668	sigma_state prog f_lbls f_regs restr (set_sp ? ptr st).
669	#prog #f_lbls #f_regs #restr #ptr #st whd in match set_sp; whd in match sigma_state;
670	normalize nodelta @eq_f3 try % whd in match (save_sp ???);
671	whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta
672	cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f
673	whd in match hwreg_store_sp; normalize nodelta whd in match sigma_hw_register_env;
674	normalize nodelta whd in match hwreg_store; normalize nodelta @eq_f2 [2: %]
675	>insert_map @eq_f >insert_map %
676	qed.
677
678	(TO BE MOVED IN TranslateUtils.ma )
679	include "utilities/listb_extra.ma".
680	lemma not_in_added_registers : ∀p : graph_params.
681	∀globals : list ident.∀fn,f_regs,r.
682	(∀lbl. code_has_label p globals (joint_if_code … fn) lbl →
683	¬(bool_to_Prop (r ∈ (f_regs lbl)))) →
684	¬ (r ∈ (set_from_list RegisterTag (added_registers p globals fn f_regs))).
685	#p #globals #fn #f_regs #r #H whd in match added_registers; normalize nodelta
686	@foldi_ind [@I] #lbl #labels_fn #stmt #regs * #lbl_not_in_fn #EQstmt #IH
687	lapply(Prop_notb … IH) -IH * #IH
688	lapply(H lbl ?)
689	[whd in match code_has_label; whd in match code_has_point; normalize nodelta
690	whd in match (stmt_at ????); >EQstmt @I]
691	* #H1 @notb_elim @if_elim [2: #_ @I] #ABS
692	lapply(mem_list_as_set … ABS) #ABS' cases(Exists_append … ABS') #ABS''
693	[ @H1 @Exists_memb lapply ABS'' elim (f_regs lbl) [ *] #hd #tl #IH whd in ⊢ (% → %);
694	* [ #EQ >EQ % %] #H %2 @IH @H
695	\| @IH @list_as_set_mem assumption
696	]
697	qed.
698
699	lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀a : A.In A l1 a → In A (l1@l2) a.
700	#A #l1 elim l1 [#l2 #a ] #hd #tl #IH
701	[#a normalize * [#H % assumption \| #H %2 >append_nil assumption]]
702	#hd1 #tl1 #a normalize * [#H % assumption \| #H %2 @IH assumption]
703	qed.
704
705	lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀a : A.In A l2 a → In A (l1@l2) a.
706	#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a ] #hd #tl #IH
707	[#a normalize * [#H %1 assumption\| #H %2 assumption]]
708	#hd1 #tl1 #a normalize *
709	[ #H %2 >append_cons @Exists_append1 >H elim tl1 [% %] #hd2 #tl2 #H1 normalize %2 //
710	\| #H %2 >append_cons @IH assumption]
711	qed.
712
713	lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
714	All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
715	#A #P #l1 elim l1
716	[ #l2 change with l2 in ⊢ (???% → ?); #H % //]
717	#a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
718	* #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
719	qed.
720
721	include alias "common/PositiveMap.ma".
722
723	lemma added_register_pm : ∀A,B. ∀m : positive_map A.
724	∀f : Pos → list B.∀b.
725	let added ≝ fold A (list B) (λp.λ_.λacc.(f p)@acc) m [ ] in
726	All B (λx.x≠b) added →
727	(∀i. lookup_opt unit i (domain_of_pm A m) ≠ None ? → All B (λx.x≠b) (f i)).
728	#A #B #m #f #b normalize nodelta @pm_fold_ind
729	[ #_ #i normalize * #H @⊥ @H %
730	\| #p #ps #a #lst #H #H1 #H2 #H3 #i cases(decidable_eq_pos i p)
731	[1,3: #EQ destruct(EQ) #_ cases(append_All … H3) //
732	\|*: #Hi >lookup_opt_insert_miss [2,4: assumption] @H2
733	cases(append_All … H3) //
734	]
735	]
736	qed.
737
738	lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) →
739	decidable (In A l a).
740	#A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
741	[ #H % %2 assumption \| * #H cases (DEC hd)
742	[ #H1 %1 %1 assumption \| * #H1 %2 % * [ #H2 @H1 assumption \| #H2 @H assumption]]
743	qed.
744
745	lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
746	#A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
747	% #H1 @H % >H1 %
748	qed.
749
750	lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
751	#A #l elim l [#a #_ % ] #hd #tl #IH #a * #H1 #H2 % *
752	[ #H3 @H1 >H3 % \| cases(IH a H2) #H3 #H4 @H3 assumption]
753	qed.
754
755	lemma added_register_aux : ∀tag,A,B.∀m : identifier_map tag A.
756	∀f : identifier tag → list B.(∀b,b' : B.decidable (b=b')) →
757	let added ≝ foldi A (list B) tag (λl.λ_.λacc. (f l)@acc) m [ ] in
758	∀i,a,b.lookup tag A m i = Some ? a → In B (f i) b → In B added b.
759	#tag #A #B * #m #f #DEC * #i #a #b whd in ⊢ (??%? → ?); normalize nodelta
760	#H #H1
761	cases(decidable_In ? (foldi A (list B) tag
762	(λl.λ_.λacc.(f l)@acc)
763	(an_id_map tag A m) []) b (DEC b)) [//]
764	#H3 @⊥ lapply(In_all ??? H3) -H3 #H3
765	lapply(added_register_pm ?? m ?? H3 i ?)
766	[cases(domain_of_pm_present ? m i) #H4 #_ @H4 >H % #EQ destruct]
767	lapply H1 elim (f ?) [] #hd #tl #IH [#EQ * >EQ * #H4 #_ @H4 %]
768	#H4 * #_ @IH assumption
769	qed.
770
771	lemma in_added_registers : ∀p : graph_params.
772	∀globals : list ident.∀fn,f_regs,r.
773	∀lbl.code_has_label p globals (joint_if_code … fn) lbl →
774	In ? (f_regs lbl) r →
775	In ? (added_registers p globals fn f_regs) r.
776	#p #globals #fn #f_regs #r #lbl whd in match code_has_label;
777	whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
778	inversion(lookup LabelTag ???) [ #_ *] #stmt #EQstmt #_
779	#H @(added_register_aux … EQstmt H)
780	* #p * #p' cases(decidable_eq_pos p p') [ #EQ destruct % % \| * #H1 %2 % #EQ destruct @H1 %]
781	qed.
782
783
784	include alias "basics/lists/listb.ma".
785
786	(*
787	definition get_internal_function_from_ident :
788	∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
789	ident → option (joint_closed_internal_function p globals) ≝
790	λp,globals,ge,id.
791	! bl ← (find_symbol (joint_function p globals) ge id);
792	! bl' ← (code_block_of_block bl);
793	! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl');
794	return fn.
795
796	lemma get_internal_function_from_ident_ok :
797	∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals).
798	∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 →
799	get_internal_function_from_ident p globals ge f= return fn.
800	#p #globals #ge #bl #f #fn #EQf
801	@('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function;
802	normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H
803	#f2 #EQf2 #H @('bind_inversion H) -H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?);
804	#EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta
805	>(symbol_of_block_rev … EQf2) >m_return_bind
806	cut(code_block_of_block bl = return bl)
807	[ whd in match code_block_of_block; normalize nodelta @match_reg_elim
808	[ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl
809	>m_return_bind >EQf %
810	qed.
811	*)
812
813	lemma eval_seq_no_pc_no_call_ok :
814	∀prog : ertl_program.
815	let trans_prog ≝ ertl_to_ertlptr prog in
816	∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
817	∀stack_size.
818	∀bl.∀id.
819	∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).∀seq.
820	(∀l. code_has_label … (joint_if_code … fn) l →
821	(All … (λreg.bool_to_Prop(¬(reg ∈ (f_regs bl l))))
822	(get_used_registers_from_seq … (functs … ERTL) seq))) →
823	preserving1 ?? res_preserve1 ????
824	(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
825	(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
826	(eval_seq_no_pc ERTL_semantics
827	(globals (mk_prog_params ERTL_semantics prog stack_size))
828	(ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id seq)
829	(eval_seq_no_pc ERTLptr_semantics
830	(globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
831	(ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size))
832	id (seq_embed … seq)).
833	#prog #f_lbls #f_regs #stack_size #bl #f #fn #seq #fresh_regs
834	cases seq in fresh_regs;
835	[ #c #_ #st @mfr_return1
836	\| #pm #fesh_regs #st whd in match pair_reg_move; normalize nodelta
837	@mfr_bind1
838	[ 2: change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
839	whd in match move_dst_not_fresh; normalize nodelta cases pm in fesh_regs;
840	* [#r1 \| #R1] #m_src [2: #_ @I] normalize nodelta #fresh_regs
841	@not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
842	whd in ⊢ (% → %); * #H #_ @Prop_notb @H
843	\| \| #regs @mfr_return_eq1 %
844	]
845	\| #r #fresh_regs #st @mfr_bind1
846	[2: @pop_ok \|
847	\| * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
848	[2: @ps_reg_store_ok
849	@not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
850	whd in ⊢ (% → %); * #H #_ @Prop_notb @H
851	]
852	]
853	\| #r #_ #st @mfr_bind1
854	[2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok \|
855	\| #bv @push_ok
856	]
857	\| #i
858	#i_spec
859	change with ((dpl_reg ERTL) → ?)
860	#dpl
861	change with ((dph_reg ERTL) → ?)
862	#dph #fresh_regs #st @mfr_bind1
863	[ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
864	\| whd in match dpl_store; normalize nodelta @mfr_bind1
865	[2: @opt_safe_elim #bl #EQbl
866	@opt_safe_elim #bl'
867	>(find_symbol_transf …
868	(λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog i) in ⊢ (%→?);
869	>EQbl #EQ destruct whd in match sigma_state; normalize nodelta
870	change with (sigma_beval prog f_lbls (BVptr …))
871	in ⊢ (???????(?????%?)?);
872	@ps_reg_store_ok
873	@not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
874	whd in ⊢ (% → %); * #H #_ @Prop_notb @H \|
875	\| #regs @mfr_return_eq1 %
876	]
877	\| #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'
878	>(find_symbol_transf …
879	(λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog i) in ⊢ (%→?);
880	>EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1
881	[2: whd in match sigma_state; normalize nodelta
882	change with (sigma_beval prog f_lbls (BVptr …))
883	in ⊢ (???????(?????%?)?);
884	@ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
885	whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H \|
886	\| #regs @mfr_return_eq1 %
887	]
888	]
889	\| #op #a #b #arg1 #arg2 #fresh_regs #st @mfr_bind1
890	[2: whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta
891	@ps_arg_retrieve_ok \|
892	\| #bv1 @mfr_bind1
893	[2: whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta
894	@ps_arg_retrieve_ok \|
895	\| #bv2 @mfr_bind1
896	[2: @be_opaccs_ok \|
897	\| * #bv3 #bv4 normalize nodelta @mfr_bind1
898	[ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
899	\| whd in match acca_store; normalize nodelta @mfr_bind1
900	[2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
901	lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H \|
902	\| #regs @mfr_return_eq1 %
903	]
904	\| #st1 whd in match accb_store; normalize nodelta @mfr_bind1
905	[2: whd in match sigma_state; normalize nodelta
906	@ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
907	lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H \|
908	\| #regs @mfr_return_eq1 %
909	]
910	]
911	]
912	]
913	]
914	\| #op #r1 #r2 #fresh_regs #st @mfr_bind1
915	[ @(sigma_beval prog f_lbls)
916	\| whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok
917	\| #bv1 @mfr_bind1
918	[ @(sigma_beval prog f_lbls)
919	\| @be_op1_ok
920	\| #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
921	[2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
922	@not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
923	whd in ⊢ (% → %); * #H #_ @Prop_notb @H \|
924	\| #regs @mfr_return_eq1 %
925	]
926	]
927	]
928	\| #op2 #r1 #r2 #arg #fresh_regs #st @mfr_bind1
929	[2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok \|
930	\| #bv @mfr_bind1
931	[2: whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok \|
932	\| #bv1 @mfr_bind1
933	[2: @be_op2_ok \|
934	\| * #bv2 #b @mfr_bind1
935	[ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
936	\| whd in match acca_store; normalize nodelta @mfr_bind1
937	[2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
938	@not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
939	whd in ⊢ (% → %); * #H #_ @Prop_notb @H \|
940	\| #regs @mfr_return_eq1 %
941	]
942	\| #st1 @mfr_return_eq1 %
943	]
944	]
945	]
946	]
947	\| #_ #st @mfr_return_eq1 %
948	\| #_ #st @mfr_return_eq1 %
949	\| #r1 #dpl #dph #fresh_regs #st @mfr_bind1
950	[2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok \|
951	\| #bv @mfr_bind1
952	[2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok \|
953	\| #bv1 @mfr_bind1
954	[ @(λx.x)
955	\| @(pointer_of_address_ok ? ? 〈bv1,bv〉)
956	\| #ptr @mfr_bind1
957	[2: @opt_to_res_preserve1 @beloadv_ok \|
958	\| #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
959	[2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
960	@not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
961	whd in ⊢ (% → %); * #H #_ @Prop_notb @H \|
962	\| #regs @mfr_return_eq1 %
963	]
964	]
965	]
966	]
967	]
968	\| #dpl #dph #r #_ #st @mfr_bind1
969	[2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok \|
970	\| #bv @mfr_bind1
971	[2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok \|
972	\| #bv1 @mfr_bind1
973	[ @(λx.x)
974	\| @(pointer_of_address_ok ? ? 〈bv1,bv〉)
975	\| #ptr @mfr_bind1
976	[2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok \|
977	\| #bv2 @mfr_bind1
978	[2: @opt_to_res_preserve1 @bestorev_ok \|
979	\| #m @mfr_return_eq1 %
980	]
981	]
982	]
983	]
984	]
985	\| #ext #fresh_regs #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f)
986	normalize nodelta
987	[ @res_preserve_error1
988	\| #n cases ext in fresh_regs; normalize nodelta
989	[1,2: #_ @mfr_bind1
990	[1,4: @(λx.x)
991	\|2,5: @sp_ok
992	\|3,6: #ptr @mfr_return_eq1 >set_sp_ok %
993	]
994	\| #r #fresh_regs whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
995	[2: whd in match sigma_state; normalize nodelta
996	change with (sigma_beval prog f_lbls (BVByte ?))
997	in ⊢ (???????(??%?)?);
998	@ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
999	lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H \|
1000	\| #regs @mfr_return_eq1 %
1001	]
1002	]
1003	]
1004	]
1005	#regs @mfr_return_eq1 %
1006	qed.
1007
1008	lemma partial_inj_sigma : ∀ prog : ertl_program.
1009	∀f_lbls : lbl_funct.
1010	let sigma ≝ get_sigma prog f_lbls in
1011	∀id,lbl1,lbl2. sigma id lbl1 ≠ None ? → sigma id lbl1 = sigma id lbl2 → lbl1 = lbl2.
1012	#prog #good #bl #lbl1 #lbl2 inversion(get_sigma … lbl1)
1013	[#_ * #H @⊥ @H %] #lbl1' whd in match get_sigma; normalize nodelta
1014	#H @('bind_inversion H) -H #bl' whd in match code_block_of_block; normalize nodelta
1015	@match_reg_elim [#_ #ABS destruct] #prf #EQ destruct #H @('bind_inversion H) -H
1016	* #id #fn #H lapply(res_eq_from_opt ??? H) -H #EQfn #H @('bind_inversion H) -H
1017	* #lbl1'' #stmt1 #H1 whd in ⊢ (??%? → ?); #EQ destruct
1018	#_ #H lapply(sym_eq ??? H) -H >m_return_bind >EQfn >m_return_bind
1019	#H @('bind_inversion H) -H * #lbl2' #stmt2 #H2
1020	whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1)
1021	lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta
1022	[ normalize nodelta @eq_identifier_elim #EQ1 *
1023	@eq_identifier_elim #EQ2 * >EQ1 >EQ2 %
1024	\| #lb #tl whd in match split_on_last; normalize nodelta whd in match (foldr ?????);
1025	cases( foldr label (option (list label×label)) … tl) normalize nodelta
1026	[2: * #x #lb1] @eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 *
1027	>EQ1 >EQ2 %
1028	]
1029	qed.
1030
1031
1032	(TO BE MOVED : GENERAL!!!)
1033	lemma pc_of_label_eq :
1034	∀p,p'.let pars ≝ mk_sem_graph_params p p' in
1035	∀globals,ge,bl,i_fn,lbl.
1036	fetch_internal_function ? ge bl = return i_fn →
1037	pc_of_label pars globals ge bl lbl =
1038	OK ? (pc_of_point ERTL_semantics bl lbl).
1039	#p #p' #globals #ge #bl #i_fn #lbl #EQf
1040	whd in match pc_of_label;
1041	normalize nodelta >EQf >m_return_bind %
1042	qed.
1043
1044	lemma pop_ra_ok :
1045	∀prog : ertl_program.
1046	∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
1047	∀restr.
1048	preserving1 … res_preserve1 …
1049	(sigma_state prog f_lbls f_regs restr)
1050	(λx.let 〈st,pc〉 ≝ x in
1051	〈sigma_state prog f_lbls f_regs restr st,
1052	sigma_stored_pc prog f_lbls pc〉)
1053	(pop_ra ERTL_semantics)
1054	(pop_ra ERTLptr_semantics).
1055	cases daemon (TODO) qed.
1056	(*
1057	#prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta
1058	@mfr_bind1
1059	[ \| @pop_ok ] * #bv #st1 @mfr_bind1 [ \| @pop_ok] * #bv1 #st2 @mfr_bind1
1060	[ @(sigma_stored_pc prog f_lbls)
1061	\| whd in match pc_of_bevals; normalize nodelta
1062	cases bv [ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc #p]
1063	whd in match sigma_beval; normalize nodelta try @res_preserve_error1
1064	inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1]
1065	#sigma_pc #sigma_pc_spec normalize nodelta cases bv1
1066	[ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
1067	normalize nodelta try @res_preserve_error1
1068	inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1]
1069	#sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1]
1070	@andb_elim @if_elim [2: #_ ] @andb_elim @if_elim [2: #_ ]
1071	#_ #H >H @eq_program_counter_elim [2: #_ *]
1072	#EQspc * @eq_program_counter_elim
1073	[#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta
1074	>sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec
1075	whd in match sigma_pc_opt; normalize nodelta @if_elim
1076	[ #H2 #EQ lapply(sym_eq ??? EQ) -EQ @if_elim [#_ whd in ⊢ (??%% → ?); #EQ destruct %]
1077	#H3 #H @('bind_inversion H) -H #x #H4 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; *
1078	\| #H2 @if_elim
1079	[ #H3 #H @('bind_inversion H) -H #x1 #_ whd in match pc_of_point; normalize nodelta
1080	whd in ⊢ (??%? → ?); #EQ destruct >H3 in H2; *
1081	\| #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim
1082	[#H >H in H3; ] #_ #EQ >EQ @('bind_inversion EQ) -EQ #x cases pc1 #bl1 #pos1
1083	whd in match (point_of_pc ??); #x_spec whd in match (pc_of_point ???);
1084	whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
1085	#H @('bind_inversion H) -H * #lbl cases pc #bl #pos whd in match (point_of_pc ??);
1086	#lbl_spec whd in match pc_of_point; normalize nodelta
1087	whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
1088	@eq_f cut(an_identifier LabelTag pos = an_identifier LabelTag pos1 → pos = pos1)
1089	[ #EQ destruct %] #APP @APP @(partial_inj_sigma prog f_lbls bl1 …)
1090	[ >lbl_spec % #EQ destruct] >x_spec >lbl_spec %
1091	]
1092	]
1093	\| #pc @mfr_return_eq1 %
1094	]
1095	qed.*)
1096
1097	lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc.
1098	sigma_pc_opt prog f_lbls pc ≠ None ? →
1099	pc_block … pc = pc_block … (sigma_stored_pc prog f_lbls pc).
1100	#prog #sigma * #bl #pos whd in match sigma_stored_pc; normalize nodelta
1101	inversion(sigma_pc_opt ???) [ #_ * #H @⊥ @H %] #pc
1102	whd in match sigma_pc_opt; normalize nodelta @if_elim
1103	[#_ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #_
1104	#H @('bind_inversion H) -H * #lbl #_
1105	whd in ⊢ (??%? → ?); #EQ destruct
1106	#_ %
1107	qed.
1108
1109	include "joint/extra_joint_semantics.ma".
1110
1111	lemma pop_frame_ok : ∀prog : ertl_program.
1112	let trans_prog ≝ ertl_to_ertlptr prog in
1113	∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
1114	∀restr.
1115	preserving1 ?? res_preserve1 ????
1116	(sigma_state prog f_lbls f_regs restr)
1117	(λx.let 〈st,pc〉 ≝ x in
1118	match fetch_internal_function ? (globalenv_noinit … prog)
1119	(pc_block pc) with
1120	[ OK y ⇒ let 〈id,f〉 ≝ y in
1121	〈sigma_state prog f_lbls f_regs
1122	(added_registers ERTL (prog_var_names … prog) f
1123	(f_regs (pc_block pc))) st,
1124	sigma_stored_pc prog f_lbls pc〉
1125	\| Error e ⇒ 〈dummy_state,null_pc one〉
1126	])
1127	(ertl_pop_frame)
1128	(ertl_pop_frame).
1129	#prog #f_lbls #f_regs #restr #st whd in match ertl_pop_frame; normalize nodelta
1130	@mfr_bind1
1131	[ @(λx.match sigma_frames_opt prog f_lbls f_regs x with [Some l ⇒ l \| None ⇒ [ ]])
1132	\| @opt_to_res_preserve1 whd in match sigma_state; normalize nodelta
1133	cases(st_frms … st) [@opt_preserve_none1] #l whd in match sigma_frames;
1134	normalize nodelta >m_return_bind #x #x_spec %{l} % [%] >x_spec %
1135	\| * normalize nodelta [@res_preserve_error1] * #loc_mem #bl #tl normalize nodelta
1136	inversion(sigma_frames_opt ????) normalize nodelta [ #_ @res_preserve_error1]
1137	#l whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta
1138	whd in match (foldr ?????); normalize nodelta inversion(fetch_internal_function ???)
1139	normalize nodelta [2: #e #_ #ABS destruct(ABS)] * #f #fn #EQfn
1140	#H @('bind_inversion H) -H #l1
1141	change with (sigma_frames_opt prog f_lbls f_regs tl = ? → ?) #EQl1
1142	whd in ⊢ (??%? → ?); #EQ destruct(EQ) @mfr_bind1
1143	[2: whd in match sigma_state; whd in match set_regs; whd in match set_frms;
1144	normalize nodelta
1145	cut( 〈sigma_register_env prog f_lbls
1146	(added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
1147	(f_regs bl))
1148	loc_mem,
1149	\snd (sigma_regs prog f_lbls restr (regs ERTLptr_semantics st))〉 =
1150	sigma_regs prog f_lbls
1151	(added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
1152	(f_regs bl)) (〈loc_mem,\snd (regs ERTL_state st)〉)) [
1153	whd in match sigma_regs; normalize nodelta cases(regs … st) #x1 #x2
1154	%] #EQ >EQ -EQ <EQl1 in ⊢ (???????%?);
1155	change with (sigma_state prog f_lbls f_regs
1156	(added_registers ERTL (prog_var_names … prog) fn (f_regs bl))
1157	(mk_state ? (Some ? tl) (istack … st) (carry … st) (〈loc_mem,\snd (regs … st)〉)
1158	(stack_usage … st) (m … st))) in ⊢ (???????(??%)?); @pop_ra_ok \|
1159	\| * #st1 #pc1 @if_elim normalize nodelta [2: #_ @res_preserve_error1]
1160	normalize nodelta @eq_block_elim [2: #_ ] #EQbl1 @if_elim
1161	[2: >EQbl1 @eq_block_elim [#_ ] #H @⊥ @H <pc_block_eq [%] %
1162	cases bl in EQbl1 EQfn; #p1 #p2 #EQ destruct lapply p2
1163	whd in match sigma_stored_pc; normalize nodelta cases(sigma_pc_opt ???)
1164	normalize nodelta [2: #pc2] #p2 [#_ #EQ destruct]
1165	>fetch_internal_function_no_zero [2: %] #EQ destruct
1166	\| @eq_block_elim [2: #_ ] #EQbl11 @mfr_return_eq1 normalize nodelta
1167	cases bl in EQbl11 EQfn; #p1 #p2 #EQ destruct
1168	lapply p2 cases(pc_block pc1) #p11 #p22 #e #EQfn1 >EQfn1 %
1169	]
1170	]
1171	]
1172	qed.
1173
1174	lemma fetch_ok_sigma_pc_ok :∀prog : ertl_program.
1175	∀ f_lbls,f_regs,id,fn,st.
1176	fetch_internal_function … (globalenv_noinit … prog)
1177	(pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
1178	pc … (sigma_state_pc prog f_lbls f_regs st) = pc … st.
1179	#prog #f_lbls #f_regs #id #fn #st whd in match sigma_state_pc;
1180	normalize nodelta cases(fetch_internal_function ?? (pc_block (pc … st)))
1181	normalize nodelta [* #id1 #fn1 #_ %]
1182	#e >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ)
1183	qed.
1184
1185	lemma fetch_ok_sigma_state_ok : ∀prog : ertl_program.
1186	∀ f_lbls,f_regs,id,fn,st.
1187	fetch_internal_function … (globalenv_noinit … prog)
1188	(pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
1189	let added ≝ (added_registers ERTL (prog_var_names … prog) fn
1190	(f_regs (pc_block (pc … st)))) in
1191	st_no_pc … (sigma_state_pc prog f_lbls f_regs st) =
1192	sigma_state prog f_lbls f_regs added (st_no_pc … st).
1193	#prog #f_lbls #f_regs #id #fn #st #EQf whd in match sigma_state_pc;
1194	normalize nodelta <(fetch_ok_sigma_pc_ok … EQf) >EQf %
1195	qed.
1196
1197	lemma fetch_ok_sigma_pc_block_ok : ∀prog : ertl_program.
1198	∀ f_lbls,id,fn,pc.
1199	fetch_internal_function … (globalenv_noinit … prog)
1200	(pc_block (sigma_stored_pc prog f_lbls pc)) = return 〈id,fn〉 →
1201	pc_block (sigma_stored_pc prog f_lbls pc) = pc_block pc.
1202	#prog #f_lbls #id #fn #pc #EQf <pc_block_eq [%]
1203	lapply EQf whd in match sigma_stored_pc; normalize nodelta
1204	cases(sigma_pc_opt ???) normalize nodelta [2: #pc #_ % #EQ destruct(EQ)]
1205	>fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ)
1206	qed.
1207
1208	lemma fetch_stmt_ok_sigma_pc_ok : ∀prog : ertl_program.
1209	∀ f_lbls,f_regs,id,fn,stmt,st.
1210	fetch_statement ERTL_semantics (prog_var_names … prog)
1211	(globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) =
1212	return 〈id,fn,stmt〉 →
1213	pc … (sigma_state_pc prog f_lbls f_regs st) = pc … st.
1214	#prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H)
1215	* #id1 #fn1 #EQfn1 #_ @(fetch_ok_sigma_pc_ok … EQfn1)
1216	qed.
1217
1218	lemma fetch_stmt_ok_sigma_state_ok : ∀prog : ertl_program.
1219	∀ f_lbls,f_regs,id,fn,stmt,st.
1220	fetch_statement ERTL_semantics (prog_var_names … prog)
1221	(globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) =
1222	return 〈id,fn,stmt〉 →
1223	let added ≝ (added_registers ERTL (prog_var_names … prog) fn
1224	(f_regs (pc_block (pc … st)))) in
1225	st_no_pc … (sigma_state_pc prog f_lbls f_regs st) =
1226	sigma_state prog f_lbls f_regs added (st_no_pc … st).
1227	#prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) -H
1228	* #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
1229	whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_state_ok … EQfn1)
1230	qed.
1231
1232	lemma fetch_stmt_ok_sigma_pc_block_ok : ∀prog : ertl_program.
1233	∀ f_lbls,id,fn,stmt,pc.
1234	fetch_statement ERTL_semantics (prog_var_names … prog)
1235	(globalenv_noinit … prog) (sigma_stored_pc prog f_lbls pc) = return 〈id,fn,stmt〉 →
1236	pc_block (sigma_stored_pc prog f_lbls pc) = pc_block pc.
1237	#prog #f_lbls #id #fn #stmt #st #H @('bind_inversion H) -H
1238	* #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
1239	whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_pc_block_ok … EQfn1)
1240	qed.
1241
1242	lemma fetch_ok_sigma_last_pop_ok :∀prog : ertl_program.
1243	∀ f_lbls,f_regs,id,fn,st.
1244	fetch_internal_function … (globalenv_noinit … prog)
1245	(pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
1246	last_pop … (sigma_state_pc prog f_lbls f_regs st) =
1247	sigma_stored_pc prog f_lbls (last_pop … st).
1248	#prog #f_lbls #f_regs #id #fn #st whd in match sigma_state_pc; normalize nodelta
1249	cases(fetch_internal_function ?? (pc_block (pc … st))) normalize nodelta
1250	[ * #x #y #_ %] #e >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?);
1251	#EQ destruct(EQ)
1252	qed.
1253
1254	lemma fetch_stmt_ok_sigma_last_pop_ok :∀prog : ertl_program.
1255	∀ f_lbls,f_regs,id,fn,stmt,st.
1256	fetch_statement ERTL_semantics (prog_var_names … prog)
1257	(globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st))
1258	= return 〈id,fn,stmt〉 →
1259	last_pop … (sigma_state_pc prog f_lbls f_regs st) =
1260	sigma_stored_pc prog f_lbls (last_pop … st).
1261	#prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) -H
1262	* #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
1263	whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_last_pop_ok … EQfn1)
1264	qed.
1265
1266	lemma excluded_middle_list :
1267	∀A : Type[0]. ∀P : A → Prop.∀ l : list A. (∀a : A.In A l a → decidable … (P a)) →
1268	All … P l ∨ Exists … (λa.¬(P a)) l.
1269	#A #P #l elim l [#_ % %] #hd #tl #IH #Dec
1270	cases IH [ cases(Dec hd ?)
1271	[ #H1 #H2 % whd % assumption
1272	\| #H #_ %2 whd % assumption
1273	\| % %
1274	]
1275	\| #H %2 whd %2 assumption
1276	\| #a #H @Dec %2 assumption
1277	]
1278	qed.
1279
1280	lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
1281	code_block_of_block bl = return bl.
1282	* #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
1283	[ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
1284	qed.
1285
1286	lemma split_on_last_append : ∀A : Type[0]. ∀pre : list A.
1287	∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
1288	#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
1289	whd in ⊢ (??%? → ?); #EQ >EQ %
1290	qed.
1291
1292	include alias "common/Identifiers.ma".
1293
1294	lemma get_sigma_idempotent :
1295	∀prog : ertl_program.
1296	∀ f_lbls,f_regs.
1297	∀f_bl_r.
1298	b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1299	(λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
1300	∀id,fn,bl,pt,stmt.
1301	fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
1302	stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt →
1303	f_lbls bl pt = [ ] → get_sigma prog f_lbls bl pt = return pt.
1304	#prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #EQfn #EQstmt #EQlabels
1305	cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
1306	#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
1307	[2,4: #x #y ] normalize nodelta #EQ destruct(EQ) #_ #_ #_ #_ #_
1308	#_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H cases stmt in EQstmt;
1309	[3: *
1310	\|2: * [#lbl \|\| ] #EQstmt normalize nodelta #bl * whd in ⊢ (% → ?);
1311	inversion (f_regs ??) [2,4: #x #y #_ #_ *] #EQregs normalize nodelta
1312	#EQ destruct(EQ) whd in ⊢ (%→?); * #pref * #mid ** #EQmid whd in ⊢ (% → ?);
1313	* #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); #EQt_stmt
1314	\| * [#c \| * [#c_id\|#c_ptr] #args #dest \| #r #lbl \| #seq ] #nxt #EQstmt
1315	whd in ⊢ (% → ?); * #bl >if_merge_right [2,4,6,8,10: %] * whd in ⊢ (% → ?);
1316	inversion(f_regs ??) normalize nodelta
1317	[2,4,5,8,10: [1,2,4,5: #x #y] #_ [1,2,3,4: #_] \|6: #r [2: #x #y] ]
1318	[1,2: #_] #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?);
1319	* #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (%→ ?);
1320	[ * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 *
1321	#EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1322	whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ)
1323	whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%); >EQlabels in e0;
1324	#e0 destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%);
1325	destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
1326	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1327	* #_ #EQ destruct(EQ) ]
1328	whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind
1329	>EQfn >m_return_bind inversion(find ????)
1330	[1,3,5,7,9,11: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels
1331	normalize nodelta @eq_identifier_elim [1,3,5,7,9,11: #_ * \|: #H #_ @H %]]
1332	* #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
1333	inversion(f_lbls ??)
1334	[1,3,5,7,9,11: #_ normalize nodelta @eq_identifier_elim [2,4,6,8,10,12: #_ *] #EQ #_ >EQ %]
1335	#lb #l @(list_elim_left … l …) normalize nodelta
1336	[1,3,5,7,9,11: #_ #EQlb @eq_identifier_elim
1337	[1,3,5,7,9,11: #EQ destruct(EQ) #_ @⊥ \|: #_ ]
1338	lapply(fresh_labs lbl) >EQlb *** #H #_ #_ @H
1339	@(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
1340	whd in match code_has_point; normalize nodelta >EQstmt @I ]
1341	#last #pre #_ #_ #EQlbl >(split_on_last_append … (lb::pre) last)
1342	normalize nodelta @eq_identifier_elim
1343	[2,4,6,8,10,12: #_ *] #EQ lapply EQlbl destruct(EQ) #EQlbl #_ @⊥
1344	lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); * #_ #H lapply(append_All … H) -H
1345	* #_ whd in ⊢ (% → ?); *** #H #_ #_ @H -H @(code_is_in_universe … (pi2 ?? fn))
1346	whd in match code_has_label; whd in match code_has_point; normalize nodelta
1347	>EQstmt @I
1348	qed.
1349
1350	lemma append_absurd : ∀A : Type[0]. ∀l : list A. ∀ a : A.
1351	l @ [a] = [ ] → False.
1352	#A * [2: #x #y] #a normalize #EQ destruct
1353	qed.
1354
1355	lemma last_append_eq : ∀A : Type[0].∀l1,l2 : list A. ∀a1,a2: A.
1356	l1 @ [a1] = l2 @ [a2] → a1 = a2.
1357	#A #l1 elim l1 [ * [2: #hd #tl] #a1 #a2 normalize #EQ destruct [2: %]
1358	@⊥ lapply(sym_eq ??? e0) -e0 #e0 @(append_absurd ??? e0)] #hd #tl #IH
1359	* [ #a1 #a2 normalize #EQ destruct @⊥ @(append_absurd ??? e0)]
1360	#hd1 #tl1 #a1 #a2 normalize #EQ destruct(EQ) @(IH tl1 a1 a2 e0)
1361	qed.
1362
1363
1364	lemma get_sigma_last :
1365	∀prog : ertl_program.
1366	∀ f_lbls,f_regs.
1367	∀f_bl_r.
1368	b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1369	(λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
1370	∀id,fn,bl,pt,stmt,pre,last.
1371	fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
1372	stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt →
1373	f_lbls bl pt = pre@[last] → get_sigma prog f_lbls bl last = return pt.
1374	#prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #pre #last
1375	#EQfn #EQstmt #EQlabels
1376	cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
1377	#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
1378	[2: #x #y ] normalize nodelta #EQ destruct(EQ) #_ #_ #_ #_ #pp_labs
1379	#_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H normalize nodelta
1380	cases stmt in EQstmt; normalize nodelta
1381	[3: *
1382	\|2: * [#lbl \|\| ] #EQstmt whd in ⊢ (%→ ?); #bl *
1383	\|: [#c \| * [ #c_id \| #c_ptr] #args #dest \| #r #lbl \| #seq ] #nxt #EQstmt
1384	>if_merge_right [2,4,6,8,10: %] whd in ⊢ (% → ?); * #bl *
1385	]
1386	whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta
1387	[2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y #_] #_ *\|10: #r #tl #_] #EQregs
1388	[ whd in ⊢ (% → ?); cases tl in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs]
1389	#EQbl destruct(EQbl) whd in ⊢ (%→?); [2,3: * #pref * #mid *\|: * #l1 * #mid1 * #mid2 * #l2 ***]
1390	#EQmid1 whd in ⊢ (% → ?);
1391	[1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
1392	[3,4,5,6: whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt #EQ destruct(EQ) ]
1393	whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ >EQlabels in e0; #e0 @(append_absurd ??? e0)]
1394	* #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
1395	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1396	* #mid3 * #rest1 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
1397	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1398	* #mid4 * #rest2 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
1399	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1400	* #mid5 * #rest3 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
1401	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1402	* #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQcall
1403	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1404	* #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
1405	>e0 in EQlabels; #EQlabels whd in match get_sigma; normalize nodelta
1406	>code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
1407	inversion(find ????)
1408	[ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >e0
1409	normalize nodelta @eq_identifier_elim [ #_ ] #H #_ @H
1410	>(last_append_eq ????? EQlabels) % ]
1411	* #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
1412	inversion(f_lbls ??)
1413	[ #EQlbl normalize nodelta @eq_identifier_elim [2: #_ *] #EQ destruct(EQ)
1414	lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ) @⊥
1415	lapply(fresh_labs pt) >e0 * #_ * #_ * #_ *** #H #_ #_ @H -H
1416	@(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
1417	whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
1418	>(find_lookup ?????? EQfind) @I
1419	]
1420	#lb #labels #_ @(list_elim_left … (labels) …) -labels normalize nodelta
1421	[2: #last1 #pre #_] #EQl [ >(split_on_last_append … (lb::pre) last1) ]
1422	normalize nodelta @eq_identifier_elim [2,4: #_ *] #EQ destruct(EQ) #_
1423	lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ)
1424	lapply pp_labs whd in match partial_partition; normalize nodelta * #_ #H
1425	lapply(H lbl pt) >e0 whd in EQmid : (??%%); >EQl
1426	#H [ >(H last1 ? ?) \| >(H lb ? ?) ] [1,4: %
1427	\|6: whd in match (memb ???); @if_elim [#_ @I]
1428	#H lapply(Prop_notb ? H) * -H #H @⊥ @H cases lb #x normalize
1429	@if_elim [#_ %] #H lapply(Prop_notb ? H) * -H #H @H >(eqb_n_n x) %
1430	\|5: >(memb_append_l2 ? lb ? [lb] ?) /2 by /
1431	\|*: >(memb_append_l2 ? last1 ? [last1] ?) /2 by /
1432	@Exists_memb %2 elim pre [ % % \| #hd #tl #IH %2 @IH]
1433	]
1434	qed.
1435
1436
1437	lemma fetch_call_commute :
1438	∀prog : ertl_program.
1439	let trans_prog ≝ ertl_to_ertlptr prog in
1440	∀ f_lbls,f_regs.
1441	∀f_bl_r.
1442	b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1443	(λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
1444	∀id,fn,c_id,c_args,c_dest,nxt,pc.
1445	fetch_statement ERTL_semantics
1446	(prog_var_names … prog) (globalenv_noinit … prog) pc =
1447	return 〈id,fn, sequential ? ?(CALL ERTL_semantics ? c_id c_args c_dest) nxt〉 →
1448	∃fn',pc'. sigma_stored_pc prog f_lbls pc' = pc ∧
1449	fetch_statement ERTLptr_semantics
1450	(prog_var_names … trans_prog) (globalenv_noinit … trans_prog) pc' =
1451	return 〈id,fn', sequential ? ?(CALL ERTLptr_semantics ? c_id c_args c_dest) nxt〉.
1452	#prog #f_lbls #f_regs #f_bl_r #good #id #fn * [ #c_id \| #c_ptr ] #c_args #c_dest
1453	#nxt #pc #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
1454	cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
1455	#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
1456	[2,4: #x #y ] normalize nodelta #EQ destruct(EQ) #_ #_ #_ #_ #_
1457	#_ #_ #_ #_ #_ #H cases(H … EQstmt) -H #bl whd in ⊢ (% → ?); *
1458	>if_merge_right [2,4: %] whd in match translate_step;
1459	normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta
1460	[\|2,3:[ #x #y #_] #_ * \|4: #r #tl #_ ] #EQregs
1461	[ \| cases tl in EQregs; [2: #x #y #_ *] #EQregs whd in ⊢ (% → ?);] #EQ destruct(EQ)
1462	whd in ⊢ (% → ?); * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
1463	[2: * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
1464	* #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1465	whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 *
1466	#EQpush1 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1467	whd in ⊢ (% → ?); * #mid4 * #rest2 ** #EQ destruct(EQ) * #nxt1 * #EQhigh
1468	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1469	* #mid5 * #rest3 ** #EQ destruct(EQ) * #nxt1 * #EQpush2
1470	change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1471	] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
1472	whd in ⊢ (% → ?); * #nxt1 * #EQcall #EQ destruct(EQ) whd in ⊢ (% → ?);
1473	* #EQ destruct(EQ) change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1474	%{calling'}
1475	[ %{(pc_of_point ERTLptr_semantics (pc_block pc) mid1)}
1476	\| %{pc}
1477	] %
1478	[1,3: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
1479	@eqZb_elim change with (pc_block pc) in match (pc_block ?) in ⊢ (% → ?);
1480	[1,3: #EQbl >fetch_internal_function_no_minus_one in EQfn; try assumption
1481	#EQ destruct(EQ)] #_ normalize nodelta
1482	[2: >(get_sigma_idempotent … good … EQfn EQstmt EQ)
1483	\|*: change with (pc_block pc) in match (pc_block ?);
1484	>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt e0)
1485	] >m_return_bind normalize nodelta >pc_of_point_of_pc %
1486	\|*: whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind
1487	[>point_of_pc_of_point ] >EQcall %
1488	]
1489	qed.
1490
1491
1492
1493	lemma next_of_call_pc_ok : ∀prog : ertl_program.
1494	let trans_prog ≝ ertl_to_ertlptr prog in
1495	∀ f_lbls,f_regs.∀f_bl_r.
1496	b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1497	(λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
1498	∀pc,lb.
1499	next_of_call_pc ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
1500	pc = return lb →
1501	∃pc'. sigma_stored_pc prog f_lbls pc' = pc ∧
1502	next_of_call_pc ERTLptr_semantics (prog_var_names … trans_prog)
1503	(globalenv_noinit … trans_prog) pc' = return lb.
1504	#prog #f_lbls #f_regs #f_bl_r #good #pc #lb whd in match next_of_call_pc;
1505	normalize nodelta #H @('bind_inversion H) -H ** #id #fn
1506	* [ [ #c \| #c_id #c_arg #c_dest \| #reg #lbl \| #seq ] #prox \| #fin \| ]
1507	#EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1508	cases(fetch_call_commute … good … EQfetch) #fn1 * #pc1 * #EQpc1 #EQt_fetch
1509	%{pc1} % [assumption] >EQt_fetch %
1510	qed.
1511
1512	lemma next_of_call_pc_error : ∀pars.∀prog : program ? ℕ. ∀init,pc.
1513	(block_id (pi1 … (pc_block pc)) = 0 ∨ block_id (pi1 … (pc_block pc)) = -1) →
1514	next_of_call_pc pars (prog_var_names … prog) (globalenv … init prog)
1515	pc = Error ? [MSG BadFunction].
1516	#pars #prg #init #pc * #EQ whd in match next_of_call_pc; normalize nodelta
1517	whd in match fetch_statement; normalize nodelta
1518	[ >fetch_internal_function_no_zero \| >fetch_internal_function_no_minus_one]
1519	//
1520	qed.
1521
1522	lemma next_of_call_pc_inv : ∀pars.∀prog : program ? ℕ. ∀init.
1523	∀pc,nxt.
1524	next_of_call_pc pars (prog_var_names … prog)
1525	(globalenv … init prog) pc = return nxt →
1526	∃id,fn,c_id,c_args,c_dest.
1527	fetch_statement pars
1528	(prog_var_names … prog) (globalenv … init prog) pc =
1529	return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉.
1530	#pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta
1531	#H @('bind_inversion H) -H ** #id #fn *
1532	[ *[ #c \| #c_id #c_arg #c_dest \| #reg #lbl \| #seq ] #prox \| #fin \| #H #r #l #l ]
1533	#EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1534	%{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption
1535	qed.
1536
1537	lemma sigma_stored_pc_inj : ∀ prog : ertl_program.
1538	∀f_lbls,pc,pc'. sigma_pc_opt prog f_lbls pc ≠ None ? →
1539	sigma_pc_opt prog f_lbls pc = sigma_pc_opt prog f_lbls pc' →
1540	pc = pc'.
1541	#prog #f_lbls #id #EQblid #off #id' #EQblid' #off'
1542	* inversion(sigma_pc_opt ???) [#_ #H @⊥ @H %]
1543	#pc1 whd in match sigma_pc_opt; normalize nodelta @if_elim
1544	[ @eqZb_elim [2: #_ ] #EQbl whd in ⊢ (??%? → ?); #EQ destruct #_
1545	#H lapply(sym_eq ??? H) -H @if_elim [#_ whd in ⊢ (??%? → ?); #EQ destruct %]
1546	@eqZb_elim [ #_ ] #EQbl' #_ #H @('bind_inversion H) -H #lb #EQlb
1547	whd in ⊢ (??%? → ?); #EQ destruct @⊥ @EQbl' assumption] @eqZb_elim [#_ ] #EQbl #_
1548	#H @('bind_inversion H) -H * #lb #EQlb whd in ⊢ (??%? → ?); #EQ destruct #_
1549	#H lapply(sym_eq ??? H) -H @if_elim
1550	[ @eqZb_elim [2: #_ *] #EQbl' #_ whd in ⊢ (??%? → ?); #EQ destruct @⊥ @EQbl @EQbl']
1551	#_ #H @('bind_inversion H) -H * #lb' #EQlb' whd in ⊢ (??%? → ?);
1552	whd in match (pc_of_point ???); whd in match (offset_of_point ??);
1553	whd in match (offset_of_point ??); #EQ destruct @eq_f
1554	cut(an_identifier LabelTag off = an_identifier LabelTag off') [2: #EQ destruct %]
1555	@(partial_inj_sigma prog f_lbls id) [>EQlb % #ABS destruct \| >EQlb >EQlb' %]
1556	qed.
1557
1558	lemma bool_of_beval_ok : ∀prog : ertl_program.
1559	∀f_lbls. preserving1 … res_preserve1 …
1560	(sigma_beval prog f_lbls)
1561	(λx.x)
1562	(bool_of_beval)
1563	(bool_of_beval).
1564	#prog #f_lbls * [ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
1565	whd in match bool_of_beval; normalize nodelta try @res_preserve_error1
1566	try @mfr_return1 whd in match sigma_beval; normalize nodelta
1567	cases (sigma_pc_opt ???) normalize nodelta [2: #pc] @res_preserve_error1
1568	qed.
1569
1570
1571	lemma block_of_call_ok : ∀prog: ertl_program.
1572	let trans_prog ≝ ertl_to_ertlptr prog in
1573	∀ f_lbls,f_regs.
1574	∀called,restr. preserving1 … res_preserve1 …
1575	(sigma_state prog f_lbls f_regs restr)
1576	(λx.x)
1577	(block_of_call ERTL_semantics (prog_var_names … prog)
1578	(globalenv_noinit … prog) called)
1579	(block_of_call ERTLptr_semantics (prog_var_names … trans_prog)
1580	(globalenv_noinit … trans_prog) called).
1581	#prog #f_lbls #f_regs #called #restr #st whd in match block_of_call; normalize nodelta
1582	@mfr_bind1
1583	[ @(λx.x)
1584	\| cases(called) [#c_id \| #c_ptr] normalize nodelta
1585	[ @opt_to_res_preserve1 #bl #EQbl %{bl} % [2: %]
1586	>(find_symbol_transf …
1587	(λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog c_id)
1588	assumption
1589	\| @mfr_bind1
1590	[2: whd in match dpl_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) \|
1591	\| #bv1 @mfr_bind1
1592	[2: whd in match dph_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) \|
1593	\| #bv2 @mfr_bind1
1594	[ @(λx.x)
1595	\| whd in match pointer_of_bevals; normalize nodelta
1596	cases bv1 normalize nodelta
1597	[ \| \| #ptr1 #ptr2 #p \| #by \| #p \| #ptr #p \| #pc1 #p1]
1598	try @res_preserve_error1
1599	[ cases bv2 [ \| \| #ptr1' #ptr2' #p' \| #by' \| #p' \| #ptr' #p' \| #pc1' #p1']
1600	normalize nodelta
1601	[1,2,3,4,5: @res_preserve_error1
1602	\| @if_elim #_ [@mfr_return_eq1 % \| @res_preserve_error1]
1603	]
1604	] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
1605	normalize nodelta [2,4: #pc ] @res_preserve_error1
1606	\|
1607	#ptr @if_elim #_ [@mfr_return_eq1 % \| @res_preserve_error1]
1608	]
1609	]
1610	]
1611	]
1612	\| #bl @opt_to_res_preserve1 whd in match code_block_of_block; normalize nodelta
1613	@match_reg_elim [ #_ @opt_preserve_none1 \| #prf @mfr_return_eq1 %]
1614	]
1615	qed.
1616
1617	lemma bvpc_sigma_pc_to_sigma_beval : ∀prog : ertl_program.
1618	∀f_lbls,pc,p. sigma_pc_opt prog f_lbls pc ≠ None ? →
1619	BVpc (sigma_stored_pc prog f_lbls pc) p =
1620	sigma_beval prog f_lbls (BVpc pc p).
1621	#prog #f_lbls #pc #p #prf whd in match sigma_stored_pc;
1622	whd in match sigma_beval; normalize nodelta lapply prf
1623	cases(sigma_pc_opt ???) [ * #H @⊥ @H % \| #pc' #_ % ]
1624	qed.
1625
1626	lemma push_ra_ok : ∀prog : ertl_program.
1627	∀f_lbls,f_regs,restr,pc. sigma_pc_opt prog f_lbls pc ≠ None ? →
1628	preserving1 ?? res_preserve1 …
1629	(sigma_state prog f_lbls f_regs restr)
1630	(sigma_state prog f_lbls f_regs restr)
1631	(λst.push_ra ERTL_semantics st (sigma_stored_pc prog f_lbls pc))
1632	(λst.push_ra ERTLptr_semantics st pc).
1633	#prog #f_lbls #f_regs #restr #pc #prf #st whd in match push_ra; normalize nodelta
1634	@mfr_bind1
1635	[ @(sigma_state prog f_lbls f_regs restr)
1636	\| >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok
1637	\| #st' >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok
1638	] qed.
1639
1640
1641	lemma ertl_save_frame_ok : ∀prog : ertl_program.
1642	∀f_lbls.∀f_regs : regs_funct.∀kind,restr.
1643	preserving1 ?? res_preserve1 ????
1644	(λst : Σs: state_pc ERTLptr_semantics.
1645	sigma_pc_opt prog f_lbls (pc … s) ≠ None ?
1646	. match fetch_internal_function … (globalenv_noinit … prog)
1647	(pc_block (pc … st)) with
1648	[ OK y ⇒ let 〈f,fn〉 ≝ y in
1649	let added ≝ added_registers … (prog_var_names … prog) fn
1650	(f_regs (pc_block (pc … st))) in
1651	mk_state_pc ? (sigma_state prog f_lbls f_regs added st)
1652	(sigma_stored_pc prog f_lbls (pc … st))
1653	(sigma_stored_pc prog f_lbls (last_pop … st))
1654	\| Error e ⇒ dummy_state_pc
1655	])
1656	(sigma_state prog f_lbls f_regs restr)
1657	(ertl_save_frame kind it)
1658	(match kind with
1659	[ID ⇒ ertlptr_save_frame kind it
1660	\|PTR ⇒ λst. !st' ← push_ra … st (pc … st);
1661	ertlptr_save_frame kind it (set_no_pc … st' st)
1662	]).
1663	#prog #f_lbls #f_regs * #restr * #st #st_prf
1664	inversion(fetch_internal_function ???) normalize nodelta
1665	[1,3: * #f #fn #EQfn normalize nodelta whd in match ertl_save_frame; whd in match ertlptr_save_frame;
1666	normalize nodelta @mfr_bind1
1667	[2,5: @push_ra_ok [1,2: assumption] \|1,4: skip
1668	\|*: #st1 [ >m_return_bind] @mfr_bind_inversion1
1669	[1,4: @(λf.match sigma_frames_opt prog f_lbls f_regs f with [Some g ⇒ g \| None ⇒ [ ]])
1670	\|2,5: @opt_to_res_preserve1 whd in match sigma_state; whd in match set_no_pc;
1671	normalize nodelta cases(st_frms … st1) [1,3: @opt_preserve_none1]
1672	#frames #frames1 whd in match sigma_frames; normalize nodelta
1673	>m_return_bind #EQframes %{frames} % [%] >EQframes %
1674	\|*: #frames #H lapply(opt_eq_from_res ???? H) -H whd in match sigma_state;
1675	normalize nodelta #EQt_frames #H lapply(opt_eq_from_res ???? H) -H
1676	whd in match set_no_pc; normalize nodelta #EQframes >EQframes in EQt_frames;
1677	whd in match sigma_frames; normalize nodelta >m_return_bind
1678	inversion(sigma_frames_opt ???) [1,3: #_ #ABS destruct(ABS)]
1679	#t_frames #EQt_frames #_ @mfr_return_eq1 normalize nodelta @eq_f
1680	whd in match set_frms; normalize nodelta >m_return_bind
1681	cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,f1,f2.
1682	a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 → f1 = f2 →
1683	mk_state ERTL_semantics a1 b1 c1 d1 e1 f1 =
1684	mk_state ERTL_semantics a2 b2 c2 d2 e2 f2)
1685	[1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
1686	#H15 #H16 #H17 #H18 //] #APP @APP try %
1687	[1,3: whd in match sigma_frames_opt; whd in match m_list_map;
1688	normalize nodelta whd in match (foldr ?????); normalize nodelta
1689	>EQfn >m_return_bind normalize nodelta
1690	change with (sigma_frames_opt prog f_lbls f_regs frames)
1691	in match (foldr ?????);
1692	>EQt_frames >m_return_bind whd in match sigma_regs;
1693	normalize nodelta cases(regs … st1) #ps_reg #hw_reg
1694	>(pc_block_eq … st_prf) %
1695	\|*: whd in match set_regs; whd in match sigma_regs; normalize nodelta
1696	cases(regs … st1) #ps_r #hw_r normalize nodelta
1697	whd in match sigma_register_env; normalize nodelta
1698	@eq_f2 // change with (empty_map RegisterTag beval) in match (map RegisterTag ????);
1699	<(empty_set_minus … restr) %
1700	]
1701	]
1702	]
1703	\|*: #e #_ #x whd in match ertl_save_frame; normalize nodelta normalize nodelta
1704	#H @('bind_inversion H) -H #y whd in match push_ra; normalize nodelta
1705	#H @('bind_inversion H) -H #z whd in match push; normalize nodelta
1706	whd in match (istack ??); whd in match is_push; normalize nodelta
1707	>m_return_bind whd in match set_istack; normalize nodelta whd in ⊢ (??%% →?);
1708	#EQ destruct(EQ) normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
1709	#EQ destruct(EQ) whd in match (st_frms ??); whd in ⊢ (??%% → ?);
1710	#EQ destruct(EQ)
1711	]
1712	qed.

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

Download in other formats:

Original Format