source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2940

Last change on this file since 2940 was 2940, checked in by sacerdot, 8 years ago
  1. StatusSimulationHelper? changed to allow to use status_rel that depends on the pc (necessary for ERTLptrToLTL)
  2. partial repairing of ERTLToERTLptrOK.ma, still in progress
  3. some progress in ERTLptrToLTLProof, but: a) some axioms were wrong, once fixed we now see some proof obligations

related to liveness analysis. Example: the variables live before and
after a COND must be the same. I have put daemons for the time being.

b) I strongly suspect that Interference should be changed to use livebefore,

in the correctness conditions (now it uses liveafter, the two sets
are probably equivalent for correct programs, but one is simpler to use:
which one?)

c) to_be_cleared_* must consult livebefore, but it is now passed liveafter.

Passing liveafter is necessary to typechek the graph, unless we do
b) first. Passing only the set computed by livebefore would be so much
better.

File size: 40.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
532axiom to_be_cleared_sb_respects_equal_valuations:
533 ∀live,coloured,l1,l2.
534  live l1 = live l2 →
535   to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2.
536
537axiom to_be_cleared_fb_respects_equal_valuations:
538 ∀live,l1,l2.
539  live l1 = live l2 →
540   to_be_cleared_fb live l1 = to_be_cleared_fb live l2.
541
542lemma make_ERTLptr_To_LTL_good_state_relation :
543∀fix_comp,colour,prog.
544let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
545let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
546let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
547let stacksizes ≝ lookup_stack_cost … m in
548∃init_regs : block → list register.
549∃f_lbls : block → label → list label.
550∃f_regs : block → label → list register.
551∃good : b_graph_transform_program_props ERTLptr_semantics LTL_semantics
552        (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
553        prog init_regs f_lbls f_regs.
554good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
555 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
556 init_regs f_lbls f_regs good (state_rel fix_comp colour prog)
557 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
558#fix_comp #colour #prog
559cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
560          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog)
561#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
562%
563[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
564  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
565  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn
566  normalize nodelta #H cases(state_pc_eq … H) * #H1 #_ #_ whd %{f} %{fn} %{EQfn}
567  assumption
568| #st1 #st2 #f #fn #Rst1st2 #EQfetcn >(pc_eq_sigma_commute … good … EQfetcn Rst1st2) %
569| #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
570  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
571  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn normalize nodelta
572   #H cases(state_pc_eq … H) * #_ #_ //
573| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
574  #EQ destruct(EQ) normalize nodelta #state_rel #EQ destruct(EQ) whd
575  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
576  >EQfn >EQfn normalize nodelta //
577| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
578| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
579  #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc;
580  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
581  whd in match eval_statement_advance; normalize nodelta
582  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
583  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
584  #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
585  cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
586  [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
587    >m_return_bind ] whd in ⊢ (??%% → ?); #EQ destruct(EQ) #Rst1st2
588  #t_fn1 #EQt_fn1 whd normalize nodelta
589  letin trans_prog ≝ (b_graph_transform_program ????)
590  letin stacksizes ≝ (lookup_stack_cost ?)
591  letin prog_pars_in ≝ (mk_prog_params ERTLptr_semantics ??)
592  letin prog_pars_out ≝ (mk_prog_params LTL_semantics ??) %{(refl …)}
593  #mid #EQmid
594  letin st2_pre_mid_no_pc ≝
595  (write_decision RegisterA
596          (read_arg_decision
597              (colouring
598                  (analyse_liveness fix_comp (globals prog_pars_in) fn)
599                  (colour (globals prog_pars_in) fn
600                  (analyse_liveness fix_comp (globals prog_pars_in) fn))
601              (inl register Register a)) st2) st2)
602  %{st2_pre_mid_no_pc}
603  %
604  [1,3: >map_eval_add_dummy_variance_id %
605       [1,3: %
606            [1,3: %
607                 [1,3: @move_spec
608                 |*: lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
609                     whd in match sigma_sb_state_pc; normalize nodelta >EQfn
610                     <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
611                     normalize nodelta #EQ cases(state_pc_eq … EQ) *
612                     #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
613                     <(insensitive_to_be_cleared_sb prog … st2)
614                     [2,4: @dead_registers_in_dead @acc_is_dead ]
615                     whd >point_of_pc_of_point
616                     [ cut
617                        (analyse_liveness fix_comp … fn ltrue =
618                          analyse_liveness fix_comp … fn
619                          (point_of_pc ERTLptr_semantics (pc … st1)))
620                       [ cases daemon (*CSC: Genuine proof obligation! *)
621                       | #Hext ]
622                     |  cut
623                        (analyse_liveness fix_comp … fn lfalse =
624                          analyse_liveness fix_comp … fn
625                          (point_of_pc ERTLptr_semantics (pc … st1)))
626                       [ cases daemon (*CSC: Genuine proof obligation! *)
627                       | #Hext ]]
628                     >(to_be_cleared_sb_respects_equal_valuations …
629                        (colour … fn …) … Hext) <EQst1st2
630                     >(to_be_cleared_fb_respects_equal_valuations … Hext) %
631                 ]
632            |*: %
633            ]
634       |*: %
635       ]
636  |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
637      >hw_reg_retrieve_write_decision_hit >m_return_bind
638      cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog …
639                                                        good fn … Rst1st2 … EQbv)
640        [2,4: @(all_used_are_live_before … EQstmt)
641            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
642        change with (prog_var_names … prog) in match (globals ?); >EQbv1
643        >EQbv' in EQbool; #EQbool
644        >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
645        normalize nodelta
646        [2: <(pc_eq_sigma_commute … good … EQfn Rst1st2) %]
647        whd in match goto; normalize nodelta
648        >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) %
649  ]
650| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
651  letin p_out ≝ (mk_prog_params LTL_semantics ??)
652  letin trans_prog ≝ (b_graph_transform_program ????)
653  #st1 #st1' #st2 #f #fn
654  #stms #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
655  normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
656  #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
657  #Heval_seq_no_pc
658  whd in match eval_statement_advance; normalize nodelta
659  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
660  whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
661  whd normalize nodelta
662  change with p_out in match p_out;
663  change with p_in in match p_in;
664  change with trans_prog in match trans_prog;
665  inversion eliminable_step #Heliminable normalize nodelta %
666  [ @([ ])
667  | % [%] % [2: % [%] | skip] whd
668    cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
669    % [2: % [2: % [%] | skip] | skip]
670    (* CSC: BEGIN cut&paste from previous case: make lemma? *)
671    lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
672    whd in match sigma_sb_state_pc; normalize nodelta >EQfn
673    <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
674    normalize nodelta #EQ cases(state_pc_eq … EQ) *
675    #EQst1st2 #_ #_
676    (* CSC: END *)
677    <EQst1st2 whd in EQst1_no_pc:(??%%); whd in match (st_no_pc ??);
678
679
680       
681       
682       
683        <(injective_OK ??? EQst1_no_pc)
684        change with (set_regs ???) in match (st_no_pc ??);
685 
686 
687  *
688  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
689      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
690      #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
691      whd in match eval_seq_no_pc; normalize  nodelta
692      #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
693      #bv #EQbv #H @('bind_inversion H) -H #bv_op1 #EQbv_op1 #EQst1_no_pc
694      whd in match eval_statement_advance; normalize nodelta
695      whd in ⊢ (??%% → ?); #EQ destruct(EQ)
696      whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
697      whd normalize nodelta whd in match translate_op1;
698      normalize nodelta
699      change with p_out in match p_out;
700      change with p_in in match p_in;
701      change with trans_prog in match trans_prog;
702      inversion eliminable_step #Heliminable normalize nodelta %
703      [ @([ ])
704      | % [%] % [2: % [%] | skip] whd
705        cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
706        % [2: % [2: % [%] | skip] | skip]
707        (* CSC: BEGIN cut&paste from previous case: make lemma? *)
708        lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
709        whd in match sigma_sb_state_pc; normalize nodelta >EQfn
710        <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
711        normalize nodelta #EQ cases(state_pc_eq … EQ) *
712        #EQst1st2 #_ #_
713        (* CSC: END *)
714        <EQst1st2 whd in EQst1_no_pc:(??%%); <(injective_OK ??? EQst1_no_pc)
715        change with (set_regs ???) in match (st_no_pc ??);
716
717       
718       
719       
720       
721       
722       
723       
724         destruct (EQst1_no_pc)
725       
726        <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
727          (point_of_pc ERTLptr_semantics (pc … st2)))
728                     [2,4: @dead_registers_in_dead @acc_is_dead ]
729                     assumption
730     
731      Rst1st2
732     
733      % [2: % [ % | ] | skip]
734qed.
735
736
737lemma eval_cond_ok :
738∀fix_comp,colour.
739∀prog.
740∀ f_lbls,f_regs.∀f_bl_r.
741∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
742     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
743∀st1,st2,st1',f,fn,a,ltrue,lfalse.
744let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
745R st1 st2 →
746 fetch_statement ERTLptr_semantics …
747  (globalenv_noinit ? prog) (pc … st1) =
748    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
749let stacksizes ≝ lookup_stack_cost …
750                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 
751 eval_state ERTLptr_semantics
752   (prog_var_names … ℕ prog)
753   (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes))
754   st1 = return st1' →
755as_costed (ERTLptr_status prog stacksizes) st1' →
756∃ st2'. R st1' st2' ∧
757∃taf : trace_any_any_free (LTL_status ? ?)
758st2 st2'.
759bool_to_Prop (taaf_non_empty … taf).
760#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
761#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
762letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
763@(general_eval_cond_ok … good … Rst1st2 EQfetch EQeval)
764%
765[ #st1 #st2 #Rst1St2 >(pc_eq_sigma_commute … good … Rst1St2) %
766| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
767|
768
769
770
771whd in match eval_state; normalize nodelta
772>EQfetch >m_return_bind
773whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
774whd in match eval_statement_advance; normalize nodelta
775change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
776#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
777#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
778lapply(fetch_statement_inv … EQfetch) * #EQfn #_
779[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
780| whd in match next; normalize nodelta
781]
782whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
783cases(b_graph_transform_program_fetch_statement … good … EQfetch)
784#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
785[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
786[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
787whd in match translate_step; normalize nodelta *** #blp #blm #bls *
788whd in ⊢ (% → ?); #EQbl
789whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
790#seq_pre_l
791letin stacksizes ≝ (lookup_stack_cost …
792                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
793letin p≝ (mk_prog_params LTL_semantics
794                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
795                         stacksizes)
796cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
797           pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧
798           last_pop … st2' = last_pop … st2)
799   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
800#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
801>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
802>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
803whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
804>EQ in EQmid ⊢ %; -nxt1 #EQmid
805lapply(taaf_to_taa ???
806           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
807                                       seq_pre_l res_st2_pre_mid) ?)
808[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
809      whd in match (as_label ??); whd in match (as_pc_of ??);
810      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
811      >m_return_bind whd in match point_of_pc; normalize nodelta
812      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
813      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
814#taa_pre_mid whd in ⊢ (% → ?);
815cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
816                     return st2_cond )
817[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
818#st2_mid #EQst2_mid
819cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
820[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
821* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
822letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
823cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
824%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
825[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
826     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
827|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
828]
829qed.
830
831
832theorem ERTLptrToLTL_ok :
833∀fix_comp : fixpoint_computer.
834∀colour : coloured_graph_computer.
835∀p_in : ertlptr_program.
836let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
837let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
838let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
839(* what should we do with n? *)
840let stacksizes ≝ lookup_stack_cost m in
841∃[1] R.
842  status_simulation
843    (joint_status ERTLptr_semantics p_in stacksizes)
844    (joint_status LTL_semantics p_out stacksizes)
845    R.
846#fix_comp #colour #p_in
847cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
848          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
849#fregs * #f_lbls * #f_bl_r #good
850%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
851whd in match status_simulation; normalize nodelta
852whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
853whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
854change with
855  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 
856#EQeval @('bind_inversion EQeval)
857** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
858#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
859cases stmt in EQfetch; -stmt
860[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
861#EQfetch
862change with (joint_classify ??) in
863                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
864[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
865  (* XXX
866  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
867  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
868  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
869  *) cases daemon
870| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
871          normalize nodelta #is_call_st1
872          (* XXX
873          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
874          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
875          #call_rel * #taa * #st2' * #sem_rel #eval_rel
876          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
877          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
878          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
879          *) cases daemon
880| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
881          normalize nodelta #n_costed
882          cases(eval_cond_ok  … good … EQst2 … EQfetch EQeval … n_costed)
883          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
884          whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*)
885| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
886          normalize nodelta
887          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
888          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
889          % [% //] whd >(as_label_ok … good … st3) [%]
890          cases daemon (*needs lemma about preservation of fetch_statement *)
891|  cases fin_step in EQfetch;
892  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
893     >EQfetch normalize nodelta
894    cases (eval_goto_ok … good  … EQfetch EQeval)
895    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
896    % [% //] whd >(as_label_ok … good … st3) [%]
897    cases daemon (*needs lemma about preservation of fetch_statement *)
898  | (*RETURN*) #EQfetch
899     whd in match joint_classify; normalize nodelta
900    >EQfetch  normalize nodelta
901    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
902    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
903    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
904    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
905    % [2: assumption] % [2: %] % [2: assumption] % assumption
906  | (*TAILCALL*) *
907  ]
908]
909
Note: See TracBrowser for help on using the repository browser.