source: src/ERTLptr/ERTLptrToLTLProof.ma @ 3362

Last change on this file since 3362 was 3254, checked in by sacerdot, 7 years ago

Code I always forgot to commit.
To be ported to ERTLtoLTLProof.ma.

File size: 40.4 KB
Line 
1include "ERTLptr/ERTLptrToLTL.ma".
2include "ERTLptr/ERTLptr_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6include "common/AssocList.ma".
7
8(* Inefficient, replace with Trie lookup *)
9definition lookup_stack_cost ≝
10 λp.λid : ident.
11  assoc_list_lookup ? ℕ id (eq_identifier …) p.
12
13(*TO BE MOVED*)
14definition ERTLptr_status ≝
15λprog : ertlptr_program.λstack_sizes.
16joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
17
18definition LTL_status ≝
19λprog : ltl_program.λstack_sizes.
20joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
21
22definition local_clear_sb_type ≝ decision → bool.
23definition clear_sb_type ≝ label → local_clear_sb_type.
24 
25axiom to_be_cleared_sb : 
26∀live_before : valuation register_lattice. coloured_graph live_before → clear_sb_type.
27
28definition local_clear_fb_type ≝ vertex → bool.
29definition clear_fb_type ≝ label → local_clear_fb_type.
30
31axiom to_be_cleared_fb :
32∀live_before : valuation register_lattice.clear_fb_type.
33
34axiom sigma_fb_state:
35 ertlptr_program → local_clear_fb_type →
36  state ERTLptr_semantics → state ERTLptr_semantics.
37
38axiom 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
43axiom 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
54axiom sigma_sb_state:
55 ertlptr_program → local_clear_sb_type → state LTL_semantics → state ERTLptr_semantics.
56
57definition dummy_state : state ERTLptr_semantics ≝
58mk_state ERTL_semantics
59   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
60
61definition dummy_state_pc : state_pc ERTLptr_semantics ≝
62mk_state_pc ? dummy_state (null_pc one) (null_pc one).
63
64
65definition 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
81include "joint/StatusSimulationHelper.ma".
82
83definition 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
101definition state_rel : fixpoint_computer → coloured_graph_computer →
102ertlptr_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〉 ∧
106let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
107let before ≝ livebefore … fn after in
108let 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
112axiom write_decision :
113 decision → beval → state LTL_LIN_state → state LTL_LIN_state.
114
115axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval.
116
117axiom 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
124definition 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.
129b_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 →
131let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
132let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
133let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
134let stacksizes ≝ lookup_stack_cost … m in 
135status_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 ≝ *) ?.
149cases daemon
150qed.
151
152axiom 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.
158let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
159R st1 st2 → 
160fetch_statement ERTLptr_semantics (prog_var_names … prog)
161      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
162as_label ? st2 = as_label ? st1.
163
164(*
165(* Copy the proof too from previous pass *)
166axiom fetch_stmt_ok_sigma_state_ok :
167∀prog : ertlptr_program.
168∀ f_lbls,f_regs,id,fn,stmt,st.
169fetch_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〉 →
172let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn
173                                               (f_regs (pc_block (pc … st)))) in
174st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) =
175sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
176*)
177
178axiom 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.
183let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
184R st1 st2 →
185pc_block (pc … st1) = pc_block (pc … st2).
186
187axiom 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.
192fetch_internal_function ? (globalenv_noinit … prog)
193                (pc_block (pc … st1)) = return 〈f,fn〉 →
194let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
195R st1 st2 →
196(pc … st1) = (pc … st2).
197
198(*
199axiom 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.
204let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
205R st1 st2 →
206∀pc1,pc2.pc1 = pc2 →
207R (set_pc … pc1 st1) (set_pc … pc2 st2).
208
209axiom 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〉.
213prog_var_names … prog = prog_var_names … p_out.
214
215lemma 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 % [%] //
218qed.*)
219
220include "joint/semantics_blocks.ma".
221include "ASM/Util.ma".
222
223axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
224∀st : state LTL_LIN_state.
225hw_reg_retrieve (regs … (write_decision r bv st)) r = return bv.
226
227axiom 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.
231repeat_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
235axiom sigma_beval:
236 ertlptr_program → (block → label → list label) → beval → beval.
237 
238
239axiom 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).
245let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
246let 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 →
251lives (inl ? ? r) (livebefore  … fn after (point_of_pc ERTLptr_semantics (pc … st1))) →
252ps_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                             
259axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
260axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
261axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
262set_member A DEC a (set_union … x y).
263axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
264set_member A DEC a (set_union … x y).
265axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
266¬set_member A DEC a y →
267set_member A DEC a (set_diff … x y).
268
269lemma 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.
274stmt_at … (joint_if_code … fn) l = return stmt →
275∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
276let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
277eliminable ? (after l) stmt = false →
278lives (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
297whd in match (livebefore ????); whd in EQstmt : (??%?); >EQstmt
298normalize nodelta -EQstmt whd in match (statement_semantics ???);
299whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
300normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
301qed.
302
303axiom bool_of_beval_sigma_commute :
304∀prog.∀f_lbls.∀bv,b.
305bool_of_beval (sigma_beval prog f_lbls bv) = return b →
306bool_of_beval bv = return b.
307
308lemma 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 %
311qed.
312
313lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
314st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
315pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
316#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
317%{(refl …)} %{(refl …)} %
318qed.
319
320(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
321lemma 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)
324whd in ⊢ (??%? → ?); #EQ >EQ %
325qed.
326
327lemma 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
334qed.
335
336lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
337 #A #a #b #EQ destruct %
338qed.
339
340lemma eq_notb_true_to_eq_false:
341 ∀b. (¬b) = true → b = false.
342* // #abs normalize in abs; destruct
343qed.
344
345axiom 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
356axiom 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
368axiom 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
374lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
375 ** normalize #abs destruct /2/
376qed.
377
378lemma eta_set_carry:
379 ∀P,st. set_carry P (carry P st) st = st.
380#P * //
381qed.
382
383lemma 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 * //
386qed.
387
388lemma 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 %
403qed.
404
405lemma 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
431lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim)
432#EQ_livebefore_after -next
433cases stms in Heval Helim;
434try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
435try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
436try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
437try (#arg1 #Heval #Helim) try (#Heval #Helim)
438whd in Heval:(??%?);
439whd 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]
445lapply (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 ]
474whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
475try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
476try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption)
477try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption)
478try (@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 ]
504qed.
505
506axiom 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
511axiom 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
516lemma make_ERTLptr_To_LTL_good_state_relation :
517∀fix_comp,colour,prog.
518let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
519let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
520let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
521let 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.
528good_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
533cases(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]
717qed.
718
719
720lemma 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.
727let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
728R st1 st2 →
729 fetch_statement ERTLptr_semantics …
730  (globalenv_noinit ? prog) (pc … st1) =
731    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
732let 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' →
738as_costed (ERTLptr_status prog stacksizes) st1' →
739∃ st2'. R st1' st2' ∧
740∃taf : trace_any_any_free (LTL_status ? ?)
741st2 st2'.
742bool_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
745letin 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
754whd in match eval_state; normalize nodelta
755>EQfetch >m_return_bind
756whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
757whd in match eval_statement_advance; normalize nodelta
758change 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
761lapply(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]
765whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
766cases(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
770whd in match translate_step; normalize nodelta *** #blp #blm #bls *
771whd in ⊢ (% → ?); #EQbl
772whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
773#seq_pre_l
774letin stacksizes ≝ (lookup_stack_cost …
775                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
776letin p≝ (mk_prog_params LTL_semantics
777                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
778                         stacksizes)
779cases(? : ∃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
786whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
787>EQ in EQmid ⊢ %; -nxt1 #EQmid
788lapply(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 ⊢ (% → ?);
798cases(? : ∃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
802cut(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
805letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
806cut(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]
812qed.
813
814
815theorem ERTLptrToLTL_ok :
816∀fix_comp : fixpoint_computer.
817∀colour : coloured_graph_computer.
818∀p_in : ertlptr_program.
819let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
820let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
821let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
822(* what should we do with n? *)
823let 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
830cases(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)}
834whd in match status_simulation; normalize nodelta
835whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
836whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
837change 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
842cases stmt in EQfetch; -stmt
843[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
844#EQfetch
845change 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.