source: src/joint/StatusSimulationHelper.ma @ 2855

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

little bug fixed in TranslateUtils?.

File size: 6.9 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "joint/semanticsUtils.ma".
16include "joint/Traces.ma".
17include "common/StatusSimulation.ma".
18include "joint/semantics_blocks.ma".
19
20lemma set_no_pc_eta:
21 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
22#P * //
23qed.
24
25lemma pc_of_label_eq :
26  ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
27  ∀globals,ge,bl,i_fn,lbl.
28  fetch_internal_function ? ge bl = return i_fn →
29  pc_of_label pars globals ge bl lbl =
30    OK ? (pc_of_point pars bl lbl).
31#p #p' #globals #ge #bl #i_fn #lbl #EQf
32whd in match pc_of_label;
33normalize nodelta >EQf >m_return_bind %
34qed.
35
36
37lemma bind_new_bind_new_instantiates :
38∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P.
39bind_new_instantiates B X x m l → bind_new_P' ?? P m →
40P l x.
41#B #X #m elim m normalize nodelta
42[#x #y * normalize // #B #l' #P *
43| #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H)
44 @Hr
45]
46qed.
47
48
49lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
50∀prog : joint_program P_in.
51∀stack_sizes.
52∀ f_lbls,f_regs.∀f_bl_r.∀init.
53∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
54let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
55let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
56let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
57∀st1,st1' : joint_abstract_status prog_pars_in.
58∀st2 : joint_abstract_status prog_pars_out.
59∀f,fn,a,ltrue,lfalse.
60∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
61R st1 st2 →
62let step ≝ (COND P_in ? a ltrue) in
63bind_new_P' ??
64 (λregs1.λdata.∀lbl.bind_new_P' ??
65  (λregs2.λblp.
66   (∀mid1.∃st2'.
67     repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? (\fst (\fst blp)) mid1) (st_no_pc … st2)
68     = return (st_no_pc … st2') ∧
69     pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
70     last_pop … st2' = last_pop … st2)
71   ) (f_step ??? data lbl step)   
72  ) (init ? fn) →
73 fetch_statement P_in …
74  (globalenv_noinit ? prog) (pc … st1) =
75    return 〈f, fn,  sequential … step lfalse〉 →
76 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
77            st1 = return st1' →
78as_costed (joint_abstract_status prog_pars_in) st1' →
79∃ st2'. R st1' st2' ∧
80∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
81bool_to_Prop (taaf_non_empty … taf).
82#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st1 #st1' #st2
83#f #fn #a #ltrue #lfalse #R #Rst1st2 #Hb_graph #EQfetch whd in match eval_state; normalize nodelta
84>EQfetch >m_return_bind
85whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
86whd in match eval_statement_advance; normalize nodelta
87#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
88#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
89lapply(fetch_statement_inv … EQfetch) * #EQfn #_
90[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
91| whd in match next; normalize nodelta
92]
93whd in ⊢ (??%% → ?); #EQ destruct(EQ) #n_cost
94cases(b_graph_transform_program_fetch_statement … good … EQfetch)
95#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); #Hinit (*cases (f_bl_r ?) normalize nodelta
96[2,4: #r #tl] whd in ⊢ (%→?); #EQ >EQ -init_data
97>if_merge_right in ⊢ (% → ?); [2,4: %] *)
98* #labs * #regs
99(*[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *]*)
100** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls *
101whd in ⊢ (% → ?); #EQbl
102whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
103#seq_pre_l
104letin trans_prog  ≝ (b_graph_transform_program P_in P_out init prog)
105letin prog_pars_out ≝ (mk_prog_params P_out trans_prog stack_sizes)
106cases(? : ∃st2'.
107           repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2)
108           = return (st_no_pc … st2') ∧
109           pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
110           last_pop … st2' = last_pop … st2)
111   [2,4: assumption ]
112#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
113>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
114>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
115whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
116>EQ in EQmid ⊢ %; -nxt1 #EQmid
117lapply(taaf_to_taa ???
118           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
119                                       seq_pre_l res_st2_pre_mid) ?)
120[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
121      whd in match (as_label ??); whd in match (as_pc_of ??);
122      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
123      >m_return_bind whd in match point_of_pc; normalize nodelta
124      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
125      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
126#taa_pre_mid whd in ⊢ (% → ?);
127cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
128                     return st2_cond )
129[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
130#st2_mid #EQst2_mid
131cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
132[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
133* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
134letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
135cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
136%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
137[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
138     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
139|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
140]
141qed.*)
Note: See TracBrowser for help on using the repository browser.