(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) include "joint/semanticsUtils.ma". include "joint/Traces.ma". include "common/StatusSimulation.ma". include "joint/semantics_blocks.ma". include "utilities/listb_extra.ma". include "utilities/lists.ma". lemma set_no_pc_eta: ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1. #P * // qed. lemma pc_of_label_eq : ∀pars: sem_graph_params. ∀globals,ge,bl,i_fn,lbl. fetch_internal_function ? globals ge bl = return i_fn → pc_of_label pars globals ge bl lbl = OK ? (pc_of_point pars bl lbl). #p #globals #ge #bl #i_fn #lbl #EQf whd in match pc_of_label; normalize nodelta >EQf >m_return_bind % qed. lemma bind_new_bind_new_instantiates' : ∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P. bind_new_instantiates B X x m l → bind_new_P' ?? P m → P l x. #B #X #m elim m normalize nodelta [#x #y * normalize // #B #l' #P * | #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H) @Hr ] qed. lemma bind_new_bind_new_instantiates : ∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P. bind_new_instantiates B X x m l → bind_new_P ?? P m → P x. #B #X #m elim m normalize nodelta [#x #y * normalize // #B #l' #P * | #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H) @Hr ] qed. let rec bind_instantiate B X (b : bind_new B X) (l : list B) on b : (option X) ≝ match b with [ bret B ⇒ match l with [ nil ⇒ Some ? B | _ ⇒ None ? ] | bnew f ⇒ match l with [ nil ⇒ None ? | cons r l' ⇒ bind_instantiate B X (f r) l' ] ]. lemma bind_instantiates_to_instantiate : ∀B,X.∀b : bind_new B X. ∀l : list B.∀x : X. bind_instantiate B X b l = Some ? x → bind_new_instantiates B X x b l. #B #X #b elim b [#x1 * [2: #hd #tl] #x whd in ⊢ (??%? → ?); #EQ destruct(EQ) % |#f #IH * [2: #hd #tl] #x whd in ⊢ (??%? → ?); [2: #EQ destruct(EQ)] #H whd @IH assumption ] qed. lemma bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X. ∀l : list B.∀x : X. bind_new_instantiates B X x b l → bind_instantiate B X b l = Some ? x. #B #X #b elim b [ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) % | #f #IH * [2: #hd #tl] #x whd in ⊢ (% → ?); [2: *] #H whd in ⊢ (??%?); @IH @H ] qed. coercion bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X. ∀l : list B.∀x : X. ∀prf : bind_new_instantiates B X x b l. bind_instantiate B X b l = Some ? x ≝ bind_instantiate_instantiates on _prf : bind_new_instantiates ????? to eq (option ?) (bind_instantiate ????) (Some ??). definition lbl_funct_type ≝ block → label → (list label). definition regs_funct_type ≝ block → label → (list register). definition preamble_length ≝ λP_in : sem_graph_params.λP_out : sem_graph_params.λprog : joint_program P_in. λstack_size : (ident → option ℕ). λinit : ∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals. λinit_regs : block → list register. λf_regs : regs_funct_type.λbl : block.λlbl : label. ! bl ← code_block_of_block bl ; ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (joint_globalenv P_in prog stack_size) bl); ! stmt ← stmt_at P_in … (joint_if_code … fn) lbl; ! data ← bind_instantiate ?? (init … fn) (init_regs bl); match stmt with [ sequential step nxt ⇒ ! step_block ← bind_instantiate ?? (f_step … data lbl step) (f_regs bl lbl); return |\fst (\fst step_block)| | final fin ⇒ ! fin_block ← bind_instantiate ?? (f_fin … data lbl fin) (f_regs bl lbl); return |\fst fin_block| | FCOND abs _ _ _ ⇒ Ⓧabs ]. definition sigma_label : ∀p_in,p_out : sem_graph_params. joint_program p_in → (ident → option ℕ) → (∀globals.joint_closed_internal_function p_in globals →bound_b_graph_translate_data p_in p_out globals) → (block → list register) → lbl_funct_type → regs_funct_type → block → label → option label ≝ λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched. ! bl ← code_block_of_block bl ; ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (joint_globalenv p_in prog stack_size) bl); ! 〈res,s〉 ← find ?? (joint_if_code ?? fn) (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with [ None ⇒ false | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with [ None ⇒ false | Some x ⇒ eq_identifier … searched x ] ]); return res. lemma partial_inj_sigma_label : ∀p_in,p_out,prog,stack_size,init,init_regs. ∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2. sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 = sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 → lbl1 = lbl2. #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2 inversion(sigma_label ????????? lbl1) [ #_ * #H @⊥ @H %] #lbl1' #H @('bind_inversion H) -H #bl' #EQbl' #H @('bind_inversion H) -H * #f #fn #H lapply(res_eq_from_opt ??? H) -H #EQfn #H @('bind_inversion H) -H * #res #stmt #H1 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H #bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) -H * #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ) lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2) cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???) normalize nodelta [*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ % qed. definition sigma_pc_opt : ∀p_in,p_out : sem_graph_params. joint_program p_in → (ident → option ℕ) → (∀globals.joint_closed_internal_function p_in globals →bound_b_graph_translate_data p_in p_out globals) → (block → list register) → lbl_funct_type → regs_funct_type → program_counter → option program_counter ≝ λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. let target_point ≝ point_of_pc p_out pc in if (orb (eqZb (block_id (pc_block pc)) (-1)) (eqZb (block_id (pc_block pc)) OZ)) then return pc else ! source_point ← sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs (pc_block pc) target_point; return pc_of_point p_in (pc_block pc) source_point. lemma sigma_stored_pc_inj : ∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'. sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? → sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc = sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' → pc = pc'. #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs * #bl1 #p1 * #bl2 #p2 inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1 whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta @if_elim normalize nodelta #Hbl [2: #H @('bind_inversion H) -H * #pt1 #EQpt1] whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) -H whd in match sigma_pc_opt; normalize nodelta @if_elim #Hbl1 normalize nodelta [2,4: #H @('bind_inversion H) -H * #pt2 #EQpt2] whd in match pc_of_point; normalize nodelta whd in match (offset_of_point ??); whd in ⊢ (??%% → ?); #EQ destruct(EQ) [2,3: @⊥ lapply Hbl lapply Hbl1 @eqZb_elim normalize nodelta #_ [1,3: **] @eqZb_elim #_ ** |4: %] whd in match (offset_of_point ??) in EQpt2; EQpt1 % #EQ -prog destruct(EQ)] whd in match point_of_pc; normalize nodelta whd in match (point_of_offset ??); whd in match (point_of_offset ??); #EQ -prog destruct(EQ) % qed. definition sigma_stored_pc ≝ λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x]. definition joint_state_relation ≝ λP_in,P_out.program_counter → state P_in → state P_out → Prop. definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop. definition seq_commutation_statement ≝ λP_in,P_out : sem_graph_params. λprog : joint_program P_in.λstack_sizes : ident → option ℕ. λinit : (∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals). λinit_regs : block → list register. λf_lbls : lbl_funct_type. λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out. λst_rel : joint_state_pc_relation P_in P_out. let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). ∀f,fn,stmt,nxt. block_id … (pc_block (pc … st1)) ≠ -1 → let seq ≝ (step_seq P_in ? stmt) in fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential … seq nxt〉 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → st_rel st1 st2 → ∀t_fn. fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = return 〈f,t_fn〉 → bind_new_P' ?? (λregs1.λdata.bind_new_P' ?? (λregs2.λblp. ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))). blp = (ensure_step_block ?? l) ∧ ∃st2_fin_no_pc. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f l (st_no_pc … st2)= return st2_fin_no_pc ∧ st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc ) (f_step … data (point_of_pc P_in (pc … st1)) seq) ) (init ? fn) . definition cond_commutation_statement ≝ λP_in,P_out : sem_graph_params. λprog : joint_program P_in.λstack_sizes : ident → option ℕ. λinit : (∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals). λinit_regs : block → list register. λf_lbls : lbl_funct_type. λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out. λst_rel : joint_state_pc_relation P_in P_out. let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). ∀f,fn,a,ltrue,lfalse,bv,b. block_id … (pc_block (pc … st1)) ≠ -1 → let cond ≝ (COND P_in ? a ltrue) in fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential … cond lfalse〉 → acca_retrieve … P_in (st_no_pc … st1) a = return bv → bool_of_beval … bv = return b → st_rel st1 st2 → ∀t_fn. fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = return 〈f,t_fn〉 → bind_new_P' ?? (λregs1.λdata.bind_new_P' ?? (λregs2.λblp.(\snd blp) = [ ] ∧ ∀mid. stmt_at P_out … (joint_if_code ?? t_fn) mid = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ ∃st2_pre_mid_no_pc. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) = return st2_pre_mid_no_pc ∧ let new_pc ≝ if b then (pc_of_point P_in (pc_block (pc … st1)) ltrue) else (pc_of_point P_in (pc_block (pc … st1)) lfalse) in st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧ ∃a'. ((\snd (\fst blp)) mid) = COND P_out ? a' ltrue ∧ ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧ bool_of_beval … bv' = return b ) (f_step … data (point_of_pc P_in (pc … st1)) cond) ) (init ? fn). definition return_commutation_statement ≝ λP_in,P_out : sem_graph_params. λprog : joint_program P_in.λstack_sizes : ident → option ℕ. λinit : (∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals). λinit_regs : block → list register. λf_lbls : lbl_funct_type. λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out. λst_rel : joint_state_pc_relation P_in P_out. let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). ∀f,fn. block_id … (pc_block (pc … st1)) ≠ -1 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, final P_in ? (RETURN …)〉 → ∀n. stack_sizes f = return n → let curr_ret ≝ joint_if_result … fn in ∀st_pop,pc_pop. pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret (st_no_pc … st1) = return 〈st_pop,pc_pop〉 → ∀nxt.∀f1,fn1,id,args,dest. fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop = return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 → st_rel st1 st2 → ∀t_fn. fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = return 〈f,t_fn〉 → bind_new_P' ?? (λregs1.λdata. bind_new_P' ?? (λregs2.λblp. \snd blp = (RETURN …) ∧ ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f (\fst blp) (st_no_pc … st2)= return st_fin ∧ ∃t_st_pop,t_pc_pop. pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧ sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs t_pc_pop = pc_pop ∧ if eqZb (block_id (pc_block pc_pop)) (-1) then st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) ∧ next_of_call_pc P_out … (joint_globalenv P_out trans_prog stack_sizes) t_pc_pop = return nxt else bind_new_P' ?? (λregs4.λdata1. bind_new_P' ?? (λregs3.λblp1. ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧ st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) (decrement_stack_usage ? n st_pop) st2' ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest)) ) (init ? fn1) ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …)) ) (init ? fn). definition pre_main_commutation_statement ≝ λP_in,P_out : sem_graph_params. λprog : joint_program P_in.λstack_sizes : ident → option ℕ. λinit : (∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals). λinit_regs : block → list register. λf_lbls : lbl_funct_type. λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out. λst_rel : joint_state_pc_relation P_in P_out. let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). block_id … (pc_block (pc … st1)) = -1 → eval_state P_in … (joint_globalenv P_in prog stack_sizes) st1 = return st1' → st_rel st1 st2 → joint_classify … (mk_prog_params P_in prog stack_sizes) st1 = joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧ ∃st2'. st_rel st1' st2' ∧ eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2' ∧ as_label (joint_status P_in prog stack_sizes) st1' = as_label (joint_status P_out trans_prog stack_sizes) st2'. definition call_commutation_statement ≝ λP_in,P_out : sem_graph_params. λprog : joint_program P_in.λstack_sizes : ident → option ℕ. λinit : (∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals). λinit_regs : block → list register. λf_lbls : lbl_funct_type. λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out. λst_rel : joint_state_pc_relation P_in P_out. let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). ∀f,fn,id,arg,dest,nxt. block_id … (pc_block (pc … st1)) ≠ -1 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, sequential P_in ? (CALL P_in ? id arg dest) nxt〉 → ∀bl. block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1) = return bl → ∀f1,fn1. fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl = return 〈f1,fn1〉 → ∀st1_pre. save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre → ∀n.stack_sizes f1 = return n → ∀st1'. setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … n (joint_if_params … fn1) arg f1 st1_pre = return st1' → st_rel st1 st2 → ∀t_fn1. fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl = return 〈f1,t_fn1〉 → bind_new_P' ?? (λregs1.λdata. bind_new_P' ?? (λregs2.λblp. ∀pc',t_fn,id',arg',dest',nxt1. sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs pc' = (pc … st1) → fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc' = return 〈f,t_fn, sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1〉→ ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') → ∃st2_pre_call. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧ block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id' st2_pre_call = return bl ∧ ∃st2_pre. save_frame … P_out (kind_of_call P_out id') dest' (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧ ∃st2_after_call. setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … n (joint_if_params … t_fn1) arg' f1 st2_pre = return st2_after_call ∧ bind_new_P' ?? (λregs11.λdata1. ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) = return st2' ∧ st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1)) (increment_stack_usage P_in n st1') st2' ) (init ? fn1) ) (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest)) ) (init ? fn). definition goto_commutation_statement ≝ λP_in,P_out : sem_graph_params. λprog : joint_program P_in.λstack_sizes : ident → option ℕ. λinit : (∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals). λinit_regs : block → list register. λf_lbls : lbl_funct_type. λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out. λst_rel : joint_state_pc_relation P_in P_out. let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). ∀f,fn,lbl. block_id … (pc_block (pc … st1)) ≠ -1 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, final P_in ? (GOTO ? lbl)〉 → st_rel st1 st2 → ∀t_fn. fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = return 〈f,t_fn〉 → bind_new_P' ?? (λregs1.λdata. bind_new_P' ?? (λregs2.λblp. ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f (\fst blp) (st_no_pc … st2)= return st_fin ∧ \snd blp = GOTO ? lbl ∧ st_no_pc_rel (pc_of_point P_in (pc_block (pc … st1)) lbl) (st_no_pc … st1) (st_fin) ) (f_fin … data (point_of_pc P_in (pc … st1)) (GOTO ? lbl)) ) (init ? fn). definition tailcall_commutation_statement ≝ λP_in,P_out : sem_graph_params. λprog : joint_program P_in.λstack_sizes : ident → option ℕ. λinit : (∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals). λinit_regs : block → list register. λf_lbls : lbl_funct_type. λf_regs : regs_funct_type.λst_no_pc_rel : joint_state_relation P_in P_out. λst_rel : joint_state_pc_relation P_in P_out. let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). ∀f,fn,has_tail,id,arg. block_id … (pc_block (pc … st1)) ≠ -1 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = return 〈f, fn, final P_in ? (TAILCALL P_in has_tail id arg)〉 → ∀bl. block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1) = return bl → ∀f1,fn1. fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl = return 〈f1,fn1〉 → ∀ssize_f.stack_sizes f = return ssize_f → ∀ssize_f1.stack_sizes f1 = return ssize_f1 → ∀st1'. setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … ssize_f1 (joint_if_params … fn1) arg f1 (decrement_stack_usage P_in ssize_f (st_no_pc … st1)) = return st1' → st_rel st1 st2 → ∀t_fn1. fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl = return 〈f1,t_fn1〉 → bind_new_P' ?? (λregs1.λdata. bind_new_P' ?? (λregs2.λblp. ∃ has_tail',id',arg'. (\snd blp) = TAILCALL P_out has_tail' id' arg' ∧ ∃st2_pre_call. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f (\fst blp) (st_no_pc ? st2) = return st2_pre_call ∧ block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id' st2_pre_call = return bl ∧ ∃st2_after. setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … ssize_f1 (joint_if_params … t_fn1) arg' f1 (decrement_stack_usage P_out ssize_f st2_pre_call) = return st2_after ∧ bind_new_P' ?? (λregs11.λdata1. ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 (added_prologue … data1) (increment_stack_usage P_out ssize_f1 st2_after) = return st2' ∧ st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1)) (increment_stack_usage P_in ssize_f1 st1') st2' ) (init ? fn1) ) (f_fin … data (point_of_pc P_in (pc … st1)) (TAILCALL P_in has_tail id arg)) ) (init ? fn). record good_state_relation (P_in : sem_graph_params) (P_out : sem_graph_params) (prog : joint_program P_in) (stack_sizes : ident → option ℕ) (init : ∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals) (init_regs : block → list register) (f_lbls : lbl_funct_type) (f_regs : regs_funct_type) (st_no_pc_rel : joint_state_relation P_in P_out) (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝ { good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init prog init_regs f_lbls f_regs ; fetch_ok_sigma_state_ok : ∀st1,st2,f,fn. st_rel st1 st2 → fetch_internal_function … (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) = return 〈f,fn〉 → st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2) ; fetch_ok_pc_ok : ∀st1,st2,f,fn.st_rel st1 st2 → fetch_internal_function … (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) = return 〈f,fn〉 → pc … st1 = pc … st2 ; fetch_ok_sigma_last_pop_ok : ∀st1,st2,f,fn.st_rel st1 st2 → fetch_internal_function … (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) = return 〈f,fn〉 → (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs (last_pop … st2) ; st_rel_def : ∀st1,st2,pc,lp1,lp2,f,fn. fetch_internal_function … (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 → st_no_pc_rel pc st1 st2 → lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs lp2 → st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2) ; pre_main_ok : pre_main_commutation_statement P_in P_out prog stack_sizes init init_regs f_lbls f_regs st_no_pc_rel st_rel ; pre_main_no_return : ∀f,fn,pc. block_id (pc_block pc) = -1 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc = return 〈f,fn,final P_in ? (RETURN …)〉 → False ; cond_commutation : cond_commutation_statement P_in P_out prog stack_sizes init init_regs f_lbls f_regs st_no_pc_rel st_rel ; seq_commutation : seq_commutation_statement P_in P_out prog stack_sizes init init_regs f_lbls f_regs st_no_pc_rel st_rel ; call_is_call :∀f,fn,bl. fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl = return 〈f,fn〉 → ∀id,args,dest,lbl. bind_new_P' ?? (λregs1.λdata.bind_new_P' ?? (λregs2.λblp. ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') (f_step … data lbl (CALL P_in ? id args dest))) (init ? fn) ; cost_commutation : let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1,st2,pc.∀f,fn,c,nxt. block_id … (pc_block pc) ≠ -1 → st_no_pc_rel pc st1 st2 → fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc = return 〈f, fn, sequential ?? (COST_LABEL ?? c) nxt〉 → st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2 ; return_commutation : return_commutation_statement P_in P_out prog stack_sizes init init_regs f_lbls f_regs st_no_pc_rel st_rel ; call_commutation : call_commutation_statement P_in P_out prog stack_sizes init init_regs f_lbls f_regs st_no_pc_rel st_rel ; goto_commutation : goto_commutation_statement P_in P_out prog stack_sizes init init_regs f_lbls f_regs st_no_pc_rel st_rel ; tailcall_commutation : tailcall_commutation_statement P_in P_out prog stack_sizes init init_regs f_lbls f_regs st_no_pc_rel st_rel ; as_result_ok : let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). st_rel st1 st2 → as_result … st1 = as_result … st2 ; as_label_premain_ok : let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). block_id … (pc_block (pc … st1)) = -1 → st_rel st1 st2 → as_label … st1 = as_label … st2 }. record good_init_relation (P_in : sem_graph_params) (P_out : sem_graph_params) (prog : joint_program P_in) (stack_sizes : ident → option ℕ) (init : ∀globals.joint_closed_internal_function P_in globals →bound_b_graph_translate_data P_in P_out globals) (st_no_pc_rel : joint_state_relation P_in P_out) : Prop ≝ { good_empty : ∀m0.init_mem … (λx.x) prog = return m0 → let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in let trans_prog ≝ b_graph_transform_program P_in P_out init prog in let globals_size ≝ globals_stacksize … prog in let globals_size' ≝ globals_stacksize … trans_prog in let spp ≝ mk_pointer spb (mk_offset (bitvector_of_Z 16 (-S (globals_size)))) in let spp' ≝ mk_pointer spb (mk_offset (bitvector_of_Z 16 (-S (globals_size')))) in ∀prf,prf'. let st ≝ mk_state P_in (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … «spp,prf») m 0 in let st' ≝ mk_state P_out (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … «spp',prf'») m 0 in st_no_pc_rel init_pc (set_sp … «spp,prf» st) (set_sp … «spp',prf'» st') ; good_init_cost_label : let trans_prog ≝ b_graph_transform_program P_in P_out init prog in match fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) init_pc with [ OK x ⇒ match cost_label_of_stmt … (\snd x) with [ Some c ⇒ ∃y. fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) init_pc = OK ? y ∧ cost_label_of_stmt … (\snd y) = Some ? c | None ⇒ (∃e'. fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) init_pc = Error ? e') ∨ (∃x. fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) init_pc = OK ? x ∧ cost_label_of_stmt … (\snd x) = None ?) ] | Error e ⇒ (∃e'. fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) init_pc = Error ? e') ∨ (∃x. fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) init_pc = OK ? x ∧ cost_label_of_stmt … (\snd x) = None ?) ] }. lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code. code_block_of_block bl = return bl. * #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim [ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 % qed. (*TO BE MOVED*) lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2). #A #l1 elim l1 [#l2 #P *] #hd #tl #IH * [#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption | #H %2 @IH assumption] qed. lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2). #A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH * [#a normalize // ] #hd1 #tl1 #a normalize * [ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 // | #H %2 >append_cons @IH assumption] qed. lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident. ∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst. seq_list_in_code p globals code src l1 l2 dst → |l1| = |l2|. #p #globals #code #src #l1 lapply src -src elim l1 [ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct] #hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct] #hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt #EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H) qed. lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params. ∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl. In ? (stmt_labels p ? stmt) lbl→ fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 → pc' = pc_of_point p (pc_block pc) lbl → ∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉. #p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt #EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) * cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?) [3: * cases lbl #x #y cases(decidable_eq_pos … x y) [#EQ destruct % % | * #H %2 % #H1 @H destruct %] | whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct whd in match code_has_label; whd in match code_has_point; normalize nodelta inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'} whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind >point_of_pc_of_point >EQstmt' % | #H lapply(In_all ??? H) -H cases(Exists_append … Hlbl) [ cases stmt [ #step #nxt | #fin | *] whd in match stmt_implicit_label; normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_ whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'} whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind >point_of_pc_of_point >EQstmt' % | #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H % ] ] qed. lemma fetch_stmt_ok_nxt_ok : ∀p : sem_graph_params. ∀prog : joint_program p.∀stack_size,f,fn,stmt,bl,pt,nxt. fetch_internal_function … (joint_globalenv p prog stack_size) bl = return 〈f,fn〉→ stmt_at p … (joint_if_code … fn) pt = return sequential p ? stmt nxt → ∃stmt'. stmt_at p … (joint_if_code … fn) nxt = return stmt'. #p #prog #stack_size #f #fn #stmt #bl #pt #nxt #EQfn #EQstmt cases(fetch_stmt_ok_succ_ok … prog stack_size f fn (sequential p … stmt nxt) (pc_of_point p bl pt) (pc_of_point p bl nxt) nxt ???) [ #stmt' #H cases(fetch_statement_inv … H) -H #_ >point_of_pc_of_point normalize nodelta #EQstmt' %{stmt'} assumption | whd in match stmt_labels; normalize nodelta % % | whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind >point_of_pc_of_point >EQstmt % | % ] qed. lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs. ∀f_lbls : lbl_funct_type.∀f_regs. b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs → ∀id,fn. ∀bl:Σb.block_region b = Code. ∀pt,stmt. block_id … bl ≠ -1 → fetch_internal_function … (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 → stmt_at p_in … (joint_if_code … fn) pt = return stmt → ∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧ match n with [ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt | S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt ]. #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn #bl #pt #stmt * #Hbl #EQfn #EQstmt lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn) @eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; -stmt [ #j_step #nxt | #fin | * ] #EQstmt normalize nodelta ** [ * #pre_instr #instr #post_instr | #pre_instr #instr] * [ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta [ @eq_identifier_elim #EQentry normalize nodelta [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ) |*: #Hregs ] | #Hregs ] | #Hregs ] #syntax_spec [4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_ [1,2,4,5: %{(|pre_instr|)} | %{O}] cut(? : Prop) [3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec whd in match (length ??); #EQn whd in match (length ??); normalize nodelta] [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????) [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit >m_return_bind cases stmt1 in EQfind; -stmt1 [1,4,7,10,13: #j_step1 #nxt1 |2,5,8,11,14: #fin1 |*: *] #EQfind normalize nodelta cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *] [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1 ] >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl] whd in match (length ??); normalize nodelta [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] #EQ #_ >EQ %] whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *] #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥ cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) ** #H #_ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; whd in match code_has_point; normalize nodelta >EQstmt @I |*: cases syntax_spec -syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *] cases pre -pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) -EQ #pre_spec whd in ⊢ (% → ?); [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec |*: #EQt_stmt ] %{mid1} cut(? : Prop) [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????) [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit >m_return_bind cases stmt1 in EQfind; -stmt1 [1,4,7,10: #j_step1 #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind normalize nodelta cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *] [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 |*: * #pre_instr1 #instr1] >m_return_bind cases pre_instr1 -pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1] whd in match (length ??); normalize nodelta whd in match (nth_opt ???); [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_ @(proj2 … pp_labs ?? lbl2) @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)] >e0 @Exists_append2 % % |*: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥ lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * -H ** #H #_ #_ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; whd in match code_has_point; normalize nodelta whd in match (stmt_at ????); >(find_lookup ?????? EQfind) @I ] |2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H) [1,2: >length_map] -H #H >H >nth_opt_append_r cases(|rest|) try % try( #n %) #n code_block_of_block_eq >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta [1,2,3,4: >Hregs % | >EQregs EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data) whd in match (bind_instantiate ????); % ] |*: ] qed. lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls, f_regs,pc. sigma_pc_opt p_in p_out prog stack_sizes init init_regs f_lbls f_regs pc ≠ None ? → pc_block … pc = pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs pc). #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc whd in match sigma_stored_pc; normalize nodelta inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1 whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ %] #_ #H @('bind_inversion H) -H #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ % qed. definition stmt_get_next : ∀p,globals.joint_statement p globals → option (succ p) ≝ λp,globals,stmt. match stmt with [sequential stmt nxt ⇒ Some ? nxt | _ ⇒ None ? ]. definition sigma_next : ∀p_in,p_out : sem_graph_params. joint_program p_in → (ident → option ℕ) → (∀globals.joint_closed_internal_function p_in globals →bound_b_graph_translate_data p_in p_out globals) → (block → list register) → lbl_funct_type → regs_funct_type → block → label → option label ≝ λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched. ! bl ← code_block_of_block bl ; ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (joint_globalenv p_in prog stack_size) bl); ! 〈res,s〉 ← find ?? (joint_if_code ?? fn) (λlbl.λstmt.match stmt_get_next … stmt with [ None ⇒ false | Some nxt ⇒ match preamble_length … prog stack_size init init_regs f_regs bl lbl with [ None ⇒ false | Some n ⇒ match nth_opt ? n ((f_lbls bl lbl) @ [nxt]) with [ None ⇒ false | Some x ⇒ eq_identifier … searched x ] ] ]); stmt_get_next … s. lemma fetch_internal_function_no_zero : ∀p,prog,stack_size,bl. block_id (pi1 … bl) = 0 → fetch_internal_function … (joint_globalenv p prog stack_size) bl = Error ? [MSG BadFunction]. #p #prg #stack_size #bl #Hbl whd in match fetch_internal_function; whd in match fetch_function; normalize nodelta @eqZb_elim [ >Hbl #EQ @⊥ cases(not_eq_OZ_neg one) #H @H assumption ] #_ normalize nodelta cases(symbol_for_block ???) [%] #id >m_return_bind cases bl in Hbl; * #id #prf #EQ destruct(EQ) change with (mk_block OZ) in match (mk_block ?); cut(find_funct_ptr (fundef (joint_closed_internal_function p (prog_names p prg))) (joint_globalenv p prg stack_size) (mk_block OZ) = None ?) [%] #EQ >EQ % qed. lemma fetch_statement_sigma_stored_pc : ∀p_in,p_out,prog,stack_sizes, init,init_regs,f_lbls,f_regs,pc,f,fn,stmt. b_graph_transform_program_props p_in p_out stack_sizes init prog init_regs f_lbls f_regs → block_id … (pc_block pc) ≠ -1 → let trans_prog ≝ b_graph_transform_program p_in p_out init prog in fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc = return 〈f,fn,stmt〉 → ∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧ match stmt with [ sequential step nxt ⇒ ∃step_block : step_block p_out (prog_names … trans_prog). bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step) (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧ ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs pc' = pc ∧ ∃fn',nxt',l1,l2. fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' = if not_emptyb … (added_prologue … data) ∧ eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn) then OK ? 〈f,fn',sequential ?? (NOOP …) nxt'〉 else OK ? 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉 ∧ seq_list_in_code p_out (prog_names … trans_prog) (joint_if_code … fn') (point_of_pc p_out pc) (map_eval … (\fst (\fst step_block)) (point_of_pc p_out pc')) l1 (point_of_pc p_out pc') ∧ seq_list_in_code p_out ? (joint_if_code … fn') nxt' (\snd step_block) l2 nxt ∧ sigma_next p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc_block pc) nxt' = return nxt | final fin ⇒ ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin) (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧ ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs pc' = pc ∧ ∃fn'.fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' = return 〈f,fn',final ?? (\snd fin_block)〉 | FCOND abs _ _ _ ⇒ Ⓧabs ]. #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt #good #Hbl #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn) @eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) -H #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H normalize nodelta #H #_ %{data} >Hinit %{(refl …)} -EQfetch cases stmt in EQstmt H; [ #step #nxt | #fin | *] normalize nodelta #EQstmt -stmt [ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta [ @eq_identifier_elim #EQentry normalize nodelta ] ] * #block * [ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) |*: #Hregs #syntax_spec ] [ whd in match (point_of_pc ??) in EQstmt EQentry; EQstmt #EQ destruct(EQ) % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] |] %{pc} whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta @eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ @eqZb_elim [ #EQ >fetch_internal_function_no_zero in EQt_fn; [2: assumption] whd in ⊢ (???% → ?); #ABS destruct(ABS) ] normalize nodelta #_ |*: %{block} >Hregs %{(refl …)} ] cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab [ whd in match (point_of_pc ??) in e0; e0 in EQnth_opt; whd in ⊢ (??%% → ?); #EQ destruct(EQ) |5: whd in match (point_of_pc ??); EQsigma_lab >m_return_bind normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} %{[ ]} %{[ ]} whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind >EQt_stmt >m_return_bind % [ % [ % [ @eq_identifier_elim [#_ %] * #H @⊥ @H % | %{(refl …) (refl …)}] | %{(refl …) (refl …)}]] whd in match sigma_next; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????) [ #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta >EQpreamble normalize nodelta >EQentry >e0 normalize nodelta @eq_identifier_elim [#_ *] * #H #_ @H %] * #lbl1 #stmt1 #EQfind >m_return_bind lapply(find_predicate ?????? EQfind) inversion(stmt_get_next … stmt1) [#_ *] #nxt1 #EQnxt1 normalize nodelta inversion(preamble_length ?????????) [#_ *] #m whd in match preamble_length; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit >m_return_bind cases stmt1 in EQfind; [#j_step #succ | #fin | *] #EQfind normalize nodelta cases(bind_instantiate ???) [1,3: whd in ⊢ (??%% → ?); #EQ destruct] #bl1 >m_return_bind whd in ⊢ (??%? → ?); #EQ destruct(EQ) inversion(nth_opt ???) [1,3: #_ *] #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4: #_ *] #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 cases(Exists_append … (nth_opt_Exists ???? EQlbl2)) [2,4: * [2,4: *] #EQ >EQ #_ %] #H @⊥ cases(Exists_All … H (fresh_labs lbl1)) #x * #EQ destruct(EQ) ** -H #H #_ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; whd in match code_has_point; normalize nodelta cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt2 #EQ >EQ @I |2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)} |6,7,8: %{pc} ] whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta @eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta @eqZb_elim [1,3,5,7,9,11: #EQ >fetch_internal_function_no_zero in EQt_fn; [2,4,6,8,10,12: assumption] whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_ normalize nodelta [1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc) %{(refl …)} %{t_fn} cases block in Hregs syntax_spec; -block [1,2,4,5: * #pre #instr #post |*: #pre #instr ] #Hregs * [1,2,3,4: #l1 * #mid1 * #mid2 * #l2 *** |*: #l1 * #mid ** ] #EQmid #EQpre whd in ⊢ (% → ?); [1,2,3,4: * #nxt1 *] #EQt_stmt [1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2} %{l1} %{l2} %] [1,3,5,7,9,10: whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; -pre [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ)] [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid; [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct] * #mid * #rest ** #EQ destruct(EQ)] [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: % [ %{(refl …)} %{(refl …) (refl …)} ] assumption] @eq_identifier_elim [2: #_ % [ %{(refl …)} %{(refl …) (refl …)} | assumption] ] #EQ e0 in EQnth_opt; lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1 >nth_opt_append_r [2,4,6: %] cut(|rest|-|rest|=O) [1,3,5: cases(|rest|) //] #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 -EQ2 -EQ1 [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt [2: >point_of_pc_of_point % [%{(refl …)} whd %{mid'} %{rest} % [2: assumption] % [2: assumption] %] assumption] @eq_identifier_elim [#EQ4 point_of_pc_of_point % [ %{(refl …)} whd %{mid'} %{rest} % [ %{(refl …)} assumption ] assumption | assumption ] ] destruct(EQ3) >point_of_pc_of_point >EQt_stmt %] whd in match sigma_next; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????) [1,3,5,7: #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta >EQpreamble normalize nodelta cases post in Hregs EQpost; [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs >m_return_bind cases pre in EQpre Hregs; [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct |2,4: #fst #remaining] * [1,2: #lab1 * #rest ** #EQ destruct(EQ) * #nxt' * #EQpc change with nxt' in ⊢ (??%? → ?); #EQ destruct(EQ) #Hrest #Hregs whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) whd in EQmid : (??%%); destruct(EQmid) >e0 lapply(seq_list_in_code_length … Hrest) >length_map #EQ >EQ >nth_opt_append_r [2,4: >length_append whd in match (length ? [mid1]); whd in match (length ? [ ]); cases(|rest|) //] >length_append whd in match (length ? [mid1]); whd in match (length ? [ ]); cut(S (|rest|) - (|rest| + 1) = O) [1,3: cases(|rest|) // #m normalize cases m // #m1 normalize nodelta cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 EQ1 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #EQregs #_ whd in EQmid : (??%%); destruct(EQmid) >e0 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % ] |*: #fst #rems #Hregs * #lab1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQmid2 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs >m_return_bind cases pre in EQpre Hregs; [1,3,6,8: [3,4: #x #y] #_ #_ whd in ⊢ (??%? → ?); whd in match (length ??); #EQ destruct|2,4: #hd1 #tl1] * [1,2: #lab1 * #rest1 ** #EQ destruct(EQ) * #nxt1 * #EQpc change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest1 #Hregs whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #Hregs #_ ] whd in EQmid : (??%%); destruct(EQmid) >e0 normalize nodelta [3,4: @eq_identifier_elim [1,3: #_ *] * #H #_ @H %] lapply(seq_list_in_code_length … EQrest1) >length_map #EQ >EQ >nth_opt_append_l [2,4: >length_append whd in match (length ? (mid1::?)); whd in match (length ? (mid2::rest)); cases(|rest1|) //] >append_cons >append_cons >nth_opt_append_l [2,4: >length_append >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]); cases(|rest1|) // ] >nth_opt_append_r [2,4: >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]); cases(|rest1|) // ] >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]); cut(S(|rest1|) - (|rest1|+1) = 0) [1,3: cases(|rest1|) // #m normalize cases m // #m1 normalize nodelta cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 EQ1 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % ] |*: * #lab2 * [1,4,7,10: #j_step #nxt1 |2,5,8,11: #fin1 |*: *] #EQfind lapply(find_predicate ?????? EQfind) normalize nodelta [5,6,7,8: *] cases(preamble_length ?????????) normalize nodelta [1,3,5,7: *] #n inversion(nth_opt ???) normalize nodelta [1,3,5,7: #_ *] #lab1 #EQlab1 @eq_identifier_elim [2,4,6,8: #_ *] #EQ destruct(EQ) cases(Exists_append … (nth_opt_Exists ???? EQlab1)) [2,4,6,8: * [2,4,6,8: *] #EQ destruct(EQ) cases post in Hregs EQpost; [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) #_ %] #hd1 #tl1 #Hregs * #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * #EQt_lab1 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3 @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) |2,4: #hd1 #tl1] #Hregs * [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4 whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_ ] whd in EQmid : (??%%); destruct(EQmid) @⊥ lapply(fresh_labs (point_of_pc p_in pc)) >e0 [1,2: #H cases(append_All … H) #_ * #_ *** -H #H #_ #_ @H |*: *** #H #_ #_ @H ] @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; whd in match code_has_point; normalize nodelta cases(fetch_stmt_ok_nxt_ok … EQfn (find_lookup ?????? EQfind)) #stmt' #EQstmt' >EQstmt' @I |*: #Hlab2 cases post in Hregs EQpost; [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) cases(Exists_All … Hlab2 (fresh_labs lab2)) #x * #EQ destruct(EQ) ** #H @⊥ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; whd in match code_has_point; normalize nodelta cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt' #EQstmt' >EQstmt' @I |*: #hd1 #tl1 #Hregs * #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * #EQt_lab1 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3 @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) |2,4: #hd1 #tl1] #Hregs * [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4 whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ |*: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_ ] whd in EQmid : (??%%); destruct(EQmid) cases(pp_labs) #_ #H lapply(H lab2 (point_of_pc p_in pc) lab1 ? ?) [3,6,9,12: #EQ destruct(EQ) whd in match (stmt_at ????) in EQstmt; >(find_lookup ?????? EQfind) in EQstmt; #EQ destruct(EQ) % |1,4,7,10: >e0 [3,4: whd in match (memb ???); @eqb_elim [2,4: * #H @⊥ @H %] #_ @I] >memb_append_l2 [1,3: @I] whd in match (memb ???); @if_elim [1,3: #_ %] #_ whd in match (memb ???); @eqb_elim [1,3: #_ %] * #H1 @⊥ @H1 % |*: @Exists_memb assumption ] ] ] ] qed. definition make_is_relation_from_beval : (beval → beval → Prop) → internal_stack → internal_stack → Prop≝ λR,is1,is2. match is1 with [ empty_is ⇒ match is2 with [ empty_is ⇒ True | _ ⇒ False] | one_is b ⇒ match is2 with [ one_is b' ⇒ R b b' | _ ⇒ False ] | both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2' | _ ⇒ False ] ]. lemma is_push_ok : ∀Rbeval : beval → beval → Prop. ∀Ristack1 : internal_stack → internal_stack → Prop. ∀Ristack2 : internal_stack → internal_stack → Prop. (∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) → (∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) → (∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 → Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) → gen_preserving2 ?? gen_res_preserve … Ristack1 Rbeval Ristack2 is_push is_push. #Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4 whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta [2:#x|3: #x #y #_ @res_preserve_error_gen] cases is2 normalize nodelta [1,3,5,6: [| #z #w | #z | #z #w] #H5 cases(H … H5) | #y] #H5 @m_gen_return [@H2 [assumption | @(H … H5) ] | @H1 assumption] qed. (* lemma is_push_ok : ∀R : beval → beval → Prop. gen_preserving2 ?? gen_res_preserve … (make_is_relation_from_beval R) R (make_is_relation_from_beval R) is_push is_push. #R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H} qed. *) lemma is_pop_ok: ∀Rbeval : beval → beval → Prop. ∀Ristack1 : internal_stack → internal_stack → Prop. ∀Ristack2 : internal_stack → internal_stack → Prop. (∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) → Ristack2 empty_is empty_is → (∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) → gen_preserving ?? gen_res_preserve … Ristack1 (λx,y.Rbeval (\fst x) (\fst y) ∧ Ristack2 (\snd x) (\snd y)) is_pop is_pop. #Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [|#y] cases is2 [1,3,4,5: [|#x #y||#x] #H3 cases(H … H3) | #y | #z #w] #H3 normalize nodelta @m_gen_return [ % [ @(H … H3) | assumption ] | cases(H … H3) #H4 #H5 %{H5} @(H2 … H4) qed. (* lemma is_pop_ok1 : ∀R : beval → beval → Prop. gen_preserving ?? gen_res_preserve … (make_is_relation_from_beval R) (λx,y.R (\fst x) (\fst y) ∧ (make_is_relation_from_beval R) (\snd x) (\snd y)) is_pop is_pop. #R @is_pop_ok // qed. definition make_weak_state_relation ≝ λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out. (make_is_relation_from_beval R) (istack … st1) (istack … st2). *) lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2. (∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 → make_is_relation_from_beval Rbeval is1 is2) → (∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 → Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) → (∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 → Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) → gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2 (push p_in) (push p_out). #p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4 whd in match push; normalize nodelta @(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval)) [ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) // [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5} | @(H … H3) % ] | * [|#x|#x1 #x2] * [1,4,7:|2,5,8: #y |*: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?); [1,2,3,4,6,7,8,9: * [2: #H7 #H8] | #H7] @m_gen_return [ @(H2 … H3) assumption | cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?); #EQ destruct(EQ) | @(H1 … H3) assumption ] ] qed. lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2. (∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 → make_is_relation_from_beval Rbeval is1 is2) → (∀st1,st2.Rstate1 st1 st2 → Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) → (∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 → Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) → gen_preserving ?? gen_res_preserve … Rstate1 (λx,y.Rbeval (\fst x) (\fst y) ∧ Rstate2(\snd x) (\snd y)) (pop p_in) (pop p_out). #p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3 whd in match pop; normalize nodelta @(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧ (make_is_relation_from_beval Rbeval (\snd x) (\snd y)))) [ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) % | * #bv1 * [|#x|#x1 #x2] * #bv2 * [1,4,7:|2,5,8: #y |*: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [|#z|#z #w] whd in ⊢ (??%% → ?); #EQ destruct ] #_ #_ * #H4 [2,3,4,6: *| #_ | whd in ⊢ (% → ?); #H5] @m_gen_return % // [ @(H1 … H3) | @(H2 … H3) assumption] qed. (* lemma next_of_call_pc_ok : ∀P_in,P_out : sem_graph_params. ∀init,prog,stack_sizes,init_regs,f_lbls,f_regs. b_graph_transform_program_props P_in P_out stack_sizes init prog init_regs f_lbls f_regs → let trans_prog ≝ b_graph_transform_program P_in P_out init prog in ∀bl :Σb.block_region b =Code.block_id bl ≠ -1 → ∀f,fn. fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl = return 〈f,fn〉 → (∀id,args,dest,lbl. bind_new_P' ?? (λregs1.λdata.bind_new_P' ?? (λregs2.λblp. ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') (f_step … data lbl (CALL P_in ? id args dest))) (init ? fn)) → gen_preserving ?? gen_res_preserve ???? (λpc1,pc2 : Σpc.pc_block pc = bl. sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs pc2 = pc1) (λn1,n2.sigma_next P_in P_out prog stack_sizes init init_regs f_lbls f_regs bl n2 = return n1) (next_of_call_pc P_in … (joint_globalenv P_in prog stack_sizes)) (next_of_call_pc P_out … (joint_globalenv P_out trans_prog stack_sizes)). #p_in #p_out #init #prog #stack_sizes #init_regs #f_lbls #f_regs #good #bl #Hbl #f #fn #EQfn #Hcall #pc1 #pc2 #Hpc1pc2 #lbl1 #H @('bind_inversion H) -H ** #f1 #fn1 * [ * [#c| #id #args #dest | #r #lb | #seq ] #nxt | #fin | *] whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) >EQfn >m_return_bind #H @('bind_inversion H) -H #stmt #H lapply(opt_eq_from_res ???? H) -H #EQstmt whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases(fetch_statement_sigma_stored_pc … pc1 f1 fn1 … good …) [3: >(pi2 ?? pc1) assumption |4: whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) in ⊢ (??%?); >EQfn in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >EQstmt in ⊢ (??%?); % |2:] #data * #Hdata normalize nodelta * #st_bl * #Hst_bl * #pc' * #EQpc' * #t_fn * #nxt1 * #l1 * #l2 *** #EQt_fetch #_ #_ #nxt1rel %{nxt1} % [2: <(pi2 ?? pc1) assumption] whd in match next_of_call_pc; normalize nodelta ABS in EQpc'; normalize nodelta #EQ <(pi2 ?? pc1) in EQfn; >fetch_internal_function_no_zero [2: fetch_internal_function_no_zero [1,3: #EQ destruct] >(pc_block_eq p_in p_out prog stack_sizes init init_regs f_lbls f_regs) [1,3: whd in match sigma_stored_pc; normalize nodelta >EQsigma_pc' % |*: >EQsigma_pc' % #EQ destruct ] ] #pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) EQsigma_pc' % #EQ destruct] #EQ destruct(EQ) >EQt_fetch @eq_identifier_elim [ #EQ1 >EQ1 in EQstmt; cases(entry_is_cost … (pi2 ?? fn1)) #nxt2 * #c #ABS >ABS #EQ1 destruct(EQ1) ] #_ cases(not_emptyb ??) normalize nodelta >m_return_bind normalize nodelta lapply(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hst_bl) (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hdata) (Hcall id args dest (point_of_pc p_in pc1)))) #H cases(H (point_of_pc p_in pc2)) #id' * #args' * #dest' #EQ >EQ % qed. *) definition JointStatusSimulation : ∀p_in,p_out : sem_graph_params. ∀ prog.∀stack_sizes. ∀ f_lbls, f_regs. ∀init_regs.∀init.∀st_no_pc_rel,st_rel. good_state_relation p_in p_out prog stack_sizes init init_regs f_lbls f_regs st_no_pc_rel st_rel → let trans_prog ≝ b_graph_transform_program p_in p_out init prog in status_rel (joint_abstract_status (mk_prog_params p_in prog stack_sizes)) (joint_abstract_status (mk_prog_params p_out trans_prog stack_sizes)) ≝ λp_in,p_out,prog,stack_sizes,f_lbls,f_regs,init_regs,init,st_no_pc_rel,st_rel,good. mk_status_rel ?? (* sem_rel ≝ *) (λs1 : (joint_abstract_status (mk_prog_params p_in ??)). λs2 : (joint_abstract_status (mk_prog_params p_out ??)).st_rel s1 s2) (* call_rel ≝ *) (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call .λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call .pc ? s1 = sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).