source: src/joint/StatusSimulationHelper.ma @ 2863

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

Added new invariant to good_if
Generalized version of cond case for the correctness proof of each translate step

File size: 8.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
48check joint_classify
49check as_label
50
51record good_state_relation (P_in : sem_graph_params)
52   (P_out : sem_graph_params) (prog : joint_program P_in)
53   (stack_sizes : ident → option ℕ)
54   (init : ∀globals.joint_closed_internal_function P_in globals
55         →bound_b_graph_translate_data P_in P_out globals)
56   (R : joint_abstract_status (mk_prog_params P_in prog stack_sizes) →
57        joint_abstract_status (mk_prog_params P_out
58                                (b_graph_transform_program P_in P_out init prog)
59                                stack_sizes)
60        → Prop) : Prop ≝
61{ pc_eq_sigma_commute : ∀st1,st2.R st1 st2 → 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    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
74    st1 = return st1' →
75    let cond ≝ (COND P_in ? a ltrue) in
76    fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
77    return 〈f, fn,  sequential … cond lfalse〉 →
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.
85        ∀mid,nxt1.
86          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
87          = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→
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) nxt1) = None ? ∧
98            (\snd blp) = [ ] ∧
99            ∃st2_mid .
100                eval_state P_out (prog_var_names … trans_prog)
101                (ev_genv (mk_prog_params P_out trans_prog stack_sizes)) st2_pre_mid =
102                return st2_mid ∧ R st1' st2_mid
103   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
104  ) (init ? fn)
105}.
106
107
108lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
109∀prog : joint_program P_in.
110∀stack_sizes.
111∀ f_lbls,f_regs.∀f_bl_r.∀init.
112∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
113let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
114let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
115let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
116∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
117good_state_relation P_in P_out prog stack_sizes init R →
118∀st1,st1' : joint_abstract_status prog_pars_in.
119∀st2 : joint_abstract_status prog_pars_out.
120∀f.
121∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
122∀a,ltrue,lfalse.
123R st1 st2 →
124    let cond ≝ (COND P_in ? a ltrue) in
125 fetch_statement P_in …
126  (globalenv_noinit ? prog) (pc … st1) =
127    return 〈f, fn,  sequential … cond lfalse〉 →
128 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
129            st1 = return st1' →
130as_costed (joint_abstract_status prog_pars_in) st1' →
131∃ st2'. R st1' st2' ∧
132∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
133bool_to_Prop (taaf_non_empty … taf).
134#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' #st2
135#f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed
136cases(b_graph_transform_program_fetch_statement … good … EQfetch)
137#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2)
138#EQt_fn1 whd in ⊢ (% → ?); #Hinit
139* #labs * #regs
140** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls *
141whd in ⊢ (% → ?); @if_elim
142[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
143  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
144  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2) whd in match point_of_pc;
145  normalize nodelta whd in match (point_of_offset ??); <ABS
146  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
147]
148#_ <(pc_eq_sigma_commute … goodR … Rst1st2) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1
149* #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
150* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
151cases(bind_new_bind_new_instantiates … EQbl
152            (bind_new_bind_new_instantiates … Hinit
153               (cond_commutation … goodR … EQeval EQfetch Rst1st2 t_fn1 EQt_fn1))
154            … EQmid)   
155#st_pre_mid_no_pc * #EQst_pre_mid_no_pc *** #CL_JUMP #COST #EQ destruct(EQ) *
156#st2_mid * #EQst2mid #Hst2_mid whd in ⊢(% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
157%{st2_mid} %{Hst2_mid}
158>(pc_eq_sigma_commute … goodR … Rst1st2) in seq_pre_l; #seq_pre_l
159lapply(taaf_to_taa ???
160           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
161                                       seq_pre_l EQst_pre_mid_no_pc) ?)
162[ @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
163  whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
164  whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
165  >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
166  #H @H %
167] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
168[ whd <(as_label_ok … goodR … Hst2_mid) [assumption] cases daemon (*TODO: general lemma!*)
169| whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
170  >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
171  assumption
172| assumption
173]
174qed.
175
Note: See TracBrowser for help on using the repository browser.