Changeset 2437 for src/joint/BEMem.ma
 Timestamp:
 Nov 6, 2012, 5:00:01 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/BEMem.ma
r2286 r2437 20 20 [ XData ⇒ true  Code ⇒ true  _ ⇒ false ]. 21 21 22 definition is_address : (beval × beval) → Prop ≝ λa.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 (*30 definition is_addressb : (beval × beval) → bool ≝ λa.31 let 〈a0,a1〉 ≝ a in32 match a0 with33 [ BVptr b0 part0 o0 ⇒34 is_addressable (block_region b0) ∧ eqb part0 0 ∧35 match a1 with36 [ BVptr b1 part1 o1 ⇒37 eq_block b0 b1 ∧ eqb part1 1 ∧ subvector_with … (eq_bv 8) o0 o138  _ ⇒ false39 ]40  _ ⇒ false41 ].42 43 lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.44 (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).45 #P * * [#b0(*#r0*)#part0#b0#part0#o0] #a146 [5: whd in match is_addressb; normalize nodelta47 elim (true_or_false_Prop (is_addressable (block_region b0)))48 #H >H49 [ @(eqb_elim part0 0) #Heq50 [ 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 destruct55 %{b1} [assumption] %{part0} %{part1} %{o0} %{o1}56 % [ % [ % [ % ]]] try assumption %57 ]58 ]59 ]60 ]61 ]62 ]63 ]64 #_ #Pfalse @Pfalse % ** #b0' #H' * #part0' * #part1' * #o0' * #o1' ****65 #H0 #H1 #H2 #H3 #H4 destruct /2 by absurd/66 qed.67 *)68 69 22 (* CSC: only pointers to XRAM or code memory ATM *) 70 23 definition address ≝ beval × beval. 71 72 (* definition safe_address ≝ Sig address is_address.73 unification hint 0 ≔ ;74 P ≟ Prod beval beval75 (**)⊢76 safe_address ≡ Sig P is_address. *)77 78 definition eq_address: address → address → bool ≝79 λaddr1,addr2.80 eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).81 24 82 25 definition pointer_of_address: address → res pointer ≝ 83 26 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2]. 84 27 28 definition is_address : (beval × beval) → Prop ≝ λa. 29 ∃ptr.pointer_of_address a = OK … ptr. 30 85 31 lemma bevals_of_pointer_is_address : 86 32 ∀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: % ] 33 * #bl #o 34 whd in ⊢ (?%); whd % 35 [2: whd in ⊢ (??%?); 36 >eq_block_b_b 37 change with (eq_bv ???) in match (eq_bv_suffix ?????); 38 >eq_bv_refl normalize %] 120 39 qed. 121 40 … … 163 82 qed.*) 164 83 165 definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.166 167 example address_of_pointer_OK_to_safe :168 ∀p,a.address_of_pointer p = OK … a → is_address a.169 #p #a whd in match address_of_pointer; normalize nodelta170 #EQ lapply (sym_eq ??? EQ) EQ #EQ destruct(EQ)171 //172 qed.173 174 84 (*definition safe_address_of_pointer: pointer → res safe_address ≝ λp. 175 85 do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
Note: See TracChangeset
for help on using the changeset viewer.