hackers-delight.mlw 11.6 KB
 1 2 3 4 ``````(** {1 Examples from Hacker's Delight book*} *second edition *) `````` Clément Fumex committed Jun 02, 2015 5 6 7 8 9 10 ``````(** {2 Utilitaries} We introduce in this theory two functions that will help us write properties on bit-manipulating procedures *) theory Utils `````` Clément Fumex committed Apr 16, 2015 11 `````` use import bv.BV32 `````` 12 `````` `````` Clément Fumex committed Apr 16, 2015 13 `````` constant one : t = of_int 1 `````` 14 `````` constant two : t = of_int 2 `````` Clément Fumex committed Oct 07, 2015 15 `````` constant lastbit : t = sub size_bv one `````` 16 17 18 19 `````` 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) `````` Clément Fumex committed Jun 02, 2015 20 21 `````` (** We start by introducing a function that returns the number of 1-bit in a bitvector (p.82) *) `````` 22 23 `````` function count (bv : t) : t = `````` Clément Fumex committed Apr 16, 2015 24 `````` let x = sub bv (bw_and (lsr_bv bv one) (of_int 0x55555555)) in `````` 25 `````` let x = add (bw_and x (of_int 0x33333333)) `````` Clément Fumex committed Apr 16, 2015 26 27 `````` (bw_and (lsr_bv x (of_int 2)) (of_int (0x33333333))) in let x = bw_and (add x (lsr_bv x (of_int 4))) `````` 28 `````` (of_int 0x0F0F0F0F) in `````` Clément Fumex committed Apr 16, 2015 29 30 `````` let x = add x (lsr_bv x (of_int 8)) in let x = add x (lsr_bv x (of_int 16)) in `````` 31 32 `````` bw_and x (of_int 0x0000003F) `````` Clément Fumex committed Jun 02, 2015 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 `````` (** 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) end (** {2 Correctness of Utils} Before using our two functions let's first check that they are correct ! *) module Utils_Spec use import int.Int use import int.NumOf use import bv.BV32 use import Utils (** {6 count correctness } *) (** Let's start by checking that there are no 1-bits in the `````` Clément Fumex committed Jan 28, 2016 54 `````` bitvector "zeros": *) `````` 55 `````` `````` Clément Fumex committed Jan 28, 2016 56 `````` lemma countZero: count zeros = zeros `````` 57 `````` `````` Clément Fumex committed Jan 28, 2016 58 `````` lemma numOfZero: NumOf.numof (\i. nth zeros i) 0 32 = 0 `````` Clément Fumex committed Jun 02, 2015 59 60 `````` (** Now, for b a bitvector with n 1-bits, we check that if its `````` 61 62 63 64 65 `````` 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 Jan 28, 2016 66 67 `````` (not (nth_bv b zeros) <-> count (lsr_bv b one) = count b) /\ (nth_bv b zeros <-> count (lsr_bv b one) = sub (count b) one) `````` 68 `````` `````` Clément Fumex committed May 28, 2015 69 70 71 72 73 74 75 76 `````` let rec lemma numof_shift (p q : int -> bool) (a b k: int) : unit requires {forall i. q i = p (i + k)} variant {b - a} ensures {numof p (a+k) (b+k) = numof q a b} = if a < b then numof_shift p q a (b-1) k `````` Clément Fumex committed Jun 02, 2015 77 `````` let rec lemma countSpec_Aux (bv : t) : unit `````` Clément Fumex committed May 28, 2015 78 79 80 `````` variant {bv with ult} ensures {to_uint (count bv) = NumOf.numof (nth bv) 0 32} = `````` Clément Fumex committed Jan 28, 2016 81 `````` if bv = zeros then () `````` Clément Fumex committed May 28, 2015 82 83 `````` else begin `````` Clément Fumex committed Jun 02, 2015 84 `````` countSpec_Aux (lsr_bv bv one); `````` Clément Fumex committed May 28, 2015 85 `````` assert { `````` Clément Fumex committed Jan 28, 2016 86 `````` let x = (if nth_bv bv zeros then 1 else 0) in `````` Clément Fumex committed May 28, 2015 87 88 89 90 91 92 93 94 95 96 `````` let f = nth bv in let g = nth (lsr_bv bv one) in let h = \i. nth bv (i+1) in (forall i. 0 <= i < 31 -> g i = h i) && NumOf.numof f 0 32 - x = NumOf.numof f (0+1) 32 && NumOf.numof f (0+1) (31+1) = NumOf.numof h 0 31 && NumOf.numof g 0 (32-1) = NumOf.numof g 0 32 } end `````` Clément Fumex committed Jun 02, 2015 97 98 99 `````` (** With these lemmas, we can now prove the correctness property of count: *) `````` Clément Fumex committed May 28, 2015 100 101 102 `````` lemma countSpec: forall b. to_uint (count b) = NumOf.numof (nth b) 0 32 `````` Clément Fumex committed Jun 02, 2015 103 `````` (** {6 hammingD correctness } *) `````` Clément Fumex committed May 28, 2015 104 105 106 `````` use HighOrd as HO `````` Clément Fumex committed Jun 02, 2015 107 `````` predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i `````` Clément Fumex committed May 28, 2015 108 `````` `````` Clément Fumex committed Jun 02, 2015 109 `````` (** The correctness property can be express as the following: *) `````` Clément Fumex committed May 28, 2015 110 111 112 113 114 `````` let lemma hamming_spec (a b : t) : unit ensures {to_uint (hammingD a b) = NumOf.numof (nth_diff a b) 0 32} = assert { forall i. 0 <= i < 32 -> nth (bw_xor a b) i <-> (nth_diff a b i) } `````` Clément Fumex committed Jun 02, 2015 115 116 `````` (** In addition we can prove that it is indeed a distance in the algebraic sens: *) `````` 117 118 119 `````` lemma symmetric: forall a b. hammingD a b = hammingD b a `````` Clément Fumex committed Jan 28, 2016 120 `````` lemma separation: forall a b. hammingD a b = zeros <-> a = b `````` 121 `````` `````` Clément Fumex committed Jun 02, 2015 122 123 `````` function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x `````` Clément Fumex committed May 28, 2015 124 125 126 127 128 129 130 131 132 133 `````` let rec lemma numof_or (p q : int -> bool) (a b: int) : unit variant {b - a} ensures {numof (fun_or p q) a b <= numof p a b + numof q a b} = if a < b then numof_or p q a (b-1) let lemma triangleInequalityInt (a b c : t) : unit ensures {to_uint (hammingD a b) + to_uint (hammingD b c) >= to_uint (hammingD a c)} = `````` Clément Fumex committed Jan 26, 2016 134 135 136 `````` assert {numof (fun_or (nth_diff a b) (nth_diff b c)) 0 32 >= numof (nth_diff a c) 0 32 by forall j:int. 0 <= j < 32 -> nth_diff a c j -> fun_or (nth_diff a b) (nth_diff b c) j} `````` Clément Fumex committed May 28, 2015 137 `````` `````` Clément Fumex committed Jun 02, 2015 138 `````` lemma triangleInequality: forall a b c. `````` 139 140 `````` uge (add (hammingD a b) (hammingD b c)) (hammingD a c) `````` Clément Fumex committed Jun 02, 2015 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 ``````end module Hackers_delight use import int.Int use import int.NumOf use import bool.Bool use import bv.BV32 use import Utils (** {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! *) `````` Clément Fumex committed May 28, 2015 157 `````` `````` 158 159 160 161 162 `````` (** {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 Jan 28, 2016 163 `````` predicate validAscii (b : t) = (nth_bv (count b) zeros) = False `````` 164 165 166 167 168 169 `````` (** 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 170 `````` requires { not (nth_bv b lastbit) } `````` 171 172 `````` ensures { validAscii result } let c = count b in `````` Clément Fumex committed Apr 16, 2015 173 `````` bw_or b (lsl_bv c lastbit) `````` 174 175 176 177 178 179 180 181 182 183 `````` (** 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 Jan 28, 2016 184 `````` validAscii a)) <-> nth_bv (hammingD a b) zeros `````` 185 186 187 188 189 190 191 192 193 194 195 196 197 `````` (** {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 198 `````` bw_xor bv (lsr_bv bv one) `````` 199 200 `````` function fromGray (gr : t) : t = `````` Clément Fumex committed Apr 16, 2015 201 202 203 204 205 `````` 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)) `````` 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 `````` (** 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 229 `````` xorb (nth_bv b i) (nth_bv b (add i one)) <-> nth_bv (toGray b) i `````` 230 231 232 233 `````` (** (using 0 if there is no bit to the left of i) *) lemma lastNthGray: forall b. `````` Clément Fumex committed Apr 16, 2015 234 `````` nth_bv (toGray b) lastbit <-> nth_bv b lastbit `````` 235 236 237 238 239 240 `````` (** 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. `````` Clément Fumex committed Oct 07, 2015 241 `````` ult i size_bv -> `````` Clément Fumex committed Jan 28, 2016 242 `````` nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zeros `````` 243 244 245 246 247 248 `````` (** 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 Jan 28, 2016 249 `````` nth_bv b zeros <-> nth_bv (count (toGray b)) zeros `````` 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 `````` (** {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. `````` Clément Fumex committed Jan 28, 2016 282 `````` zeros = bw_not( bw_or x (neg( add x (of_int 1)))) `````` 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 `````` (** {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)*) `````` Clément Fumex committed Oct 07, 2015 345 `````` lemma SR1: forall x n. ult n size_bv -> `````` Clément Fumex committed Apr 16, 2015 346 347 `````` bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (of_int 31) )) (sub (of_int 31) n)) = asr_bv x n `````` 348 349 350 351 `````` (** rotate vs shift (p.37)*) lemma RS_left: forall x. `````` MARCHE Claude committed Nov 19, 2015 352 `````` bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31)) = rotate_left_bv x one `````` 353 354 `````` lemma RS_right: forall x. `````` MARCHE Claude committed Nov 19, 2015 355 `````` bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31)) = rotate_right_bv x one `````` 356 357 358 359 360 361 362 363 364 365 366 `````` (** {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 *) `````` Clément Fumex committed Jan 28, 2016 367 368 `````` ule zeros (bw_and x y) /\ ule (bw_and x y) (min b d) /\ (* 0 <= x & y <= min b d *) ule zeros (bw_xor x y) /\ ule (bw_xor x y) (add b d) /\ (* 0 <= x xor y <= b + d *) `````` 369 370 371 `````` ule (bw_not b) (bw_not x) /\ ule (bw_not x) (bw_not a) (* not b <= not x <= not a *) end``````