source: src/joint/StatusSimulationHelper.ma @ 2885

Last change on this file since 2885 was 2885, checked in by sacerdot, 7 years ago

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