(**************************************************************************) (* ___ *) (* ||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 "ERTL/ERTLToERTLptr.ma". include "common/StatusSimulation.ma". include "joint/Traces.ma". include "ERTLptr/ERTLptr_semantics.ma". include "common/ExtraMonads.ma". definition ERTL_status ≝ λprog : ertl_program.λstack_sizes. joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes). definition ERTLptr_status ≝ λprog : ertlptr_program.λstack_sizes. joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes). definition sigma_map ≝ block → label → option label. definition lbl_funct ≝ block → label → (list label). definition regs_funct ≝ block → label → (list register). (*TO BE MOVED*) lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region. ∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) → (∀ prf : r = Code.P (g prf)) → P ((match r return λx.(r = x → ?) with [XData ⇒ f | Code ⇒ g])(refl ? r)). #A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2] qed. definition get_sigma : ertl_program → lbl_funct → sigma_map ≝ λprog,f_lbls.λbl,searched. let globals ≝ prog_var_names … prog in let ge ≝ globalenv_noinit … prog in ! bl ← code_block_of_block bl ; ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl); !〈res,s〉 ← find ?? (joint_if_code … fn) (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with [None ⇒ eq_identifier … searched lbl |Some x ⇒ eq_identifier … searched (\snd x) ]); return res. definition sigma_pc_opt : ertl_program → lbl_funct → program_counter → option program_counter ≝ λprog,f_lbls,pc. let sigma ≝ get_sigma prog f_lbls in let ertl_ptr_point ≝ point_of_pc ERTLptr_semantics pc in if eqZb (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *) return pc else ! ertl_point ← sigma (pc_block pc) ertl_ptr_point; return pc_of_point ERTL_semantics (pc_block pc) ertl_point. definition sigma_stored_pc ≝ λprog,f_lbls,pc. match sigma_pc_opt prog f_lbls pc with [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x]. definition sigma_beval : ertl_program → lbl_funct → beval → beval ≝ λprog,f_lbls,bv. match bv with [ BVpc pc prt ⇒ match sigma_pc_opt prog f_lbls pc with [None ⇒ BVundef | Some x ⇒ BVpc x prt] | _ ⇒ bv ]. definition sigma_is : ertl_program → lbl_funct → internal_stack → internal_stack ≝ λprog,f_lbls,is. match is with [ empty_is ⇒ empty_is | one_is bv ⇒ one_is (sigma_beval prog f_lbls bv) | both_is bv1 bv2 ⇒ both_is (sigma_beval prog f_lbls bv1) (sigma_beval prog f_lbls bv2) ]. lemma sigma_is_empty : ∀prog,sigma. sigma_is prog sigma empty_is = empty_is. #prog #sigma % qed. definition sigma_mem : ertl_program → lbl_funct → bemem → bemem ≝ λprog,f_lbls,m. mk_mem (λb. If Zltb (block_id b) (nextblock m) then with prf' do let l ≝ low_bound m b in let h ≝ high_bound m b in mk_block_contents l h (λz.If Zleb l z ∧ Zltb z h then with prf'' do sigma_beval prog f_lbls (contents (blocks m b) z) else BVundef) else empty_block OZ OZ) (nextblock m) (nextblock_pos m). include "common/ExtraIdentifiers.ma". definition sigma_register_env : ertl_program → lbl_funct → list register → register_env beval → register_env beval ≝ λprog,f_lbls,ids,psd_env. let m' ≝ map ??? psd_env (λbv.sigma_beval prog f_lbls bv) in m' ∖ ids. definition sigma_frames_opt : ertl_program → lbl_funct → regs_funct → list (register_env beval × (Σb:block.block_region b=Code)) → option (list (register_env beval × (Σb:block.block_region b=Code))) ≝ λprog,f_lbls,f_regs,frms. let globals ≝ prog_var_names … prog in let ge ≝ globalenv_noinit … prog in m_list_map ? ? ? (λx.let 〈reg_env,bl〉 ≝ x in ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl); return 〈sigma_register_env prog f_lbls (added_registers ERTL globals fn (f_regs bl)) reg_env,bl〉) frms. definition sigma_frames : ertl_program → lbl_funct → regs_funct → option (list (register_env beval × (Σb:block.block_region b=Code))) → option (list (register_env beval × (Σb:block.block_region b=Code))) ≝ λprog,f_lbls,f_regs,frms. ! frames ← frms; sigma_frames_opt prog f_lbls f_regs frames. include "common/BitVectorTrieMap.ma". definition sigma_hw_register_env :ertl_program → lbl_funct → hw_register_env → hw_register_env ≝ λprog,f_lbls,h_reg.mk_hw_register_env (map ? ? (sigma_beval prog f_lbls) 6 (reg_env … h_reg)) (other_bit … h_reg). definition sigma_regs :ertl_program → lbl_funct → list register → (register_env beval)×hw_register_env→ (register_env beval)×hw_register_env ≝ λprog,f_lbls,ids,regs.let 〈x,y〉≝ regs in 〈sigma_register_env prog f_lbls ids x, sigma_hw_register_env prog f_lbls y〉. definition dummy_state : state ERTL_semantics ≝ mk_state ERTL_semantics (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 0 empty. definition sigma_state : ertl_program → lbl_funct → regs_funct → list register → state ERTLptr_semantics → state ERTL_semantics ≝ λprog,f_lbls,f_regs,restr,st. mk_state ERTL_semantics (sigma_frames prog f_lbls f_regs (st_frms ERTLptr_semantics st)) (sigma_is prog f_lbls (istack … st)) (carry … st) (sigma_regs prog f_lbls restr (regs … st)) (stack_usage … st) (sigma_mem prog f_lbls (m … st)). definition dummy_state_pc : state_pc ERTL_semantics ≝ mk_state_pc ? dummy_state (null_pc one) (null_pc one). definition sigma_state_pc : ertl_program → lbl_funct → regs_funct → state_pc ERTLptr_semantics → state_pc ERTL_semantics ≝ λprog,f_lbls,f_regs,st. let ge ≝ globalenv_noinit … prog in let globals ≝ prog_var_names … prog in match fetch_internal_function … ge (pc_block (pc … st)) with [ OK y ⇒ let 〈i,fn〉 ≝ y in let added ≝ added_registers ERTL globals fn (f_regs (pc_block (pc … st))) in mk_state_pc ? (sigma_state prog f_lbls f_regs added st) (pc … st) (sigma_stored_pc prog f_lbls (last_pop … st)) | Error e ⇒ dummy_state_pc ]. lemma ps_reg_retrieve_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀r,restr. preserving1 ?? res_preserve1 … (sigma_regs prog f_lbls restr) (sigma_beval prog f_lbls) (λregs.ps_reg_retrieve regs r) (λregs.ps_reg_retrieve regs r). #prog #f_lbls #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1 whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta >lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in >(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1 #bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec % qed. lemma hw_reg_retrieve_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀r,restr. preserving1 ?? res_preserve1 … (sigma_regs prog f_lbls restr) (sigma_beval prog f_lbls) (λregs.hw_reg_retrieve regs r) (λregs.hw_reg_retrieve regs r). #prog #f_lbls #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve; whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs; whd in match sigma_hw_register_env; normalize nodelta change with (sigma_beval prog f_lbls BVundef) in ⊢ (???????(??(?????%))?); #bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct %{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)} % // qed. lemma ps_reg_store_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀r,restr. ¬(r ∈ (set_from_list RegisterTag restr)) → preserving21 ?? res_preserve1 … (sigma_beval prog f_lbls) (sigma_regs prog f_lbls restr) (sigma_regs prog f_lbls restr) (ps_reg_store r) (ps_reg_store r). #prog #f_lbls #r #restr #Hreg whd in match ps_reg_store; normalize nodelta #bv * #psd_r #hw_r @mfr_return_eq1 whd in match reg_store; whd in match sigma_regs; normalize nodelta whd in match sigma_register_env; normalize nodelta >map_add >add_set_minus [% | assumption] qed. (* lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_ lapply x_spec -x_spec lapply EQpsd -EQpsd whd in match sigma_register_env; normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %] #id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) -H #x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % // | #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % // ] qed.*) lemma hw_reg_store_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀r,restr. preserving21 ?? res_preserve1 … (sigma_beval prog f_lbls) (sigma_regs prog f_lbls restr) (sigma_regs prog f_lbls restr) (hw_reg_store r) (hw_reg_store r). #prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta #bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs; normalize nodelta whd in match sigma_hw_register_env; normalize nodelta Hzlb * #H @⊥ @H %] #_ @andb_elim @if_elim [2: #_ *] #Hzleb #Hzlb' >Hzlb normalize nodelta >Hzlb' normalize nodelta @mfr_return_eq1 whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] * >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] * % qed. lemma bestorev_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct. ∀ptr. preserving21 … opt_preserve1 … (sigma_mem prog f_lbls) (sigma_beval prog f_lbls) (sigma_mem prog f_lbls) (λm.bestorev m ptr) (λm.bestorev m ptr). #prog #sigma #ptr #mem #bv whd in match bestorev; whd in match do_if_in_bounds; normalize nodelta @if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb @if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *] whd in match sigma_mem in ⊢ (% → % → ?); normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] * #Hzleb #Hzlb' normalize nodelta >Hzleb >Hzlb' normalize nodelta @mfr_return_eq1 whd in ⊢ (???%); @eq_f @mem_ext_eq [ #bl normalize nodelta % [%] [ whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match update_block; normalize nodelta @if_elim [ @eq_block_elim [2: #_ *] #EQbl * >EQbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta @if_elim [ #_ %] @eq_block_elim #_ * % | @eq_block_elim [#_ *] * #Hbl * @If_elim [ #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption | #Hzlb'' >Hzlb'' @If_elim [*] #_ % ] ] | whd in match update_block; whd in match sigma_mem; normalize nodelta @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_ @If_elim [3,4: >Hbl >Hzlb * [2: #H @⊥ @H %] @If_elim [2: * #H @⊥ @H %] * whd in match high_bound; normalize nodelta @if_elim [#_ %] @eq_block_elim [ #_ *] * #H @⊥ @H % | #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match high_bound; normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption | #Hzlb'' >Hzlb'' @If_elim [*] #_ % ] | #z whd in match update_block; whd in match sigma_mem; normalize nodelta @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_ [ @If_elim #Hzlb'' >Hzlb'' [2: @If_elim * #_ %] @If_elim @andb_elim @if_elim [2: #_ *] #Hzleb' #Hzlb''' [ @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta @If_elim @andb_elim @if_elim [2: #_ *] @if_elim [1,3,5: @eq_block_elim [2,4,6: #_ *] #H @⊥ @Hbl assumption] #_ >Hzleb' * whd in match high_bound; normalize nodelta @if_elim [1,3: @eq_block_elim [2,4: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb''' [ * %] * #H @⊥ @H % | @If_elim * [2: #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzleb' whd in match high_bound; normalize nodelta @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb''' @If_elim [2: #_ %] * | @If_elim [2: * #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ #_ whd in match low_bound in Hzleb'; normalize nodelta in Hzleb'; whd in match high_bound; normalize nodelta @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; * ] | whd in ⊢ (??%?); @if_elim @eqZb_elim [2,3: #_ * |4: *] #Hz * [ >Hzlb @If_elim [2: * #H @⊥ @H %] * @If_elim @andb_elim @if_elim [2: #_ *] #Hzleb' #Hzlb'' >Hbl >Hzlb @If_elim [2,4,6: * #H @⊥ @H %] #_ whd in match low_bound; normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound; normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %] #_ normalize nodelta [1,2: >Hzleb' >Hzlb'' @If_elim [2,3: * #H @⊥ @H %] #_ [2: %] whd in ⊢ (???(???%)); @if_elim [2: #_ %] @eqZb_elim [2: #_ *] #H @⊥ @Hz assumption | @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; * ] | >Hbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] normalize nodelta >Hz >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] #_ #_ whd in ⊢ (???(???%)); @eqZb_elim [2: * #H @⊥ @H %] #_ % ] ] ] | % ] qed. lemma sp_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀f_regs : regs_funct.∀restr. preserving1 … res_preserve1 … (λst.sigma_state prog f_lbls f_regs restr st) (λx.x) (sp ERTL_semantics) (sp ERTLptr_semantics). #prog #f_lbls #f_regs #restr #st whd in match sp; normalize nodelta whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state; normalize nodelta whd in match sigma_regs; normalize nodelta cases(regs ? st) #psd_r #hw_r normalize nodelta inversion(pointer_of_address ?) normalize nodelta [2: #e #_ @res_preserve_error1] #pt #EQ lapply(jmeq_to_eq ??? EQ) -EQ whd in match hwreg_retrieve; normalize nodelta whd in match sigma_hw_register_env; normalize nodelta change with (sigma_beval prog f_lbls BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?); >lookup_map >lookup_map cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef) [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1] whd in match pointer_of_address; whd in match pointer_of_bevals; normalize nodelta [1,2,3,4,5: #ABS destruct | cases(lookup beval 6 (bitvector_of_register RegisterSPH) (reg_env hw_r) BVundef) [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1'] whd in match sigma_beval; normalize nodelta [1,2,3,4,5: #ABS destruct | @if_elim [2: #_ #ABS destruct] #H whd in ⊢ (??%? → ?); #EQ destruct normalize nodelta @match_reg_elim #INUTILE [ @mfr_return_eq1 % | @res_preserve_error1 ] | cases (sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct ] | whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct ] qed. lemma set_sp_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀f_regs : regs_funct.∀restr.∀ptr,st. set_sp ? ptr (sigma_state prog f_lbls f_regs restr st) = sigma_state prog f_lbls f_regs restr (set_sp ? ptr st). #prog #f_lbls #f_regs #restr #ptr #st whd in match set_sp; whd in match sigma_state; normalize nodelta @eq_f3 try % whd in match (save_sp ???); whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f whd in match hwreg_store_sp; normalize nodelta whd in match sigma_hw_register_env; normalize nodelta whd in match hwreg_store; normalize nodelta @eq_f2 [2: %] >insert_map @eq_f >insert_map % qed. (*TO BE MOVED IN TranslateUtils.ma *) include "utilities/listb_extra.ma". lemma not_in_added_registers : ∀p : graph_params. ∀globals : list ident.∀fn,f_regs,r. (∀lbl. code_has_label p globals (joint_if_code … fn) lbl → ¬(bool_to_Prop (r ∈ (f_regs lbl)))) → ¬ (r ∈ (set_from_list RegisterTag (added_registers p globals fn f_regs))). #p #globals #fn #f_regs #r #H whd in match added_registers; normalize nodelta @foldi_ind [@I] #lbl #labels_fn #stmt #regs * #lbl_not_in_fn #EQstmt #IH lapply(Prop_notb … IH) -IH * #IH lapply(H lbl ?) [whd in match code_has_label; whd in match code_has_point; normalize nodelta whd in match (stmt_at ????); >EQstmt @I] * #H1 @notb_elim @if_elim [2: #_ @I] #ABS lapply(mem_list_as_set … ABS) #ABS' cases(Exists_append … ABS') #ABS'' [ @H1 @Exists_memb lapply ABS'' elim (f_regs lbl) [ *] #hd #tl #IH whd in ⊢ (% → %); * [ #EQ >EQ % %] #H %2 @IH @H | @IH @list_as_set_mem assumption ] qed. lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀a : A.In A l1 a → In A (l1@l2) a. #A #l1 elim l1 [#l2 #a *] #hd #tl #IH * [#a normalize * [#H % assumption | #H %2 >append_nil assumption]] #hd1 #tl1 #a normalize * [#H % assumption | #H %2 @IH assumption] qed. lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀a : A.In A l2 a → In A (l1@l2) a. #A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH * [#a normalize * [#H %1 assumption| #H %2 assumption]] #hd1 #tl1 #a normalize * [ #H %2 >append_cons @Exists_append1 >H elim tl1 [% %] #hd2 #tl2 #H1 normalize %2 // | #H %2 >append_cons @IH assumption] qed. lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A. All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2. #A #P #l1 elim l1 [ #l2 change with l2 in ⊢ (???% → ?); #H % //] #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?); * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % // qed. include alias "common/PositiveMap.ma". lemma added_register_pm : ∀A,B. ∀m : positive_map A. ∀f : Pos → list B.∀b. let added ≝ fold A (list B) (λp.λ_.λacc.(f p)@acc) m [ ] in All B (λx.x≠b) added → (∀i. lookup_opt unit i (domain_of_pm A m) ≠ None ? → All B (λx.x≠b) (f i)). #A #B #m #f #b normalize nodelta @pm_fold_ind [ #_ #i normalize * #H @⊥ @H % | #p #ps #a #lst #H #H1 #H2 #H3 #i cases(decidable_eq_pos i p) [1,3: #EQ destruct(EQ) #_ cases(append_All … H3) // |*: #Hi >lookup_opt_insert_miss [2,4: assumption] @H2 cases(append_All … H3) // ] ] qed. lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → decidable (In A l a). #A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC) [ #H % %2 assumption | * #H cases (DEC hd) [ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]] qed. lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l. #A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption] % #H1 @H % >H1 % qed. lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a. #A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % * [ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption] qed. lemma added_register_aux : ∀tag,A,B.∀m : identifier_map tag A. ∀f : identifier tag → list B.(∀b,b' : B.decidable (b=b')) → let added ≝ foldi A (list B) tag (λl.λ_.λacc. (f l)@acc) m [ ] in ∀i,a,b.lookup tag A m i = Some ? a → In B (f i) b → In B added b. #tag #A #B * #m #f #DEC * #i #a #b whd in ⊢ (??%? → ?); normalize nodelta #H #H1 cases(decidable_In ? (foldi A (list B) tag (λl.λ_.λacc.(f l)@acc) (an_id_map tag A m) []) b (DEC b)) [//] #H3 @⊥ lapply(In_all ??? H3) -H3 #H3 lapply(added_register_pm ?? m ?? H3 i ?) [cases(domain_of_pm_present ? m i) #H4 #_ @H4 >H % #EQ destruct] lapply H1 elim (f ?) [*] #hd #tl #IH * [#EQ * >EQ * #H4 #_ @H4 %] #H4 * #_ @IH assumption qed. lemma in_added_registers : ∀p : graph_params. ∀globals : list ident.∀fn,f_regs,r. ∀lbl.code_has_label p globals (joint_if_code … fn) lbl → In ? (f_regs lbl) r → In ? (added_registers p globals fn f_regs) r. #p #globals #fn #f_regs #r #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta whd in match (stmt_at ????); inversion(lookup LabelTag ???) [ #_ *] #stmt #EQstmt #_ #H @(added_register_aux … EQstmt H) * #p * #p' cases(decidable_eq_pos p p') [ #EQ destruct % % | * #H1 %2 % #EQ destruct @H1 %] qed. include alias "basics/lists/listb.ma". (* definition get_internal_function_from_ident : ∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals). ident → option (joint_closed_internal_function p globals) ≝ λp,globals,ge,id. ! bl ← (find_symbol (joint_function p globals) ge id); ! bl' ← (code_block_of_block bl); ! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl'); return fn. lemma get_internal_function_from_ident_ok : ∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals). ∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 → get_internal_function_from_ident p globals ge f= return fn. #p #globals #ge #bl #f #fn #EQf @('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function; normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta >(symbol_of_block_rev … EQf2) >m_return_bind cut(code_block_of_block bl = return bl) [ whd in match code_block_of_block; normalize nodelta @match_reg_elim [ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl >m_return_bind >EQf % qed. *) lemma eval_seq_no_pc_no_call_ok : ∀prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀f_lbls : lbl_funct. ∀f_regs : regs_funct. ∀stack_size. ∀bl.∀id. ∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).∀seq. (∀l. code_has_label … (joint_if_code … fn) l → (All … (λreg.bool_to_Prop(¬(reg ∈ (f_regs bl l)))) (get_used_registers_from_seq … (functs … ERTL) seq))) → preserving1 ?? res_preserve1 ???? (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl))) (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl))) (eval_seq_no_pc ERTL_semantics (globals (mk_prog_params ERTL_semantics prog stack_size)) (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id seq) (eval_seq_no_pc ERTLptr_semantics (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size)) (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (seq_embed … seq)). #prog #f_lbls #f_regs #stack_size #bl #f #fn #seq #fresh_regs cases seq in fresh_regs; [ #c #_ #st @mfr_return1 | #pm #fesh_regs #st whd in match pair_reg_move; normalize nodelta @mfr_bind1 [ 2: change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok whd in match move_dst_not_fresh; normalize nodelta cases pm in fesh_regs; * [#r1 | #R1] #m_src [2: #_ @I] normalize nodelta #fresh_regs @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] | #r #fresh_regs #st @mfr_bind1 [2: @pop_ok | | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1 [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H ] ] | #r #_ #st @mfr_bind1 [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok | | #bv @push_ok ] | #i #i_spec change with ((dpl_reg ERTL) → ?) #dpl change with ((dph_reg ERTL) → ?) #dph #fresh_regs #st @mfr_bind1 [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl))) | whd in match dpl_store; normalize nodelta @mfr_bind1 [2: @opt_safe_elim #bl #EQbl @opt_safe_elim #bl' >(find_symbol_transf … (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog i) in ⊢ (%→?); >EQbl #EQ destruct whd in match sigma_state; normalize nodelta change with (sigma_beval prog f_lbls (BVptr …)) in ⊢ (???????(?????%?)?); @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl' >(find_symbol_transf … (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog i) in ⊢ (%→?); >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1 [2: whd in match sigma_state; normalize nodelta change with (sigma_beval prog f_lbls (BVptr …)) in ⊢ (???????(?????%?)?); @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] ] | #op #a #b #arg1 #arg2 #fresh_regs #st @mfr_bind1 [2: whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta @ps_arg_retrieve_ok | | #bv1 @mfr_bind1 [2: whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta @ps_arg_retrieve_ok | | #bv2 @mfr_bind1 [2: @be_opaccs_ok | | * #bv3 #bv4 normalize nodelta @mfr_bind1 [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl))) | whd in match acca_store; normalize nodelta @mfr_bind1 [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] | #st1 whd in match accb_store; normalize nodelta @mfr_bind1 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] ] ] ] ] | #op #r1 #r2 #fresh_regs #st @mfr_bind1 [ @(sigma_beval prog f_lbls) | whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok | #bv1 @mfr_bind1 [ @(sigma_beval prog f_lbls) | @be_op1_ok | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] ] ] | #op2 #r1 #r2 #arg #fresh_regs #st @mfr_bind1 [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok | | #bv @mfr_bind1 [2: whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok | | #bv1 @mfr_bind1 [2: @be_op2_ok | | * #bv2 #b @mfr_bind1 [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl))) | whd in match acca_store; normalize nodelta @mfr_bind1 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] | #st1 @mfr_return_eq1 % ] ] ] ] | #_ #st @mfr_return_eq1 % | #_ #st @mfr_return_eq1 % | #r1 #dpl #dph #fresh_regs #st @mfr_bind1 [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok | | #bv @mfr_bind1 [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok | | #bv1 @mfr_bind1 [ @(λx.x) | @(pointer_of_address_ok ? ? 〈bv1,bv〉) | #ptr @mfr_bind1 [2: @opt_to_res_preserve1 @beloadv_ok | | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] ] ] ] ] | #dpl #dph #r #_ #st @mfr_bind1 [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok | | #bv @mfr_bind1 [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok | | #bv1 @mfr_bind1 [ @(λx.x) | @(pointer_of_address_ok ? ? 〈bv1,bv〉) | #ptr @mfr_bind1 [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok | | #bv2 @mfr_bind1 [2: @opt_to_res_preserve1 @bestorev_ok | | #m @mfr_return_eq1 % ] ] ] ] ] | #ext #fresh_regs #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f) normalize nodelta [ @res_preserve_error1 | #n cases ext in fresh_regs; normalize nodelta [1,2: #_ @mfr_bind1 [1,4: @(λx.x) |2,5: @sp_ok |3,6: #ptr @mfr_return_eq1 >set_sp_ok % ] | #r #fresh_regs whd in match ps_reg_store_status; normalize nodelta @mfr_bind1 [2: whd in match sigma_state; normalize nodelta change with (sigma_beval prog f_lbls (BVByte ?)) in ⊢ (???????(??%?)?); @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H | | #regs @mfr_return_eq1 % ] ] ] ] #regs @mfr_return_eq1 % qed. lemma partial_inj_sigma : ∀ prog : ertl_program. ∀f_lbls : lbl_funct. let sigma ≝ get_sigma prog f_lbls in ∀id,lbl1,lbl2. sigma id lbl1 ≠ None ? → sigma id lbl1 = sigma id lbl2 → lbl1 = lbl2. #prog #good #bl #lbl1 #lbl2 inversion(get_sigma … lbl1) [#_ * #H @⊥ @H %] #lbl1' whd in match get_sigma; normalize nodelta #H @('bind_inversion H) -H #bl' whd in match code_block_of_block; normalize nodelta @match_reg_elim [#_ #ABS destruct] #prf #EQ destruct #H @('bind_inversion H) -H * #id #fn #H lapply(res_eq_from_opt ??? H) -H #EQfn #H @('bind_inversion H) -H * #lbl1'' #stmt1 #H1 whd in ⊢ (??%? → ?); #EQ destruct #_ #H lapply(sym_eq ??? H) -H >m_return_bind >EQfn >m_return_bind #H @('bind_inversion H) -H * #lbl2' #stmt2 #H2 whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta [ normalize nodelta @eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 * >EQ1 >EQ2 % | #lb #tl whd in match split_on_last; normalize nodelta whd in match (foldr ?????); cases( foldr label (option (list label×label)) … tl) normalize nodelta [2: * #x #lb1] @eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 * >EQ1 >EQ2 % ] qed. (*TO BE MOVED : GENERAL!!!*) lemma pc_of_label_eq : ∀p,p'.let pars ≝ mk_sem_graph_params p p' in ∀globals,ge,bl,i_fn,lbl. fetch_internal_function ? ge bl = return i_fn → pc_of_label pars globals ge bl lbl = OK ? (pc_of_point ERTL_semantics bl lbl). #p #p' #globals #ge #bl #i_fn #lbl #EQf whd in match pc_of_label; normalize nodelta >EQf >m_return_bind % qed. lemma pop_ra_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀f_regs : regs_funct. ∀restr. preserving1 … res_preserve1 … (sigma_state prog f_lbls f_regs restr) (λx.let 〈st,pc〉 ≝ x in 〈sigma_state prog f_lbls f_regs restr st, sigma_stored_pc prog f_lbls pc〉) (pop_ra ERTL_semantics) (pop_ra ERTLptr_semantics). cases daemon (*TODO*) qed. (* #prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta @mfr_bind1 [ | @pop_ok ] * #bv #st1 @mfr_bind1 [ | @pop_ok] * #bv1 #st2 @mfr_bind1 [ @(sigma_stored_pc prog f_lbls) | whd in match pc_of_bevals; normalize nodelta cases bv [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p] whd in match sigma_beval; normalize nodelta try @res_preserve_error1 inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1] #sigma_pc #sigma_pc_spec normalize nodelta cases bv1 [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1] normalize nodelta try @res_preserve_error1 inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1] #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1] @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *] #_ #H >H @eq_program_counter_elim [2: #_ *] #EQspc * @eq_program_counter_elim [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; H2 in H3; * | #H2 @if_elim [ #H3 #H @('bind_inversion H) -H #x1 #_ whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct >H3 in H2; * | #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) -EQ * #x cases pc1 #bl1 #pos1 whd in match (point_of_pc ??); #x_spec whd in match (pc_of_point ???); whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct #H @('bind_inversion H) -H * #lbl cases pc #bl #pos whd in match (point_of_pc ??); #lbl_spec whd in match pc_of_point; normalize nodelta whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct @eq_f cut(an_identifier LabelTag pos = an_identifier LabelTag pos1 → pos = pos1) [ #EQ destruct %] #APP @APP @(partial_inj_sigma prog f_lbls bl1 …) [ >lbl_spec % #EQ destruct] >x_spec >lbl_spec % ] ] | #pc @mfr_return_eq1 % ] qed.*) lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc. sigma_pc_opt prog f_lbls pc ≠ None ? → pc_block … pc = pc_block … (sigma_stored_pc prog f_lbls pc). #prog #sigma * #bl #pos whd in match sigma_stored_pc; normalize nodelta inversion(sigma_pc_opt ???) [ #_ * #H @⊥ @H %] #pc whd in match sigma_pc_opt; normalize nodelta @if_elim [#_ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #_ #H @('bind_inversion H) -H * #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ % qed. include "joint/extra_joint_semantics.ma". lemma pop_frame_ok : ∀prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀f_lbls : lbl_funct. ∀f_regs : regs_funct. ∀restr. preserving1 ?? res_preserve1 ???? (sigma_state prog f_lbls f_regs restr) (λx.let 〈st,pc〉 ≝ x in match fetch_internal_function ? (globalenv_noinit … prog) (pc_block pc) with [ OK y ⇒ let 〈id,f〉 ≝ y in 〈sigma_state prog f_lbls f_regs (added_registers ERTL (prog_var_names … prog) f (f_regs (pc_block pc))) st, sigma_stored_pc prog f_lbls pc〉 | Error e ⇒ 〈dummy_state,null_pc one〉 ]) (ertl_pop_frame) (ertl_pop_frame). #prog #f_lbls #f_regs #restr #st whd in match ertl_pop_frame; normalize nodelta @mfr_bind1 [ @(λx.match sigma_frames_opt prog f_lbls f_regs x with [Some l ⇒ l | None ⇒ [ ]]) | @opt_to_res_preserve1 whd in match sigma_state; normalize nodelta cases(st_frms … st) [@opt_preserve_none1] #l whd in match sigma_frames; normalize nodelta >m_return_bind #x #x_spec %{l} % [%] >x_spec % | * normalize nodelta [@res_preserve_error1] * #loc_mem #bl #tl normalize nodelta inversion(sigma_frames_opt ????) normalize nodelta [ #_ @res_preserve_error1] #l whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta whd in match (foldr ?????); normalize nodelta inversion(fetch_internal_function ???) normalize nodelta [2: #e #_ #ABS destruct(ABS)] * #f #fn #EQfn #H @('bind_inversion H) -H #l1 change with (sigma_frames_opt prog f_lbls f_regs tl = ? → ?) #EQl1 whd in ⊢ (??%? → ?); #EQ destruct(EQ) @mfr_bind1 [2: whd in match sigma_state; whd in match set_regs; whd in match set_frms; normalize nodelta cut( 〈sigma_register_env prog f_lbls (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn (f_regs bl)) loc_mem, \snd  (sigma_regs prog f_lbls restr (regs ERTLptr_semantics st))〉 = sigma_regs prog f_lbls (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn (f_regs bl)) (〈loc_mem,\snd  (regs ERTL_state st)〉)) [ whd in match sigma_regs; normalize nodelta cases(regs … st) #x1 #x2 %] #EQ >EQ -EQ EQbl1 @eq_block_elim [#_ *] * #H @⊥ @H fetch_internal_function_no_zero [2: %] #EQ destruct | @eq_block_elim [2: #_ *] #EQbl11 * @mfr_return_eq1 normalize nodelta cases bl in EQbl11 EQfn; #p1 #p2 #EQ destruct lapply p2 cases(pc_block pc1) #p11 #p22 #e #EQfn1 >EQfn1 % ] ] ] qed. lemma fetch_ok_sigma_pc_ok :∀prog : ertl_program. ∀ f_lbls,f_regs,id,fn,st. fetch_internal_function … (globalenv_noinit … prog) (pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 → pc … (sigma_state_pc prog f_lbls f_regs st) = pc … st. #prog #f_lbls #f_regs #id #fn #st whd in match sigma_state_pc; normalize nodelta cases(fetch_internal_function ?? (pc_block (pc … st))) normalize nodelta [* #id1 #fn1 #_ %] #e >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ) qed. lemma fetch_ok_sigma_state_ok : ∀prog : ertl_program. ∀ f_lbls,f_regs,id,fn,st. fetch_internal_function … (globalenv_noinit … prog) (pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 → let added ≝ (added_registers ERTL (prog_var_names … prog) fn (f_regs (pc_block (pc … st)))) in st_no_pc … (sigma_state_pc prog f_lbls f_regs st) = sigma_state prog f_lbls f_regs added (st_no_pc … st). #prog #f_lbls #f_regs #id #fn #st #EQf whd in match sigma_state_pc; normalize nodelta <(fetch_ok_sigma_pc_ok … EQf) >EQf % qed. lemma fetch_ok_sigma_pc_block_ok : ∀prog : ertl_program. ∀ f_lbls,id,fn,pc. fetch_internal_function … (globalenv_noinit … prog) (pc_block (sigma_stored_pc prog f_lbls pc)) = return 〈id,fn〉 → pc_block (sigma_stored_pc prog f_lbls pc) = pc_block pc. #prog #f_lbls #id #fn #pc #EQf fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ) qed. lemma fetch_stmt_ok_sigma_pc_ok : ∀prog : ertl_program. ∀ f_lbls,f_regs,id,fn,stmt,st. fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) = return 〈id,fn,stmt〉 → pc … (sigma_state_pc prog f_lbls f_regs st) = pc … st. #prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) * #id1 #fn1 #EQfn1 #_ @(fetch_ok_sigma_pc_ok … EQfn1) qed. lemma fetch_stmt_ok_sigma_state_ok : ∀prog : ertl_program. ∀ f_lbls,f_regs,id,fn,stmt,st. fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) = return 〈id,fn,stmt〉 → let added ≝ (added_registers ERTL (prog_var_names … prog) fn (f_regs (pc_block (pc … st)))) in st_no_pc … (sigma_state_pc prog f_lbls f_regs st) = sigma_state prog f_lbls f_regs added (st_no_pc … st). #prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) -H * #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_state_ok … EQfn1) qed. lemma fetch_stmt_ok_sigma_pc_block_ok : ∀prog : ertl_program. ∀ f_lbls,id,fn,stmt,pc. fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) (sigma_stored_pc prog f_lbls pc) = return 〈id,fn,stmt〉 → pc_block (sigma_stored_pc prog f_lbls pc) = pc_block pc. #prog #f_lbls #id #fn #stmt #st #H @('bind_inversion H) -H * #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_pc_block_ok … EQfn1) qed. lemma fetch_ok_sigma_last_pop_ok :∀prog : ertl_program. ∀ f_lbls,f_regs,id,fn,st. fetch_internal_function … (globalenv_noinit … prog) (pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 → last_pop … (sigma_state_pc prog f_lbls f_regs st) = sigma_stored_pc prog f_lbls (last_pop … st). #prog #f_lbls #f_regs #id #fn #st whd in match sigma_state_pc; normalize nodelta cases(fetch_internal_function ?? (pc_block (pc … st))) normalize nodelta [ * #x #y #_ %] #e >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ) qed. lemma fetch_stmt_ok_sigma_last_pop_ok :∀prog : ertl_program. ∀ f_lbls,f_regs,id,fn,stmt,st. fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) = return 〈id,fn,stmt〉 → last_pop … (sigma_state_pc prog f_lbls f_regs st) = sigma_stored_pc prog f_lbls (last_pop … st). #prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) -H * #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_last_pop_ok … EQfn1) qed. lemma excluded_middle_list : ∀A : Type[0]. ∀P : A → Prop.∀ l : list A. (∀a : A.In A l a → decidable … (P a)) → All … P l ∨ Exists … (λa.¬(P a)) l. #A #P #l elim l [#_ % %] #hd #tl #IH #Dec cases IH [ cases(Dec hd ?) [ #H1 #H2 % whd % assumption | #H #_ %2 whd % assumption | % % ] | #H %2 whd %2 assumption | #a #H @Dec %2 assumption ] qed. 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. lemma split_on_last_append : ∀A : Type[0]. ∀pre : list A. ∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉. #A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last) whd in ⊢ (??%? → ?); #EQ >EQ % qed. include alias "common/Identifiers.ma". lemma get_sigma_idempotent : ∀prog : ertl_program. ∀ f_lbls,f_regs. ∀f_bl_r. b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → ∀id,fn,bl,pt,stmt. fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 → stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → f_lbls bl pt = [ ] → get_sigma prog f_lbls bl pt = return pt. #prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #EQfn #EQstmt #EQlabels cases(b_graph_transform_program_fetch_internal_function … good … EQfn) #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_ #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H cases stmt in EQstmt; [3: * |2: * [#lbl || *] #EQstmt normalize nodelta * #bl * whd in ⊢ (% → ?); inversion (f_regs ??) [2,4: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (%→?); * #pref * #mid ** #EQmid whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); #EQt_stmt | * [#c | * [#c_id|#c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt whd in ⊢ (% → ?); * #bl >if_merge_right [2,4,6,8,10: %] * whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [2,4,5,8,10: [1,2,4,5: #x #y] #_ [1,2,3,4: #_] *|6: #r * [2: #x #y] ] [1,2: #_] #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (%→ ?); [ * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%); >EQlabels in e0; #e0 destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%); destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #_ #EQ destruct(EQ) ] whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????) [1,3,5,7,9,11: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels normalize nodelta @eq_identifier_elim [1,3,5,7,9,11: #_ * |*: * #H #_ @H %]] * #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind) inversion(f_lbls ??) [1,3,5,7,9,11: #_ normalize nodelta @eq_identifier_elim [2,4,6,8,10,12: #_ *] #EQ #_ >EQ %] #lb #l @(list_elim_left … l …) normalize nodelta [1,3,5,7,9,11: #_ #EQlb @eq_identifier_elim [1,3,5,7,9,11: #EQ destruct(EQ) #_ @⊥ |*: #_ *] lapply(fresh_labs lbl) >EQlb *** #H #_ #_ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; whd in match code_has_point; normalize nodelta >EQstmt @I ] #last #pre #_ #_ #EQlbl >(split_on_last_append … (lb::pre) last) normalize nodelta @eq_identifier_elim [2,4,6,8,10,12: #_ *] #EQ lapply EQlbl destruct(EQ) #EQlbl #_ @⊥ lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); * #_ #H lapply(append_All … H) -H * #_ whd in ⊢ (% → ?); *** #H #_ #_ @H -H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; whd in match code_has_point; normalize nodelta >EQstmt @I qed. lemma append_absurd : ∀A : Type[0]. ∀l : list A. ∀ a : A. l @ [a] = [ ] → False. #A * [2: #x #y] #a normalize #EQ destruct qed. lemma last_append_eq : ∀A : Type[0].∀l1,l2 : list A. ∀a1,a2: A. l1 @ [a1] = l2 @ [a2] → a1 = a2. #A #l1 elim l1 [ * [2: #hd #tl] #a1 #a2 normalize #EQ destruct [2: %] @⊥ lapply(sym_eq ??? e0) -e0 #e0 @(append_absurd ??? e0)] #hd #tl #IH * [ #a1 #a2 normalize #EQ destruct @⊥ @(append_absurd ??? e0)] #hd1 #tl1 #a1 #a2 normalize #EQ destruct(EQ) @(IH tl1 a1 a2 e0) qed. lemma get_sigma_last : ∀prog : ertl_program. ∀ f_lbls,f_regs. ∀f_bl_r. b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → ∀id,fn,bl,pt,stmt,pre,last. fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 → stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → f_lbls bl pt = pre@[last] → get_sigma prog f_lbls bl last = return pt. #prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #pre #last #EQfn #EQstmt #EQlabels cases(b_graph_transform_program_fetch_internal_function … good … EQfn) #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H normalize nodelta cases stmt in EQstmt; normalize nodelta [3: * |2: * [#lbl || *] #EQstmt whd in ⊢ (%→ ?); * #bl * |*: * [#c | * [ #c_id | #c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt >if_merge_right [2,4,6,8,10: %] whd in ⊢ (% → ?); * #bl * ] whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y #_] #_ *|10: #r #tl #_] #EQregs [ whd in ⊢ (% → ?); cases tl in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs] #EQbl destruct(EQbl) whd in ⊢ (%→?); [2,3: * #pref * #mid **|*: * #l1 * #mid1 * #mid2 * #l2 ***] #EQmid1 whd in ⊢ (% → ?); [1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) [3,4,5,6: whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt #EQ destruct(EQ) ] whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ >EQlabels in e0; #e0 @(append_absurd ??? e0)] * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #mid4 * #rest2 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #mid5 * #rest3 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQcall change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) >e0 in EQlabels; #EQlabels whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????) [ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >e0 normalize nodelta @eq_identifier_elim [ #_ *] * #H #_ @H >(last_append_eq ????? EQlabels) % ] * #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind) inversion(f_lbls ??) [ #EQlbl normalize nodelta @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ) @⊥ lapply(fresh_labs pt) >e0 * #_ * #_ * #_ *** #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 ] #lb #labels #_ @(list_elim_left … (labels) …) -labels normalize nodelta [2: #last1 #pre #_] #EQl [ >(split_on_last_append … (lb::pre) last1) ] normalize nodelta @eq_identifier_elim [2,4: #_ *] #EQ destruct(EQ) #_ lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ) lapply pp_labs whd in match partial_partition; normalize nodelta * #_ #H lapply(H lbl pt) >e0 whd in EQmid : (??%%); >EQl #H [ >(H last1 ? ?) | >(H lb ? ?) ] [1,4: % |6: whd in match (memb ???); @if_elim [#_ @I] #H lapply(Prop_notb ? H) * -H #H @⊥ @H cases lb #x normalize @if_elim [#_ %] #H lapply(Prop_notb ? H) * -H #H @H >(eqb_n_n x) % |5: >(memb_append_l2 ? lb ? [lb] ?) /2 by / |*: >(memb_append_l2 ? last1 ? [last1] ?) /2 by / @Exists_memb %2 elim pre [ % % | #hd #tl #IH %2 @IH] ] qed. lemma fetch_call_commute : ∀prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs. ∀f_bl_r. b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → ∀id,fn,c_id,c_args,c_dest,nxt,pc. fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) pc = return 〈id,fn, sequential ? ?(CALL ERTL_semantics ? c_id c_args c_dest) nxt〉 → ∃fn',pc'. sigma_stored_pc prog f_lbls pc' = pc ∧ fetch_statement ERTLptr_semantics (prog_var_names … trans_prog) (globalenv_noinit … trans_prog) pc' = return 〈id,fn', sequential ? ?(CALL ERTLptr_semantics ? c_id c_args c_dest) nxt〉. #prog #f_lbls #f_regs #f_bl_r #good #id #fn * [ #c_id | #c_ptr ] #c_args #c_dest #nxt #pc #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt cases(b_graph_transform_program_fetch_internal_function … good … EQfn) #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #H cases(H … EQstmt) -H #bl whd in ⊢ (% → ?); * >if_merge_right [2,4: %] whd in match translate_step; normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [|2,3:[ #x #y #_] #_ * |4: #r #tl #_ ] #EQregs [ | cases tl in EQregs; [2: #x #y #_ *] #EQregs whd in ⊢ (% → ?);] #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?); [2: * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 * #EQpush1 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #mid4 * #rest2 ** #EQ destruct(EQ) * #nxt1 * #EQhigh change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #mid5 * #rest3 ** #EQ destruct(EQ) * #nxt1 * #EQpush2 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQcall #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ destruct(EQ) change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) %{calling'} [ %{(pc_of_point ERTLptr_semantics (pc_block pc) mid1)} | %{pc} ] % [1,3: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta @eqZb_elim change with (pc_block pc) in match (pc_block ?) in ⊢ (% → ?); [1,3: #EQbl >fetch_internal_function_no_minus_one in EQfn; try assumption #EQ destruct(EQ)] #_ normalize nodelta [2: >(get_sigma_idempotent … good … EQfn EQstmt EQ) |*: change with (pc_block pc) in match (pc_block ?); >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt e0) ] >m_return_bind normalize nodelta >pc_of_point_of_pc % |*: whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind [>point_of_pc_of_point ] >EQcall % ] qed. lemma next_of_call_pc_ok : ∀prog : ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs.∀f_bl_r. b_graph_transform_program_props ERTL_semantics ERTLptr_semantics (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → ∀pc,lb. next_of_call_pc ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) pc = return lb → ∃pc'. sigma_stored_pc prog f_lbls pc' = pc ∧ next_of_call_pc ERTLptr_semantics (prog_var_names … trans_prog) (globalenv_noinit … trans_prog) pc' = return lb. #prog #f_lbls #f_regs #f_bl_r #good #pc #lb whd in match next_of_call_pc; normalize nodelta #H @('bind_inversion H) -H ** #id #fn * [ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | *] #EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(fetch_call_commute … good … EQfetch) #fn1 * #pc1 * #EQpc1 #EQt_fetch %{pc1} % [assumption] >EQt_fetch % qed. lemma next_of_call_pc_error : ∀pars.∀prog : program ? ℕ. ∀init,pc. (block_id (pi1 … (pc_block pc)) = 0 ∨ block_id (pi1 … (pc_block pc)) = -1) → next_of_call_pc pars (prog_var_names … prog) (globalenv … init prog) pc = Error ? [MSG BadFunction]. #pars #prg #init #pc * #EQ whd in match next_of_call_pc; normalize nodelta whd in match fetch_statement; normalize nodelta [ >fetch_internal_function_no_zero | >fetch_internal_function_no_minus_one] // qed. lemma next_of_call_pc_inv : ∀pars.∀prog : program ? ℕ. ∀init. ∀pc,nxt. next_of_call_pc pars (prog_var_names … prog) (globalenv … init prog) pc = return nxt → ∃id,fn,c_id,c_args,c_dest. fetch_statement pars (prog_var_names … prog) (globalenv … init prog) pc = return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉. #pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta #H @('bind_inversion H) -H ** #id #fn * [ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | #H #r #l #l ] #EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption qed. lemma sigma_stored_pc_inj : ∀ prog : ertl_program. ∀f_lbls,pc,pc'. sigma_pc_opt prog f_lbls pc ≠ None ? → sigma_pc_opt prog f_lbls pc = sigma_pc_opt prog f_lbls pc' → pc = pc'. #prog #f_lbls ** #id #EQblid #off ** #id' #EQblid' #off' * inversion(sigma_pc_opt ???) [#_ #H @⊥ @H %] #pc1 whd in match sigma_pc_opt; normalize nodelta @if_elim [ @eqZb_elim [2: #_ *] #EQbl * whd in ⊢ (??%? → ?); #EQ destruct #_ #H lapply(sym_eq ??? H) -H @if_elim [#_ whd in ⊢ (??%? → ?); #EQ destruct %] @eqZb_elim [ #_ *] * #EQbl' #_ #H @('bind_inversion H) -H #lb #EQlb whd in ⊢ (??%? → ?); #EQ destruct @⊥ @EQbl' assumption] @eqZb_elim [#_ *] * #EQbl #_ #H @('bind_inversion H) -H * #lb #EQlb whd in ⊢ (??%? → ?); #EQ destruct #_ #H lapply(sym_eq ??? H) -H @if_elim [ @eqZb_elim [2: #_ *] #EQbl' #_ whd in ⊢ (??%? → ?); #EQ destruct @⊥ @EQbl @EQbl'] #_ #H @('bind_inversion H) -H * #lb' #EQlb' whd in ⊢ (??%? → ?); whd in match (pc_of_point ???); whd in match (offset_of_point ??); whd in match (offset_of_point ??); #EQ destruct @eq_f cut(an_identifier LabelTag off = an_identifier LabelTag off') [2: #EQ destruct %] @(partial_inj_sigma prog f_lbls id) [>EQlb % #ABS destruct | >EQlb >EQlb' %] qed. lemma bool_of_beval_ok : ∀prog : ertl_program. ∀f_lbls. preserving1 … res_preserve1 … (sigma_beval prog f_lbls) (λx.x) (bool_of_beval) (bool_of_beval). #prog #f_lbls * [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1] whd in match bool_of_beval; normalize nodelta try @res_preserve_error1 try @mfr_return1 whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ???) normalize nodelta [2: #pc] @res_preserve_error1 qed. lemma block_of_call_ok : ∀prog: ertl_program. let trans_prog ≝ ertl_to_ertlptr prog in ∀ f_lbls,f_regs. ∀called,restr. preserving1 … res_preserve1 … (sigma_state prog f_lbls f_regs restr) (λx.x) (block_of_call ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) called) (block_of_call ERTLptr_semantics (prog_var_names … trans_prog) (globalenv_noinit … trans_prog) called). #prog #f_lbls #f_regs #called #restr #st whd in match block_of_call; normalize nodelta @mfr_bind1 [ @(λx.x) | cases(called) [#c_id | #c_ptr] normalize nodelta [ @opt_to_res_preserve1 #bl #EQbl %{bl} % [2: %] >(find_symbol_transf … (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog c_id) assumption | @mfr_bind1 [2: whd in match dpl_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) | | #bv1 @mfr_bind1 [2: whd in match dph_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) | | #bv2 @mfr_bind1 [ @(λx.x) | whd in match pointer_of_bevals; normalize nodelta cases bv1 normalize nodelta [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1] try @res_preserve_error1 [ cases bv2 [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1'] normalize nodelta [1,2,3,4,5: @res_preserve_error1 | @if_elim #_ [@mfr_return_eq1 % | @res_preserve_error1] ] ] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???) normalize nodelta [2,4: #pc ] @res_preserve_error1 | #ptr @if_elim #_ [@mfr_return_eq1 % | @res_preserve_error1] ] ] ] ] | #bl @opt_to_res_preserve1 whd in match code_block_of_block; normalize nodelta @match_reg_elim [ #_ @opt_preserve_none1 | #prf @mfr_return_eq1 %] ] qed. lemma bvpc_sigma_pc_to_sigma_beval : ∀prog : ertl_program. ∀f_lbls,pc,p. sigma_pc_opt prog f_lbls pc ≠ None ? → BVpc (sigma_stored_pc prog f_lbls pc) p = sigma_beval prog f_lbls (BVpc pc p). #prog #f_lbls #pc #p #prf whd in match sigma_stored_pc; whd in match sigma_beval; normalize nodelta lapply prf cases(sigma_pc_opt ???) [ * #H @⊥ @H % | #pc' #_ % ] qed. lemma push_ra_ok : ∀prog : ertl_program. ∀f_lbls,f_regs,restr,pc. sigma_pc_opt prog f_lbls pc ≠ None ? → preserving1 ?? res_preserve1 … (sigma_state prog f_lbls f_regs restr) (sigma_state prog f_lbls f_regs restr) (λst.push_ra ERTL_semantics st (sigma_stored_pc prog f_lbls pc)) (λst.push_ra ERTLptr_semantics st pc). #prog #f_lbls #f_regs #restr #pc #prf #st whd in match push_ra; normalize nodelta @mfr_bind1 [ @(sigma_state prog f_lbls f_regs restr) | >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok | #st' >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok ] qed. lemma ertl_save_frame_ok : ∀prog : ertl_program. ∀f_lbls.∀f_regs : regs_funct.∀kind,restr. preserving1 ?? res_preserve1 ???? (λst : Σs: state_pc ERTLptr_semantics. sigma_pc_opt prog f_lbls (pc … s) ≠ None ? . match fetch_internal_function … (globalenv_noinit … prog) (pc_block (pc … st)) with [ OK y ⇒ let 〈f,fn〉 ≝ y in let added ≝ added_registers … (prog_var_names … prog) fn (f_regs (pc_block (pc … st))) in mk_state_pc ? (sigma_state prog f_lbls f_regs added st) (sigma_stored_pc prog f_lbls (pc … st)) (sigma_stored_pc prog f_lbls (last_pop … st)) | Error e ⇒ dummy_state_pc ]) (sigma_state prog f_lbls f_regs restr) (ertl_save_frame kind it) (match kind with [ID ⇒ ertlptr_save_frame kind it |PTR ⇒ λst. !st' ← push_ra … st (pc … st); ertlptr_save_frame kind it (set_no_pc … st' st) ]). #prog #f_lbls #f_regs * #restr * #st #st_prf inversion(fetch_internal_function ???) normalize nodelta [1,3: * #f #fn #EQfn normalize nodelta whd in match ertl_save_frame; whd in match ertlptr_save_frame; normalize nodelta @mfr_bind1 [2,5: @push_ra_ok [1,2: assumption] |1,4: skip |*: #st1 [ >m_return_bind] @mfr_bind_inversion1 [1,4: @(λf.match sigma_frames_opt prog f_lbls f_regs f with [Some g ⇒ g | None ⇒ [ ]]) |2,5: @opt_to_res_preserve1 whd in match sigma_state; whd in match set_no_pc; normalize nodelta cases(st_frms … st1) [1,3: @opt_preserve_none1] #frames #frames1 whd in match sigma_frames; normalize nodelta >m_return_bind #EQframes %{frames} % [%] >EQframes % |*: #frames #H lapply(opt_eq_from_res ???? H) -H whd in match sigma_state; normalize nodelta #EQt_frames #H lapply(opt_eq_from_res ???? H) -H whd in match set_no_pc; normalize nodelta #EQframes >EQframes in EQt_frames; whd in match sigma_frames; normalize nodelta >m_return_bind inversion(sigma_frames_opt ???) [1,3: #_ #ABS destruct(ABS)] #t_frames #EQt_frames #_ @mfr_return_eq1 normalize nodelta @eq_f whd in match set_frms; normalize nodelta >m_return_bind cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2,f1,f2. a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 → f1 = f2 → mk_state ERTL_semantics a1 b1 c1 d1 e1 f1 = mk_state ERTL_semantics a2 b2 c2 d2 e2 f2) [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 //] #APP @APP try % [1,3: whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta whd in match (foldr ?????); normalize nodelta >EQfn >m_return_bind normalize nodelta change with (sigma_frames_opt prog f_lbls f_regs frames) in match (foldr ?????); >EQt_frames >m_return_bind whd in match sigma_regs; normalize nodelta cases(regs … st1) #ps_reg #hw_reg >(pc_block_eq … st_prf) % |*: whd in match set_regs; whd in match sigma_regs; normalize nodelta cases(regs … st1) #ps_r #hw_r normalize nodelta whd in match sigma_register_env; normalize nodelta @eq_f2 // change with (empty_map RegisterTag beval) in match (map RegisterTag ????); <(empty_set_minus … restr) % ] ] ] |*: #e #_ #x whd in match ertl_save_frame; normalize nodelta normalize nodelta #H @('bind_inversion H) -H #y whd in match push_ra; normalize nodelta #H @('bind_inversion H) -H #z whd in match push; normalize nodelta whd in match (istack ??); whd in match is_push; normalize nodelta >m_return_bind whd in match set_istack; normalize nodelta whd in ⊢ (??%% →?); #EQ destruct(EQ) normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (st_frms ??); whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] qed.