hackers-delight.mlw 11.2 KB
Newer Older
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
8
  use import bv.BV32
9

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 =
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))
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
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.
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

Clément Fumex's avatar
Clément Fumex committed
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
  use import int.NumOf

  lemma tointzero: to_uint zero = 0
  lemma tointone: to_uint one = 1

  lemma numOfZero: NumOf.numof (\i. nth zero i) 0 32 = 0

  lemma numof_change_equiv:
    forall p1 p2: int -> bool, a b: int.
    (forall j: int. a <= j < b -> p1 j <-> p2 j) ->
    numof p2 a b = numof p1 a b

  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


  let rec lemma countAux (bv : t) : unit
  variant {bv with ult}
  ensures {to_uint (count bv) = NumOf.numof (nth bv) 0 32}
  =
    if bv = zero then ()
    else
    begin
      countAux (lsr_bv bv one);
      assert {
                 let x = (if nth_bv bv zero then 1 else 0) in
                  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

  lemma countSpec: forall b. to_uint (count b) = NumOf.numof
        (nth b) 0 32

99 100 101 102 103 104
  (** 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)

Clément Fumex's avatar
Clément Fumex committed
105 106 107 108 109 110 111 112 113 114 115
  predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i

  use HighOrd as HO

  function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x

  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) }

116 117 118 119 120 121
  (** 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

Clément Fumex's avatar
Clément Fumex committed
122 123 124 125 126 127 128 129 130 131 132 133 134 135
  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)}
  =
    assert {numof (nth_diff a b) 0 32 + numof (nth_diff b c) 0 32 >=
    numof (fun_or (nth_diff a b) (nth_diff b c)) 0 32 >=
    numof (nth_diff a c) 0 32}

136 137 138
  lemma triangleInequality: forall a b c. (* not proved ! :-( *)
    uge (add (hammingD a b) (hammingD b c)) (hammingD a c)

Clément Fumex's avatar
Clément Fumex committed
139

140 141 142 143 144
  (** {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) *)
145
  predicate validAscii (b : t) = not (nth_bv (count b) zero)
146 147 148 149 150 151

  (** 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) =
152
    requires { not (nth_bv b lastbit) }
153 154
    ensures  { validAscii result }
    let c = count b in
155
    bw_or b (lsl_bv c lastbit)
156 157 158 159 160 161 162 163 164 165

  (** 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
166
      validAscii a)) <-> nth_bv (hammingD a b) zero
167 168 169 170 171 172 173 174 175 176 177 178 179

  (** {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 =
180
    bw_xor bv (lsr_bv bv one)
181 182

  function fromGray (gr : t) : t =
183 184 185 186 187
    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))
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210

  (** 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 ->
211
      xorb (nth_bv b i) (nth_bv b (add i one)) <-> nth_bv (toGray b) i
212 213 214 215

  (** (using 0 if there is no bit to the left of i) *)

  lemma lastNthGray: forall b.
216
    nth_bv (toGray b) lastbit <-> nth_bv b lastbit
217 218 219 220 221 222 223

  (** 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 ->
224
      nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zero
225 226 227 228 229 230

  (** 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.
231
    nth_bv b zero <-> nth_bv (count (toGray b)) zero
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 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 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

  (** {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 ->
328 329
    bw_or (lsr_bv x n) (lsl_bv (neg( lsr_bv x (of_int 31) )) (sub (of_int 31) n))
  = asr_bv x n
330 331 332 333

  (** rotate vs shift (p.37)*)

  lemma RS_left: forall x.
334
    bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31)) = rotate_left x one
335 336

  lemma RS_right: forall x.
337
    bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31)) = rotate_right x one
338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353

  (** {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