source: src/joint/StatusSimulationHelper.ma @ 3050

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

1) Added general commutation theorem for monads.

2) Added some commutation lemma for push and pop that can be useful
for sigle steps of correctness proof.

3) fixed some bugs.

File size: 55.5 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "joint/semanticsUtils.ma".
16include "joint/Traces.ma".
17include "common/StatusSimulation.ma".
18include "joint/semantics_blocks.ma".
19include "utilities/listb_extra.ma".
20include "utilities/lists.ma".
21
22lemma set_no_pc_eta:
23 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
24#P * //
25qed.
26
27lemma pc_of_label_eq :
28  ∀pars: sem_graph_params.
29  ∀globals,ge,bl,i_fn,lbl.
30  fetch_internal_function ? globals ge bl = return i_fn →
31  pc_of_label pars globals ge bl lbl =
32    OK ? (pc_of_point pars bl lbl).
33#p #globals #ge #bl #i_fn #lbl #EQf
34whd in match pc_of_label;
35normalize nodelta >EQf >m_return_bind %
36qed.
37
38
39lemma bind_new_bind_new_instantiates :
40∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P.
41bind_new_instantiates B X x m l → bind_new_P' ?? P m →
42P l x.
43#B #X #m elim m normalize nodelta
44[#x #y * normalize // #B #l' #P *
45| #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H)
46 @Hr
47]
48qed.
49
50let rec bind_instantiate B X (b : bind_new B X) (l : list B) on b : (option X) ≝
51  match b with
52  [ bret B ⇒
53    match l with
54    [ nil ⇒ Some ? B
55    | _ ⇒ None ?
56    ]
57  | bnew f ⇒
58    match l with
59    [ nil ⇒ None ?
60    | cons r l' ⇒
61      bind_instantiate B X (f r) l'
62    ]
63  ].
64 
65lemma bind_instantiates_to_instantiate : ∀B,X.∀b : bind_new B X.
66∀l : list B.∀x : X.
67bind_instantiate B X b l = Some ? x →
68bind_new_instantiates B X x b l.
69#B #X #b elim b
70[#x1 * [2: #hd #tl] #x whd in ⊢ (??%? → ?); #EQ destruct(EQ) %
71|#f #IH * [2: #hd #tl] #x whd in ⊢ (??%? → ?); [2: #EQ destruct(EQ)] #H
72 whd @IH assumption
73]
74qed.
75
76lemma bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
77∀l : list B.∀x : X.
78bind_new_instantiates B X x b l →
79bind_instantiate B X b l = Some ? x.
80#B #X #b elim b
81[ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) %
82| #f #IH * [2: #hd #tl] #x whd in ⊢ (% → ?); [2: *] #H whd in ⊢ (??%?); @IH @H
83]
84qed.
85
86coercion bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
87∀l : list B.∀x : X.
88∀prf : bind_new_instantiates B X x b l.
89bind_instantiate B X b l = Some ? x ≝
90bind_instantiate_instantiates
91on _prf : bind_new_instantiates ?????
92to eq (option ?) (bind_instantiate ????) (Some ??).
93
94definition lbl_funct_type ≝  block → label → (list label).
95definition regs_funct_type ≝ block → label → (list register).
96
97
98definition preamble_length ≝
99λP_in : sem_graph_params.λP_out : sem_graph_params.λprog : joint_program P_in.
100λstack_size : (ident → option ℕ).
101λinit : ∀globals.joint_closed_internal_function P_in globals
102         →bound_b_graph_translate_data P_in P_out globals.
103λinit_regs : block → list register.
104λf_regs : regs_funct_type.λbl : block.λlbl : label.
105! bl ← code_block_of_block bl ;
106! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
107                           (joint_globalenv P_in prog stack_size) bl);
108! stmt ← stmt_at P_in … (joint_if_code … fn) lbl;
109! data ← bind_instantiate ?? (init … fn) (init_regs bl);
110match stmt with
111[ sequential step nxt ⇒
112    ! step_block ← bind_instantiate ?? (f_step … data lbl step) (f_regs bl lbl);
113    return |\fst (\fst step_block)|
114| final fin ⇒
115    ! fin_block ← bind_instantiate ?? (f_fin … data lbl fin) (f_regs bl lbl);
116    return |\fst fin_block|
117| FCOND abs _ _ _ ⇒ Ⓧabs
118].
119
120
121definition sigma_label : ∀p_in,p_out : sem_graph_params.
122joint_program p_in → (ident → option ℕ) →
123(∀globals.joint_closed_internal_function p_in globals
124         →bound_b_graph_translate_data p_in p_out globals) →
125(block → list register) → lbl_funct_type → regs_funct_type →
126block → label → option label ≝
127λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
128! bl ← code_block_of_block bl ;
129! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
130                           (joint_globalenv p_in prog stack_size) bl);
131! 〈res,s〉 ←
132 find ?? (joint_if_code ?? fn)
133  (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
134             [ None ⇒ false
135             | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
136                         [ None ⇒ false
137                         | Some x ⇒ eq_identifier … searched x
138                         ]
139             ]);
140return res.
141
142lemma partial_inj_sigma :
143∀p_in,p_out,prog,stack_size,init,init_regs.
144∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2.
145sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→
146sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 =
147sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 →
148lbl1 = lbl2.
149#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2
150inversion(sigma_label ????????? lbl1)
151[ #_ * #H @⊥ @H %]
152#lbl1' #H @('bind_inversion H) -H #bl' #EQbl'
153#H @('bind_inversion H) -H * #f #fn #H lapply(res_eq_from_opt ??? H) -H
154#EQfn #H @('bind_inversion H) -H * #res #stmt #H1 whd in ⊢ (??%? → ?);
155#EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H
156#bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) -H
157* #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ)
158lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2)
159cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???)
160normalize nodelta
161[*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim
162[2: #_ *] #EQ destruct(EQ) #_ %
163qed.
164
165definition sigma_pc_opt : 
166∀p_in,p_out : sem_graph_params.
167joint_program p_in → (ident → option ℕ) →
168(∀globals.joint_closed_internal_function p_in globals
169         →bound_b_graph_translate_data p_in p_out globals) →
170(block → list register) → lbl_funct_type → regs_funct_type →
171program_counter → option program_counter ≝
172λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
173let target_point ≝ point_of_pc p_out pc in
174if eqZb (block_id (pc_block pc)) (-1) then
175 return pc
176else
177 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs
178                   f_lbls f_regs (pc_block pc) target_point;
179 return pc_of_point p_in (pc_block pc) source_point.
180
181lemma sigma_stored_pc_inj :
182∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
183sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
184sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
185sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
186pc = pc'.
187#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs
188* #bl1 #p1 * #bl2 #p2
189inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1
190whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta
191@eqZb_elim [2: *] normalize nodelta #Hbl
192[ #H @('bind_inversion H) -H * #pt1 #EQpt1]
193whd in ⊢ (??%? → ?); #EQ destruct(EQ)
194#_ #H lapply(sym_eq ??? H) -H whd in match sigma_pc_opt;
195normalize nodelta @eqZb_elim [2,4: *] #Hbl1 normalize nodelta
196[1,2: #H @('bind_inversion H) -H * #pt2 #EQpt2] whd in match pc_of_point;
197normalize nodelta whd in match (offset_of_point ??);
198whd in ⊢ (??%% → ?); #EQ destruct(EQ)
199[2,3: @⊥ [ >Hbl in Hbl1; | >Hbl1 in Hbl;] #H @H % |4: %]
200whd in match (offset_of_point ??) in EQpt2;
201<EQpt1 in EQpt2; #H lapply(partial_inj_sigma … (sym_eq ??? H))
202[ >EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta
203whd in match (point_of_offset ??); whd in match (point_of_offset ??);
204#EQ -prog destruct(EQ) %
205qed.
206
207lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
208∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
209(∀ prf : r = Code.P (g prf)) →
210P ((match r return λx.(r = x → ?) with
211    [XData ⇒ f | Code ⇒ g])(refl ? r)).
212#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
213qed.
214
215definition sigma_stored_pc ≝
216λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
217match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
218      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
219     
220lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
221code_block_of_block bl = return bl.
222* #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
223[ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
224qed.
225
226(*TO BE MOVED*)
227lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2).
228#A #l1 elim l1 [#l2 #P *] #hd #tl #IH *
229[#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption | #H %2 @IH assumption]
230qed.
231
232lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2).
233#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
234[#a normalize // ] #hd1 #tl1 #a normalize *
235[ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 //
236| #H %2 >append_cons @IH assumption]
237qed.
238
239lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident.
240∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst.
241seq_list_in_code p globals code src l1 l2 dst → |l1| = |l2|.
242#p #globals #code #src #l1 lapply src -src elim l1
243[ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct]
244#hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct]
245#hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt
246#EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H)
247qed.
248
249lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs.
250∀f_lbls : lbl_funct_type.∀f_regs.
251b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs →
252∀id,fn.
253∀bl:Σb.block_region b = Code. ∀pt,stmt.
254block_id … bl ≠ -1 →
255fetch_internal_function …
256   (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 →
257stmt_at p_in … (joint_if_code … fn) pt = return stmt → 
258∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧
259match n with
260[ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt
261| S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧
262    sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt
263].
264#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn
265#bl #pt #stmt * #Hbl #EQfn #EQstmt   
266lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
267@eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
268#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
269lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
270[ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
271[ * #pre_instr #instr #post_instr | #pre_instr #instr] *
272[ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta
273 [ @eq_identifier_elim #EQentry normalize nodelta
274   [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
275     whd in ⊢ (???% → ?); #EQ destruct(EQ)
276   |*: #Hregs
277   ]
278 | #Hregs
279 ]
280| #Hregs
281]
282#syntax_spec
283[4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_
284[1,2,4,5: %{(|pre_instr|)} | %{O}]
285cut(? : Prop)
286[3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta
287 [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec
288           whd in match (length ??); #EQn whd in match (length ??); normalize nodelta]
289 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq
290   >m_return_bind >EQfn >m_return_bind inversion(find ????)
291   [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
292     @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind
293   >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length;
294   normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
295   whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
296   >m_return_bind cases stmt1 in EQfind; -stmt1
297   [1,4,7,10,13: #j_step1 #nxt1 |2,5,8,11,14: #fin1 |*: *] #EQfind normalize nodelta
298   cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *]
299   [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1 ]
300   >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl]
301   whd in match (length ??); normalize nodelta
302   [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] #EQ #_ >EQ %]
303   whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *]
304   #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
305   #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥
306   cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) **
307   #H #_ @H  @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
308   whd in match code_has_point; normalize nodelta >EQstmt @I
309 |*: cases syntax_spec -syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *]
310     cases pre -pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?);
311     #EQ destruct(EQ) -EQ #pre_spec whd in ⊢ (% → ?);
312     [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec
313     |*:   #EQt_stmt
314     ]
315     %{mid1} cut(? : Prop)
316     [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta
317       >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????)
318       [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
319         whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim
320         [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f
321       lapply(find_predicate ?????? EQfind) whd in match preamble_length;
322       normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
323       whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
324       >m_return_bind cases stmt1 in EQfind; -stmt1
325       [1,4,7,10: #j_step1 #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind normalize nodelta
326       cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *]
327       [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1]
328       >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1]
329       whd in match (length ??); normalize nodelta whd in match (nth_opt ???);
330       [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2
331         #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *]
332         #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_  @(proj2 … pp_labs ?? lbl2)
333         @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)]
334         >e0 @Exists_append2 % %
335       |*: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥
336         lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * -H ** #H #_ #_ @H
337         @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
338         whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
339         >(find_lookup ?????? EQfind) @I
340       ]   
341     |2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ)
342                whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?);
343                #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H)
344                [1,2: >length_map] -H #H >H >nth_opt_append_r cases(|rest|)
345                try % try( #n %) #n <minus_n_n %
346     |*:
347     ]
348  ]
349 |2,5,8,11,14: whd in match preamble_length; normalize nodelta >code_block_of_block_eq
350   >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
351   normalize nodelta
352   [1,2,3,4: >Hregs %
353   | >EQregs <EQentry in EQstmt; cases(entry_is_cost … (pi2 ?? fn)) #succ * #c
354     #EQstmt >EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data)
355     whd in match (bind_instantiate ????); %
356   ]
357 |*:
358 ]
359qed.
360
361lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls,
362f_regs,pc.
363sigma_pc_opt p_in p_out prog stack_sizes init
364   init_regs f_lbls f_regs pc ≠ None ? →
365 pc_block … pc =
366 pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init
367                                           init_regs f_lbls f_regs pc).
368#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc
369whd in match sigma_stored_pc; normalize nodelta
370inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1
371whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #_ normalize nodelta
372[ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #H @('bind_inversion H) -H
373#lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ %
374qed.
375
376lemma fetch_statement_sigma_stored_pc :
377∀p_in,p_out,prog,stack_sizes,
378init,init_regs,f_lbls,f_regs,pc,f,fn,stmt.
379b_graph_transform_program_props p_in p_out stack_sizes
380  init prog init_regs f_lbls f_regs →
381block_id … (pc_block pc) ≠ -1 →
382let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
383fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
384return 〈f,fn,stmt〉 →
385∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
386match stmt with
387[ sequential step nxt ⇒
388    ∃step_block. bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
389                 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
390    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
391                                           init_regs f_lbls f_regs pc' = pc ∧
392    ∃fn',nxt'.
393    fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
394    if not_emptyb … (added_prologue … data) ∧
395       eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
396    then return 〈f,fn',sequential ?? (NOOP …) nxt'〉
397    else return 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉
398| final fin ⇒
399    ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
400                  (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧
401    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
402                                           init_regs f_lbls f_regs pc' = pc ∧
403    ∃fn'.fetch_statement p_out …
404       (joint_globalenv p_out trans_prog stack_sizes) pc'
405       = return 〈f,fn',final ?? (\snd fin_block)〉           
406| FCOND abs _ _ _ ⇒ Ⓧabs
407].
408#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt
409#good #Hbl #EQfetch
410lapply(b_graph_transform_program_fetch_statement … good pc f fn ?)
411[2: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta
412      #H cases(H EQfetch) -H |*:]
413#data * #t_fn ** #EQt_fn #Hinit #H %{data} >Hinit %{(refl …)} cases stmt in EQfetch H;
414[ #step #nxt | #fin | *] normalize nodelta #EQfetch -stmt
415[ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta
416  [ @eq_identifier_elim #EQentry normalize nodelta ] ]
417* #block *
418[ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
419  #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1
420  whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1
421  * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
422  * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
423|*: #Hregs #syntax_spec
424]
425cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
426[ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt;
427  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ)
428  % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] |] %{pc}
429  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
430  @eqZb_elim normalize nodelta [#ABS >ABS in Hbl; * #H @⊥ @H %] #_
431|*: %{block} >Hregs %{(refl …)}
432]
433cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble
434normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab
435[   whd in match (point_of_pc ??) in e0; <EQentry in e0; #e0 >e0 in EQnth_opt;
436    whd in ⊢ (??%% → ?); #EQ destruct(EQ)
437|5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind
438    normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt}
439    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
440    >EQt_stmt >m_return_bind @eq_identifier_elim [#_ %] * #H @⊥ @H %
441|2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)}
442|6,7,8: %{pc}
443]
444whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
445@eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta
446[1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc)
447%{(refl …)} %{t_fn} cases block in Hregs syntax_spec; -block
448[1,2,4,5: * #pre #instr #post |*: #pre #instr ] #Hregs *
449[1,2,3,4: #l1 * #mid1 * #mid2 * #l2 ***
450|*: #l1 * #mid **
451]
452#EQmid #EQpre whd in ⊢ (% → ?);
453[1,2,3,4: * #nxt1 *] #EQt_stmt
454[1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2}]
455whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
456@('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?);
457#EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
458normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; -pre
459[1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
460   #EQ destruct(EQ)]
461[1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid;
462[1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct]
463   * #mid * #rest ** #EQ destruct(EQ)]
464[1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
465[4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: %] @eq_identifier_elim [2: #_ %]
466        #EQ <EQ in EQentry; * #H @⊥ @H %]
467* #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??);
468whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt;
469lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1
470>nth_opt_append_r [2,4,6: %] cut(|rest|-|rest|=O) [1,3,5: cases(|rest|) //]
471#EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 -EQ2 -EQ1
472[1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt [2: >point_of_pc_of_point %]
473      @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_
474      >point_of_pc_of_point %]
475destruct(EQ3) >point_of_pc_of_point >EQt_stmt %
476qed.
477
478definition make_is_relation_from_beval : (beval → beval → Prop) →
479internal_stack → internal_stack → Prop≝
480λR,is1,is2.
481match is1 with
482[ empty_is ⇒ match is2 with [ empty_is ⇒ True | _ ⇒ False]
483| one_is b ⇒ match is2 with [ one_is b' ⇒ R b b' | _ ⇒ False ]
484| both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2' | _ ⇒ False ]
485].
486
487lemma is_push_ok : ∀Rbeval : beval → beval → Prop.
488∀Ristack1 : internal_stack → internal_stack → Prop.
489∀Ristack2 : internal_stack → internal_stack → Prop.
490(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
491(∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 →
492                                   Ristack2 (one_is bv1) (one_is bv2)) →
493(∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 →
494                         Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) →
495                         gen_preserving2 ?? gen_res_preserve …
496                              Ristack1 Rbeval Ristack2 is_push is_push.
497#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4
498whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta
499[2:#x|3: #x #y #_ @res_preserve_error_gen]
500cases is2 normalize nodelta
501 [1,3,5,6: [| #z #w | #z | #z #w] #H5 cases(H … H5) | #y] #H5 @m_gen_return
502 [@H2 [assumption | @(H … H5) ] | @H1 assumption]
503qed.
504(*
505lemma is_push_ok : ∀R : beval → beval → Prop.
506               gen_preserving2 ?? gen_res_preserve …
507                       (make_is_relation_from_beval R) R
508                       (make_is_relation_from_beval R)
509                       is_push is_push.
510#R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H}
511qed.
512*)
513lemma is_pop_ok: ∀Rbeval : beval → beval → Prop.
514∀Ristack1 : internal_stack → internal_stack → Prop.
515∀Ristack2 : internal_stack → internal_stack → Prop.
516(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
517Ristack2 empty_is empty_is →
518(∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) →
519          gen_preserving ?? gen_res_preserve …
520                              Ristack1
521                              (λx,y.Rbeval (\fst x) (\fst y) ∧
522                                Ristack2 (\snd x) (\snd y)) is_pop is_pop.
523#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta
524cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [|#y] cases is2
525[1,3,4,5: [|#x #y||#x] #H3 cases(H … H3) | #y | #z #w] #H3 normalize nodelta
526@m_gen_return [ % [ @(H … H3) | assumption ] | cases(H … H3) #H4 #H5 %{H5} @(H2 … H4)
527qed.
528
529(*
530lemma is_pop_ok1 : ∀R : beval → beval → Prop.
531           gen_preserving ?? gen_res_preserve …
532                         (make_is_relation_from_beval R)
533                         (λx,y.R (\fst x) (\fst y) ∧
534                               (make_is_relation_from_beval R) (\snd x) (\snd y))
535                         is_pop is_pop.
536#R @is_pop_ok //
537qed.
538
539
540definition make_weak_state_relation ≝
541λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out.
542(make_is_relation_from_beval R) (istack … st1) (istack … st2).
543*)
544
545
546lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
547(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
548                  make_is_relation_from_beval Rbeval is1 is2) →
549(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
550 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
551(∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 →
552 Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) →
553                    gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2
554                                   (push p_in) (push p_out).
555#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4
556whd in match push; normalize nodelta
557@(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval))
558[ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) //
559  [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5}
560  | @(H … H3) %
561  ]
562| * [|#x|#x1 #x2] * [1,4,7:|2,5,8: #y |*: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?);
563  [1,2,3,4,6,7,8,9: * [2: #H7 #H8] | #H7] @m_gen_return
564  [ @(H2 … H3) assumption
565  | cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?);
566    #EQ destruct(EQ)
567  | @(H1 … H3) assumption
568  ]
569]
570qed.
571
572
573lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
574(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
575                  make_is_relation_from_beval Rbeval is1 is2) →
576(∀st1,st2.Rstate1 st1 st2 →
577 Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) →
578(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
579 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
580               gen_preserving ?? gen_res_preserve …
581                 Rstate1
582                (λx,y.Rbeval (\fst x) (\fst y) ∧
583                 Rstate2(\snd x) (\snd y))
584                (pop p_in) (pop p_out).
585#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3
586whd in match pop; normalize nodelta
587@(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧
588           (make_is_relation_from_beval Rbeval (\snd x) (\snd y)))) 
589[ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) %
590| * #bv1 * [|#x|#x1 #x2] * #bv2 *
591[1,4,7:|2,5,8: #y
592|*: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [|#z|#z #w] whd in ⊢ (??%% → ?); #EQ destruct ]
593#_ #_ * #H4 [2,3,4,6: *| #_ | whd in ⊢ (% → ?); #H5] @m_gen_return
594% // [ @(H1 … H3) | @(H2 … H3) assumption]
595qed.
596
597
598definition joint_state_relation ≝
599λP_in,P_out.program_counter → state P_in → state P_out → Prop.
600
601definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
602
603
604record good_state_relation (P_in : sem_graph_params)
605   (P_out : sem_graph_params) (prog : joint_program P_in)
606   (stack_sizes : ident → option ℕ)
607   (init : ∀globals.joint_closed_internal_function P_in globals
608         →bound_b_graph_translate_data P_in P_out globals)
609   (init_regs : block → list register) (f_lbls : lbl_funct_type)
610   (f_regs : regs_funct_type)
611   (st_no_pc_rel : joint_state_relation P_in P_out)
612   (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝
613{ good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init
614                     prog init_regs f_lbls f_regs
615; fetch_ok_sigma_state_ok :
616   ∀st1,st2,f,fn. st_rel st1 st2 →
617    fetch_internal_function …
618     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
619     = return 〈f,fn〉 →
620     st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
621; fetch_ok_pc_ok :
622  ∀st1,st2,f,fn.st_rel st1 st2 →
623   fetch_internal_function …
624     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
625     = return 〈f,fn〉 →
626   pc … st1 = pc … st2
627; fetch_ok_sigma_last_pop_ok :
628  ∀st1,st2,f,fn.st_rel st1 st2 →
629   fetch_internal_function …
630     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
631     = return 〈f,fn〉 →
632   (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
633                       f_lbls f_regs (last_pop … st2)
634; st_rel_def :
635  ∀st1,st2,pc,lp1,lp2,f,fn.
636  fetch_internal_function …
637     (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 →
638   st_no_pc_rel pc st1 st2 →
639   lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
640          f_lbls f_regs lp2 →
641  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
642; as_label_ok_non_entry :
643  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
644  ∀st1,st2,f,fn,stmt.
645  fetch_statement …
646  (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
647  st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
648  as_label (joint_status P_in prog stack_sizes) st1 =
649  as_label (joint_status P_out trans_prog stack_sizes) st2
650; pre_main_ok :
651  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
652    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
653    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
654    block_id … (pc_block (pc … st1)) = -1 →
655    st_rel st1 st2 →
656    as_label (joint_status P_in prog stack_sizes) st1 =
657    as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
658    joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
659    joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
660    (eval_state P_in … (joint_globalenv P_in prog stack_sizes)
661      st1 = return st1' →
662    ∃st2'. st_rel st1' st2' ∧
663    eval_state P_out …
664     (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
665; cond_commutation :
666    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
667    ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
668    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
669    ∀f,fn,a,ltrue,lfalse,bv,b.
670    block_id … (pc_block (pc … st1)) ≠ -1 →
671    let cond ≝ (COND P_in ? a ltrue) in
672    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
673    return 〈f, fn,  sequential … cond lfalse〉 → 
674    acca_retrieve … P_in (st_no_pc … st1) a = return bv →
675    bool_of_beval … bv = return b →
676    st_rel st1 st2 →
677    ∀t_fn.
678    fetch_internal_function …
679     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
680     return 〈f,t_fn〉 →
681    bind_new_P' ??
682     (λregs1.λdata.bind_new_P' ??
683     (λregs2.λblp.(\snd blp) = [ ] ∧
684        ∀mid.
685          stmt_at P_out … (joint_if_code ?? t_fn) mid
686          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
687         ∃st2_pre_mid_no_pc.
688            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
689             (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
690            = return st2_pre_mid_no_pc ∧
691            let new_pc ≝ if b then
692                           (pc_of_point P_in (pc_block (pc … st1)) ltrue)
693                         else
694                           (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
695            st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
696            ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
697            ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
698                  bool_of_beval … bv' = return b
699            (*let st2_pre_mid ≝  mk_state_pc P_out st2_pre_mid_no_pc
700                               (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in
701            let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in
702            eval_statement_advance P_out (prog_var_names … trans_prog)
703             (joint_globalenv P_out trans_prog stack_sizes) f t_fn
704             (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'*)
705   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
706  ) (init ? fn)
707; seq_commutation :
708  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
709  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
710  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
711  ∀f,fn,stmt,nxt.
712  block_id … (pc_block (pc … st1)) ≠ -1 →
713  let seq ≝ (step_seq P_in ? stmt) in
714  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
715  return 〈f, fn,  sequential … seq nxt〉 → 
716  eval_state P_in … (joint_globalenv P_in prog stack_sizes)
717  st1 = return st1' →
718  st_rel st1 st2 →
719  ∀t_fn.
720  fetch_internal_function …
721     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
722  return 〈f,t_fn〉 →
723  bind_new_P' ??
724     (λregs1.λdata.bind_new_P' ??
725      (λregs2.λblp.
726       ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
727                            blp = (ensure_step_block ?? l) ∧
728       ∃st2_fin_no_pc.
729           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
730              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
731           st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
732      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
733     ) (init ? fn)
734; cost_commutation :
735  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
736  ∀st1,st2,pc.∀f,fn,c,nxt.
737  block_id … (pc_block pc) ≠ -1 →
738  st_no_pc_rel pc st1 st2 →
739  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc =
740  return 〈f, fn,  sequential ?? (COST_LABEL ?? c) nxt〉 → 
741  st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2
742}.
743
744lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
745∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
746In ? (stmt_labels p ? stmt) lbl→
747fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
748pc' = pc_of_point p (pc_block pc) lbl →
749∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
750#p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
751cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
752#EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
753cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?)
754[3: * cases lbl #x #y cases(decidable_eq_pos … x y)
755    [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
756| whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
757  whd in match code_has_label; whd in match code_has_point; normalize nodelta
758  inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
759  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
760  >point_of_pc_of_point >EQstmt' %
761| #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
762  [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
763    normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_
764    whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
765    inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
766    whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
767    >point_of_pc_of_point >EQstmt' %
768  | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
769  ]
770]
771qed.
772
773
774
775lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
776∀prog : joint_program P_in.
777∀stack_sizes.
778∀ f_lbls,f_regs.∀f_bl_r.∀init.∀st_no_pc_rel,st_rel.
779∀f,fn,stmt,st1,st2.
780good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
781                    st_no_pc_rel st_rel →
782st_rel st1 st2 →
783fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
784 return 〈f,fn,stmt〉 →
785st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2).
786#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
787#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
788cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
789@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
790qed.
791
792lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
793∀prog : joint_program P_in.
794∀stack_sizes.
795∀ f_lbls,f_regs.∀f_bl_r.∀init.
796∀st_no_pc_rel,st_rel.
797∀f,fn,stmt,st1,st2.
798good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
799                    st_no_pc_rel st_rel→
800st_rel st1 st2 →
801fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
802 return 〈f,fn,stmt〉 →
803pc … st1 = pc … st2.
804#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
805#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
806cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
807@(fetch_ok_pc_ok … goodR … EQfn) assumption
808qed.
809
810lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
811∀prog : joint_program P_in.
812∀stack_sizes.
813∀ f_lbls,f_regs.∀f_bl_r.∀init.
814∀st_no_pc_rel,st_rel.
815∀f,fn,stmt,st1,st2.
816good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
817                    st_no_pc_rel st_rel →
818st_rel st1 st2 →
819fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
820 return 〈f,fn,stmt〉 →
821(last_pop … st1) =
822 sigma_stored_pc P_in P_out prog stack_sizes init f_bl_r f_lbls
823  f_regs (last_pop … st2).
824#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
825#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
826cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
827@(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption
828qed.
829
830(*
831lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params.
832∀prog : joint_program P_in.
833∀stack_sizes.
834∀ f_lbls,f_regs.∀f_bl_r.∀init.
835∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
836∀st_no_pc_rel,st_rel.
837∀f,fn,stmt,st1,st2.
838good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
839                    st_no_pc_rel st_rel →
840st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) →
841(last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) →
842fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
843 return 〈f,fn,stmt〉 → st_rel st1 st2.
844#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel
845#st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ)
846#EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
847@(st_rel_def … goodR … EQfn) assumption
848qed.
849*)
850
851(*
852(*CSC: Isn't this already proved somewhere else??? *)
853lemma point_of_pc_pc_of_point:
854 ∀P_in: sem_graph_params.∀l,st.
855   point_of_pc P_in
856    (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in))
857     (pc_block (pc P_in st)) l) = l.
858 #P * //
859qed.*)
860
861
862lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
863∀prog : joint_program P_in.
864∀stack_sizes.
865∀ f_lbls,f_regs.∀f_bl_r.∀init.
866∀st_no_pc_rel,st_rel.
867let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
868let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
869let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
870good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
871                    st_no_pc_rel st_rel →
872∀st1,st1' : joint_abstract_status prog_pars_in.
873∀st2 : joint_abstract_status prog_pars_out.
874∀f : ident.
875∀fn : joint_closed_internal_function P_in ?.
876∀a,ltrue,lfalse.
877block_id … (pc_block (pc … st1)) ≠ -1 →
878st_rel st1 st2 →
879 let cond ≝ (COND P_in ? a ltrue) in
880  fetch_statement P_in ?
881   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
882     return 〈f, fn, sequential … cond lfalse〉 →
883 eval_state P_in …
884  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
885as_costed (joint_abstract_status prog_pars_in) st1' →
886∃ st2'. st_rel st1' st2' ∧
887∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
888bool_to_Prop (taaf_non_empty … taf).
889#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
890#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2
891#EQfetch #EQeval
892@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
893whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
894#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
895#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
896cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
897[ >(pc_of_label_eq … EQfn)
898  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
899| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
900]
901#EQ destruct(EQ) #n_costed
902lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
903[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
904      #H cases(H EQfetch) -H |*:]
905#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
906#EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta
907*** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
908[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
909      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
910      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_
911      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
912      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
913      <ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
914]
915#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
916#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
917* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
918cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
919               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
920[2,4: % assumption]
921#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
922cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
923normalize nodelta
924#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v'
925[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
926     (last_pop … st2))}
927| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
928     (last_pop … st2))}
929]
930letin st1' ≝ (mk_state_pc P_in ???)
931letin st2' ≝ (mk_state_pc P_out ???)
932cut(st_rel st1' st2')
933[1,3: @(st_rel_def … goodR … f fn ?)
934      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
935      |2,5: assumption
936      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
937      ]
938]
939#H_fin
940%
941[1,3: assumption]
942>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
943lapply(taaf_to_taa ???
944           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
945                                       seq_pre_l EQst_pre_mid_no_pc) ?)
946[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
947      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
948      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
949      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >EQt_cond *
950      #H @H %
951]
952#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
953[1,4: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
954      [2: @ltrue|3: %2 % % |4: % |6: @lfalse |7: % % |8: %] #stmt' #EQstmt'
955      whd <(as_label_ok_non_entry … goodR … EQstmt' H_fin)
956      [1,3: assumption
957      |2,4: cases(entry_unused … (pi2 ?? fn) … EQstmt)
958            [ whd in match stmt_forall_labels; whd in match stmt_labels;
959              normalize nodelta #H cases(append_All … H) #_
960              whd in match stmt_explicit_labels; whd in match step_labels;
961              normalize nodelta * whd in match (point_of_label ????);
962              * #H1 #_ #_ >point_of_pc_of_point % #H2 @H1 >H2 %
963            | ** whd in match (point_of_label ????); #H1 #_ #_ % whd in match st1';
964              #H2 @H1 <H2 whd in match succ_pc; whd in match point_of_pc;
965              normalize nodelta whd in match pc_of_point; normalize nodelta
966              >point_of_offset_of_point %
967            ]
968      ]
969|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
970      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
971      >EQt_cond %
972|*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
973    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond
974    whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
975    whd in match eval_statement_advance; normalize nodelta >EQbv' >m_return_bind
976    >rel_v_v' >m_return_bind normalize nodelta
977    [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)]
978      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) %
979]
980qed.
981
982
983lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
984∀prog : joint_program P_in.
985∀stack_sizes.
986∀ f_lbls,f_regs.∀f_bl_r.∀init.
987∀st_no_pc_rel,st_rel.
988let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
989let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
990let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
991good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
992                    st_no_pc_rel st_rel →
993∀st1,st1' : joint_abstract_status prog_pars_in.
994∀st2 : joint_abstract_status prog_pars_out.
995∀f.∀fn : joint_closed_internal_function P_in ?.
996∀stmt,nxt.
997block_id … (pc_block (pc … st1)) ≠ -1 →
998st_rel st1 st2 →
999 let seq ≝ (step_seq P_in ? stmt) in
1000  fetch_statement P_in …
1001   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1002     return 〈f, fn,  sequential ?? seq nxt〉 →
1003 eval_state P_in … (joint_globalenv P_in prog stack_sizes)
1004  st1 = return st1' →
1005∃st2'. st_rel st1' st2' ∧           
1006∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
1007 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
1008(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
1009 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
1010#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel
1011#goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval
1012@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1013#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
1014#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
1015whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
1016lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
1017[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
1018      #H cases(H EQfetch) -H |*:]
1019#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1020#EQt_fn #Hinit normalize nodelta * #bl * @if_elim
1021[ @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] whd in match point_of_pc;
1022  normalize nodelta whd in match (point_of_offset ??); #ABS #_
1023  lapply(fetch_statement_inv … EQfetch) * #_
1024  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
1025  normalize nodelta whd in match (point_of_offset ??); <ABS
1026  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
1027]
1028#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
1029>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
1030cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
1031               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
1032               [2: % assumption]
1033#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
1034%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
1035cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1036#EQfn #_
1037%
1038[ @(st_rel_def ?????????? goodR … f fn)
1039      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
1040      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
1041      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
1042      ]
1043]
1044%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
1045                                      SBiC EQst2_fin_no_pc)}
1046@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
1047qed.
1048
1049
1050lemma general_eval_cost_ok :
1051∀ P_in , P_out: sem_graph_params.
1052∀prog : joint_program P_in.
1053∀stack_sizes.
1054∀ f_lbls,f_regs.∀f_bl_r.∀init.
1055∀st_no_pc_rel,st_rel.
1056let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
1057let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1058let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
1059good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1060                    st_no_pc_rel st_rel →
1061∀st1,st1' : joint_abstract_status prog_pars_in.
1062∀st2 : joint_abstract_status prog_pars_out.
1063∀f.
1064∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
1065block_id … (pc_block (pc … st1)) ≠ -1 →
1066st_rel st1 st2 →
1067let cost ≝ COST_LABEL P_in ? c in
1068 fetch_statement P_in …
1069  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1070    return 〈f, fn,  sequential ?? cost nxt〉 →
1071 eval_state P_in … (ev_genv … prog_pars_in)
1072            st1 = return st1' →
1073∃ st2'. st_rel st1' st2' ∧
1074∃taf : trace_any_any_free
1075        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
1076        st2 st2'.
1077bool_to_Prop (taaf_non_empty … taf).
1078#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
1079#st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta
1080#EQfetch
1081whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta
1082>EQfetch >m_return_bind normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
1083#EQ destruct(EQ)
1084%{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt)
1085                 (last_pop … st2))} %
1086[ cases(fetch_statement_inv … EQfetch) #EQfn #_
1087  <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1088  whd in match (succ_pc ???); whd in match (point_of_succ ???);
1089  >set_no_pc_eta
1090  @(st_rel_def … prog … stack_size … goodR
1091          (st_no_pc … st1) (st_no_pc … st2)) [3: >EQfn in ⊢ (??%?); %|1,2:]
1092  [ @(cost_commutation … prog … stack_size … goodR … EQfetch) [ % assumption]
1093    @(fetch_stmt_ok_sigma_state_ok … goodR … Rst1st2 EQfetch)
1094  | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch)
1095  ]
1096| lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
1097  [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
1098      #H cases(H EQfetch) -H |*:]
1099  #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1100  #EQt_fn #Hinit normalize nodelta * #bl *
1101  @if_elim @eq_identifier_elim [2: #_ cases(not_emptyb ??) *]
1102  [ #EQentry inversion(not_emptyb ??) [2: #_ *] #non_empty_pre #_ whd in ⊢ (% → ?);
1103    inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
1104    whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?);
1105    * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
1106    change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1107    * #EQ1 #EQ2 destruct(EQ1 EQ2)
1108  | #EQentry inversion(not_emptyb ??) [ #_ *] #empty_pre #_
1109    >(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *]
1110   #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 *
1111   #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt
1112   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
1113  | #EQentry #_  >(f_step_on_cost … init_data) whd in ⊢ (% → ?);
1114    inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
1115    * #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
1116    #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1117    * #EQ1 #EQ2 destruct(EQ1 EQ2)
1118  ] 
1119  %{(taaf_step … (taa_base …) …)}
1120  [3,6,9: @I
1121  |*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
1122     >EQt_fn >m_return_bind >EQt_stmt >m_return_bind %
1123  ]
1124]
1125qed.
1126
1127(*
1128lemma eval_return_ok :
1129∀ P_in , P_out: sem_graph_params.
1130∀prog : joint_program P_in.
1131∀stack_sizes.
1132∀ f_lbls,f_regs.∀f_bl_r.∀init.
1133∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
1134∀st_no_pc_rel,st_rel.
1135let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
1136let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1137let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
1138good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
1139                    st_no_pc_rel st_rel →
1140∀st1,st1' :  joint_abstract_status prog_pars_in.
1141∀st2 : joint_abstract_status prog_pars_out.
1142∀f.
1143∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
1144*)
1145
Note: See TracBrowser for help on using the repository browser.