## 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

References: ProofInUse joint laboratory

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 (1 : t)
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.
t'int (nth_as_bv a i) = nth_as_int a (t'int 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 (1 : t)) (0x55 : t)) }
ensures { t'int (bw_and (lsr x1 (2*i)) (0x03 : t))
= numof (nth n) (2*i) (2*i + 2) }
ensures { ule (bw_and (lsr x1 (2*i)) (0x03 : t)) (2 : t) }
=
assert { let i' = of_int i in
let twoi = mul (2 : t) i' in
bw_and (lsr_bv x1 twoi) (0x03 : t)
= add (nth_as_bv n twoi) (nth_as_bv n (add twoi (1 : t)))
&&
t'int (bw_and (lsr_bv x1 twoi) (0x03 : t))
= numof (nth n) (t'int twoi) (t'int 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 (1 : t)) (0x55 : t)) }
(bw_and x1 (0x33 : t))
(bw_and (lsr_bv x1 (2 : t)) (0x33 : t)) }
ensures  { t'int (bw_and (lsr x2 (4*i)) (0x0F : t))
= numof (nth n) (4*i) (4*i+4) }
ensures  { ule (bw_and (lsr_bv x2 (of_int (4*i))) (0x0F : t))
(4 : t) }
=
step1 n x1 (2*i);
step1 n x1 (2*i+1);

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

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

assert {  t'int (bw_and x2 (0x0F : t)) +
t'int (bw_and (lsr_bv x2 (4 : t)) (0x0F : t))
= t'int (bw_and (lsr x2 0) (0x0F : t)) +
t'int (bw_and (lsr x2 4) (0x0F : t)) }

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

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

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

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

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 (1 : t)) (0x55555555 : t))

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

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

let ghost proof1 (n x1 x2 : t) (i : int) : unit
requires { 0 <= i < 8 }
requires { step0 n x1  }
requires { step1 x1 x2 }
ensures  { t'int (bw_and (lsr x2 (4*i)) (0x07 : t))
= 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' (8 : t) };
assert { t'int (mul (4 : t) i') = 4*i };
assert { bw_and (lsr x2 (4*i)) (0x07 : t)
= bw_and (lsr_bv x2 (mul (4 : t) i')) (0x07 : t)
= add (bw_and (lsr_bv x1 (mul (4 : t) i')) (0x03 : t))
(bw_and (lsr_bv x1 (add (mul (4 : t) i') (2 : t)))
(0x03 : t))
= add (bw_and (lsr x1 (4*i)) (0x03 : t))
(bw_and (lsr x1 ((4*i)+2)) (0x03 : t)) }

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

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  { t'int (bw_and (lsr x3 (8*i)) (0x0F : t))
= 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' (4 : t) };
assert { t'int (mul (8 : t) i') = 8*i };
assert { t'int (add (mul (8 : t) i') (4 : t)) = 8*i+4 };
assert { bw_and (lsr x3 (8*i)) (0x0F : t)
= bw_and (lsr_bv x3 (mul (8 : t) i')) (0x0F : t)
= add (bw_and (lsr_bv x2 (mul (8 : t) i')) (0x07 : t))
(bw_and (lsr_bv x2 (add (mul (8 : t) i') (4 : t))) (0x07 : t))
= add (bw_and (lsr x2 (8*i)) (0x07 : t))
(bw_and (lsr x2 ((8*i)+4)) (0x07 : t)) }

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

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  { t'int (bw_and (lsr x4 (16*i)) (0x1F : t))
= 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' (2 : t) };
assert { t'int (mul (16 : t) i') = 16*i };
assert { t'int (add (mul (16 : t) i') (8 : t)) = 16*i+8 };
assert { bw_and (lsr x4 (16*i)) (0x1F : t)
= bw_and (lsr_bv x4 (mul (16 : t) i')) (0x1F : t)
= add (bw_and (lsr_bv x3 (mul (16 : t) i')) (0x0F : t))
(bw_and (lsr_bv x3 (add (mul (16 : t) i') (8 : t))) (0x0F : t))
= add (bw_and (lsr x3 (16*i)) (0x0F : t))
(bw_and (lsr x3 ((16*i)+8)) (0x0F : t)) }

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

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 { t'int (bw_and x5 (0x3F : t)) = 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 (0x3F : t)
= add (bw_and x4 (0x1F : t)) (bw_and (lsr_bv x4 (16 : t)) (0x1F : t))
= add (bw_and (lsr x4 0) (0x1F : t)) (bw_and (lsr x4 16) (0x1F : t)) }

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

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

prove n x1 x2 x3 x4 !x;

(* return (x & 0x0000003F) *)
bw_and !x (0x0000003F : t)

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 { t'int 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 = 1 : t
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 (t'int b) <-> not (nth b 0) }
=
assert { not (nth_bv b zeros) <-> b = mul (2 : t) (lsr_bv b one) };
assert { (exists k. b = mul (2 : t) k) -> not (nth_bv b zeros) };
assert { (exists k. t'int b = 2 * k) -> (exists k. b = mul (2 : t) k) };
assert { not (nth b 0) <-> t'int b = 2 * t'int (lsr b 1) }

lemma bv_odd : forall b : t. odd (t'int 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 (t'int c) ->
not (nth_bv c zeros)
&& count_logic maskbit    = 0 };
assert { odd  (t'int c) ->
nth_bv c zeros
&& (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

```

# Why3 Proof Results for Project "bitcount"

## Theory "bitcount.BitCount8bit_fact": fully verified in 0.29 s

 Obligations Alt-Ergo (1.01) Alt-Ergo (1.30) CVC4 (1.4) CVC4 (1.4 noBV) Z3 (4.4.1) Z3 (4.5.0) Z3 (4.5.0 noBV) nth_as_bv_is_int --- 0.16 0.05 0.08 --- --- --- 2. VC for step1 --- --- --- --- --- --- --- split_goal_wp 1. assertion --- --- --- --- --- --- --- split_goal_wp 1. assertion --- --- --- --- 0.02 0.06 --- 2. assertion --- --- 0.56 --- --- 0.11 --- 2. postcondition --- 0.20 --- --- --- 0.08 --- 3. postcondition 0.17 0.17 --- --- --- 0.08 --- 3. VC for step2 --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.04 0.03 0.04 0.07 --- 0.02 0.02 2. precondition 0.02 0.03 0.04 0.07 --- 0.02 0.02 3. precondition --- --- --- --- --- --- --- split_goal_wp 1. VC for step2 0.05 0.03 0.04 0.07 --- 0.02 0.02 2. VC for step2 0.04 0.03 0.04 0.07 --- 0.02 0.02 4. precondition --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.02 0.03 0.04 0.07 --- 0.02 0.01 5. assertion --- --- --- --- --- --- --- split_goal_wp 1. assertion 0.10 0.05 0.11 0.10 --- 0.04 0.66 2. assertion 0.10 0.12 0.16 --- --- 0.04 --- 3. assertion 0.73 0.84 --- 0.12 --- 0.07 --- 4. assertion --- --- 0.04 --- --- 0.08 --- 5. assertion --- --- 2.74 --- --- 0.08 --- 6. postcondition --- 3.14 0.05 0.12 --- 0.04 --- 7. postcondition 0.36 0.13 0.10 0.12 --- 0.04 --- 4. VC for prove --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.04 0.03 0.03 0.04 --- 0.02 0.02 2. precondition 0.04 0.03 0.04 0.06 --- 0.02 0.01 3. precondition 0.04 0.03 0.04 0.06 --- 0.02 0.02 4. precondition 0.04 0.04 0.03 0.04 --- 0.02 0.02 5. precondition 0.04 0.04 0.03 0.06 --- 0.02 0.02 6. precondition 0.04 0.04 0.04 0.06 --- 0.01 0.02 7. assertion 0.12 0.16 --- 0.10 --- 0.18 --- 8. postcondition --- --- 0.20 --- --- 0.06 --- 5. VC for count --- --- --- --- --- --- --- split_goal_wp 1. precondition --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.04 0.02 0.04 0.07 --- 0.01 0.02 2. precondition 0.05 0.03 0.04 0.07 --- 0.02 0.02 3. precondition --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.05 0.02 0.04 0.06 --- 0.02 0.02 4. postcondition 0.05 0.03 0.04 0.05 --- 0.02 0.02

## Theory "bitcount.BitCounting32": fully verified in 0.00 s

 Obligations Alt-Ergo (1.01) Alt-Ergo (1.30) CVC4 (1.4) CVC4 (1.4 noBV) Z3 (4.3.2) Z3 (4.4.1) Z3 (4.5.0) Z3 (4.5.0 noBV) 1. VC for proof0 --- --- --- --- --- --- --- --- split_goal_wp 1. assertion 0.03 0.03 --- --- --- --- 0.04 --- 2. assertion 0.04 0.04 --- --- --- --- 0.07 --- 3. assertion --- --- --- --- --- --- --- --- split_goal_wp 1. VC for proof0 --- --- --- --- --- --- --- --- introduce_premises 1. VC for proof0 --- --- 0.19 --- --- --- 0.12 --- 2. VC for proof0 0.41 0.05 --- 0.12 --- --- --- --- 3. VC for proof0 0.30 0.20 --- 0.12 --- --- 0.14 --- 4. postcondition 0.16 0.18 --- 0.11 --- --- 0.23 --- 2. VC for proof1 --- --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.03 0.03 0.05 0.06 --- --- 0.02 0.04 2. precondition 0.02 0.03 0.05 0.06 --- --- 0.01 0.02 3. precondition 0.04 0.02 0.05 0.07 --- --- 0.02 0.03 4. precondition 0.03 0.03 0.05 0.06 --- --- 0.02 0.02 5. assertion 0.04 0.04 --- 0.10 --- --- 0.06 0.61 6. assertion 0.10 0.13 0.12 --- --- --- 0.04 --- 7. assertion --- --- --- --- --- --- --- --- split_goal_wp 1. VC for proof1 0.03 0.04 --- 0.10 --- --- 0.06 --- 2. VC for proof1 --- --- 0.05 --- --- --- 0.12 --- 3. VC for proof1 0.04 0.04 --- 1.00 --- --- 0.09 --- 8. postcondition --- --- 0.05 0.13 --- --- 0.06 --- 3. VC for proof2 --- --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.04 0.02 0.05 0.07 --- --- 0.02 0.03 2. precondition 0.04 0.02 0.05 0.07 --- --- 0.02 0.02 3. precondition 0.03 0.03 0.05 0.07 --- --- 0.02 0.02 4. precondition 0.04 0.03 0.05 0.06 --- --- 0.02 0.03 5. precondition 0.03 0.03 0.05 0.06 --- --- 0.01 0.01 6. precondition 0.04 0.03 0.05 0.06 --- --- 0.02 0.02 7. assertion 0.06 0.05 --- 0.11 --- --- 0.06 0.62 8. assertion 0.14 0.04 0.06 --- --- --- 0.04 --- 9. assertion 0.11 0.02 0.11 --- --- --- 0.04 --- 10. assertion --- --- --- --- --- --- --- --- split_goal_wp 1. VC for proof2 0.03 0.04 --- 0.10 --- --- 0.09 --- 2. VC for proof2 --- --- 0.07 --- --- 0.02 0.11 --- 3. VC for proof2 0.03 0.04 --- 0.10 --- --- 0.09 --- 11. postcondition --- --- 0.06 0.14 --- --- 0.10 --- 4. VC for proof3 --- --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.04 0.03 0.05 0.06 --- --- 0.02 0.03 2. precondition 0.03 0.02 0.06 0.07 --- --- 0.01 0.02 3. precondition 0.03 0.03 0.05 0.06 --- --- 0.02 0.02 4. precondition 0.04 0.02 0.06 0.07 --- --- 0.02 0.02 5. precondition 0.03 0.03 0.06 0.06 --- --- 0.03 0.03 6. precondition 0.03 0.02 0.07 0.07 --- --- 0.02 0.02 7. precondition 0.04 0.03 0.06 0.06 --- --- 0.02 0.02 8. precondition 0.04 0.03 0.06 0.07 --- --- 0.01 0.02 9. assertion 0.05 0.04 --- 0.10 --- --- 0.06 0.65 10. assertion 0.26 0.04 0.12 --- --- --- 0.04 --- 11. assertion 0.03 0.03 0.14 --- --- --- 0.04 --- 12. assertion --- --- --- --- --- --- --- --- split_goal_wp 1. VC for proof3 0.04 0.04 --- 0.10 --- --- 0.03 --- 2. VC for proof3 --- --- 0.07 --- --- --- 0.15 --- 3. VC for proof3 0.03 0.04 --- 0.08 --- --- 0.06 --- 13. postcondition --- --- 0.17 0.12 --- --- 0.16 --- 5. VC for prove --- --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.04 0.03 0.04 0.04 --- --- 0.02 0.02 2. precondition 0.04 0.03 0.05 0.06 --- --- 0.02 0.02 3. precondition 0.04 0.03 0.05 0.06 --- --- 0.02 0.02 4. precondition 0.04 0.03 0.06 0.06 --- --- 0.02 0.02 5. precondition 0.04 0.04 0.05 0.06 --- --- 0.02 0.02 6. precondition 0.04 0.03 0.04 0.04 --- --- 0.02 0.02 7. precondition 0.04 0.03 0.06 0.06 --- --- 0.02 0.02 8. precondition 0.05 0.03 0.06 0.06 --- --- 0.01 0.02 9. precondition 0.04 0.03 0.05 0.06 --- --- 0.01 0.02 10. precondition 0.05 0.03 0.05 0.06 --- --- 0.02 0.02 11. assertion --- --- --- --- --- --- --- --- split_goal_wp 1. VC for prove --- --- 0.04 --- Timeout (6s) --- 0.03 --- 2. VC for prove 0.04 0.06 --- 0.09 --- --- --- 0.23 12. postcondition --- --- 0.21 0.11 --- --- 0.21 --- 6. VC for count --- --- --- --- --- --- --- --- split_goal_wp 1. precondition 0.04 0.03 0.02 0.08 --- --- 0.04 0.23 2. precondition 0.03 0.03 0.03 0.08 --- --- 0.39 0.62 3. precondition 0.05 0.03 0.02 0.08 --- --- 0.12 0.64 4. precondition 0.03 0.03 0.03 0.08 --- --- 0.08 0.61 5. precondition 0.04 0.03 0.03 0.09 --- --- 0.25 0.59 6. postcondition 0.05 0.11 0.05 0.09 --- --- 0.04 0.22

## Theory "bitcount.Hamming": fully verified in 9.16 s

 Obligations Alt-Ergo (1.01) Alt-Ergo (1.30) CVC4 (1.4) CVC4 (1.4 noBV) Z3 (4.4.1) Z3 (4.5.0) Z3 (4.5.0 noBV) 1. VC for hammingD --- --- --- --- --- --- --- split_goal_wp 1. assertion 0.83 2.70 --- 0.07 --- --- --- 2. postcondition Timeout (6s) 1.02 --- --- --- 0.08 --- symmetric 2.29 0.39 --- --- --- 0.12 --- numof_ytpmE --- --- 1.20 1.30 --- --- --- 4. VC for separation --- --- --- --- --- --- --- split_goal_wp 1. assertion 0.47 0.20 --- --- --- 0.08 --- 2. postcondition --- --- --- --- --- --- --- split_goal_wp 1. VC for separation 0.04 0.05 --- 0.08 --- --- 0.22 2. VC for separation 0.14 0.16 --- --- --- 0.03 --- 5. VC for numof_or Timeout (6s) 2.81 0.34 0.39 --- 0.06 --- 6. VC for triangleInequalityInt --- --- --- --- --- --- --- split_goal_wp 1. assertion --- --- --- --- --- --- --- split_goal_wp 1. VC for triangleInequalityInt 0.03 0.02 0.07 0.09 0.02 0.04 0.22 2. VC for triangleInequalityInt --- --- --- --- 0.08 --- --- 2. postcondition 0.03 0.04 0.08 0.04 0.02 0.05 0.65 triangleInequality 0.05 0.03 0.04 0.10 --- 0.03 0.01

## Theory "bitcount.AsciiCode": fully verified in 2.93 s

 Obligations Alt-Ergo (1.01) Alt-Ergo (1.30) CVC4 (1.4) CVC4 (1.4 noBV) Z3 (4.4.1) Z3 (4.5.0) Z3 (4.5.0 noBV) 1. VC for bv_even --- --- --- --- --- --- --- split_goal_wp 1. assertion --- --- 0.06 --- --- 0.04 --- 2. assertion --- --- 0.04 --- --- 0.04 --- 3. assertion 1.21 0.43 --- --- --- --- --- 4. assertion --- --- --- --- --- --- --- split_goal_wp 1. VC for bv_even --- 1.50 --- --- --- --- --- 2. VC for bv_even --- 0.06 --- --- --- --- --- 5. postcondition 0.14 0.14 --- --- --- --- --- bv_odd 0.05 0.04 0.03 0.09 --- 0.04 --- 3. VC for numof_or --- --- 0.25 0.36 --- 0.06 --- 4. VC for count_or --- --- --- --- --- --- --- split_goal_wp 1. assertion --- --- 0.09 --- --- 0.05 --- 2. assertion 0.03 0.04 --- 0.10 --- --- 0.23 3. assertion --- --- --- --- --- 0.04 --- 4. assertion --- --- --- 1.81 --- --- --- 5. postcondition 0.06 0.04 0.08 0.13 --- 0.05 --- 5. VC for ascii --- --- --- --- --- --- --- split_goal_wp 1. precondition --- 0.09 0.05 0.11 --- 0.01 --- 2. assertion --- --- 0.10 --- --- 0.04 --- 3. assertion --- --- --- --- --- --- --- split_goal_wp 1. assertion --- 0.08 --- 0.10 --- --- 0.25 2. assertion --- --- 0.13 --- --- --- --- 4. assertion --- --- --- --- --- --- --- split_goal_wp 1. assertion --- 0.17 --- 0.10 --- --- 0.24 2. assertion --- 0.16 --- 0.14 --- --- --- 3. assertion --- 0.24 0.17 0.11 --- --- --- 4. assertion --- --- --- --- --- 0.09 --- 5. assertion 0.05 0.04 --- 0.11 --- --- --- 6. postcondition --- --- 0.11 1.55 --- 0.04 --- 7. postcondition 0.20 0.18 --- 0.52 --- 0.06 --- 6. VC for tmp --- --- --- --- --- --- --- split_goal_wp 1. variant decrease 0.02 0.03 0.04 0.07 --- 0.04 0.04 2. precondition 0.02 0.03 0.02 0.08 --- 0.02 0.01 3. postcondition --- --- --- --- --- 0.73 --- 4. postcondition --- 2.06 4.31 1.42 0.26 5.75 --- asciiProp 1.51 0.26 0.05 0.13 --- 0.06 ---