source: src/joint/StatusSimulationHelper.ma @ 2891

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

added precondition on seq statement and tested correct in the ERTl-ERTLptr passed

File size: 13.3 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
48record good_state_relation (P_in : sem_graph_params)
49   (P_out : sem_graph_params) (prog : joint_program P_in)
50   (stack_sizes : ident → option ℕ)
51   (init : ∀globals.joint_closed_internal_function P_in globals
52         →bound_b_graph_translate_data P_in P_out globals)
53   (R : joint_abstract_status (mk_prog_params P_in prog stack_sizes) →
54        joint_abstract_status (mk_prog_params P_out
55                                (b_graph_transform_program P_in P_out init prog)
56                                stack_sizes)
57        → Prop) : Prop ≝
58{ pc_eq_sigma_commute : ∀st1,st2,f,fn,stmt.R st1 st2 →
59                 fetch_statement ? (prog_var_names … prog)
60                     (globalenv_noinit … prog) (pc … st1)  = return 〈f,fn,stmt〉 →
61                 pc … st1 = pc … st2
62; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes).
63                ∀st2 : joint_abstract_status ?.
64                ∀f,fn,stmt.
65                  fetch_statement ? (prog_var_names … prog)
66                  (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 →
67                  R st1 st2 → as_label ? st1 = as_label ? st2
68; cond_commutation :
69    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
70    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
71    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
72    ∀f,fn,a,ltrue,lfalse.
73    let cond ≝ (COND P_in ? a ltrue) in
74    fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
75    return 〈f, fn,  sequential … cond lfalse〉 → 
76    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
77    st1 = return st1' →
78    R st1 st2 →
79    ∀t_fn.
80    fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
81    return 〈f,t_fn〉 →
82    bind_new_P' ??
83     (λregs1.λdata.bind_new_P' ??
84     (λregs2.λblp.(\snd blp) = [ ] ∧
85        ∀mid.
86          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
87          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
88         ∃st2_pre_mid_no_pc.
89            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid)
90                                   (st_no_pc ? st2)
91            = return st2_pre_mid_no_pc ∧
92            let st2_pre_mid ≝ mk_state_pc ? st2_pre_mid_no_pc (pc_of_point P_out (pc_block (pc … st2)) mid)
93                                            (last_pop … st2) in
94            joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
95                                ((\snd (\fst blp)) mid)  = cl_jump ∧
96            cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
97                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
98            ∃st2_mid .
99                eval_state P_out (prog_var_names … trans_prog)
100                (ev_genv (mk_prog_params P_out trans_prog stack_sizes)) st2_pre_mid =
101                return st2_mid ∧ R st1' st2_mid
102   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
103  ) (init ? fn)
104; seq_commutation :
105  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
106  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
107  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
108  ∀f,fn,stmt,nxt.
109  let seq ≝ (step_seq P_in ? stmt) in
110  fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
111  return 〈f, fn,  sequential … seq nxt〉 → 
112  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
113  st1 = return st1' →
114  R st1 st2 →
115  ∀t_fn.
116  fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
117  return 〈f,t_fn〉 →
118  bind_new_P' ??
119     (λregs1.λdata.bind_new_P' ??
120     (λregs2.λblp.
121       ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes)
122                            (globals (mk_prog_params P_out trans_prog stack_sizes))).
123                            blp = (ensure_step_block ?? l) ∧
124       ∃st2_fin_no_pc.
125           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
126              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
127           let st2_fin ≝
128           mk_state_pc ? st2_fin_no_pc
129                         (pc_of_point P_out (pc_block(pc … st2)) nxt)
130                         (last_pop … st2) in
131           R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
132      ) (init ? fn)         
133}.
134
135lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
136∀prog : joint_program P_in.
137∀stack_sizes.
138∀ f_lbls,f_regs.∀f_bl_r.∀init.
139∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
140let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
141let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
142let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
143∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
144good_state_relation P_in P_out prog stack_sizes init R →
145∀st1,st1' : joint_abstract_status prog_pars_in.
146∀st2 : joint_abstract_status prog_pars_out.
147∀f.
148∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
149∀a,ltrue,lfalse.
150R st1 st2 →
151    let cond ≝ (COND P_in ? a ltrue) in
152 fetch_statement P_in …
153  (globalenv_noinit ? prog) (pc … st1) =
154    return 〈f, fn,  sequential … cond lfalse〉 →
155 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
156            st1 = return st1' →
157as_costed (joint_abstract_status prog_pars_in) st1' →
158∃ st2'. R st1' st2' ∧
159∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
160bool_to_Prop (taaf_non_empty … taf).
161#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' #st2
162#f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed
163cases(b_graph_transform_program_fetch_statement … good … EQfetch)
164#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
165#EQt_fn1 whd in ⊢ (% → ?); #Hinit
166* #labs * #regs
167** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls *
168whd in ⊢ (% → ?); @if_elim
169[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
170  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
171  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
172  normalize nodelta whd in match (point_of_offset ??); <ABS
173  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
174]
175#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
176* #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
177* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
178cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
179               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
180#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
181cases(APP … EQmid) -APP
182#st_pre_mid_no_pc * #EQst_pre_mid_no_pc ** #CL_JUMP #COST *
183#st2_mid * #EQst2mid #Hst2_mid %{st2_mid} %{Hst2_mid}
184>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
185lapply(taaf_to_taa ???
186           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
187                                       seq_pre_l EQst_pre_mid_no_pc) ?)
188[ @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
189  whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
190  whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
191  >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
192  #H @H %
193] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
194[ whd <(as_label_ok … goodR … Hst2_mid) [assumption] cases daemon (*TODO: general lemma!*)
195| whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
196  >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
197  assumption
198| assumption
199]
200qed.
201
202(*
203let rec taa_to_taaf  S st1 st2 (taa : trace_any_any S st1 st2) on taa :
204trace_any_any_free S st1 st2 ≝
205(match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with
206[taa_base st1' ⇒ λprf.?
207|taa_step st1' st2' st3' H I J tl ⇒ λprf.?
208]) (refl … st1) (refl … st2) (refl_jmeq ? taa).
209*)
210
211lemma general_eval_seq_no_call_ok : ∀ P_in , P_out: sem_graph_params.
212∀prog : joint_program P_in.
213∀stack_sizes.
214∀ f_lbls,f_regs.∀f_bl_r.∀init.
215∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
216let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
217let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
218let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
219∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
220good_state_relation P_in P_out prog stack_sizes init R →
221∀st1,st1' : joint_abstract_status prog_pars_in.
222∀st2 : joint_abstract_status prog_pars_out.
223∀f.
224∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
225∀stmt,nxt.
226R st1 st2 →
227    let seq ≝ (step_seq P_in ? stmt) in
228 fetch_statement P_in …
229  (globalenv_noinit ? prog) (pc … st1) =
230    return 〈f, fn,  sequential ?? seq nxt〉 →
231 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
232            st1 = return st1' →
233∃st2'. R st1' st2' ∧           
234∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
235 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
236(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
237 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
238#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1'
239#st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
240cases(b_graph_transform_program_fetch_statement … good … EQfetch)
241#init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
242#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim
243[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
244  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
245  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
246  normalize nodelta whd in match (point_of_offset ??); <ABS
247  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
248]
249#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl
250>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC
251cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
252               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
253#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
254%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
255%{Rsem} 
256%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
257                                      SBiC EQst2_fin_no_pc)}
258@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
259qed.
Note: See TracBrowser for help on using the repository browser.