source: src/joint/StatusSimulationHelper.ma @ 2991

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

Fixed cond and seq case in StatusSimulationHelper?

Added cost case in StatusSimulationHelper?

File size: 36.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  ∀pars: sem_graph_params.
27  ∀globals,ge,bl,i_fn,lbl.
28  fetch_internal_function ? globals ge bl = return i_fn →
29  pc_of_label pars globals ge bl lbl =
30    OK ? (pc_of_point pars bl lbl).
31#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
48let rec bind_instantiates B X (b : bind_new B X) (l : list B) on b : (option X) ≝
49  match b with
50  [ bret B ⇒
51    match l with
52    [ nil ⇒ Some ? B
53    | _ ⇒ None ?
54    ]
55  | bnew f ⇒
56    match l with
57    [ nil ⇒ None ?
58    | cons r l' ⇒
59      bind_instantiates B X (f r) l'
60    ]
61  ].
62 
63lemma bind_instantiates_bind_new_instantiates : ∀B,X.∀b : bind_new B X.
64∀l : list B.∀x : X.
65bind_instantiates B X b l = Some ? x →
66bind_new_instantiates B X x b l.
67#B #X #b elim b
68[#x1 * [2: #hd #tl] #x whd in ⊢ (??%? → ?); #EQ destruct(EQ) %
69|#f #IH * [2: #hd #tl] #x whd in ⊢ (??%? → ?); [2: #EQ destruct(EQ)] #H
70 whd @IH assumption
71]
72qed.
73
74lemma bind_new_instantiates_bind_instantiates : ∀B,X.∀b : bind_new B X.
75∀l : list B.∀x : X.
76bind_new_instantiates B X x b l →
77bind_instantiates B X b l = Some ? x.
78#B #X #b elim b
79[ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) %
80| #f #IH * [2: #hd #tl] #x whd in ⊢ (% → ?); [2: *] #H whd in ⊢ (??%?); @IH @H
81]
82qed.
83
84
85definition joint_state_relation ≝
86λP_in,P_out.program_counter → state P_in → state P_out → Prop.
87
88definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
89
90definition lbl_funct_type ≝  block → label → (list label).
91definition regs_funct_type ≝ block → label → (list register).
92
93definition preamble_length ≝
94λP_in : sem_graph_params.λP_out : sem_graph_params.λprog : joint_program P_in.
95λstack_size : (ident → option ℕ).
96λinit : ∀globals.joint_closed_internal_function P_in globals
97         →bound_b_graph_translate_data P_in P_out globals.
98λinit_regs : block → list register.
99λf_regs : regs_funct_type.λbl : block.λlbl : label.
100! bl ← code_block_of_block bl ;
101! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (prog_var_names … prog)
102                           (joint_globalenv P_in prog stack_size) bl);
103! stmt ← stmt_at P_in (prog_var_names … prog) (joint_if_code … fn) lbl;
104! data ← bind_instantiates ?? (init … fn) (init_regs bl);
105match stmt with
106[ sequential step nxt ⇒
107    ! step_block ← bind_instantiates ?? (f_step … data lbl step) (f_regs bl lbl);
108    return |\fst (\fst step_block)|
109| final fin ⇒
110    ! fin_block ← bind_instantiates ?? (f_fin … data lbl fin) (f_regs bl lbl);
111    return |\fst fin_block|
112| FCOND abs _ _ _ ⇒ Ⓧabs
113].
114
115
116definition sigma_label : ∀p_in,p_out : sem_graph_params.
117joint_program p_in → (ident → option ℕ) →
118(∀globals.joint_closed_internal_function p_in globals
119         →bound_b_graph_translate_data p_in p_out globals) →
120(block → list register) → lbl_funct_type → regs_funct_type →
121block → label → option label ≝
122λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
123! bl ← code_block_of_block bl ;
124! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (prog_var_names … prog)
125                           (joint_globalenv p_in prog stack_size) bl);
126! 〈res,s〉 ←
127 find ?? (joint_if_code ?? fn)
128  (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
129             [ None ⇒ false
130             | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
131                         [ None ⇒ false
132                         | Some x ⇒ eq_identifier … searched x
133                         ]
134             ]);
135return res.
136
137lemma partial_inj_sigma :
138∀p_in,p_out,prog,stack_size,init,init_regs.
139∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2.
140sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→
141sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 =
142sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 →
143lbl1 = lbl2.
144#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2
145inversion(sigma_label ????????? lbl1)
146[ #_ * #H @⊥ @H %]
147#lbl1' #H @('bind_inversion H) -H #bl' #EQbl'
148#H @('bind_inversion H) -H * #f #fn #H lapply(res_eq_from_opt ??? H) -H
149#EQfn #H @('bind_inversion H) -H * #res #stmt #H1 whd in ⊢ (??%? → ?);
150#EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H
151#bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) -H
152* #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ)
153lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2)
154cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???)
155normalize nodelta
156[*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim
157[2: #_ *] #EQ destruct(EQ) #_ %
158qed.
159
160definition sigma_pc_opt : 
161∀p_in,p_out : sem_graph_params.
162joint_program p_in → (ident → option ℕ) →
163(∀globals.joint_closed_internal_function p_in globals
164         →bound_b_graph_translate_data p_in p_out globals) →
165(block → list register) → lbl_funct_type → regs_funct_type →
166program_counter → option program_counter ≝
167λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
168let target_point ≝ point_of_pc p_out pc in
169if eqZb (block_id (pc_block pc)) (-1) then
170 return pc
171else
172 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs
173                   f_lbls f_regs (pc_block pc) target_point;
174 return pc_of_point p_in (pc_block pc) source_point.
175
176lemma sigma_stored_pc_inj :
177∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
178sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
179sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
180sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
181pc = pc'.
182#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs
183* #bl1 #p1 * #bl2 #p2
184inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1
185whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta
186@eqZb_elim [2: *] normalize nodelta #Hbl
187[ #H @('bind_inversion H) -H * #pt1 #EQpt1]
188whd in ⊢ (??%? → ?); #EQ destruct(EQ)
189#_ #H lapply(sym_eq ??? H) -H whd in match sigma_pc_opt;
190normalize nodelta @eqZb_elim [2,4: *] #Hbl1 normalize nodelta
191[1,2: #H @('bind_inversion H) -H * #pt2 #EQpt2] whd in match pc_of_point;
192normalize nodelta whd in match (offset_of_point ??);
193whd in ⊢ (??%% → ?); #EQ destruct(EQ)
194[2,3: @⊥ [ >Hbl in Hbl1; | >Hbl1 in Hbl;] #H @H % |4: %]
195whd in match (offset_of_point ??) in EQpt2;
196<EQpt1 in EQpt2; #H lapply(partial_inj_sigma … (sym_eq ??? H))
197[ >EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta
198whd in match (point_of_offset ??); whd in match (point_of_offset ??);
199#EQ -prog destruct(EQ) %
200qed.
201
202definition sigma_stored_pc ≝
203λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
204match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
205      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
206
207
208record good_state_relation (P_in : sem_graph_params)
209   (P_out : sem_graph_params) (prog : joint_program P_in)
210   (stack_sizes : ident → option ℕ)
211   (init : ∀globals.joint_closed_internal_function P_in globals
212         →bound_b_graph_translate_data P_in P_out globals)
213   (init_regs : block → list register) (f_lbls : lbl_funct_type)
214   (f_regs : regs_funct_type)
215   (st_no_pc_rel : joint_state_relation P_in P_out)
216   (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝
217{ good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init
218                     prog init_regs f_lbls f_regs
219; fetch_ok_sigma_state_ok :
220   ∀st1,st2,f,fn. st_rel st1 st2 →
221    fetch_internal_function … (prog_var_names … prog)
222     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
223     = return 〈f,fn〉 →
224     st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
225; fetch_ok_pc_ok :
226  ∀st1,st2,f,fn.st_rel st1 st2 →
227   fetch_internal_function … (prog_var_names … prog)
228     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
229     = return 〈f,fn〉 →
230   pc … st1 = pc … st2
231; fetch_ok_sigma_last_pop_ok :
232  ∀st1,st2,f,fn.st_rel st1 st2 →
233   fetch_internal_function … (prog_var_names … prog)
234     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
235     = return 〈f,fn〉 →
236   (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
237                       f_lbls f_regs (last_pop … st2)
238; st_rel_def :
239  ∀st1,st2,pc,lp1,lp2,f,fn.
240  fetch_internal_function … (prog_var_names … prog)
241     (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 →
242   st_no_pc_rel pc st1 st2 →
243   lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
244          f_lbls f_regs lp2 →
245  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
246; as_label_ok_non_entry :
247  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
248  ∀st1,st2,f,fn,stmt.
249  fetch_statement … (prog_var_names … prog)
250  (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
251  st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
252  as_label (joint_status P_in prog stack_sizes) st1 =
253  as_label (joint_status P_out trans_prog stack_sizes) st2
254; pre_main_ok :
255  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
256    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
257    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
258    block_id … (pc_block (pc … st1)) = -1 →
259    st_rel st1 st2 →
260    as_label (joint_status P_in prog stack_sizes) st1 =
261    as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
262    joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
263    joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
264    (eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
265      st1 = return st1' →
266    ∃st2'. st_rel st1' st2' ∧
267    eval_state P_out (prog_var_names … trans_prog)
268     (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
269; cond_commutation :
270    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
271    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
272    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
273    ∀f,fn,a,ltrue,lfalse.
274    block_id … (pc_block (pc … st1)) ≠ -1 →
275    let cond ≝ (COND P_in ? a ltrue) in
276    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
277    return 〈f, fn,  sequential … cond lfalse〉 → 
278    eval_state P_in (prog_var_names … prog)
279    (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
280    st_rel st1 st2 →
281    ∀t_fn.
282    fetch_internal_function … (prog_var_names … trans_prog)
283     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
284     return 〈f,t_fn〉 →
285    bind_new_P' ??
286     (λregs1.λdata.bind_new_P' ??
287     (λregs2.λblp.(\snd blp) = [ ] ∧
288        ∀mid.
289          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
290          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
291         ∃st2_pre_mid_no_pc.
292            repeat_eval_seq_no_pc … (mk_prog_params P_out trans_prog stack_sizes) f
293             (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
294            = return st2_pre_mid_no_pc ∧
295            st_no_pc_rel (pc … st1') (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
296            joint_classify_step … ((\snd (\fst blp)) mid)  = cl_jump ∧
297            cost_label_of_stmt P_out (prog_var_names … trans_prog)
298                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
299            let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc
300                               (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in
301            let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in
302            eval_statement_advance P_out (prog_var_names … trans_prog)
303             (joint_globalenv P_out trans_prog stack_sizes) f t_fn
304             (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'
305   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
306  ) (init ? fn)
307; seq_commutation :
308  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
309  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
310  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
311  ∀f,fn,stmt,nxt.
312  block_id … (pc_block (pc … st1)) ≠ -1 →
313  let seq ≝ (step_seq P_in ? stmt) in
314  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
315  return 〈f, fn,  sequential … seq nxt〉 → 
316  eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
317  st1 = return st1' →
318  st_rel st1 st2 →
319  ∀t_fn.
320  fetch_internal_function … (prog_var_names … trans_prog)
321     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
322  return 〈f,t_fn〉 →
323  bind_new_P' ??
324     (λregs1.λdata.bind_new_P' ??
325      (λregs2.λblp.
326       ∃l : list (joint_seq P_out (prog_var_names … trans_prog)).
327                            blp = (ensure_step_block ?? l) ∧
328       ∃st2_fin_no_pc.
329           repeat_eval_seq_no_pc … (mk_prog_params P_out trans_prog stack_sizes) f
330              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
331           st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
332      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
333     ) (init ? fn)
334; cost_commutation :
335  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
336  ∀st1,st2,pc.∀f,fn,c,nxt.
337  block_id … (pc_block pc) ≠ -1 →
338  st_no_pc_rel pc st1 st2 →
339  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc =
340  return 〈f, fn,  sequential ?? (COST_LABEL ?? c) nxt〉 → 
341  st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2
342}.
343
344(*TO BE MOVED*)
345lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
346decidable (In A l a).
347#A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
348[ #H % %2 assumption | * #H cases (DEC hd)
349[ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]]
350qed.
351
352lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
353#A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
354% #H1 @H % >H1 %
355qed.
356
357lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
358#A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *
359[ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption]
360qed.
361
362lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
363∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
364In ? (stmt_labels p ? stmt) lbl→
365fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
366pc' = pc_of_point p (pc_block pc) lbl →
367∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
368#p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
369cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
370#EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
371cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?)
372[3: * cases lbl #x #y cases(decidable_eq_pos … x y)
373    [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
374| whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
375  whd in match code_has_label; whd in match code_has_point; normalize nodelta
376  inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
377  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
378  >point_of_pc_of_point >EQstmt' %
379| #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
380  [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
381    normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_
382    whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
383    inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
384    whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
385    >point_of_pc_of_point >EQstmt' %
386  | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
387  ]
388]
389qed.
390
391
392
393lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
394∀prog : joint_program P_in.
395∀stack_sizes.
396∀ f_lbls,f_regs.∀f_bl_r.∀init.∀st_no_pc_rel,st_rel.
397∀f,fn,stmt,st1,st2.
398good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
399                    st_no_pc_rel st_rel →
400st_rel st1 st2 →
401fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
402 return 〈f,fn,stmt〉 →
403st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2).
404#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
405#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
406cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
407@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
408qed.
409
410lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
411∀prog : joint_program P_in.
412∀stack_sizes.
413∀ f_lbls,f_regs.∀f_bl_r.∀init.
414∀st_no_pc_rel,st_rel.
415∀f,fn,stmt,st1,st2.
416good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
417                    st_no_pc_rel st_rel →
418st_rel st1 st2 →
419fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
420 return 〈f,fn,stmt〉 →
421pc … st1 = pc … st2.
422#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
423#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
424cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
425@(fetch_ok_pc_ok … goodR … EQfn) assumption
426qed.
427
428lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
429∀prog : joint_program P_in.
430∀stack_sizes.
431∀ f_lbls,f_regs.∀f_bl_r.∀init.
432∀st_no_pc_rel,st_rel.
433∀f,fn,stmt,st1,st2.
434good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
435                    st_no_pc_rel st_rel →
436st_rel st1 st2 →
437fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
438 return 〈f,fn,stmt〉 →
439(last_pop … st1) =
440 sigma_stored_pc P_in P_out prog stack_sizes init f_bl_r f_lbls
441  f_regs (last_pop … st2).
442#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
443#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
444cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
445@(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption
446qed.
447
448(*
449lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params.
450∀prog : joint_program P_in.
451∀stack_sizes.
452∀ f_lbls,f_regs.∀f_bl_r.∀init.
453∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
454∀st_no_pc_rel,st_rel.
455∀f,fn,stmt,st1,st2.
456good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
457                    st_no_pc_rel st_rel →
458st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) →
459(last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) →
460fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
461 return 〈f,fn,stmt〉 → st_rel st1 st2.
462#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel
463#st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ)
464#EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
465@(st_rel_def … goodR … EQfn) assumption
466qed.
467*)
468
469(*
470(*CSC: Isn't this already proved somewhere else??? *)
471lemma point_of_pc_pc_of_point:
472 ∀P_in: sem_graph_params.∀l,st.
473   point_of_pc P_in
474    (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in))
475     (pc_block (pc P_in st)) l) = l.
476 #P * //
477qed.*)
478
479(*TO BE MOVED*)
480lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
481All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
482#A #P #l1 elim l1
483[ #l2 change with l2 in ⊢ (???% → ?); #H % //]
484#a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
485* #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
486qed.
487
488lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
489∀prog : joint_program P_in.
490∀stack_sizes.
491∀ f_lbls,f_regs.∀f_bl_r.∀init.
492∀st_no_pc_rel,st_rel.
493let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
494let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
495let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
496good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
497                    st_no_pc_rel st_rel→
498∀st1,st1' : joint_abstract_status prog_pars_in.
499∀st2 : joint_abstract_status prog_pars_out.
500∀f.
501∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
502∀a,ltrue,lfalse.
503block_id … (pc_block (pc … st1)) ≠ -1 →
504st_rel st1 st2 →
505 let cond ≝ (COND P_in ? a ltrue) in
506  fetch_statement P_in …
507   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
508     return 〈f, fn,  sequential … cond lfalse〉 →
509 eval_state P_in (prog_var_names … prog)
510  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
511as_costed (joint_abstract_status prog_pars_in) st1' →
512∃ st2'. st_rel st1' st2' ∧
513∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
514bool_to_Prop (taaf_non_empty … taf).
515#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
516#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2 #EQfetch
517#EQeval
518@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
519whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
520#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
521#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
522cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
523[ >(pc_of_label_eq … EQfn)
524  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
525| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
526]
527#EQ destruct(EQ) #n_costed
528lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
529[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
530      #H cases(H EQfetch) -H |*:]
531#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
532#EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta
533*** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
534[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
535      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
536      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_
537      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
538      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
539      <ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
540]
541#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
542#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
543* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
544cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
545               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
546[2,4: % assumption]
547#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
548cases(APP … EQmid) -APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta
549#EQst_pre_mid_no_pc #Hsem #CL_JUMP #COST #Hst2_mid
550[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
551     (last_pop … st2))}
552| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
553     (last_pop … st2))}
554]
555letin st1' ≝ (mk_state_pc P_in ???)
556letin st2' ≝ (mk_state_pc P_out ???)
557cut(st_rel st1' st2')
558[1,3: @(st_rel_def … goodR … f fn ?)
559      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
560      |2,5: assumption
561      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
562      ]
563]
564#H_fin
565%
566[1,3: assumption]
567>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
568lapply(taaf_to_taa ???
569           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
570                                       seq_pre_l EQst_pre_mid_no_pc) ?)
571[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
572      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
573      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
574      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
575      #H @H %
576]
577#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
578[1,4: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
579      [2: @ltrue|3: %2 % % |4: % |6: @lfalse |7: % % |8: %] #stmt' #EQstmt'
580      whd <(as_label_ok_non_entry … goodR … EQstmt' H_fin)
581      [1,3: assumption
582      |2,4: cases(entry_unused … (pi2 ?? fn) … EQstmt)
583            [ whd in match stmt_forall_labels; whd in match stmt_labels;
584              normalize nodelta #H cases(append_All … H) #_
585              whd in match stmt_explicit_labels; whd in match step_labels;
586              normalize nodelta * whd in match (point_of_label ????);
587              * #H1 #_ #_ >point_of_pc_of_point % #H2 @H1 >H2 %
588            | ** whd in match (point_of_label ????); #H1 #_ #_ % whd in match st1';
589              #H2 @H1 <H2 whd in match succ_pc; whd in match point_of_pc;
590              normalize nodelta whd in match pc_of_point; normalize nodelta
591              >point_of_offset_of_point %
592            ]
593      ]
594|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
595      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
596      assumption
597|*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
598    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
599    cases(blm mid1) in CL_JUMP COST Hst2_mid;
600    [1,5: #c #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
601    |2,4,6,8: [1,3: #c_id #args #dest |*: #seq] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
602    ]
603    #r #ltrue #_ #_ #Hst2_mid whd in match eval_statement_no_pc; normalize nodelta
604    >m_return_bind assumption
605]
606qed.
607
608
609lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
610∀prog : joint_program P_in.
611∀stack_sizes.
612∀ f_lbls,f_regs.∀f_bl_r.∀init.
613∀st_no_pc_rel,st_rel.
614let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
615let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
616let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
617good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
618                    st_no_pc_rel st_rel →
619∀st1,st1' : joint_abstract_status prog_pars_in.
620∀st2 : joint_abstract_status prog_pars_out.
621∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
622∀stmt,nxt.
623block_id … (pc_block (pc … st1)) ≠ -1 →
624st_rel st1 st2 →
625 let seq ≝ (step_seq P_in ? stmt) in
626  fetch_statement P_in …
627   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
628     return 〈f, fn,  sequential ?? seq nxt〉 →
629 eval_state P_in (prog_var_names … prog) (joint_globalenv P_in prog stack_sizes)
630  st1 = return st1' →
631∃st2'. st_rel st1' st2' ∧           
632∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
633 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
634(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
635 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
636#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel
637#goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval
638@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
639#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
640#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
641whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
642lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
643[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
644      #H cases(H EQfetch) -H |*:]
645#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
646#EQt_fn #Hinit normalize nodelta * #bl * @if_elim
647[ @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] whd in match point_of_pc;
648  normalize nodelta whd in match (point_of_offset ??); #ABS #_
649  lapply(fetch_statement_inv … EQfetch) * #_
650  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
651  normalize nodelta whd in match (point_of_offset ??); <ABS
652  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
653]
654#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
655>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
656cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
657               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
658               [2: % assumption]
659#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
660%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
661cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
662#EQfn #_
663%
664[ @(st_rel_def ?????????? goodR … f fn)
665      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
666      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
667      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
668      ]
669]
670%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
671                                      SBiC EQst2_fin_no_pc)}
672@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
673qed.
674
675
676lemma general_eval_cost_ok :
677∀ P_in , P_out: sem_graph_params.
678∀prog : joint_program P_in.
679∀stack_sizes.
680∀ f_lbls,f_regs.∀f_bl_r.∀init.
681∀st_no_pc_rel,st_rel.
682let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
683let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
684let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
685good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
686                    st_no_pc_rel st_rel →
687∀st1,st1' : joint_abstract_status prog_pars_in.
688∀st2 : joint_abstract_status prog_pars_out.
689∀f.
690∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt.
691block_id … (pc_block (pc … st1)) ≠ -1 →
692st_rel st1 st2 →
693let cost ≝ COST_LABEL P_in ? c in
694 fetch_statement P_in …
695  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
696    return 〈f, fn,  sequential ?? cost nxt〉 →
697 eval_state P_in (prog_var_names … prog) (ev_genv … prog_pars_in)
698            st1 = return st1' →
699∃ st2'. st_rel st1' st2' ∧
700∃taf : trace_any_any_free
701        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
702        st2 st2'.
703bool_to_Prop (taaf_non_empty … taf).
704#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
705#st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta
706#EQfetch
707whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta
708>EQfetch >m_return_bind normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
709#EQ destruct(EQ)
710%{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt)
711                 (last_pop … st2))} %
712[ cases(fetch_statement_inv … EQfetch) #EQfn #_
713  <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
714  whd in match (succ_pc ???); whd in match (point_of_succ ???);
715  >set_no_pc_eta
716  @(st_rel_def … prog … stack_size … goodR
717          (st_no_pc … st1) (st_no_pc … st2)) [3: >EQfn in ⊢ (??%?); %|1,2:]
718  [ @(cost_commutation … prog … stack_size … goodR … EQfetch) [ % assumption]
719    @(fetch_stmt_ok_sigma_state_ok … goodR … Rst1st2 EQfetch)
720  | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch)
721  ]
722| lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
723  [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
724      #H cases(H EQfetch) -H |*:]
725  #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
726  #EQt_fn #Hinit normalize nodelta * #bl *
727  @if_elim @eq_identifier_elim [2: #_ cases(not_emptyb ??) *]
728  [ #EQentry inversion(not_emptyb ??) [2: #_ *] #non_empty_pre #_ whd in ⊢ (% → ?);
729    inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
730    whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?);
731    * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
732    change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
733    * #EQ1 #EQ2 destruct(EQ1 EQ2)
734  | #EQentry inversion(not_emptyb ??) [ #_ *] #empty_pre #_
735    >(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *]
736   #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 *
737   #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt
738   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
739  | #EQentry #_  >(f_step_on_cost … init_data) whd in ⊢ (% → ?);
740    inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
741    * #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
742    #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
743    * #EQ1 #EQ2 destruct(EQ1 EQ2)
744  ] 
745  %{(taaf_step … (taa_base …) …)}
746  [3,6,9: @I
747  |*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
748     >EQt_fn >m_return_bind >EQt_stmt >m_return_bind %
749  ]
750]
751qed.
752
753(*
754lemma eval_return_ok :
755∀ P_in , P_out: sem_graph_params.
756∀prog : joint_program P_in.
757∀stack_sizes.
758∀ f_lbls,f_regs.∀f_bl_r.∀init.
759∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
760∀st_no_pc_rel,st_rel.
761let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
762let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
763let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
764good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
765                    st_no_pc_rel st_rel →
766∀st1,st1' :  joint_abstract_status prog_pars_in.
767∀st2 : joint_abstract_status prog_pars_out.
768∀f.
769∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
770*)
771
Note: See TracBrowser for help on using the repository browser.