Changeset 3259 for src/ERTL/ERTLToLTLProof.ma
 Timestamp:
 May 9, 2013, 12:49:38 AM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTLProof.ma
r3253 r3259 20 20 joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes). 21 21 22 definition local_clear_sb_type ≝ decision → bool. 23 definition clear_sb_type ≝ label → local_clear_sb_type. 24 25 (*function that will be used in order to retrieve ERTLstates from LTLstates. 26 Now it is an axiom. To be Implemented *) 27 axiom to_be_cleared_sb : 28 ∀live_before : valuation register_lattice. 29 coloured_graph live_before → clear_sb_type. 30 31 definition local_clear_fb_type ≝ vertex → bool. 32 definition clear_fb_type ≝ label → local_clear_fb_type. 33 34 35 (*function that will be used in order to clear ERTLstates from dead registers. 36 Now it is an axiom. To be implemented *) 37 definition to_be_cleared_fb : 38 ∀live_before : valuation register_lattice.clear_fb_type≝ 39 λlive_before,pt,v.notb (lives v (live_before pt)). 40 41 include "common/ExtraIdentifiers.ma". 42 43 definition sigma_fb_register_env : local_clear_fb_type → register_env beval → 44 register_env beval ≝ 45 λclear_fun,regs.find_all … regs (λi.λ_.notb (clear_fun (inl ?? i))). 46 22 definition local_live_type ≝ vertex → bool. 23 definition live_type ≝ label → local_live_type. 24 25 definition ps_relation : 26 ℕ → local_live_type → (vertex → decision) → (beval → beval → Prop) → 27 pointer → register_env beval → hw_register_env × bemem → Prop ≝ 28 λlocalss,live_fun,colour,R,sp,rgs,st. 29 gen_preserving … gen_res_preserve … 30 (λr : (Σr.bool_to_Prop(live_fun (inl ?? r))).λd.colour(inl ?? r) = d) R 31 (reg_retrieve rgs) 32 (λd.match d with 33 [decision_colour R ⇒ return hwreg_retrieve (\fst st) R 34 decision_spill n ⇒ opt_to_res ? [MSG FailedLoad] 35 (beloadv (\snd st) 36 (shift_pointer ? sp (bitvector_of_nat 8 (localss + n)))) 37 ]). 38 39 definition hw_relation : local_live_type → (beval → beval → Prop) → 40 hw_register_env → hw_register_env → Prop ≝ 41 λlive_fun,R,hw1,hw2. 42 ∀r : Register.live_fun (inr ?? r) → 43 R (hwreg_retrieve hw1 r) (hwreg_retrieve hw2 r). 44 45 include alias "arithmetics/nat.ma". 46 include alias "basics/logic.ma". 47 48 (*filters now are axioms but they will be implemented *) 49 axiom ertl_sp_filter : pointer → Prop. 50 axiom ltl_sp_filter : pointer → Prop. 51 52 definition mem_relation : 53 (beval → beval → Prop) → bemem → bemem → Prop ≝ 54 λR,m1,m2. 55 gen_preserving ?? gen_opt_preserve ???? 56 (λptr1 : Σptr.ertl_sp_filter ptr. 57 λptr2 : Σptr.ltl_sp_filter ptr.pi1 ?? ptr1 = pi1 ?? ptr2) R 58 (beloadv m1) (beloadv m2). 59 60 axiom frames_relation : 61 fixpoint_computer → coloured_graph_computer → 62 ertl_program → (beval → beval → Prop) → 63 framesT ERTL_state → (hw_register_env × bemem) → Prop. 64 65 (* 47 66 definition register_of_bitvector : BitVector 6 → option Register≝ 48 67 λvect. … … 86 105 else if eqb n 36 then Some ? RegisterCarry (* was 1, increment as needed *) 87 106 else None ?. 88 89 90 91 definition sigma_fb_hw_register_env : local_clear_fb_type → hw_register_env → 92 hw_register_env ≝ 93 λclear_fun,regs. 94 let f ≝ λvect,val,m. 95 match register_of_bitvector vect with 96 [ Some r ⇒ 97 if (clear_fun (inr ?? r)) then 98 m 99 else 100 insert … vect val m 101  None ⇒ m 102 ] in 103 mk_hw_register_env … (fold … f (reg_env … regs) (Stub …)) BBundef. 104 105 definition sigma_fb_regs : local_clear_fb_type → ertl_reg_env → ertl_reg_env ≝ 106 λclear_fun,regs.〈sigma_fb_register_env clear_fun (\fst regs), 107 sigma_fb_hw_register_env clear_fun (\snd regs)〉. 108 109 definition sigma_fb_frames : local_clear_fb_type → 110 list (register_env beval × (Σb:block.block_region b=Code)) → 111 list (register_env beval × (Σb:block.block_region b=Code)) ≝ 112 λclear_fun,frms.map … (λx.〈sigma_fb_register_env clear_fun (\fst x),\snd x〉) frms. 113 114 definition sigma_fb_state: 115 ertl_program → local_clear_fb_type → 116 state ERTL_semantics → state ERTL_semantics ≝ 117 λprog,clear_fun,st. 118 mk_state ? 119 (option_map ?? (sigma_fb_frames clear_fun) (st_frms … st)) 120 (istack … st) 121 (if clear_fun (inr ?? RegisterCarry) then BBundef 122 else (carry … st)) 123 (sigma_fb_regs clear_fun (regs … st)) (m … st) (stack_usage … st). 107 *) 124 108 125 109 axiom acc_is_dead : ∀fix_comp.∀prog : ertl_program. … … 127 111 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in 128 112 ¬ lives (inr ? ? RegisterA) (livebefore … fn after l). 129 113 (* 130 114 axiom dead_registers_in_dead : 131 115 ∀fix_comp.∀build : coloured_graph_computer. … … 138 122 ¬ lives (inr ? ? R) (livebefore … fn after l) → 139 123 to_be_cleared_sb … coloured_graph l R. 140 141 axiom sigma_sb_state: list (Σb.block_region b = Code) → 142 ertl_program → local_clear_sb_type → state LTL_semantics → state ERTL_semantics. 124 *) 143 125 144 126 definition dummy_state : state ERTL_semantics ≝ … … 154 136 list (Σb:block.block_region b=Code) ≝ map … \snd. 155 137 156 definition sigma_fb_state_pc :157 fixpoint_computer → coloured_graph_computer → ertl_program →158 state_pc ERTL_semantics → state_pc ERTL_semantics ≝159 λfix_comp,colour,prog,st.160 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in161 let stacksizes ≝ lookup_stack_cost … m in162 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in163 let globals ≝ prog_names … prog in164 match fetch_internal_function … ge (pc_block (pc … st)) with165 [ OK y ⇒166 let pt ≝ point_of_pc ERTL_semantics (pc ? st) in167 let after ≝ (analyse_liveness fix_comp (prog_names … prog) (\snd y)) in168 let before ≝ livebefore … (\snd y) after in169 mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb before pt) st) (pc … st)170 (last_pop … st)171  Error e ⇒ dummy_state_pc172 ].173 174 definition sigma_sb_state_pc:175 fixpoint_computer → coloured_graph_computer →176 ertl_program → list (Σb:block.block_region b=Code) →177 (block → list register) → lbl_funct_type →178 regs_funct_type → state_pc LTL_semantics → state_pc ERTL_semantics ≝179 λfix_comp,build,prog,cs,init_regs,f_lbls,f_regs,st.180 let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in181 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in182 let stacksizes ≝ lookup_stack_cost … m in183 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in184 let globals ≝ prog_names … prog in185 match fetch_internal_function … ge (pc_block (pc … st)) with186 [ OK y ⇒187 let pt ≝ point_of_pc ERTL_semantics (pc ? st) in188 let after ≝ (analyse_liveness fix_comp (prog_names … prog) (\snd y)) in189 let coloured_graph ≝ build … (\snd y) after in190 mk_state_pc ? (sigma_sb_state cs prog191 (to_be_cleared_sb … coloured_graph pt) st) (pc … st)192 (sigma_stored_pc ERTL_semantics LTL_semantics193 prog stacksizes init init_regs f_lbls f_regs (last_pop … st))194  Error e ⇒ dummy_state_pc195 ].196 @hide_prf % qed.197 198 definition state_rel : fixpoint_computer → coloured_graph_computer →199 ertl_program → joint_state_relation ERTL_semantics LTL_semantics ≝200 λfix_comp,build,prog,pc,st1,st2.201 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in202 let stacksizes ≝ lookup_stack_cost … m in203 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in204 ∃f,fn.fetch_internal_function … ge (pc_block pc)205 = return 〈f,fn〉 ∧206 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in207 let before ≝ livebefore … fn after in208 let coloured_graph ≝ build … fn after in209 match st_frms … st1 with210 [ None ⇒ False211  Some frames ⇒212 (sigma_fb_state prog (to_be_cleared_fb before (point_of_pc ERTL_semantics pc)) st1) =213 (sigma_sb_state (get_ertl_call_stack frames) prog214 (to_be_cleared_sb … coloured_graph (point_of_pc ERTL_semantics pc)) st2)215 ].216 217 definition state_pc_rel :218 fixpoint_computer → coloured_graph_computer →219 ertl_program → (block → list register) → lbl_funct_type →220 regs_funct_type → joint_state_pc_relation ERTL_semantics LTL_semantics ≝221 λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2.222 match st_frms … (st_no_pc … st1) with223 [ None ⇒ False224  Some frames ⇒225 sigma_fb_state_pc fix_comp build prog st1 =226 sigma_sb_state_pc fix_comp build prog (get_ertl_call_stack frames) init_regs227 f_lbls f_regs st2228 ].229 230 axiom insensitive_to_be_cleared_sb :231 ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.232 ∀d : decision.∀bv,st',localss,cs.tb d →233 write_decision localss d bv st = return st' →234 sigma_sb_state cs prog tb st =235 sigma_sb_state cs prog tb st'.236 237 lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss.238 ∀st : state LTL_LIN_state.239 ∀st'. (write_decision localss r bv st) = return st' →240 hw_reg_retrieve (regs … st') r = return bv.241 #r #bv #localss #st #st' whd in match write_decision; normalize nodelta242 whd in match hw_reg_store; normalize nodelta >m_return_bind243 whd in ⊢ (??%% → ?); #EQ destruct(EQ)244 whd in match hw_reg_retrieve; normalize nodelta @eq_f245 whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta246 @lookup_insert_hit247 qed.248 138 249 139 definition sigma_beval : fixpoint_computer → coloured_graph_computer → … … 262 152 @hide_prf % qed. 263 153 264 axiom ps_reg_retrieve_hw_reg_retrieve_commute : 154 definition state_rel : fixpoint_computer → coloured_graph_computer → 155 ertl_program → (block → list register) → lbl_funct_type → regs_funct_type → 156 joint_state_relation ERTL_semantics LTL_semantics ≝ 157 λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc,st1,st2. 158 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in 159 let stacksizes ≝ lookup_stack_cost … m1 in 160 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in 161 ∃f,fn.fetch_internal_function … ge (pc_block pc) 162 = return 〈f,fn〉 ∧ 163 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in 164 let before ≝ livebefore … fn after in 165 let coloured_graph ≝ build … fn after in 166 let R ≝ λbv1,bv2.bv2 = sigma_beval fix_comp build prog init_regs f_lbls f_regs bv1 in 167 let live_fun ≝ λv.lives v (before (point_of_pc ERTL_semantics pc)) in 168 match st_frms … st1 with 169 [ None ⇒ False 170  Some frames ⇒ 171 mem_relation R (m … st1) (m … st2) ∧ 172 frames_relation fix_comp build prog R frames 〈regs … st2,m … st2〉 ∧ 173 hw_relation live_fun R (\snd (regs … st1)) (regs … st2) ∧ 174 make_is_relation_from_beval R (istack … st1) (istack … st2) ∧ 175 (live_fun (inr ?? RegisterCarry) → carry … st1 = carry … st2) ∧ 176 ∃ptr.sp … st2 = return ptr ∧ 177 ps_relation (joint_if_local_stacksize … fn) live_fun (colouring … coloured_graph) 178 R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉 179 ]. 180 181 definition state_pc_rel : 182 fixpoint_computer → coloured_graph_computer → 183 ertl_program → (block → list register) → lbl_funct_type → 184 regs_funct_type → joint_state_pc_relation ERTL_semantics LTL_semantics ≝ 185 λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2. 186 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in 187 let stacksizes ≝ lookup_stack_cost … m1 in 188 let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in 189 state_rel fix_comp build prog init_regs f_lbls f_regs (pc … st1) st1 st2 ∧ 190 pc … st1 = pc … st2 ∧ 191 (last_pop … st2 = sigma_stored_pc ERTL_semantics LTL_semantics prog stacksizes 192 init init_regs f_lbls f_regs (last_pop … st1)). 193 @hide_prf % qed. 194 195 lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss. 196 ∀st : state LTL_LIN_state. 197 ∀st'. (write_decision localss r bv st) = return st' → 198 hw_reg_retrieve (regs … st') r = return bv. 199 #r #bv #localss #st #st' whd in match write_decision; normalize nodelta 200 whd in match hw_reg_store; normalize nodelta >m_return_bind 201 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 202 whd in match hw_reg_retrieve; normalize nodelta @eq_f 203 whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta 204 @lookup_insert_hit 205 qed. 206 207 lemma ps_reg_retrieve_hw_reg_retrieve_commute : 265 208 ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,fn,pc. 266 209 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in 267 210 gen_preserving2 ?? gen_res_preserve ?????? 268 (state_rel fix_comp colour prog pc)211 (state_rel fix_comp colour prog init_regs f_lbls f_regs pc) 269 212 (λr : register.λd : arg_decision.d = 270 213 (colouring … (colour (prog_names … prog) fn after) … … 274 217 (λst,d.m_map Res ?? (\fst …) 275 218 (read_arg_decision (joint_if_local_stacksize ?? fn) st d)). 219 xxxxxxxxxxxxxx 276 220 277 221 (*set_theoretical axioms *)
Note: See TracChangeset
for help on using the changeset viewer.