mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
517 lines
13 KiB
Plaintext
517 lines
13 KiB
Plaintext
|
|
|
|
theory BitVector
|
|
|
|
use export bool.Bool
|
|
use int.Int
|
|
use power2.Pow2int
|
|
|
|
function size : int
|
|
(* size at least 2 since we need 2-complement representation *)
|
|
axiom size_positive: size > 1
|
|
|
|
type bv
|
|
|
|
function nth bv int: bool
|
|
|
|
function bvzero : bv
|
|
axiom Nth_zero:
|
|
forall n:int. 0 <= n < size -> nth bvzero n = False
|
|
|
|
function bvone : bv
|
|
axiom Nth_one:
|
|
forall n:int. 0 <= n < size -> nth bvone n = True
|
|
|
|
predicate eq (v1 v2 : bv) =
|
|
forall n:int. 0 <= n < size -> nth v1 n = nth v2 n
|
|
|
|
axiom extensionality:
|
|
forall v1 v2 : bv. eq v1 v2 -> v1 = v2
|
|
|
|
function bw_and (v1 v2 : bv) : bv
|
|
axiom Nth_bw_and:
|
|
forall v1 v2:bv, n:int. 0 <= n < size ->
|
|
nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)
|
|
|
|
function bw_or (v1 v2 : bv) : bv
|
|
axiom Nth_bw_or:
|
|
forall v1 v2:bv, n:int. 0 <= n < size ->
|
|
nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)
|
|
|
|
function bw_xor (v1 v2 : bv) : bv
|
|
axiom Nth_bw_xor:
|
|
forall v1 v2:bv, n:int. 0 <= n < size ->
|
|
nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
|
|
|
|
lemma Nth_bw_xor_v1true:
|
|
forall v1 v2:bv, n:int. 0 <= n < size /\ nth v1 n = True ->
|
|
nth (bw_xor v1 v2) n = notb (nth v2 n)
|
|
|
|
lemma Nth_bw_xor_v1false:
|
|
forall v1 v2:bv, n:int. 0 <= n < size /\ nth v1 n = False->
|
|
nth (bw_xor v1 v2) n = nth v2 n
|
|
|
|
lemma Nth_bw_xor_v2true:
|
|
forall v1 v2:bv, n:int. 0 <= n < size /\ nth v2 n = True->
|
|
nth (bw_xor v1 v2) n = notb (nth v1 n)
|
|
|
|
lemma Nth_bw_xor_v2false:
|
|
forall v1 v2:bv, n:int. 0 <= n < size /\ nth v2 n = False->
|
|
nth (bw_xor v1 v2) n = nth v1 n
|
|
|
|
function bw_not (v : bv) : bv
|
|
axiom Nth_bw_not:
|
|
forall v:bv, n:int. 0 <= n < size ->
|
|
nth (bw_not v) n = notb (nth v n)
|
|
|
|
(* logical shift right *)
|
|
function lsr bv int : bv
|
|
(*
|
|
axiom lsr_nth_low:
|
|
forall b:bv, n s:int.
|
|
0 <= n < size -> 0 <= s ->
|
|
n+s < size -> nth (lsr b s) n = nth b (n+s)
|
|
|
|
axiom lsr_nth_high:
|
|
forall b:bv, n s:int.
|
|
0 <= n < size -> 0 <= s ->
|
|
n+s >= size -> nth (lsr b s) n = False
|
|
*)
|
|
axiom lsr_nth_low:
|
|
forall b:bv, n s:int.
|
|
0 <= n < size /\ 0 <= s<size /\
|
|
n+s < size -> nth (lsr b s) n = nth b (n+s)
|
|
|
|
axiom lsr_nth_high:
|
|
forall b:bv, n s:int.
|
|
0 <= n < size /\ 0 <= s<size /\
|
|
n+s >= size -> nth (lsr b s) n = False
|
|
|
|
(* arithmetic shift right *)
|
|
function asr bv int : bv
|
|
|
|
axiom asr_nth_low:
|
|
forall b:bv, n s:int.
|
|
0 <= n < size -> 0 <= s ->
|
|
n+s < size -> nth (asr b s) n = nth b (n+s)
|
|
|
|
axiom asr_nth_high:
|
|
forall b:bv, n s:int.
|
|
0 <= n < size -> 0 <= s ->
|
|
n+s >= size -> nth (asr b s) n = nth b (size-1)
|
|
|
|
(* logical shift left *)
|
|
function lsl bv int : bv
|
|
|
|
axiom lsl_nth_high:
|
|
forall b:bv, n s:int.
|
|
0 <= n < size -> 0 <= s ->
|
|
0 <= n-s -> nth (lsl b s) n = nth b (n-s)
|
|
|
|
axiom lsl_nth_low:
|
|
forall b:bv, n s:int.
|
|
0 <= n < size -> 0 <= s ->
|
|
0 > n-s -> nth (lsl b s) n = False
|
|
|
|
(* conversion to/from integers *)
|
|
|
|
(*
|
|
|
|
function to_nat_aux bv int : int
|
|
(* (to_nat_aux b i) returns the non-negative integer whose
|
|
binary repr is b[size-1..i] *)
|
|
|
|
axiom to_nat_aux_zero :
|
|
forall b:bv, i:int.
|
|
0 <= i < size ->
|
|
nth b i = False ->
|
|
to_nat_aux b i = 2 * to_nat_aux b (i+1)
|
|
|
|
axiom to_nat_aux_one :
|
|
forall b:bv, i:int.
|
|
0 <= i < size ->
|
|
nth b i = True ->
|
|
to_nat_aux b i = 1 + 2 * to_nat_aux b (i+1)
|
|
|
|
axiom to_nat_aux_high :
|
|
forall b:bv, i:int.
|
|
i >= size ->
|
|
to_nat_aux b i = 0
|
|
|
|
|
|
*)
|
|
|
|
|
|
(* generalization : (to_nat_sub b j i) returns the non-negative number represented
|
|
by b[j..i] *)
|
|
|
|
function to_nat_sub bv int int : int
|
|
(* (to_nat_sub b j i) returns the non-negative integer whose
|
|
binary repr is b[j..i] *)
|
|
|
|
(* axiom to_nat_sub_zero :
|
|
forall b:bv, j i:int.
|
|
0 <= i <= j ->
|
|
nth b i = False ->
|
|
to_nat_sub b j i = 2 * to_nat_sub b j (i+1)
|
|
|
|
axiom to_nat_sub_one :
|
|
forall b:bv, j i:int.
|
|
0 <= i <= j ->
|
|
nth b i = True ->
|
|
to_nat_sub b j i = 1 + 2 * to_nat_sub b j (i+1)
|
|
|
|
axiom to_nat_sub_high :
|
|
forall b:bv, j i:int.
|
|
i > j ->
|
|
to_nat_sub b j i = 0
|
|
*)
|
|
|
|
axiom to_nat_sub_zero :
|
|
forall b:bv, j i:int.
|
|
0 <= i <= j < size ->
|
|
nth b j = False ->
|
|
to_nat_sub b j i = to_nat_sub b (j-1) i
|
|
|
|
axiom to_nat_sub_one :
|
|
forall b:bv, j i:int.
|
|
0 <= i <= j < size ->
|
|
nth b j = True ->
|
|
to_nat_sub b j i = (pow2 (j-i)) + to_nat_sub b (j-1) i
|
|
|
|
axiom to_nat_sub_high :
|
|
forall b:bv, j i:int.
|
|
i > j ->
|
|
to_nat_sub b j i = 0
|
|
|
|
(* lemma to_nat_sub_low_true :
|
|
forall b:bv, j:int.nth b j = True -> to_nat_sub b j j = 1
|
|
|
|
lemma to_nat_sub_low_false :
|
|
forall b:bv, j:int.nth b j = False -> to_nat_sub b j j = 0
|
|
*)
|
|
|
|
lemma to_nat_of_zero2:
|
|
forall b:bv, i j:int. size > j >= i >= 0 ->
|
|
(forall k:int. j >= k > i -> nth b k = False) ->
|
|
to_nat_sub b j 0 = to_nat_sub b i 0
|
|
|
|
|
|
lemma to_nat_of_zero:
|
|
forall b:bv, j i:int. size > j /\ i >= 0 ->
|
|
(forall k:int. j >= k >= i -> nth b k = False) ->
|
|
to_nat_sub b j i = 0
|
|
|
|
let rec lemma to_nat_of_one (b: bv) i j
|
|
requires { size > j >= i >= 0 }
|
|
requires { forall k:int. j >= k >= i -> nth b k = True }
|
|
ensures { to_nat_sub b j i = pow2 (j-i+1) - 1 }
|
|
variant { j - i }
|
|
= if j > i then to_nat_of_one b i (j-1)
|
|
|
|
lemma to_nat_sub_footprint: forall b1 b2:bv, j i:int. size > j /\ i >=0 ->
|
|
(forall k:int. i <= k <= j -> nth b1 k = nth b2 k) ->
|
|
to_nat_sub b1 j i = to_nat_sub b2 j i
|
|
(*
|
|
lemma to_nat_sub_of_zero_ij:
|
|
forall b:bv, i j:int.
|
|
(forall k:int. j >= k >= i -> nth b k = False) ->
|
|
to_nat_sub b j i = 0
|
|
*)
|
|
|
|
(* function to_nat (b:bv) : int = to_nat_aux b 0*)
|
|
function to_nat (b:bv) : int = to_nat_sub b (size-1) 0
|
|
|
|
(* this lemma is for TestBv32*)
|
|
(*false::: lemma lsr_to_nat_sub:
|
|
forall b:bv, n s:int.
|
|
0 <= s <size -> to_nat_sub (lsr b s) (size -1) 0 = to_nat_sub b (size-1-s) 0*)
|
|
(*
|
|
lemma lsr_to_nat_sub:
|
|
forall b:bv, n s:int.
|
|
0 <= s <size -> to_nat_sub (lsr b s) (size -1) 0 = to_nat_sub b (size-1) s
|
|
*)
|
|
|
|
(* 2-complement version *)
|
|
|
|
(*
|
|
|
|
function to_int_aux bv int : int
|
|
(* (to_int_aux b i) returns the integer whose
|
|
2-complement binary repr is b[size-1..i] *)
|
|
|
|
axiom to_int_aux_zero :
|
|
forall b:bv, i:int.
|
|
0 <= i < size-1 ->
|
|
nth b i = False ->
|
|
to_int_aux b i = 2 * to_int_aux b (i+1)
|
|
|
|
axiom to_int_aux_one :
|
|
forall b:bv, i:int.
|
|
0 <= i < size-1 ->
|
|
nth b i = True ->
|
|
to_int_aux b i = 1 + 2 * to_int_aux b (i+1)
|
|
|
|
axiom to_int_aux_pos :
|
|
forall b:bv. nth b (size-1) = False ->
|
|
to_int_aux b (size-1) = 0
|
|
|
|
axiom to_int_aux_neg :
|
|
forall b:bv. nth b (size-1) = True ->
|
|
to_int_aux b (size-1) = -1
|
|
lemma to_int_zero:
|
|
forall b:bv. (forall i:int. 0 <= i <size-1-> nth b i = False)
|
|
-> to_int_aux b 0 = 0
|
|
lemma to_int_one:
|
|
forall b:bv. (forall i:int. 0 <= i <size-> nth b i = True)
|
|
-> to_int_aux b 0 = -1
|
|
|
|
|
|
function to_int (b:bv) : int = to_int_aux b 0
|
|
|
|
*)
|
|
|
|
(* (from_uint n) returns the bitvector representing the non-negative
|
|
integer n on size bits. *)
|
|
function from_int (n:int) : bv
|
|
|
|
use int.EuclideanDivision
|
|
|
|
|
|
(* axiom nth_from_int_high:
|
|
forall n i:int. size>i > 0 -> nth (from_int n) i = nth (from_int (div n 2)) (i-1)
|
|
*)
|
|
|
|
|
|
(*Notice: replace 0 <= i <size by 0 <= i < size-1 because the bit at (size -1) is the sign of i*)
|
|
(* axiom from_int_sign_positive:
|
|
forall n:int. n>=0 -> nth (from_int n) (size - 1) = False
|
|
axiom from_int_sign_negative:
|
|
forall n:int. n<0 -> nth (from_int n) (size - 1) = True
|
|
*)
|
|
|
|
axiom nth_from_int_high_even:
|
|
forall n i:int. size > i >= 0 /\ mod (div n (pow2 i)) 2 = 0 -> nth (from_int n) i = False
|
|
|
|
axiom nth_from_int_high_odd:
|
|
forall n i:int. size > i >= 0 /\ mod (div n (pow2 i)) 2 <> 0 -> nth (from_int n) i = True
|
|
|
|
lemma nth_from_int_low_even:
|
|
forall n:int. mod n 2 = 0 -> nth (from_int n) 0 = False
|
|
|
|
lemma nth_from_int_low_odd:
|
|
forall n:int. mod n 2 <> 0 -> nth (from_int n) 0 = True
|
|
|
|
lemma nth_from_int_0:
|
|
forall i:int. size > i >= 0 -> nth (from_int 0) i = False
|
|
|
|
(*********************************************************************)
|
|
(*from_int2c: int -> bv *)
|
|
(* Take an integer as input and returns a bv with 2-complement*)
|
|
(* bit size-1:sign, false if n is non-negative, true otherwise*)
|
|
(*********************************************************************)
|
|
function from_int2c (n:int) : bv
|
|
|
|
(*********************************************************************)
|
|
(* axiom for n is non-negative *)
|
|
(*********************************************************************)
|
|
|
|
axiom nth_sign_positive:
|
|
forall n :int. n>=0 -> nth (from_int2c n) (size-1) = False
|
|
|
|
(*********************************************************************)
|
|
(* axiom for n is negative *)
|
|
(*********************************************************************)
|
|
|
|
axiom nth_sign_negative:
|
|
forall n:int. n<0 -> nth (from_int2c n) (size-1) = True
|
|
|
|
(*********************************************************************)
|
|
(* axioms for any n *)
|
|
(*********************************************************************)
|
|
|
|
axiom nth_from_int2c_high_even:
|
|
forall n i:int. size-1 > i >= 0 /\ mod (div n (pow2 i)) 2 = 0
|
|
-> nth (from_int2c n) i = False
|
|
|
|
axiom nth_from_int2c_high_odd:
|
|
forall n i:int. size-1 > i >= 0 /\ mod (div n (pow2 i)) 2 <> 0
|
|
-> nth (from_int2c n) i = True
|
|
|
|
lemma nth_from_int2c_low_even:
|
|
forall n:int. mod n 2 = 0 -> nth (from_int2c n) 0 = False
|
|
|
|
lemma nth_from_int2c_low_odd:
|
|
forall n:int. mod n 2 <> 0 -> nth (from_int2c n) 0 = True
|
|
|
|
lemma nth_from_int2c_0:
|
|
forall i:int. size > i >= 0 -> nth (from_int2c 0) i = False
|
|
|
|
lemma nth_from_int2c_plus_pow2:
|
|
forall x k i:int. 0 <= k < i /\ k < size-1 ->
|
|
nth (from_int2c (x+pow2 i)) k = nth (from_int2c x) k
|
|
|
|
end
|
|
|
|
|
|
theory BV32
|
|
|
|
function size : int = 32
|
|
|
|
clone export BitVector with function size, lemma size_positive, axiom .
|
|
|
|
end
|
|
|
|
|
|
theory BV64
|
|
|
|
function size : int = 64
|
|
|
|
clone export BitVector with function size, lemma size_positive, axiom .
|
|
|
|
end
|
|
|
|
theory BV32_64
|
|
|
|
use int.Int
|
|
|
|
use BV32 as BV32
|
|
use BV64 as BV64
|
|
|
|
function concat BV32.bv BV32.bv : BV64.bv
|
|
|
|
axiom concat_low: forall b1 b2:BV32.bv.
|
|
forall i:int. 0 <= i < 32 -> BV64.nth (concat b1 b2) i = BV32.nth b2 i
|
|
|
|
axiom concat_high: forall b1 b2:BV32.bv.
|
|
forall i:int. 32 <= i < 64 -> BV64.nth (concat b1 b2) i = BV32.nth b1 (i-32)
|
|
|
|
end
|
|
|
|
|
|
theory TestBv32
|
|
|
|
use BV32
|
|
use int.Int
|
|
|
|
goal Test1:
|
|
let b = bw_and bvzero bvone in nth b 1 = False
|
|
|
|
goal Test2:
|
|
let b = lsr bvone 16 in nth b 15 = True
|
|
|
|
goal Test3:
|
|
let b = lsr bvone 16 in nth b 16 = False
|
|
|
|
goal Test4:
|
|
let b = asr bvone 16 in nth b 15 = True
|
|
|
|
goal Test5:
|
|
let b = asr bvone 16 in nth b 16 = True
|
|
|
|
goal Test6:
|
|
let b = asr (lsr bvone 1) 16 in nth b 16 = False
|
|
|
|
goal to_nat_0x00000000:
|
|
to_nat bvzero = 0
|
|
|
|
goal to_nat_0x00000001:
|
|
to_nat (lsr bvone 31) = 1
|
|
|
|
goal to_nat_0x00000003:
|
|
to_nat (lsr bvone 30) = 3
|
|
|
|
goal to_nat_0x00000007:
|
|
to_nat (lsr bvone 29) = 7
|
|
|
|
goal to_nat_0x0000000F:
|
|
to_nat (lsr bvone 28) = 15
|
|
|
|
goal to_nat_0x0000001F:
|
|
to_nat (lsr bvone 27) = 31
|
|
|
|
goal to_nat_0x0000003F:
|
|
to_nat (lsr bvone 26) = 63
|
|
|
|
goal to_nat_0x0000007F:
|
|
to_nat (lsr bvone 25) = 127
|
|
|
|
goal to_nat_0x000000FF:
|
|
to_nat (lsr bvone 24) = 255
|
|
|
|
goal to_nat_0x000001FF:
|
|
to_nat (lsr bvone 23) = 511
|
|
|
|
goal to_nat_0x000003FF:
|
|
to_nat (lsr bvone 22) = 1023
|
|
|
|
goal to_nat_0x000007FF:
|
|
to_nat (lsr bvone 21) = 2047
|
|
|
|
goal to_nat_0x00000FFF:
|
|
to_nat (lsr bvone 20) = 4095
|
|
|
|
goal to_nat_0x00001FFF:
|
|
to_nat (lsr bvone 19) = 8191
|
|
|
|
goal to_nat_0x00003FFF:
|
|
to_nat (lsr bvone 18) = 16383
|
|
|
|
goal to_nat_0x00007FFF:
|
|
to_nat (lsr bvone 17) = 32767
|
|
|
|
goal to_nat_0x0000FFFF:
|
|
to_nat (lsr bvone 16) = 65535
|
|
|
|
(*
|
|
goal to_nat_smoke:
|
|
to_nat (lsr bvone 16) = 65536
|
|
*)
|
|
|
|
goal to_nat_0x0001FFFF:
|
|
to_nat (lsr bvone 15) = 131071
|
|
|
|
goal to_nat_0x0003FFFF:
|
|
to_nat (lsr bvone 14) = 262143
|
|
|
|
goal to_nat_0x0007FFFF:
|
|
to_nat (lsr bvone 13) = 524287
|
|
|
|
goal to_nat_0x000FFFFF:
|
|
to_nat (lsr bvone 12) = 1048575
|
|
|
|
goal to_nat_0x00FFFFFF:
|
|
to_nat (lsr bvone 8) = 16777215
|
|
|
|
goal to_nat_0xFFFFFFFF:
|
|
to_nat bvone = 4294967295
|
|
|
|
(*
|
|
goal to_int_0x00000000:
|
|
to_int bvzero = 0
|
|
|
|
goal to_int_0xFFFFFFFF:
|
|
to_int bvone = -1
|
|
|
|
goal to_int_0x7FFFFFFF:
|
|
to_int (lsr bvone 1) = 2147483647
|
|
|
|
goal to_int_0x80000000:
|
|
to_int (lsl bvone 31) = -2147483648
|
|
|
|
goal to_int_0x0000FFFF:
|
|
to_int (lsr bvone 16) = 65535
|
|
|
|
goal to_int_smoke:
|
|
to_int (lsr bvone 16) = 65536
|
|
|
|
*)
|
|
|
|
end
|
|
|
|
(*
|
|
Local Variables:
|
|
compile-command: "why3 ide -L . bitvector.why"
|
|
End:
|
|
*)
|