source: src/joint/StatusSimulationHelper.ma @ 2939

Last change on this file since 2939 was 2939, checked in by sacerdot, 8 years ago

Major problem: in order to accomodate the ERTLptrToLTL proof pass, the
relation between states must be parameterized over the current label.

This makes the previous proof fail:

if s1 == s2 then it is not automatically true that s1' == s2'

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