source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2938

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