source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2898

Last change on this file since 2898 was 2898, checked in by piccolo, 8 years ago

1) simplification of cond and seq case for StatusSimulationHelper? which has
been tested correct in ERTL to ERTlptr correctness proof.

2) the cond case for ERTLptr to LTL correctenss proof has been adapted to the
new specification

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