Changeset 1882 for src/joint/BEMem.ma
 Timestamp:
 Apr 6, 2012, 8:02:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/BEMem.ma
r1419 r1882 44 44 mk_mem … blocks (nextblock … m) (nextblock_pos … m)). 45 45 46 definition is_addressable : region → bool ≝ λr.match r with 47 [ XData ⇒ true  Code ⇒ true  _ ⇒ false ]. 48 49 50 definition is_address : (beval × beval) → Prop ≝ λa. 51 ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1. 52 \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧ 53 \snd a = BVptr p p1 ∧ part_no ? p1 = 1. 54 55 definition is_addressb : (beval × beval) → bool ≝ λa. 56 match a with 57 [ mk_Prod a0 a1 ⇒ 58 match a0 with 59 [ BVptr p0 part0 ⇒ 60 is_addressable (ptype p0) ∧ eqb part0 0 ∧ 61 match a1 with 62 [ BVptr p1 part1 ⇒ 63 eq_pointer p0 p1 ∧ eqb part1 1 64  _ ⇒ false 65 ] 66  _ ⇒ false 67 ] 68 ]. 69 70 lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval. 71 (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a). 72 #P * * 73 [4:*: [#b0#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)] 74 #p0 #part0 #a1 75 whd in match is_addressb; normalize nodelta 76 elim (true_or_false_Prop (is_addressable (ptype p0))) 77 #H >H 78 [ @(eqb_elim part0 0) #Heq 79 [ cases a1 [#b0#r0#part0#p1#part1] whd in match (?∧?); 80 [4: @eq_pointer_elim #Heq' 81 [ @(eqb_elim part1 1) #Heq'' 82 [ #Ptrue #_ @Ptrue destruct 83 %{p1} [assumption] %{part0} %{part1} 84 % [ % [ % ]] try % assumption 85 ] 86 ] 87 ] 88 ] 89 ] 90 #_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' *** 91 #H0 #H1 #H2 #H3 destruct /2 by absurd/ 92 qed. 93 46 94 (* CSC: only pointers to XRAM or code memory ATM *) 47 95 definition address ≝ beval × beval. 96 definition safe_address ≝ Sig address is_address. 97 unification hint 0 ≔ ; 98 P ≟ Prod beval beval 99 (**)⊢ 100 safe_address ≡ Sig P is_address. 48 101 49 102 definition eq_address: address → address → bool ≝ … … 53 106 definition pointer_of_address: address → res pointer ≝ 54 107 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2]. 55 definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer. 56 57 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair. 108 109 definition pointer_of_address_safe : safe_address → pointer ≝ 110 λp.match \fst p return λx.\fst p = x → ? with 111 [ BVptr ptr _ ⇒ λ_.ptr 112  _ ⇒ λabs.⊥ 113 ] (refl …). 114 lapply abs abs cases p 115 * #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4 116 destruct(H0 H4) 117 qed. 118 119 definition pointer_compat' ≝ λb,r. 120 match b with 121 [ mk_block r' z ⇒ 122 if eq_region r' r then True 123 else 124 match r with 125 [ Any ⇒ True 126  XData ⇒ match r' with 127 [ PData ⇒ True 128  _ ⇒ False 129 ] 130  _ ⇒ False 131 ] 132 ]. 133 134 lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r. 135 ** #z ** // 136 qed. 137 138 lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r. 139 #b #r #H inversion H 140 [ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region % 141  #id #EQ1 #EQ2 #EQ3 % 142  #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) % 143 ] 144 qed. 145 146 lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a). 147 ** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr) 148 cases r in Hr ⊢ %; #Hr * 149 ** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1 150 destruct normalize 151 @eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))] 152 @eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))] 153 #_ #_ normalize % 154 qed. 155 156 definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer. 157 158 example address_of_pointer_OK_to_safe : 159 ∀p,a.address_of_pointer p = OK … a → is_address a. 160 #p 161 lapply (refl … p) 162 generalize in match p in ⊢ (???%→%); ** 163 whd in match (address_of_pointer ?); 164 #b #H #o #EQp * #a0 #a1 165 normalize #EQ destruct(EQ) 166 %{p} >EQp [1,3: %] 167 % [2,4: % [2,4: % [1,3: % [1,3: %]]]] % 168 qed. 169 170 definition safe_address_of_pointer: pointer → res safe_address ≝ λp. 171 do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ». 172 173 lemma address_of_pointer_is_safe : 174 ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address). 175 ****#z #H 176 lapply (pointer_compat_from_ind ?? H) * #o 177 normalize % 178 qed. 179 180 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ 181 code_pointer_of_beval_pair. 182 58 183 definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer. 59 184 185 definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer. 186 cases H H * #r #b #H #o #EQ destruct(EQ) normalize lapply H 187 lapply (pointer_compat_from_ind … H) H cases b * #z * #H 188 %{«mk_pointer ? (mk_block Code z) H o,I»} 189 % [2: % [2: % [ % [ % ]] % ]] 190 qed. 191 192 (* Paolo: why only code pointers and not XRAM too? *) 60 193 definition addr_add: address → nat → res address ≝ 61 194 λaddr,n. … … 65 198 qed. 66 199 200 definition safe_addr_add: safe_address → nat → res safe_address ≝ 201 λaddr,n. 202 do ptr ← code_pointer_of_address addr ; 203 OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))). 204 normalize cases ptr #p #E @E 205 qed. 206 67 207 definition addr_sub: address → nat → res address ≝ 68 208 λaddr,n. … … 71 211 normalize cases ptr #p #E @E 72 212 qed. 213 214 definition safe_addr_sub: safe_address → nat → res safe_address ≝ 215 λaddr,n. 216 do ptr ← code_pointer_of_address addr ; 217 OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))). 218 normalize cases ptr #p #E @E 219 qed.
Note: See TracChangeset
for help on using the changeset viewer.