Changeset 2176 for src/joint/BEMem.ma
- Timestamp:
- Jul 12, 2012, 1:28:28 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/BEMem.ma
r1993 r2176 23 23 definition is_address : (beval × beval) → Prop ≝ λa. 24 24 ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1. 25 \fst a = BVptr p p0 ∧ part_no ?p0 = 0 ∧26 \snd a = BVptr p p1 ∧ part_no ?p1 = 1.25 \fst a = BVptr p p0 ∧ part_no … p0 = 0 ∧ 26 \snd a = BVptr p p1 ∧ part_no … p1 = 1. 27 27 28 28 definition is_addressb : (beval × beval) → bool ≝ λa. … … 44 44 (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a). 45 45 #P * * 46 [4:|*: [|#b0| #r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]46 [4:|*: [|#b0|(*#r0*)#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)] 47 47 #p0 #part0 #a1 48 48 whd in match is_addressb; normalize nodelta … … 50 50 #H >H 51 51 [ @(eqb_elim part0 0) #Heq 52 [ cases a1 [|#b0| #r0#part0|#p1#part1] whd in match (?∧?);52 [ cases a1 [|#b0|(*#r0*)#part0|#p1#part1] whd in match (?∧?); 53 53 [4: @eq_pointer_elim #Heq' 54 54 [ @(eqb_elim part1 1) #Heq'' … … 89 89 destruct(H0 H4) 90 90 qed. 91 91 (* For full 8051 memory spaces 92 92 definition pointer_compat' ≝ λb,r. 93 93 match b with … … 116 116 ] 117 117 qed. 118 118 *) 119 119 lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a). 120 ** #a0 #a1 ***** #z #o 121 #Hr 122 (* 120 123 ** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr) 121 124 cases r in Hr ⊢ %; #Hr * 125 *) 122 126 ** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1 123 127 destruct normalize … … 133 137 #p 134 138 lapply (refl … p) 135 generalize in match p in ⊢ (???%→%); * *139 generalize in match p in ⊢ (???%→%); *(***) 136 140 whd in match (address_of_pointer ?); 137 #b #H#o #EQp * #a0 #a1141 #b (*#H*) #o #EQp * #a0 #a1 138 142 normalize #EQ destruct(EQ) 143 %{p} >EQp [ cases (block_region b) // | % [2: % [2: % [ % [ % ] ] ] ] % 144 (* 139 145 %{p} >EQp [1,3: %] 140 146 % [2,4: % [2,4: % [1,3: % [1,3: %]]]] % 147 *) 141 148 qed. 142 149 … … 146 153 lemma address_of_pointer_is_safe : 147 154 ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address). 155 #p normalize % qed. 156 (* 148 157 ****#z #H 149 158 lapply (pointer_compat_from_ind ?? H) * #o 150 159 normalize % 151 qed. 160 qed.*) 152 161 153 162 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ … … 157 166 158 167 definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer. 168 cases H -H * #b #o normalize cases b * #z #EQ destruct 169 %{«mk_pointer (mk_block Code z) o,I»} 170 % [2: % [2: % [ % [ % ]]]] % 171 qed. 172 (* 159 173 cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H 160 174 lapply (pointer_compat_from_ind … H) -H cases b * #z * #H 161 175 %{«mk_pointer ? (mk_block Code z) H o,I»} 162 176 % [2: % [2: % [ % [ % ]] % |]|] 163 qed. 177 qed.*) 164 178 165 179 (* Paolo: why only code pointers and not XRAM too? *)
Note: See TracChangeset
for help on using the changeset viewer.