mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
496 lines
16 KiB
Plaintext
496 lines
16 KiB
Plaintext
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
|
|
|
|
(** {2 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 *)
|
|
|
|
(** {4 Checksum computation and correctness} *)
|
|
|
|
(** 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.) *)
|
|
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 *)
|
|
|
|
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
|
|
|
|
(*** unfinished
|
|
|
|
module GrayCode
|
|
use int.Int
|
|
use int.NumOf
|
|
use number.Parity
|
|
use bool.Bool
|
|
use mach.bv.BVCheck32
|
|
use BitCounting32
|
|
use Hamming
|
|
|
|
constant one : t = 1 : t
|
|
constant lastbit : t = sub size_bv one
|
|
|
|
(** {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 =
|
|
bw_xor bv (lsr_bv bv one)
|
|
|
|
function fromGray (gr : t) : t =
|
|
let b = bw_xor gr (lsr_bv gr (1 : t)) in
|
|
let b = bw_xor b (lsr_bv b (2 : t)) in
|
|
let b = bw_xor b (lsr_bv b (4 : t)) in
|
|
let b = bw_xor b (lsr_bv b (8 : t)) in
|
|
bw_xor b (lsr_bv b (16 : t))
|
|
|
|
(** 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. *)
|
|
|
|
let lemma grayIsGray (b:t)
|
|
ensures { Hamming.hammingD_logic (toGray b) (toGray (add b one)) = 1 }
|
|
=
|
|
assert { b <> ones -> toGray (add b one) = bw_xor (toGray b) (bw_and (bw_not b) (add b one)) };
|
|
assert { b <> ones -> exists k. (bw_and (bw_not b) (add b one)) = lsl one k };
|
|
assert { b <> ones -> count_logic (bw_and (bw_not b) (add b one)) = 1 };
|
|
assert { b = ones -> (toGray b) = 0x80000000 : t /\ (toGray (add b one)) = zeros }
|
|
|
|
(** 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 ->
|
|
xorb (nth_bv b i) (nth_bv b (add i one)) <-> nth_bv (toGray b) i
|
|
|
|
(** (using 0 if there is no bit to the left of i) *)
|
|
|
|
lemma lastNthGray: forall b.
|
|
nth_bv (toGray b) lastbit <-> nth_bv b lastbit
|
|
|
|
(** 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_bv ->
|
|
nth_bv (fromGray b) i <-> even (count_logic (lsr_bv b i))
|
|
|
|
(** 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.
|
|
nth_bv b zeros <-> even (count_logic (toGray b))
|
|
|
|
end
|
|
|
|
*)
|