source: src/joint/StatusSimulationHelper.ma @ 3145

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

1) finished return case in StatusSimulationHelper?

2) started to write Deliverable D4.4

File size: 91.1 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
142                                         
143                         
144
145lemma partial_inj_sigma_label :
146∀p_in,p_out,prog,stack_size,init,init_regs.
147∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2.
148sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→
149sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 =
150sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 →
151lbl1 = lbl2.
152#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2
153inversion(sigma_label ????????? lbl1)
154[ #_ * #H @⊥ @H %]
155#lbl1' #H @('bind_inversion H) -H #bl' #EQbl'
156#H @('bind_inversion H) -H * #f #fn #H lapply(res_eq_from_opt ??? H) -H
157#EQfn #H @('bind_inversion H) -H * #res #stmt #H1 whd in ⊢ (??%? → ?);
158#EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H
159#bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) -H
160* #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ)
161lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2)
162cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???)
163normalize nodelta
164[*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim
165[2: #_ *] #EQ destruct(EQ) #_ %
166qed.
167
168definition sigma_pc_opt : 
169∀p_in,p_out : sem_graph_params.
170joint_program p_in → (ident → option ℕ) →
171(∀globals.joint_closed_internal_function p_in globals
172         →bound_b_graph_translate_data p_in p_out globals) →
173(block → list register) → lbl_funct_type → regs_funct_type →
174program_counter → option program_counter ≝
175λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
176let target_point ≝ point_of_pc p_out pc in
177if eqZb (block_id (pc_block pc)) (-1) then
178 return pc
179else
180 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs
181                   f_lbls f_regs (pc_block pc) target_point;
182 return pc_of_point p_in (pc_block pc) source_point.
183
184lemma sigma_stored_pc_inj :
185∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
186sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
187sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
188sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
189pc = pc'.
190#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs
191* #bl1 #p1 * #bl2 #p2
192inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1
193whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta
194@eqZb_elim [2: *] normalize nodelta #Hbl
195[ #H @('bind_inversion H) -H * #pt1 #EQpt1]
196whd in ⊢ (??%? → ?); #EQ destruct(EQ)
197#_ #H lapply(sym_eq ??? H) -H whd in match sigma_pc_opt;
198normalize nodelta @eqZb_elim [2,4: *] #Hbl1 normalize nodelta
199[1,2: #H @('bind_inversion H) -H * #pt2 #EQpt2] whd in match pc_of_point;
200normalize nodelta whd in match (offset_of_point ??);
201whd in ⊢ (??%% → ?); #EQ destruct(EQ)
202[2,3: @⊥ [ >Hbl in Hbl1; | >Hbl1 in Hbl;] #H @H % |4: %]
203whd in match (offset_of_point ??) in EQpt2;
204<EQpt1 in EQpt2; #H lapply(partial_inj_sigma_label … (sym_eq ??? H))
205[ >EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta
206whd in match (point_of_offset ??); whd in match (point_of_offset ??);
207#EQ -prog destruct(EQ) %
208qed.
209
210lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
211∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
212(∀ prf : r = Code.P (g prf)) →
213P ((match r return λx.(r = x → ?) with
214    [XData ⇒ f | Code ⇒ g])(refl ? r)).
215#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
216qed.
217
218definition sigma_stored_pc ≝
219λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
220match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
221      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
222     
223lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
224code_block_of_block bl = return bl.
225* #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
226[ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
227qed.
228
229(*TO BE MOVED*)
230lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2).
231#A #l1 elim l1 [#l2 #P *] #hd #tl #IH *
232[#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption | #H %2 @IH assumption]
233qed.
234
235lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2).
236#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
237[#a normalize // ] #hd1 #tl1 #a normalize *
238[ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 //
239| #H %2 >append_cons @IH assumption]
240qed.
241
242lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident.
243∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst.
244seq_list_in_code p globals code src l1 l2 dst → |l1| = |l2|.
245#p #globals #code #src #l1 lapply src -src elim l1
246[ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct]
247#hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct]
248#hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt
249#EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H)
250qed.
251
252lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
253∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
254In ? (stmt_labels p ? stmt) lbl→
255fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
256pc' = pc_of_point p (pc_block pc) lbl →
257∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
258#p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
259cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
260#EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
261cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?)
262[3: * cases lbl #x #y cases(decidable_eq_pos … x y)
263    [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
264| whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
265  whd in match code_has_label; whd in match code_has_point; normalize nodelta
266  inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
267  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
268  >point_of_pc_of_point >EQstmt' %
269| #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
270  [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
271    normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_
272    whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
273    inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
274    whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
275    >point_of_pc_of_point >EQstmt' %
276  | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
277  ]
278]
279qed.
280
281
282lemma fetch_stmt_ok_nxt_ok : ∀p : sem_graph_params.
283∀prog : joint_program p.∀stack_size,f,fn,stmt,bl,pt,nxt.
284fetch_internal_function … (joint_globalenv p prog stack_size) bl =
285return 〈f,fn〉→
286stmt_at p … (joint_if_code … fn) pt = return sequential p ? stmt nxt →
287∃stmt'.
288stmt_at p … (joint_if_code … fn) nxt = return stmt'.
289#p #prog #stack_size #f #fn #stmt #bl #pt #nxt #EQfn #EQstmt
290cases(fetch_stmt_ok_succ_ok …
291       prog stack_size f fn (sequential p … stmt nxt) (pc_of_point p bl pt)
292       (pc_of_point p bl nxt) nxt ???)
293[ #stmt' #H cases(fetch_statement_inv … H) -H #_ >point_of_pc_of_point normalize nodelta
294  #EQstmt' %{stmt'} assumption
295| whd in match stmt_labels; normalize nodelta % %
296| whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
297  >point_of_pc_of_point >EQstmt %
298| %
299]
300qed.
301
302
303lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs.
304∀f_lbls : lbl_funct_type.∀f_regs.
305b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs →
306∀id,fn.
307∀bl:Σb.block_region b = Code. ∀pt,stmt.
308block_id … bl ≠ -1 →
309fetch_internal_function …
310   (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 →
311stmt_at p_in … (joint_if_code … fn) pt = return stmt → 
312∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧
313match n with
314[ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt
315| S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧
316    sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt     
317].
318#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn
319#bl #pt #stmt * #Hbl #EQfn #EQstmt   
320lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
321@eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
322#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
323lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
324[ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
325[ * #pre_instr #instr #post_instr | #pre_instr #instr] *
326[ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta
327 [ @eq_identifier_elim #EQentry normalize nodelta
328   [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
329     whd in ⊢ (???% → ?); #EQ destruct(EQ)
330   |*: #Hregs
331   ]
332 | #Hregs
333 ]
334| #Hregs
335]
336#syntax_spec
337[4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_
338[1,2,4,5: %{(|pre_instr|)} | %{O}]
339cut(? : Prop)
340[3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta
341 [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec
342           whd in match (length ??); #EQn whd in match (length ??); normalize nodelta]
343 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq
344     >m_return_bind >EQfn >m_return_bind inversion(find ????)
345     [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
346     @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind
347     >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length;
348     normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
349     whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
350     >m_return_bind cases stmt1 in EQfind; -stmt1
351     [1,4,7,10,13: #j_step1 #nxt1 |2,5,8,11,14: #fin1 |*: *] #EQfind normalize nodelta
352     cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *]
353     [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1 ]
354     >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl]
355     whd in match (length ??); normalize nodelta
356     [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
357     #EQ #_ >EQ %]
358     whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *]
359     #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
360     #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥
361     cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ)
362     ** #H #_ @H  @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
363     whd in match code_has_point; normalize nodelta >EQstmt @I
364 |*: cases syntax_spec -syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *]
365     cases pre -pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?);
366     #EQ destruct(EQ) -EQ #pre_spec whd in ⊢ (% → ?);
367     [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec
368     |*:   #EQt_stmt
369     ]
370     %{mid1} cut(? : Prop)
371     [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta
372       >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????)
373       [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
374         whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim
375         [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f
376       lapply(find_predicate ?????? EQfind) whd in match preamble_length;
377       normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
378       whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
379       >m_return_bind cases stmt1 in EQfind; -stmt1
380       [1,4,7,10: #j_step1 #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind normalize nodelta
381       cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *]
382       [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1]
383       >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1]
384       whd in match (length ??); normalize nodelta whd in match (nth_opt ???);
385       [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2
386         #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *]
387         #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_  @(proj2 … pp_labs ?? lbl2)
388         @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)]
389         >e0 @Exists_append2 % %
390       |*: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥
391         lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * -H ** #H #_ #_ @H
392         @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
393         whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
394         >(find_lookup ?????? EQfind) @I
395       ]   
396     |2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ)
397                whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?);
398                #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H)
399                [1,2: >length_map] -H #H >H >nth_opt_append_r cases(|rest|)
400                try % try( #n %) #n <minus_n_n %
401     |*:
402     ]
403  ]
404 |2,5,8,11,14: whd in match preamble_length; normalize nodelta >code_block_of_block_eq
405   >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
406   normalize nodelta
407   [1,2,3,4: >Hregs %
408   | >EQregs <EQentry in EQstmt; cases(entry_is_cost … (pi2 ?? fn)) #succ * #c
409     #EQstmt >EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data)
410     whd in match (bind_instantiate ????); %
411   ]
412 |*:
413 ]
414qed.
415
416lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls,
417f_regs,pc.
418sigma_pc_opt p_in p_out prog stack_sizes init
419   init_regs f_lbls f_regs pc ≠ None ? →
420 pc_block … pc =
421 pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init
422                                           init_regs f_lbls f_regs pc).
423#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc
424whd in match sigma_stored_pc; normalize nodelta
425inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1
426whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #_ normalize nodelta
427[ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #H @('bind_inversion H) -H
428#lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ %
429qed.
430
431definition stmt_get_next : ∀p,globals.joint_statement p globals → option (succ p) ≝
432λp,globals,stmt.
433match stmt with
434[sequential stmt nxt ⇒ Some ? nxt
435| _ ⇒ None ?
436].
437
438
439definition sigma_next : ∀p_in,p_out : sem_graph_params.
440joint_program p_in → (ident → option ℕ) →
441(∀globals.joint_closed_internal_function p_in globals
442         →bound_b_graph_translate_data p_in p_out globals) →
443(block → list register) → lbl_funct_type → regs_funct_type →
444block → label → option label ≝
445λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
446! bl ← code_block_of_block bl ;
447! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
448                           (joint_globalenv p_in prog stack_size) bl);
449! 〈res,s〉 ←
450 find ?? (joint_if_code ?? fn)
451  (λlbl.λstmt.match stmt_get_next … stmt with
452    [ None ⇒ false
453    | Some nxt ⇒
454       match preamble_length … prog stack_size init init_regs f_regs bl lbl with
455        [ None ⇒ false
456        | Some n ⇒ match nth_opt ? n ((f_lbls bl lbl) @ [nxt]) with
457                         [ None ⇒ false
458                         | Some x ⇒ eq_identifier … searched x
459                         ]
460        ]
461    ]);
462stmt_get_next … s.
463
464lemma fetch_statement_sigma_stored_pc :
465∀p_in,p_out,prog,stack_sizes,
466init,init_regs,f_lbls,f_regs,pc,f,fn,stmt.
467b_graph_transform_program_props p_in p_out stack_sizes
468  init prog init_regs f_lbls f_regs →
469block_id … (pc_block pc) ≠ -1 →
470let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
471fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
472return 〈f,fn,stmt〉 →
473∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
474match stmt with
475[ sequential step nxt ⇒
476    ∃step_block : step_block p_out (prog_names … trans_prog).
477    bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
478                 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
479    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
480                                           init_regs f_lbls f_regs pc' = pc ∧
481    ∃fn',nxt',l1,l2.
482    fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
483    if not_emptyb … (added_prologue … data) ∧
484       eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
485    then OK ? 〈f,fn',sequential ?? (NOOP …) nxt'〉
486    else OK ? 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉 ∧
487    seq_list_in_code p_out (prog_names … trans_prog) (joint_if_code … fn') (point_of_pc p_out pc)
488     (map_eval … (\fst (\fst step_block)) (point_of_pc p_out pc'))
489     l1 (point_of_pc p_out pc')
490    ∧ seq_list_in_code p_out ? (joint_if_code … fn') nxt' (\snd step_block) l2 nxt
491    ∧ sigma_next p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc_block pc) nxt' = return nxt
492| final fin ⇒
493    ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
494                  (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧
495    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
496                                           init_regs f_lbls f_regs pc' = pc ∧
497    ∃fn'.fetch_statement p_out …
498       (joint_globalenv p_out trans_prog stack_sizes) pc'
499       = return 〈f,fn',final ?? (\snd fin_block)〉           
500| FCOND abs _ _ _ ⇒ Ⓧabs
501].
502#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt
503#good #Hbl #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta
504#EQstmt
505lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn)
506@eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
507#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
508lapply(H … EQstmt) -H normalize nodelta #H #_ %{data} >Hinit %{(refl …)}
509-EQfetch cases stmt in EQstmt H;
510[ #step #nxt | #fin | *] normalize nodelta #EQstmt -stmt
511[ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta
512  [ @eq_identifier_elim #EQentry normalize nodelta ] ]
513* #block *
514[ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
515  #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1
516  whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1
517  * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
518  * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
519|*: #Hregs #syntax_spec
520]
521[ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt;
522  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ)
523  % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] |] %{pc}
524  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
525  @eqZb_elim normalize nodelta [#ABS >ABS in Hbl; * #H @⊥ @H %] #_
526|*: %{block} >Hregs %{(refl …)}
527]
528cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble
529normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab
530[   whd in match (point_of_pc ??) in e0; <EQentry in e0; #e0 >e0 in EQnth_opt;
531    whd in ⊢ (??%% → ?); #EQ destruct(EQ)
532|5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind
533    normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} %{[ ]} %{[ ]}
534    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
535    >EQt_stmt >m_return_bind %
536    [ % [ % [ @eq_identifier_elim [#_ %] * #H @⊥ @H % | %{(refl …) (refl …)}] | %{(refl …) (refl …)}]]
537    whd in match sigma_next; normalize nodelta >code_block_of_block_eq
538    >m_return_bind >EQfn >m_return_bind inversion(find ????)
539    [ #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta
540    >EQpreamble normalize  nodelta >EQentry >e0 normalize nodelta
541    @eq_identifier_elim [#_ *] * #H #_ @H %]
542    * #lbl1 #stmt1 #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
543    inversion(stmt_get_next … stmt1) [#_ *] #nxt1 #EQnxt1 normalize nodelta
544    inversion(preamble_length ?????????) [#_ *] #m whd in match preamble_length;
545    normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
546    whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind
547    >Hinit >m_return_bind cases stmt1 in EQfind; [#j_step #succ | #fin | *]
548    #EQfind normalize nodelta cases(bind_instantiate ???)
549    [1,3: whd in ⊢ (??%% → ?); #EQ destruct] #bl1 >m_return_bind whd in ⊢ (??%? → ?);
550    #EQ destruct(EQ) inversion(nth_opt ???) [1,3: #_ *] #lbl2 #EQlbl2 normalize nodelta
551    @eq_identifier_elim [2,4: #_ *] #EQ lapply EQlbl2 destruct(EQ) #EQlbl2
552    cases(Exists_append … (nth_opt_Exists ???? EQlbl2)) [2,4: * [2,4: *] #EQ >EQ #_ %]
553    #H @⊥ cases(Exists_All … H (fresh_labs lbl1)) #x * #EQ destruct(EQ) ** -H #H #_
554    @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
555    whd in match code_has_point; normalize nodelta
556    cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt2 #EQ >EQ @I
557|2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)}
558|6,7,8: %{pc}
559]
560whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
561@eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta
562[1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc)
563%{(refl …)} %{t_fn} cases block in Hregs syntax_spec; -block
564[1,2,4,5: * #pre #instr #post |*: #pre #instr ] #Hregs *
565[1,2,3,4: #l1 * #mid1 * #mid2 * #l2 ***
566|*: #l1 * #mid **
567]
568#EQmid #EQpre whd in ⊢ (% → ?);
569[1,2,3,4: * #nxt1 *] #EQt_stmt
570[1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2} %{l1} %{l2} %]
571[1,3,5,7,9,10: whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
572 @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?);
573 #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
574 normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; -pre
575 [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
576    #EQ destruct(EQ)]
577 [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid;
578 [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct]
579    * #mid * #rest ** #EQ destruct(EQ)]
580 [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
581 [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: % [ %{(refl …)} %{(refl …) (refl …)} ] assumption]
582   @eq_identifier_elim [2: #_ % [ %{(refl …)} %{(refl …) (refl …)} | assumption] ]
583   #EQ <EQ in EQentry; * #H @⊥ @H %]
584 * #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??);
585 whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt;
586 lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1
587 >nth_opt_append_r [2,4,6: %] cut(|rest|-|rest|=O) [1,3,5: cases(|rest|) //]
588 #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 -EQ2 -EQ1
589 [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt
590    [2: >point_of_pc_of_point % [%{(refl …)} whd %{mid'} %{rest} % [2: assumption] % [2: assumption] %]
591       assumption]
592    @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_ >point_of_pc_of_point %
593    [ %{(refl …)} whd %{mid'} %{rest} % [ %{(refl …)} assumption ] assumption | assumption ] ]
594 destruct(EQ3) >point_of_pc_of_point >EQt_stmt %]
595whd in match sigma_next; normalize nodelta >code_block_of_block_eq >m_return_bind
596>EQfn >m_return_bind inversion(find ????)
597[1,3,5,7: #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta >EQpreamble
598  normalize nodelta cases post in Hregs EQpost;
599  [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) @('bind_inversion EQpreamble)
600    #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn
601    >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta
602    >Hregs >m_return_bind cases pre in EQpre Hregs;
603    [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct
604    |2,4: #fst #remaining] *
605    [1,2: #lab1 * #rest ** #EQ destruct(EQ) * #nxt' * #EQpc change with nxt' in ⊢ (??%? → ?);
606      #EQ destruct(EQ) #Hrest #Hregs whd in match (length ??); whd in ⊢ (??%? → ?);
607      #EQ destruct(EQ) whd in EQmid : (??%%); destruct(EQmid) >e0
608      lapply(seq_list_in_code_length … Hrest) >length_map #EQ >EQ
609      >nth_opt_append_r
610      [2,4: >length_append whd in match (length ? [mid1]);
611             whd in match (length ? [ ]); cases(|rest|) //]
612      >length_append whd in match (length ? [mid1]); whd in match (length ? [ ]);
613      cut(S (|rest|) - (|rest| + 1) = O)
614      [1,3: cases(|rest|) // #m normalize cases m // #m1 normalize nodelta
615            cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ]
616      #EQ1 >EQ1 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
617    |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #EQregs #_ whd in EQmid : (??%%); destruct(EQmid)
618        >e0 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
619    ]
620  |*: #fst #rems #Hregs * #lab1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQmid2
621      change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest @('bind_inversion EQpreamble)
622    #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn
623      >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta
624      >Hregs >m_return_bind cases pre in EQpre Hregs;
625      [1,3,6,8: [3,4: #x #y] #_ #_ whd in ⊢ (??%? → ?); whd in match (length ??);
626        #EQ destruct|2,4: #hd1 #tl1] *
627      [1,2: #lab1 * #rest1 ** #EQ destruct(EQ) * #nxt1 * #EQpc
628        change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest1 #Hregs
629        whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ)
630      |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #Hregs #_
631      ]
632      whd in EQmid : (??%%); destruct(EQmid) >e0 normalize nodelta
633      [3,4: @eq_identifier_elim [1,3: #_ *] * #H #_ @H %]
634      lapply(seq_list_in_code_length … EQrest1) >length_map #EQ >EQ
635      >nth_opt_append_l [2,4: >length_append whd in match (length ? (mid1::?));
636      whd in match (length ? (mid2::rest)); cases(|rest1|) //] >append_cons
637      >append_cons >nth_opt_append_l
638      [2,4: >length_append >length_append whd in match (length ? [ ? ]);
639            whd in match (length ? [ ]); cases(|rest1|) // ]
640      >nth_opt_append_r
641      [2,4: >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]);
642            cases(|rest1|) // ]
643      >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]);
644      cut(S(|rest1|) - (|rest1|+1) = 0)
645      [1,3: cases(|rest1|) // #m normalize cases m // #m1 normalize nodelta
646            cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ] #EQ1 >EQ1
647      normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
648  ]
649|*: * #lab2 * [1,4,7,10: #j_step #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind
650    lapply(find_predicate ?????? EQfind) normalize nodelta [5,6,7,8: *]
651    cases(preamble_length ?????????) normalize nodelta [1,3,5,7: *] #n
652    inversion(nth_opt ???) normalize nodelta [1,3,5,7: #_ *] #lab1 #EQlab1
653    @eq_identifier_elim [2,4,6,8: #_ *] #EQ destruct(EQ)
654    cases(Exists_append … (nth_opt_Exists ???? EQlab1))
655    [2,4,6,8: * [2,4,6,8: *] #EQ destruct(EQ) cases post in Hregs EQpost;
656      [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) #_ %] #hd1 #tl1 #Hregs *
657      #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * #EQt_lab1
658      change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3
659      @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq
660      whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt
661      >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs
662      >m_return_bind cases pre in Hregs EQpre;
663      [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
664        #EQ destruct(EQ) |2,4: #hd1 #tl1] #Hregs *
665      [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc
666        change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4
667        whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_
668      |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_
669      ]
670      whd in EQmid : (??%%); destruct(EQmid) @⊥ lapply(fresh_labs (point_of_pc p_in pc))
671      >e0
672      [1,2: #H cases(append_All … H) #_ * #_ *** -H #H #_ #_ @H
673      |*: *** #H #_ #_ @H
674      ]
675      @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
676      whd in match code_has_point; normalize nodelta
677      cases(fetch_stmt_ok_nxt_ok … EQfn (find_lookup ?????? EQfind))
678      #stmt' #EQstmt' >EQstmt' @I
679    |*: #Hlab2 cases post in Hregs EQpost;
680        [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2)
681          cases(Exists_All … Hlab2 (fresh_labs lab2)) #x * #EQ destruct(EQ) ** #H
682          @⊥ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
683          whd in match code_has_point; normalize nodelta
684          cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt' #EQstmt' >EQstmt' @I
685        |*: #hd1 #tl1 #Hregs * #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 *
686          #EQt_lab1 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3
687          @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq
688          whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt
689          >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs
690          >m_return_bind cases pre in Hregs EQpre;
691          [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
692             #EQ destruct(EQ)
693          |2,4: #hd1 #tl1]
694          #Hregs *
695          [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc
696            change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4
697            whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_
698          |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_
699          ]
700          whd in EQmid : (??%%); destruct(EQmid) cases(pp_labs) #_ #H
701          lapply(H lab2 (point_of_pc p_in pc) lab1 ? ?)
702          [3,6,9,12: #EQ destruct(EQ) whd in match (stmt_at ????) in EQstmt;
703             >(find_lookup ?????? EQfind) in EQstmt; #EQ destruct(EQ) %
704          |1,4,7,10: >e0 [3,4: whd in match (memb ???); @eqb_elim
705            [2,4: * #H @⊥ @H %] #_ @I] >memb_append_l2 [1,3: @I]
706             whd in match (memb ???); @if_elim [1,3: #_ %] #_
707             whd in match (memb ???); @eqb_elim [1,3: #_ %] * #H1 @⊥ @H1 %
708          |*:  @Exists_memb assumption
709          ]
710        ]
711     ]
712]
713qed.
714
715
716definition make_is_relation_from_beval : (beval → beval → Prop) →
717internal_stack → internal_stack → Prop≝
718λR,is1,is2.
719match is1 with
720[ empty_is ⇒ match is2 with [ empty_is ⇒ True | _ ⇒ False]
721| one_is b ⇒ match is2 with [ one_is b' ⇒ R b b' | _ ⇒ False ]
722| both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2' | _ ⇒ False ]
723].
724
725lemma is_push_ok : ∀Rbeval : beval → beval → Prop.
726∀Ristack1 : internal_stack → internal_stack → Prop.
727∀Ristack2 : internal_stack → internal_stack → Prop.
728(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
729(∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 →
730                                   Ristack2 (one_is bv1) (one_is bv2)) →
731(∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 →
732                         Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) →
733                         gen_preserving2 ?? gen_res_preserve …
734                              Ristack1 Rbeval Ristack2 is_push is_push.
735#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4
736whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta
737[2:#x|3: #x #y #_ @res_preserve_error_gen]
738cases is2 normalize nodelta
739 [1,3,5,6: [| #z #w | #z | #z #w] #H5 cases(H … H5) | #y] #H5 @m_gen_return
740 [@H2 [assumption | @(H … H5) ] | @H1 assumption]
741qed.
742(*
743lemma is_push_ok : ∀R : beval → beval → Prop.
744               gen_preserving2 ?? gen_res_preserve …
745                       (make_is_relation_from_beval R) R
746                       (make_is_relation_from_beval R)
747                       is_push is_push.
748#R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H}
749qed.
750*)
751lemma is_pop_ok: ∀Rbeval : beval → beval → Prop.
752∀Ristack1 : internal_stack → internal_stack → Prop.
753∀Ristack2 : internal_stack → internal_stack → Prop.
754(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
755Ristack2 empty_is empty_is →
756(∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) →
757          gen_preserving ?? gen_res_preserve …
758                              Ristack1
759                              (λx,y.Rbeval (\fst x) (\fst y) ∧
760                                Ristack2 (\snd x) (\snd y)) is_pop is_pop.
761#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta
762cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [|#y] cases is2
763[1,3,4,5: [|#x #y||#x] #H3 cases(H … H3) | #y | #z #w] #H3 normalize nodelta
764@m_gen_return [ % [ @(H … H3) | assumption ] | cases(H … H3) #H4 #H5 %{H5} @(H2 … H4)
765qed.
766
767(*
768lemma is_pop_ok1 : ∀R : beval → beval → Prop.
769           gen_preserving ?? gen_res_preserve …
770                         (make_is_relation_from_beval R)
771                         (λx,y.R (\fst x) (\fst y) ∧
772                               (make_is_relation_from_beval R) (\snd x) (\snd y))
773                         is_pop is_pop.
774#R @is_pop_ok //
775qed.
776
777
778definition make_weak_state_relation ≝
779λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out.
780(make_is_relation_from_beval R) (istack … st1) (istack … st2).
781*)
782
783
784lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
785(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
786                  make_is_relation_from_beval Rbeval is1 is2) →
787(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
788 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
789(∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 →
790 Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) →
791                    gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2
792                                   (push p_in) (push p_out).
793#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4
794whd in match push; normalize nodelta
795@(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval))
796[ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) //
797  [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5}
798  | @(H … H3) %
799  ]
800| * [|#x|#x1 #x2] * [1,4,7:|2,5,8: #y |*: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?);
801  [1,2,3,4,6,7,8,9: * [2: #H7 #H8] | #H7] @m_gen_return
802  [ @(H2 … H3) assumption
803  | cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?);
804    #EQ destruct(EQ)
805  | @(H1 … H3) assumption
806  ]
807]
808qed.
809
810
811lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
812(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
813                  make_is_relation_from_beval Rbeval is1 is2) →
814(∀st1,st2.Rstate1 st1 st2 →
815 Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) →
816(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
817 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
818               gen_preserving ?? gen_res_preserve …
819                 Rstate1
820                (λx,y.Rbeval (\fst x) (\fst y) ∧
821                 Rstate2(\snd x) (\snd y))
822                (pop p_in) (pop p_out).
823#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3
824whd in match pop; normalize nodelta
825@(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧
826           (make_is_relation_from_beval Rbeval (\snd x) (\snd y)))) 
827[ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) %
828| * #bv1 * [|#x|#x1 #x2] * #bv2 *
829[1,4,7:|2,5,8: #y
830|*: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [|#z|#z #w] whd in ⊢ (??%% → ?); #EQ destruct ]
831#_ #_ * #H4 [2,3,4,6: *| #_ | whd in ⊢ (% → ?); #H5] @m_gen_return
832% // [ @(H1 … H3) | @(H2 … H3) assumption]
833qed.
834
835lemma fetch_internal_function_no_zero :
836∀p,prog,stack_size,bl.
837  block_id (pi1 … bl) = 0 →
838  fetch_internal_function … (joint_globalenv p prog stack_size) bl =
839  Error ? [MSG BadFunction].
840#p #prg #stack_size #bl #Hbl whd in match fetch_internal_function;
841whd in match fetch_function; normalize nodelta @eqZb_elim
842[ >Hbl #EQ @⊥ cases(not_eq_OZ_neg one) #H @H assumption ]
843#_ normalize nodelta cases(symbol_for_block ???) [%] #id >m_return_bind
844cases bl in Hbl; * #id #prf #EQ destruct(EQ)
845change with (mk_block OZ) in match (mk_block ?);
846cut(find_funct_ptr
847    (fundef (joint_closed_internal_function p (prog_names p prg)))
848    (joint_globalenv p prg stack_size) (mk_block OZ) = None ?) [%]
849#EQ >EQ %
850qed.
851 
852lemma next_of_call_pc_ok : ∀P_in,P_out : sem_graph_params.
853∀init,prog,stack_sizes,init_regs,f_lbls,f_regs.
854b_graph_transform_program_props P_in P_out stack_sizes
855  init prog init_regs f_lbls f_regs →
856let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
857∀bl :Σb.block_region b =Code.block_id bl ≠ -1 →
858∀f,fn.
859fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl =
860 return 〈f,fn〉 →
861(∀id,args,dest,lbl.
862  bind_new_P' ??
863  (λregs1.λdata.bind_new_P' ??
864   (λregs2.λblp.
865     ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
866   (f_step … data lbl (CALL P_in ? id args dest)))
867  (init ? fn)) →
868gen_preserving ?? gen_res_preserve ????
869 (λpc1,pc2 : Σpc.pc_block pc = bl.
870           sigma_stored_pc P_in P_out prog stack_sizes init
871                                           init_regs f_lbls f_regs pc2 = pc1)
872 (λn1,n2.sigma_next P_in P_out prog stack_sizes init init_regs f_lbls f_regs bl n2 = return n1)
873 (next_of_call_pc P_in … (joint_globalenv P_in prog stack_sizes))
874 (next_of_call_pc P_out … (joint_globalenv P_out trans_prog stack_sizes)).
875#p_in #p_out #init #prog #stack_sizes #init_regs #f_lbls #f_regs #good #bl #Hbl
876#f #fn #EQfn #Hcall #pc1 #pc2 #Hpc1pc2 #lbl1 #H @('bind_inversion H) -H ** #f1 #fn1 *
877[ * [#c| #id #args #dest | #r #lb | #seq ] #nxt | #fin | *]
878whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) >EQfn >m_return_bind
879#H @('bind_inversion H) -H #stmt #H lapply(opt_eq_from_res ???? H) -H
880#EQstmt whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
881cases(fetch_statement_sigma_stored_pc … pc1 f1 fn1 … good …)
882[3: >(pi2 ?? pc1) assumption
883|4: whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) in ⊢ (??%?);
884    >EQfn in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >EQstmt in ⊢ (??%?); % |2:]
885#data * #Hdata normalize nodelta * #st_bl * #Hst_bl * #pc' * #EQpc' * #t_fn
886* #nxt1 * #l1 * #l2 *** #EQt_fetch #_ #_ #nxt1rel %{nxt1} % [2: <(pi2 ?? pc1) assumption]
887whd in match next_of_call_pc; normalize nodelta <EQpc' in Hpc1pc2;
888#H lapply(sym_eq ??? H) -H whd in match sigma_stored_pc; normalize nodelta
889inversion(sigma_pc_opt ?????????)
890[ #ABS @⊥ whd in match sigma_stored_pc in EQpc'; normalize nodelta in EQpc';
891  >ABS in EQpc'; normalize nodelta #EQ <(pi2 ?? pc1) in EQfn;
892  >fetch_internal_function_no_zero [2: <EQ %] whd in ⊢ (???% → ?); #EQ1 destruct(EQ1) ]
893#sigma_pc' #EQsigma_pc' normalize nodelta inversion(sigma_pc_opt ?????????)
894[ #_ normalize nodelta #EQ destruct(EQ) @⊥ lapply EQt_fetch @if_elim #_ #EQf
895  cases(fetch_statement_inv … EQf) >fetch_internal_function_no_zero [1,3: #EQ destruct]
896  >(pc_block_eq p_in p_out prog stack_sizes init init_regs f_lbls f_regs)
897  [1,3: whd in match sigma_stored_pc; normalize nodelta >EQsigma_pc' %
898  |*: >EQsigma_pc' % #EQ destruct
899  ]
900]
901#pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQsigma_pc' in EQpc3; #H
902lapply(sym_eq ??? H) -H #EQp lapply(sigma_stored_pc_inj … EQp) [>EQsigma_pc' % #EQ destruct]
903#EQ destruct(EQ) >EQt_fetch @eq_identifier_elim
904[ #EQ1 >EQ1 in EQstmt; cases(entry_is_cost … (pi2 ?? fn1)) #nxt2 * #c #ABS >ABS #EQ1 destruct(EQ1) ]
905#_ cases(not_emptyb ??) normalize nodelta >m_return_bind normalize nodelta
906lapply(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hst_bl)
907       (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hdata)
908        (Hcall id args dest (point_of_pc p_in pc1))))
909#H cases(H (point_of_pc p_in pc2)) #id' * #args' * #dest' #EQ >EQ %
910qed.
911
912definition joint_state_relation ≝
913λP_in,P_out.program_counter → state P_in → state P_out → Prop.
914
915definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
916
917record good_state_relation (P_in : sem_graph_params)
918   (P_out : sem_graph_params) (prog : joint_program P_in)
919   (stack_sizes : ident → option ℕ)
920   (init : ∀globals.joint_closed_internal_function P_in globals
921         →bound_b_graph_translate_data P_in P_out globals)
922   (init_regs : block → list register) (f_lbls : lbl_funct_type)
923   (f_regs : regs_funct_type)
924   (st_no_pc_rel : joint_state_relation P_in P_out)
925   (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝
926{ good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init
927                     prog init_regs f_lbls f_regs
928; fetch_ok_sigma_state_ok :
929   ∀st1,st2,f,fn. st_rel st1 st2 →
930    fetch_internal_function …
931     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
932     = return 〈f,fn〉 →
933     st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
934; fetch_ok_pc_ok :
935  ∀st1,st2,f,fn.st_rel st1 st2 →
936   fetch_internal_function …
937     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
938     = return 〈f,fn〉 →
939   pc … st1 = pc … st2
940; fetch_ok_sigma_last_pop_ok :
941  ∀st1,st2,f,fn.st_rel st1 st2 →
942   fetch_internal_function …
943     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
944     = return 〈f,fn〉 →
945   (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
946                       f_lbls f_regs (last_pop … st2)
947; st_rel_def :
948  ∀st1,st2,pc,lp1,lp2,f,fn.
949  fetch_internal_function …
950     (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 →
951   st_no_pc_rel pc st1 st2 →
952   lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
953          f_lbls f_regs lp2 →
954  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
955; as_label_ok_non_entry :
956  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
957  ∀st1,st2,f,fn,stmt.
958  fetch_statement …
959  (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
960  st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
961  as_label (joint_status P_in prog stack_sizes) st1 =
962  as_label (joint_status P_out trans_prog stack_sizes) st2
963; pre_main_ok :
964  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
965    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
966    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
967    block_id … (pc_block (pc … st1)) = -1 →
968    st_rel st1 st2 →
969    as_label (joint_status P_in prog stack_sizes) st1 =
970    as_label (joint_status P_out trans_prog stack_sizes) st2 ∧
971    joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
972    joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
973    (eval_state P_in … (joint_globalenv P_in prog stack_sizes)
974      st1 = return st1' →
975    ∃st2'. st_rel st1' st2' ∧
976    eval_state P_out …
977     (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')
978; cond_commutation :
979    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
980    ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
981    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
982    ∀f,fn,a,ltrue,lfalse,bv,b.
983    block_id … (pc_block (pc … st1)) ≠ -1 →
984    let cond ≝ (COND P_in ? a ltrue) in
985    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
986    return 〈f, fn,  sequential … cond lfalse〉 → 
987    acca_retrieve … P_in (st_no_pc … st1) a = return bv →
988    bool_of_beval … bv = return b →
989    st_rel st1 st2 →
990    ∀t_fn.
991    fetch_internal_function …
992     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
993     return 〈f,t_fn〉 →
994    bind_new_P' ??
995     (λregs1.λdata.bind_new_P' ??
996     (λregs2.λblp.(\snd blp) = [ ] ∧
997        ∀mid.
998          stmt_at P_out … (joint_if_code ?? t_fn) mid
999          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
1000         ∃st2_pre_mid_no_pc.
1001            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
1002             (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
1003            = return st2_pre_mid_no_pc ∧
1004            let new_pc ≝ if b then
1005                           (pc_of_point P_in (pc_block (pc … st1)) ltrue)
1006                         else
1007                           (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
1008            st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
1009            ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
1010            ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
1011                  bool_of_beval … bv' = return b
1012   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
1013  ) (init ? fn)
1014; seq_commutation :
1015  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
1016  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
1017  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
1018  ∀f,fn,stmt,nxt.
1019  block_id … (pc_block (pc … st1)) ≠ -1 →
1020  let seq ≝ (step_seq P_in ? stmt) in
1021  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1022  return 〈f, fn,  sequential … seq nxt〉 → 
1023  eval_state P_in … (joint_globalenv P_in prog stack_sizes)
1024  st1 = return st1' →
1025  st_rel st1 st2 →
1026  ∀t_fn.
1027  fetch_internal_function …
1028     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
1029  return 〈f,t_fn〉 →
1030  bind_new_P' ??
1031     (λregs1.λdata.bind_new_P' ??
1032      (λregs2.λblp.
1033       ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
1034                            blp = (ensure_step_block ?? l) ∧
1035       ∃st2_fin_no_pc.
1036           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
1037              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
1038           st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
1039      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
1040     ) (init ? fn)
1041;  call_is_call :∀f,fn,bl.
1042  fetch_internal_function …
1043     (joint_globalenv P_in prog stack_sizes) bl = return 〈f,fn〉 →
1044   ∀id,args,dest,lbl.
1045    bind_new_P' ??
1046     (λregs1.λdata.bind_new_P' ??
1047      (λregs2.λblp.
1048        ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
1049      (f_step … data lbl (CALL P_in ? id args dest)))
1050     (init ? fn)
1051; cost_commutation :
1052  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
1053  ∀st1,st2,pc.∀f,fn,c,nxt.
1054  block_id … (pc_block pc) ≠ -1 →
1055  st_no_pc_rel pc st1 st2 →
1056  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc =
1057  return 〈f, fn,  sequential ?? (COST_LABEL ?? c) nxt〉 → 
1058  st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2
1059; return_commutation :
1060  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
1061  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
1062  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
1063  ∀f,fn.
1064  block_id … (pc_block (pc … st1)) ≠ -1 →
1065  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1066  return 〈f, fn,  final P_in ? (RETURN …)〉 → 
1067  ∀n. stack_sizes f = return n →
1068  let curr_ret ≝ joint_if_result … fn in
1069  ∀st_pop,pc_pop.
1070  pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret
1071   (st_no_pc … st1) = return 〈st_pop,pc_pop〉 →
1072  ∀nxt.∀f1,fn1,id,args,dest.
1073    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop  =
1074    return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 →
1075  st_rel st1 st2 →
1076  ∀t_fn.
1077  fetch_internal_function …
1078     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
1079  return 〈f,t_fn〉 →
1080  bind_new_P' ??
1081     (λregs1.λdata.
1082      bind_new_P' ??
1083      (λregs2.λblp.
1084       \snd blp = (RETURN …) ∧
1085       ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
1086              (\fst blp)  (st_no_pc … st2)= return st_fin ∧
1087        ∃t_st_pop,t_pc_pop.
1088        pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f
1089         (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧
1090        sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs
1091         t_pc_pop = pc_pop ∧
1092        if eqZb (block_id (pc_block pc_pop)) (-1) then
1093            st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
1094             (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*)
1095        else
1096            bind_new_P' ??
1097            (λregs4.λdata1.
1098               bind_new_P' ??
1099               (λregs3.λblp1.
1100                 ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
1101                      (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧
1102                      st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
1103                       (decrement_stack_usage ? n st_pop) st2'
1104               ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest))
1105            ) (init ? fn1)
1106          ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …))
1107     ) (init ? fn)
1108; call_commutation :
1109  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
1110  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
1111  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
1112  ∀f,fn,id,arg,dest,nxt.
1113  block_id … (pc_block (pc … st1)) ≠ -1 →
1114  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1115  return 〈f, fn,  sequential P_in ? (CALL P_in ? id arg dest) nxt〉 →
1116  ∀bl.
1117   block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1)
1118      = return bl →
1119  ∀f1,fn1.
1120   fetch_internal_function …
1121    (joint_globalenv P_in prog stack_sizes) bl =  return 〈f1,fn1〉 →
1122  ∀st1_pre.
1123  save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre →
1124  ∀n.stack_sizes f1 = return n → 
1125  ∀st1'.
1126  setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
1127  st_rel st1 st2 → 
1128  ∀t_fn.
1129  fetch_internal_function …
1130  (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
1131  return 〈f,t_fn〉 →
1132  ∀t_fn1.
1133  fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl =
1134  return 〈f1,t_fn1〉 →
1135  bind_new_P' ??
1136    (λregs1.λdata.
1137     bind_new_P' ??
1138      (λregs2.λblp.
1139        ∀mid,id',arg',dest',nxt1.
1140          stmt_at P_out … (joint_if_code ?? t_fn) mid
1141          = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→
1142          ((\snd (\fst blp)) mid) = (CALL P_out ? id' arg' dest') → 
1143       ∃st2_pre_call.
1144        repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
1145          (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) = return st2_pre_call ∧
1146       block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id'
1147        st2_pre_call = return bl ∧
1148       ∃st2_pre.
1149        save_frame … P_out (kind_of_call P_out id') dest'
1150         (mk_state_pc ? st2_pre_call (pc_of_point P_out (pc_block(pc … st2)) mid)
1151          (last_pop … st2)) = return st2_pre ∧
1152       ∃st2_after_call.
1153         setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
1154          = return st2_after_call ∧
1155       bind_new_P' ??
1156         (λregs11.λdata1.
1157          ∃st2'.
1158           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
1159           (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
1160           return st2' ∧
1161           st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1))
1162            (increment_stack_usage P_in n st1') st2'
1163               
1164         ) (init ? fn1)
1165     )
1166     (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest))
1167    ) (init ? fn)
1168}.
1169
1170definition JointStatusSimulation :
1171∀p_in,p_out : sem_graph_params.
1172∀ prog.∀stack_sizes.
1173∀ f_lbls, f_regs. ∀init_regs.∀init.∀st_no_pc_rel,st_rel.
1174good_state_relation p_in p_out prog stack_sizes init init_regs f_lbls f_regs
1175                    st_no_pc_rel st_rel →
1176let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
1177status_rel (joint_abstract_status (mk_prog_params p_in prog stack_sizes))
1178           (joint_abstract_status (mk_prog_params p_out trans_prog stack_sizes)) ≝
1179λp_in,p_out,prog,stack_sizes,f_lbls,f_regs,init_regs,init,st_no_pc_rel,st_rel,good.
1180   mk_status_rel ??
1181    (* sem_rel ≝ *) (λs1 : (joint_abstract_status (mk_prog_params p_in ??)).
1182                     λs2 : (joint_abstract_status (mk_prog_params p_out ??)).st_rel s1 s2)
1183    (* call_rel ≝ *) 
1184       (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call
1185          .λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call
1186           .pc ? s1 =
1187        sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
1188
1189(*
1190lemma fetch_stmt_ok_succs_ok : ∀p : sem_graph_params.
1191∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
1192In ? (stmt_labels p ? stmt) lbl→
1193fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
1194pc' = pc_of_point p (pc_block pc) lbl →
1195∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
1196#p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
1197cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
1198#EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
1199cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?)
1200[3: * cases lbl #x #y cases(decidable_eq_pos … x y)
1201    [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
1202| whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
1203  whd in match code_has_label; whd in match code_has_point; normalize nodelta
1204  inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
1205  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
1206  >point_of_pc_of_point >EQstmt' %
1207| #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
1208  [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
1209    normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_
1210    whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
1211    inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
1212    whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
1213    >point_of_pc_of_point >EQstmt' %
1214  | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
1215  ]
1216]
1217qed.
1218*)
1219
1220
1221lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
1222∀prog : joint_program P_in.
1223∀stack_sizes.
1224∀ f_lbls,f_regs.∀f_bl_r.∀init.∀st_no_pc_rel,st_rel.
1225∀f,fn,stmt,st1,st2.
1226good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1227                    st_no_pc_rel st_rel →
1228st_rel st1 st2 →
1229fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1230 return 〈f,fn,stmt〉 →
1231st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2).
1232#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
1233#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
1234cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
1235@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
1236qed.
1237
1238lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
1239∀prog : joint_program P_in.
1240∀stack_sizes.
1241∀ f_lbls,f_regs.∀f_bl_r.∀init.
1242∀st_no_pc_rel,st_rel.
1243∀f,fn,stmt,st1,st2.
1244good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
1245                    st_no_pc_rel st_rel→
1246st_rel st1 st2 →
1247fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1248 return 〈f,fn,stmt〉 →
1249pc … st1 = pc … st2.
1250#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
1251#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
1252cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
1253@(fetch_ok_pc_ok … goodR … EQfn) assumption
1254qed.
1255
1256lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
1257∀prog : joint_program P_in.
1258∀stack_sizes.
1259∀ f_lbls,f_regs.∀f_bl_r.∀init.
1260∀st_no_pc_rel,st_rel.
1261∀f,fn,stmt,st1,st2.
1262good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1263                    st_no_pc_rel st_rel →
1264st_rel st1 st2 →
1265fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
1266 return 〈f,fn,stmt〉 →
1267(last_pop … st1) =
1268 sigma_stored_pc P_in P_out prog stack_sizes init f_bl_r f_lbls
1269  f_regs (last_pop … st2).
1270#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
1271#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
1272cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
1273@(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption
1274qed.
1275
1276(*
1277lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params.
1278∀prog : joint_program P_in.
1279∀stack_sizes.
1280∀ f_lbls,f_regs.∀f_bl_r.∀init.
1281∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
1282∀st_no_pc_rel,st_rel.
1283∀f,fn,stmt,st1,st2.
1284good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good
1285                    st_no_pc_rel st_rel →
1286st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) →
1287(last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) →
1288fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
1289 return 〈f,fn,stmt〉 → st_rel st1 st2.
1290#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel
1291#st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ)
1292#EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
1293@(st_rel_def … goodR … EQfn) assumption
1294qed.
1295*)
1296
1297(*
1298(*CSC: Isn't this already proved somewhere else??? *)
1299lemma point_of_pc_pc_of_point:
1300 ∀P_in: sem_graph_params.∀l,st.
1301   point_of_pc P_in
1302    (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in))
1303     (pc_block (pc P_in st)) l) = l.
1304 #P * //
1305qed.*)
1306
1307
1308lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
1309∀prog : joint_program P_in.
1310∀stack_sizes.
1311∀ f_lbls,f_regs.∀f_bl_r.∀init.
1312∀st_no_pc_rel,st_rel.
1313let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
1314let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1315let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
1316good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1317                    st_no_pc_rel st_rel →
1318∀st1,st1' : joint_abstract_status prog_pars_in.
1319∀st2 : joint_abstract_status prog_pars_out.
1320∀f : ident.
1321∀fn : joint_closed_internal_function P_in ?.
1322∀a,ltrue,lfalse.
1323block_id … (pc_block (pc … st1)) ≠ -1 →
1324st_rel st1 st2 →
1325 let cond ≝ (COND P_in ? a ltrue) in
1326  fetch_statement P_in ?
1327   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1328     return 〈f, fn, sequential … cond lfalse〉 →
1329 eval_state P_in …
1330  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
1331as_costed (joint_abstract_status prog_pars_in) st1' →
1332∃ st2'. st_rel st1' st2' ∧
1333∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
1334bool_to_Prop (taaf_non_empty … taf).
1335#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
1336#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2
1337#EQfetch #EQeval
1338@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1339whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
1340#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
1341#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
1342cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
1343[ >(pc_of_label_eq … EQfn)
1344  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
1345| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
1346]
1347#EQ destruct(EQ) #n_costed
1348lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
1349[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
1350      #H cases(H EQfetch) -H |*:]
1351#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1352#EQt_fn1 whd in ⊢ (% → ?); #Hinit normalize nodelta
1353*** #blp #blm #bls * whd in ⊢ (% → ?); @if_elim
1354[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
1355      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
1356      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_
1357      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1358      whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??);
1359      <ABS cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
1360]
1361#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
1362#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
1363* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1364cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
1365               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)))
1366[2,4: % assumption]
1367#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
1368cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
1369normalize nodelta
1370#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v'
1371[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
1372     (last_pop … st2))}
1373| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
1374     (last_pop … st2))}
1375]
1376letin st1' ≝ (mk_state_pc P_in ???)
1377letin st2' ≝ (mk_state_pc P_out ???)
1378cut(st_rel st1' st2')
1379[1,3: @(st_rel_def … goodR … f fn ?)
1380      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
1381      |2,5: assumption
1382      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
1383      ]
1384]
1385#H_fin
1386%
1387[1,3: assumption]
1388>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
1389lapply(taaf_to_taa ???
1390           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
1391                                       seq_pre_l EQst_pre_mid_no_pc) ?)
1392[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
1393      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
1394      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
1395      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >EQt_cond *
1396      #H @H %
1397]
1398#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
1399[1,4: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
1400      [2: @ltrue|3: %2 % % |4: % |6: @lfalse |7: % % |8: %] #stmt' #EQstmt'
1401      whd <(as_label_ok_non_entry … goodR … EQstmt' H_fin)
1402      [1,3: assumption
1403      |2,4: cases(entry_unused … (pi2 ?? fn) … EQstmt)
1404            [ whd in match stmt_forall_labels; whd in match stmt_labels;
1405              normalize nodelta #H cases(append_All … H) #_
1406              whd in match stmt_explicit_labels; whd in match step_labels;
1407              normalize nodelta * whd in match (point_of_label ????);
1408              * #H1 #_ #_ >point_of_pc_of_point % #H2 @H1 >H2 %
1409            | ** whd in match (point_of_label ????); #H1 #_ #_ % whd in match st1';
1410              #H2 @H1 <H2 whd in match succ_pc; whd in match point_of_pc;
1411              normalize nodelta whd in match pc_of_point; normalize nodelta
1412              >point_of_offset_of_point %
1413            ]
1414      ]
1415|2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
1416      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
1417      >EQt_cond %
1418|*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
1419    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond
1420    whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
1421    whd in match eval_statement_advance; normalize nodelta >EQbv' >m_return_bind
1422    >rel_v_v' >m_return_bind normalize nodelta
1423    [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)]
1424      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) %
1425]
1426qed.
1427
1428
1429lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
1430∀prog : joint_program P_in.
1431∀stack_sizes.
1432∀ f_lbls,f_regs.∀f_bl_r.∀init.
1433∀st_no_pc_rel,st_rel.
1434let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
1435let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1436let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
1437good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1438                    st_no_pc_rel st_rel →
1439∀st1,st1' : joint_abstract_status prog_pars_in.
1440∀st2 : joint_abstract_status prog_pars_out.
1441∀f.∀fn : joint_closed_internal_function P_in ?.
1442∀stmt,nxt.
1443block_id … (pc_block (pc … st1)) ≠ -1 →
1444st_rel st1 st2 →
1445 let seq ≝ (step_seq P_in ? stmt) in
1446  fetch_statement P_in …
1447   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1448     return 〈f, fn,  sequential ?? seq nxt〉 →
1449 eval_state P_in … (joint_globalenv P_in prog stack_sizes)
1450  st1 = return st1' →
1451∃st2'. st_rel st1' st2' ∧           
1452∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
1453 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
1454(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
1455 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
1456#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel
1457#goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval
1458@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1459#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
1460#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
1461whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
1462lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
1463[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
1464      #H cases(H EQfetch) -H |*:]
1465#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1466#EQt_fn #Hinit normalize nodelta * #bl * @if_elim
1467[ @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] whd in match point_of_pc;
1468  normalize nodelta whd in match (point_of_offset ??); #ABS #_
1469  lapply(fetch_statement_inv … EQfetch) * #_
1470  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
1471  normalize nodelta whd in match (point_of_offset ??); <ABS
1472  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
1473]
1474#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
1475>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
1476cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
1477               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
1478               [2: % assumption]
1479#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
1480%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
1481cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1482#EQfn #_
1483%
1484[ @(st_rel_def ?????????? goodR … f fn)
1485      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
1486      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
1487      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
1488      ]
1489]
1490%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
1491                                      SBiC EQst2_fin_no_pc)}
1492@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
1493qed.
1494
1495
1496lemma general_eval_cost_ok :
1497∀ P_in , P_out: sem_graph_params.
1498∀prog : joint_program P_in.
1499∀stack_sizes.
1500∀ f_lbls,f_regs.∀f_bl_r.∀init.
1501∀st_no_pc_rel,st_rel.
1502let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
1503let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1504let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
1505good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1506                    st_no_pc_rel st_rel →
1507∀st1,st1' : joint_abstract_status prog_pars_in.
1508∀st2 : joint_abstract_status prog_pars_out.
1509∀f.
1510∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
1511block_id … (pc_block (pc … st1)) ≠ -1 →
1512st_rel st1 st2 →
1513let cost ≝ COST_LABEL P_in ? c in
1514 fetch_statement P_in …
1515  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1516    return 〈f, fn,  sequential ?? cost nxt〉 →
1517 eval_state P_in … (ev_genv … prog_pars_in)
1518            st1 = return st1' →
1519∃ st2'. st_rel st1' st2' ∧
1520∃taf : trace_any_any_free
1521        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
1522        st2 st2'.
1523bool_to_Prop (taaf_non_empty … taf).
1524#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
1525#st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta
1526#EQfetch
1527whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta
1528>EQfetch >m_return_bind normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
1529#EQ destruct(EQ)
1530%{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt)
1531                 (last_pop … st2))} %
1532[ cases(fetch_statement_inv … EQfetch) #EQfn #_
1533  <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1534  whd in match (succ_pc ???); whd in match (point_of_succ ???);
1535  >set_no_pc_eta
1536  @(st_rel_def … prog … stack_size … goodR
1537          (st_no_pc … st1) (st_no_pc … st2)) [3: >EQfn in ⊢ (??%?); %|1,2:]
1538  [ @(cost_commutation … prog … stack_size … goodR … EQfetch) [ % assumption]
1539    @(fetch_stmt_ok_sigma_state_ok … goodR … Rst1st2 EQfetch)
1540  | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch)
1541  ]
1542| lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
1543  [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
1544      #H cases(H EQfetch) -H |*:]
1545  #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
1546  #EQt_fn #Hinit normalize nodelta * #bl *
1547  @if_elim @eq_identifier_elim [2: #_ cases(not_emptyb ??) *]
1548  [ #EQentry inversion(not_emptyb ??) [2: #_ *] #non_empty_pre #_ whd in ⊢ (% → ?);
1549    inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
1550    whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?);
1551    * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
1552    change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1553    * #EQ1 #EQ2 destruct(EQ1 EQ2)
1554  | #EQentry inversion(not_emptyb ??) [ #_ *] #empty_pre #_
1555    >(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *]
1556   #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 *
1557   #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt
1558   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
1559  | #EQentry #_  >(f_step_on_cost … init_data) whd in ⊢ (% → ?);
1560    inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
1561    * #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
1562    #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1563    * #EQ1 #EQ2 destruct(EQ1 EQ2)
1564  ] 
1565  %{(taaf_step … (taa_base …) …)}
1566  [3,6,9: @I
1567  |*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
1568     >EQt_fn >m_return_bind >EQt_stmt >m_return_bind %
1569  ]
1570]
1571qed.
1572
1573lemma next_of_call_pc_error : ∀pars.∀prog. ∀stack_size,pc.
1574block_id (pi1 … (pc_block pc)) = 0→
1575next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size))
1576  pc = Error ? [MSG BadFunction].
1577#pars #prg #init #pc #EQ whd in match next_of_call_pc; normalize nodelta
1578whd in match fetch_statement; normalize nodelta
1579>fetch_internal_function_no_zero //
1580qed.
1581
1582lemma next_of_call_pc_inv :  ∀pars.∀prog. ∀stack_size.
1583∀pc,nxt.
1584next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size)) pc
1585= return nxt →
1586∃id,fn,c_id,c_args,c_dest.
1587fetch_statement pars
1588    … (ev_genv … (mk_prog_params pars prog stack_size)) pc =
1589    return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉.
1590#pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta
1591#H @('bind_inversion H) -H ** #id #fn *
1592[ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | #H #r #l #l ]
1593#EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1594%{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption
1595qed.
1596
1597lemma stored_pc_inj :
1598∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
1599sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
1600sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
1601sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
1602pc = pc'.
1603#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H
1604whd in match sigma_stored_pc; normalize nodelta
1605inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1
1606normalize nodelta inversion(sigma_pc_opt ?????????)
1607[ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1; whd in match sigma_pc_opt;
1608  normalize nodelta @eqZb_elim
1609  [ #ABS1 whd in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ABS1 : (??%%); destruct]
1610  #Hbl normalize nodelta #H @('bind_inversion H) -H #lbl whd in match sigma_label;
1611  normalize nodelta >code_block_of_block_eq >m_return_bind
1612  >fetch_internal_function_no_zero [ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
1613  >(pc_block_eq … H) whd in match sigma_stored_pc; normalize nodelta >EQpc1 %
1614]
1615#pc2 #EQpc2 normalize nodelta #EQ destruct(EQ)
1616@(sigma_stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs …)
1617[ assumption] >EQpc1 >EQpc2 %
1618qed.
1619
1620
1621
1622
1623
1624lemma eval_return_ok :
1625∀ P_in , P_out: sem_graph_params.
1626∀prog : joint_program P_in.
1627∀stack_sizes.
1628∀ f_lbls,f_regs.∀f_bl_r.∀init.
1629∀st_no_pc_rel,st_rel.
1630let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
1631let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1632let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
1633∀good : good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1634                    st_no_pc_rel st_rel.
1635∀st1,st1' : joint_abstract_status prog_pars_in.
1636∀st2 : joint_abstract_status prog_pars_out.
1637∀f.
1638∀fn : joint_closed_internal_function P_in ?.
1639block_id … (pc_block (pc … st1)) ≠ -1 →
1640st_rel st1 st2 →
1641 fetch_statement P_in …
1642  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1643    return 〈f, fn,final P_in ? (RETURN …)〉 →
1644 eval_state P_in … (ev_genv … prog_pars_in)
1645            st1 = return st1' →
1646∃st2_ret,st2_after_ret,st2' : joint_abstract_status prog_pars_out.
1647∃taa2 : trace_any_any … st2 st2_ret.
1648∃taa2' : trace_any_any_free … st2_after_ret st2'.
1649(if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
1650as_classifier … st2_ret cl_return ∧
1651        as_execute … st2_ret st2_after_ret ∧ st_rel st1' st2' ∧
1652        ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret.
1653#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
1654#st_rel #good #st1 #st1' #st2 #f #fn #Hbl #Rst1st2 #EQfetch
1655whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
1656whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
1657whd in match eval_statement_advance; whd in match eval_return; normalize nodelta
1658#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #ssize
1659#H lapply(opt_eq_from_res ???? H) -H change with (stack_size f) in ⊢ (??%? → ?);
1660#EQssize #H @('bind_inversion H) -H * #st_pop #pc_pop #EQpop #H @('bind_inversion H)
1661-H #next_of_call #EQnext_of_call whd in ⊢ (??%% → ?); whd in match next;
1662whd in match set_last_pop; whd in match set_pc; normalize nodelta #EQ destruct(EQ)
1663lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
1664[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta
1665      #H cases(H EQfetch) -H |*:]
1666#data * #t_fn ** #EQt_fn >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn;
1667#EQt_fn #Hinit normalize nodelta ** #pre #fin_s * #Hregs * #pre * #mid
1668** #EQmid #EQpre whd in ⊢ (% → ?); #EQt_stmt
1669cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall
1670<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs
1671cases(bind_new_bind_new_instantiates … Hregs (bind_new_bind_new_instantiates … Hinit
1672 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall …
1673   Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
1674** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta
1675[ #sem_rel (*premain case TODO *) cases daemon ]
1676cases(fetch_statement_sigma_stored_pc … good … Hbl_pcpop … EQcall) #data1 * #Hinit1
1677normalize nodelta *** #pre_c #instr_c #post_c * #Hregs1 * #pc1 * destruct(EQt_pc_pop)
1678whd in match sigma_stored_pc in ⊢ (% → ?); normalize nodelta
1679inversion(sigma_pc_opt ???????? t_pc_pop)
1680[ #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero [#EQ destruct(EQ)]
1681  whd in match sigma_stored_pc; normalize nodelta >ABS %]
1682#pc2 #EQpc2 normalize nodelta inversion(sigma_pc_opt ?????????)
1683[ #_ normalize nodelta #EQ destruct(EQ) cases(fetch_statement_inv … EQcall)
1684  >fetch_internal_function_no_zero [2: whd in match sigma_stored_pc; normalize nodelta >EQpc2 %]
1685  #EQ destruct(EQ) ]
1686#pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQpc2 in EQpc3; #H lapply(sym_eq ??? H) -H #H
1687lapply(sigma_stored_pc_inj … H) [ >EQpc2 % #EQ destruct] #EQ destruct(EQ) * #t_fn1 * #nxt1
1688* #pre * #post @eq_identifier_elim
1689[ #EQentry cases(entry_is_cost … (pi2 ?? fn1)) #nxt1 * #c <EQentry #ABS
1690  cases(fetch_statement_inv … EQcall) #_ normalize nodelta >ABS #EQ destruct(EQ) ]
1691#_ cut(∀x : bool.andb x false = false) [* %] #EQ >EQ -EQ normalize nodelta ***
1692cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1)
1693 (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1)
1694  ((call_is_call … good … (proj1 … (fetch_statement_inv … EQcall))) id args dest ?)) (point_of_pc p_in pc1))
1695#id' * #args' * #dest' #EQ >EQ -EQ #EQt_call #EQpre_c #EQpost_c #EQnxt1 #H
1696cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1)
1697      (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1) H))
1698-H #st2' * #EQst2' #fin_sem_rel
1699%{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))}
1700%{(next p_out nxt1
1701   (set_last_pop p_out (decrement_stack_usage ? ssize t_st_pop) pc1))}
1702%{(mk_state_pc ? st2' (pc_of_point p_out (pc_block pc1) next_of_call) pc1)}
1703%{((taaf_to_taa …
1704     (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))}
1705[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); whd in match (as_label ??);
1706  whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
1707  >point_of_pc_of_point >EQt_stmt >m_return_bind normalize nodelta * #H @H % ]
1708letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog)
1709lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size) ??????????)
1710[11: * #taaf * #_ #prf %{taaf}
1711|3: change with (pc_block pc1) in match (pc_block ?);
1712    @(proj1 … (fetch_statement_inv … EQt_call))
1713|2: whd in match next; whd in match succ_pc; whd in match set_pc;
1714    whd in match point_of_pc; normalize nodelta whd in match pc_of_point;
1715    normalize nodelta >point_of_offset_of_point in ⊢ (????%???);
1716    whd in match (point_of_succ ???); @EQpost_c
1717|1: assumption
1718|*:
1719]
1720%
1721[ %
1722  [ %
1723    [ %
1724      [ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *]
1725        #hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) *
1726        #succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ)
1727        #EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??);
1728        whd in match (as_pc_of ??); whd in match (point_of_succ ???);
1729        change with (pc_block pc1) in match (pc_block ?);
1730        whd in match fetch_statement; normalize nodelta
1731        >(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind
1732        whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
1733        >EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt;
1734        normalize nodelta * #H @H % ]
1735    ]
1736    whd [ whd in match (as_classify ??); | whd in match eval_state; normalize nodelta]
1737    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
1738    >point_of_pc_of_point >EQt_stmt [%] >m_return_bind whd in match eval_statement_no_pc;
1739    normalize nodelta >m_return_bind whd in match eval_statement_advance;
1740    whd in match eval_return; normalize nodelta whd in match (stack_sizes ????);
1741    >EQssize >m_return_bind >EQt_pop >m_return_bind whd in match next_of_call_pc;
1742    normalize nodelta >EQt_call >m_return_bind %
1743  | whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct]
1744    whd in match (point_of_succ ???); @(st_rel_def … good)
1745    [3: change with (pc_block pc1) in match (pc_block ?);
1746        lapply(proj1 ?? (fetch_statement_inv … EQcall)) <pc_block_eq in ⊢ (% → ?);
1747        [2: >EQpc2 % #EQ destruct] #H @H
1748    |1,2:
1749    | <pc_block_eq in fin_sem_rel; [2: >EQpc2 % #EQ destruct] #H @H
1750    | %
1751    ]
1752  ]
1753]   
1754whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i
1755#calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call
1756whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQpc1_pc_s1_pre  #EQsucc_pc
1757whd in ⊢ (% → ?); #EQpc_s1_pre >EQpc_s1_pre in EQfetch_call; #EQfetch_call
1758cases(fetch_statement_sigma_stored_pc … good … EQfetch_call)
1759[2: <EQpc_s1_pre % #ABS elim Hbl_pcpop #H @H -H >EQpc1_pc_s1_pre assumption ]
1760#data2 * #EQdata2 normalize nodelta * #bl2 * #EQbl2 * #pc3 * #EQstored
1761lapply(stored_pc_inj … (sym_eq ??? EQstored))
1762[ % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero
1763  [ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS % ]
1764#EQ destruct(EQ) * #fn' * #nxt'' * #l1 * #l2 @eq_identifier_elim
1765[ #EQentry cases(fetch_statement_inv … EQfetch_call) #_ >EQentry normalize nodelta
1766  cases(entry_is_cost … (pi2 ?? calling)) #nxt1 * #c #EQ >EQ #EQ1 destruct]
1767#_ cut(∀b : bool.andb b false = false) [ * //] #EQ >EQ -EQ normalize nodelta
1768*** #EQt_fetch_call #_ #_ #EQnxt' whd >EQt_fetch_call normalize nodelta
1769cut(? : Prop)
1770[3: whd in match (last_pop ??); #H %{H}
1771|2: @(stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs … )
1772  [ % #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero
1773   [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS % ]
1774 >EQpc1_pc_s1_pre assumption
1775|]
1776destruct(H)
1777cut(nxt'' = nxt1) [2: #EQ destruct whd in ⊢ (??%%); % ]
1778cut(nxt' = next_of_call)
1779[ lapply EQsucc_pc whd in match (succ_pc); normalize nodelta
1780  whd in match (point_of_succ ???); whd in match (point_of_succ ???);
1781  whd in ⊢ (??%% → ?); cases next_of_call #x cases nxt' #y
1782  whd in match (offset_of_point ??); whd in match (offset_of_point ??);
1783  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) % ]
1784#EQ destruct(EQ) >EQcall in EQfetch_call; >EQt_call in EQt_fetch_call;
1785whd in ⊢ (? → ??%? → ?); #EQ1 #EQ2 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) %
1786qed.
1787
1788
1789theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
1790∀prog : joint_program p_in.∀stack_size : ident → option ℕ.
1791∀init : (∀globals.joint_closed_internal_function p_in globals →
1792         bound_b_graph_translate_data p_in p_out globals).
1793∀init_regs : block → list register.∀f_lbls : lbl_funct_type.
1794∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out.
1795∀st_rel : joint_state_pc_relation p_in p_out.
1796good_state_relation p_in p_out prog stack_size init init_regs
1797 f_lbls f_regs st_no_pc_rel st_rel →
1798let trans_prog ≝ b_graph_transform_program … init prog in
1799∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
1800∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
1801∃[1] R.
1802  status_simulation_with_init
1803    (joint_abstract_status (mk_prog_params p_in prog stack_size))
1804    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
1805    R init_in init_out.
1806cases daemon
1807qed.
1808
1809
Note: See TracBrowser for help on using the repository browser.