Commit 505b068e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove outdated sessions and proofs.

parent 2c4b20fc
theory BitVector
use export bool.Bool
use import int.Int
function size : int
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)
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
(* 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
function to_nat (b:bv) : int = to_nat_aux b 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
lemma to_nat_sub_footprint: forall b1 b2:bv, j i:int.
(forall k:int. i <= k <= j -> nth b1 k = nth b2 k) ->
to_nat_sub b1 j i = to_nat_sub b2 j i
(* 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
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_low_even:
forall n:int. mod n 2 = 0 -> nth (from_int n) 0 = False
axiom nth_from_int_low_odd:
forall n:int. mod n 2 <> 0 -> nth (from_int n) 0 = True
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)
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 BV_double
use import BV64
use import real.Real
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
axiom zero : forall b:bv.
exp(b) = 0 /\ mantissa(b) = 0 -> double_of_bv64(b) = 0.0
(* TODO *)
end
theory TestNegAsXOR
use import BV64
use import BV_double
use import int.Int
use import real.RealInfix
function j : bv = from_int 0x8000000000000000
lemma Nth_j: forall i:int. 0 <= i <= 62 -> nth j i = False
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 MainResult : forall x:bv. 0 < exp(x) < 2047 ->
double_of_bv64 (bw_xor x j) = -. double_of_bv64 x
end
theory TestDoubleOfInt
use BV32
use BV64
use BV32_64
use import BV_double
use import real.Real
use import real.FromInt
function j : BV32.bv = BV32.from_int 0x43300000
function j' : BV32.bv = BV32.from_int 0x80000000
function const : BV64.bv = BV32_64.concat j j'
function const_as_double : real = double_of_bv64 const
clone import int.Exponentiation with type t = real
lemma L: const_as_double = power 2.0 52 + power 2.0 31
function double_of_int32 (i:int) : real =
let var = BV32_64.concat j (BV32.bw_xor j' (BV32.from_int i)) in
let v = double_of_bv64 var in
v - const_as_double
lemma MainResult: forall i:int. double_of_int32 i = from_int i
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 bitvector.why"
End:
*)
This diff is collapsed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
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).
Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
Axiom pow2_0 : ((pow2 0%Z) = 1%Z).
Axiom pow2_1 : ((pow2 1%Z) = 2%Z).
Axiom pow2_2 : ((pow2 2%Z) = 4%Z).
Axiom pow2_3 : ((pow2 3%Z) = 8%Z).
Axiom pow2_4 : ((pow2 4%Z) = 16%Z).
Axiom pow2_5 : ((pow2 5%Z) = 32%Z).
Axiom pow2_6 : ((pow2 6%Z) = 64%Z).
Axiom pow2_7 : ((pow2 7%Z) = 128%Z).
Axiom pow2_8 : ((pow2 8%Z) = 256%Z).
Axiom pow2_9 : ((pow2 9%Z) = 512%Z).
Axiom pow2_10 : ((pow2 10%Z) = 1024%Z).
Axiom pow2_11 : ((pow2 11%Z) = 2048%Z).
Axiom pow2_12 : ((pow2 12%Z) = 4096%Z).
Axiom pow2_13 : ((pow2 13%Z) = 8192%Z).
Axiom pow2_14 : ((pow2 14%Z) = 16384%Z).
Axiom pow2_15 : ((pow2 15%Z) = 32768%Z).
Axiom pow2_16 : ((pow2 16%Z) = 65536%Z).
Axiom pow2_17 : ((pow2 17%Z) = 131072%Z).
Axiom pow2_18 : ((pow2 18%Z) = 262144%Z).
Axiom pow2_19 : ((pow2 19%Z) = 524288%Z).
Axiom pow2_20 : ((pow2 20%Z) = 1048576%Z).
Axiom pow2_21 : ((pow2 21%Z) = 2097152%Z).
Axiom pow2_22 : ((pow2 22%Z) = 4194304%Z).
Axiom pow2_23 : ((pow2 23%Z) = 8388608%Z).
Axiom pow2_24 : ((pow2 24%Z) = 16777216%Z).
Axiom pow2_25 : ((pow2 25%Z) = 33554432%Z).
Axiom pow2_26 : ((pow2 26%Z) = 67108864%Z).
Axiom pow2_27 : ((pow2 27%Z) = 134217728%Z).
Axiom pow2_28 : ((pow2 28%Z) = 268435456%Z).
Axiom pow2_29 : ((pow2 29%Z) = 536870912%Z).
Axiom pow2_30 : ((pow2 30%Z) = 1073741824%Z).
Axiom pow2_31 : ((pow2 31%Z) = 2147483648%Z).
Axiom pow2_32 : ((pow2 32%Z) = 4294967296%Z).
Axiom pow2_33 : ((pow2 33%Z) = 8589934592%Z).
Axiom pow2_34 : ((pow2 34%Z) = 17179869184%Z).
Axiom pow2_35 : ((pow2 35%Z) = 34359738368%Z).
Axiom pow2_36 : ((pow2 36%Z) = 68719476736%Z).
Axiom pow2_37 : ((pow2 37%Z) = 137438953472%Z).
Axiom pow2_38 : ((pow2 38%Z) = 274877906944%Z).
Axiom pow2_39 : ((pow2 39%Z) = 549755813888%Z).
Axiom pow2_40 : ((pow2 40%Z) = 1099511627776%Z).
Axiom pow2_41 : ((pow2 41%Z) = 2199023255552%Z).
Axiom pow2_42 : ((pow2 42%Z) = 4398046511104%Z).
Axiom pow2_43 : ((pow2 43%Z) = 8796093022208%Z).
Axiom pow2_44 : ((pow2 44%Z) = 17592186044416%Z).
Axiom pow2_45 : ((pow2 45%Z) = 35184372088832%Z).
Axiom pow2_46 : ((pow2 46%Z) = 70368744177664%Z).
Axiom pow2_47 : ((pow2 47%Z) = 140737488355328%Z).
Axiom pow2_48 : ((pow2 48%Z) = 281474976710656%Z).
Axiom pow2_49 : ((pow2 49%Z) = 562949953421312%Z).
Axiom pow2_50 : ((pow2 50%Z) = 1125899906842624%Z).
Axiom pow2_51 : ((pow2 51%Z) = 2251799813685248%Z).
Axiom pow2_52 : ((pow2 52%Z) = 4503599627370496%Z).
Axiom pow2_53 : ((pow2 53%Z) = 9007199254740992%Z).
Axiom pow2_54 : ((pow2 54%Z) = 18014398509481984%Z).
Axiom pow2_55 : ((pow2 55%Z) = 36028797018963968%Z).
Axiom pow2_56 : ((pow2 56%Z) = 72057594037927936%Z).
Axiom pow2_57 : ((pow2 57%Z) = 144115188075855872%Z).
Axiom pow2_58 : ((pow2 58%Z) = 288230376151711744%Z).
Axiom pow2_59 : ((pow2 59%Z) = 576460752303423488%Z).
Axiom pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z).
Axiom pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z).
Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Parameter size: Z.
Parameter bv : Type.
Axiom size_positive : (0%Z < size)%Z.
Parameter nth: bv -> Z -> bool.
Parameter bvzero: bv.
Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth bvzero n) = false).
Parameter bvone: bv.
Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
n) = true).
Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
Parameter bw_and: bv -> bv -> bv.
Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).
Parameter bw_or: bv -> bv -> bv.
Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).
Parameter bw_xor: bv -> bv -> bv.
Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).
Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2)
n) = (negb (nth v2 n))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Open Scope Z_scope.
(* DO NOT EDIT BELOW *)
Theorem Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\
(n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2)