Changeset 2286 for src/joint/BEMem.ma
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/BEMem.ma
r2185 r2286 20 20 [ XData ⇒ true  Code ⇒ true  _ ⇒ false ]. 21 21 22 23 22 definition is_address : (beval × beval) → Prop ≝ λa. 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. 27 23 ∃b : Σb.bool_to_Prop (is_addressable (block_region b)). 24 ∃p0,p1,o0,o1. 25 \fst a = BVptr b p0 o0 ∧ part_no … p0 = 0 ∧ 26 \snd a = BVptr b p1 o1 ∧ part_no … p1 = 1 ∧ 27 bool_to_Prop (vsuffix … (eq_bv 8) o0 o1). 28 29 (* 28 30 definition is_addressb : (beval × beval) → bool ≝ λa. 29 match a with 30 [ mk_Prod a0 a1 ⇒ 31 match a0 with 32 [ BVptr p0 part0 ⇒ 33 is_addressable (ptype p0) ∧ eqb part0 0 ∧ 31 let 〈a0,a1〉 ≝ a in 32 match a0 with 33 [ BVptr b0 part0 o0 ⇒ 34 is_addressable (block_region b0) ∧ eqb part0 0 ∧ 34 35 match a1 with 35 [ BVptr p1 part1 ⇒36 eq_ pointer p0 p1 ∧ eqb part1136 [ BVptr b1 part1 o1 ⇒ 37 eq_block b0 b1 ∧ eqb part1 1 ∧ subvector_with … (eq_bv 8) o0 o1 37 38  _ ⇒ false 38 39 ] 39  _ ⇒ false 40 ] 40  _ ⇒ false 41 41 ]. 42 42 43 43 lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval. 44 44 (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a). 45 #P * * 46 [4:*: [#b0(*#r0*)#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)] 47 #p0 #part0 #a1 48 whd in match is_addressb; normalize nodelta 49 elim (true_or_false_Prop (is_addressable (ptype p0))) 50 #H >H 51 [ @(eqb_elim part0 0) #Heq 52 [ cases a1 [#b0(*#r0*)#part0#p1#part1] whd in match (?∧?); 53 [4: @eq_pointer_elim #Heq' 54 [ @(eqb_elim part1 1) #Heq'' 55 [ #Ptrue #_ @Ptrue destruct 56 %{p1} [assumption] %{part0} %{part1} 57 % [ % [ % ]] try % assumption 45 #P * * [#b0(*#r0*)#part0#b0#part0#o0] #a1 46 [5: whd in match is_addressb; normalize nodelta 47 elim (true_or_false_Prop (is_addressable (block_region b0))) 48 #H >H 49 [ @(eqb_elim part0 0) #Heq 50 [ cases a1 [#b1(*#r1*)#part1#b1#part1#o1] whd in match (?∧?); 51 [5: @eq_block_elim #Heq' 52 [ @(eqb_elim part1 1) #Heq'' 53 [ elim (true_or_false_Prop (subvector_with … (eq_bv 8) o0 o1)) #Heq''' >Heq''' 54 [ #Ptrue #_ @Ptrue destruct 55 %{b1} [assumption] %{part0} %{part1} %{o0} %{o1} 56 % [ % [ % [ % ]]] try assumption % 57 ] 58 ] 58 59 ] 59 60 ] … … 61 62 ] 62 63 ] 63 #_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' *** 64 #H0 #H1 #H2 #H3 destruct /2 by absurd/ 65 qed. 64 #_ #Pfalse @Pfalse % ** #b0' #H' * #part0' * #part1' * #o0' * #o1' **** 65 #H0 #H1 #H2 #H3 #H4 destruct /2 by absurd/ 66 qed. 67 *) 66 68 67 69 (* CSC: only pointers to XRAM or code memory ATM *) 68 70 definition address ≝ beval × beval. 69 definition safe_address ≝ Sig address is_address. 71 72 (* definition safe_address ≝ Sig address is_address. 70 73 unification hint 0 ≔ ; 71 74 P ≟ Prod beval beval 72 75 (**)⊢ 73 safe_address ≡ Sig P is_address. 76 safe_address ≡ Sig P is_address. *) 74 77 75 78 definition eq_address: address → address → bool ≝ … … 79 82 definition pointer_of_address: address → res pointer ≝ 80 83 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2]. 81 82 definition pointer_of_address_safe : safe_address → pointer ≝ 83 λp.match \fst p return λx.\fst p = x → ? with 84 [ BVptr ptr _ ⇒ λ_.ptr 85  _ ⇒ λabs.⊥ 86 ] (refl …). 87 lapply abs abs cases p 88 * #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4 89 destruct(H0 H4) 90 qed. 84 85 lemma bevals_of_pointer_is_address : 86 ∀p.is_address (list_to_pair … (bevals_of_pointer p) (refl …)). 87 * #b * #o whd in ⊢ (?%); whd 88 %{b} [ elim (block_region b) % ] %{(mk_part 0 ?)} [ %2 %1 ] %{(mk_part 1 ?)} [ %1 ] 89 @(vsplit_elim … 8 8 o) #o1 #o0 #EQ >EQ o 90 %{[[o0]]} %{[[o1;o0]]} 91 % [2: change with (bool_to_Prop (if eq_bv ??? then ? else ?)) 92 >eq_bv_refl % ] 93 %%[2: normalize nodelta @vsplit_elim #pre >(Vector_O … pre) #post #EQ 94 normalize in EQ; <EQ pre post 95 whd in match (rvsplit ????); 96 <(vsplit_prod … (refl …)) normalize nodelta 97  % [2: % ] 98 ] 99 whd in match (rvsplit ????); 100 try <(vector_append_empty … o0) in ⊢ (??%?); 101 <(vsplit_prod … (refl …)) normalize nodelta % 102 qed. 103 104 lemma is_address_to_pointer : ∀a.is_address a → ∃p.pointer_of_address a = return p. 105 * #a0 #a1 ** #bl #bl_prf ** #p0 #p0_prf ** #p1 #p1_prf * #o0' * #o1o0 **** 106 #EQ1 #EQ2 #EQ3 #EQ4 destruct 107 @(Vector_pair_elim … o1o0) #o1 #o0 #EQ >EQ o1o0 108 @(Vector_singl_elim … o0') #o0'' #EQ >EQ o0' 109 whd in ⊢ (?%→?); 110 @eq_bv_elim #EQ * >EQ o0'' 111 whd in match (pointer_of_address ?); 112 >eq_block_b_b >(eqb_n_n 1) 113 >vsuffix_vflatten 114 [2: change with (bool_to_Prop (vsuffix ????? ([[?]]@@[[?]]))) 115 @vsuffix_true change with (bool_to_Prop (if eq_bv ? o0 o0 then ? else ?)) 116 >eq_bv_refl % ] 117 normalize nodelta 118 whd in ⊢ (??(λ_.??%?)); 119 % [2: % ] 120 qed. 121 91 122 (* For full 8051 memory spaces 92 123 definition pointer_compat' ≝ λb,r. … … 117 148 qed. 118 149 *) 119 lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).150 (*lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a). 120 151 ** #a0 #a1 ***** #z #o 121 152 #Hr … … 130 161 @eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))] 131 162 #_ #_ normalize % 132 qed. 163 qed.*) 133 164 134 165 definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer. … … 136 167 example address_of_pointer_OK_to_safe : 137 168 ∀p,a.address_of_pointer p = OK … a → is_address a. 138 #p 139 lapply (refl … p) 140 generalize in match p in ⊢ (???%→%); *(***) 141 whd in match (address_of_pointer ?); 142 #b (*#H*) #o #EQp * #a0 #a1 143 normalize #EQ destruct(EQ) 144 %{p} >EQp [ cases (block_region b) //  % [2: % [2: % [ % [ % ] ] ] ] % 145 (* 146 %{p} >EQp [1,3: %] 147 % [2,4: % [2,4: % [1,3: % [1,3: %]]]] % 148 *) 149 qed. 150 151 definition safe_address_of_pointer: pointer → res safe_address ≝ λp. 169 #p #a whd in match address_of_pointer; normalize nodelta 170 #EQ lapply (sym_eq ??? EQ) EQ #EQ destruct(EQ) 171 // 172 qed. 173 174 (*definition safe_address_of_pointer: pointer → res safe_address ≝ λp. 152 175 do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ». 153 176 … … 177 200 % [2: % [2: % [ % [ % ]] % ]] 178 201 qed.*) 202 *) 179 203 180 204 (* Paolo: why only code pointers and not XRAM too? *) 181 definition addr_add: address → nat → res address ≝205 (*definition addr_add: address → nat → res address ≝ 182 206 λaddr,n. 183 207 do ptr ← code_pointer_of_address addr ; … … 206 230 normalize cases ptr #p #E @E 207 231 qed. 232 *)
Note: See TracChangeset
for help on using the changeset viewer.