source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2883

Last change on this file since 2883 was 2883, checked in by piccolo, 7 years ago

partial commit

File size: 29.0 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
24axiom sigma_stored_pc : ertlptr_program → (block → label → list label) → 
25program_counter → program_counter.
26
27
28definition clear_sb_type ≝ label → decision → bool.
29 
30axiom to_be_cleared_sb : 
31∀after : valuation register_lattice. coloured_graph after → clear_sb_type.
32
33definition clear_fb_type ≝ label → vertex → bool.
34
35axiom to_be_cleared_fb :
36∀after : valuation register_lattice.clear_fb_type.
37
38axiom sigma_fb_state: ertlptr_program → (block → label → list label) →
39 (block → label → list register) →
40 clear_fb_type → state ERTLptr_semantics → state ERTLptr_semantics.
41
42axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program.
43∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
44∀l.
45let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
46¬ lives (inr ? ? RegisterA) (livebefore  … fn l after).
47
48axiom dead_registers_in_dead :  ∀fix_comp.∀build : coloured_graph_computer.
49∀prog : ertlptr_program.
50∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
51∀l.
52let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
53let coloured_graph ≝ build … fn after in
54∀R : Register.
55¬ lives (inr ? ? R) (livebefore  … fn l after) →
56to_be_cleared_sb after coloured_graph l R.
57 
58axiom sigma_sb_state: ertlptr_program → (block → label → list label) →
59 (block → label → list register) → clear_sb_type → state LTL_semantics → state ERTLptr_semantics.
60
61definition dummy_state : state ERTLptr_semantics ≝
62mk_state ERTL_semantics
63   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
64
65definition dummy_state_pc : state_pc ERTLptr_semantics ≝
66mk_state_pc ? dummy_state (null_pc one) (null_pc one).
67
68
69definition sigma_fb_state_pc : fixpoint_computer → ertlptr_program →
70(block → label → list label) → (block → label → list register) →
71state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
72λfix_comp,prog,f_lbls,f_regs,st.
73let ge ≝ globalenv_noinit … prog in
74let globals ≝ prog_var_names … prog in
75match fetch_internal_function … ge (pc_block (pc … st)) with
76  [ OK y ⇒
77  let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
78  mk_state_pc ? (sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st) (pc … st) 
79                         (last_pop … st)
80  | Error e ⇒ dummy_state_pc
81  ].
82
83definition sigma_sb_state_pc :fixpoint_computer → coloured_graph_computer → 
84ertlptr_program → (block → label → list label) →
85(block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
86λfix_comp,build,prog,f_lbls,f_regs,st.
87let ge ≝ globalenv_noinit … prog in
88let globals ≝ prog_var_names … prog in
89match fetch_internal_function … ge (pc_block (pc … st)) with
90  [ OK y ⇒ 
91     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
92     let coloured_graph ≝ build … (\snd y) after in
93     mk_state_pc ? (sigma_sb_state prog f_lbls f_regs
94                          (to_be_cleared_sb after coloured_graph) st) (pc … st) 
95                          (sigma_stored_pc prog f_lbls (last_pop … st))
96  | Error e ⇒ dummy_state_pc
97  ].
98
99axiom write_decision : decision → beval → state LTL_LIN_state →
100state LTL_LIN_state.
101
102axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval.
103
104axiom insensitive_to_be_cleared_sb : ∀prog. ∀f_lbls : (block → label → list label).
105∀f_regs : (block → label → list register).∀tb : clear_sb_type.
106∀st : state LTL_LIN_state.∀lab.
107∀d : decision.∀bv.tb lab d →
108sigma_sb_state prog f_lbls f_regs tb st =
109sigma_sb_state prog f_lbls f_regs tb (write_decision d bv st).
110
111
112definition ERTLptr_to_LTL_StatusSimulation :
113∀fix_comp : fixpoint_computer.
114∀colour : coloured_graph_computer.
115∀ prog : ertlptr_program.
116∀ f_lbls. ∀ f_regs. ∀f_bl_r.
117b_graph_transform_program_props ERTLptr_semantics LTL_semantics
118     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
119let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
120let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
121let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
122let stacksizes ≝ lookup_stack_cost … m in 
123status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝
124λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r.λgood.
125    mk_status_rel ??
126    (* sem_rel ≝ *)
127         (λs1:ERTLptr_status ? ?
128          .λs2:LTL_status ? ?
129           .sigma_fb_state_pc fix_comp prog f_lbls f_regs s1
130            =sigma_sb_state_pc fix_comp colour prog f_lbls f_regs s2)
131    (* call_rel ≝ *) 
132       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
133          .λs2:Σs:LTL_status ??.as_classifier ? s cl_call
134           .pc ? s1 =sigma_stored_pc prog f_lbls (pc ? s2))
135    (* sim_final ≝ *) ?.
136cases daemon
137qed.
138
139axiom as_label_ok :
140∀fix_comp,colour.
141∀prog.∀f_lbls,f_regs. ∀f_bl_r.
142∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
143     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
144∀st1,st2,fn,id,stmt.
145let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
146R st1 st2 → 
147fetch_statement ERTLptr_semantics (prog_var_names … prog)
148      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
149as_label ? st2 = as_label ? st1.
150
151
152
153
154(*
155(* Copy the proof too from previous pass *)
156axiom fetch_stmt_ok_sigma_state_ok :
157∀prog : ertlptr_program.
158∀ f_lbls,f_regs,id,fn,stmt,st.
159fetch_statement ERTLptr_semantics (prog_var_names … prog)
160    (globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) =
161               return 〈id,fn,stmt〉 →
162let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn
163                                               (f_regs (pc_block (pc … st)))) in
164st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) =
165sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
166*)
167
168
169lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
170 #T #x #y #EQ destruct %
171qed.
172
173
174axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
175∀prog.∀ f_lbls,f_regs.∀f_bl_r.
176∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
177     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
178∀st1,st2.
179let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
180R st1 st2 →
181pc_block (pc … st1) = pc_block (pc … st2).
182
183
184axiom pc_eq_sigma_commute : ∀fix_comp,colour.
185∀prog.∀ f_lbls,f_regs.∀f_bl_r.
186∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
187     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
188∀st1,st2,f,fn,stmt.
189fetch_statement ERTLptr_semantics (prog_var_names … prog) (globalenv_noinit … prog)
190                (pc … st1) = return 〈f,fn,stmt〉 →
191let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
192R st1 st2 →
193(pc … st1) = (pc … st2).
194
195
196axiom change_pc_sigma_commute : ∀fix_comp,colour.
197∀prog.∀ f_lbls,f_regs.∀f_bl_r.
198∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
199     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
200∀st1,st2.
201let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
202R st1 st2 →
203∀pc1,pc2.pc1 = pc2 →
204R (set_pc … pc1 st1) (set_pc … pc2 st2).
205(*
206axiom globals_commute : ∀fix_comp,colour.
207∀prog.
208∀p_out,m,n.
209∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
210prog_var_names … prog = prog_var_names … p_out.*)
211
212lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
213〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
214#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
215qed.
216
217include "joint/semantics_blocks.ma".
218include "ASM/Util.ma".
219include "joint/StatusSimulationHelper.ma".
220
221
222axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
223∀st : state LTL_LIN_state.
224hw_reg_retrieve (regs … (write_decision r bv st)) r = return bv.
225
226axiom move_spec : ∀prog.∀stack_size.∀localss : nat.
227∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
228∀f : ident.
229∀s : state LTL_LIN_state.
230repeat_eval_seq_no_pc (mk_prog_params LTL_semantics prog stack_size) f
231   (move (prog_var_names … prog) localss carry_lives_after dest src) s =
232   return write_decision dest (read_arg_decision src s) s.
233
234axiom sigma_beval : ertlptr_program → (block → label → list label) →
235                    beval → beval.
236 
237
238axiom ps_reg_retrieve_hw_reg_retrieve_commute :
239∀fix_comp,colour,prog.
240∀ f_lbls,f_regs.∀f_bl_r.
241∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
242 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
243∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
244let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
245let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
246∀st1 : state_pc ERTL_state.
247∀st2 : state_pc LTL_LIN_state.
248∀bv.
249∀r : register.R st1 st2 →
250lives (inl ? ? r) (livebefore  … fn (point_of_pc ERTLptr_semantics (pc … st1)) after) →
251ps_reg_retrieve (regs … st1) r = return bv →
252∃bv'.bv = sigma_beval prog f_lbls bv' ∧
253read_arg_decision (colouring after (colour (prog_var_names … prog) fn after)
254                                            (inl register Register r))
255                              st2 = bv'.
256                             
257axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
258axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
259axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
260set_member A DEC a (set_union … x y).
261axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
262set_member A DEC a (set_union … x y).
263axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
264¬set_member A DEC a y →
265set_member A DEC a (set_diff … x y).
266
267
268lemma all_used_are_live_before :
269∀fix_comp.
270∀prog : ertlptr_program.
271∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
272∀l,stmt.
273stmt_at … (joint_if_code … fn) l = return stmt →
274∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
275let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
276eliminable ? (after l) stmt = None ? →
277lives (inl ? ? r)  (livebefore  … fn l after).
278#fix_comp #prog #fn #l *
279[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
280[ #str
281| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
282| #a
283| * [ #r | #b]
284| #i #i_spec #dpl #dph
285| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
286| #op #a #a'
287| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
288|
289|
290| #a #dpl #dph
291| #dpl #dph #a
292| * [ * [|| #r] | #r #lbl | #r #lbl ]
293]
294] #nxt| * [ #lbl | | *] |*]
295#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
296whd in match (livebefore ????); whd in EQstmt : (??%?); >EQstmt
297normalize nodelta -EQstmt whd in match (statement_semantics ???);
298whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
299normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
300qed.
301
302axiom bool_of_beval_sigma_commute :
303∀prog.∀f_lbls.∀bv,b.
304bool_of_beval (sigma_beval prog f_lbls bv) = return b →
305bool_of_beval bv = return b.
306
307lemma map_eval_add_dummy_variance_id :
308∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
309#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
310qed.
311
312lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
313st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
314pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
315#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
316%{(refl …)} %{(refl …)} %
317qed.
318(*
319axiom dead_is_to_be_clear :
320*)
321
322(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
323lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
324∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
325#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
326whd in ⊢ (??%? → ?); #EQ >EQ %
327qed.
328
329lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
330 OptPred True (λres.
331  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
332  (split_on_last … l2).
333#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
334#hd #tl #IH #l1 whd >split_on_last_append_singl whd
335<associative_append @split_on_last_append_singl
336qed.
337
338lemma make_ERTLptr_To_LTL_good_state_relation :
339∀fix_comp,colour,prog.
340let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
341let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
342let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
343let stacksizes ≝ lookup_stack_cost … m in
344∃init_regs : block → list register.
345∃f_lbls : block → label → list label.
346∃f_regs : block → label → list register.
347∃good : b_graph_transform_program_props ERTLptr_semantics LTL_semantics
348        (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
349        prog init_regs f_lbls f_regs.
350good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
351 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
352 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
353#fix_comp #colour #prog
354cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
355          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog)
356#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
357%
358[ #st1 #st2 #f #fn #stmt #Rst1st2 #EQstmt >(pc_eq_sigma_commute … good … EQstmt Rst1st2) %
359| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
360| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
361  #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc;
362  normalize nodelta
363  >EQfetch >m_return_bind normalize nodelta >m_return_bind
364  whd in match eval_statement_advance; normalize nodelta
365  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
366  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
367  #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
368  cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
369  [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
370    >m_return_bind ] whd in ⊢ (??%% → ?); #EQ destruct(EQ) #Rst1st2
371  #t_fn1 #EQt_fn1 whd normalize nodelta
372  letin trans_prog ≝ (b_graph_transform_program ????)
373  letin stacksizes ≝ (lookup_stack_cost ?)
374  letin prog_pars_in ≝ (mk_prog_params ERTLptr_semantics ??)
375  letin prog_pars_out ≝ (mk_prog_params LTL_semantics ??) %{(refl …)}
376  #mid #EQmid
377  letin st2_pre_mid_no_pc ≝
378  (write_decision RegisterA
379          (read_arg_decision
380              (colouring
381                  (analyse_liveness fix_comp (globals prog_pars_in) fn)
382                  (colour (globals prog_pars_in) fn
383                  (analyse_liveness fix_comp (globals prog_pars_in) fn))
384              (inl register Register a)) st2) st2)
385  %{st2_pre_mid_no_pc}
386  %
387  [1,3: >map_eval_add_dummy_variance_id @move_spec]
388  % [1,3: % %] %{(mk_state_pc ? st2_pre_mid_no_pc
389                       (pc_of_point LTL_semantics (pc_block (pc … st2)) ?)
390                        (last_pop … st2))} [@ltrue |3: @lfalse]
391  change with prog_pars_out in match (mk_prog_params ???); %
392  [1,3: whd in match eval_state; whd in match eval_statement_no_pc;
393        whd in match fetch_statement; normalize nodelta
394       >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
395        normalize nodelta >m_return_bind
396        change with prog_pars_out in match (mk_prog_params ???);
397        whd in match eval_statement_advance; normalize nodelta
398        change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
399        whd in match set_no_pc; normalize nodelta
400        >hw_reg_retrieve_write_decision_hit >m_return_bind
401        cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog … good fn … Rst1st2 … EQbv)
402        [2,4: @(all_used_are_live_before … EQstmt)
403            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
404        change with (prog_var_names … prog) in match (globals ?); >EQbv1
405        >EQbv' in EQbool; #EQbool
406        >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
407        normalize nodelta [2: %] whd in match goto; normalize nodelta
408        >(pc_of_label_eq … EQt_fn1) %
409  |2,4: whd whd in match sigma_fb_state_pc; normalize nodelta
410        whd in match sigma_sb_state_pc; normalize nodelta
411        change with (pc_block (pc … st1)) in match (pc_block ?);
412        cases(fetch_statement_inv … EQfetch) #EQfn #_ >EQfn
413        normalize nodelta <(pc_eq_sigma_commute … good … EQfetch Rst1st2)
414        change with (pc_block (pc … st1)) in ⊢ (???match (???%) with [_⇒ ? | _ ⇒ ?]);
415        >EQfn normalize nodelta
416        lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
417         whd in match sigma_sb_state_pc; normalize nodelta >EQfn
418         <(pc_eq_sigma_commute … good … EQfetch Rst1st2) >EQfn normalize nodelta
419         #EQ cases(state_pc_eq … EQ) * #EQst1st2 #EQpc #EQlp @eq_f3
420        [3,6:  assumption
421        |2,5: %
422        |*: <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
423               (point_of_pc ERTLptr_semantics (pc … st2)))
424            [2,4: @dead_registers_in_dead @acc_is_dead ]
425            assumption
426        ]
427  ]
428| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
429  letin p_out ≝ (mk_prog_params LTL_semantics ??)
430  letin trans_prog ≝ (b_graph_transform_program ????)
431  #st1 #st1' #st2 #f #fn *
432  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
433      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
434      #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
435      whd in match eval_seq_no_pc; normalize  nodelta
436      #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
437      #bv #EQbv #H @('bind_inversion H) -H #bv_op1 #EQbv_op1 #EQst1_no_pc
438      whd in match eval_statement_advance; normalize nodelta
439      whd in ⊢ (??%% → ?); #EQ destruct(EQ)
440      whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
441      whd normalize nodelta whd in match translate_op1;
442      normalize nodelta
443      change with p_out in match p_out;
444      change with p_in in match p_in;
445      change with trans_prog in match trans_prog;
446      #mid #mid1 #EQmid % [%]
447      [ cases (andb ??) whd in match (preserve_carry_bit ???);
448        whd in match ensure_step_block; normalize nodelta
449        XXX
450     
451     
452      whd normalize nodelta
453      change with p_out in match p_out;
454      change with p_in in match p_in;
455      change with trans_prog in match trans_prog;
456      letin coloured_dst ≝ (colouring ???)
457      letin coloured_src ≝ (colouring ???)
458      whd in match translate_op1; normalize nodelta
459
460
461
462      whd in match (translate_op1 ?????);
463      change with (bind_new_P' ? (? × ?) ?
464       (f_step ERTLptr_semantics ?????));
465      whd in match (translate_data ????);
466      change with (bind_new_P' ??? (f_step ??????));
467      whd in match (f_step ??????);
468      @(λH.H)
469     
470      whd in match (  #mid whd #
471 
472
473qed.
474
475
476lemma eval_cond_ok :
477∀fix_comp,colour.
478∀prog.
479∀ f_lbls,f_regs.∀f_bl_r.
480∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
481     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
482∀st1,st2,st1',f,fn,a,ltrue,lfalse.
483let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
484R st1 st2 →
485 fetch_statement ERTLptr_semantics …
486  (globalenv_noinit ? prog) (pc … st1) =
487    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
488let stacksizes ≝ lookup_stack_cost …
489                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 
490 eval_state ERTLptr_semantics
491   (prog_var_names … ℕ prog)
492   (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes))
493   st1 = return st1' →
494as_costed (ERTLptr_status prog stacksizes) st1' →
495∃ st2'. R st1' st2' ∧
496∃taf : trace_any_any_free (LTL_status ? ?)
497st2 st2'.
498bool_to_Prop (taaf_non_empty … taf).
499#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
500#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
501letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
502@(general_eval_cond_ok … good … Rst1st2 EQfetch EQeval)
503%
504[ #st1 #st2 #Rst1St2 >(pc_eq_sigma_commute … good … Rst1St2) %
505| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
506|
507
508
509
510whd in match eval_state; normalize nodelta
511>EQfetch >m_return_bind
512whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
513whd in match eval_statement_advance; normalize nodelta
514change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
515#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
516#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
517lapply(fetch_statement_inv … EQfetch) * #EQfn #_
518[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
519| whd in match next; normalize nodelta
520]
521whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
522cases(b_graph_transform_program_fetch_statement … good … EQfetch)
523#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
524[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
525[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
526whd in match translate_step; normalize nodelta *** #blp #blm #bls *
527whd in ⊢ (% → ?); #EQbl
528whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
529#seq_pre_l
530letin stacksizes ≝ (lookup_stack_cost …
531                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
532letin p≝ (mk_prog_params LTL_semantics
533                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
534                         stacksizes)
535cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
536           pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧
537           last_pop … st2' = last_pop … st2)
538   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
539#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
540>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
541>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
542whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
543>EQ in EQmid ⊢ %; -nxt1 #EQmid
544lapply(taaf_to_taa ???
545           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
546                                       seq_pre_l res_st2_pre_mid) ?)
547[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
548      whd in match (as_label ??); whd in match (as_pc_of ??);
549      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
550      >m_return_bind whd in match point_of_pc; normalize nodelta
551      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
552      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
553#taa_pre_mid whd in ⊢ (% → ?);
554cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
555                     return st2_cond )
556[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
557#st2_mid #EQst2_mid
558cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
559[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
560* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
561letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
562cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
563%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
564[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
565     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
566|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
567]
568qed.
569
570
571theorem ERTLptrToLTL_ok :
572∀fix_comp : fixpoint_computer.
573∀colour : coloured_graph_computer.
574∀p_in : ertlptr_program.
575let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
576let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
577let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
578(* what should we do with n? *)
579let stacksizes ≝ lookup_stack_cost m in
580∃[1] R.
581  status_simulation
582    (joint_status ERTLptr_semantics p_in stacksizes)
583    (joint_status LTL_semantics p_out stacksizes)
584    R.
585#fix_comp #colour #p_in
586cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
587          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
588#fregs * #f_lbls * #f_bl_r #good
589%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
590whd in match status_simulation; normalize nodelta
591whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
592whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
593change with
594  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 
595#EQeval @('bind_inversion EQeval)
596** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
597#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
598cases stmt in EQfetch; -stmt
599[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
600#EQfetch
601change with (joint_classify ??) in
602                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
603[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
604  (* XXX
605  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
606  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
607  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
608  *) cases daemon
609| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
610          normalize nodelta #is_call_st1
611          (* XXX
612          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
613          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
614          #call_rel * #taa * #st2' * #sem_rel #eval_rel
615          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
616          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
617          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
618          *) cases daemon
619| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
620          normalize nodelta #n_costed
621          cases(eval_cond_ok  … good … EQst2 … EQfetch EQeval … n_costed)
622          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
623          whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*)
624| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
625          normalize nodelta
626          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
627          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
628          % [% //] whd >(as_label_ok … good … st3) [%]
629          cases daemon (*needs lemma about preservation of fetch_statement *)
630|  cases fin_step in EQfetch;
631  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
632     >EQfetch normalize nodelta
633    cases (eval_goto_ok … good  … EQfetch EQeval)
634    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
635    % [% //] whd >(as_label_ok … good … st3) [%]
636    cases daemon (*needs lemma about preservation of fetch_statement *)
637  | (*RETURN*) #EQfetch
638     whd in match joint_classify; normalize nodelta
639    >EQfetch  normalize nodelta
640    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
641    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
642    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
643    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
644    % [2: assumption] % [2: %] % [2: assumption] % assumption
645  | (*TAILCALL*) *
646  ]
647]
648
Note: See TracBrowser for help on using the repository browser.