hackers-delight.mlw 9.04 KB
 1 2 3 4 5 6 7 ``````(** {1 Examples from Hacker's Delight book*} *second edition *) module Hackers_delight use import int.Int use import bool.Bool `````` Clément Fumex committed Apr 16, 2015 8 `````` use import bv.BV32 `````` 9 `````` `````` Clément Fumex committed Apr 16, 2015 10 `````` constant one : t = of_int 1 `````` 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 `````` constant two : t = of_int 2 constant lastbit : t = sub size one function max (x y : t) : t = (if ult x y then y else x) function min (x y : t) : t = (if ult x y then x else y) (** {2 ASCII cheksum } In the beginning the encoding of an ascii character was done on 8 bits: the first 7 bits were used for the carracter itself while the 8th bit was used as a cheksum: a mean to detect errors. The cheksum value was the binary sum of the 7 other bits, allowing the detections of any change of an odd number of bits in the initial value. Let's prove it! *) (** {6 Hamming distance } *) (** In order to express these properties we start by introducing a function that returns the number of 1-bit in a bitvector (p.82) *) function count (bv : t) : t = `````` Clément Fumex committed Apr 16, 2015 32 `````` let x = sub bv (bw_and (lsr_bv bv one) (of_int 0x55555555)) in `````` 33 `````` let x = add (bw_and x (of_int 0x33333333)) `````` Clément Fumex committed Apr 16, 2015 34 35 `````` (bw_and (lsr_bv x (of_int 2)) (of_int (0x33333333))) in let x = bw_and (add x (lsr_bv x (of_int 4))) `````` 36 `````` (of_int 0x0F0F0F0F) in `````` Clément Fumex committed Apr 16, 2015 37 38 `````` let x = add x (lsr_bv x (of_int 8)) in let x = add x (lsr_bv x (of_int 16)) in `````` 39 40 41 42 43 44 45 46 47 48 49 50 51 `````` bw_and x (of_int 0x0000003F) (** We can verify our definition by, first, checking that there are no 1-bits in the bitvector "zero": *) lemma countZero: count zero = zero (** And then, for b a bitvector with n 1-bits, checking that if its first bit is 0 then shifting b by one on the right doesn't change the number of 1-bit. And if its first bit is one, then there are n-1 1-bits in the shifting of b by one on the right. *) lemma countStep: forall b. `````` Clément Fumex committed Apr 16, 2015 52 53 `````` (not (nth_bv b zero) <-> count (lsr_bv b one) = count b) /\ (nth_bv b zero <-> count (lsr_bv b one) = sub (count b) one) `````` 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 `````` (** We then define the associated notion of distance, namely "Hamming distance", that counts the number of bits that differ between two bitvectors. *) function hammingD (a b : t) : t = count (bw_xor a b) (** It is indeed a distance in the algebraic sense: *) lemma symmetric: forall a b. hammingD a b = hammingD b a lemma separation: forall a b. hammingD a b = zero <-> a = b lemma triangleInequality: forall a b c. (* not proved ! :-( *) uge (add (hammingD a b) (hammingD b c)) (hammingD a c) (** {6 Checksum computation and correctness } *) (** A ascii character is valid if its number of bits is even. (Remember that a binary number is odd if and only if its first bit is 1) *) `````` Clément Fumex committed Apr 16, 2015 75 `````` predicate validAscii (b : t) = not (nth_bv (count b) zero) `````` 76 77 78 79 80 81 `````` (** The ascii checksum aim is to make any character valid in the sens that we just defined. One way to implement it is to count the number of bit of a character encoded in 7 bits, and if this number is odd, set the 8th bit to 1 if not, do nothing:*) let ascii (b : t) = `````` Clément Fumex committed Apr 16, 2015 82 `````` requires { not (nth_bv b lastbit) } `````` 83 84 `````` ensures { validAscii result } let c = count b in `````` Clément Fumex committed Apr 16, 2015 85 `````` bw_or b (lsl_bv c lastbit) `````` 86 87 88 89 90 91 92 93 94 95 `````` (** Now, for the correctness of the checksum : We prove that two numbers differ by an odd number of bits, i.e. are of odd hamming distance, iff one is a valid ascii character while the other is not. This imply that if there is an odd number of changes on a valid ascii character, the result will be invalid, hence the validity of the encoding. *) lemma asciiProp: forall a b. ((validAscii a /\ not validAscii b) \/ (validAscii b /\ not `````` Clément Fumex committed Apr 16, 2015 96 `````` validAscii a)) <-> nth_bv (hammingD a b) zero `````` 97 98 99 100 101 102 103 104 105 106 107 108 109 `````` (** {2 Gray code} Gray codes are bit-wise representations of integers with the property that every integer differs from its predecessor by only one bit. In this section we look at the "reflected binary Gray code" discussed in Chapter 13, p.311. *) (** {4 the two transformations, to and from Gray-coded integer } *) function toGray (bv : t) : t = `````` Clément Fumex committed Apr 16, 2015 110 `````` bw_xor bv (lsr_bv bv one) `````` 111 112 `````` function fromGray (gr : t) : t = `````` Clément Fumex committed Apr 16, 2015 113 114 115 116 117 `````` let b = bw_xor gr (lsr_bv gr (of_int 1)) in let b = bw_xor b (lsr_bv b (of_int 2)) in let b = bw_xor b (lsr_bv b (of_int 4)) in let b = bw_xor b (lsr_bv b (of_int 8)) in bw_xor b (lsr_bv b (of_int 16)) `````` 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 `````` (** Which define an isomorphism. *) lemma iso: forall b. toGray (fromGray b) = b /\ fromGray (toGray b) = b (** {4 Some properties of the reflected binary Gray code } *) (** The first property that we want to check is that the reflected binary Gray code is indeed a Gray code. *) lemma grayIsGray: forall b. ult b ones -> hammingD (toGray b) (toGray (add b one)) = one (** Now, a couple of property between the Gray code and the binary representation. Bit i of a Gray coded integer is the parity of the bit i and the bit to the left of i in the corresponding binary integer *) lemma nthGray: forall b i. ult i lastbit -> `````` Clément Fumex committed Apr 16, 2015 141 `````` xorb (nth_bv b i) (nth_bv b (add i one)) <-> nth_bv (toGray b) i `````` 142 143 144 145 `````` (** (using 0 if there is no bit to the left of i) *) lemma lastNthGray: forall b. `````` Clément Fumex committed Apr 16, 2015 146 `````` nth_bv (toGray b) lastbit <-> nth_bv b lastbit `````` 147 148 149 150 151 152 153 `````` (** Bit i of a binary integer is the parity of all the bits at and to the left of position i in the corresponding Gray coded integer *) lemma nthBinary: forall b i. ult i size -> `````` Clément Fumex committed Apr 16, 2015 154 `````` nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zero `````` 155 156 157 158 159 160 `````` (** The last property that we check is that if an integer is even its encoding has an even number of 1-bits, and if it is odd, its encoding has an odd number of 1-bits. *) lemma evenOdd : forall b. `````` Clément Fumex committed Apr 16, 2015 161 `````` nth_bv b zero <-> nth_bv (count (toGray b)) zero `````` 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 `````` (** {2 Various (in)equalities between bitvectors. } *) (** {6 De Morgan's laws (p.13)} Some variations on De Morgan's laws on bitvectors. *) lemma DM1: forall x y. bw_not( bw_and x y ) = bw_or (bw_not x) (bw_not y) lemma DM2: forall x y. bw_not( bw_or x y ) = bw_and (bw_not x) (bw_not y) lemma DM3: forall x. bw_not( add x (of_int 1) ) = sub (bw_not x) (of_int 1) lemma DM4: forall x. bw_not( sub x (of_int 1) ) = add (bw_not x) (of_int 1) lemma DM5: forall x. bw_not( neg x ) = sub x (of_int 1) lemma DM6: forall x y. bw_not( bw_xor x y ) = bw_xor (bw_not x) y lemma DM7: forall x y. bw_not( add x y ) = sub (bw_not x) y lemma DM8: forall x y. bw_not( sub x y ) = add (bw_not x) y lemma DMtest: forall x. zero = bw_not( bw_or x (neg( add x (of_int 1)))) (** {6 Addition Combined with Logical Operations (p.16)} *) lemma Aa: forall x. neg x = add (bw_not x) one lemma Ac: forall x. bw_not x = sub (neg x) one lemma Ad: forall x. neg (bw_not x) = add x one lemma Ae: forall x. bw_not (neg x) = sub x one lemma Af: forall x y. add x y = sub x (add (bw_not y) one) lemma Aj: forall x y. sub x y = add x (add (bw_not y) one) lemma An: forall x y. bw_xor x y = sub (bw_or x y) (bw_and x y) lemma Ao: forall x y. bw_and x (bw_not y) = sub (bw_or x y) y lemma Aq: forall x y. bw_not (sub x y) = sub y (add x one) lemma At: forall x y. not (bw_xor x y) = add (bw_and x y) (bw_not (bw_or x y)) lemma Au: forall x y. bw_or x y = add (bw_and x (bw_not y)) y lemma Av: forall x y. bw_and x y = sub (bw_or (bw_not x) y) (bw_not x) (** {6 Inequalities (p. 17, 18)} *) lemma IE1: forall x y. ule (bw_xor x y) (bw_or x y) lemma IE2: forall x y. ule (bw_and x y) (bw_not( bw_xor x y )) lemma IEa: forall x y. uge (bw_or x y) (max x y) lemma IEb: forall x y. ule (bw_and x y) (min x y) lemma IE3: forall x y. ( ule x (add x y) /\ ule y (add x y) ) -> ule (bw_or x y) (add x y) lemma IE4: forall x y. not ( ule x (add x y) /\ ule y (add x y) ) -> ugt (bw_or x y) (add x y) (** {6 Shifts and rotates} *) (** shift right and arithmetic shift right (p.20)*) lemma SR1: forall x n. ult n size -> `````` Clément Fumex committed Apr 16, 2015 258 259 `````` bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (of_int 31) )) (sub (of_int 31) n)) = asr_bv x n `````` 260 261 262 263 `````` (** rotate vs shift (p.37)*) lemma RS_left: forall x. `````` Clément Fumex committed Apr 16, 2015 264 `````` bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31)) = rotate_left x one `````` 265 266 `````` lemma RS_right: forall x. `````` Clément Fumex committed Apr 16, 2015 267 `````` bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31)) = rotate_right x one `````` 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 `````` (** {6 bound propagation (p.73)} *) (** Using a predicate to check if an addition of bitvector overflowed *) predicate addDontOverflow (a b : t) = ule b (add b a) /\ ule a (add b a) (** We have that. *) lemma BP: forall a b c d x y. ( ule a x /\ ule x b /\ ule c y /\ ule y d ) -> (* a <= x <= b and c <= y <= d *) addDontOverflow b d -> ule (max a c) (bw_or x y) /\ ule (bw_or x y) (add b d) /\ (* max a c <= x | y <= b + d *) ule zero (bw_and x y) /\ ule (bw_and x y) (min b d) /\ (* 0 <= x & y <= min b d *) ule zero (bw_xor x y) /\ ule (bw_xor x y) (add b d) /\ (* 0 <= x xor y <= b + d *) ule (bw_not b) (bw_not x) /\ ule (bw_not x) (bw_not a) (* not b <= not x <= not a *) end``````