Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 0d3d2818 authored by MARCHE Claude's avatar MARCHE Claude

more on bitvectors and floats

parent 5155cf7e
......@@ -108,6 +108,36 @@ theory BitVector
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
......@@ -135,6 +165,23 @@ 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
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. i > 0 -> nth (from_int n) i = nth (from_int (div n 2)) (i-1)
end
......@@ -147,6 +194,129 @@ theory BV32
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
......
......@@ -52,119 +52,333 @@
expanded="true">
<theory
name="BitVector"
verified="true"
verified="false"
expanded="true">
<goal
name="to_nat_sub_footprint"
sum="d1acdc2fec43b1e6dc349c7d2873f07f"
proved="false"
expanded="true"
shape="ainfix =ato_nat_subV0V2V3ato_nat_subV1V2V3Iainfix =anthV0V4anthV1V4Iainfix <=V4V2Aainfix <=V3V4FF">
</goal>
</theory>
<theory
name="BV32"
verified="true"
expanded="true">
</theory>
<theory
name="BV64"
verified="true"
expanded="true">
</theory>
<theory
name="BV32_64"
verified="true"
expanded="true">
</theory>
<theory
name="BV_double"
verified="true"
expanded="true">
</theory>
<theory
name="TestNegAsXOR"
verified="false"
expanded="true">
<goal
name="Nth_j"
sum="5a7c100ec1acf7a28679707c123ceca9"
proved="false"
expanded="true"
shape="ainfix =anthajV0aFalseIainfix <=V0c62Aainfix <=c0V0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.64"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="7.27"/>
</proof>
</goal>
<goal
name="Exp_of_xor_j"
sum="707beb36d4e78dc6e088f0d6d10ca37a"
proved="true"
expanded="true"
shape="ainfix =aexpabw_xorV0ajaexpV0F">
<proof
prover="coq"
timelimit="5"
edited="bitvector_TestNegAsXOR_Exp_of_xor_j_1.v"
obsolete="true"><undone/>
</proof>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="1.61"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.44"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="Mantissa_of_xor_j"
sum="9f7ea16d8a3cd5f4dcae82d98a99b811"
proved="true"
expanded="true"
shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.94"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="9.26"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="MainResultZero"
sum="1dc8b3012b86b43353c7e1e981b9bac1"
proved="true"
expanded="true"
shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="true">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="true">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="MainResult"
sum="16249ee2605bdc50bfebcaff0383ef0a"
proved="false"
expanded="true"
shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix <aexpV0c2047Aainfix <c0aexpV0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="7.46"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="7.07"/>
</proof>
</goal>
</theory>
<theory
name="TestDoubleOfInt"
verified="false"
expanded="true">
<goal
name="L"
sum="8f17294573ff352f750e637a1d8888ce"
proved="false"
expanded="true"
shape="ainfix =aconst_as_doubleainfix +apowerc2.0c52apowerc2.0c31">
</goal>
<goal
name="MainResult"
sum="d5173e798028bb27898e0bc65fcbc6b4"
proved="false"
expanded="true"
shape="ainfix =adouble_of_int32V0afrom_intV0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="true">
<result status="timeout" time="5.27"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="true">
<result status="timeout" time="7.09"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="true">
<result status="timeout" time="5.86"/>
</proof>
</goal>
</theory>
<theory
name="TestBv32"
verified="false"
expanded="true">
<goal
name="Test1"
sum="081a5423810d47ab1fe2b0a82b35eb24"
proved="true"
sum="22645df9721f1d46795d7e11ee07181b"
proved="false"
expanded="true"
shape="Labw_andabvzeroabvoneainfix =anthV0c1aFalse">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Test2"
sum="0dfd1f488bc3a073e572644d428b8479"
proved="true"
sum="1a4ce989c06016e9f2dd00824e3a38a2"
proved="false"
expanded="true"
shape="Lalsrabvonec16ainfix =anthV0c15aTrue">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Test3"
sum="3d3025e93d04d19b4a65c7e91de25997"
proved="true"
sum="2dc1b38b6768d2c8ff7b5bdb0cd73fa7"
proved="false"
expanded="true"
shape="Lalsrabvonec16ainfix =anthV0c16aFalse">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="Test4"
sum="8f1766048b98478855859610a82ced71"
proved="true"
sum="4407501478d849326394ed748bf6615f"
proved="false"
expanded="true"
shape="Laasrabvonec16ainfix =anthV0c15aTrue">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="Test5"
sum="7f73dfdaefe18506af991f371f3f457b"
proved="true"
sum="3922c1e60876d3a8f293789ba96507c1"
proved="false"
expanded="true"
shape="Laasrabvonec16ainfix =anthV0c16aTrue">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="Test6"
sum="b191056321013bfe380ec980009cccc9"
proved="true"
sum="fb7a45badc5c0c049caaf2c33637c8a0"
proved="false"
expanded="true"
shape="Laasralsrabvonec1c16ainfix =anthV0c16aFalse">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="to_nat_0x00000000"
sum="3ee0fe188bb040f08b4279f413f39835"
proved="true"
sum="2bb085421494250521fc1ecd09aa00f0"
proved="false"
expanded="true"
shape="ainfix =ato_natabvzeroc0">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="valid" time="0.39"/>
</proof>
</goal>
<goal
name="to_nat_0x0000000F"
sum="fb89baa5a9ff9705440a2ec8e5599398"
sum="e9beee88cc7ab7e4ec446f46c43932fb"
proved="false"
expanded="true"
shape="ainfix =ato_natalsrabvonec28c15">
......@@ -172,13 +386,13 @@
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="60.15"/>
</proof>
</goal>
<goal
name="to_nat_0x0000001F"
sum="6e0fb9b6b86dd2e94af40ec0a80b4a58"
sum="1cdf40b547d2c9bc4a43fbb380c359d8"
proved="false"
expanded="true"
shape="ainfix =ato_natalsrabvonec27c31">
......@@ -186,13 +400,13 @@
prover="z3"
timelimit="60"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="60.15"/>
</proof>
</goal>
<goal
name="to_nat_0x0000003F"
sum="122cf1440c33fffe9ddb16ae7e8819c9"
sum="e324bc7e0d9450ea2c91a2e36b40e53e"
proved="false"
expanded="true"
shape="ainfix =ato_natalsrabvonec26c63">
......@@ -200,13 +414,13 @@
prover="z3"
timelimit="60"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="60.05"/>
</proof>
</goal>
<goal
name="to_nat_0x0000007F"
sum="b509cc35c184038ba6cff7c07f17834d"
sum="10b435336730cc547e782c64af3dee4c"
proved="false"
expanded="true"
shape="ainfix =ato_natalsrabvonec25c127">
......@@ -214,13 +428,13 @@
prover="z3"
timelimit="60"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="60.09"/>
</proof>
</goal>
<goal
name="to_nat_0x000000FF"
sum="807b63c6feb2d47472dc142d58ab099d"
sum="d475eb1825e08ffcc8c7fb0780cf9dee"
proved="false"
expanded="true"
shape="ainfix =ato_natalsrabvonec24c255">
......@@ -228,13 +442,13 @@
prover="z3"
timelimit="10"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="60.09"/>
</proof>
</goal>
<goal
name="to_nat_0x000001FF"
sum="786fa4285e60143b7c2e29b9abb612a7"
sum="e6a340776b510cee56b28828722d36a5"
proved="false"
expanded="true"
shape="ainfix =ato_natalsrabvonec23c511">
......@@ -242,27 +456,27 @@
prover="z3"
timelimit="60"
edited=""
obsolete="false">
obsolete="true">
<result status="timeout" time="60.09"/>
</proof>
</goal>
<goal
name="to_nat_0x000003FF"
sum="18f97e041d6198984ab8fb7066f768c5"
proved="true"
sum="469de7c9de2367d1eb7496e0261c5368"
proved="false"
expanded="true"
shape="ainfix =ato_natalsrabvonec22c1023">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete=