source: src/joint/StatusSimulationHelper.ma @ 2883

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

partial commit

File size: 17.2 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
49definition step_to_seq : ∀p : prog_params.∀stmt : joint_step p (globals p).
50joint_classify_step p stmt = cl_other →
51(∀c.stmt ≠ COST_LABEL ?? c) → Σ seq.stmt = step_seq ?? seq ≝
52λp,stmt,CL_OTHER,COST.
53(match stmt return λx.x = stmt → ? with
54[ COST_LABEL c ⇒ λprf.⊥
55| CALL id args dest ⇒ λprf.⊥
56| COND r lab ⇒ λprf.⊥
57| step_seq seq ⇒ λprf.«seq,?»
58])(refl …).
59@hide_prf
60[ lapply(COST c) * #H @H >prf %
61|2,3: <prf in CL_OTHER; whd in match (joint_classify_step ??); #EQ destruct(EQ)
62| >prf %
63]
64qed.
65 
66
67record good_state_relation (P_in : sem_graph_params)
68   (P_out : sem_graph_params) (prog : joint_program P_in)
69   (stack_sizes : ident → option ℕ)
70   (init : ∀globals.joint_closed_internal_function P_in globals
71         →bound_b_graph_translate_data P_in P_out globals)
72   (R : joint_abstract_status (mk_prog_params P_in prog stack_sizes) →
73        joint_abstract_status (mk_prog_params P_out
74                                (b_graph_transform_program P_in P_out init prog)
75                                stack_sizes)
76        → Prop) : Prop ≝
77{ pc_eq_sigma_commute : ∀st1,st2,f,fn,stmt.R st1 st2 →
78                 fetch_statement ? (prog_var_names … prog)
79                     (globalenv_noinit … prog) (pc … st1)  = return 〈f,fn,stmt〉 →
80                 pc … st1 = pc … st2
81; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes).
82                ∀st2 : joint_abstract_status ?.
83                ∀f,fn,stmt.
84                  fetch_statement ? (prog_var_names … prog)
85                  (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 →
86                  R st1 st2 → as_label ? st1 = as_label ? st2
87; cond_commutation :
88    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
89    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
90    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
91    ∀f,fn,a,ltrue,lfalse.
92    let cond ≝ (COND P_in ? a ltrue) in
93    fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
94    return 〈f, fn,  sequential … cond lfalse〉 → 
95    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
96    st1 = return st1' →
97    R st1 st2 →
98    ∀t_fn.
99    fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
100    return 〈f,t_fn〉 →
101    bind_new_P' ??
102     (λregs1.λdata.bind_new_P' ??
103     (λregs2.λblp.(\snd blp) = [ ] ∧
104        ∀mid.
105          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
106          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
107         ∃st2_pre_mid_no_pc.
108            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid)
109                                   (st_no_pc ? st2)
110            = return st2_pre_mid_no_pc ∧
111            let st2_pre_mid ≝ mk_state_pc ? st2_pre_mid_no_pc (pc_of_point P_out (pc_block (pc … st2)) mid)
112                                            (last_pop … st2) in
113            joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
114                                ((\snd (\fst blp)) mid)  = cl_jump ∧
115            cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
116                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
117            ∃st2_mid .
118                eval_state P_out (prog_var_names … trans_prog)
119                (ev_genv (mk_prog_params P_out trans_prog stack_sizes)) st2_pre_mid =
120                return st2_mid ∧ R st1' st2_mid
121   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
122  ) (init ? fn)
123; seq_commutation :
124  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
125  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
126  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
127  ∀f,fn,stmt,nxt.
128  let seq ≝ (step_seq P_in ? stmt) in
129  fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
130  return 〈f, fn,  sequential … seq nxt〉 → 
131  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
132  st1 = return st1' →
133  R st1 st2 →
134  ∀t_fn.
135  fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
136  return 〈f,t_fn〉 →
137  bind_new_P' ??
138     (λregs1.λdata.bind_new_P' ??
139     (λregs2.λblp.
140           ∀mid,mid1.
141            stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
142            = return sequential P_out ? ((\snd (\fst blp)) mid) mid1→
143            ∃CL_OTHER : joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
144                          ((\snd (\fst blp)) mid)  = cl_other.
145            ∃COST : cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
146                         (sequential P_out ? ((\snd (\fst blp)) mid) mid1) = None ?.
147            ∃st2_fin_no_pc.
148            let pre ≝ (map_eval ?? (\fst (\fst blp)) mid) in
149            let middle ≝ [pi1 ?? (step_to_seq (mk_prog_params P_out trans_prog stack_sizes)
150                                  ((\snd (\fst blp)) mid) CL_OTHER ?)] in
151           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
152              (pre@ middle @ (\snd blp))  (st_no_pc … st2)= return st2_fin_no_pc ∧
153           let st2_fin ≝
154           mk_state_pc ? st2_fin_no_pc
155                         (pc_of_point P_out (pc_block(pc … st2)) nxt)
156                         (last_pop … st2) in
157           R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
158      ) (init ? fn)         
159}.
160@hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
161qed.
162
163lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
164∀prog : joint_program P_in.
165∀stack_sizes.
166∀ f_lbls,f_regs.∀f_bl_r.∀init.
167∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
168let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
169let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
170let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
171∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
172good_state_relation P_in P_out prog stack_sizes init R →
173∀st1,st1' : joint_abstract_status prog_pars_in.
174∀st2 : joint_abstract_status prog_pars_out.
175∀f.
176∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
177∀a,ltrue,lfalse.
178R st1 st2 →
179    let cond ≝ (COND P_in ? a ltrue) in
180 fetch_statement P_in …
181  (globalenv_noinit ? prog) (pc … st1) =
182    return 〈f, fn,  sequential … cond lfalse〉 →
183 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
184            st1 = return st1' →
185as_costed (joint_abstract_status prog_pars_in) st1' →
186∃ st2'. R st1' st2' ∧
187∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
188bool_to_Prop (taaf_non_empty … taf).
189#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' #st2
190#f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed
191cases(b_graph_transform_program_fetch_statement … good … EQfetch)
192#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
193#EQt_fn1 whd in ⊢ (% → ?); #Hinit
194* #labs * #regs
195** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls *
196whd in ⊢ (% → ?); @if_elim
197[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
198  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
199  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
200  normalize nodelta whd in match (point_of_offset ??); <ABS
201  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
202]
203#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
204* #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
205* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
206cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
207               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
208#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
209cases(APP … EQmid) -APP
210#st_pre_mid_no_pc * #EQst_pre_mid_no_pc ** #CL_JUMP #COST *
211#st2_mid * #EQst2mid #Hst2_mid %{st2_mid} %{Hst2_mid}
212>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
213lapply(taaf_to_taa ???
214           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
215                                       seq_pre_l EQst_pre_mid_no_pc) ?)
216[ @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
217  whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
218  whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
219  >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
220  #H @H %
221] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
222[ whd <(as_label_ok … goodR … Hst2_mid) [assumption] cases daemon (*TODO: general lemma!*)
223| whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
224  >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
225  assumption
226| assumption
227]
228qed.
229
230(*
231let rec taa_to_taaf  S st1 st2 (taa : trace_any_any S st1 st2) on taa :
232trace_any_any_free S st1 st2 ≝
233(match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with
234[taa_base st1' ⇒ λprf.?
235|taa_step st1' st2' st3' H I J tl ⇒ λprf.?
236]) (refl … st1) (refl … st2) (refl_jmeq ? taa).
237*)
238
239lemma general_eval_seq_no_call_ok : ∀ P_in , P_out: sem_graph_params.
240∀prog : joint_program P_in.
241∀stack_sizes.
242∀ f_lbls,f_regs.∀f_bl_r.∀init.
243∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
244let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
245let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
246let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
247∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
248good_state_relation P_in P_out prog stack_sizes init R →
249∀st1,st1' : joint_abstract_status prog_pars_in.
250∀st2 : joint_abstract_status prog_pars_out.
251∀f.
252∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
253∀stmt,nxt.
254R st1 st2 →
255    let seq ≝ (step_seq P_in ? stmt) in
256 fetch_statement P_in …
257  (globalenv_noinit ? prog) (pc … st1) =
258    return 〈f, fn,  sequential ?? seq nxt〉 →
259 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
260            st1 = return st1' →
261∃st2'. R st1' st2' ∧           
262∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
263 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
264(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
265 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
266#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1'
267#st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
268cases(b_graph_transform_program_fetch_statement … good … EQfetch)
269#init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
270#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta ***
271#blp #blm #bls * @if_elim
272[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
273  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
274  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
275  normalize nodelta whd in match (point_of_offset ??); <ABS
276  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
277]
278#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl
279>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC lapply SBiC
280whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
281#_ whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
282#_
283cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
284               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
285[4: @EQmid |*:] #COST * #CL_OTHER * #st2_fin_no_pc normalize nodelta cases(step_to_seq ????)
286    #seq_mid cases daemon (*TODO*)
287    qed.
288   
289(*   
290    cases(blm mid1) in
291#stmt_at_middle #EQstmt_at_middle normalize nodelta * >EQstmt_at_middle in SBiC;  destruct(EQ) whd in ⊢ (??%% → ?);#EQ destruct(EQ)
292
293
294* #EQst2_pre_mid_no_pc
295* #st2_mid * #EQst2_mid * #st2_fin_no_pc * #EQst2_fin_no_pc #Hfin
296%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
297%{Hfin}
298lapply(taaf_to_taa ???
299           (produce_trace_any_any_free ? st2 f t_fn ??? st2_pre_mid_no_pc EQt_fn
300                                       seq_pre_l EQst2_pre_mid_no_pc) ?)
301[ @if_elim #_ [2: @I] % whd in match as_costed; normalize nodelta
302  whd in match (as_label ??); whd in match fetch_statement; normalize nodelta
303  >EQt_fn >m_return_bind whd in match (as_pc_of ??); whd in match point_of_pc;
304  normalize nodelta >point_of_offset_of_point >EQmid >m_return_bind
305  normalize nodelta >COST * #H @H %]
306#taa1
307letin st2_mid_pc ≝ (mk_state_pc ? st2_mid
308                                (pc_of_point P_out (pc_block (pc … st2)) mid2)
309                                (last_pop … st2))
310<(point_of_pc_of_point P_out (pc_block (pc … st2)) mid2) in seq_post_l;
311#seq_post_l
312lapply (produce_trace_any_any_free (mk_prog_params P_out ? stack_sizes)
313                     st2_mid_pc f t_fn ??? st2_fin_no_pc EQt_fn
314                                       (seq_post_l) EQst2_fin_no_pc)
315* #taaf2 * #taaf2_prf1 #taaf2_prf2
316%{(taaf_append_taaf ???? (taaf_step ???? taa1 ??) taaf2 ?)}
317[ @hide_prf @if_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H #_
318  % whd in match (as_costed ??); whd in match (as_label ??);
319  whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
320  >EQt_fn >m_return_bind whd in match point_of_pc; normalize nodelta
321  >point_of_offset_of_point lapply(taaf2_prf2 H) lapply seq_post_l cases bls
322  [ #_ *] #stmt1 #tl * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQstmt1
323  >point_of_pc_of_point change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #_
324  >point_of_pc_of_point in EQstmt1; #EQstmt1 >EQstmt1 >m_return_bind normalize nodelta
325  * #H @H %
326| @hide_prf whd whd in match eval_state; normalize nodelta whd in match fetch_statement;
327  normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid
328  >m_return_bind >EQst2_mid >m_return_bind whd in match eval_statement_advance;
329  normalize nodelta lapply COST lapply CL_OTHER lapply EQmid cases(blm mid1)
330  normalize nodelta
331  [ #c #_ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
332  | #id #args #dest #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
333  | #r #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
334  | #jseq #EQjseq #_ #_ %
335  ]
336| @hide_prf whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn
337  >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind assumption
338| @if_elim #_ [%] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
339]
340qed.
341*)
Note: See TracBrowser for help on using the repository browser.