source: src/ERTLptr/ERTLptrToLTLProof.ma @ 3155

Last change on this file since 3155 was 2949, checked in by sacerdot, 8 years ago

Some advance/repairing in ERTLptrToLTLProof. In particular, we know take in
account that the fixpoint computation only returns a pre-fixpoint.

File size: 49.8 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).
268axiom set_member_subset_if:
269 ∀A,DEC,S1,S2.
270  set_subset A DEC S1 S2 →
271   ∀x. set_member A DEC x S1 → set_member A DEC x S2.
272axiom set_member_subset_onlyif:
273 ∀A,DEC,S1,S2.
274  (∀x. set_member A DEC x S1 → set_member A DEC x S2) →
275   set_subset A DEC S1 S2.
276
277
278lemma all_used_are_live_before :
279∀fix_comp.
280∀prog : ertlptr_program.
281∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
282∀l,stmt.
283stmt_at … (joint_if_code … fn) l = return stmt →
284∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
285let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
286eliminable ? (after l) stmt = false →
287lives (inl ? ? r)  (livebefore  … fn after l).
288#fix_comp #prog #fn #l *
289[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
290[ #str
291| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
292| #a
293| * [ #r | #b]
294| #i #i_spec #dpl #dph
295| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
296| #op #a #a'
297| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
298|
299|
300| #a #dpl #dph
301| #dpl #dph #a
302| * [ * [|| #r] | #r #lbl | #r #lbl ]
303]
304] #nxt| * [ #lbl | | *] |*]
305#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
306whd in match (livebefore ????); whd in EQstmt : (??%?); >EQstmt
307normalize nodelta -EQstmt whd in match (statement_semantics ???);
308whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
309normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
310qed.
311
312axiom bool_of_beval_sigma_commute :
313∀prog.∀f_lbls.∀bv,b.
314bool_of_beval (sigma_beval prog f_lbls bv) = return b →
315bool_of_beval bv = return b.
316
317lemma map_eval_add_dummy_variance_id :
318∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
319#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
320qed.
321
322lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
323st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
324pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
325#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
326%{(refl …)} %{(refl …)} %
327qed.
328
329(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
330lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
331∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
332#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
333whd in ⊢ (??%? → ?); #EQ >EQ %
334qed.
335
336lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
337 OptPred True (λres.
338  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
339  (split_on_last … l2).
340#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
341#hd #tl #IH #l1 whd >split_on_last_append_singl whd
342<associative_append @split_on_last_append_singl
343qed.
344
345lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
346 #A #a #b #EQ destruct %
347qed.
348
349lemma eq_notb_true_to_eq_false:
350 ∀b. (¬b) = true → b = false.
351* // #abs normalize in abs; destruct
352qed.
353
354axiom sigma_fb_state_insensitive_to_dead_reg:
355 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label.
356 ∀r: register. ∀before.
357  set_member … (eq_identifier RegisterTag) r (\fst  (before l)) = false →
358  sigma_fb_state prog
359   (to_be_cleared_fb before l)
360   (set_regs ERTLptr_semantics
361    〈reg_store r bv (\fst  (regs ERTLptr_semantics st)),
362    \snd  (regs ERTLptr_semantics st)〉 st)
363  = sigma_fb_state prog (to_be_cleared_fb before l) st.
364
365axiom sigma_fb_state_insensitive_to_dead_Reg:
366 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label.
367 ∀r: Register. ∀before.
368  set_member … eq_Register r (\snd  (before l)) = false →
369  sigma_fb_state prog
370   (to_be_cleared_fb before l)
371   (set_regs ERTLptr_semantics
372     〈\fst  (regs ERTLptr_semantics st),
373      hwreg_store r bv (\snd  (regs ERTLptr_semantics st))〉
374      st)
375  = sigma_fb_state prog (to_be_cleared_fb before l) st.
376
377axiom sigma_fb_state_insensitive_to_dead_carry:
378 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label. ∀before.
379  set_member Register eq_Register RegisterCarry (\snd (before l)) = false →
380   sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTLptr_semantics bv st) =
381   sigma_fb_state prog (to_be_cleared_fb before l) st.
382
383lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
384 ** normalize #abs destruct /2/
385qed.
386
387lemma eta_set_carry:
388 ∀P,st. set_carry P (carry P st) st = st.
389#P * //
390qed.
391
392lemma set_carry_set_regs_commute:
393 ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
394 #P * //
395qed.
396
397lemma eliminable_step_to_eq_livebefore_liveafter:
398 ∀prog,stackcost,fn.
399 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
400 ∀st1: joint_abstract_status p_in.
401 ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
402 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
403 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
404 ∀liveafter.
405 eliminable_step (globals p_in) (liveafter (point_of_pc ERTLptr_semantics (pc … st1))) stms = true →
406  livebefore … fn liveafter pt = liveafter pt.
407 #prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim
408 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
409 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
410 #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
411 whd in match eliminable; normalize nodelta >Helim %
412qed.
413
414lemma set_subset_to_set_subst_set_union_left:
415 ∀T,eqT,A,B,C. set_subset T eqT A B → set_subset … eqT A (set_union … B C).
416 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
417 lapply (set_member_subset_if … H) #H2 /3 by set_member_union1/
418qed.
419
420lemma set_subset_to_set_subst_set_union_right:
421 ∀T,eqT,A,B,C. set_subset T eqT A C → set_subset … eqT A (set_union … B C).
422 #T #eqT #A #B #C #H @set_member_subset_onlyif #x #K
423 lapply (set_member_subset_if … H) #H2 /3 by set_member_union2/
424qed.
425
426lemma rl_included_rl_join_left:
427 ∀A,B,C. rl_included A B → rl_included A (rl_join B C).
428 #A #B #C whd in match rl_included; normalize nodelta #H
429 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
430 /2 by set_subset_to_set_subst_set_union_left/
431qed.
432
433lemma rl_included_rl_join_right:
434 ∀A,B,C. rl_included A C → rl_included A (rl_join B C).
435 #A #B #C whd in match rl_included; normalize nodelta #H
436 cases (andb_Prop_true … H) -H #H1 #H2 @andb_Prop
437 /2 by set_subset_to_set_subst_set_union_right/
438qed.
439
440lemma set_subset_reflexive: ∀A,DEC,x. set_subset A DEC x x.
441 /2/
442qed.
443
444lemma rl_included_reflexive: ∀x. rl_included x x.
445 /2/
446qed.
447
448lemma mem_of_fold_join:
449 ∀F,dom.
450  ∀x. x ∈ dom →
451   rl_included (F x)
452    (fold label (l_property register_lattice) rl_join rl_bottom (λl:label.true)
453      F dom).
454 #F #dom elim dom [ #x * ] #hd #tl #IH #x whd in match (? ∈ ?); @eqb_elim
455 normalize nodelta #Hx #H change with (rl_join ??) in ⊢ (?(??%));
456 destruct /3 by rl_included_rl_join_left,rl_included_rl_join_right/
457qed.
458
459lemma set_subset_transitive:
460 ∀A,DEC,S1,S2,S3.
461  set_subset A DEC S1 S2 → set_subset … DEC S2 S3 → set_subset … DEC S1 S3.
462 #A #DEC #S1 #S2 #S3
463 #H1 lapply (set_member_subset_if … H1) -H1 #H1
464 #H2 lapply (set_member_subset_if … H2) -H2 #H2
465 @set_member_subset_onlyif /3 by/
466qed.
467
468lemma rl_included_transitive:
469 ∀S1,S2,S3. rl_included S1 S2 → rl_included S2 S3 → rl_included S1 S3.
470 #S1 #S2 #S3 whd in match rl_included; normalize nodelta
471 #H cases (andb_Prop_true … H) -H #H1 #H2
472 #H cases (andb_Prop_true … H) -H #H3 #H4
473 /3 by andb_Prop,set_subset_transitive/
474qed.
475
476lemma rl_included_rl_diff_rl_empty:
477 ∀S1. rl_included S1 (rl_diff S1 rl_bottom).
478 #S1 whd in match (rl_included ??);
479 lapply (set_member_subset_onlyif … (eq_identifier …) (\fst S1) (\fst (rl_diff S1 rl_bottom)))
480 cases (set_subset ????)
481 /3 by set_member_diff,set_member_subset_onlyif/
482qed.
483
484lemma included_livebefore_livebeafter_stmt_labels:
485 ∀fix_comp,globals,fn,l,stmt.
486  let after ≝ analyse_liveness fix_comp globals fn in
487   stmt_at … (joint_if_code ERTLptr … fn) l = Some … stmt →
488  ∀nxt.
489   nxt ∈
490    stmt_labels (mk_stmt_params (g_u_pars ERTLptr) label (Some label) false)
491     globals stmt →
492  l_included register_lattice (livebefore … fn after nxt) (after l).
493#fix_comp #globals #fn #l #stmt letin after ≝ (analyse_liveness ???) #EQlookup #nxt
494#Hnxt lapply (fix_correct … after l) #spec @(rl_included_transitive … spec) -spec
495whd in match (liveafter ????); whd in EQlookup:(??%?); >EQlookup -EQlookup normalize nodelta
496/2 by mem_of_fold_join/
497qed.
498
499axiom eq_sigma_state_monotonicity:
500 ∀prog,live,graph,st1,st2,l1,l2.
501  rl_included (live l2) (live l1) →
502  sigma_fb_state prog (to_be_cleared_fb live l1) st1 =
503   sigma_sb_state prog (to_be_cleared_sb live graph l1) st2 →
504  sigma_fb_state prog (to_be_cleared_fb live l2) st1 =
505   sigma_sb_state prog (to_be_cleared_sb live graph l2) st2.
506
507(* True and useless
508axiom to_be_cleared_sb_respects_equal_valuations:
509 ∀live,coloured,l1,l2.
510  live l1 = live l2 →
511   to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2.
512
513axiom to_be_cleared_fb_respects_equal_valuations:
514 ∀live,l1,l2.
515  live l1 = live l2 →
516   to_be_cleared_fb live l1 = to_be_cleared_fb live l2.
517*)
518
519(*
520lemma sigma_fb_state_insensitive_to_eliminable:
521 ∀fix_comp: fixpoint_computer.
522 ∀prog: ertlptr_program.
523 ∀stackcost.
524 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
525 ∀f,fn.
526 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in
527 let before ≝ livebefore … fn after in
528 ∀st1 : joint_abstract_status p_in.
529 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
530 ∀st1_no_pc. ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
531 stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) →
532 ∀Heval_seq_no_pc:
533   eval_seq_no_pc ERTLptr_semantics
534   (prog_var_names (joint_function ERTLptr_semantics) ℕ prog)
535   (ev_genv
536    (mk_prog_params ERTLptr_semantics prog stackcost))
537   f stms (st_no_pc … st1)
538   =return st1_no_pc.
539 ∀Heliminable:
540   eliminable_step (globals p_in)
541    (after (point_of_pc ERTLptr_semantics (pc p_in st1))) stms =true.
542 sigma_fb_state prog (to_be_cleared_fb before next) st1_no_pc =
543  sigma_fb_state prog (to_be_cleared_fb before pt) (st_no_pc … st1).
544#fix_comp #prog #stackcost letin p_in ≝ (mk_prog_params ???) #f #fn
545letin after ≝ (analyse_liveness ???)
546#st1 #st1' #stms #next #stmt_at #Heval #Helim
547lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim)
548#EQ_livebefore_after
549cases stms in Heval Helim;
550try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
551try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
552try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
553try (#arg1 #Heval #Helim) try (#Heval #Helim)
554whd in Heval:(??%?);
555whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim))
556[7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] |*: #arg2 #arg3 ] #Harg1
557    normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?);
558    try (change with (false=true) in Helim; destruct (Helim))
559    [4,8: cases arg1 in Heval Helim; normalize nodelta
560      [ * normalize nodelta #arg10 #arg11] #Heval #Helim]
561lapply (eq_notb_true_to_eq_false ? Helim) -Helim #Helim
562[1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?);
563  [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta
564        inversion ps_reg_retrieve normalize nodelta
565        [2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ]
566        #bv #EQbv ]
567|3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval;
568    [2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
569    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
570    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
571    #vres * #Hvres #X cases (bind_inversion ????? X) -X
572    #st1'' * #Hst1''
573|9: inversion (opt_to_res ???) in Heval;
574    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
575    #bv normalize nodelta #EQbv
576|10,11: inversion (get_pc_from_label ?????) in Heval;
577     [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
578     #bv normalize nodelta #EQbv
579|12: lapply Heval -Heval
580|14: inversion (acca_retrieve ???) in Heval;
581    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
582    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
583    #v1 * #Hv1
584|15: inversion (dph_arg_retrieve ???) in Heval;
585    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
586    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
587    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
588    #vres * #Hvres #X cases (bind_inversion ????? X) -X
589    #v1 * #Hv2 ]
590whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
591try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
592
593XXX
594
595try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption)
596try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption)
597try (@sigma_fb_state_insensitive_to_dead_carry >EQ_livebefore_after assumption)
598[1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ]
599[1,2,3:
600  >sigma_fb_state_insensitive_to_dead_carry try (>EQ_livebefore_after assumption)
601  @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
602|4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta
603    [2: #error #abs destruct (abs) ]
604    #by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ
605    whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry
606    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
607|5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta
608      try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres
609      try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta
610      try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres
611      try (destruct (Hvres) @I)
612      [5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I)
613          cases andb normalize nodelta #Hvres
614      |9,10,11,12: cases cic:/matita/arithmetics/nat/eqb.fix(0,0,1) in Hvres;
615          normalize nodelta try (#abs destruct(abs) @I) #Hvres ]
616      whd in Hvres:(??%%); destruct (Hvres) >set_carry_set_regs_commute >eta_set_carry
617      @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
618|7: cases (split_orb_false … Helim1) -Helim1 #Helim1 #Helim3
619   >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
620   @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
621|8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
622    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ]
623qed.
624
625
626lemma sigma_fb_state_insensitive_to_eliminable:
627 ∀fix_comp: fixpoint_computer.
628 ∀prog: ertlptr_program.
629 ∀stackcost.
630 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
631 ∀f,fn.
632 ∀after: valuation ?.
633 let before ≝ livebefore … fn after in
634 ∀st1 : joint_abstract_status p_in.
635 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
636 ∀st1_no_pc. ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
637 stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) →
638 ∀Heval_seq_no_pc:
639   eval_seq_no_pc ERTLptr_semantics
640   (prog_var_names (joint_function ERTLptr_semantics) ℕ prog)
641   (ev_genv
642    (mk_prog_params ERTLptr_semantics prog stackcost))
643   f stms (st_no_pc … st1)
644   =return st1_no_pc.
645 ∀Heliminable:
646   eliminable_step (globals p_in)
647    (after (point_of_pc ERTLptr_semantics (pc p_in st1))) stms =true.
648 sigma_fb_state prog (to_be_cleared_fb before pt) st1_no_pc =
649  sigma_fb_state prog (to_be_cleared_fb before pt) (st_no_pc … st1).
650#fix_comp #prog #stackcost letin p_in ≝ (mk_prog_params ???) #f #fn #after
651#st1 #st1' #stms #next #stmt_at #Heval #Helim
652lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at … Helim)
653#EQ_livebefore_after -next
654cases stms in Heval Helim;
655try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
656try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
657try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
658try (#arg1 #Heval #Helim) try (#Heval #Helim)
659whd in Heval:(??%?);
660whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim))
661[7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] |*: #arg2 #arg3 ] #Harg1
662    normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?);
663    try (change with (false=true) in Helim; destruct (Helim))
664    [4,8: cases arg1 in Heval Helim; normalize nodelta
665      [ * normalize nodelta #arg10 #arg11] #Heval #Helim]
666lapply (eq_notb_true_to_eq_false ? Helim) -Helim #Helim
667[1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?);
668  [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta
669        inversion ps_reg_retrieve normalize nodelta
670        [2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ]
671        #bv #EQbv ]
672|3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval;
673    [2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
674    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
675    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
676    #vres * #Hvres #X cases (bind_inversion ????? X) -X
677    #st1'' * #Hst1''
678|9: inversion (opt_to_res ???) in Heval;
679    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
680    #bv normalize nodelta #EQbv
681|10,11: inversion (get_pc_from_label ?????) in Heval;
682     [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
683     #bv normalize nodelta #EQbv
684|12: lapply Heval -Heval
685|14: inversion (acca_retrieve ???) in Heval;
686    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
687    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
688    #v1 * #Hv1
689|15: inversion (dph_arg_retrieve ???) in Heval;
690    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
691    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
692    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
693    #vres * #Hvres #X cases (bind_inversion ????? X) -X
694    #v1 * #Hv2 ]
695whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
696try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
697try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption)
698try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption)
699try (@sigma_fb_state_insensitive_to_dead_carry >EQ_livebefore_after assumption)
700[1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ]
701[1,2,3:
702  >sigma_fb_state_insensitive_to_dead_carry try (>EQ_livebefore_after assumption)
703  @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
704|4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta
705    [2: #error #abs destruct (abs) ]
706    #by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ
707    whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry
708    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
709|5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta
710      try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres
711      try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta
712      try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres
713      try (destruct (Hvres) @I)
714      [5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I)
715          cases andb normalize nodelta #Hvres
716      |9,10,11,12: cases cic:/matita/arithmetics/nat/eqb.fix(0,0,1) in Hvres;
717          normalize nodelta try (#abs destruct(abs) @I) #Hvres ]
718      whd in Hvres:(??%%); destruct (Hvres) >set_carry_set_regs_commute >eta_set_carry
719      @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
720|7: cases (split_orb_false … Helim1) -Helim1 #Helim1 #Helim3
721   >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
722   @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
723|8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
724    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ]
725qed. *)
726
727lemma make_ERTLptr_To_LTL_good_state_relation :
728∀fix_comp,colour,prog.
729let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
730let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
731let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
732let stacksizes ≝ lookup_stack_cost … m in
733∃init_regs : block → list register.
734∃f_lbls : block → label → list label.
735∃f_regs : block → label → list register.
736∃good : b_graph_transform_program_props ERTLptr_semantics LTL_semantics
737        (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
738        prog init_regs f_lbls f_regs.
739good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
740 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
741 init_regs f_lbls f_regs good (state_rel fix_comp colour prog)
742 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
743#fix_comp #colour #prog
744cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
745          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog)
746#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
747%
748[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
749  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
750  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn
751  normalize nodelta #H cases(state_pc_eq … H) * #H1 #_ #_ whd %{f} %{fn} %{EQfn}
752  assumption
753| #st1 #st2 #f #fn #Rst1st2 #EQfetcn >(pc_eq_sigma_commute … good … EQfetcn Rst1st2) %
754| #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
755  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
756  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn normalize nodelta
757   #H cases(state_pc_eq … H) * #_ #_ //
758| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
759  #EQ destruct(EQ) normalize nodelta #state_rel #EQ destruct(EQ) whd
760  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
761  >EQfn >EQfn normalize nodelta //
762| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
763| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
764  #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc;
765  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
766  whd in match eval_statement_advance; normalize nodelta
767  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
768  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
769  #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
770  cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
771  [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
772    >m_return_bind ] whd in ⊢ (??%% → ?); #EQ destruct(EQ) #Rst1st2
773  #t_fn1 #EQt_fn1 whd normalize nodelta
774  letin trans_prog ≝ (b_graph_transform_program ????)
775  letin stacksizes ≝ (lookup_stack_cost ?)
776  letin prog_pars_in ≝ (mk_prog_params ERTLptr_semantics ??)
777  letin prog_pars_out ≝ (mk_prog_params LTL_semantics ??) %{(refl …)}
778  #mid #EQmid
779  letin st2_pre_mid_no_pc ≝
780  (write_decision RegisterA
781          (read_arg_decision
782              (colouring
783                  …
784                  (colour (globals prog_pars_in) fn
785                  (analyse_liveness fix_comp (globals prog_pars_in) fn))
786              (inl register Register a)) st2) st2)
787  %{st2_pre_mid_no_pc}
788  %
789  [1,3: >map_eval_add_dummy_variance_id %
790       [1,3: %
791            [1,3: %
792                 [1,3: @move_spec
793                 |*: lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
794                     whd in match sigma_sb_state_pc; normalize nodelta >EQfn
795                     <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
796                     normalize nodelta #EQ cases(state_pc_eq … EQ) *
797                     #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
798                     <(insensitive_to_be_cleared_sb prog … st2)
799                     [2,4: @dead_registers_in_dead @acc_is_dead ]
800                     whd >point_of_pc_of_point
801                     @(eq_sigma_state_monotonicity … EQst1st2)
802                     letin after ≝ (analyse_liveness fix_comp … fn)
803                     letin before ≝ (livebefore … fn after)
804                     [2: change with lfalse in match (point_of_succ ???); ]
805                     lapply (included_livebefore_livebeafter_stmt_labels
806                      fix_comp … EQstmt)
807                     normalize in match (stmt_labels ???);
808                     change with after in match after;
809                     #H [ lapply (H lfalse ?) [ >memb_hd % ]
810                        | lapply (H ltrue ?) [ >memb_cons try % >memb_hd %]]
811                     #K change with (bool_to_Prop (rl_included ??)) in K;
812                     @(rl_included_transitive … K)
813                     whd in match (livebefore ????);
814                     whd in EQstmt; whd in EQstmt:(??%?);
815                     >EQstmt normalize nodelta
816                     @rl_included_rl_join_left
817                     normalize in match (defined ??);
818                     @rl_included_rl_diff_rl_empty ]
819            |*: % ]
820       |*: % ]
821  |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
822      >hw_reg_retrieve_write_decision_hit >m_return_bind
823      cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog …
824                                                        good fn … Rst1st2 … EQbv)
825        [2,4: @(all_used_are_live_before … EQstmt)
826            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
827        change with (prog_var_names … prog) in match (globals ?); >EQbv1
828        >EQbv' in EQbool; #EQbool
829        >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
830        normalize nodelta
831        [2: <(pc_eq_sigma_commute … good … EQfn Rst1st2) %]
832        whd in match goto; normalize nodelta
833        >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) %
834  ]
835| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
836  letin p_out ≝ (mk_prog_params LTL_semantics ??)
837  letin trans_prog ≝ (b_graph_transform_program ????)
838  #st1 #st1' #st2 #f #fn
839  #stms #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
840  normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
841  #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
842  #Heval_seq_no_pc
843  whd in match eval_statement_advance; normalize nodelta
844  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
845  whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
846  whd normalize nodelta
847  change with p_out in match p_out;
848  change with p_in in match p_in;
849  change with trans_prog in match trans_prog;
850  inversion eliminable_step #Heliminable normalize nodelta %
851  [ @([ ])
852  | % [%] % [2: % [%] | skip] whd
853    cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
854    % [2: % [2: % [%] | skip] | skip]
855    (* CSC: BEGIN cut&paste from previous case: make lemma? *)
856    lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
857    whd in match sigma_sb_state_pc; normalize nodelta >EQfn
858    <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
859    normalize nodelta #EQ cases(state_pc_eq … EQ) *
860    #EQst1st2 #_ #_
861    (* CSC: END *)
862    letin before ≝ (livebefore ???)
863    whd in match succ_pc; normalize nodelta >point_of_pc_of_point
864    whd in match (point_of_succ ???);
865    lapply(eq_sigma_state_monotonicity … nxt … EQst1st2)
866    [2: #X >X
867
868   
869    cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1)))
870    [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt
871      (* Ha funzionato solo a dx, non a sinistra...*)
872      normalize nodelta whd in match statement_semantics; normalize nodelta
873      >Heliminable
874     cases daemon (*CSC: Genuine proof obligation! *)
875    | #Hext ]
876    >(to_be_cleared_fb_respects_equal_valuations … Hext)
877    >(sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable)
878    >EQst1st2
879    >(to_be_cleared_sb_respects_equal_valuations … Hext) %
880|
881|
882 
883  XXXX
884 
885  *
886  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
887      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
888      #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
889      whd in match eval_seq_no_pc; normalize  nodelta
890      #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
891      #bv #EQbv #H @('bind_inversion H) -H #bv_op1 #EQbv_op1 #EQst1_no_pc
892      whd in match eval_statement_advance; normalize nodelta
893      whd in ⊢ (??%% → ?); #EQ destruct(EQ)
894      whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
895      whd normalize nodelta whd in match translate_op1;
896      normalize nodelta
897      change with p_out in match p_out;
898      change with p_in in match p_in;
899      change with trans_prog in match trans_prog;
900      inversion eliminable_step #Heliminable normalize nodelta %
901      [ @([ ])
902      | % [%] % [2: % [%] | skip] whd
903        cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
904        % [2: % [2: % [%] | skip] | skip]
905        (* CSC: BEGIN cut&paste from previous case: make lemma? *)
906        lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
907        whd in match sigma_sb_state_pc; normalize nodelta >EQfn
908        <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
909        normalize nodelta #EQ cases(state_pc_eq … EQ) *
910        #EQst1st2 #_ #_
911        (* CSC: END *)
912        <EQst1st2 whd in EQst1_no_pc:(??%%); <(injective_OK ??? EQst1_no_pc)
913        change with (set_regs ???) in match (st_no_pc ??);
914
915       
916       
917       
918       
919       
920       
921       
922         destruct (EQst1_no_pc)
923       
924        <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
925          (point_of_pc ERTLptr_semantics (pc … st2)))
926                     [2,4: @dead_registers_in_dead @acc_is_dead ]
927                     assumption
928     
929      Rst1st2
930     
931      % [2: % [ % | ] | skip]
932qed.
933
934
935lemma eval_cond_ok :
936∀fix_comp,colour.
937∀prog.
938∀ f_lbls,f_regs.∀f_bl_r.
939∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
940     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
941∀st1,st2,st1',f,fn,a,ltrue,lfalse.
942let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
943R st1 st2 →
944 fetch_statement ERTLptr_semantics …
945  (globalenv_noinit ? prog) (pc … st1) =
946    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
947let stacksizes ≝ lookup_stack_cost …
948                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 
949 eval_state ERTLptr_semantics
950   (prog_var_names … ℕ prog)
951   (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes))
952   st1 = return st1' →
953as_costed (ERTLptr_status prog stacksizes) st1' →
954∃ st2'. R st1' st2' ∧
955∃taf : trace_any_any_free (LTL_status ? ?)
956st2 st2'.
957bool_to_Prop (taaf_non_empty … taf).
958#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
959#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
960letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
961@(general_eval_cond_ok … good … Rst1st2 EQfetch EQeval)
962%
963[ #st1 #st2 #Rst1St2 >(pc_eq_sigma_commute … good … Rst1St2) %
964| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
965|
966
967
968
969whd in match eval_state; normalize nodelta
970>EQfetch >m_return_bind
971whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
972whd in match eval_statement_advance; normalize nodelta
973change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
974#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
975#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
976lapply(fetch_statement_inv … EQfetch) * #EQfn #_
977[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
978| whd in match next; normalize nodelta
979]
980whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
981cases(b_graph_transform_program_fetch_statement … good … EQfetch)
982#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
983[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
984[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
985whd in match translate_step; normalize nodelta *** #blp #blm #bls *
986whd in ⊢ (% → ?); #EQbl
987whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
988#seq_pre_l
989letin stacksizes ≝ (lookup_stack_cost …
990                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
991letin p≝ (mk_prog_params LTL_semantics
992                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
993                         stacksizes)
994cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
995           pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧
996           last_pop … st2' = last_pop … st2)
997   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
998#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
999>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
1000>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
1001whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
1002>EQ in EQmid ⊢ %; -nxt1 #EQmid
1003lapply(taaf_to_taa ???
1004           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
1005                                       seq_pre_l res_st2_pre_mid) ?)
1006[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
1007      whd in match (as_label ??); whd in match (as_pc_of ??);
1008      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
1009      >m_return_bind whd in match point_of_pc; normalize nodelta
1010      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
1011      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
1012#taa_pre_mid whd in ⊢ (% → ?);
1013cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
1014                     return st2_cond )
1015[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
1016#st2_mid #EQst2_mid
1017cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
1018[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
1019* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
1020letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
1021cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
1022%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
1023[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
1024     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
1025|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
1026]
1027qed.
1028
1029
1030theorem ERTLptrToLTL_ok :
1031∀fix_comp : fixpoint_computer.
1032∀colour : coloured_graph_computer.
1033∀p_in : ertlptr_program.
1034let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
1035let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
1036let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
1037(* what should we do with n? *)
1038let stacksizes ≝ lookup_stack_cost m in
1039∃[1] R.
1040  status_simulation
1041    (joint_status ERTLptr_semantics p_in stacksizes)
1042    (joint_status LTL_semantics p_out stacksizes)
1043    R.
1044#fix_comp #colour #p_in
1045cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
1046          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
1047#fregs * #f_lbls * #f_bl_r #good
1048%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
1049whd in match status_simulation; normalize nodelta
1050whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
1051whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
1052change with
1053  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 
1054#EQeval @('bind_inversion EQeval)
1055** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
1056#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
1057cases stmt in EQfetch; -stmt
1058[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
1059#EQfetch
1060change with (joint_classify ??) in
1061                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1062[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
1063  (* XXX
1064  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
1065  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
1066  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
1067  *) cases daemon
1068| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
1069          normalize nodelta #is_call_st1
1070          (* XXX
1071          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
1072          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
1073          #call_rel * #taa * #st2' * #sem_rel #eval_rel
1074          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
1075          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
1076          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
1077          *) cases daemon
1078| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
1079          normalize nodelta #n_costed
1080          cases(eval_cond_ok  … good … EQst2 … EQfetch EQeval … n_costed)
1081          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
1082          whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*)
1083| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
1084          normalize nodelta
1085          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
1086          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
1087          % [% //] whd >(as_label_ok … good … st3) [%]
1088          cases daemon (*needs lemma about preservation of fetch_statement *)
1089|  cases fin_step in EQfetch;
1090  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
1091     >EQfetch normalize nodelta
1092    cases (eval_goto_ok … good  … EQfetch EQeval)
1093    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
1094    % [% //] whd >(as_label_ok … good … st3) [%]
1095    cases daemon (*needs lemma about preservation of fetch_statement *)
1096  | (*RETURN*) #EQfetch
1097     whd in match joint_classify; normalize nodelta
1098    >EQfetch  normalize nodelta
1099    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
1100    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
1101    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
1102    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
1103    % [2: assumption] % [2: %] % [2: assumption] % assumption
1104  | (*TAILCALL*) *
1105  ]
1106]
1107
Note: See TracBrowser for help on using the repository browser.