source: src/joint/StatusSimulationUtils.ma @ 3371

Last change on this file since 3371 was 3371, checked in by piccolo, 6 years ago

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File size: 70.6 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14 
15include "joint/semanticsUtils.ma".
16include "joint/Traces.ma".
17include "common/StatusSimulation.ma".
18include "joint/semantics_blocks.ma".
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
50lemma bind_new_bind_new_instantiates :
51∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P.
52bind_new_instantiates B X x m l → bind_new_P ?? P m →
53P x.
54#B #X #m elim m normalize nodelta
55[#x #y * normalize // #B #l' #P *
56| #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H)
57 @Hr
58]
59qed.
60
61let rec bind_instantiate B X (b : bind_new B X) (l : list B) on b : (option X) ≝
62  match b with
63  [ bret B ⇒
64    match l with
65    [ nil ⇒ Some ? B
66    | _ ⇒ None ?
67    ]
68  | bnew f ⇒
69    match l with
70    [ nil ⇒ None ?
71    | cons r l' ⇒
72      bind_instantiate B X (f r) l'
73    ]
74  ].
75 
76lemma bind_instantiates_to_instantiate : ∀B,X.∀b : bind_new B X.
77∀l : list B.∀x : X.
78bind_instantiate B X b l = Some ? x →
79bind_new_instantiates B X x b l.
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: #EQ destruct(EQ)] #H
83 whd @IH assumption
84]
85qed.
86
87lemma bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
88∀l : list B.∀x : X.
89bind_new_instantiates B X x b l →
90bind_instantiate B X b l = Some ? x.
91#B #X #b elim b
92[ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) %
93| #f #IH * [2: #hd #tl] #x whd in ⊢ (% → ?); [2: *] #H whd in ⊢ (??%?); @IH @H
94]
95qed.
96
97coercion bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X.
98∀l : list B.∀x : X.
99∀prf : bind_new_instantiates B X x b l.
100bind_instantiate B X b l = Some ? x ≝
101bind_instantiate_instantiates
102on _prf : bind_new_instantiates ?????
103to eq (option ?) (bind_instantiate ????) (Some ??).
104
105definition lbl_funct_type ≝  block → label → (list label).
106definition regs_funct_type ≝ block → label → (list register).
107
108
109definition preamble_length ≝
110λP_in : sem_graph_params.λP_out : sem_graph_params.λprog : joint_program P_in.
111λstack_size : (ident → option ℕ).
112λinit : ∀globals.joint_closed_internal_function P_in globals
113         →bound_b_graph_translate_data P_in P_out globals.
114λinit_regs : block → list register.
115λf_regs : regs_funct_type.λbl : block.λlbl : label.
116! bl ← code_block_of_block bl ;
117! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
118                           (joint_globalenv P_in prog stack_size) bl);
119! stmt ← stmt_at P_in … (joint_if_code … fn) lbl;
120! data ← bind_instantiate ?? (init … fn) (init_regs bl);
121match stmt with
122[ sequential step nxt ⇒
123    ! step_block ← bind_instantiate ?? (f_step … data lbl step) (f_regs bl lbl);
124    return |\fst (\fst step_block)|
125| final fin ⇒
126    ! fin_block ← bind_instantiate ?? (f_fin … data lbl fin) (f_regs bl lbl);
127    return |\fst fin_block|
128| FCOND abs _ _ _ ⇒ Ⓧabs
129].
130
131
132definition sigma_label : ∀p_in,p_out : sem_graph_params.
133joint_program p_in → (ident → option ℕ) →
134(∀globals.joint_closed_internal_function p_in globals
135         →bound_b_graph_translate_data p_in p_out globals) →
136(block → list register) → lbl_funct_type → regs_funct_type →
137block → label → option label ≝
138λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
139! bl ← code_block_of_block bl ;
140! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
141                           (joint_globalenv p_in prog stack_size) bl);
142! 〈res,s〉 ←
143 find ?? (joint_if_code ?? fn)
144  (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
145             [ None ⇒ false
146             | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
147                         [ None ⇒ false
148                         | Some x ⇒ eq_identifier … searched x
149                         ]
150             ]);
151return res.
152
153                                         
154                         
155
156lemma partial_inj_sigma_label :
157∀p_in,p_out,prog,stack_size,init,init_regs.
158∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2.
159sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→
160sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 =
161sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 →
162lbl1 = lbl2.
163#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2
164inversion(sigma_label ????????? lbl1)
165[ #_ * #H @⊥ @H %]
166#lbl1' #H @('bind_inversion H) -H #bl' #EQbl'
167#H @('bind_inversion H) -H * #f #fn #H lapply(res_eq_from_opt ??? H) -H
168#EQfn #H @('bind_inversion H) -H * #res #stmt #H1 whd in ⊢ (??%? → ?);
169#EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H
170#bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) -H
171* #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ)
172lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2)
173cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???)
174normalize nodelta
175[*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim
176[2: #_ *] #EQ destruct(EQ) #_ %
177qed.
178
179definition sigma_pc_opt : 
180∀p_in,p_out : sem_graph_params.
181joint_program p_in → (ident → option ℕ) →
182(∀globals.joint_closed_internal_function p_in globals
183         →bound_b_graph_translate_data p_in p_out globals) →
184(block → list register) → lbl_funct_type → regs_funct_type →
185program_counter → option program_counter ≝
186λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
187let target_point ≝ point_of_pc p_out pc in
188if (orb (eqZb   (block_id (pc_block pc)) (-1)) (eqZb (block_id (pc_block pc)) OZ)) then
189 return pc
190else
191 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs
192                   f_lbls f_regs (pc_block pc) target_point;
193 return pc_of_point p_in (pc_block pc) source_point.
194
195
196lemma sigma_stored_pc_inj :
197∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
198sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
199sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
200sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
201pc = pc'.
202#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs
203* #bl1 #p1 * #bl2 #p2
204inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1
205whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta
206@if_elim normalize nodelta #Hbl
207[2: #H @('bind_inversion H) -H * #pt1 #EQpt1]
208whd in ⊢ (??%? → ?); #EQ destruct(EQ)
209#_ #H lapply(sym_eq ??? H) -H whd in match sigma_pc_opt;
210normalize nodelta @if_elim #Hbl1 normalize nodelta
211[2,4: #H @('bind_inversion H) -H * #pt2 #EQpt2] whd in match pc_of_point;
212normalize nodelta whd in match (offset_of_point ??);
213whd in ⊢ (??%% → ?); #EQ destruct(EQ)
214[2,3: @⊥ lapply Hbl lapply Hbl1 @eqZb_elim normalize nodelta  #_ [1,3: **]
215  @eqZb_elim #_ **  |4: %]
216whd in match (offset_of_point ??) in EQpt2;
217<EQpt1 in EQpt2; #H lapply(partial_inj_sigma_label … (sym_eq ??? H))
218[ >EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta
219whd in match (point_of_offset ??); whd in match (point_of_offset ??);
220#EQ -prog destruct(EQ) %
221qed.
222
223
224definition sigma_stored_pc ≝
225λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc.
226  match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with
227      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
228
229definition joint_state_relation ≝
230λP_in,P_out.program_counter → state P_in → state P_out → Prop.
231
232definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
233
234definition seq_commutation_statement ≝
235  λP_in,P_out : sem_graph_params.
236  λprog : joint_program P_in.λstack_sizes : ident → option ℕ.
237  λinit : (∀globals.joint_closed_internal_function P_in globals
238         →bound_b_graph_translate_data P_in P_out globals).
239  λinit_regs : block → list register. λf_lbls : lbl_funct_type.
240  λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out.
241  λst_rel : joint_state_pc_relation P_in P_out.
242  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
243  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
244  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
245  ∀f,fn,stmt,nxt.
246  block_id … (pc_block (pc … st1)) ≠ -1 →
247  let seq ≝ (step_seq P_in ? stmt) in
248  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
249  return 〈f, fn,  sequential … seq nxt〉 → 
250  eval_state P_in … (joint_globalenv P_in prog stack_sizes)
251  st1 = return st1' →
252  st_rel st1 st2 →
253  ∀t_fn.
254  fetch_internal_function …
255     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
256  return 〈f,t_fn〉 →
257  bind_new_P' ??
258     (λregs1.λdata.
259     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
260      (λregs2.λblp.
261       ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))).
262                            blp = (ensure_step_block ?? l) ∧
263       ∃st2_fin_no_pc.
264           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
265              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
266           st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc
267      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
268     ) (init ? fn)
269.
270
271definition cond_commutation_statement ≝
272λP_in,P_out : sem_graph_params.
273  λprog : joint_program P_in.λstack_sizes : ident → option ℕ.
274  λinit : (∀globals.joint_closed_internal_function P_in globals
275         →bound_b_graph_translate_data P_in P_out globals).
276  λinit_regs : block → list register. λf_lbls : lbl_funct_type.
277  λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out.
278  λst_rel : joint_state_pc_relation P_in P_out.
279 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
280    ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
281    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
282    ∀f,fn,a,ltrue,lfalse,bv,b.
283    block_id … (pc_block (pc … st1)) ≠ -1 →
284    let cond ≝ (COND P_in ? a ltrue) in
285    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
286    return 〈f, fn,  sequential … cond lfalse〉 → 
287    acca_retrieve … P_in (st_no_pc … st1) a = return bv →
288    bool_of_beval … bv = return b →
289    st_rel st1 st2 →
290    ∀t_fn.
291    fetch_internal_function …
292     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
293     return 〈f,t_fn〉 →
294    bind_new_P' ??
295     (λregs1.λdata.
296      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
297     (λregs2.λblp.(\snd blp) = [ ] ∧
298        ∀mid.
299          stmt_at P_out … (joint_if_code ?? t_fn) mid
300          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→
301         ∃st2_pre_mid_no_pc.
302            repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
303             (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)
304            = return st2_pre_mid_no_pc ∧
305            let new_pc ≝ if b then
306                           (pc_of_point P_in (pc_block (pc … st1)) ltrue)
307                         else
308                           (pc_of_point P_in (pc_block (pc … st1)) lfalse) in
309            st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧
310            ∃a'. ((\snd (\fst blp)) mid)  = COND P_out ? a' ltrue ∧
311            ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧
312                  bool_of_beval … bv' = return b
313   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
314  ) (init ? fn).
315 
316definition return_commutation_statement ≝
317λP_in,P_out : sem_graph_params.
318  λprog : joint_program P_in.λstack_sizes : ident → option ℕ.
319  λinit : (∀globals.joint_closed_internal_function P_in globals
320         →bound_b_graph_translate_data P_in P_out globals).
321  λinit_regs : block → list register. λf_lbls : lbl_funct_type.
322  λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out.
323  λst_rel : joint_state_pc_relation P_in P_out.
324  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
325  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
326  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
327  ∀f,fn.
328  block_id … (pc_block (pc … st1)) ≠ -1 →
329  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
330  return 〈f, fn,  final P_in ? (RETURN …)〉 → 
331  ∀n. stack_sizes f = return n →
332  let curr_ret ≝ joint_if_result … fn in
333  ∀st_pop,pc_pop.
334  pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret
335   (st_no_pc … st1) = return 〈st_pop,pc_pop〉 →
336  ∀nxt.∀f1,fn1,id,args,dest.
337    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop  =
338    return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 →
339  st_rel st1 st2 →
340  ∀t_fn.
341  fetch_internal_function …
342     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
343  return 〈f,t_fn〉 →
344  bind_new_P' ??
345     (λregs1.λdata.
346      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
347      (λregs2.λblp.
348       \snd blp = (RETURN …) ∧
349       ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
350              (\fst blp)  (st_no_pc … st2)= return st_fin ∧
351        ∃t_st_pop,t_pc_pop.
352        pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f
353         (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧
354        sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs
355         t_pc_pop = pc_pop ∧
356        if eqZb (block_id (pc_block pc_pop)) (-1) then
357            st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
358             (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) ∧
359            next_of_call_pc P_out … (joint_globalenv P_out trans_prog stack_sizes)
360             t_pc_pop = return nxt
361        else
362            bind_new_P' ??
363            (λregs4.λdata1.
364               bind_new_P' ??
365               (λregs3.λblp1.
366                 ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
367                      (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧
368                      st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)
369                       (decrement_stack_usage ? n st_pop) st2'
370               ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest))
371            ) (init ? fn1)
372          ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …))
373     ) (init ? fn).
374
375definition pre_main_commutation_statement ≝
376λP_in,P_out : sem_graph_params.
377  λprog : joint_program P_in.λstack_sizes : ident → option ℕ.
378  λinit : (∀globals.joint_closed_internal_function P_in globals
379         →bound_b_graph_translate_data P_in P_out globals).
380  λinit_regs : block → list register. λf_lbls : lbl_funct_type.
381  λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out.
382  λst_rel : joint_state_pc_relation P_in P_out.
383let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
384    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
385    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
386    block_id … (pc_block (pc … st1)) = -1 →
387    eval_state P_in … (joint_globalenv P_in prog stack_sizes)
388     st1 = return st1' →
389    st_rel st1 st2 →
390    joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =
391     joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧
392    ∃st2'. st_rel st1' st2' ∧
393    eval_state P_out …
394     (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2' ∧
395    as_label (joint_status P_in prog stack_sizes) st1' =
396     as_label (joint_status P_out trans_prog stack_sizes) st2'.
397
398definition call_commutation_statement ≝
399λP_in,P_out : sem_graph_params.
400  λprog : joint_program P_in.λstack_sizes : ident → option ℕ.
401  λinit : (∀globals.joint_closed_internal_function P_in globals
402         →bound_b_graph_translate_data P_in P_out globals).
403  λinit_regs : block → list register. λf_lbls : lbl_funct_type.
404  λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out.
405  λst_rel : joint_state_pc_relation P_in P_out.
406let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
407  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
408  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
409  ∀f,fn,id,arg,dest,nxt.
410  block_id … (pc_block (pc … st1)) ≠ -1 →
411  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
412  return 〈f, fn,  sequential P_in ? (CALL P_in ? id arg dest) nxt〉 →
413  ∀bl.
414   block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1)
415      = return bl →
416  ∀f1,fn1.
417   fetch_internal_function …
418    (joint_globalenv P_in prog stack_sizes) bl =  return 〈f1,fn1〉 →
419  ∀st1_pre.
420  save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre →
421  ∀n.stack_sizes f1 = return n → 
422  ∀st1'.
423  setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
424  st_rel st1 st2 → 
425  ∀t_fn1.
426  fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl =
427  return 〈f1,t_fn1〉 →
428  bind_new_P' ??
429    (λregs1.λdata.
430     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
431      (λregs2.λblp.
432        ∀pc',t_fn,id',arg',dest',nxt1.
433          sigma_stored_pc P_in P_out prog stack_sizes init init_regs
434           f_lbls f_regs pc' = (pc … st1) →
435          fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc'
436          = return 〈f,t_fn,
437                    sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1〉→
438          ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') → 
439       ∃st2_pre_call.
440        repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
441          (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧
442       block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id'
443        st2_pre_call = return bl ∧
444       ∃st2_pre.
445        save_frame … P_out (kind_of_call P_out id') dest'
446         (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
447       ∃st2_after_call.
448         setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
449          = return st2_after_call ∧
450       bind_new_P' ??
451         (λregs11.λdata1.
452          init_regs bl = new_regs … data1 → ∃st2'.
453           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
454           (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =
455           return st2' ∧
456           st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1))
457            (increment_stack_usage P_in n st1') st2'               
458         ) (init ? fn1)
459     )
460     (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest))
461    ) (init ? fn).
462   
463definition goto_commutation_statement ≝
464λP_in,P_out : sem_graph_params.
465  λprog : joint_program P_in.λstack_sizes : ident → option ℕ.
466  λinit : (∀globals.joint_closed_internal_function P_in globals
467         →bound_b_graph_translate_data P_in P_out globals).
468  λinit_regs : block → list register. λf_lbls : lbl_funct_type.
469  λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out.
470  λst_rel : joint_state_pc_relation P_in P_out.
471let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
472  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
473  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
474  ∀f,fn,lbl.
475  block_id … (pc_block (pc … st1)) ≠ -1 →
476  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
477  return 〈f, fn,  final P_in ? (GOTO ? lbl)〉 →
478  st_rel st1 st2 →
479  ∀t_fn.
480  fetch_internal_function …
481     (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =
482  return 〈f,t_fn〉 →
483  bind_new_P' ??
484     (λregs1.λdata.
485      init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
486      (λregs2.λblp.
487        ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
488              (\fst blp)  (st_no_pc … st2)= return st_fin ∧
489        \snd blp = GOTO ? lbl ∧
490        st_no_pc_rel (pc_of_point P_in (pc_block (pc … st1)) lbl)
491           (st_no_pc … st1) (st_fin)
492      ) (f_fin … data (point_of_pc P_in (pc … st1)) (GOTO ? lbl))
493     ) (init ? fn).
494     
495definition tailcall_commutation_statement ≝
496λP_in,P_out : sem_graph_params.
497  λprog : joint_program P_in.λstack_sizes : ident → option ℕ.
498  λinit : (∀globals.joint_closed_internal_function P_in globals
499         →bound_b_graph_translate_data P_in P_out globals).
500  λinit_regs : block → list register. λf_lbls : lbl_funct_type.
501  λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out.
502  λst_rel : joint_state_pc_relation P_in P_out.
503  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
504  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
505  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
506  ∀f,fn,has_tail,id,arg.
507  block_id … (pc_block (pc … st1)) ≠ -1 →
508  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
509  return 〈f, fn,  final P_in ? (TAILCALL P_in has_tail id arg)〉 →
510  ∀bl.
511   block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1)
512      = return bl →
513   ∀f1,fn1.
514   fetch_internal_function …
515    (joint_globalenv P_in prog stack_sizes) bl =  return 〈f1,fn1〉 →
516   ∀ssize_f.stack_sizes f = return ssize_f →
517   ∀ssize_f1.stack_sizes f1 = return ssize_f1 →   
518   ∀st1'.
519    setup_call ?? P_in ssize_f1 (joint_if_params … fn1) arg
520     (decrement_stack_usage P_in ssize_f (st_no_pc … st1)) = return st1' →
521   st_rel st1 st2 → 
522   ∀t_fn1.
523   fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl =
524   return 〈f1,t_fn1〉 →
525   bind_new_P' ??
526    (λregs1.λdata.
527     init_regs (pc_block (pc … st1)) = new_regs … data → bind_new_P' ??
528      (λregs2.λblp.
529       ∃ has_tail',id',arg'.
530       (\snd blp) = TAILCALL P_out has_tail' id' arg' ∧
531       ∃st2_pre_call.
532        repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f
533         (\fst blp) (st_no_pc ? st2) = return st2_pre_call ∧
534        block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id'
535         st2_pre_call = return bl ∧
536       ∃st2_after.
537        setup_call ?? P_out ssize_f1 (joint_if_params … t_fn1) arg'
538         (decrement_stack_usage P_out ssize_f st2_pre_call) = return st2_after ∧
539       bind_new_P' ??
540         (λregs11.λdata1.
541          init_regs bl = new_regs … data1 → ∃st2'.
542           repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1
543           (added_prologue … data1) (increment_stack_usage P_out ssize_f1 st2_after) =
544           return st2' ∧
545           st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1))
546            (increment_stack_usage P_in ssize_f1 st1') st2'               
547         ) (init ? fn1)
548     ) (f_fin … data (point_of_pc P_in (pc … st1)) (TAILCALL P_in has_tail id arg))
549   ) (init ? fn).
550
551record good_state_relation (P_in : sem_graph_params)
552   (P_out : sem_graph_params) (prog : joint_program P_in)
553   (stack_sizes : ident → option ℕ)
554   (init : ∀globals.joint_closed_internal_function P_in globals
555         →bound_b_graph_translate_data P_in P_out globals)
556   (init_regs : block → list register) (f_lbls : lbl_funct_type)
557   (f_regs : regs_funct_type)
558   (st_no_pc_rel : joint_state_relation P_in P_out)
559   (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝
560{ good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init
561                     prog init_regs f_lbls f_regs
562; fetch_ok_sigma_state_ok :
563   ∀st1,st2,f,fn. st_rel st1 st2 →
564    fetch_internal_function …
565     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
566     = return 〈f,fn〉 →
567     st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)
568; fetch_ok_pc_ok :
569  ∀st1,st2,f,fn.st_rel st1 st2 →
570   fetch_internal_function …
571     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
572     = return 〈f,fn〉 →
573   pc … st1 = pc … st2
574; fetch_ok_sigma_last_pop_ok :
575  ∀st1,st2,f,fn.st_rel st1 st2 →
576   fetch_internal_function …
577     (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 
578     = return 〈f,fn〉 →
579   (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
580                       f_lbls f_regs (last_pop … st2)
581; st_rel_def :
582  ∀st1,st2,pc,lp1,lp2,f,fn.
583  fetch_internal_function …
584     (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 →
585   st_no_pc_rel pc st1 st2 →
586   lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs
587          f_lbls f_regs lp2 →
588  st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
589; pre_main_ok : pre_main_commutation_statement P_in P_out prog stack_sizes init
590                    init_regs f_lbls f_regs st_no_pc_rel st_rel
591; pre_main_no_return :
592    ∀f,fn,pc. block_id (pc_block pc) = -1 →
593    fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc =
594      return 〈f,fn,final P_in ? (RETURN …)〉 → False
595; cond_commutation : cond_commutation_statement P_in P_out prog stack_sizes init
596                    init_regs f_lbls f_regs st_no_pc_rel st_rel
597; seq_commutation : seq_commutation_statement P_in P_out prog stack_sizes init
598                    init_regs f_lbls f_regs st_no_pc_rel st_rel
599;  call_is_call :∀f,fn,bl.
600  fetch_internal_function …
601     (joint_globalenv P_in prog stack_sizes) bl = return 〈f,fn〉 →
602   ∀id,args,dest,lbl.
603    bind_new_P' ??
604     (λregs1.λdata.bind_new_P' ??
605      (λregs2.λblp.
606        ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
607      (f_step … data lbl (CALL P_in ? id args dest)))
608     (init ? fn)
609; cost_commutation :
610  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
611  ∀st1,st2,pc.∀f,fn,c,nxt.
612  block_id … (pc_block pc) ≠ -1 →
613  st_no_pc_rel pc st1 st2 →
614  fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc =
615  return 〈f, fn,  sequential ?? (COST_LABEL ?? c) nxt〉 → 
616  st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2
617; return_commutation : return_commutation_statement P_in P_out prog stack_sizes init
618                    init_regs f_lbls f_regs st_no_pc_rel st_rel
619; call_commutation : call_commutation_statement P_in P_out prog stack_sizes init
620                    init_regs f_lbls f_regs st_no_pc_rel st_rel
621; goto_commutation : goto_commutation_statement P_in P_out prog stack_sizes init
622                    init_regs f_lbls f_regs st_no_pc_rel st_rel
623; tailcall_commutation : tailcall_commutation_statement P_in P_out prog stack_sizes
624                   init init_regs f_lbls f_regs st_no_pc_rel st_rel
625; as_result_ok :
626  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in   
627  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
628  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
629  st_rel st1 st2 →
630  as_result … st1 = as_result … st2
631; as_label_premain_ok :
632  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in   
633  ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
634  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
635  block_id … (pc_block (pc … st1)) = -1 →
636  st_rel st1 st2 → as_label … st1 = as_label … st2
637}.
638
639record good_init_relation (P_in : sem_graph_params) (P_out : sem_graph_params)
640(prog : joint_program P_in) (stack_sizes : ident → option ℕ)
641(init : ∀globals.joint_closed_internal_function P_in globals
642         →bound_b_graph_translate_data P_in P_out globals)
643(st_no_pc_rel : joint_state_relation P_in P_out) : Prop ≝
644{ good_empty :
645   ∀m0.init_mem … (λx.x) prog = return m0 →
646   let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
647   let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
648   let globals_size ≝ globals_stacksize … prog in
649   let globals_size' ≝ globals_stacksize … trans_prog in
650   let spp ≝ mk_pointer spb (mk_offset (bitvector_of_Z 16 (-S (globals_size)))) in
651   let spp' ≝ mk_pointer spb (mk_offset (bitvector_of_Z 16 (-S (globals_size')))) in
652   ∀prf,prf'.
653   let st ≝ mk_state P_in (Some ? (empty_framesT …)) empty_is
654                (BBbit false) (empty_regsT … «spp,prf») m 0 in
655   let st' ≝ mk_state P_out (Some ? (empty_framesT …)) empty_is
656                (BBbit false) (empty_regsT … «spp',prf'») m 0 in
657   st_no_pc_rel init_pc (set_sp … «spp,prf» st) (set_sp … «spp',prf'» st')
658; good_init_cost_label :
659  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
660  match fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) init_pc with
661  [ OK x ⇒ match cost_label_of_stmt … (\snd x) with
662           [ Some c ⇒ ∃y.
663                     fetch_statement P_out …
664                      (joint_globalenv P_out trans_prog stack_sizes) init_pc =
665                     OK ? y ∧
666                     cost_label_of_stmt … (\snd y) = Some ? c
667           | None ⇒ (∃e'.
668                     fetch_statement P_out …
669                      (joint_globalenv P_out trans_prog stack_sizes) init_pc =
670                     Error ? e') ∨
671                    (∃x.
672                     fetch_statement P_out …
673                      (joint_globalenv P_out trans_prog stack_sizes) init_pc =
674                       OK ? x ∧ cost_label_of_stmt … (\snd x) = None ?)
675           ]
676  | Error e ⇒
677    (∃e'.
678     fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) init_pc =
679      Error ? e') ∨
680    (∃x.
681      fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) init_pc =
682      OK ? x ∧ cost_label_of_stmt … (\snd x) = None ?)
683  ]
684}.
685
686
687lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
688code_block_of_block bl = return bl.
689* #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
690[ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
691qed.
692
693(*TO BE MOVED*)
694lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2).
695#A #l1 elim l1 [#l2 #P *] #hd #tl #IH *
696[#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption | #H %2 @IH assumption]
697qed.
698
699lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2).
700#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
701[#a normalize // ] #hd1 #tl1 #a normalize *
702[ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 //
703| #H %2 >append_cons @IH assumption]
704qed.
705
706lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident.
707∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst.
708seq_list_in_code p globals code src l1 l2 dst → |l1| = |l2|.
709#p #globals #code #src #l1 lapply src -src elim l1
710[ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct]
711#hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct]
712#hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt
713#EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H)
714qed.
715
716lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params.
717∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl.
718In ? (stmt_labels p ? stmt) lbl→
719fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 →
720pc' = pc_of_point p (pc_block pc) lbl →
721∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉.
722#p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch
723cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
724#EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) *
725cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?)
726[3: * cases lbl #x #y cases(decidable_eq_pos … x y)
727    [#EQ destruct % % | * #H %2 % #H1 @H destruct %]
728| whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct
729  whd in match code_has_label; whd in match code_has_point; normalize nodelta
730  inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'}
731  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
732  >point_of_pc_of_point >EQstmt' %
733| #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl)
734  [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label;
735    normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_
736    whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta
737    inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'}
738    whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
739    >point_of_pc_of_point >EQstmt' %
740  | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H %
741  ]
742]
743qed.
744
745
746lemma fetch_stmt_ok_nxt_ok : ∀p : sem_graph_params.
747∀prog : joint_program p.∀stack_size,f,fn,stmt,bl,pt,nxt.
748fetch_internal_function … (joint_globalenv p prog stack_size) bl =
749return 〈f,fn〉→
750stmt_at p … (joint_if_code … fn) pt = return sequential p ? stmt nxt →
751∃stmt'.
752stmt_at p … (joint_if_code … fn) nxt = return stmt'.
753#p #prog #stack_size #f #fn #stmt #bl #pt #nxt #EQfn #EQstmt
754cases(fetch_stmt_ok_succ_ok …
755       prog stack_size f fn (sequential p … stmt nxt) (pc_of_point p bl pt)
756       (pc_of_point p bl nxt) nxt ???)
757[ #stmt' #H cases(fetch_statement_inv … H) -H #_ >point_of_pc_of_point normalize nodelta
758  #EQstmt' %{stmt'} assumption
759| whd in match stmt_labels; normalize nodelta % %
760| whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind
761  >point_of_pc_of_point >EQstmt %
762| %
763]
764qed.
765
766
767lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs.
768∀f_lbls : lbl_funct_type.∀f_regs.
769b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs →
770∀id,fn.
771∀bl:Σb.block_region b = Code. ∀pt,stmt.
772block_id … bl ≠ -1 →
773fetch_internal_function …
774   (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 →
775stmt_at p_in … (joint_if_code … fn) pt = return stmt → 
776∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧
777match n with
778[ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt
779| S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧
780    sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt     
781].
782#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn
783#bl #pt #stmt * #Hbl #EQfn #EQstmt   
784lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn)
785@eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
786#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H
787lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt
788[ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta **
789[ * #pre_instr #instr #post_instr | #pre_instr #instr] *
790[ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta
791 [ @eq_identifier_elim #EQentry normalize nodelta
792   [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
793     whd in ⊢ (???% → ?); #EQ destruct(EQ)
794   |*: #Hregs
795   ]
796 | #Hregs
797 ]
798| #Hregs
799]
800#syntax_spec
801[4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_
802[1,2,4,5: %{(|pre_instr|)} | %{O}]
803cut(? : Prop)
804[3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta
805 [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec
806           whd in match (length ??); #EQn whd in match (length ??); normalize nodelta]
807 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq
808     >m_return_bind >EQfn >m_return_bind inversion(find ????)
809     [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
810     @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind
811     >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length;
812     normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
813     whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
814     >m_return_bind cases stmt1 in EQfind; -stmt1
815     [1,4,7,10,13: #j_step1 #nxt1 |2,5,8,11,14: #fin1 |*: *] #EQfind normalize nodelta
816     cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *]
817     [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1 ]
818     >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl]
819     whd in match (length ??); normalize nodelta
820     [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
821     #EQ #_ >EQ %]
822     whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *]
823     #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *]
824     #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥
825     cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ)
826     ** #H #_ @H  @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
827     whd in match code_has_point; normalize nodelta >EQstmt @I
828 |*: cases syntax_spec -syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *]
829     cases pre -pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?);
830     #EQ destruct(EQ) -EQ #pre_spec whd in ⊢ (% → ?);
831     [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec
832     |*:   #EQt_stmt
833     ]
834     %{mid1} cut(? : Prop)
835     [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta
836       >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????)
837       [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta
838         whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim
839         [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f
840       lapply(find_predicate ?????? EQfind) whd in match preamble_length;
841       normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
842       whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit
843       >m_return_bind cases stmt1 in EQfind; -stmt1
844       [1,4,7,10: #j_step1 #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind normalize nodelta
845       cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *]
846       [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1]
847       >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1]
848       whd in match (length ??); normalize nodelta whd in match (nth_opt ???);
849       [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2
850         #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *]
851         #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_  @(proj2 … pp_labs ?? lbl2)
852         @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)]
853         >e0 @Exists_append2 % %
854       |*: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥
855         lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * -H ** #H #_ #_ @H
856         @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
857         whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
858         >(find_lookup ?????? EQfind) @I
859       ]   
860     |2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ)
861                whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?);
862                #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H)
863                [1,2: >length_map] -H #H >H >nth_opt_append_r cases(|rest|)
864                try % try( #n %) #n <minus_n_n %
865     |*:
866     ]
867  ]
868 |2,5,8,11,14: whd in match preamble_length; normalize nodelta >code_block_of_block_eq
869   >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
870   normalize nodelta
871   [1,2,3,4: >Hregs %
872   | >EQregs <EQentry in EQstmt; cases(entry_is_cost … (pi2 ?? fn)) #succ * #c
873     #EQstmt >EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data)
874     whd in match (bind_instantiate ????); %
875   ]
876 |*:
877 ]
878qed.
879
880lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls,
881f_regs,pc.
882sigma_pc_opt p_in p_out prog stack_sizes init
883   init_regs f_lbls f_regs pc ≠ None ? →
884 pc_block … pc =
885 pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init
886                                           init_regs f_lbls f_regs pc).
887#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc
888whd in match sigma_stored_pc; normalize nodelta
889inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1
890whd in match sigma_pc_opt; normalize nodelta @if_elim
891[ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ %] #_
892#H @('bind_inversion H) -H #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ %
893qed.
894
895definition stmt_get_next : ∀p,globals.joint_statement p globals → option (succ p) ≝
896λp,globals,stmt.
897match stmt with
898[sequential stmt nxt ⇒ Some ? nxt
899| _ ⇒ None ?
900].
901
902
903definition sigma_next : ∀p_in,p_out : sem_graph_params.
904joint_program p_in → (ident → option ℕ) →
905(∀globals.joint_closed_internal_function p_in globals
906         →bound_b_graph_translate_data p_in p_out globals) →
907(block → list register) → lbl_funct_type → regs_funct_type →
908block → label → option label ≝
909λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched.
910! bl ← code_block_of_block bl ;
911! 〈id,fn〉 ← res_to_opt … (fetch_internal_function …
912                           (joint_globalenv p_in prog stack_size) bl);
913! 〈res,s〉 ←
914 find ?? (joint_if_code ?? fn)
915  (λlbl.λstmt.match stmt_get_next … stmt with
916    [ None ⇒ false
917    | Some nxt ⇒
918       match preamble_length … prog stack_size init init_regs f_regs bl lbl with
919        [ None ⇒ false
920        | Some n ⇒ match nth_opt ? n ((f_lbls bl lbl) @ [nxt]) with
921                         [ None ⇒ false
922                         | Some x ⇒ eq_identifier … searched x
923                         ]
924        ]
925    ]);
926stmt_get_next … s.
927
928lemma fetch_internal_function_no_zero :
929∀p,prog,stack_size,bl.
930  block_id (pi1 … bl) = 0 →
931  fetch_internal_function … (joint_globalenv p prog stack_size) bl =
932  Error ? [MSG BadFunction].
933#p #prg #stack_size #bl #Hbl whd in match fetch_internal_function;
934whd in match fetch_function; normalize nodelta @eqZb_elim
935[ >Hbl #EQ @⊥ cases(not_eq_OZ_neg one) #H @H assumption ]
936#_ normalize nodelta cases(symbol_for_block ???) [%] #id >m_return_bind
937cases bl in Hbl; * #id #prf #EQ destruct(EQ)
938change with (mk_block OZ) in match (mk_block ?);
939cut(find_funct_ptr
940    (fundef (joint_closed_internal_function p (prog_names p prg)))
941    (joint_globalenv p prg stack_size) (mk_block OZ) = None ?) [%]
942#EQ >EQ %
943qed.
944
945lemma fetch_statement_sigma_stored_pc :
946∀p_in,p_out,prog,stack_sizes,
947init,init_regs,f_lbls,f_regs,pc,f,fn,stmt.
948b_graph_transform_program_props p_in p_out stack_sizes
949  init prog init_regs f_lbls f_regs →
950block_id … (pc_block pc) ≠ -1 →
951let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
952fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc =
953return 〈f,fn,stmt〉 →
954∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧
955match stmt with
956[ sequential step nxt ⇒
957    ∃step_block : step_block p_out (prog_names … trans_prog).
958    bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step)
959                 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧
960    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
961                                           init_regs f_lbls f_regs pc' = pc ∧
962    ∃fn',nxt',l1,l2.
963    fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' =
964    if not_emptyb … (added_prologue … data) ∧
965       eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn)
966    then OK ? 〈f,fn',sequential ?? (NOOP …) nxt'〉
967    else OK ? 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉 ∧
968    seq_list_in_code p_out (prog_names … trans_prog) (joint_if_code … fn') (point_of_pc p_out pc)
969     (map_eval … (\fst (\fst step_block)) (point_of_pc p_out pc'))
970     l1 (point_of_pc p_out pc')
971    ∧ seq_list_in_code p_out ? (joint_if_code … fn') nxt' (\snd step_block) l2 nxt
972    ∧ sigma_next p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc_block pc) nxt' = return nxt
973| final fin ⇒
974    ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin)
975                  (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧
976    ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init
977                                           init_regs f_lbls f_regs pc' = pc ∧
978    ∃fn'.fetch_statement p_out …
979       (joint_globalenv p_out trans_prog stack_sizes) pc'
980       = return 〈f,fn',final ?? (\snd fin_block)〉           
981| FCOND abs _ _ _ ⇒ Ⓧabs
982].
983#p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt
984#good #Hbl #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta
985#EQstmt
986lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn)
987@eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H
988#data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H
989lapply(H … EQstmt) -H normalize nodelta #H #_ %{data} >Hinit %{(refl …)}
990-EQfetch cases stmt in EQstmt H;
991[ #step #nxt | #fin | *] normalize nodelta #EQstmt -stmt
992[ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta
993  [ @eq_identifier_elim #EQentry normalize nodelta ] ]
994* #block *
995[ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta
996  #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1
997  whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1
998  * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
999  * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
1000|*: #Hregs #syntax_spec
1001]
1002[ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt;
1003  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ)
1004  % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] |] %{pc}
1005  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
1006  @eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ @eqZb_elim
1007  [ #EQ >fetch_internal_function_no_zero in EQt_fn; [2: assumption] whd in ⊢ (???% → ?);
1008    #ABS destruct(ABS) ] normalize nodelta #_
1009|*: %{block} >Hregs %{(refl …)}
1010]
1011cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble
1012normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab
1013[   whd in match (point_of_pc ??) in e0; <EQentry in e0; #e0 >e0 in EQnth_opt;
1014    whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1015|5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind
1016    normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} %{[ ]} %{[ ]}
1017    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
1018    >EQt_stmt >m_return_bind %
1019    [ % [ % [ @eq_identifier_elim [#_ %] * #H @⊥ @H % | %{(refl …) (refl …)}] | %{(refl …) (refl …)}]]
1020    whd in match sigma_next; normalize nodelta >code_block_of_block_eq
1021    >m_return_bind >EQfn >m_return_bind inversion(find ????)
1022    [ #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta
1023    >EQpreamble normalize  nodelta >EQentry >e0 normalize nodelta
1024    @eq_identifier_elim [#_ *] * #H #_ @H %]
1025    * #lbl1 #stmt1 #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
1026    inversion(stmt_get_next … stmt1) [#_ *] #nxt1 #EQnxt1 normalize nodelta
1027    inversion(preamble_length ?????????) [#_ *] #m whd in match preamble_length;
1028    normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
1029    whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind
1030    >Hinit >m_return_bind cases stmt1 in EQfind; [#j_step #succ | #fin | *]
1031    #EQfind normalize nodelta cases(bind_instantiate ???)
1032    [1,3: whd in ⊢ (??%% → ?); #EQ destruct] #bl1 >m_return_bind whd in ⊢ (??%? → ?);
1033    #EQ destruct(EQ) inversion(nth_opt ???) [1,3: #_ *] #lbl2 #EQlbl2 normalize nodelta
1034    @eq_identifier_elim [2,4: #_ *] #EQ lapply EQlbl2 destruct(EQ) #EQlbl2
1035    cases(Exists_append … (nth_opt_Exists ???? EQlbl2)) [2,4: * [2,4: *] #EQ >EQ #_ %]
1036    #H @⊥ cases(Exists_All … H (fresh_labs lbl1)) #x * #EQ destruct(EQ) ** -H #H #_
1037    @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
1038    whd in match code_has_point; normalize nodelta
1039    cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt2 #EQ >EQ @I
1040|2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)}
1041|6,7,8: %{pc}
1042]
1043whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
1044@eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta
1045@eqZb_elim
1046[1,3,5,7,9,11: #EQ >fetch_internal_function_no_zero in EQt_fn; [2,4,6,8,10,12: assumption]
1047  whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_ normalize nodelta
1048[1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc)
1049%{(refl …)} %{t_fn} cases block in Hregs syntax_spec; -block
1050[1,2,4,5: * #pre #instr #post |*: #pre #instr ] #Hregs *
1051[1,2,3,4: #l1 * #mid1 * #mid2 * #l2 ***
1052|*: #l1 * #mid **
1053]
1054#EQmid #EQpre whd in ⊢ (% → ?);
1055[1,2,3,4: * #nxt1 *] #EQt_stmt
1056[1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2} %{l1} %{l2} %]
1057[1,3,5,7,9,10: whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
1058 @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?);
1059 #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind
1060 normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; -pre
1061 [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
1062    #EQ destruct(EQ)]
1063 [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid;
1064 [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct]
1065    * #mid * #rest ** #EQ destruct(EQ)]
1066 [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1067 [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: % [ %{(refl …)} %{(refl …) (refl …)} ] assumption]
1068   @eq_identifier_elim [2: #_ % [ %{(refl …)} %{(refl …) (refl …)} | assumption] ]
1069   #EQ <EQ in EQentry; * #H @⊥ @H %]
1070 * #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??);
1071 whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt;
1072 lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1
1073 >nth_opt_append_r [2,4,6: %] cut(|rest|-|rest|=O) [1,3,5: cases(|rest|) //]
1074 #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 -EQ2 -EQ1
1075 [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt
1076    [2: >point_of_pc_of_point % [%{(refl …)} whd %{mid'} %{rest} % [2: assumption] % [2: assumption] %]
1077       assumption]
1078    @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_ >point_of_pc_of_point %
1079    [ %{(refl …)} whd %{mid'} %{rest} % [ %{(refl …)} assumption ] assumption | assumption ] ]
1080 destruct(EQ3) >point_of_pc_of_point >EQt_stmt %]
1081whd in match sigma_next; normalize nodelta >code_block_of_block_eq >m_return_bind
1082>EQfn >m_return_bind inversion(find ????)
1083[1,3,5,7: #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta >EQpreamble
1084  normalize nodelta cases post in Hregs EQpost;
1085  [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) @('bind_inversion EQpreamble)
1086    #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn
1087    >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta
1088    >Hregs >m_return_bind cases pre in EQpre Hregs;
1089    [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct
1090    |2,4: #fst #remaining] *
1091    [1,2: #lab1 * #rest ** #EQ destruct(EQ) * #nxt' * #EQpc change with nxt' in ⊢ (??%? → ?);
1092      #EQ destruct(EQ) #Hrest #Hregs whd in match (length ??); whd in ⊢ (??%? → ?);
1093      #EQ destruct(EQ) whd in EQmid : (??%%); destruct(EQmid) >e0
1094      lapply(seq_list_in_code_length … Hrest) >length_map #EQ >EQ
1095      >nth_opt_append_r
1096      [2,4: >length_append whd in match (length ? [mid1]);
1097             whd in match (length ? [ ]); cases(|rest|) //]
1098      >length_append whd in match (length ? [mid1]); whd in match (length ? [ ]);
1099      cut(S (|rest|) - (|rest| + 1) = O)
1100      [1,3: cases(|rest|) // #m normalize cases m // #m1 normalize nodelta
1101            cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ]
1102      #EQ1 >EQ1 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
1103    |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #EQregs #_ whd in EQmid : (??%%); destruct(EQmid)
1104        >e0 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
1105    ]
1106  |*: #fst #rems #Hregs * #lab1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQmid2
1107      change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest @('bind_inversion EQpreamble)
1108    #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn
1109      >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta
1110      >Hregs >m_return_bind cases pre in EQpre Hregs;
1111      [1,3,6,8: [3,4: #x #y] #_ #_ whd in ⊢ (??%? → ?); whd in match (length ??);
1112        #EQ destruct|2,4: #hd1 #tl1] *
1113      [1,2: #lab1 * #rest1 ** #EQ destruct(EQ) * #nxt1 * #EQpc
1114        change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest1 #Hregs
1115        whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ)
1116      |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #Hregs #_
1117      ]
1118      whd in EQmid : (??%%); destruct(EQmid) >e0 normalize nodelta
1119      [3,4: @eq_identifier_elim [1,3: #_ *] * #H #_ @H %]
1120      lapply(seq_list_in_code_length … EQrest1) >length_map #EQ >EQ
1121      >nth_opt_append_l [2,4: >length_append whd in match (length ? (mid1::?));
1122      whd in match (length ? (mid2::rest)); cases(|rest1|) //] >append_cons
1123      >append_cons >nth_opt_append_l
1124      [2,4: >length_append >length_append whd in match (length ? [ ? ]);
1125            whd in match (length ? [ ]); cases(|rest1|) // ]
1126      >nth_opt_append_r
1127      [2,4: >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]);
1128            cases(|rest1|) // ]
1129      >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]);
1130      cut(S(|rest1|) - (|rest1|+1) = 0)
1131      [1,3: cases(|rest1|) // #m normalize cases m // #m1 normalize nodelta
1132            cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ] #EQ1 >EQ1
1133      normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H %
1134  ]
1135|*: * #lab2 * [1,4,7,10: #j_step #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind
1136    lapply(find_predicate ?????? EQfind) normalize nodelta [5,6,7,8: *]
1137    cases(preamble_length ?????????) normalize nodelta [1,3,5,7: *] #n
1138    inversion(nth_opt ???) normalize nodelta [1,3,5,7: #_ *] #lab1 #EQlab1
1139    @eq_identifier_elim [2,4,6,8: #_ *] #EQ destruct(EQ)
1140    cases(Exists_append … (nth_opt_Exists ???? EQlab1))
1141    [2,4,6,8: * [2,4,6,8: *] #EQ destruct(EQ) cases post in Hregs EQpost;
1142      [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) #_ %] #hd1 #tl1 #Hregs *
1143      #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * #EQt_lab1
1144      change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3
1145      @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq
1146      whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt
1147      >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs
1148      >m_return_bind cases pre in Hregs EQpre;
1149      [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
1150        #EQ destruct(EQ) |2,4: #hd1 #tl1] #Hregs *
1151      [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc
1152        change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4
1153        whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_
1154      |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_
1155      ]
1156      whd in EQmid : (??%%); destruct(EQmid) @⊥ lapply(fresh_labs (point_of_pc p_in pc))
1157      >e0
1158      [1,2: #H cases(append_All … H) #_ * #_ *** -H #H #_ #_ @H
1159      |*: *** #H #_ #_ @H
1160      ]
1161      @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
1162      whd in match code_has_point; normalize nodelta
1163      cases(fetch_stmt_ok_nxt_ok … EQfn (find_lookup ?????? EQfind))
1164      #stmt' #EQstmt' >EQstmt' @I
1165    |*: #Hlab2 cases post in Hregs EQpost;
1166        [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2)
1167          cases(Exists_All … Hlab2 (fresh_labs lab2)) #x * #EQ destruct(EQ) ** #H
1168          @⊥ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
1169          whd in match code_has_point; normalize nodelta
1170          cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt' #EQstmt' >EQstmt' @I
1171        |*: #hd1 #tl1 #Hregs * #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 *
1172          #EQt_lab1 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3
1173          @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq
1174          whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt
1175          >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs
1176          >m_return_bind cases pre in Hregs EQpre;
1177          [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?);
1178             #EQ destruct(EQ)
1179          |2,4: #hd1 #tl1]
1180          #Hregs *
1181          [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc
1182            change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4
1183            whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_
1184          |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_
1185          ]
1186          whd in EQmid : (??%%); destruct(EQmid) cases(pp_labs) #_ #H
1187          lapply(H lab2 (point_of_pc p_in pc) lab1 ? ?)
1188          [3,6,9,12: #EQ destruct(EQ) whd in match (stmt_at ????) in EQstmt;
1189             >(find_lookup ?????? EQfind) in EQstmt; #EQ destruct(EQ) %
1190          |1,4,7,10: >e0 [3,4: whd in match (memb ???); @eqb_elim
1191            [2,4: * #H @⊥ @H %] #_ @I] >memb_append_l2 [1,3: @I]
1192             whd in match (memb ???); @if_elim [1,3: #_ %] #_
1193             whd in match (memb ???); @eqb_elim [1,3: #_ %] * #H1 @⊥ @H1 %
1194          |*:  @Exists_memb assumption
1195          ]
1196        ]
1197     ]
1198]
1199qed.
1200
1201
1202definition make_is_relation_from_beval : (beval → beval → Prop) →
1203internal_stack → internal_stack → Prop≝
1204λR,is1,is2.
1205match is1 with
1206[ empty_is ⇒ match is2 with [ empty_is ⇒ True | _ ⇒ False]
1207| one_is b ⇒ match is2 with [ one_is b' ⇒ R b b' | _ ⇒ False ]
1208| both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2' | _ ⇒ False ]
1209].
1210
1211lemma is_push_ok : ∀Rbeval : beval → beval → Prop.
1212∀Ristack1 : internal_stack → internal_stack → Prop.
1213∀Ristack2 : internal_stack → internal_stack → Prop.
1214(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
1215(∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 →
1216                                   Ristack2 (one_is bv1) (one_is bv2)) →
1217(∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 →
1218                         Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) →
1219                         gen_preserving2 ?? gen_res_preserve …
1220                              Ristack1 Rbeval Ristack2 is_push is_push.
1221#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4
1222whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta
1223[2:#x|3: #x #y #_ @res_preserve_error_gen]
1224cases is2 normalize nodelta
1225 [1,3,5,6: [| #z #w | #z | #z #w] #H5 cases(H … H5) | #y] #H5 @m_gen_return
1226 [@H2 [assumption | @(H … H5) ] | @H1 assumption]
1227qed.
1228(*
1229lemma is_push_ok : ∀R : beval → beval → Prop.
1230               gen_preserving2 ?? gen_res_preserve …
1231                       (make_is_relation_from_beval R) R
1232                       (make_is_relation_from_beval R)
1233                       is_push is_push.
1234#R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H}
1235qed.
1236*)
1237lemma is_pop_ok: ∀Rbeval : beval → beval → Prop.
1238∀Ristack1 : internal_stack → internal_stack → Prop.
1239∀Ristack2 : internal_stack → internal_stack → Prop.
1240(∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) →
1241Ristack2 empty_is empty_is →
1242(∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) →
1243          gen_preserving ?? gen_res_preserve …
1244                              Ristack1
1245                              (λx,y.Rbeval (\fst x) (\fst y) ∧
1246                                Ristack2 (\snd x) (\snd y)) is_pop is_pop.
1247#Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta
1248cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [|#y] cases is2
1249[1,3,4,5: [|#x #y||#x] #H3 cases(H … H3) | #y | #z #w] #H3 normalize nodelta
1250@m_gen_return [ % [ @(H … H3) | assumption ] | cases(H … H3) #H4 #H5 %{H5} @(H2 … H4)
1251qed.
1252
1253(*
1254lemma is_pop_ok1 : ∀R : beval → beval → Prop.
1255           gen_preserving ?? gen_res_preserve …
1256                         (make_is_relation_from_beval R)
1257                         (λx,y.R (\fst x) (\fst y) ∧
1258                               (make_is_relation_from_beval R) (\snd x) (\snd y))
1259                         is_pop is_pop.
1260#R @is_pop_ok //
1261qed.
1262
1263
1264definition make_weak_state_relation ≝
1265λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out.
1266(make_is_relation_from_beval R) (istack … st1) (istack … st2).
1267*)
1268
1269
1270lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
1271(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
1272                  make_is_relation_from_beval Rbeval is1 is2) →
1273(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
1274 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
1275(∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 →
1276 Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) →
1277                    gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2
1278                                   (push p_in) (push p_out).
1279#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4
1280whd in match push; normalize nodelta
1281@(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval))
1282[ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) //
1283  [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5}
1284  | @(H … H3) %
1285  ]
1286| * [|#x|#x1 #x2] * [1,4,7:|2,5,8: #y |*: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?);
1287  [1,2,3,4,6,7,8,9: * [2: #H7 #H8] | #H7] @m_gen_return
1288  [ @(H2 … H3) assumption
1289  | cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?);
1290    #EQ destruct(EQ)
1291  | @(H1 … H3) assumption
1292  ]
1293]
1294qed.
1295
1296
1297lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2.
1298(∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 →
1299                  make_is_relation_from_beval Rbeval is1 is2) →
1300(∀st1,st2.Rstate1 st1 st2 →
1301 Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) →
1302(∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 →
1303 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) →
1304               gen_preserving ?? gen_res_preserve …
1305                 Rstate1
1306                (λx,y.Rbeval (\fst x) (\fst y) ∧
1307                 Rstate2(\snd x) (\snd y))
1308                (pop p_in) (pop p_out).
1309#p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3
1310whd in match pop; normalize nodelta
1311@(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧
1312           (make_is_relation_from_beval Rbeval (\snd x) (\snd y)))) 
1313[ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) %
1314| * #bv1 * [|#x|#x1 #x2] * #bv2 *
1315[1,4,7:|2,5,8: #y
1316|*: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [|#z|#z #w] whd in ⊢ (??%% → ?); #EQ destruct ]
1317#_ #_ * #H4 [2,3,4,6: *| #_ | whd in ⊢ (% → ?); #H5] @m_gen_return
1318% // [ @(H1 … H3) | @(H2 … H3) assumption]
1319qed.
1320
1321(* 
1322lemma next_of_call_pc_ok : ∀P_in,P_out : sem_graph_params.
1323∀init,prog,stack_sizes,init_regs,f_lbls,f_regs.
1324b_graph_transform_program_props P_in P_out stack_sizes
1325  init prog init_regs f_lbls f_regs →
1326let trans_prog ≝ b_graph_transform_program P_in P_out init prog in
1327∀bl :Σb.block_region b =Code.block_id bl ≠ -1 →
1328∀f,fn.
1329fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl =
1330 return 〈f,fn〉 →
1331(∀id,args,dest,lbl.
1332  bind_new_P' ??
1333  (λregs1.λdata.bind_new_P' ??
1334   (λregs2.λblp.
1335     ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')
1336   (f_step … data lbl (CALL P_in ? id args dest)))
1337  (init ? fn)) →
1338gen_preserving ?? gen_res_preserve ????
1339 (λpc1,pc2 : Σpc.pc_block pc = bl.
1340           sigma_stored_pc P_in P_out prog stack_sizes init
1341                                           init_regs f_lbls f_regs pc2 = pc1)
1342 (λn1,n2.sigma_next P_in P_out prog stack_sizes init init_regs f_lbls f_regs bl n2 = return n1)
1343 (next_of_call_pc P_in … (joint_globalenv P_in prog stack_sizes))
1344 (next_of_call_pc P_out … (joint_globalenv P_out trans_prog stack_sizes)).
1345#p_in #p_out #init #prog #stack_sizes #init_regs #f_lbls #f_regs #good #bl #Hbl
1346#f #fn #EQfn #Hcall #pc1 #pc2 #Hpc1pc2 #lbl1 #H @('bind_inversion H) -H ** #f1 #fn1 *
1347[ * [#c| #id #args #dest | #r #lb | #seq ] #nxt | #fin | *]
1348whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) >EQfn >m_return_bind
1349#H @('bind_inversion H) -H #stmt #H lapply(opt_eq_from_res ???? H) -H
1350#EQstmt whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
1351cases(fetch_statement_sigma_stored_pc … pc1 f1 fn1 … good …)
1352[3: >(pi2 ?? pc1) assumption
1353|4: whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) in ⊢ (??%?);
1354    >EQfn in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >EQstmt in ⊢ (??%?); % |2:]
1355#data * #Hdata normalize nodelta * #st_bl * #Hst_bl * #pc' * #EQpc' * #t_fn
1356* #nxt1 * #l1 * #l2 *** #EQt_fetch #_ #_ #nxt1rel %{nxt1} % [2: <(pi2 ?? pc1) assumption]
1357whd in match next_of_call_pc; normalize nodelta <EQpc' in Hpc1pc2;
1358#H lapply(sym_eq ??? H) -H whd in match sigma_stored_pc; normalize nodelta
1359inversion(sigma_pc_opt ?????????)
1360[ #ABS @⊥ whd in match sigma_stored_pc in EQpc'; normalize nodelta in EQpc';
1361  >ABS in EQpc'; normalize nodelta #EQ <(pi2 ?? pc1) in EQfn;
1362  >fetch_internal_function_no_zero [2: <EQ %] whd in ⊢ (???% → ?); #EQ1 destruct(EQ1) ]
1363#sigma_pc' #EQsigma_pc' normalize nodelta inversion(sigma_pc_opt ?????????)
1364[ #_ normalize nodelta #EQ destruct(EQ) @⊥ lapply EQt_fetch @if_elim #_ #EQf
1365  cases(fetch_statement_inv … EQf) >fetch_internal_function_no_zero [1,3: #EQ destruct]
1366  >(pc_block_eq p_in p_out prog stack_sizes init init_regs f_lbls f_regs)
1367  [1,3: whd in match sigma_stored_pc; normalize nodelta >EQsigma_pc' %
1368  |*: >EQsigma_pc' % #EQ destruct
1369  ]
1370]
1371#pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQsigma_pc' in EQpc3; #H
1372lapply(sym_eq ??? H) -H #EQp lapply(sigma_stored_pc_inj … EQp) [>EQsigma_pc' % #EQ destruct]
1373#EQ destruct(EQ) >EQt_fetch @eq_identifier_elim
1374[ #EQ1 >EQ1 in EQstmt; cases(entry_is_cost … (pi2 ?? fn1)) #nxt2 * #c #ABS >ABS #EQ1 destruct(EQ1) ]
1375#_ cases(not_emptyb ??) normalize nodelta >m_return_bind normalize nodelta
1376lapply(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hst_bl)
1377       (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hdata)
1378        (Hcall id args dest (point_of_pc p_in pc1))))
1379#H cases(H (point_of_pc p_in pc2)) #id' * #args' * #dest' #EQ >EQ %
1380qed.
1381*)
1382
1383
1384definition JointStatusSimulation :
1385∀p_in,p_out : sem_graph_params.
1386∀ prog.∀stack_sizes.
1387∀ f_lbls, f_regs. ∀init_regs.∀init.∀st_no_pc_rel,st_rel.
1388good_state_relation p_in p_out prog stack_sizes init init_regs f_lbls f_regs
1389                    st_no_pc_rel st_rel →
1390let trans_prog ≝ b_graph_transform_program p_in p_out init prog in
1391status_rel (joint_abstract_status (mk_prog_params p_in prog stack_sizes))
1392           (joint_abstract_status (mk_prog_params p_out trans_prog stack_sizes)) ≝
1393λp_in,p_out,prog,stack_sizes,f_lbls,f_regs,init_regs,init,st_no_pc_rel,st_rel,good.
1394   mk_status_rel ??
1395    (* sem_rel ≝ *) (λs1 : (joint_abstract_status (mk_prog_params p_in ??)).
1396                     λs2 : (joint_abstract_status (mk_prog_params p_out ??)).st_rel s1 s2)
1397    (* call_rel ≝ *) 
1398       (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call
1399          .λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call
1400           .pc ? s1 =
1401        sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
Note: See TracBrowser for help on using the repository browser.