Skip to content

why3
why3
Commit 1b24d75d authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Floating-Point: multi-rounding model

parent 3fb5845a
Hide whitespace changes
Inline Side-by-side
Showing with 357 additions and 155 deletions
Makefile.in
View file @ 1b24d75d
......@@ -887,7 +887,7 @@ COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime
COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding Single Double
COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
......
drivers/gappa.drv
View file @ 1b24d75d
......@@ -167,6 +167,16 @@ theory real.FromInt
end
theory floating_point.Rounding
syntax function NearestTiesToEven "ne"
syntax function ToZero "zr"
syntax function Up "up"
syntax function Down "dn"
syntax function NearestTiesToAway "na"
end
theory floating_point.Single
syntax function round "float<ieee_32,%1>(%2)"
......@@ -181,15 +191,22 @@ theory floating_point.Double
end
theory floating_point.Rounding
(*
theory floating_point.SingleMultiRounding
syntax function NearestTiesToEven "ne"
syntax function ToZero "zr"
syntax function Up "up"
syntax function Down "dn"
syntax function NearestTiesToAway "na"
syntax function round "float<ieee_32,%1>(%2)"
meta "instantiate : auto" prop Bounded_value
end
*)
theory floating_point.DoubleMultiRounding
syntax function round "float<ieee_64,%1>(%2)"
meta "instantiate : auto" prop Bounded_value
end
(*
Local Variables:
......
examples/bts/12475/why3session.xml
View file @ 1b24d75d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="bts/12475/why3session.xml">
<prover
......@@ -34,7 +34,7 @@
name="toto"
locfile="bts/12475/../12475.why"
loclnum="6" loccnumb="7" loccnume="11"
sum="1528698e7ee515779e096133af624d2f"
sum="07763c823feaf262c263cca6378f25f1"
proved="true"
expanded="true"
shape="ainfix &lt;V0ainfix +aroundaUpV0c1.F">
......@@ -44,7 +44,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -52,7 +52,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -68,7 +68,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/floats/why3session.xml
View file @ 1b24d75d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="check-builtin/floats/why3session.xml">
<prover
......@@ -32,7 +32,7 @@
name="Round_single_01"
locfile="check-builtin/floats/../floats.why"
loclnum="11" loccnumb="7" loccnume="22"
sum="3242b4e9102c2fc37a9a7dd6cfd10efa"
sum="397906d94bbb0b5341288dfce84f89dc"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
......@@ -49,7 +49,7 @@
name="Round_double_01"
locfile="check-builtin/floats/../floats.why"
loclnum="14" loccnumb="7" loccnume="22"
sum="95147a77cfc066399edef8befff58feb"
sum="35b08355e175d22b4d9ab4c1c827526f"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
......@@ -66,7 +66,7 @@
name="Test00"
locfile="check-builtin/floats/../floats.why"
loclnum="17" loccnumb="8" loccnume="14"
sum="f04ce085ad30e1fb1b6594cd78d977bd"
sum="e45b8dc86a2bf34e6b3beb8b8a8a720e"
proved="true"
expanded="true"
shape="ainfix &lt;=aprefix -c3.0V0Iainfix &lt;=aabsV0c2.0F">
......@@ -76,7 +76,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -84,7 +84,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -92,7 +92,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -107,7 +107,7 @@
name="Test01"
locfile="check-builtin/floats/../floats.why"
loclnum="19" loccnumb="8" loccnume="14"
sum="512a97ac8833620d3c1fe4338f5109c6"
sum="ebff461c0eb487a4284b1d316905f8a2"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix &lt;=avalueV0c2.0Aainfix &lt;=aprefix -c2.0avalueV0F">
......@@ -117,14 +117,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test02"
locfile="check-builtin/floats/../floats.why"
loclnum="25" loccnumb="8" loccnume="14"
sum="303330d34dd6e52d73fcdcc7f34319f3"
sum="10d968c72c3f3e64f89fa7904576ed89"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -134,14 +134,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test03"
locfile="check-builtin/floats/../floats.why"
loclnum="32" loccnumb="8" loccnume="14"
sum="2d6c2d43256f71efff7bd2e63cb3541e"
sum="07cb638f137dc0341ef32cb3e91c11fc"
proved="true"
expanded="true"
shape="ainfix &lt;=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -151,7 +151,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
examples/my_cosine/my_cosine_CosineSingle_MethodError_1.v
View file @ 1b24d75d
......@@ -13,8 +13,9 @@ Require int.Int.
Require real.Square.
Require floating_point.Rounding.
Require floating_point.Single.
Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%R /\
(PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%R /\
(PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
Axiom Cos_plus_pi : forall (x:R),
((Rtrigo_def.cos (x + PI)%R) = (-(Rtrigo_def.cos x))%R).
......@@ -41,19 +42,18 @@ Axiom Sin_sum : forall (x:R) (y:R),
Parameter atan: R -> R.
Axiom Tan_atan : forall (x:R), ((Rtrigo.tan (atan x)) = x).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Parameter single : Type.
Require Import Interval_tactic.
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Theorem MethodError : forall (x:R), ((Rabs x) <= (1 / 32)%R)%R ->
((Rabs ((1%R - ((05 / 10)%R * (x * x)%R)%R)%R - (Rtrigo_def.cos x))%R) <= (1 / 16777216)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x H.
interval with (i_bisect_diff x).
Qed.
(* DO NOT EDIT BELOW *)
examples/my_cosine/why3session.xml
View file @ 1b24d75d
......@@ -28,7 +28,7 @@
name="MethodError"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="13" loccnumb="6" loccnume="17"
sum="2467a67484295345557f0076ed412561"
sum="5654505132d0df95fb8d98d86e9154f0"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix &lt;=aabsV0c0x1.p-5F">
......@@ -39,14 +39,14 @@
edited="my_cosine_CosineSingle_MethodError_1.v"
obsolete="false"
archived="false">
<result status="valid" time="3.77"/>
<result status="valid" time="3.68"/>
</proof>
</goal>
<goal
name="TotalErrorFullyExpanded"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="20" loccnumb="6" loccnume="29"
sum="16c317808f261ff9cc5b16296167cd8b"
sum="b272d2bbaa334f583a44d792f1e66da2"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix &lt;=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix &lt;=aabsavalueV0c0x1.p-5F">
......@@ -56,14 +56,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="TotalErrorExpanded"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="31" loccnumb="6" loccnume="24"
sum="fe418525d8a2ed9a3cc54a44066dff60"
sum="e8eb30517031d5f9aa29e249a13fcaaf"
proved="true"
expanded="true"
shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix &lt;=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix &lt;=aabsavalueV0c0x1.p-5F">
......@@ -73,14 +73,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.22"/>
<result status="valid" time="0.82"/>
</proof>
</goal>
<goal
name="TotalError"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="51" loccnumb="6" loccnume="16"
sum="967dbbbd6b72c88306fbf58d0d697b15"
sum="0457c10047c2e650ca89f0b4f6c924e4"
proved="true"
expanded="true"
shape="Lacos_singleV0ainfix &lt;=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix &lt;=aabsavalueV0c0x1.p-5F">
......@@ -90,7 +90,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="4.56"/>
<result status="valid" time="3.13"/>
</proof>
</goal>
</theory>
......
examples/programs/my_cosine/my_cosine_M_WP_parameter_my_cosine_1.v
View file @ 1b24d75d
......@@ -6,33 +6,35 @@ Require Import Rbasic_fun.
Require Import R_sqrt.
Require Import Rtrigo.
Require Import AltSeries. (* for def of pi *)
Require int.Int.
Require real.Real.
Require real.RealInfix.
Require real.Abs.
Require real.FromInt.
Require int.Int.
Require real.Square.
Require floating_point.Rounding.
Require floating_point.Single.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%R /\
(PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R < PI)%R /\
(PI < (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
Axiom Cos_plus_pi : forall (x:R),
((Rtrigo_def.cos (x + PI)%R) = (-(Rtrigo_def.cos x))%R).
......@@ -59,15 +61,12 @@ Axiom Sin_sum : forall (x:R) (y:R),
Parameter atan: R -> R.
Axiom Tan_atan : forall (x:R), ((Rtrigo.tan (atan x)) = x).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Require Import Interval_tactic.
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Theorem WP_parameter_my_cosine : forall (x:floating_point.Single.single),
((Rabs (floating_point.Single.value x)) <= (1 / 32)%R)%R ->
((Rabs ((1%R - (((floating_point.Single.value x) * (floating_point.Single.value x))%R * (05 / 10)%R)%R)%R - (Rtrigo_def.cos (floating_point.Single.value x)))%R) <= (1 / 16777216)%R)%R.
......@@ -75,6 +74,5 @@ Theorem WP_parameter_my_cosine : forall (x:floating_point.Single.single),
intros x H.
interval with (i_bisect_diff (Single.value x)).
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/my_cosine/why3session.xml
View file @ 1b24d75d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="examples/programs/my_cosine/why3session.xml">
<prover
......@@ -25,7 +25,7 @@
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="parameter my_cosine"
sum="8c5ef4e174040dfc2edbec12b7ad11c9"
sum="43a387020a8494975293041bea91d995"
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FAainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -40,7 +40,7 @@
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="assertion"
sum="f19d8615cb5c434b8497ae0d46cb1e88"
sum="1847af31ffb0fc79bb3f99eb48677194"
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -48,12 +48,12 @@
name="expl:parameter my_cosine"/>
<proof
prover="0"
timelimit="12"
memlimit="0"
timelimit="5"
memlimit="1000"
edited="my_cosine_M_WP_parameter_my_cosine_1.v"
obsolete="false"
archived="false">
<result status="valid" time="3.69"/>
<result status="valid" time="3.58"/>
</proof>
</goal>
<goal
......@@ -61,7 +61,7 @@
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
sum="13fda2c30862d2282aa50e9f3aed5e61"
sum="ed7fd59f8e3662b57ab5ff723e124166"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -81,7 +81,7 @@
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
sum="83faf9aa4fd66bb3090a0e3a03bfb095"
sum="01c28821422107c03234edd2f723d53e"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -101,7 +101,7 @@
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="precondition"
sum="c2a58280312e1542c64994f3bab49f6b"
sum="d30950e1e41f800ca0172d07dda83ad4"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......@@ -121,7 +121,7 @@
locfile="examples/programs/my_cosine/../my_cosine.mlw"
loclnum="30" loccnumb="4" loccnume="13"
expl="normal postcondition"
sum="fb20bbbd761cb5dae33e358483e311a4"
sum="2eafda4f7656e405bda4587b4c59ab3c"
proved="true"
expanded="true"
shape="ainfix &lt;=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
......
examples/tests-provers/gappa/why3session.xml
View file @ 1b24d75d
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="tests-provers/gappa/why3session.xml">
<prover
......@@ -20,7 +20,7 @@
name="Round_single_01"
locfile="tests-provers/gappa/../gappa.why"
loclnum="11" loccnumb="8" loccnume="23"
sum="3242b4e9102c2fc37a9a7dd6cfd10efa"
sum="397906d94bbb0b5341288dfce84f89dc"
proved="true"
expanded="false"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
......@@ -37,7 +37,7 @@
name="Round_double_01"
locfile="tests-provers/gappa/../gappa.why"
loclnum="14" loccnumb="8" loccnume="23"
sum="d39bb272fc8d9297bec1df1e1fb1106a"
sum="1e27690968c7f98982dcf973be229e14"
proved="true"
expanded="false"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
......@@ -54,7 +54,7 @@
name="Test00"
locfile="tests-provers/gappa/../gappa.why"
loclnum="17" loccnumb="9" loccnume="15"
sum="9ebac93d6a57654f3787929bdc703aaf"
sum="f9eacb01a4307782d62d79a7cf147491"
proved="true"
expanded="false"
shape="ainfix &lt;=aprefix -c3.0V0Iainfix &lt;=aabsV0c2.0F">
......@@ -64,14 +64,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test01"
locfile="tests-provers/gappa/../gappa.why"
loclnum="19" loccnumb="9" loccnume="15"
sum="bf409087a884fe327065f5dbc2eb0d4d"
sum="fb50504a077e11b75a2da8e2febba4b7"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix &lt;=avalueV0c2.0Aainfix &lt;=aprefix -c2.0avalueV0F">
......@@ -81,14 +81,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test02"
locfile="tests-provers/gappa/../gappa.why"
loclnum="25" loccnumb="9" loccnume="15"
sum="8feed07428304f0920d7f41124c883b3"
sum="14d6ea8815c6984e17fbf9f76ac012eb"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -98,14 +98,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test03"
locfile="tests-provers/gappa/../gappa.why"
loclnum="32" loccnumb="9" loccnume="15"
sum="0da33f7c98ccd09c0d1e66fd78e72212"
sum="49f4cde6219c2d0ed441a51b636026e1"
proved="true"
expanded="false"
shape="ainfix &lt;=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -115,7 +115,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......@@ -129,7 +129,7 @@
name="Test1"
locfile="tests-provers/gappa/../gappa.why"
loclnum="53" loccnumb="8" loccnume="13"
sum="33c71394fca93d3d410fb722fcb970b5"
sum="76814dc6e642481127875db73c1d2aba"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -avalueaac0.1c0x1.p-53Iainfix =aaarIainfix =avalueararoundaNearestTiesToEvenc0.1">
......@@ -146,7 +146,7 @@
name="Test2"
locfile="tests-provers/gappa/../gappa.why"
loclnum="58" loccnumb="8" loccnume="13"
sum="65602af0f639b8cea8843b1fc07542b7"
sum="a4abf368f1add9e3c8814776fd5d6011"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -avalueafc0c0.1c0x1.p-53Iainfix =afc0arIainfix =avalueararoundaNearestTiesToEvenc0.1">
......@@ -156,14 +156,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test3"
locfile="tests-provers/gappa/../gappa.why"
loclnum="63" loccnumb="8" loccnume="13"
sum="1764bc962492b20b5ca636eea0acb2b5"
sum="78fbf11d146c5e828a60bad7789bc85a"
proved="true"
expanded="false"
shape="ainfix &lt;=aabsainfix -avalueagc0c1c0.1c0x1.p-53Iainfix =agc0c1arIainfix =avalueararoundaNearestTiesToEvenc0.1">
......@@ -173,7 +173,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......@@ -187,7 +187,7 @@
name="G1"
locfile="tests-provers/gappa/../gappa.why"
loclnum="89" loccnumb="7" loccnume="9"
sum="f0532ec1f07ee528e1c4ad329cbd2426"
sum="5830193d59ffa5b88f451863e4d6161c"
proved="true"
expanded="true"
shape="ainfix &lt;=ainfix -avaluearesultainfix *avalueaq1avalueaq2c0x1.p-52">
......@@ -204,7 +204,7 @@
name="G2"
locfile="tests-provers/gappa/../gappa.why"
loclnum="91" loccnumb="7" loccnume="9"
sum="76fd08ebf94a56233e552dcc7ba63305"
sum="4ecf70457e24cf2f84fc2ba52e7b1184"
proved="true"
expanded="true"
shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
......@@ -221,7 +221,7 @@
name="G3"
locfile="tests-provers/gappa/../gappa.why"
loclnum="94" loccnumb="7" loccnume="9"
sum="147725714d029b09fa91b96558079798"
sum="4ffa5eddd14694f5c2cf635063c5b843"
proved="true"
expanded="true"
shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
......@@ -231,7 +231,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
lib/coq/floating_point/Double.v
View file @ 1b24d75d
......@@ -8,44 +8,43 @@ Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require floating_point.DoubleFormat.
Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition double : Type.
exact (t 53 1024).
Defined.
(* Why3 goal *)
Definition round: floating_point.Rounding.mode -> R -> R.
exact (round 53 1024).
Defined.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R -> double.
Definition round_logic: floating_point.Rounding.mode -> R ->
floating_point.DoubleFormat.double.
exact (round_logic 53 1024 (refl_equal true) (refl_equal true)).
Defined.
(* Why3 goal *)
Definition value: double -> R.
Definition value: floating_point.DoubleFormat.double -> R.
exact (value 53 1024).
Defined.
(* Why3 goal *)
Definition exact: double -> R.
Definition exact: floating_point.DoubleFormat.double -> R.
exact (exact 53 1024).
Defined.
(* Why3 goal *)
Definition model: double -> R.
Definition model: floating_point.DoubleFormat.double -> R.
exact (model 53 1024).
Defined.
(* Why3 assumption *)
Definition round_error(x:double): R := (Rabs ((value x) - (exact x))%R).
Definition round_error(x:floating_point.DoubleFormat.double): R :=
(Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error(x:double): R := (Rabs ((value x) - (model x))%R).
Definition total_error(x:floating_point.DoubleFormat.double): R :=
(Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow(m:floating_point.Rounding.mode) (x:R): Prop :=
......@@ -75,13 +74,13 @@ now apply Round_idempotent.
Qed.
(* Why3 goal *)
Lemma Round_value : forall (m:floating_point.Rounding.mode) (x:double),
((round m (value x)) = (value x)).
Lemma Round_value : forall (m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double), ((round m (value x)) = (value x)).
now apply Round_value.
Qed.
(* Why3 goal *)
Lemma Bounded_value : forall (x:double),
Lemma Bounded_value : forall (x:floating_point.DoubleFormat.double),
((Rabs (value x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
now apply Bounded_value.
Qed.
......@@ -119,35 +118,49 @@ now apply Round_up_neg.
Qed.
(* Why3 assumption *)
Definition add_post(m:floating_point.Rounding.mode) (x:double) (y:double)
(res:double): Prop := ((value res) = (round m
Definition of_real_post(m:floating_point.Rounding.mode) (x:R)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
x)) /\ (((exact res) = x) /\ ((model res) = x)).
(* Why3 assumption *)
Definition add_post(m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
((value x) + (value y))%R)) /\
(((exact res) = ((exact x) + (exact y))%R) /\
((model res) = ((model x) + (model y))%R)).
(* Why3 assumption *)
Definition sub_post(m:floating_point.Rounding.mode) (x:double) (y:double)
(res:double): Prop := ((value res) = (round m
Definition sub_post(m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
((value x) - (value y))%R)) /\
(((exact res) = ((exact x) - (exact y))%R) /\
((model res) = ((model x) - (model y))%R)).
(* Why3 assumption *)