source: src/joint/StatusSimulationHelper.ma @ 2898

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

1) simplification of cond and seq case for StatusSimulationHelper? which has
been tested correct in ERTL to ERTlptr correctness proof.

2) the cond case for ERTLptr to LTL correctenss proof has been adapted to the
new specification

File size: 23.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
48definition joint_state_relation ≝
49λP_in,P_out.(Σb:block.block_region b=Code) → state P_in → state P_out → Prop.
50
51definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
52
53definition sigma_map ≝  block → label → option label.
54definition lbl_funct ≝  block → label → (list label).
55definition regs_funct ≝ block → label → (list register).
56
57definition get_sigma : ∀p : sem_graph_params.
58joint_program p → lbl_funct → sigma_map ≝
59λp,prog,f_lbls.λbl,searched.
60let globals ≝ prog_var_names … prog in
61let ge ≝ globalenv_noinit … prog in
62! bl ← code_block_of_block bl ;
63! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
64!〈res,s〉 ← find ?? (joint_if_code  ?? fn)
65                (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with
66                          [None ⇒ eq_identifier … searched lbl
67                          |Some x ⇒ eq_identifier … searched (\snd x)
68                          ]);
69return res.
70
71definition sigma_pc_opt :  ∀p_in,p_out : sem_graph_params.
72joint_program p_in →  lbl_funct →
73program_counter → option program_counter ≝
74λp_in,p_out,prog,f_lbls,pc.
75  let sigma ≝ get_sigma p_in prog f_lbls in
76  let ertl_ptr_point ≝ point_of_pc p_out pc in
77  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
78    return pc
79  else
80       ! point ← sigma (pc_block pc) ertl_ptr_point;
81       return pc_of_point p_in (pc_block pc) point.
82
83definition sigma_stored_pc ≝
84λp_in,p_out,prog,f_lbls,pc. match sigma_pc_opt p_in p_out prog f_lbls pc with
85      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
86
87record good_state_relation (P_in : sem_graph_params)
88   (P_out : sem_graph_params) (prog : joint_program P_in)
89   (stack_sizes : ident → option ℕ)
90   (init : ∀globals.joint_closed_internal_function P_in globals
91         →bound_b_graph_translate_data P_in P_out globals)
92   (f_bl_r : block → list register) (f_lbls : lbl_funct) (f_regs : regs_funct)
93   (good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs)
94   (st_no_pc_rel : joint_state_relation P_in P_out)
95   (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝
96{ fetch_ok_sigma_state_ok :
97   ∀st1,st2,f,fn. st_rel st1 st2 →
98    fetch_internal_function ? (globalenv_noinit … prog)
99     (pc_block (pc … st1))  = return 〈f,fn〉 →
100     st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1) (st_no_pc … st2)
101; fetch_ok_pc_ok :
102  ∀st1,st2,f,fn.st_rel st1 st2 →
103   fetch_internal_function ? (globalenv_noinit … prog)
104  (pc_block (pc … st1))  = return 〈f,fn〉 →
105   pc … st1 = pc … st2
106; fetch_ok_sigma_last_pop_ok :
107  ∀st1,st2,f,fn.st_rel st1 st2 →
108   fetch_internal_function ? (globalenv_noinit … prog)
109    (pc_block (pc … st1))  = return 〈f,fn〉 →
110   (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2)
111; st_rel_def :
112  ∀st1,st2,pc,lp1,lp2,f,fn.
113  fetch_internal_function ? (globalenv_noinit … prog)
114   (pc_block pc) = return 〈f,fn〉 → st_no_pc_rel (pc_block pc) st1 st2 →
115   lp1 = sigma_stored_pc P_in P_out prog f_lbls lp2 →
116  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
117; as_label_ok :     let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
118  ∀st1,st2,f,fn,stmt.
119   fetch_statement ? (prog_var_names … prog)
120   (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 →
121   st_rel st1 st2 →
122   as_label (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 =
123    as_label (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) st2
124; cond_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,a,ltrue,lfalse.
129    let cond ≝ (COND P_in ? a ltrue) in
130    fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
131    return 〈f, fn,  sequential … cond lfalse〉 → 
132    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
133    st1 = return st1' →
134    st_rel 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.(\snd blp) = [ ] ∧
141        ∀mid.
142          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
143          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
144         ∃st2_pre_mid_no_pc.
145            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid)
146                                   (st_no_pc ? st2)
147            = return st2_pre_mid_no_pc ∧
148            st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
149            joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
150                                ((\snd (\fst blp)) mid)  = cl_jump ∧
151            cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
152                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
153            let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc
154                               (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in
155            let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in
156            eval_statement_advance P_out (prog_var_names … trans_prog)
157             (ev_genv … (mk_prog_params P_out trans_prog stack_sizes)) f t_fn
158             (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'
159   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
160  ) (init ? fn)
161; seq_commutation :
162  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
163  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
164  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
165  ∀f,fn,stmt,nxt.
166  let seq ≝ (step_seq P_in ? stmt) in
167  fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
168  return 〈f, fn,  sequential … seq nxt〉 → 
169  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes))
170  st1 = return st1' →
171  st_rel st1 st2 →
172  ∀t_fn.
173  fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
174  return 〈f,t_fn〉 →
175  bind_new_P' ??
176     (λregs1.λdata.bind_new_P' ??
177      (λregs2.λblp.
178       ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes)
179                            (globals (mk_prog_params P_out trans_prog stack_sizes))).
180                            blp = (ensure_step_block ?? l) ∧
181       ∃st2_fin_no_pc.
182           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
183              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
184           st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1') st2_fin_no_pc
185      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
186     ) (init ? fn)
187}.
188
189lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
190∀prog : joint_program P_in.
191∀stack_sizes.
192∀ f_lbls,f_regs.∀f_bl_r.∀init.
193∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
194∀st_no_pc_rel,st_rel.
195∀f,fn,stmt,st1,st2.
196good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
197                    st_no_pc_rel st_rel →
198st_rel st1 st2 →
199fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
200 return 〈f,fn,stmt〉 →
201st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1) (st_no_pc … st2).
202#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
203#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
204cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
205@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
206qed.
207
208lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
209∀prog : joint_program P_in.
210∀stack_sizes.
211∀ f_lbls,f_regs.∀f_bl_r.∀init.
212∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
213∀st_no_pc_rel,st_rel.
214∀f,fn,stmt,st1,st2.
215good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
216                    st_no_pc_rel st_rel →
217st_rel st1 st2 →
218fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
219 return 〈f,fn,stmt〉 →
220pc … st1 = pc … st2.
221#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
222#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
223cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
224@(fetch_ok_pc_ok … goodR … EQfn) assumption
225qed.
226
227lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
228∀prog : joint_program P_in.
229∀stack_sizes.
230∀ f_lbls,f_regs.∀f_bl_r.∀init.
231∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
232∀st_no_pc_rel,st_rel.
233∀f,fn,stmt,st1,st2.
234good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
235                    st_no_pc_rel st_rel →
236st_rel st1 st2 →
237fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
238 return 〈f,fn,stmt〉 →
239(last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2).
240#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
241#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
242cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
243@(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption
244qed.
245
246(*
247lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params.
248∀prog : joint_program P_in.
249∀stack_sizes.
250∀ f_lbls,f_regs.∀f_bl_r.∀init.
251∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
252∀st_no_pc_rel,st_rel.
253∀f,fn,stmt,st1,st2.
254good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
255                    st_no_pc_rel st_rel →
256st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) →
257(last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) →
258fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
259 return 〈f,fn,stmt〉 → st_rel st1 st2.
260#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel
261#st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ)
262#EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
263@(st_rel_def … goodR … EQfn) assumption
264qed.
265*)
266 
267
268lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
269∀prog : joint_program P_in.
270∀stack_sizes.
271∀ f_lbls,f_regs.∀f_bl_r.∀init.
272∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
273∀st_no_pc_rel,st_rel.
274let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
275let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
276let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
277good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
278                    st_no_pc_rel st_rel →
279∀st1,st1' : joint_abstract_status prog_pars_in.
280∀st2 : joint_abstract_status prog_pars_out.
281∀f.
282∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
283∀a,ltrue,lfalse.
284st_rel st1 st2 →
285    let cond ≝ (COND P_in ? a ltrue) in
286 fetch_statement P_in …
287  (globalenv_noinit ? prog) (pc … st1) =
288    return 〈f, fn,  sequential … cond lfalse〉 →
289 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
290            st1 = return st1' →
291as_costed (joint_abstract_status prog_pars_in) st1' →
292∃ st2'. st_rel st1' st2' ∧
293∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
294bool_to_Prop (taaf_non_empty … taf).
295#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel
296#goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval
297@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
298whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
299#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
300#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
301cases(fetch_statement_inv … EQfetch) #EQfn #_
302[ >(pc_of_label_eq … EQfn)
303  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
304| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
305]
306#EQ destruct(EQ) #n_costed
307cases(b_graph_transform_program_fetch_statement … good … EQfetch)
308#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
309#EQt_fn1 whd in ⊢ (% → ?); #Hinit
310* #labs * #regs ** #EQlabs #EQf_regs normalize nodelta *** #blp #blm #bls *
311whd in ⊢ (% → ?); @if_elim
312[1,3: @eq_identifier_elim [2,4: #_ *] whd in match point_of_pc; normalize nodelta
313  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
314  * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
315  normalize nodelta whd in match (point_of_offset ??); <ABS
316  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
317]
318#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
319#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
320* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
321cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
322               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
323#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
324cases(APP … EQmid) -APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta
325#EQst_pre_mid_no_pc #Hsem #CL_JUMP #COST #Hst2_mid
326[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
327     (last_pop … st2))}
328| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
329     (last_pop … st2))}
330]
331letin st1' ≝ (mk_state_pc P_in ???)
332letin st2' ≝ (mk_state_pc P_out ???)
333cut(st_rel st1' st2')
334[1,3: @(st_rel_def … goodR … f fn ?)
335      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
336      |2,5: assumption
337      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
338      ]
339]
340#H_fin
341%
342[1,3: assumption]
343>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
344lapply(taaf_to_taa ???
345           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
346                                       seq_pre_l EQst_pre_mid_no_pc) ?)
347[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
348      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
349      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
350      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
351      #H @H %
352]
353#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
354[1,4: whd <(as_label_ok ??????????? goodR st1' st2' f fn ?? H_fin) [1,4: assumption]
355      cases daemon (*TODO: general lemma!*)
356|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
357      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
358      assumption
359|*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
360    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
361    cases(blm mid1) in CL_JUMP COST Hst2_mid;
362    [1,5: #c #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
363    |2,4,6,8: [1,3: #c_id #args #dest |*: #seq] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
364    ]
365    #r #ltrue #_ #_ #Hst2_mid whd in match eval_statement_no_pc; normalize nodelta
366    >m_return_bind assumption
367]
368qed.
369
370(*
371let rec taa_to_taaf  S st1 st2 (taa : trace_any_any S st1 st2) on taa :
372trace_any_any_free S st1 st2 ≝
373(match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with
374[taa_base st1' ⇒ λprf.?
375|taa_step st1' st2' st3' H I J tl ⇒ λprf.?
376]) (refl … st1) (refl … st2) (refl_jmeq ? taa).
377*)
378
379lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
380∀prog : joint_program P_in.
381∀stack_sizes.
382∀ f_lbls,f_regs.∀f_bl_r.∀init.
383∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
384∀st_no_pc_rel,st_rel.
385let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
386let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
387let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
388good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
389                    st_no_pc_rel st_rel →
390∀st1,st1' : joint_abstract_status prog_pars_in.
391∀st2 : joint_abstract_status prog_pars_out.
392∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
393∀stmt,nxt.
394st_rel st1 st2 →
395    let seq ≝ (step_seq P_in ? stmt) in
396 fetch_statement P_in …
397  (globalenv_noinit ? prog) (pc … st1) =
398    return 〈f, fn,  sequential ?? seq nxt〉 →
399 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
400            st1 = return st1' →
401∃st2'. st_rel st1' st2' ∧           
402∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
403 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
404(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
405 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
406#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel
407#goodR #st1 #st1' #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
408@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
409#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
410#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
411whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
412cases(b_graph_transform_program_fetch_statement … good … EQfetch)
413#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
414#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim
415[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
416  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
417  * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
418  normalize nodelta whd in match (point_of_offset ??); <ABS
419  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
420]
421#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
422>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
423cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
424               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
425#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
426%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
427cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
428#EQfn #_
429%
430[ @(st_rel_def ??????????? goodR … f fn)
431      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
432      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
433      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
434      ]
435]
436%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
437                                      SBiC EQst2_fin_no_pc)}
438@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
439qed.
440
441(*
442lemma eval_cost_ok :
443∀ P_in , P_out: sem_graph_params.
444∀prog : joint_program P_in.
445∀stack_sizes.
446∀ f_lbls,f_regs.∀f_bl_r.∀init.
447∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
448let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
449let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
450let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
451∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
452∀st1,st1' : joint_abstract_status prog_pars_in.
453∀st2 : joint_abstract_status prog_pars_out.
454∀f.
455∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt.
456R st1 st2 →
457let cost ≝ COST_LABEL P_in ? c in
458 fetch_statement P_in …
459  (globalenv_noinit ? prog) (pc … st1) =
460    return 〈f, fn,  sequential ?? cost nxt〉 →
461 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
462            st1 = return st1' →
463∃ st2'. R st1' st2' ∧
464∃taf : trace_any_any_free
465        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
466        st2 st2'.
467bool_to_Prop (taaf_non_empty … taf).
468#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #good #R #st1 #st1'
469#st2 #f #fn #c #nxt #Rst1st2 normalize nodelta #EQfetch whd in match eval_state;
470whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
471normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ)
472*)
Note: See TracBrowser for help on using the repository browser.