diff --git a/examples/bitvectors/bitvector.why b/examples/bitvectors/bitvector.why new file mode 100644 index 0000000000000000000000000000000000000000..6bcc3421d43cc1b2d25a24da9ccfd32945c05dbb --- /dev/null +++ b/examples/bitvectors/bitvector.why @@ -0,0 +1,509 @@ + + +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 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 -> 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 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 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 nth b i = False) + -> to_int_aux b 0 = 0 + lemma to_int_one: + forall b:bv. (forall i:int. 0 <= i 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 =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: +*) diff --git a/examples/bitvectors/bitvector/why3session.xml b/examples/bitvectors/bitvector/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..e72fe0f3616a4e09a56f1dbb2c53830b96d15de8 --- /dev/null +++ b/examples/bitvectors/bitvector/why3session.xml @@ -0,0 +1,726 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/bitvectors/double.why b/examples/bitvectors/double.why new file mode 100644 index 0000000000000000000000000000000000000000..dd63b9ae388a08c8d608aa674d168d2aa96400ae --- /dev/null +++ b/examples/bitvectors/double.why @@ -0,0 +1,90 @@ +theory BV_double + + use import int.Int + use import real.RealInfix + use import real.FromInt + use import power2.Pow2real + use import bitvector.BV64 + + function double_of_bv64 (b:bv) : real + + (* TODO: axioms + + real represented by bv = sign . exp . mantissa + + sign on bit 63 + + exp on bits 62..52 + + mantissa on bits 51..0 + + si exp = 0 : zero or denormalized, we specify only zero + + si exp = 2047 : infinities or nan, we don't specify anything + + si 1 <= exp <= 2046 : the number represented is + + (-1)^sign * 2^(exp - bias) * (1 + mantissa * 2^(1-prec)) + + where bias = 1023, prec = 53 + (e.g. the largest representable number is 2^(2046-1023) * (1+ (2^52-1)* 2^(-52)) = + 2^1023 * (1 + 1 - 2^-52) = 2^1024 - 2^(1023-52) = 2^1024 - 2^971 +) + + *) + + function exp (b:bv) : int = BV64.to_nat_sub b 62 52 + function mantissa (b:bv) : int = BV64.to_nat_sub b 51 0 + function sign (b:bv) : bool = BV64.nth b 63 + + function sign_value(s:bool):real + + axiom sign_value_false: + sign_value(False) = 1.0 + + axiom sign_value_true: + sign_value(True) = -.1.0 + + axiom zero : forall b:bv. + exp(b) = 0 /\ mantissa(b) = 0 -> double_of_bv64(b) = 0.0 + + axiom sign_of_double_positive: + forall b:bv. sign b = False -> double_of_bv64(b) >=. 0.0 + axiom sign_of_double_negative: + forall b:bv. sign b = True -> double_of_bv64(b) <=. 0.0 + + axiom double_of_bv64_value: + forall b:bv. 0 < exp(b) < 2047 -> + double_of_bv64(b) = + sign_value(sign(b)) *. + (pow2 ((exp b) - 1023)) *. + (1.0 +. (FromInt.from_int (mantissa b)) *. (pow2 (-52))) + +end + +theory TestDouble + + use import int.Int + use import bitvector.BV64 + use import BV_double + + function one:bv = from_int 4607182418800017408 (* 1.0 *) + + lemma nth_one1: forall i:int. 0 <= i <= 51 -> nth one i = False + lemma nth_one2: forall i:int. 52 <= i <= 61 -> nth one i = True + lemma nth_one3: forall i:int. 62 <= i <= 63 -> nth one i = False + + lemma sign_one: sign(one) = False + lemma exp_one: exp(one) = 1023 + lemma mantissa_one: mantissa(one) = 0 + + lemma double_value_of_1: double_of_bv64(one) = 1.0 + +end + + +(* +Local Variables: +compile-command: "why3ide -L . double.why" +End: +*) diff --git a/examples/bitvectors/double/why3session.xml b/examples/bitvectors/double/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..41de418a4c6c9c60e1214368260078d5f716f4bf --- /dev/null +++ b/examples/bitvectors/double/why3session.xml @@ -0,0 +1,255 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/bitvectors/double_of_int.why b/examples/bitvectors/double_of_int.why new file mode 100644 index 0000000000000000000000000000000000000000..79e790d73c984c5a254c157cbf76c1c0a94cd222 --- /dev/null +++ b/examples/bitvectors/double_of_int.why @@ -0,0 +1,229 @@ + + +theory DoubleOfInt + + use import int.Int + use import bool.Bool + use import real.RealInfix + use import real.FromInt + + use power2.Pow2int + use power2.Pow2real + use bitvector.BV32 + use bitvector.BV64 + use bitvector.BV32_64 + use import double.BV_double + + (*********************************************************************) + (* j = 0x43300000 *) + (* j' = 0x80000000 *) + (*********************************************************************) + + function j : BV32.bv = BV32.from_int 0x43300000 + + function j' : BV32.bv = BV32.from_int 0x80000000 + lemma jp0_30: forall i:int. 0<=i<30 -> BV32.nth j' i = False + + (*********************************************************************) + (* definitions: *) + (* const : bv64 = concat j j' *) + (* const_as_double : real = double_of_bv64(const) *) + (*********************************************************************) + + function const : BV64.bv = BV32_64.concat j j' + + function const_as_double : real = double_of_bv64 const + + (*********************************************************************) + (* next lemma: const_as_double = 2^52 + 2^31 *) + (*********************************************************************) + + lemma nth_const1: forall i:int. 0 <= i <= 30 -> BV64.nth const i = False + lemma nth_const2: BV64.nth const 31 = True + lemma nth_const3: forall i:int. 32 <= i <= 51 -> BV64.nth const i = False + lemma nth_const4: forall i:int. 52 <= i <= 53 -> BV64.nth const i = True + lemma nth_const5: forall i:int. 54 <= i <= 55 -> BV64.nth const i = False + lemma nth_const6: forall i:int. 56 <= i <= 57 -> BV64.nth const i = True + lemma nth_const7: forall i:int. 58 <= i <= 61 -> BV64.nth const i = False + lemma nth_const8: BV64.nth const 62 = True + lemma nth_const9: BV64.nth const 63 = False + + lemma sign_const: sign(const) = False + + lemma exp_const: exp(const) = 1075 + + lemma to_nat_mantissa_1: (BV64.to_nat_sub const 30 0) = 0 + + lemma mantissa_const_nth2: + forall i:int. 32 <= i <= 51 -> BV64.nth const i = False + + lemma mantissa_const_to_nat51: + BV64.to_nat_sub const 51 0 = BV64.to_nat_sub const 31 0 + + lemma mantissa_const: mantissa(const) = Pow2int.pow2 31 + + lemma real1075m1023: from_int (1075 - 1023) = 52.0 + + lemma real1075m1023_2: 1075.0 -. 1023.0 = 52.0 + + lemma real52_a_m52: Pow2real.pow2 (1075 - 1023) *. Pow2real.pow2 31 *. Pow2real.pow2 (-52) = Pow2real.pow2 31 + + lemma const_value0: const_as_double = + 1.0*.Pow2real.pow2 (1075 - 1023) *. (1.0 +. Pow2real.pow2 31 *. Pow2real.pow2 (-52)) + + lemma const_value: const_as_double = Pow2real.pow2 52 +. Pow2real.pow2 31 + + (*********************************************************************) + (* definitions: *) + (* var(x) : bv64 = concat j (j' xor x) *) + (* var_as_double(x) : real = double_of_bv64(var(x)) *) + (*********************************************************************) + + function jpxor(i:int): BV32.bv = (BV32.bw_xor j' (BV32.from_int2c i)) + + function var(i:int): BV64.bv = (BV32_64.concat j (jpxor i)) + + function var_as_double(x:int) : real = double_of_bv64 (var x) + + (*********************************************************************) + (* lemma 1: for all integer x, to_nat(jpxor(x)) = 2^31 + x *) + (*********************************************************************) + + predicate is_int32(x:int) = - Pow2int.pow2 31 <= x < Pow2int.pow2 31 + +(* + lemma two_compl_pos: forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x + lemma two_compl_neg: forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = Pow2int.pow2 32 + x +*) + + (* bits of jpxor x *) + lemma nth_0_30: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=30 -> + BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) i = BV32.nth (BV32.from_int2c x) i + lemma nth_jpxor_0_30: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=30 -> + BV32.nth (jpxor x) i = BV32.nth (BV32.from_int2c x) i + lemma nth_var31: + forall x:int. (BV32.nth (jpxor x) 31) = notb (BV32.nth (BV32.from_int2c x) 31) + + lemma to_nat_sub_0_30: forall x:int. is_int32(x) -> + (BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0) + + + + (* case x >= 0 *) + + lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True + +(* + lemma from_int2c_to_nat_sub31: + forall x:int. x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x +*) + + lemma from_int2c_to_nat_sub_gen: + forall i:int. 0 <= i <= 30 -> + forall x:int. 0 <= x < Pow2int.pow2 i -> + BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x + + lemma from_int2c_to_nat_sub: + forall x:int. is_int32(x) /\ x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 30 0 = x + + lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x + + (* case x < 0 *) + + lemma to_nat_sub_0_30_neg: forall x:int. is_int32(x) /\ x<0 -> + (BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0) + + lemma to_nat_sub_0_30_neg1: forall x:int. is_int32(x) /\ x<0 -> + (BV32.to_nat_sub (BV32.from_int2c x) 30 0) = Pow2int.pow2 31 + x + + lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x + + (* final lemma *) + + lemma lemma1 : forall x:int. is_int32 x -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x + + + (*********************************************************************) + (* lemma 2: for all integer x, mantissa(var(x)) = 2^31 + x *) + (*********************************************************************) + + lemma nth_var_0_31: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=31-> + BV64.nth (var x) i = BV32.nth (jpxor x) i + lemma to_nat_bv32_bv64_aux: forall b1:BV32.bv. forall b2:BV32.bv. forall j:int. 0<=j<32-> BV64.to_nat_sub (BV32_64.concat b1 b2) j 0 = BV32.to_nat_sub b2 j 0 + lemma to_nat_bv32_bv64: forall b1:BV32.bv. forall b2:BV32.bv. BV64.to_nat_sub (BV32_64.concat b1 b2) 31 0 = BV32.to_nat_sub b2 31 0 + + lemma to_nat_var_0_31: forall x:int. is_int32(x) -> + BV64.to_nat_sub (var x) 31 0 = BV32.to_nat_sub (jpxor x) 31 0 + lemma nth_var32to63: + forall x k:int. 32 <= k <= 63 -> BV64.nth (var x) k = BV32.nth j (k - 32) + + lemma nth_var3: forall x:int. forall i:int. 32 <= i <= 51 -> BV64.nth (var x) i = False + + lemma lemma2 : forall x:int. is_int32 x -> mantissa(var(x)) = Pow2int.pow2 31 + x + + (*********************************************************************) + (* lemma 3: for all integer x, exp(var(x)) = 1075 *) + (*********************************************************************) + + lemma nth_var4: forall x:int. forall i:int. 52 <= i <= 53 -> BV64.nth (var x) i = True + lemma nth_var5: forall x:int. forall i:int. 54 <= i <= 55 -> BV64.nth (var x) i = False + lemma nth_var6: forall x:int. forall i:int. 56 <= i <= 57 -> BV64.nth (var x) i = True + lemma nth_var7: forall x:int. forall i:int. 58 <= i <= 61 -> BV64.nth (var x) i = False + lemma nth_var8: forall x:int. BV64.nth (var x) 62 = True + + lemma lemma3 : forall x:int. exp(var(x)) = 1075 + + (*********************************************************************) + (* lemma 4: for all integer x, sign(var(x)) = false *) + (*********************************************************************) + + lemma nth_var9: forall x:int. BV64.nth (var x) 63 = False + + lemma lemma4 : forall x:int. sign(var(x)) = False + + (*********************************************************************) + (* lemma 5: for all integer x, var_as_double(x) = 2^52 + 2^31 + x *) + (*********************************************************************) + lemma sign_var: forall x:int. sign(var(x)) = False + (*proved by Coq*) + lemma var_value0: forall x:int. is_int32(x) ->var_as_double(x) = + Pow2real.pow2 (1075 - 1023) *. (1.0 +. (from_int (Pow2int.pow2 31 + x)) *. Pow2real.pow2 (-52)) + + + lemma from_int_sum : forall x:int. is_int32(x)-> + from_int (Pow2int.pow2 31 + x) = from_int (Pow2int.pow2 31) +. from_int x + + lemma var_value3: forall x:int. is_int32(x)->var_as_double(x) = + Pow2real.pow2 52 +. Pow2real.pow2 52 *. (from_int (Pow2int.pow2 31) +. from_int x) *. Pow2real.pow2 (-52) + + + lemma distr_pow52 : forall x:real. + Pow2real.pow2 52 *. x *. Pow2real.pow2 (-52) = x + + lemma var_value4: forall x:int. is_int32(x)->var_as_double(x) = + Pow2real.pow2 52 +. (from_int (Pow2int.pow2 31)) +. from_int x + + lemma pow31 : from_int (Pow2int.pow2 31) = Pow2real.pow2 31 + + lemma lemma5: forall x:int. is_int32(x)-> var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x) + + + + (*********************************************************************) + (* main result *) + (*********************************************************************) + + function double_of_int32 (x:int) : real = var_as_double(x) -. const_as_double + + lemma MainResult: forall x:int. is_int32 x -> double_of_int32 x = from_int x + + +end + + + +(* +Local Variables: +compile-command: "why3ide -L . double_of_int.why" +End: +*) diff --git a/examples/bitvectors/double_of_int/why3session.xml b/examples/bitvectors/double_of_int/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..0c29a3cca494839dd8ffc7de3c3986aa0066d87d --- /dev/null +++ b/examples/bitvectors/double_of_int/why3session.xml @@ -0,0 +1,1978 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/bitvectors/neg_as_xor.why b/examples/bitvectors/neg_as_xor.why new file mode 100644 index 0000000000000000000000000000000000000000..9fd2249682d994796a57e11da596cc57b7d5e258 --- /dev/null +++ b/examples/bitvectors/neg_as_xor.why @@ -0,0 +1,45 @@ + +theory TestNegAsXOR + + use import int.Int + use import bool.Bool + use import real.RealInfix + + use import bitvector.BV64 + use import double.BV_double + + function j : bv = from_int 0x8000000000000000 + + lemma Nth_j: forall i:int. 0 <= i <= 62 -> nth j i = False + + lemma sign_of_j: sign(j) = True + lemma mantissa_of_j: mantissa(j) = 0 + lemma exp_of_j: exp(j) = 0 + lemma int_of_bv: double_of_bv64(j) = 0.0 + + lemma MainResultBits : forall x:bv. forall i:int. 0 <= i < 63 -> + nth (bw_xor x j) i = nth x i + + lemma MainResultSign : forall x:bv. nth (bw_xor x j) 63 = notb (nth x 63) + + lemma Sign_of_xor_j : forall x:bv. sign(bw_xor x j) = notb (sign x) + + lemma Exp_of_xor_j : forall x:bv. exp(bw_xor x j) = exp(x) + + lemma Mantissa_of_xor_j : forall x:bv. mantissa(bw_xor x j) = mantissa(x) + + lemma MainResultZero : forall x:bv. 0 = exp(x) /\ mantissa(x) = 0 -> + double_of_bv64 (bw_xor x j) = -. double_of_bv64 x + + lemma sign_neg: + forall x:bv. sign_value(notb(sign(x))) = -.sign_value(sign(x)) + lemma MainResult : forall x:bv. 0 < exp(x) < 2047 -> + double_of_bv64 (bw_xor x j) = -. double_of_bv64 x + +end + +(* +Local Variables: +compile-command: "why3ide -L . neg_as_xor.why" +End: +*) diff --git a/examples/bitvectors/neg_as_xor/why3session.xml b/examples/bitvectors/neg_as_xor/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..092f249a210a207bb620ce04be08c06ba6fac49b --- /dev/null +++ b/examples/bitvectors/neg_as_xor/why3session.xml @@ -0,0 +1,390 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/bitvectors/power2.why b/examples/bitvectors/power2.why new file mode 100644 index 0000000000000000000000000000000000000000..493de6366a0ce9bb6bc5355bc42a8dd1f534038e --- /dev/null +++ b/examples/bitvectors/power2.why @@ -0,0 +1,127 @@ +theory Pow2int + + use import int.Int + + function pow2 (i:int) : int + + axiom Power_0 : pow2 0 = 1 + + axiom Power_s : forall n: int. n >= 0 -> pow2 (n+1) = 2 * pow2 n + + lemma Power_1 : pow2 1 = 2 + + lemma Power_sum : + forall n m: int. n >= 0 /\ m >= 0 -> pow2 (n+m) = pow2 n * pow2 m + + lemma pow2_0: pow2 0 = 1 + lemma pow2_1: pow2 1 = 2 + lemma pow2_2: pow2 2 = 4 + lemma pow2_3: pow2 3 = 8 + lemma pow2_4: pow2 4 = 16 + lemma pow2_5: pow2 5 = 32 + lemma pow2_6: pow2 6 = 64 + lemma pow2_7: pow2 7 = 128 + lemma pow2_8: pow2 8 = 256 + lemma pow2_9: pow2 9 = 512 + lemma pow2_10: pow2 10 = 1024 + lemma pow2_11: pow2 11 = 2048 + lemma pow2_12: pow2 12 = 4096 + lemma pow2_13: pow2 13 = 8192 + lemma pow2_14: pow2 14 = 16384 + lemma pow2_15: pow2 15 = 32768 + lemma pow2_16: pow2 16 = 65536 + lemma pow2_17: pow2 17 = 131072 + lemma pow2_18: pow2 18 = 262144 + lemma pow2_19: pow2 19 = 524288 + lemma pow2_20: pow2 20 = 1048576 + lemma pow2_21: pow2 21 = 2097152 + lemma pow2_22: pow2 22 = 4194304 + lemma pow2_23: pow2 23 = 8388608 + lemma pow2_24: pow2 24 = 16777216 + lemma pow2_25: pow2 25 = 33554432 + lemma pow2_26: pow2 26 = 67108864 + lemma pow2_27: pow2 27 = 134217728 + lemma pow2_28: pow2 28 = 268435456 + lemma pow2_29: pow2 29 = 536870912 + lemma pow2_30: pow2 30 = 1073741824 + lemma pow2_31: pow2 31 = 2147483648 + lemma pow2_32: pow2 32 = 4294967296 + lemma pow2_33: pow2 33 = 8589934592 + lemma pow2_34: pow2 34 = 17179869184 + lemma pow2_35: pow2 35 = 34359738368 + lemma pow2_36: pow2 36 = 68719476736 + lemma pow2_37: pow2 37 = 137438953472 + lemma pow2_38: pow2 38 = 274877906944 + lemma pow2_39: pow2 39 = 549755813888 + lemma pow2_40: pow2 40 = 1099511627776 + lemma pow2_41: pow2 41 = 2199023255552 + lemma pow2_42: pow2 42 = 4398046511104 + lemma pow2_43: pow2 43 = 8796093022208 + lemma pow2_44: pow2 44 = 17592186044416 + lemma pow2_45: pow2 45 = 35184372088832 + lemma pow2_46: pow2 46 = 70368744177664 + lemma pow2_47: pow2 47 = 140737488355328 + lemma pow2_48: pow2 48 = 281474976710656 + lemma pow2_49: pow2 49 = 562949953421312 + lemma pow2_50: pow2 50 = 1125899906842624 + lemma pow2_51: pow2 51 = 2251799813685248 + lemma pow2_52: pow2 52 = 4503599627370496 + lemma pow2_53: pow2 53 = 9007199254740992 + lemma pow2_54: pow2 54 = 18014398509481984 + lemma pow2_55: pow2 55 = 36028797018963968 + lemma pow2_56: pow2 56 = 72057594037927936 + lemma pow2_57: pow2 57 = 144115188075855872 + lemma pow2_58: pow2 58 = 288230376151711744 + lemma pow2_59: pow2 59 = 576460752303423488 + lemma pow2_60: pow2 60 = 1152921504606846976 + lemma pow2_61: pow2 61 = 2305843009213693952 + lemma pow2_62: pow2 62 = 4611686018427387904 + lemma pow2_63: pow2 63 = 9223372036854775808 + +end + +theory Pow2real + + use import int.Int + use import real.RealInfix + + function pow2 (i:int) : real + axiom Power_0 : pow2 0 = 1.0 + axiom Power_s : forall n: int. n >= 0 -> pow2 (n+1) = 2.0 *. pow2 n + axiom Power_p : forall n: int. n <= 0 -> pow2 (n-1) = 0.5 *. pow2 n + + lemma Power_s_all : forall n:int. pow2 (n+1) = 2.0 *. pow2 n + + lemma Power_p_all : forall n:int. pow2 (n-1) = 0.5 *. pow2 n + + lemma Power_1_2: 0.5 = 1.0 /. 2.0 + + lemma Power_1 : pow2 1 = 2.0 + + lemma Power_neg1 : pow2 (-1) = 0.5 + + lemma Power_non_null_aux: forall n:int.n>=0 -> pow2 n <> 0.0 + + lemma Power_neg_aux : forall n:int. n>=0 -> pow2 (-n) = 1.0 /. pow2 n + + lemma Power_non_null: forall n:int. pow2 n <> 0.0 + + lemma Power_neg : forall n:int. pow2 (-n) = 1.0 /. pow2 n + + lemma Power_sum_aux : forall n m: int. m >= 0 -> pow2 (n+m) = pow2 n *. pow2 m + + lemma Power_sum : forall n m: int. pow2 (n+m) = pow2 n *. pow2 m + + use Pow2int + use import real.FromInt + + lemma Pow2_int_real: + forall x:int. x >= 0 -> pow2 x = from_int (Pow2int.pow2 x) + +end + +(* +Local Variables: +compile-command: "why3ide power2.why" +End: +*) diff --git a/examples/bitvectors/power2/power2_Pow2int_Power_sum_1.v b/examples/bitvectors/power2/power2_Pow2int_Power_sum_1.v new file mode 100644 index 0000000000000000000000000000000000000000..74130ac73676dac805cd9869a6fe1d8befa65e76 --- /dev/null +++ b/examples/bitvectors/power2/power2_Pow2int_Power_sum_1.v @@ -0,0 +1,34 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Require int.Int. + +Parameter pow2: Z -> Z. + +Axiom Power_0 : ((pow2 0%Z) = 1%Z). + +Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> + ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z). + +Axiom Power_1 : ((pow2 1%Z) = 2%Z). + +Open Scope Z_scope. +Require Import Why3. + +(* Why3 goal *) +Theorem Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> + ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z). +intros n m (Hn & Hm). +generalize Hm. +pattern m; apply Z_lt_induction; auto. +clear m Hm. +intros m Hind Hm. +assert (h:(m = 0 \/ m > 0)) by omega; destruct h. +why3 "alt-ergo". +replace m with ((m-1)+1) by omega. +rewrite Power_s; auto with zarith. +why3 "alt-ergo". +Qed. + + diff --git a/examples/bitvectors/power2/why3session.xml b/examples/bitvectors/power2/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..7df59bd0fd9ba55d2b753febfc7c0dd7470eb343 --- /dev/null +++ b/examples/bitvectors/power2/why3session.xml @@ -0,0 +1,3827 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +