Changeset 744 for src/common/Integers.ma
 Timestamp:
 Apr 7, 2011, 6:53:59 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Integers.ma
r700 r744 17 17 18 18 include "arithmetics/nat.ma". 19 include "utilities/binary/Z.ma". 20 include "utilities/extralib.ma". 19 include "utilities/extranat.ma". 21 20 22 21 include "ASM/BitVector.ma". 23 include "ASM/BitVectorZ.ma".24 22 include "ASM/Arithmetic.ma". 25 23 … … 68 66 69 67 definition wordsize : nat ≝ 32. 68 (* 70 69 definition modulus : Z ≝ Z_two_power_nat wordsize. 71 70 definition half_modulus : Z ≝ modulus / 2. … … 85 84 modulus > 0. 86 85 //; qed. 87 86 *) 88 87 (* * Representation of machine integers *) 89 88 … … 93 92 94 93 definition int : Type[0] ≝ BitVector wordsize. 95 94 (* 96 95 definition intval: int → Z ≝ Z_of_unsigned_bitvector ?. 97 96 definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus. … … 111 110 then unsigned n 112 111 else unsigned n  modulus. 113 112 *) 114 113 (* Conversely, [repr] takes a Coq integer and returns the corresponding 115 114 machine integer. The argument is treated modulo [modulus]. *) 116 115 (* 117 116 definition repr : Z → int ≝ λz. bitvector_of_Z wordsize z. 117 *) 118 definition repr : nat → int ≝ λn. bitvector_of_nat wordsize n. 118 119 119 120 definition zero := repr 0. 120 121 definition one := repr 1. 121 definition mone := repr (1).122 definition iwordsize := repr (Z_of_nat wordsize).122 definition mone := subtraction ? zero one. 123 definition iwordsize := repr wordsize. 123 124 124 125 lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y). … … 135 136 136 137 definition neg : int → int ≝ two_complement_negation wordsize. 137 138 let rec zero_ext (n:Z) (x:int) on x : int ≝ 139 repr (modZ (unsigned x) (two_p n)). 140 let rec sign_ext (n:Z) (x:int) on x : int ≝ 141 repr (let p ≝ two_p n in 142 let y ≝ modZ (unsigned x) p in 143 if Zltb y (two_p (n1)) then y else y  p). 144 145 definition add ≝ addition_n wordsize. 146 definition sub ≝ subtraction wordsize. 147 (*definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).*) 148 definition mul ≝ λx,y. repr ((unsigned x) * (unsigned y)). 149 definition Zdiv_round : Z → Z → Z ≝ λx,y: Z. 150 if Zltb x 0 then 151 if Zltb y 0 then (x) / (y) else  ((x) / y) 152 else 153 if Zltb y 0 then (x / (y)) else x / y. 154 155 definition Zmod_round : Z → Z → Z ≝ λx,y: Z. 156 x  (Zdiv_round x y) * y. 157 158 definition divs : int → int → int ≝ λx,y:int. 159 repr (Zdiv_round (signed x) (signed y)). 160 definition mods : int → int → int ≝ λx,y:int. 161 repr (Zmod_round (signed x) (signed y)). 162 definition divu : int → int → int ≝ λx,y. 163 repr (unsigned x / unsigned y). 164 definition modu : int → int → int ≝ λx,y. 165 repr (unsigned x \mod unsigned y). 166 167 (* * For bitwise operations, we need to convert between Coq integers [Z] 168 and their bitlevel representations. Bitlevel representations are 169 represented as characteristic functions, that is, functions [f] 170 of type [nat > bool] such that [f i] is the value of the [i]th bit 171 of the number. The values of characteristic functions for [i] greater 172 than 32 are ignored. *) 173 174 definition Z_shift_add ≝ λb: bool. λx: Z. 175 if b then 2 * x + 1 else 2 * x. 176 177 definition Z_bin_decomp : Z → bool × Z ≝ 178 λx.match x with 179 [ OZ ⇒ 〈false, OZ〉 180  pos p ⇒ 181 match p with 182 [ p1 q ⇒ 〈true, pos q〉 183  p0 q ⇒ 〈false, pos q〉 184  one ⇒ 〈true, OZ〉 185 ] 186  neg p ⇒ 187 match p return λ_.bool × Z with 188 [ p1 q ⇒ 〈true, Zpred (neg q)〉 189  p0 q ⇒ 〈false, neg q〉 190  one ⇒ 〈true, neg one〉 191 ] 192 ]. 193 194 let rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝ 195 match n with 196 [ O ⇒ λi:Z. false 197  S m ⇒ 198 match Z_bin_decomp x with [ pair b y ⇒ 199 let f ≝ bits_of_Z m y in 200 λi:Z. if eqZb i 0 then b else f (Zpred i) ] 201 ]. 202 203 let rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝ 204 match n with 205 [ O ⇒ OZ 206  S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i))) 207 ]. 138 definition mul ≝ λx,y. \snd (split ? wordsize wordsize (multiplication wordsize x y)). 139 140 definition zero_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝ 141 λw,n. 142 match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with 143 [ nat_lt n' w' ⇒ λi. 144 let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in 145 switch_bv_plus ??? (pad ?? l) 146  _ ⇒ λi.i 147 ]. 148 149 definition zero_ext : nat → int → int ≝ zero_ext_n wordsize. 150 151 definition sign_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝ 152 λw,n. 153 match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with 154 [ nat_lt n' w' ⇒ λi. 155 let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in 156 switch_bv_plus ??? (pad_vector ? (match l with [ VEmpty ⇒ false  VCons _ h _ ⇒ h ]) ?? l) 157  _ ⇒ λi.i 158 ]. 159 160 definition sign_ext : nat → int → int ≝ sign_ext_n wordsize. 208 161 209 162 (* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *) 210 163 211 definition bitwise_binop ≝ λf: bool > bool > bool. λx,y: int.212 let fx ≝ bits_of_Z wordsize (unsigned x) in213 let fy ≝ bits_of_Z wordsize (unsigned y) in214 repr (Z_of_bits wordsize (λi. f (fx i) (fy i))).215 164 216 165 definition i_and : int → int → int ≝ conjunction_bv wordsize. … … 222 171 (* * Shifts and rotates. *) 223 172 224 definition shl : int → int → int ≝ λx,y. 225 let fx ≝ bits_of_Z wordsize (unsigned x) in 226 let vy ≝ unsigned y in 227 repr (Z_of_bits wordsize (λi. fx (i  vy))). 228 229 definition shru : int → int → int ≝ λx,y. 230 let fx ≝ bits_of_Z wordsize (unsigned x) in 231 let vy ≝ unsigned y in 232 repr (Z_of_bits wordsize (λi. fx (i + vy))). 173 definition shl : int → int → int ≝ λx,y. shift_left ?? (nat_of_bitvector … y) x false. 174 definition shru : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x false. 233 175 234 176 (* * Arithmetic right shift is defined as signed division by a power of two. … … 237 179 [shrx] rounds towards zero. *) 238 180 239 definition shr : int → int → int ≝ λx,y. 240 repr (signed x / two_p (unsigned y)). 241 181 definition shr : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x (head' … x). 242 182 definition shrx : int → int → int ≝ λx,y. 243 divs x (shl one y).183 match division_s ? x (shl one y) with [ None ⇒ zero  Some i ⇒ i ]. 244 184 245 185 definition shr_carry ≝ λx,y: int. 246 sub (shrx x y) (shr x y). 247 248 definition rol : int → int → int ≝ λx,y. 249 let fx ≝ bits_of_Z wordsize (unsigned x) in 250 let vy ≝ unsigned y in 251 repr (Z_of_bits wordsize 252 (λi. fx (i  vy \mod Z_of_nat wordsize))). 253 254 definition ror : int → int → int ≝ λx,y. 255 let fx := bits_of_Z wordsize (unsigned x) in 256 let vy := unsigned y in 257 repr (Z_of_bits wordsize 258 (λi. fx (i + vy \mod Z_of_nat wordsize))). 186 subtraction ? (shrx x y) (shr x y). 187 188 definition rol : int → int → int ≝ λx,y. rotate_left ?? (nat_of_bitvector ? y) x. 189 definition ror : int → int → int ≝ λx,y. rotate_right ?? (nat_of_bitvector ? y) x. 259 190 260 191 definition rolm ≝ λx,a,m: int. i_and (rol x a) m. … … 487 418 *) 488 419 theorem one_not_zero: one ≠ zero. 489 % #H 490 lapply (refl ? (get_index' ? 31 0 one)) 491 >H in ⊢ (???% → ?) 492 normalize #E destruct 420 % #H @(match eq_dec one zero return λx.match x with [ inl _ ⇒ True  inr _ ⇒ False ] with [ inl _ ⇒ I  inr p ⇒ ?]) normalize 421 cases p #H' @(H' H) 493 422 qed. 494 423 … … 705 634 Qed. 706 635 *) 707 636 (* 708 637 theorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus. 709 638 #i @intrange … … 2710 2639 2711 2640 2641 *)
Note: See TracChangeset
for help on using the changeset viewer.