source: src/joint/StatusSimulationHelper.ma @ 2967

Last change on this file since 2967 was 2940, checked in by sacerdot, 7 years ago
  1. StatusSimulationHelper? changed to allow to use status_rel that depends on the pc (necessary for ERTLptrToLTL)
  2. partial repairing of ERTLToERTLptrOK.ma, still in progress
  3. some progress in ERTLptrToLTLProof, but: a) some axioms were wrong, once fixed we now see some proof obligations

related to liveness analysis. Example: the variables live before and
after a COND must be the same. I have put daemons for the time being.

b) I strongly suspect that Interference should be changed to use livebefore,

in the correctness conditions (now it uses liveafter, the two sets
are probably equivalent for correct programs, but one is simpler to use:
which one?)

c) to_be_cleared_* must consult livebefore, but it is now passed liveafter.

Passing liveafter is necessary to typechek the graph, unless we do
b) first. Passing only the set computed by livebefore would be so much
better.

File size: 23.6 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(*
275(*CSC: Isn't this already proved somewhere else??? *)
276lemma point_of_pc_pc_of_point:
277 ∀P_in: sem_graph_params.∀l,st.
278   point_of_pc P_in
279    (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in))
280     (pc_block (pc P_in st)) l) = l.
281 #P * //
282qed.*)
283
284lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
285∀prog : joint_program P_in.
286∀stack_sizes.
287∀ f_lbls,f_regs.∀f_bl_r.∀init.
288∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
289∀st_no_pc_rel,st_rel.
290let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
291let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
292let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
293good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
294                    st_no_pc_rel st_rel →
295∀st1,st1' : joint_abstract_status prog_pars_in.
296∀st2 : joint_abstract_status prog_pars_out.
297∀f.
298∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
299∀a,ltrue,lfalse.
300st_rel st1 st2 →
301 let cond ≝ (COND P_in ? a ltrue) in
302  fetch_statement P_in …
303   (globalenv_noinit ? prog) (pc … st1) =
304     return 〈f, fn,  sequential … cond lfalse〉 →
305 eval_state P_in (prog_var_names … ℕ prog)
306  (ev_genv … prog_pars_in) st1 = return st1' →
307as_costed (joint_abstract_status prog_pars_in) st1' →
308∃ st2'. st_rel st1' st2' ∧
309∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
310bool_to_Prop (taaf_non_empty … taf).
311#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel
312#goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval
313@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
314whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
315#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
316#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
317cases(fetch_statement_inv … EQfetch) #EQfn #_
318[ >(pc_of_label_eq … EQfn)
319  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
320| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
321]
322#EQ destruct(EQ) #n_costed
323cases(b_graph_transform_program_fetch_statement … good … EQfetch)
324#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
325#EQt_fn1 whd in ⊢ (% → ?); #Hinit
326* #labs * #regs ** #EQlabs #EQf_regs normalize nodelta *** #blp #blm #bls *
327whd in ⊢ (% → ?); @if_elim
328[1,3: @eq_identifier_elim [2,4: #_ *] whd in match point_of_pc; normalize nodelta
329  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
330  * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
331  normalize nodelta whd in match (point_of_offset ??); <ABS
332  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
333]
334#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
335#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
336* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
337cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
338               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
339#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
340cases(APP … EQmid) -APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta
341#EQst_pre_mid_no_pc #Hsem #CL_JUMP #COST #Hst2_mid
342[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
343     (last_pop … st2))}
344| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
345     (last_pop … st2))}
346]
347letin st1' ≝ (mk_state_pc P_in ???)
348letin st2' ≝ (mk_state_pc P_out ???)
349cut(st_rel st1' st2')
350[1,3: @(st_rel_def … goodR … f fn ?)
351      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
352      |2,5: assumption
353      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
354      ]
355]
356#H_fin
357%
358[1,3: assumption]
359>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
360lapply(taaf_to_taa ???
361           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
362                                       seq_pre_l EQst_pre_mid_no_pc) ?)
363[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
364      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
365      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
366      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
367      #H @H %
368]
369#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
370[1,4: whd <(as_label_ok ??????????? goodR st1' st2' f fn ?? H_fin) [1,4: assumption]
371      cases daemon (*TODO: general lemma!*)
372|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
373      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
374      assumption
375|*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
376    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
377    cases(blm mid1) in CL_JUMP COST Hst2_mid;
378    [1,5: #c #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
379    |2,4,6,8: [1,3: #c_id #args #dest |*: #seq] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
380    ]
381    #r #ltrue #_ #_ #Hst2_mid whd in match eval_statement_no_pc; normalize nodelta
382    >m_return_bind assumption
383]
384qed.
385
386(*
387let rec taa_to_taaf  S st1 st2 (taa : trace_any_any S st1 st2) on taa :
388trace_any_any_free S st1 st2 ≝
389(match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with
390[taa_base st1' ⇒ λprf.?
391|taa_step st1' st2' st3' H I J tl ⇒ λprf.?
392]) (refl … st1) (refl … st2) (refl_jmeq ? taa).
393*)
394
395lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
396∀prog : joint_program P_in.
397∀stack_sizes.
398∀ f_lbls,f_regs.∀f_bl_r.∀init.
399∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
400∀st_no_pc_rel,st_rel.
401let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
402let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
403let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
404good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
405                    st_no_pc_rel st_rel →
406∀st1,st1' : joint_abstract_status prog_pars_in.
407∀st2 : joint_abstract_status prog_pars_out.
408∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
409∀stmt,nxt.
410st_rel st1 st2 →
411 let seq ≝ (step_seq P_in ? stmt) in
412  fetch_statement P_in …
413   (globalenv_noinit ? prog) (pc … st1) =
414     return 〈f, fn,  sequential ?? seq nxt〉 →
415 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
416  st1 = return st1' →
417∃st2'. st_rel st1' st2' ∧           
418∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
419 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
420(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
421 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
422#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel
423#goodR #st1 #st1' #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
424@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
425#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
426#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
427whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
428cases(b_graph_transform_program_fetch_statement … good … EQfetch)
429#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
430#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim
431[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
432  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
433  * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
434  normalize nodelta whd in match (point_of_offset ??); <ABS
435  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
436]
437#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
438>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
439cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
440               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
441#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
442%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
443cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
444#EQfn #_
445%
446[ @(st_rel_def ??????????? goodR … f fn)
447      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
448      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
449      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
450      ]
451]
452%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
453                                      SBiC EQst2_fin_no_pc)}
454@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
455qed.
456
457(*
458lemma eval_cost_ok :
459∀ P_in , P_out: sem_graph_params.
460∀prog : joint_program P_in.
461∀stack_sizes.
462∀ f_lbls,f_regs.∀f_bl_r.∀init.
463∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
464let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
465let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
466let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
467∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
468∀st1,st1' : joint_abstract_status prog_pars_in.
469∀st2 : joint_abstract_status prog_pars_out.
470∀f.
471∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt.
472R st1 st2 →
473let cost ≝ COST_LABEL P_in ? c in
474 fetch_statement P_in …
475  (globalenv_noinit ? prog) (pc … st1) =
476    return 〈f, fn,  sequential ?? cost nxt〉 →
477 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
478            st1 = return st1' →
479∃ st2'. R st1' st2' ∧
480∃taf : trace_any_any_free
481        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
482        st2 st2'.
483bool_to_Prop (taaf_non_empty … taf).
484#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #good #R #st1 #st1'
485#st2 #f #fn #c #nxt #Rst1st2 normalize nodelta #EQfetch whd in match eval_state;
486whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
487normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ)
488*)
Note: See TracBrowser for help on using the repository browser.