Commit 49443780 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

using pow2 instead of power

parent 093df864
theory PowerValue
function pow_of2 (i:int) : int
axiom pow_of2_value:
pow_of2 0 = 1 /\
pow_of2 1 = 2 /\
pow_of2 2 = 4 /\
pow_of2 3 = 8 /\
pow_of2 4 = 16 /\
pow_of2 5 = 32 /\
pow_of2 6 = 64 /\
pow_of2 7 = 128 /\
pow_of2 8 = 256 /\
pow_of2 9 = 512 /\
pow_of2 10 = 1024 /\
pow_of2 11 = 2048 /\
pow_of2 12 = 4096 /\
pow_of2 13 = 8192 /\
pow_of2 14 = 16384 /\
pow_of2 15 = 32768 /\
pow_of2 16 = 65536 /\
pow_of2 17 = 131072 /\
pow_of2 18 = 262144 /\
pow_of2 19 = 524288 /\
pow_of2 20 = 1048576 /\
pow_of2 21 = 2097152 /\
pow_of2 22 = 4194304 /\
pow_of2 23 = 8388608 /\
pow_of2 24 = 16777216 /\
pow_of2 25 = 33554432 /\
pow_of2 26 = 67108864 /\
pow_of2 27 = 134217728 /\
pow_of2 28 = 268435456 /\
pow_of2 29 = 536870912 /\
pow_of2 30 = 1073741824 /\
pow_of2 31 = 2147483648 /\
pow_of2 32 = 4294967296 /\
pow_of2 33 = 8589934592 /\
pow_of2 34 = 17179869184 /\
pow_of2 35 = 34359738368 /\
pow_of2 36 = 68719476736 /\
pow_of2 37 = 137438953472 /\
pow_of2 38 = 274877906944 /\
pow_of2 39 = 549755813888 /\
pow_of2 40 = 1099511627776 /\
pow_of2 41 = 2199023255552 /\
pow_of2 42 = 4398046511104 /\
pow_of2 43 = 8796093022208 /\
pow_of2 44 = 17592186044416 /\
pow_of2 45 = 35184372088832 /\
pow_of2 46 = 70368744177664 /\
pow_of2 47 = 140737488355328 /\
pow_of2 48 = 281474976710656 /\
pow_of2 49 = 562949953421312 /\
pow_of2 50 = 1125899906842624 /\
pow_of2 51 = 2251799813685248 /\
pow_of2 52 = 4503599627370496 /\
pow_of2 53 = 9007199254740992 /\
pow_of2 54 = 18014398509481984 /\
pow_of2 55 = 36028797018963968 /\
pow_of2 56 = 72057594037927936 /\
pow_of2 57 = 144115188075855872 /\
pow_of2 58 = 288230376151711744 /\
pow_of2 59 = 576460752303423488 /\
pow_of2 60 = 1152921504606846976 /\
pow_of2 61 = 2305843009213693952 /\
pow_of2 62 = 4611686018427387904 /\
pow_of2 63 = 9223372036854775808
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_1 : pow2 1 = 2.0
lemma Power_neg1 : pow2 (-1) = 0.5
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
......@@ -74,7 +112,7 @@ theory BitVector
use export bool.Bool
use import int.Int
use import PowerValue
use import Pow2int
function size : int
type bv
......@@ -110,21 +148,22 @@ theory BitVector
forall v1 v2:bv, n:int. 0 <= n < size ->
nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
axiom Nth_bw_xor_v1true:
forall v1 v2:bv, n:int. 0 <= n < size /\ nth v1 n = True->
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)
axiom Nth_bw_xor_v1false:
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
axiom Nth_bw_xor_v2true:
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)
axiom Nth_bw_xor_v2false:
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 ->
......@@ -172,6 +211,8 @@ theory BitVector
(* 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] *)
......@@ -194,7 +235,7 @@ theory BitVector
to_nat_aux b i = 0
*)
(* generalization : (to_nat_sub b j i) returns the non-negative number represented
......@@ -232,7 +273,7 @@ theory BitVector
forall b:bv, j i:int.
0 <= i <= j ->
nth b j = True ->
to_nat_sub b j i = (pow_of2 (j-i)) + to_nat_sub b (j-1) i
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.
......@@ -245,6 +286,13 @@ theory BitVector
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. 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.
(forall k:int. j >= k >= i -> nth b k = False) ->
......@@ -253,7 +301,7 @@ theory BitVector
lemma to_nat_of_one:
forall b:bv, i j:int.
(forall k:int. j >= k >= i -> nth b k = True) ->
to_nat_sub b j i = pow_of2 (j-i+1) - 1
to_nat_sub b j i = pow2 (j-i+1) - 1
lemma to_nat_sub_footprint: forall b1 b2:bv, j i:int.
(forall k:int. i <= k <= j -> nth b1 k = nth b2 k) ->
......@@ -276,6 +324,8 @@ theory BitVector
(* 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] *)
......@@ -309,6 +359,8 @@ theory BitVector
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
......@@ -320,10 +372,10 @@ theory BitVector
*)
axiom nth_from_int_high_even:
forall n i:int. size > i >= 0 /\ mod (div n (pow_of2 i)) 2 = 0 -> nth (from_int n) i = False
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 (pow_of2 i)) 2 <> 0 -> nth (from_int n) i = True
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
......@@ -362,6 +414,7 @@ theory TestNatSub
function b:bv = from_int 7
lemma to_nat_sub_b: (to_nat_sub b 4 0) = 7
end
theory BV32_64
......@@ -386,7 +439,7 @@ theory BV_double
use import BV64
use import real.RealInfix
use import int.Int
use import real.Power
use import Pow2real
use import real.FromInt
function double_of_bv64 (b:bv) : real
......@@ -416,15 +469,15 @@ theory BV_double
*)
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 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_true:
axiom sign_value_false:
sign_value(False) = 1.0
axiom sign_value_false:
axiom sign_value_true:
sign_value(True) = -.1.0
axiom zero : forall b:bv.
......@@ -438,8 +491,8 @@ theory BV_double
axiom double_of_bv64_value:
forall b:bv. 0 < exp(b) < 2047 ->
double_of_bv64(b) = sign_value(sign(b)) *.
(pow 2.0 (from_int ((exp b) - 1023))) *.
(1.0 +. (from_int (mantissa b)) *. (pow 2.0 (-.52.0)))
(pow2 ((exp b) - 1023)) *.
(1.0 +. (from_int (mantissa b)) *. (pow2 (-52)))
(* TODO *)
......@@ -508,13 +561,13 @@ theory TestDoubleOfInt
use BV32
use BV64
use BV32_64
use import int.Int
use import bool.Bool
use import PowerValue
use import BV_double
use import real.RealInfix
use import real.FromInt
use import real.Power
use import int.Int
use Pow2int
use Pow2real
use import BV_double
function j : BV32.bv = BV32.from_int 0x43300000
......@@ -524,30 +577,34 @@ theory TestDoubleOfInt
lemma sign_const: sign(const) = False
lemma exp_const: exp(const) = 1075
lemma mantissa_const_nth:
forall i:int. 0 <=i <=30 -> BV64.nth const i = False
forall i:int. 0 <= i <= 30 -> BV64.nth const i = False
lemma mantissa_const_31th:
BV64.nth const 31 = True
lemma to_nat_mantissa_1: (BV64.to_nat_sub const 30 0) = 0
lemma mantissa_const_to_nat:
BV64.to_nat_sub const 31 0 = pow_of2 31
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) = pow_of2 31
function const_as_double : real = double_of_bv64 const
lemma mantissa_const: mantissa(const) = Pow2int.pow2 31
clone import int.Exponentiation with type t = real
lemma real1075m1023: from_int (1075 - 1023) = 52.0
lemma real1075m1023_2: 1075.0 -. 1023.0 = 52.0
function const_as_double : real = double_of_bv64 const
lemma const_value0: const_as_double =
pow 2.0 (1075.0 -. 1023.0) *. (1.0 +. 2147483648.0 *. pow 2.0 (-.52.0))
Pow2real.pow2 (1075 - 1023) *. (1.0 +. 2147483648.0 *. Pow2real.pow2 (-52))
lemma const_value: const_as_double = pow 2.0 52.0 +. pow 2.0 31.0
lemma const_value: const_as_double = Pow2real.pow2 52 +. Pow2real.pow2 31
function double_of_int32 (i:int) : real =
let var = BV32_64.concat j (BV32.bw_xor j' (BV32.from_int i)) in
......@@ -646,6 +703,7 @@ theory TestBv32
goal to_nat_0xFFFFFFFF:
to_nat bvone = 4294967295
(*
goal to_int_0x00000000:
to_int bvzero = 0
......@@ -664,6 +722,8 @@ theory TestBv32
goal to_int_smoke:
to_int (lsr bvone 16) = 65536
*)
end
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment