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 int.Int use int.NumOf use bv.BV8 use 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 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 int.Int use int.NumOf use bv.BV32 use 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 int.Int use int.NumOf use mach.bv.BVCheck32 use BitCounting32 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 : 'a -> bool) : 'a -> bool = fun 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
ASCII checksum
In the beginning the encoding of an ascii character was done on 8 bits: the first 7 bits were used for the character itself while the 8th bit was used as a checksum, i.e. a mean to detect errors. The checksum value was the binary sum of the 7 other bits, allowing the detection of any change of an odd number of bits in the initial value. Let's prove it!
module AsciiCode use int.Int use int.NumOf use number.Parity use bool.Bool use mach.bv.BVCheck32 use BitCounting32 constant one : t = 1 : t constant lastbit : t = sub size_bv one (* let lastbit () = (sub_check size_bv one) : t *)
Checksum computation and correctness
predicate validAscii (b : t) = even (count_logic b)
A ascii character is valid if its number of 1-bits is even. (Remember that a binary number is odd if and only if its first bit is 1.)
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 *) function fun_or (f g : 'a -> bool) : 'a -> bool = fun 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
function makes any character valid in the
sense that we just defined. One way to implement it is to count
the number of 1-bits of a character encoded on 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 = u_lsl c (31:t) 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 implies 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
Obligations | Alt-Ergo 2.0.0 | CVC4 1.4 | CVC4 1.4 (noBV) | Z3 4.11.2 | Z3 4.4.1 (noBV) | ||
nth_as_bv_is_int | 0.16 | 0.05 | 0.08 | --- | --- | ||
VC for step1 | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
assertion | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
assertion | --- | --- | --- | 0.01 | --- | ||
assertion | --- | 0.56 | --- | --- | --- | ||
postcondition | 0.20 | --- | --- | --- | --- | ||
postcondition | 0.03 | --- | --- | --- | --- | ||
VC for step2 | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
precondition | 0.04 | 0.04 | 0.07 | 0.01 | 0.02 | ||
precondition | 0.02 | 0.04 | 0.07 | 0.01 | 0.02 | ||
precondition | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
VC for step2 | 0.05 | 0.04 | 0.07 | 0.01 | 0.02 | ||
VC for step2 | 0.04 | 0.04 | 0.07 | 0.01 | 0.02 | ||
precondition | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
precondition | 0.02 | 0.04 | 0.07 | 0.01 | 0.01 | ||
assertion | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
assertion | 0.10 | 0.11 | 0.10 | --- | 0.67 | ||
assertion | 0.10 | 0.16 | --- | --- | --- | ||
assertion | 0.73 | --- | 0.12 | 0.02 | --- | ||
assertion | --- | 0.04 | --- | --- | --- | ||
assertion | --- | 3.31 | --- | --- | --- | ||
postcondition | 2.70 | 0.05 | 0.12 | 0.02 | --- | ||
postcondition | 0.08 | 0.10 | 0.12 | 0.02 | --- | ||
VC for prove | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
precondition | 0.04 | 0.03 | 0.04 | 0.01 | 0.02 | ||
precondition | 0.04 | 0.04 | 0.06 | 0.01 | 0.01 | ||
precondition | 0.04 | 0.04 | 0.06 | 0.01 | 0.02 | ||
precondition | 0.04 | 0.03 | 0.04 | 0.01 | 0.02 | ||
precondition | 0.04 | 0.03 | 0.06 | 0.01 | 0.02 | ||
precondition | 0.04 | 0.04 | 0.06 | 0.01 | 0.02 | ||
assertion | 0.12 | --- | 0.10 | --- | --- | ||
postcondition | --- | 0.20 | --- | --- | --- | ||
VC for count | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
precondition | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
precondition | 0.05 | 0.04 | 0.06 | 0.01 | 0.02 | ||
precondition | 0.05 | 0.04 | 0.07 | 0.01 | 0.02 | ||
precondition | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
precondition | 0.04 | 0.04 | 0.07 | 0.01 | 0.02 | ||
postcondition | 0.05 | 0.04 | 0.05 | 0.01 | 0.02 |
Theory "bitcount.BitCounting32": fully verified
Obligations | Alt-Ergo 2.0.0 | CVC4 1.4 | CVC4 1.4 (noBV) | Z3 4.11.2 | Z3 4.4.1 (noBV) | |||
VC for proof0 | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
assertion | 0.03 | --- | --- | --- | --- | |||
assertion | 0.04 | --- | --- | --- | --- | |||
assertion | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
VC for proof0 | --- | --- | --- | --- | --- | |||
introduce_premises | ||||||||
VC for proof0 | --- | 0.19 | --- | --- | --- | |||
VC for proof0 | 0.02 | --- | 0.12 | --- | --- | |||
VC for proof0 | 0.16 | --- | 0.12 | 0.01 | --- | |||
postcondition | 0.18 | --- | 0.11 | 0.20 | --- | |||
VC for proof1 | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
precondition | 0.03 | 0.05 | 0.06 | 0.01 | 0.04 | |||
precondition | 0.03 | 0.05 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.05 | 0.07 | 0.01 | 0.03 | |||
precondition | 0.02 | 0.05 | 0.06 | 0.01 | 0.02 | |||
assertion | 0.04 | --- | 0.10 | --- | 0.61 | |||
assertion | 0.05 | 0.12 | --- | --- | --- | |||
assertion | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
VC for proof1 | 0.03 | --- | 0.10 | 0.02 | --- | |||
VC for proof1 | --- | 0.05 | --- | 0.03 | --- | |||
VC for proof1 | 0.04 | --- | 1.29 | --- | --- | |||
postcondition | --- | 0.05 | 0.13 | --- | --- | |||
VC for proof2 | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
precondition | 0.04 | 0.05 | 0.07 | 0.01 | 0.03 | |||
precondition | 0.03 | 0.05 | 0.06 | 0.01 | 0.01 | |||
precondition | 0.04 | 0.05 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.05 | 0.06 | 0.01 | 0.03 | |||
precondition | 0.04 | 0.05 | 0.07 | 0.01 | 0.02 | |||
precondition | 0.03 | 0.05 | 0.07 | 0.01 | 0.02 | |||
assertion | 0.06 | --- | 0.11 | --- | 0.57 | |||
assertion | 0.14 | 0.06 | --- | --- | --- | |||
assertion | 0.11 | 0.11 | --- | --- | --- | |||
assertion | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
VC for proof2 | 0.03 | --- | 0.10 | 0.02 | --- | |||
VC for proof2 | --- | 0.07 | --- | 0.03 | --- | |||
VC for proof2 | 0.03 | --- | 0.10 | 0.04 | --- | |||
postcondition | --- | 0.06 | 0.14 | --- | --- | |||
VC for proof3 | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
precondition | 0.04 | 0.05 | 0.06 | 0.01 | 0.03 | |||
precondition | 0.03 | 0.07 | 0.07 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.06 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.06 | 0.07 | 0.01 | 0.02 | |||
precondition | 0.03 | 0.06 | 0.06 | 0.01 | 0.03 | |||
precondition | 0.03 | 0.06 | 0.07 | 0.01 | 0.02 | |||
precondition | 0.03 | 0.05 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.06 | 0.07 | 0.01 | 0.02 | |||
assertion | 0.05 | --- | 0.10 | --- | 0.64 | |||
assertion | 0.09 | 0.12 | --- | --- | --- | |||
assertion | 0.03 | 0.14 | --- | --- | --- | |||
assertion | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
VC for proof3 | 0.04 | --- | 0.10 | 0.02 | --- | |||
VC for proof3 | --- | 0.07 | --- | 0.03 | --- | |||
VC for proof3 | 0.03 | --- | 0.08 | 0.06 | --- | |||
postcondition | --- | 0.17 | 0.12 | --- | --- | |||
VC for prove | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
precondition | 0.04 | 0.04 | 0.04 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.05 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.05 | 0.06 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.05 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.05 | 0.05 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.04 | 0.04 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.06 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.05 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.06 | 0.06 | 0.01 | 0.02 | |||
precondition | 0.04 | 0.05 | 0.06 | 0.01 | 0.02 | |||
assertion | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
VC for prove | --- | 0.04 | --- | 0.02 | --- | |||
VC for prove | 0.04 | --- | 0.09 | --- | 0.10 | |||
postcondition | --- | 0.20 | 0.11 | --- | --- | |||
VC for count | --- | --- | --- | --- | --- | |||
split_goal_right | ||||||||
precondition | 0.04 | 0.02 | 0.08 | 0.01 | 0.10 | |||
precondition | 0.03 | 0.03 | 0.08 | 0.02 | 0.53 | |||
precondition | 0.05 | 0.02 | 0.08 | 0.03 | 0.61 | |||
precondition | 0.03 | 0.03 | 0.08 | 0.02 | 0.54 | |||
precondition | 0.04 | 0.03 | 0.09 | 0.10 | 0.59 | |||
postcondition | 0.05 | 0.05 | 0.09 | 0.01 | 0.22 |
Theory "bitcount.Hamming": fully verified
Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.4.1 | CVC4 1.4 | CVC4 1.4 (noBV) | Z3 4.11.2 | Z3 4.4.1 (noBV) | ||
VC for hammingD | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
assertion | 5.26 | --- | --- | 0.07 | --- | --- | ||
postcondition | 1.38 | --- | --- | --- | 0.01 | --- | ||
symmetric | 0.23 | --- | --- | --- | 0.01 | --- | ||
numof_ytpmE | --- | --- | 1.57 | 1.62 | --- | --- | ||
VC for separation | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
assertion | --- | 0.18 | --- | --- | --- | --- | ||
postcondition | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
VC for separation | 0.04 | --- | --- | 0.08 | --- | 0.22 | ||
VC for separation | 0.14 | --- | --- | --- | 0.01 | --- | ||
VC for numof_or | 1.40 | --- | 0.34 | 0.39 | 0.02 | --- | ||
VC for triangleInequalityInt | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
assertion | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
VC for triangleInequalityInt | 0.03 | --- | 0.07 | 0.09 | 0.01 | 0.09 | ||
VC for triangleInequalityInt | --- | --- | 7.20 | --- | --- | --- | ||
postcondition | 0.03 | --- | 0.08 | 0.04 | 0.01 | 0.55 | ||
triangleInequality | 0.05 | --- | 0.04 | 0.10 | 0.01 | 0.01 |
Theory "bitcount.AsciiCode": fully verified
Obligations | Alt-Ergo 2.0.0 | CVC4 1.4 | CVC4 1.4 (noBV) | CVC4 1.6 | Z3 4.11.2 | Z3 4.4.1 (noBV) | ||
VC for bv_even | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
assertion | --- | 0.06 | --- | --- | 0.01 | --- | ||
assertion | --- | 0.04 | --- | --- | 0.01 | --- | ||
assertion | 1.24 | --- | --- | --- | --- | --- | ||
assertion | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
VC for bv_even | 1.00 | --- | --- | --- | --- | --- | ||
VC for bv_even | 0.06 | --- | --- | --- | --- | --- | ||
postcondition | 0.14 | --- | --- | --- | --- | --- | ||
bv_odd | 0.05 | 0.03 | 0.09 | --- | --- | --- | ||
VC for numof_or | --- | 0.31 | 0.60 | --- | 0.02 | --- | ||
VC for count_or | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
assertion | --- | 0.09 | --- | --- | 0.01 | --- | ||
assertion | 0.03 | --- | 0.10 | --- | --- | 0.10 | ||
assertion | --- | --- | --- | --- | 0.01 | --- | ||
assertion | --- | --- | 2.67 | --- | --- | --- | ||
postcondition | 0.06 | 0.08 | 0.13 | --- | 0.01 | --- | ||
VC for ascii | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
out-of-bounds shifting | 0.09 | 0.05 | 0.11 | --- | 0.01 | --- | ||
assertion | --- | 0.10 | --- | --- | --- | --- | ||
assertion | 0.18 | --- | --- | --- | --- | --- | ||
assertion | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
assertion | 0.02 | --- | 0.10 | --- | --- | 0.11 | ||
assertion | 0.04 | --- | 0.14 | --- | --- | --- | ||
assertion | 0.02 | 0.17 | 0.11 | --- | --- | --- | ||
assertion | --- | --- | --- | --- | 0.02 | --- | ||
assertion | --- | --- | --- | 0.09 | --- | --- | ||
postcondition | --- | 0.11 | 2.53 | --- | --- | --- | ||
postcondition | 0.21 | --- | 1.36 | --- | 0.02 | --- | ||
VC for tmp | --- | --- | --- | --- | --- | --- | ||
split_goal_right | ||||||||
variant decrease | 0.02 | 0.04 | 0.07 | --- | 0.01 | 0.04 | ||
precondition | 0.02 | 0.02 | 0.08 | --- | 0.01 | 0.01 | ||
postcondition | --- | --- | --- | --- | 0.77 | --- | ||
asciiProp | 0.12 | 0.05 | 0.13 | --- | 0.22 | --- |