## 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)) } requires { x2 = add (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)) } requires { x2 = add (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 x := add (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 && 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 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 | --- |