- Timestamp:
- Jul 1, 2013, 4:34:13 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLToLTLProof.ma
r3371 r3372 66 66 (beloadv m2) (beloadv m3). 67 67 68 (* 68 69 definition callee_saved_remap : 69 70 (Σb:block.block_region b=Code) → (block → list register) → … … 87 88 ] 88 89 ]. 90 *) 91 89 92 (* 90 93 definition mem_relation : fixpoint_computer → coloured_graph_computer → … … 97 100 (λptr1,ptr2.ERTL_validate_pointer … ge f st ptr1 = return it ∧ ptr1 = ptr2) R 98 101 (beloadv m2) (beloadv m3). 102 *) 99 103 100 104 definition callee_saved_remap : fixpoint_computer → coloured_graph_computer → … … 123 127 | None ⇒ d 124 128 ] 125 ]. *) 126 129 ]. 130 131 xxxxxxxxxxxxx 127 132 128 133 let rec frames_relation_aux (prog : ertl_program) (stacksize : ident → option ℕ) … … 520 525 qed.*) 521 526 522 523 527 lemma ps_reg_retrieve_hw_reg_retrieve_commute : 524 528 ∀prog,stacksize,init,color_f,live_f,color_fun,live_fun. … … 1023 1027 cases daemon qed. 1024 1028 1029 axiom BadVertexValue : ErrorMessage. 1030 1025 1031 definition ertl_vertex_retrieve : ertl_reg_env → vertex → res beval ≝ 1026 λregs,v.match v with [inl r ⇒ ps_reg_retrieve regs r | inr r ⇒ hw_reg_retrieve regs r ]. 1027 1032 λregs,v.match v with 1033 [inl r ⇒ ps_reg_retrieve regs r 1034 | inr r ⇒ match hwreg_retrieve (\snd regs) r with 1035 [ BVundef ⇒ Error ? [MSG BadVertexValue] 1036 | _ ⇒ OK ? (hwreg_retrieve (\snd regs) r) 1037 ] 1038 ]. 1039 1028 1040 definition eq_decision : decision → decision → bool ≝ 1029 1041 λd1,d2.match d1 with … … 1042 1054 qed. 1043 1055 1056 lemma ertl_vertex_retrieve_ok_on_hw_regs : 1057 ∀regs,r,bv.ertl_vertex_retrieve regs (inr ?? r) = return bv → 1058 hwreg_retrieve (\snd regs) r = bv. 1059 #regs #r #bv whd in match ertl_vertex_retrieve; normalize nodelta 1060 cases(hwreg_retrieve ??) normalize nodelta 1061 [|| #x #y #p | #b | #p | #ptr #p | #pc #p ] 1062 #EQ whd in EQ : (???%); destruct % 1063 qed. 1044 1064 1045 1065 lemma vertex_retrieve_read_arg_decision_commute : … … 1054 1074 (λv,d. 1055 1075 bool_to_Prop 1056 (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧ 1076 (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧ 1057 1077 d = 1058 1078 (color_fun fn v)) 1059 (λbv,bv'.bv = sigma_beval prog stacksize init init_regs f_lbls f_regs bv') … 1060 (λst1.ertl_vertex_retrieve (regs … st1)) 1061 (λst,d.m_map Res ?? (\fst …) 1062 (read_arg_decision (joint_if_local_stacksize ?? fn) st d)). 1079 (λx,y.\fst x = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst y) ∧ 1080 gen_state_rel prog stacksize init color_f live_f color_fun 1081 live_fun init_regs f_lbls f_regs pc (\snd x) (\snd y)) … 1082 (λst1,v.! bv ← ertl_vertex_retrieve (regs … st1) v; 1083 return〈bv,st1〉) 1084 (λst,d.(read_arg_decision (joint_if_local_stacksize ?? fn) st d)). 1063 1085 #prog #stacksize #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls #f_regs 1064 1086 #f #fn #pc #EQfn #st1 #st2 * … … 1066 1088 ** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) #_ cases(st_frms ??) [*] #frames 1067 1089 normalize nodelta ***** #_ #H1 #_ #_ #_ #_ * #live_R #EQ destruct(EQ) #bv #EQbv 1068 lapply((proj2 ?? H1 …) R live_R) cases(color_fun ??) normalize nodelta [#n1 | #R1 ] 1069 whd in EQbv : (??%%); destruct(EQbv) 1090 lapply((proj2 ?? H1 …) R live_R ?) 1091 [ % #ABS whd in match ertl_vertex_retrieve in EQbv; normalize nodelta in EQbv; 1092 >ABS in EQbv; normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ) ] 1093 cases(color_fun ??) normalize nodelta [#n1 | #R1 ] lapply(ertl_vertex_retrieve_ok_on_hw_regs … EQbv) 1094 #EQ destruct(EQ) 1070 1095 [ inversion (hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *] #sp #EQsp 1071 1096 inversion(beloadv ??) normalize nodelta [ #_ *] #bv1 #EQbv1 #Hbv1 %{bv1} … … 1112 1137 qed. 1113 1138 1139 (* 1114 1140 lemma update_color_lemma : 1115 1141 ∀fix_comp,colour,prog,init. … … 1178 1204 (update_fun ?? eq_vertex (live_fun fn (point_of_pc ERTL_semantics pc)) v new_live)) 1179 1205 init_regs f_lbls f_regs pc st1 st2. 1180 cases daemon qed. 1206 cases daemon qed. *) 1181 1207 1182 1208 lemma move_preserve :
Note: See TracChangeset
for help on using the changeset viewer.