hackers-delight.mlw 11.5 KB
Newer Older
1 2 3 4
(** {1 Examples from Hacker's Delight book*}

    *second edition *)

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

11
  use import bv.BV32
12

13
  constant one : t = of_int 1
14 15 16 17 18 19
  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)

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

33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
  (** 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
      bitvector "zero": *)
55 56 57

  lemma countZero: count zero = zero

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

  (** 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.
66 67
    (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)
68

Clément Fumex's avatar
Clément Fumex committed
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

77
  let rec lemma countSpec_Aux (bv : t) : unit
Clément Fumex's avatar
Clément Fumex committed
78 79 80 81 82 83
  variant {bv with ult}
  ensures {to_uint (count bv) = NumOf.numof (nth bv) 0 32}
  =
    if bv = zero then ()
    else
    begin
84
      countSpec_Aux (lsr_bv bv one);
Clément Fumex's avatar
Clément Fumex committed
85 86 87 88 89 90 91 92 93 94 95 96
      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

97 98 99
  (** With these lemmas, we can now prove the correctness property of
  count: *)

Clément Fumex's avatar
Clément Fumex committed
100 101 102
  lemma countSpec: forall b. to_uint (count b) = NumOf.numof
        (nth b) 0 32

103
  (** {6 hammingD correctness } *)
Clément Fumex's avatar
Clément Fumex committed
104 105 106

  use HighOrd as HO

107
  predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i
Clément Fumex's avatar
Clément Fumex committed
108

109
  (** The correctness property can be express as the following: *)
Clément Fumex's avatar
Clément Fumex committed
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) }

115 116
  (** In addition we can prove that it is indeed a distance in the
      algebraic sens: *)
117 118 119 120 121

  lemma symmetric: forall a b. hammingD a b = hammingD b a

  lemma separation: forall a b. hammingD a b = zero <-> a = b

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

Clément Fumex's avatar
Clément Fumex committed
124 125 126 127 128 129 130 131 132 133 134 135 136 137
  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}

138
  lemma triangleInequality: forall a b c.
139 140
    uge (add (hammingD a b) (hammingD b c)) (hammingD a c)

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's avatar
Clément Fumex committed
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) *)
163
  predicate validAscii (b : t) = (nth_bv (count b) zero) = 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) =
170
    requires { not (nth_bv b lastbit) }
171 172
    ensures  { validAscii result }
    let c = count b in
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
184
      validAscii a)) <-> nth_bv (hammingD a b) zero
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 =
198
    bw_xor bv (lsr_bv bv one)
199 200

  function fromGray (gr : t) : t =
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 ->
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.
234
    nth_bv (toGray b) lastbit <-> nth_bv b lastbit
235 236 237 238 239 240 241

  (** 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 ->
242
      nth_bv (fromGray b) i <-> nth_bv (count (lsr_bv b i)) zero
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.
249
    nth_bv b zero <-> nth_bv (count (toGray b)) zero
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 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345

  (** {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 ->
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.
352
    bw_or (lsl_bv x (of_int 1)) (lsr_bv x (of_int 31)) = rotate_left x one
353 354

  lemma RS_right: forall x.
355
    bw_or (lsr_bv x (of_int 1)) (lsl_bv x (of_int 31)) = rotate_right x one
356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371

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