examples/hackers-delight.mlw

   1 (** {1 Examples from Hacker's Delight book*}
   2
   3     *second edition *)
   4
   5 (** {2 Utilitaries}
   6     We introduce in this theory two functions that will help us
   7     write properties on bit-manipulating procedures *)
   8
   9 theory Utils
  10
  11   use bv.BV32
  12
  13   let constant one : t = (1:t)
  14   let constant two : t = (2:t)
  15   let constant lastbit : t = (31:t)
  16
  17   function max (x y : t) : t = (if ult x y then y else x)
  18   function min (x y : t) : t = (if ult x y then x else y)
  19
  20   (** We start by introducing a function that returns the number of
  21       1-bit in a bitvector (p.82) *)
  22
  23   let function count (bv : t) : t =
  24     let x = sub bv (bw_and (lsr_bv bv one) (0x55555555:t)) in
  25     let x = add (bw_and x (0x33333333:t))
  26                 (bw_and (lsr_bv x two) (0x33333333:t)) in
  27     let x = bw_and (add x (lsr_bv x (4:t)))
  28                    (0x0F0F0F0F:t) in
  29     let x = add x (lsr_bv x (8:t)) in
  30     let x = add x (lsr_bv x (16:t)) in
  31     bw_and x (0x0000003F:t)
  32
  33   (** We then define the associated notion of distance, namely
  34       "Hamming distance", that counts the number of bits that differ
  35       between two bitvectors. *)
  36
  37   function hammingD (a b : t) : t = count (bw_xor a b)
  38
  39 end
  40
  41 (** {2 Correctness of Utils}
  42     Before using our two functions let's first check that they are correct !
  43 *)
  44
  45 module Utils_Spec
  46   use int.Int
  47   use int.NumOf
  48   use bv.BV32
  49   use Utils
  50
  51   (** {6 count correctness } *)
  52
  53   (** Let's start by checking that there are no 1-bits in the
  54       bitvector "zeros": *)
  55
  56   lemma countZero: count zeros = zeros
  57
  58   lemma numOfZero: NumOf.numof (fun i -> nth zeros i) 0 32 = 0
  59
  60   (** Now, for b a bitvector with n 1-bits, we check that if its
  61       first bit is 0 then shifting b by one on the right doesn't
  62       change the number of 1-bit. And if its first bit is one, then
  63       there are n-1 1-bits in the shifting of b by one on the right. *)
  64
  65   lemma countStep: forall b.
  66     (not (nth_bv b zeros) <-> count (lsr_bv b one) = count b) /\
  67     (nth_bv b zeros <-> count (lsr_bv b one) = sub (count b) one)
  68
  69   let rec lemma numof_shift (p q : int -> bool) (a b k: int) : unit
  70     requires {forall i. q i = p (i + k)}
  71     variant {b - a}
  72     ensures {numof p (a+k) (b+k) = numof q a b}
  73   =
  74     if a < b then
  75     numof_shift p q a (b-1) k
  76
  77   let rec lemma countSpec_Aux (bv : t) : unit
  78   variant {t'int bv}
  79   ensures {t'int (count bv) = NumOf.numof (nth bv) 0 32}
  80   =
  81     if pure { bv <> zeros } then
  82     begin
  83       countSpec_Aux (lsr_bv bv one);
  84       assert {
  85                  let x = (if nth_bv bv zeros then 1 else 0) in
  86                   let f = nth bv in
  87                   let g = nth (lsr_bv bv one) in
  88                   let h = fun i -> nth bv (i+1) in
  89                   (forall i. 0 <= i < 31 -> g i = h i) &&
  90                   NumOf.numof f 0 32 - x = NumOf.numof f (0+1) 32 &&
  91                   NumOf.numof f (0+1) (31+1) = NumOf.numof h 0 31 &&
  92                   NumOf.numof g 0 (32-1) = NumOf.numof g 0 32
  93       }
  94     end
  95
  96   (** With these lemmas, we can now prove the correctness property of
  97   count: *)
  98
  99   lemma countSpec: forall b. t'int (count b) = NumOf.numof
 100         (nth b) 0 32
 101
 102   (** {6 hammingD correctness } *)
 103
 104   predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i
 105
 106   (** The correctness property can be express as the following: *)
 107   let lemma hamming_spec (a b : t) : unit
 108   ensures {t'int (hammingD a b) = NumOf.numof (nth_diff a b) 0 32}
 109   =
 110    assert { forall i. 0 <= i < 32 -> nth (bw_xor a b) i <-> (nth_diff a b i) }
 111
 112   (** In addition we can prove that it is indeed a distance in the
 113       algebraic sens: *)
 114
 115   lemma symmetric: forall a b. hammingD a b = hammingD b a
 116
 117   lemma separation: forall a b. hammingD a b = zeros <-> a = b
 118
 119   function fun_or (f g : 'a -> bool) : 'a -> bool = fun x -> f x \/ g x
 120
 121   let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
 122     variant {b - a}
 123     ensures {numof (fun_or p q) a b <= numof p a b + numof q a b}
 124   =
 125     if a < b then
 126     numof_or p q a (b-1)
 127
 128   let lemma triangleInequalityInt (a b c : t) : unit
 129     ensures {t'int (hammingD a b) + t'int (hammingD b c) >= t'int (hammingD a c)}
 130   =
 131     assert {numof (fun_or (nth_diff a b) (nth_diff b c)) 0 32 >= numof (nth_diff a c) 0 32
 132              by
 133             forall j:int. 0 <= j < 32 -> nth_diff a c j -> fun_or (nth_diff a b) (nth_diff b c) j}
 134
 135   lemma triangleInequality: forall a b c.
 136     uge (add (hammingD a b) (hammingD b c)) (hammingD a c)
 137
 138 end
 139
 140 module Hackers_delight
 141   use int.Int
 142   use int.NumOf
 143   use bool.Bool
 144   use bv.BV32
 145   use Utils
 146
 147   (** {2 ASCII checksum }
 148     In the beginning the encoding of an ascii character was done on 8
 149     bits: the first 7 bits were used for the carracter itself while
 150     the 8th bit was used as a checksum: a mean to detect errors. The
 151     checksum value was the binary sum of the 7 other bits, allowing the
 152     detections of any change of an odd number of bits in the initial
 153     value. Let's prove it! *)
 154
 155   (** {6 Checksum computation and correctness } *)
 156
 157   (** A ascii character is valid if its number of bits is even.
 158       (Remember that a binary number is odd if and only if its first
 159       bit is 1) *)
 160   predicate validAscii (b : t) = (nth_bv (count b) zeros) = False
 161
 162   (** The ascii checksum aim is to make any character valid in the
 163       sens that we just defined. One way to implement it is to count
 164       the number of bit of a character encoded in 7 bits, and if this
 165       number is odd, set the 8th bit to 1 if not, do nothing:*)
 166   let ascii (b : t) =
 167     requires { not (nth_bv b lastbit) }
 168     ensures  { validAscii result }
 169     let c = count b in
 170     bw_or b (lsl_bv c lastbit)
 171
 172   (** Now, for the correctness of the checksum :
 173
 174       We prove that two numbers differ by an odd number of bits,
 175       i.e. are of odd hamming distance, iff one is a valid ascii
 176       character while the other is not. This imply that if there is an
 177       odd number of changes on a valid ascii character, the result
 178       will be invalid, hence the validity of the encoding. *)
 179   lemma asciiProp: forall a b.
 180       ((validAscii a /\ not validAscii b) \/ (validAscii b /\ not
 181       validAscii a)) <-> nth_bv (hammingD a b) zeros
 182
 183   (** {2 Gray code}
 184     Gray codes are bit-wise representations of integers with the
 185     property that every integer differs from its predecessor by only
 186     one bit.
 187
 188     In this section we look at the "reflected binary Gray code"
 189     discussed in Chapter 13, p.311.
 190   *)
 191
 192   (** {4 the two transformations, to and from Gray-coded integer } *)
 193
 194   function toGray (bv : t) : t =
 195     bw_xor bv (lsr_bv bv one)
 196
 197   function fromGray (gr : t) : t =
 198     let b = bw_xor gr (lsr_bv gr one) in
 199     let b = bw_xor b (lsr_bv b (2:t)) in
 200     let b = bw_xor b (lsr_bv b (4:t)) in
 201     let b = bw_xor b (lsr_bv b (8:t)) in
 202       bw_xor b (lsr_bv b (16:t))
 203
 204   (** Which define an isomorphism. *)
 205
 206   lemma iso: forall b.
 207     toGray (fromGray b) = b /\ fromGray (toGray b) = b
 208
 209   (** {4 Some properties of the reflected binary Gray code } *)
 210
 211   (** The first property that we want to check is that the reflected
 212      binary Gray code is indeed a Gray code. *)
 213
 214   lemma grayIsGray: forall b.
 215     ult b ones ->
 216       hammingD (toGray b) (toGray (add b one)) = one
 217
 218   (** Now, a couple of property between the Gray code and the binary
 219       representation.
 220
 221       Bit i of a Gray coded integer is the parity of the bit i and the
 222       bit to the left of i in the corresponding binary integer *)
 223
 224   lemma nthGray: forall b i.
 225     ult i lastbit ->
 226       xorb (nth_bv b i) (nth_bv b (add i one)) <-> nth_bv (toGray b) i
 227
 228   (** (using 0 if there is no bit to the left of i) *)
 229
 230   lemma lastNthGray: forall b.
 231     nth_bv (toGray b) lastbit <-> nth_bv b lastbit
 232
 233   (** Bit i of a binary integer is the parity of all the bits at and
 234       to the left of position i in the corresponding Gray coded
 235       integer *)
 236
 237   lemma nthBinary: forall b i.
 238     ult i size_bv ->
 239       nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zeros
 240
 241   (** The last property that we check is that if an integer is even
 242       its encoding has an even number of 1-bits, and if it is odd, its
 243       encoding has an odd number of 1-bits. *)
 244
 245   lemma evenOdd : forall b.
 246     nth_bv b zeros <-> nth_bv (count (toGray b)) zeros
 247
 248   (** {2 Various (in)equalities between bitvectors. } *)
 249
 250   (** {6 De Morgan's laws (p.13)}
 251
 252   Some variations on De Morgan's laws on bitvectors. *)
 253
 254   lemma DM1: forall x y.
 255     bw_not( bw_and x y ) = bw_or (bw_not x) (bw_not y)
 256
 257   lemma DM2: forall x y.
 258     bw_not( bw_or x y ) = bw_and (bw_not x) (bw_not y)
 259
 260   lemma DM3: forall x.
 261     bw_not (add x one) = sub (bw_not x) one
 262
 263   lemma DM4: forall x.
 264     bw_not( sub x one) = add (bw_not x) one
 265
 266   lemma DM5: forall x.
 267     bw_not( neg x ) = sub x one
 268
 269   lemma DM6: forall x y.
 270     bw_not( bw_xor x y ) = bw_xor (bw_not x) y
 271
 272   lemma DM7: forall x y.
 273     bw_not( add x y ) = sub (bw_not x) y
 274
 275   lemma DM8: forall x y.
 276     bw_not( sub x y ) = add (bw_not x) y
 277
 278   lemma DMtest: forall x.
 279     zeros = bw_not( bw_or x (neg(add x one)))
 280
 281   (** {6 Addition Combined with Logical Operations (p.16)} *)
 282
 283   lemma Aa: forall x.
 284     neg x = add (bw_not x) one
 285
 286   lemma Ac: forall x.
 287     bw_not x = sub (neg x) one
 288
 289   lemma Ad: forall x.
 290     neg (bw_not x) = add x one
 291
 292   lemma Ae: forall x.
 293     bw_not (neg x) = sub x one
 294
 295   lemma Af: forall x y.
 296     add x y = sub x (add (bw_not y) one)
 297
 298   lemma Aj: forall x y.
 299     sub x y = add x (add (bw_not y) one)
 300
 301   lemma An: forall x y.
 302     bw_xor x y = sub (bw_or x y) (bw_and x y)
 303
 304   lemma Ao: forall x y.
 305     bw_and x (bw_not y) = sub (bw_or x y) y
 306
 307   lemma Aq: forall x y.
 308     bw_not (sub x y) = sub y (add x one)
 309
 310   lemma At: forall x y.
 311     not (bw_xor x y) = add (bw_and x y) (bw_not (bw_or x y))
 312
 313   lemma Au: forall x y.
 314     bw_or x y = add (bw_and x (bw_not y)) y
 315
 316   lemma Av: forall x y.
 317     bw_and x y = sub (bw_or (bw_not x) y) (bw_not x)
 318
 319   (** {6 Inequalities (p. 17, 18)} *)
 320
 321   lemma IE1: forall x y.
 322     ule (bw_xor x y) (bw_or x y)
 323
 324   lemma IE2: forall x y.
 325     ule (bw_and x y) (bw_not( bw_xor x y ))
 326
 327   lemma IEa: forall x y.
 328     uge (bw_or x y) (max x y)
 329
 330   lemma IEb: forall x y.
 331     ule (bw_and x y) (min x y)
 332
 333   lemma IE3: forall x y.
 334     ( ule x (add x y) /\ ule y (add x y) ) -> ule (bw_or x y) (add x y)
 335
 336   lemma IE4: forall x y.
 337     not ( ule x (add x y) /\ ule y (add x y) ) -> ugt (bw_or x y) (add x y)
 338
 339   (** {6 Shifts and rotates} *)
 340   (** shift right and arithmetic shift right (p.20)*)
 341
 342   lemma SR1: forall x n. ult n size_bv ->
 343     bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (31:t) )) (sub (31:t) n))
 344   = asr_bv x n
 345
 346   (** rotate vs shift (p.37)*)
 347
 348   lemma RS_left: forall x.
 349     bw_or (lsl_bv x one) (lsr_bv x (31:t)) = rotate_left_bv x one
 350
 351   lemma RS_right: forall x.
 352     bw_or (lsr_bv x one) (lsl_bv x (31:t)) = rotate_right_bv x one
 353
 354   (** {6 bound propagation (p.73)} *)
 355
 356   (** Using a predicate to check if an addition of bitvector overflowed *)
 357   predicate addDontOverflow (a b : t) = ule b (add b a) /\ ule a (add b a)
 358
 359   (** We have that. *)
 360   lemma BP: forall a b c d x y.
 361     ( ule a x /\ ule x b /\ ule c y /\ ule y d ) ->                 (*  a <= x <= b   and   c <= y <= d  *)
 362     addDontOverflow b d ->
 363       ule (max a c) (bw_or x y) /\ ule (bw_or x y) (add b d) /\     (* max a c  <=   x | y   <=   b + d  *)
 364       ule zeros (bw_and x y) /\ ule (bw_and x y) (min b d) /\       (*    0     <=   x & y   <=  min b d *)
 365       ule zeros (bw_xor x y) /\ ule (bw_xor x y) (add b d) /\       (*    0     <=  x xor y  <=   b + d  *)
 366       ule (bw_not b) (bw_not x) /\ ule (bw_not x) (bw_not a)        (*  not b   <=   not x   <=   not a  *)
 367
 368 end