Wiki Agenda Contact Version française

Counting bits in a bit vector

Computing the number of bits in a bit vector, and various applications. This case study is detailed in Inria research report 8821.


Authors: Clément Fumex / Claude Marché

Topics: Ghost code / Bitwise operations

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


module BitCount8bit_fact

  use import int.Int
  use import int.NumOf
  use import bv.BV8
  use import ref.Ref

  function nth_as_bv (a i : t) : t =
    if nth_bv a i
    then (of_int 1)
    else zeros

  function nth_as_int (a : t) (i : int) : int =
    if nth a i
    then 1
    else 0

  lemma nth_as_bv_is_int : forall a i.
    to_uint (nth_as_bv a i) = nth_as_int a (to_uint i)

    use import int.EuclideanDivision

  let ghost step1 (n x1 : t) (i : int) : unit
    requires { 0 <= i < 4 }
    requires { x1 = sub n (bw_and (lsr_bv n (of_int 1)) (of_int 0x55)) }
    ensures { to_uint (bw_and (lsr x1 (2*i)) (of_int 0x03))
            = numof (nth n) (2*i) (2*i + 2) }
    ensures { ule (bw_and (lsr x1 (2*i)) (of_int 0x03)) (of_int 2) }
  =
    assert { let i' = of_int i in
             let twoi = mul (of_int 2) i' in
                 bw_and (lsr_bv x1 twoi) (of_int 0x03)
               = add (nth_as_bv n twoi) (nth_as_bv n (add twoi (of_int 1)))
             &&
                 to_uint (bw_and (lsr_bv x1 twoi) (of_int 0x03))
               = numof (nth n) (to_uint twoi) (to_uint twoi + 2) }

  let ghost step2 (n x1 x2 : t) (i : int) : unit
    requires { 0 <= i < 2 }
    requires { x1 = sub n (bw_and (lsr_bv n (of_int 1)) (of_int 0x55)) }
    requires { x2 = add
               (bw_and x1 (of_int 0x33))
               (bw_and (lsr_bv x1 (of_int 2)) (of_int (0x33))) }
    ensures  { to_uint (bw_and (lsr x2 (4*i)) (of_int 0x0F))
             = numof (nth n) (4*i) (4*i+4) }
    ensures  { ule (bw_and (lsr_bv x2 (of_int (4*i))) (of_int 0x0F))
                   (of_int 4) }
  =
     step1 n x1 (2*i);
     step1 n x1 (2*i+1);

     assert { let i' = of_int i in
                  ult i' (of_int 2)
                &&
                  of_int (4*i) = mul (of_int 4) i'
                &&
                  to_uint (bw_and (lsr x2 (4*i)) (of_int 0x0F))
                = to_uint (bw_and (lsr_bv x2 (mul (of_int 4) i')) (of_int 0x0F))
                = to_uint (add (bw_and (lsr_bv x1 (mul (of_int 4) i')) (of_int 0x03))
                           (bw_and (lsr_bv x1 (add (mul (of_int 4) i') (of_int 2))) (of_int (0x03))))
                = to_uint (add (bw_and (lsr x1 (4*i)) (of_int 0x03))
                               (bw_and (lsr x1 ((4*i)+2)) (of_int (0x03))))}

  let ghost prove (n x1 x2 x3 : t) : unit
    requires { x1 = sub n (bw_and (lsr_bv n (of_int 1)) (of_int 0x55)) }
    requires { x2 = add
               (bw_and x1 (of_int 0x33))
               (bw_and (lsr_bv x1 (of_int 2)) (of_int (0x33))) }
    requires { x3 = bw_and (add x2 (lsr_bv x2 (of_int 4))) (of_int 0x0F) }
    ensures { to_uint x3 = numof (nth n) 0 8 }
  =
    step2 n x1 x2 0;
    step2 n x1 x2 1;

    assert {  to_uint (bw_and x2 (of_int 0x0F)) +
              to_uint (bw_and (lsr_bv x2 (of_int 4)) (of_int 0x0F))
            = to_uint (bw_and (lsr x2 0) (of_int 0x0F)) +
              to_uint (bw_and (lsr x2 4) (of_int 0x0F)) }

  let count (n : t) : t
    ensures { to_uint result = numof (nth n) 0 8 }
  =
    let x = ref n in

    x := sub !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55));
    let ghost x1 = !x in

    x := add
               (bw_and !x (of_int 0x33))
               (bw_and (lsr_bv !x (of_int 2)) (of_int (0x33)));
    let ghost x2 = !x in

    x := bw_and (add !x (lsr_bv !x (of_int 4))) (of_int 0x0F);

    prove n x1 x2 !x;

    !x

end

module BitCounting32

  use import int.Int
  use import int.NumOf
  use import bv.BV32
  use import ref.Ref

  predicate step0 (n x1 : t) =
    x1 = sub n (bw_and (lsr_bv n (of_int 1)) (of_int 0x55555555))

  let ghost proof0 (n x1 : t) (i : int) : unit
    requires { 0 <= i < 16 }
    requires { step0 n x1 }
    ensures { to_uint (bw_and (lsr x1 (2*i)) (of_int 0x03))
              = numof (nth n) (2*i) (2*i + 2) }
  =
    let i' = of_int i in
    let twoi = mul (of_int 2) i' in
    assert { to_uint twoi = 2 * i };
    assert { to_uint (add twoi (of_int 1)) = to_uint twoi + 1 };
    assert { to_uint (bw_and (lsr_bv x1 twoi) (of_int 0x03))
             = (if nth_bv n twoi then 1 else 0) +
               (if nth_bv n (add twoi (of_int 1)) then 1 else 0)
             = (if nth n (to_uint twoi) then 1 else 0) +
               (if nth n (to_uint twoi + 1) then 1 else 0)
             = numof (nth n) (to_uint twoi) (to_uint twoi + 2) }

  predicate step1 (x1 x2 : t) =
    x2 = add (bw_and x1 (of_int 0x33333333))
             (bw_and (lsr_bv x1 (of_int 2)) (of_int (0x33333333)))

  let ghost proof1 (n x1 x2 : t) (i : int) : unit
    requires { 0 <= i < 8 }
    requires { step0 n x1  }
    requires { step1 x1 x2 }
    ensures  { to_uint (bw_and (lsr x2 (4*i)) (of_int 0x07))
               = numof (nth n) (4*i) (4*i+4) }
  =
     proof0 n x1 (2*i);
     proof0 n x1 (2*i+1);
     let i' = of_int i in
     assert { ult i' (of_int 8) };
     assert { to_uint (mul (of_int 4) i') = 4*i };
     assert { bw_and (lsr x2 (4*i)) (of_int 0x07)
              = bw_and (lsr_bv x2 (mul (of_int 4) i')) (of_int 0x07)
              = add (bw_and (lsr_bv x1 (mul (of_int 4) i')) (of_int 0x03))
                      (bw_and (lsr_bv x1 (add (mul (of_int 4) i') (of_int 2)))
                              (of_int (0x03)))
              = add (bw_and (lsr x1 (4*i)) (of_int 0x03))
                      (bw_and (lsr x1 ((4*i)+2)) (of_int (0x03))) }

  predicate step2 (x2:t) (x3:t) =
    x3 = bw_and (add x2 (lsr_bv x2 (of_int 4))) (of_int 0x0F0F0F0F)

  let ghost proof2 (n x1 x2 x3 : t) (i : int) : unit
    requires { 0 <= i < 4 }
    requires { step0 n x1 }
    requires { step1 x1 x2 }
    requires { step2 x2 x3 }
    ensures  { to_uint (bw_and (lsr x3 (8*i)) (of_int 0x0F))
             = numof (nth n) (8*i) (8*i+8) }
  =
    proof1 n x1 x2 (2*i);
    proof1 n x1 x2 (2*i+1);
    let i' = of_int i in
    assert { ult i' (of_int 4) };
    assert { to_uint (mul (of_int 8) i') = 8*i };
    assert { to_uint (add (mul (of_int 8) i') (of_int 4)) = 8*i+4 };
    assert { bw_and (lsr x3 (8*i)) (of_int 0x0F)
             = bw_and (lsr_bv x3 (mul (of_int 8) i')) (of_int 0x0F)
             = add (bw_and (lsr_bv x2 (mul (of_int 8) i')) (of_int 0x07))
                   (bw_and (lsr_bv x2 (add (mul (of_int 8) i') (of_int 4))) (of_int (0x07)))
             = add (bw_and (lsr x2 (8*i)) (of_int 0x07))
                   (bw_and (lsr x2 ((8*i)+4)) (of_int (0x07))) }

  predicate step3 (x3:t) (x4:t) =
    x4 = add x3 (lsr_bv x3 (of_int 8))

  let ghost proof3 (n x1 x2 x3 x4 : t) (i : int) : unit
    requires { 0 <= i < 2 }
    requires { step0 n x1 }
    requires { step1 x1 x2 }
    requires { step2 x2 x3 }
    requires { step3 x3 x4 }
    ensures  { to_uint (bw_and (lsr x4 (16*i)) (of_int 0x1F))
               = numof (nth n) (16*i) (16*i+16) }
  =
    proof2 n x1 x2 x3 (2*i);
    proof2 n x1 x2 x3 (2*i+1);
    let i' = of_int i in
    assert { ult i' (of_int 2) };
    assert { to_uint (mul (of_int 16) i') = 16*i };
    assert { to_uint (add (mul (of_int 16) i') (of_int 8)) = 16*i+8 };
    assert { bw_and (lsr x4 (16*i)) (of_int 0x1F)
             = bw_and (lsr_bv x4 (mul (of_int 16) i')) (of_int 0x1F)
             = add (bw_and (lsr_bv x3 (mul (of_int 16) i')) (of_int 0x0F))
                   (bw_and (lsr_bv x3 (add (mul (of_int 16) i') (of_int 8))) (of_int (0x0F)))
             = add (bw_and (lsr x3 (16*i)) (of_int 0x0F))
                   (bw_and (lsr x3 ((16*i)+8)) (of_int (0x0F))) }

  predicate step4 (x4:t) (x5:t) =
    x5 = add x4 (lsr_bv x4 (of_int 16))

  let ghost prove (n x1 x2 x3 x4 x5 : t) : unit
    requires { step0 n x1 }
    requires { step1 x1 x2 }
    requires { step2 x2 x3 }
    requires { step3 x3 x4 }
    requires { step4 x4 x5 }
    ensures { to_uint (bw_and x5 (of_int 0x3F)) = numof (nth n) 0 32 }
  =
    proof3 n x1 x2 x3 x4 0;
    proof3 n x1 x2 x3 x4 1;
(* moved to the stdlib
    assert { x4 = lsr x4 0 };
*)
    assert { bw_and x5 (of_int 0x3F)
             = add (bw_and x4 (of_int 0x1F)) (bw_and (lsr_bv x4 (of_int 16)) (of_int 0x1F))
             = add (bw_and (lsr x4 0) (of_int 0x1F)) (bw_and (lsr x4 16) (of_int 0x1F)) }

  function count_logic (n:t) : int = numof (nth n) 0 32

  let count (n : t) : t
    ensures { to_uint result = count_logic n }
  =
    let x = ref n in
    (* x = x - ( (x >> 1) & 0x55555555) *)
    x := sub !x (bw_and (lsr_bv !x (of_int 1)) (of_int 0x55555555));
    let ghost x1 = !x in
    (* x = (x & 0x33333333) + ((x >> 2) & 0x33333333) *)
    x := add (bw_and !x (of_int 0x33333333))
             (bw_and (lsr_bv !x (of_int 2)) (of_int (0x33333333)));
    let ghost x2 = !x in
    (* x = (x + (x >> 4)) & 0x0F0F0F0F *)
    x := bw_and (add !x (lsr_bv !x (of_int 4))) (of_int 0x0F0F0F0F);
    let ghost x3 = !x in
    (* x = x + (x >> 8) *)
    x := add !x (lsr_bv !x (of_int 8));
    let ghost x4 = !x in
    (* x = x + (x >> 16) *)
    x := add !x (lsr_bv !x (of_int 16));

    prove n x1 x2 x3 x4 !x;

    (* return (x & 0x0000003F) *)
    bw_and !x (of_int 0x0000003F)

end

module Hamming
  use import int.Int
  use import int.NumOf
  use import mach.bv.BVCheck32
  use import BitCounting32
  use import HighOrd as HO

  predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i

  function hammingD_logic (a b : t) : int = NumOf.numof (nth_diff a b) 0 32

  let hammingD (a b : t) : t
    ensures { to_uint result = hammingD_logic a b }
  =
    assert { forall i. 0 <= i < 32 -> nth (bw_xor a b) i <-> (nth_diff a b i) };
    count (bw_xor a b)

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

  lemma numof_ytpmE :
    forall p : int -> bool, a b : int.
    numof p a b = 0 -> (forall n : int. a <= n < b -> not p n)

  let lemma separation (a b : t)
    ensures { hammingD_logic a b = 0 <-> a = b }
  =
    assert { hammingD_logic a b = 0 -> eq_sub a b 0 32 }

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

  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 {hammingD_logic a b + hammingD_logic b c >= hammingD_logic 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}

  lemma triangleInequality: forall a b c.
    (hammingD_logic a b) + (hammingD_logic b c) >= hammingD_logic a c

end

module AsciiCode
  use import int.Int
  use import int.NumOf
  use import number.Parity
  use import bool.Bool
  use import mach.bv.BVCheck32
  use import BitCounting32

  constant one : t = of_int 1
  constant lastbit : t = sub size_bv one

  (* let lastbit () = (sub_check size_bv one) : t *)

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!


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)

  predicate validAscii (b : t) = even (count_logic b)

  let lemma bv_even (b:t)
    ensures { even (to_uint b) <-> not (nth b 0) }
  =
    assert { not (nth_bv b zeros) <-> b = mul (of_int 2) (lsr_bv b one) };
    assert { (exists k. b = mul (of_int 2) k) -> not (nth_bv b zeros) };
    assert { (exists k. to_uint b = 2 * k) -> (exists k. b = mul (of_int 2) k) };
    assert { not (nth b 0) <-> to_uint b = 2 * to_uint (lsr b 1) }

  lemma bv_odd : forall b : t. odd (to_uint b) <-> nth b 0

  (* use Numofbit *)

  use HighOrd as HO

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

  let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
    requires { forall i. a <= i < b -> not (p i) \/ not (q i) }
    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 count_or (b c : t)
    requires { bw_and b c = zeros }
    ensures  { count_logic (bw_or b c) = count_logic b + count_logic c }
  =
    assert { forall i. ult i size_bv ->
               not (nth_bv b i) \/ not (nth_bv c i) };
    assert { forall i. not (nth_bv b (of_int i)) \/ not (nth_bv c (of_int i))
          -> not (nth b i) \/ not (nth c i) };
    assert { numof (fun_or (nth b) (nth c)) 0 32 = numof (nth b) 0 32 + numof (nth c) 0 32 };
    assert { numof (nth (bw_or b c)) 0 32 = numof (fun_or (nth b) (nth c)) 0 32 }

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) =
    requires { not (nth_bv b lastbit) }
    ensures  { eq_sub_bv result b zeros lastbit }
    ensures  { validAscii result }
    let c = count b in
    let maskbit = lsl_check c lastbit in
    assert { bw_and b maskbit = zeros };
    assert { even (to_uint c) ->
               not (nth_bv c zeros)
            && count_logic maskbit    = 0 };
    assert { odd  (to_uint c) ->
               nth_bv c zeros
            && nth maskbit 31
            && (forall i. 0 <= i < 31 -> not (nth maskbit i))
            && count_logic maskbit    = 1 };
    let code = bw_or b maskbit in
    assert { count_logic code = count_logic b + count_logic maskbit };
    code

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.

  use Hamming

  let rec lemma tmp (a b : t) (i j : int)
      requires { i < j }
      variant { j - i }
      ensures { (even (numof (nth a) i j) /\ odd (numof (nth b) i j)) \/ (odd (numof (nth a) i j) /\ even (numof (nth b) i j))
             <-> odd (NumOf.numof (Hamming.nth_diff a b) i j) }
  =
    if i < j - 1 then
      tmp a b i (j-1)

  lemma asciiProp : forall a b.
          ((validAscii a /\ not validAscii b) \/ (validAscii b /\ not validAscii a))
      <-> odd (Hamming.hammingD_logic a b)

end


download ZIP archive

Why3 Proof Results for Project "bitcount"

Theory "bitcount.BitCount8bit_fact": fully verified in 12.83 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)CVC4 (1.4 noBV)
nth_as_bv_is_int0.18------
VC for step1---------
split_goal_wp
  1. assertion---------
split_goal_wp
  1. assertion---0.03---
2. assertion---0.59---
2. postcondition2.88------
3. postcondition0.50------
VC for step2---------
split_goal_wp
  1. precondition0.04------
2. precondition---------
split_goal_wp
  1. precondition0.02------
3. precondition---------
split_goal_wp
  1. VC for step20.05------
2. VC for step20.04------
4. precondition0.02------
5. assertion---------
split_goal_wp
  1. assertion0.10------
2. assertion0.65------
3. assertion0.42------
4. assertion---0.07---
5. assertion------5.20
6. postcondition---0.05---
7. postcondition0.32------
VC for prove---------
split_goal_wp
  1. precondition0.04------
2. precondition0.04------
3. precondition0.04------
4. precondition0.04------
5. precondition0.04------
6. precondition0.04------
7. assertion1.10------
8. postcondition---0.14---
VC for count---------
split_goal_wp
  1. precondition---------
split_goal_wp
  1. precondition0.04------
2. precondition0.05------
3. precondition---------
split_goal_wp
  1. precondition0.05------
4. postcondition0.05------

Theory "bitcount.BitCounting32": fully verified in 6.59 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)
VC for proof0------
split_goal_wp
  1. assertion0.04---
2. assertion0.03---
3. assertion------
split_goal_wp
  1. VC for proof0------
introduce_premises
  1. VC for proof0---0.17
2. VC for proof00.04---
3. VC for proof00.83---
4. postcondition0.29---
VC for proof1------
split_goal_wp
  1. precondition0.03---
2. precondition0.02---
3. precondition0.04---
4. precondition0.03---
5. assertion0.04---
6. assertion0.63---
7. assertion------
split_goal_wp
  1. VC for proof10.03---
2. VC for proof1---0.05
3. VC for proof10.04---
8. postcondition---0.05
VC for proof2------
split_goal_wp
  1. precondition0.04---
2. precondition0.04---
3. precondition0.03---
4. precondition0.04---
5. precondition0.03---
6. precondition0.04---
7. assertion0.06---
8. assertion0.58---
9. assertion0.80---
10. assertion------
split_goal_wp
  1. VC for proof20.03---
2. VC for proof2---0.07
3. VC for proof20.03---
11. postcondition---0.07
VC for proof3------
split_goal_wp
  1. precondition0.04---
2. precondition0.03---
3. precondition0.03---
4. precondition0.04---
5. precondition0.03---
6. precondition0.03---
7. precondition0.04---
8. precondition0.04---
9. assertion0.05---
10. assertion0.57---
11. assertion0.06---
12. assertion------
split_goal_wp
  1. VC for proof30.04---
2. VC for proof3---0.07
3. VC for proof30.03---
13. postcondition---0.17
VC for prove------
split_goal_wp
  1. precondition0.04---
2. precondition0.04---
3. precondition0.04---
4. precondition0.04---
5. precondition0.04---
6. precondition0.04---
7. precondition0.04---
8. precondition0.05---
9. precondition0.04---
10. precondition0.05---
11. assertion------
split_goal_wp
  1. VC for prove---0.04
2. VC for prove0.04---
12. postcondition---0.18
VC for count------
split_goal_wp
  1. precondition0.040.02
2. precondition0.030.03
3. precondition0.050.02
4. precondition0.030.03
5. precondition0.040.03
6. postcondition0.050.05

Theory "bitcount.Hamming": fully verified in 11.75 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Z3 (4.4.0)
VC for hammingD------------
split_goal_wp
  1. assertion1.00---------
2. postcondition---------0.02
symmetric---------0.05
numof_ytpmE------1.04---
VC for separation------------
split_goal_wp
  1. assertion1.23---------
2. postcondition------------
split_goal_wp
  1. VC for separation0.04---------
2. VC for separation0.65---------
VC for numof_or------0.32---
VC for triangleInequalityInt---7.31------
triangleInequality0.05---0.04---

Theory "bitcount.AsciiCode": fully verified in 9.54 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)CVC4 (1.4 noBV)Z3 (4.4.0)
VC for bv_even---------------
split_goal_wp
  1. assertion------0.04------
2. assertion------0.04------
3. assertion---3.21---------
4. assertion---0.42---------
5. postcondition0.09------------
bv_odd0.05---0.03------
VC for numof_or------0.22------
VC for count_or---------------
split_goal_wp
  1. assertion------0.06------
2. assertion0.03------------
3. assertion------------0.02
4. assertion---------1.43---
5. postcondition0.06---0.08------
VC for ascii---------------
split_goal_wp
  1. precondition0.30---0.04------
2. assertion------0.07------
3. assertion---------------
split_goal_wp
  1. assertion0.07------------
2. assertion------0.09------
4. assertion---------------
split_goal_wp
  1. assertion0.08------------
2. assertion0.19------------
3. assertion0.55------------
4. assertion------------0.03
5. assertion0.05------------
6. postcondition------0.10------
7. postcondition0.04------------
VC for tmp---------------
split_goal_wp
  1. variant decrease0.02---0.04------
2. precondition0.02---0.02------
3. postcondition------------0.38
4. postcondition1.38------------
asciiProp0.24---0.05------