Changeset 2185 for src/common/Pointers.ma
 Timestamp:
 Jul 13, 2012, 7:59:43 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Pointers.ma
r2176 r2185 68 68 the option of extending blocks backwards. *) 69 69 70 definition offset_size ≝ 8*size_pointer. 71 70 72 (* CSC: why do we need this awful indirection? *) 71 record offset : Type[0] ≝ { offv : Z}.73 record offset : Type[0] ≝ { offv : BitVector offset_size }. 72 74 73 definition eq_offset ≝ λx,y. eq Zb(offv x) (offv y).75 definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y). 74 76 75 77 lemma reflexive_eq_offset: ∀x. eq_offset x x = true. … … 77 79 qed. 78 80 81 lemma eq_offset_elim : ∀P : bool → Prop.∀o1,o2. 82 (o1 = o2 → P true) → (o1 ≠ o2 → P false) → P (eq_offset o1 o2). 83 #P * #o1 * #o2 #T #F 84 change with (eq_bv ???) in ⊢ (?%); 85 @eq_bv_elim 86 [ /2/ 87  * #FF @F % #E destruct /2/ 88 ] qed. 89 90 definition offset_of_Z : Z → offset ≝ 91 λz. mk_offset (bitvector_of_Z … z). 79 92 definition shift_offset : ∀n. offset → BitVector n → offset ≝ 80 λn,o,i. mk_offset ( offv o + Z_of_signed_bitvector ? i).93 λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)). 81 94 (* A version of shift_offset_n for multiplied addresses which avoids overflow. *) 82 95 definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝ 83 λn,o,i,j. mk_offset ( offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).96 λn,o,i,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))). 84 97 definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝ 85 λn,o,i. mk_offset ( offv o  Z_of_signed_bitvector ? i).98 λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)). 86 99 definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝ 87 λn,o,i,j. mk_offset ( offv o  (Z_of_nat i) * (Z_of_signed_bitvector ? j)).100 λn,o,i,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))). 88 101 definition sub_offset : ∀n. offset → offset → BitVector n ≝ 89 λn,x,y. bitvector_of_Z ? (offv x  offv y).90 definition zero_offset ≝ mk_offset OZ.102 λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)). 103 definition zero_offset ≝ mk_offset (zero ?). 91 104 definition lt_offset : offset → offset → bool ≝ 92 λx,y. Zltb(offv x) (offv y).105 λx,y. lt_u ? (offv x) (offv y). 93 106 94 107 (*CSC: use this definition everywhere in Values.ma and Mem.ma. *) … … 132 145 whd in match (eq_pointer ??); 133 146 @eq_block_elim #block_eq 134 [ change with (eqZb ??) in match (eq_offset ??); 135 @eqZb_elim #offset_eq 147 [ @eq_offset_elim #offset_eq 136 148 [ destruct @Ptrue % 137 149 ]
Note: See TracChangeset
for help on using the changeset viewer.