source: src/joint/StatusSimulationHelper.ma @ 2886

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

partial commit

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