Context Navigation

ERTLptrToLTLProof.ma @ 3393

Last change on this file since 3393 was 3254, checked in by sacerdot, 8 years ago
Code I always forgot to commit. To be ported to ERTLtoLTLProof.ma.
File size: 40.4 KB

Line
1	include "ERTLptr/ERTLptrToLTL.ma".
2	include "ERTLptr/ERTLptr_semantics.ma".
3	include "LTL/LTL_semantics.ma".
4	include "joint/Traces.ma".
5	include "common/StatusSimulation.ma".
6	include "common/AssocList.ma".
7
8	(* Inefficient, replace with Trie lookup *)
9	definition lookup_stack_cost ≝
10	λp.λid : ident.
11	assoc_list_lookup ? ℕ id (eq_identifier …) p.
12
13	(TO BE MOVED)
14	definition ERTLptr_status ≝
15	λprog : ertlptr_program.λstack_sizes.
16	joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
17
18	definition LTL_status ≝
19	λprog : ltl_program.λstack_sizes.
20	joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
21
22	definition local_clear_sb_type ≝ decision → bool.
23	definition clear_sb_type ≝ label → local_clear_sb_type.
24
25	axiom to_be_cleared_sb :
26	∀live_before : valuation register_lattice. coloured_graph live_before → clear_sb_type.
27
28	definition local_clear_fb_type ≝ vertex → bool.
29	definition clear_fb_type ≝ label → local_clear_fb_type.
30
31	axiom to_be_cleared_fb :
32	∀live_before : valuation register_lattice.clear_fb_type.
33
34	axiom sigma_fb_state:
35	ertlptr_program → local_clear_fb_type →
36	state ERTLptr_semantics → state ERTLptr_semantics.
37
38	axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program.
39	∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog). ∀l.
40	let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in
41	¬ lives (inr ? ? RegisterA) (livebefore … fn after l).
42
43	axiom dead_registers_in_dead :
44	∀fix_comp.∀build : coloured_graph_computer.
45	∀prog : ertlptr_program.
46	∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
47	∀l.
48	let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in
49	let coloured_graph ≝ build … fn after in
50	∀R : Register.
51	¬ lives (inr ? ? R) (livebefore … fn after l) →
52	to_be_cleared_sb … coloured_graph l R.
53
54	axiom sigma_sb_state:
55	ertlptr_program → local_clear_sb_type → state LTL_semantics → state ERTLptr_semantics.
56
57	definition dummy_state : state ERTLptr_semantics ≝
58	mk_state ERTL_semantics
59	(None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
60
61	definition dummy_state_pc : state_pc ERTLptr_semantics ≝
62	mk_state_pc ? dummy_state (null_pc one) (null_pc one).
63
64
65	definition sigma_fb_state_pc :
66	fixpoint_computer → ertlptr_program →
67	state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
68	λfix_comp,prog,st.
69	let ge ≝ globalenv_noinit … prog in
70	let globals ≝ prog_var_names … prog in
71	match fetch_internal_function … ge (pc_block (pc … st)) with
72	[ OK y ⇒
73	let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
74	let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
75	let before ≝ livebefore … (\snd y) after in
76	mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb before pt) st) (pc … st)
77	(last_pop … st)
78	\| Error e ⇒ dummy_state_pc
79	].
80
81	include "joint/StatusSimulationHelper.ma".
82
83	definition sigma_sb_state_pc:
84	fixpoint_computer → coloured_graph_computer →
85	ertlptr_program → lbl_funct → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
86	λfix_comp,build,prog,f_lbls,st.
87	let ge ≝ globalenv_noinit … prog in
88	let globals ≝ prog_var_names … prog in
89	match fetch_internal_function … ge (pc_block (pc … st)) with
90	[ OK y ⇒
91	let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
92	let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
93	let coloured_graph ≝ build … (\snd y) after in
94	mk_state_pc ? (sigma_sb_state prog
95	(to_be_cleared_sb … coloured_graph pt) st) (pc … st)
96	(sigma_stored_pc ERTLptr_semantics LTL_semantics
97	prog f_lbls (last_pop … st))
98	\| Error e ⇒ dummy_state_pc
99	].
100
101	definition state_rel : fixpoint_computer → coloured_graph_computer →
102	ertlptr_program →
103	(Σb:block.block_region b = Code) → label → state ERTL_state → state LTL_LIN_state → Prop ≝
104	λfix_comp,build,prog,bl,pc,st1,st2.
105	∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
106	let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
107	let before ≝ livebefore … fn after in
108	let coloured_graph ≝ build … fn after in
109	(sigma_fb_state prog (to_be_cleared_fb before pc) st1) =
110	(sigma_sb_state prog (to_be_cleared_sb … coloured_graph pc) st2).
111
112	axiom write_decision :
113	decision → beval → state LTL_LIN_state → state LTL_LIN_state.
114
115	axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval.
116
117	axiom insensitive_to_be_cleared_sb :
118	∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
119	∀d : decision.∀bv.tb d →
120	sigma_sb_state prog tb st =
121	sigma_sb_state prog tb (write_decision d bv st).
122
123
124	definition ERTLptr_to_LTL_StatusSimulation :
125	∀fix_comp : fixpoint_computer.
126	∀colour : coloured_graph_computer.
127	∀ prog : ertlptr_program.
128	∀ f_lbls, f_regs. ∀f_bl_r.
129	b_graph_transform_program_props ERTLptr_semantics LTL_semantics
130	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
131	let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
132	let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
133	let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
134	let stacksizes ≝ lookup_stack_cost … m in
135	status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝
136	λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r.λgood.
137	mk_status_rel ??
138	(* sem_rel ≝ *)
139	(λs1:ERTLptr_status ? ?
140	.λs2:LTL_status ? ?
141	.sigma_fb_state_pc fix_comp prog s1
142	=sigma_sb_state_pc fix_comp colour prog f_lbls s2)
143	(* call_rel ≝ *)
144	(λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
145	.λs2:Σs:LTL_status ??.as_classifier ? s cl_call
146	.pc ? s1 =sigma_stored_pc ERTLptr_semantics LTL_semantics
147	prog f_lbls (pc ? s2))
148	(* sim_final ≝ *) ?.
149	cases daemon
150	qed.
151
152	axiom as_label_ok :
153	∀fix_comp,colour.
154	∀prog.∀f_lbls,f_regs. ∀f_bl_r.
155	∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
156	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
157	∀st1,st2,fn,id,stmt.
158	let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
159	R st1 st2 →
160	fetch_statement ERTLptr_semantics (prog_var_names … prog)
161	(globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
162	as_label ? st2 = as_label ? st1.
163
164	(*
165	(* Copy the proof too from previous pass *)
166	axiom fetch_stmt_ok_sigma_state_ok :
167	∀prog : ertlptr_program.
168	∀ f_lbls,f_regs,id,fn,stmt,st.
169	fetch_statement ERTLptr_semantics (prog_var_names … prog)
170	(globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) =
171	return 〈id,fn,stmt〉 →
172	let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn
173	(f_regs (pc_block (pc … st)))) in
174	st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) =
175	sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
176	*)
177
178	axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
179	∀prog.∀ f_lbls,f_regs.∀f_bl_r.
180	∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
181	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
182	∀st1,st2.
183	let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
184	R st1 st2 →
185	pc_block (pc … st1) = pc_block (pc … st2).
186
187	axiom pc_eq_sigma_commute : ∀fix_comp,colour.
188	∀prog.∀ f_lbls,f_regs.∀f_bl_r.
189	∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
190	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
191	∀st1,st2,f,fn.
192	fetch_internal_function ? (globalenv_noinit … prog)
193	(pc_block (pc … st1)) = return 〈f,fn〉 →
194	let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
195	R st1 st2 →
196	(pc … st1) = (pc … st2).
197
198	(*
199	axiom change_pc_sigma_commute : ∀fix_comp,colour.
200	∀prog.∀ f_lbls,f_regs.∀f_bl_r.
201	∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
202	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
203	∀st1,st2.
204	let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
205	R st1 st2 →
206	∀pc1,pc2.pc1 = pc2 →
207	R (set_pc … pc1 st1) (set_pc … pc2 st2).
208
209	axiom globals_commute : ∀fix_comp,colour.
210	∀prog.
211	∀p_out,m,n.
212	∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
213	prog_var_names … prog = prog_var_names … p_out.
214
215	lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
216	〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
217	#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
218	qed.*)
219
220	include "joint/semantics_blocks.ma".
221	include "ASM/Util.ma".
222
223	axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
224	∀st : state LTL_LIN_state.
225	hw_reg_retrieve (regs … (write_decision r bv st)) r = return bv.
226
227	axiom move_spec : ∀prog.∀stack_size.∀localss : nat.
228	∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
229	∀f : ident.
230	∀s : state LTL_LIN_state.
231	repeat_eval_seq_no_pc (mk_prog_params LTL_semantics prog stack_size) f
232	(move (prog_var_names … prog) localss carry_lives_after dest src) s =
233	return write_decision dest (read_arg_decision src s) s.
234
235	axiom sigma_beval:
236	ertlptr_program → (block → label → list label) → beval → beval.
237
238
239	axiom ps_reg_retrieve_hw_reg_retrieve_commute :
240	∀fix_comp,colour,prog.
241	∀ f_lbls,f_regs.∀f_bl_r.
242	∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
243	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
244	∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
245	let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
246	let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
247	∀st1 : state_pc ERTL_state.
248	∀st2 : state_pc LTL_LIN_state.
249	∀bv.
250	∀r : register.R st1 st2 →
251	lives (inl ? ? r) (livebefore … fn after (point_of_pc ERTLptr_semantics (pc … st1))) →
252	ps_reg_retrieve (regs … st1) r = return bv →
253	∃bv'.bv = sigma_beval prog f_lbls bv' ∧
254	read_arg_decision
255	(colouring … (colour (prog_var_names … prog) fn after)
256	(inl register Register r))
257	st2 = bv'.
258
259	axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).
260	axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
261	axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
262	set_member A DEC a (set_union … x y).
263	axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
264	set_member A DEC a (set_union … x y).
265	axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
266	¬set_member A DEC a y →
267	set_member A DEC a (set_diff … x y).
268
269	lemma all_used_are_live_before :
270	∀fix_comp.
271	∀prog : ertlptr_program.
272	∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
273	∀l,stmt.
274	stmt_at … (joint_if_code … fn) l = return stmt →
275	∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
276	let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
277	eliminable ? (after l) stmt = false →
278	lives (inl ? ? r) (livebefore … fn after l).
279	#fix_comp #prog #fn #l *
280	[ * [#c\|* [#c_id \| #c_ptr] #args #dest \| #a #lbl \| *
281	[ #str
282	\| * * [#r1 \| #R1] * [1,3: * [1,3: #r \|2,4: #R] \|2,4: #b]
283	\| #a
284	\| * [ #r \| #b]
285	\| #i #i_spec #dpl #dph
286	\| #op #a #b * [#r \| #by] * [1,3: #r'\|2,4: #by']
287	\| #op #a #a'
288	\| * #a #a' * [1,3,5,7,9,11: #r \|2,4,6,8,10,12: #b]
289	\|
290	\|
291	\| #a #dpl #dph
292	\| #dpl #dph #a
293	\| * [ * [\|\| #r] \| #r #lbl \| #r #lbl ]
294	]
295	] #nxt\| * [ #lbl \| \| ] \|]
296	#EQstmt #r #H #H1 whd in match (lives ??); normalize nodelta
297	whd in match (livebefore ????); whd in EQstmt : (??%?); >EQstmt
298	normalize nodelta -EQstmt whd in match (statement_semantics ???);
299	whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
300	normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
301	qed.
302
303	axiom bool_of_beval_sigma_commute :
304	∀prog.∀f_lbls.∀bv,b.
305	bool_of_beval (sigma_beval prog f_lbls bv) = return b →
306	bool_of_beval bv = return b.
307
308	lemma map_eval_add_dummy_variance_id :
309	∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
310	#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
311	qed.
312
313	lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
314	st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
315	pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
316	#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
317	%{(refl …)} %{(refl …)} %
318	qed.
319
320	(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
321	lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
322	∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
323	#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
324	whd in ⊢ (??%? → ?); #EQ >EQ %
325	qed.
326
327	lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
328	OptPred True (λres.
329	split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
330	(split_on_last … l2).
331	#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
332	#hd #tl #IH #l1 whd >split_on_last_append_singl whd
333	<associative_append @split_on_last_append_singl
334	qed.
335
336	lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
337	#A #a #b #EQ destruct %
338	qed.
339
340	lemma eq_notb_true_to_eq_false:
341	∀b. (¬b) = true → b = false.
342	* // #abs normalize in abs; destruct
343	qed.
344
345	axiom sigma_fb_state_insensitive_to_dead_reg:
346	∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label.
347	∀r: register. ∀before.
348	set_member … (eq_identifier RegisterTag) r (\fst (before l)) = false →
349	sigma_fb_state prog
350	(to_be_cleared_fb before l)
351	(set_regs ERTLptr_semantics
352	〈reg_store r bv (\fst (regs ERTLptr_semantics st)),
353	\snd (regs ERTLptr_semantics st)〉 st)
354	= sigma_fb_state prog (to_be_cleared_fb before l) st.
355
356	axiom sigma_fb_state_insensitive_to_dead_Reg:
357	∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label.
358	∀r: Register. ∀before.
359	set_member … eq_Register r (\snd (before l)) = false →
360	sigma_fb_state prog
361	(to_be_cleared_fb before l)
362	(set_regs ERTLptr_semantics
363	〈\fst (regs ERTLptr_semantics st),
364	hwreg_store r bv (\snd (regs ERTLptr_semantics st))〉
365	st)
366	= sigma_fb_state prog (to_be_cleared_fb before l) st.
367
368	axiom sigma_fb_state_insensitive_to_dead_carry:
369	∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label. ∀before.
370	set_member Register eq_Register RegisterCarry (\snd (before l)) = false →
371	sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTLptr_semantics bv st) =
372	sigma_fb_state prog (to_be_cleared_fb before l) st.
373
374	lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
375	** normalize #abs destruct /2/
376	qed.
377
378	lemma eta_set_carry:
379	∀P,st. set_carry P (carry P st) st = st.
380	#P * //
381	qed.
382
383	lemma set_carry_set_regs_commute:
384	∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
385	#P * //
386	qed.
387
388	lemma eliminable_step_to_eq_livebefore_liveafter:
389	∀prog,stackcost,fn.
390	let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
391	∀st1: joint_abstract_status p_in.
392	∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
393	let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
394	stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
395	∀liveafter.
396	eliminable_step (globals p_in) (liveafter (point_of_pc ERTLptr_semantics (pc … st1))) stms = true →
397	livebefore … fn liveafter pt = liveafter pt.
398	#prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim
399	whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
400	normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
401	#stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
402	whd in match eliminable; normalize nodelta >Helim %
403	qed.
404
405	lemma sigma_fb_state_insensitive_to_eliminable:
406	∀fix_comp: fixpoint_computer.
407	∀prog: ertlptr_program.
408	∀stackcost.
409	let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
410	∀f,fn.
411	∀after: valuation ?.
412	let before ≝ livebefore … fn after in
413	∀st1 : joint_abstract_status p_in.
414	let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
415	∀st1_no_pc. ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
416	stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) →
417	∀Heval_seq_no_pc:
418	eval_seq_no_pc ERTLptr_semantics
419	(prog_var_names (joint_function ERTLptr_semantics) ℕ prog)
420	(ev_genv
421	(mk_prog_params ERTLptr_semantics prog stackcost))
422	f stms (st_no_pc … st1)
423	=return st1_no_pc.
424	∀Heliminable:
425	eliminable_step (globals p_in)
426	(after (point_of_pc ERTLptr_semantics (pc p_in st1))) stms =true.
427	sigma_fb_state prog (to_be_cleared_fb before pt) st1_no_pc =
428	sigma_fb_state prog (to_be_cleared_fb before pt) (st_no_pc … st1).
429	#fix_comp #prog #stackcost letin p_in ≝ (mk_prog_params ???) #f #fn #after
430	#st1 #st1' #stms #next #stmt_at #Heval #Helim
431	lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim)
432	#EQ_livebefore_after -next
433	cases stms in Heval Helim;
434	try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
435	try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
436	try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
437	try (#arg1 #Heval #Helim) try (#Heval #Helim)
438	whd in Heval:(??%?);
439	whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim))
440	[7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] \|*: #arg2 #arg3 ] #Harg1
441	normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?);
442	try (change with (false=true) in Helim; destruct (Helim))
443	[4,8: cases arg1 in Heval Helim; normalize nodelta
444	[ * normalize nodelta #arg10 #arg11] #Heval #Helim]
445	lapply (eq_notb_true_to_eq_false ? Helim) -Helim #Helim
446	[1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?);
447	[1,3: whd in match (pair_reg_move_ ?????); normalize nodelta
448	inversion ps_reg_retrieve normalize nodelta
449	[2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ]
450	#bv #EQbv ]
451	\|3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval;
452	[2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
453	#bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
454	#v1 * #Hv1 #X cases (bind_inversion ????? X) -X
455	#vres * #Hvres #X cases (bind_inversion ????? X) -X
456	#st1'' * #Hst1''
457	\|9: inversion (opt_to_res ???) in Heval;
458	[2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
459	#bv normalize nodelta #EQbv
460	\|10,11: inversion (get_pc_from_label ?????) in Heval;
461	[2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
462	#bv normalize nodelta #EQbv
463	\|12: lapply Heval -Heval
464	\|14: inversion (acca_retrieve ???) in Heval;
465	[2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
466	#bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
467	#v1 * #Hv1
468	\|15: inversion (dph_arg_retrieve ???) in Heval;
469	[2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
470	#bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
471	#v1 * #Hv1 #X cases (bind_inversion ????? X) -X
472	#vres * #Hvres #X cases (bind_inversion ????? X) -X
473	#v1 * #Hv2 ]
474	whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
475	try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
476	try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption)
477	try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption)
478	try (@sigma_fb_state_insensitive_to_dead_carry >EQ_livebefore_after assumption)
479	[1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ]
480	[1,2,3:
481	>sigma_fb_state_insensitive_to_dead_carry try (>EQ_livebefore_after assumption)
482	@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
483	\|4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta
484	[2: #error #abs destruct (abs) ]
485	#by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ
486	whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry
487	@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
488	\|5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta
489	try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres
490	try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta
491	try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres
492	try (destruct (Hvres) @I)
493	[5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I)
494	cases andb normalize nodelta #Hvres
495	\|9,10,11,12: cases cic:/matita/arithmetics/nat/eqb.fix(0,0,1) in Hvres;
496	normalize nodelta try (#abs destruct(abs) @I) #Hvres ]
497	whd in Hvres:(??%%); destruct (Hvres) >set_carry_set_regs_commute >eta_set_carry
498	@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
499	\|7: cases (split_orb_false … Helim1) -Helim1 #Helim1 #Helim3
500	>sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
501	@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
502	\|8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
503	@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ]
504	qed.
505
506	axiom to_be_cleared_sb_respects_equal_valuations:
507	∀live,coloured,l1,l2.
508	live l1 = live l2 →
509	to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2.
510
511	axiom to_be_cleared_fb_respects_equal_valuations:
512	∀live,l1,l2.
513	live l1 = live l2 →
514	to_be_cleared_fb live l1 = to_be_cleared_fb live l2.
515
516	lemma make_ERTLptr_To_LTL_good_state_relation :
517	∀fix_comp,colour,prog.
518	let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
519	let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
520	let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
521	let stacksizes ≝ lookup_stack_cost … m in
522	∃init_regs : block → list register.
523	∃f_lbls : block → label → list label.
524	∃f_regs : block → label → list register.
525	∃good : b_graph_transform_program_props ERTLptr_semantics LTL_semantics
526	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
527	prog init_regs f_lbls f_regs.
528	good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
529	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
530	init_regs f_lbls f_regs good (state_rel fix_comp colour prog)
531	(sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
532	#fix_comp #colour #prog
533	cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
534	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog)
535	#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
536	%
537	[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
538	whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
539	normalize nodelta <(pc_eq_sigma_commute … good … EQfn REL) >EQfn
540	normalize nodelta #H cases(state_pc_eq … H) * #H1 #_ #_ whd %{f} %{fn} %{EQfn}
541	assumption
542	\| #st1 #st2 #f #fn #Rst1st2 #EQfetcn >(pc_eq_sigma_commute … good … EQfetcn Rst1st2) %
543	\| #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
544	whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
545	normalize nodelta <(pc_eq_sigma_commute … good … EQfn REL) >EQfn normalize nodelta
546	#H cases(state_pc_eq … H) * #_ #_ //
547	\| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
548	#EQ destruct(EQ) normalize nodelta #state_rel #EQ destruct(EQ) whd
549	whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
550	>EQfn >EQfn normalize nodelta //
551	\| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
552	\| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
553	#EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc;
554	normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
555	whd in match eval_statement_advance; normalize nodelta
556	change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
557	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
558	#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
559	cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
560	[ whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
561	>m_return_bind ] whd in ⊢ (??%% → ?); #EQ destruct(EQ) #Rst1st2
562	#t_fn1 #EQt_fn1 whd normalize nodelta
563	letin trans_prog ≝ (b_graph_transform_program ????)
564	letin stacksizes ≝ (lookup_stack_cost ?)
565	letin prog_pars_in ≝ (mk_prog_params ERTLptr_semantics ??)
566	letin prog_pars_out ≝ (mk_prog_params LTL_semantics ??) %{(refl …)}
567	#mid #EQmid
568	letin st2_pre_mid_no_pc ≝
569	(write_decision RegisterA
570	(read_arg_decision
571	(colouring
572	…
573	(colour (globals prog_pars_in) fn
574	(analyse_liveness fix_comp (globals prog_pars_in) fn))
575	(inl register Register a)) st2) st2)
576	%{st2_pre_mid_no_pc}
577	%
578	[1,3: >map_eval_add_dummy_variance_id %
579	[1,3: %
580	[1,3: %
581	[1,3: @move_spec
582	\|*: lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
583	whd in match sigma_sb_state_pc; normalize nodelta >EQfn
584	<(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
585	normalize nodelta #EQ cases(state_pc_eq … EQ) *
586	#EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
587	<(insensitive_to_be_cleared_sb prog … st2)
588	[2,4: @dead_registers_in_dead @acc_is_dead ]
589	whd >point_of_pc_of_point
590	letin after ≝ (analyse_liveness fix_comp … fn)
591	letin before ≝ (livebefore … fn after)
592	[ cut
593	(before ltrue =
594	before (point_of_pc ERTLptr_semantics (pc … st1)))
595	[ cases daemon (CSC: Genuine proof obligation! )
596	\| #Hext ]
597	\| cut
598	(before lfalse =
599	before (point_of_pc ERTLptr_semantics (pc … st1)))
600	[ cases daemon (CSC: Genuine proof obligation! )
601	\| #Hext ]]
602	>(to_be_cleared_sb_respects_equal_valuations …
603	(colour … fn …) … Hext) <EQst1st2
604	>(to_be_cleared_fb_respects_equal_valuations … Hext) %
605	]
606	\|*: %
607	]
608	\|*: %
609	]
610	\|*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
611	>hw_reg_retrieve_write_decision_hit >m_return_bind
612	cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog …
613	good fn … Rst1st2 … EQbv)
614	[2,4: @(all_used_are_live_before … EQstmt)
615	[1,3: @set_member_singl \|: % ] ] #bv' #EQbv' #EQbv1
616	change with (prog_var_names … prog) in match (globals ?); >EQbv1
617	>EQbv' in EQbool; #EQbool
618	>(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
619	normalize nodelta
620	[2: <(pc_eq_sigma_commute … good … EQfn Rst1st2) %]
621	whd in match goto; normalize nodelta
622	>(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) %
623	]
624	\| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
625	letin p_out ≝ (mk_prog_params LTL_semantics ??)
626	letin trans_prog ≝ (b_graph_transform_program ????)
627	#st1 #st1' #st2 #f #fn
628	#stms #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
629	normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
630	#st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
631	#Heval_seq_no_pc
632	whd in match eval_statement_advance; normalize nodelta
633	whd in ⊢ (??%% → ?); #EQ destruct(EQ)
634	whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
635	whd normalize nodelta
636	change with p_out in match p_out;
637	change with p_in in match p_in;
638	change with trans_prog in match trans_prog;
639	inversion eliminable_step #Heliminable normalize nodelta %
640	[ @([ ])
641	\| % [%] % [2: % [%] \| skip] whd
642	cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
643	% [2: % [2: % [%] \| skip] \| skip]
644	(* CSC: BEGIN cut&paste from previous case: make lemma? *)
645	lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
646	whd in match sigma_sb_state_pc; normalize nodelta >EQfn
647	<(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
648	normalize nodelta #EQ cases(state_pc_eq … EQ) *
649	#EQst1st2 #_ #_
650	(* CSC: END *)
651	letin before ≝ (livebefore ???)
652	whd in match succ_pc; normalize nodelta >point_of_pc_of_point
653	whd in match (point_of_succ ???);
654	cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1)))
655	[ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt
656	(* Ha funzionato solo a dx, non a sinistra...*)
657	normalize nodelta whd in match statement_semantics; normalize nodelta
658	>Heliminable
659	cases daemon (CSC: Genuine proof obligation! )
660	\| #Hext ]
661	>(to_be_cleared_fb_respects_equal_valuations … Hext)
662	>(sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable)
663	>EQst1st2
664	>(to_be_cleared_sb_respects_equal_valuations … Hext) %
665	\|
666	\|
667
668	XXXX
669
670	*
671	[7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
672	normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
673	#st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
674	whd in match eval_seq_no_pc; normalize nodelta
675	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
676	#bv #EQbv #H @('bind_inversion H) -H #bv_op1 #EQbv_op1 #EQst1_no_pc
677	whd in match eval_statement_advance; normalize nodelta
678	whd in ⊢ (??%% → ?); #EQ destruct(EQ)
679	whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
680	whd normalize nodelta whd in match translate_op1;
681	normalize nodelta
682	change with p_out in match p_out;
683	change with p_in in match p_in;
684	change with trans_prog in match trans_prog;
685	inversion eliminable_step #Heliminable normalize nodelta %
686	[ @([ ])
687	\| % [%] % [2: % [%] \| skip] whd
688	cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
689	% [2: % [2: % [%] \| skip] \| skip]
690	(* CSC: BEGIN cut&paste from previous case: make lemma? *)
691	lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
692	whd in match sigma_sb_state_pc; normalize nodelta >EQfn
693	<(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
694	normalize nodelta #EQ cases(state_pc_eq … EQ) *
695	#EQst1st2 #_ #_
696	(* CSC: END *)
697	<EQst1st2 whd in EQst1_no_pc:(??%%); <(injective_OK ??? EQst1_no_pc)
698	change with (set_regs ???) in match (st_no_pc ??);
699
700
701
702
703
704
705
706
707	destruct (EQst1_no_pc)
708
709	<(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
710	(point_of_pc ERTLptr_semantics (pc … st2)))
711	[2,4: @dead_registers_in_dead @acc_is_dead ]
712	assumption
713
714	Rst1st2
715
716	% [2: % [ % \| ] \| skip]
717	qed.
718
719
720	lemma eval_cond_ok :
721	∀fix_comp,colour.
722	∀prog.
723	∀ f_lbls,f_regs.∀f_bl_r.
724	∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
725	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
726	∀st1,st2,st1',f,fn,a,ltrue,lfalse.
727	let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
728	R st1 st2 →
729	fetch_statement ERTLptr_semantics …
730	(globalenv_noinit ? prog) (pc … st1) =
731	return 〈f, fn, sequential … (COND ERTLptr … a ltrue) lfalse〉 →
732	let stacksizes ≝ lookup_stack_cost …
733	(\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
734	eval_state ERTLptr_semantics
735	(prog_var_names … ℕ prog)
736	(ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes))
737	st1 = return st1' →
738	as_costed (ERTLptr_status prog stacksizes) st1' →
739	∃ st2'. R st1' st2' ∧
740	∃taf : trace_any_any_free (LTL_status ? ?)
741	st2 st2'.
742	bool_to_Prop (taaf_non_empty … taf).
743	#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
744	#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
745	letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
746	@(general_eval_cond_ok … good … Rst1st2 EQfetch EQeval)
747	%
748	[ #st1 #st2 #Rst1St2 >(pc_eq_sigma_commute … good … Rst1St2) %
749	\| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
750	\|
751
752
753
754	whd in match eval_state; normalize nodelta
755	>EQfetch >m_return_bind
756	whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
757	whd in match eval_statement_advance; normalize nodelta
758	change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
759	#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
760	#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
761	lapply(fetch_statement_inv … EQfetch) * #EQfn #_
762	[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
763	\| whd in match next; normalize nodelta
764	]
765	whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
766	cases(b_graph_transform_program_fetch_statement … good … EQfetch)
767	#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
768	[2,4: #r #tl ] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] #labs **
769	[2,4: #hd #tl #_ #_ * #pre #inst #post * whd in ⊢ (%→?); ] * #EQlabs #EQf_regs
770	whd in match translate_step; normalize nodelta *** #blp #blm #bls *
771	whd in ⊢ (% → ?); #EQbl
772	whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
773	#seq_pre_l
774	letin stacksizes ≝ (lookup_stack_cost …
775	(\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
776	letin p≝ (mk_prog_params LTL_semantics
777	(\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
778	stacksizes)
779	cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
780	pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧
781	last_pop … st2' = last_pop … st2)
782	[2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
783	#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
784	>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
785	>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
786	whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
787	>EQ in EQmid ⊢ %; -nxt1 #EQmid
788	lapply(taaf_to_taa ???
789	(produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
790	seq_pre_l res_st2_pre_mid) ?)
791	[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
792	whd in match (as_label ??); whd in match (as_pc_of ??);
793	whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
794	>m_return_bind whd in match point_of_pc; normalize nodelta
795	>point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
796	cases(appoggio ????????? EQbl) cases daemon (PASSED DEPENDANT #_ #EQ1 #_ >EQ1 % *) ]
797	#taa_pre_mid whd in ⊢ (% → ?);
798	cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
799	return st2_cond )
800	[2,4: cases daemon (THE EXTENSIONAL PROOF )]
801	#st2_mid #EQst2_mid
802	cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
803	[1,3: cases daemon (PASSED DEPENDANT )] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
804	* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
805	letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
806	cut(R st1' st2_mid) [1,3: cases daemon (PASSED DEPENDANT)] #Rst1_st2_mid
807	%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
808	[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
809	cases daemon (TODO see also ERTL_to_ERTLptrOK proof! )
810	\|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
811	]
812	qed.
813
814
815	theorem ERTLptrToLTL_ok :
816	∀fix_comp : fixpoint_computer.
817	∀colour : coloured_graph_computer.
818	∀p_in : ertlptr_program.
819	let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
820	let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
821	let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
822	(* what should we do with n? *)
823	let stacksizes ≝ lookup_stack_cost m in
824	∃[1] R.
825	status_simulation
826	(joint_status ERTLptr_semantics p_in stacksizes)
827	(joint_status LTL_semantics p_out stacksizes)
828	R.
829	#fix_comp #colour #p_in
830	cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
831	(λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
832	#fregs * #f_lbls * #f_bl_r #good
833	%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
834	whd in match status_simulation; normalize nodelta
835	whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
836	whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
837	change with
838	(eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?)
839	#EQeval @('bind_inversion EQeval)
840	** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
841	#_ whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
842	cases stmt in EQfetch; -stmt
843	[ * [ #cost \| #called_id #args #dest\| #reg #lbl \| #seq] #nxt \| #fin_step \| *]
844	#EQfetch
845	change with (joint_classify ??) in
846	⊢ (match % with [ _ ⇒ ? \| _ ⇒ ? \| _ ⇒ ? \| _ ⇒ ? \| _ ⇒ ? ]);
847	[ (COST) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
848	(* XXX
849	cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
850	%{st2'} %{taf} >tafne normalize nodelta % [ % [@I \| assumption]]
851	whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
852	*) cases daemon
853	\| (CALL) whd in match joint_classify; normalize nodelta >EQfetch
854	normalize nodelta #is_call_st1
855	(* XXX
856	cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
857	* #st2_pre_call * #is_call_st2_pre_call * * #Hcall
858	#call_rel * #taa * #st2' * #sem_rel #eval_rel
859	%{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
860	%{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
861	whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (TODO)
862	*) cases daemon
863	\| (COND) whd in match joint_classify; normalize nodelta >EQfetch
864	normalize nodelta #n_costed
865	cases(eval_cond_ok … good … EQst2 … EQfetch EQeval … n_costed)
866	#st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I\|assumption]]
867	whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (TODO)
868	\| (seq) XXX whd in match joint_classify; normalize nodelta >EQfetch
869	normalize nodelta
870	cases (eval_seq_no_call_ok … good … EQfetch EQeval)
871	#st3 * #EQ destruct * #taf #taf_spec %{st3} %{taf}
872	% [% //] whd >(as_label_ok … good … st3) [%]
873	cases daemon (needs lemma about preservation of fetch_statement )
874	\| cases fin_step in EQfetch;
875	[ (GOTO) #lbl #EQfetch whd in match joint_classify; normalize nodelta
876	>EQfetch normalize nodelta
877	cases (eval_goto_ok … good … EQfetch EQeval)
878	#st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
879	% [% //] whd >(as_label_ok … good … st3) [%]
880	cases daemon (needs lemma about preservation of fetch_statement )
881	\| (RETURN) #EQfetch
882	whd in match joint_classify; normalize nodelta
883	>EQfetch normalize nodelta
884	cases (eval_return_ok … good … EQfetch EQeval) #is_ret
885	* #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
886	% [2: % [2: % [2: %{(taa_base …)} %{taf}] \|: ] \|:]
887	% [2: whd >(as_label_ok … good … st3) [%] cases daemon (needs lemma )]
888	% [2: assumption] % [2: %] % [2: assumption] % assumption
889	\| (TAILCALL) *
890	]
891	]
892

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

Download in other formats:

Original Format