Commit dfa8bcc8 authored by MARCHE Claude's avatar MARCHE Claude

Tuyen's example moved into directory examples

parent 8983327a
theory BitVector
use export bool.Bool
use import int.Int
use import 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, i j:int. size > j /\ i >= 0 ->
(forall k:int. j >= k >= i -> nth b k = False) ->
to_nat_sub b j i = 0
lemma to_nat_of_one:
forall b:bv, i j:int. size > j >= i >= 0 ->
(forall k:int. j >= k >= i -> nth b k = True) ->
to_nat_sub b j i = pow2 (j-i+1) - 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 import 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 pow2i:
forall i:int. i>=0 -> (pow2 i) <>0
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 ->
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 = size
end
theory BV64
function size : int = 64
clone export BitVector with function size = size
end
theory BV32_64
use import int.Int
use BV32
use 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 import BV32
use import 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_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: "why3ide -L . bitvector.why"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="bitvector/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Gappa"
version="0.16.0"/>
<prover
id="4"
name="Z3"
version="2.19"/>
<prover
id="5"
name="Z3"
version="3.2"/>
<file
name="../bitvector.why"
verified="false"
expanded="true">
<theory
name="BitVector"
locfile="bitvector/../bitvector.why"
loclnum="3" loccnumb="7" loccnume="16"
verified="false"
expanded="true">
<goal
name="Nth_bw_xor_v1true"
locfile="bitvector/../bitvector.why"
loclnum="46" loccnumb="8" loccnume="25"
sum="a6c6ccf4906fa07fcd445cb7a039356c"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0V1V2anotbanthV1V2Iainfix =anthV0V2aTrueAainfix &lt;V2asizeAainfix &lt;=c0V2F">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.26"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Nth_bw_xor_v1false"
locfile="bitvector/../bitvector.why"
loclnum="50" loccnumb="8" loccnume="26"
sum="e6e0951a1637f11d84018d47b038154d"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0V1V2anthV1V2Iainfix =anthV0V2aFalseAainfix &lt;V2asizeAainfix &lt;=c0V2F">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Nth_bw_xor_v2true"
locfile="bitvector/../bitvector.why"
loclnum="54" loccnumb="8" loccnume="25"
sum="a72599df84122319527c0f26a292896e"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0V1V2anotbanthV0V2Iainfix =anthV1V2aTrueAainfix &lt;V2asizeAainfix &lt;=c0V2F">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Nth_bw_xor_v2false"
locfile="bitvector/../bitvector.why"
loclnum="58" loccnumb="8" loccnume="26"
sum="d4096a332b3ebed9e46ded167c700486"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0V1V2anthV0V2Iainfix =anthV1V2aFalseAainfix &lt;V2asizeAainfix &lt;=c0V2F">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.25"/>
</proof>
<proof
<