Commit 4aa3615d authored by MARCHE Claude's avatar MARCHE Claude

trying to use the new floats theory for real

parent 079015c7
(* Approximated cosine *)
module M
use import real.RealInfix
use import real.Abs
use import real.Trigonometry
use import floating_point.Rounding
use import floating_point.Single
val single_of_real_exact (x: real) : single
ensures { value result = x }
val add (x y: single) : single
requires { "expl:floating-point overflow"
no_overflow NearestTiesToEven ((value x) +. (value y)) }
ensures { value result = round NearestTiesToEven ((value x) +. (value y))}
val sub (x y: single) : single
requires { "expl:floating-point overflow"
no_overflow NearestTiesToEven ((value x) -. (value y)) }
ensures { value result = round NearestTiesToEven ((value x) -. (value y))}
val mul (x y: single) : single
requires { "expl:floating-point overflow"
no_overflow NearestTiesToEven ((value x) *. (value y)) }
ensures { value result = round NearestTiesToEven ((value x) *. (value y))}
let my_cosine (x:single) : single
requires { abs (value x) <=. 0x1p-5 }
ensures { abs (value result -. cos (value x)) <=. 0x1p-23 }
= assert {
abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
};
sub (single_of_real_exact 1.0) (mul (mul x x) (single_of_real_exact 0.5))
end
module IEEEfloat
use import real.RealInfix
use import real.Abs
use import real.Trigonometry
use import ieee_float.Float32
val add (x y: t) : t
requires { "expl:floating-point overflow" t'isFinite (x .+ y) }
ensures { result = x .+ y }
val sub (x y: t) : t
requires { "expl:floating-point overflow" t'isFinite (x .- y)}
ensures { result = x .- y }
val mul (x y: t) : t
requires { "expl:floating-point overflow" t'isFinite (x .* y)}
ensures { result = x .* y }
let my_cosine (x:t) : t
requires { Float32.abs x .<= (0x1p-5:t) }
ensures { Abs.abs (t'real result -. cos (t'real x)) <=. 0x1p-23 }
= assert { Abs.abs (t'real x) <=. 0x1p-5 };
assert {
Abs.abs (1.0 -. (t'real x) *. (t'real x) *. 0.5 -. cos (t'real x)) <=. 0x1p-24
};
sub (1.0:t) (mul (mul x x) (0.5:t))
end
module Combined
use import real.RealInfix
use import real.Abs
use import real.Trigonometry
use import mach.float.Single
let my_cosine (x:t) : t
requires { abs x .<= (0x1p-5:t) }
ensures { Abs.abs (t'real result -. cos (t'real x)) <=. 0x1p-23 }
= assert { Abs.abs (t'real x) <=. 0x1p-5 };
assert {
Abs.abs (1.0 -. (t'real x) *. (t'real x) *. 0.5 -. cos (t'real x)) <=. 0x1p-24
};
sub (1.0:t) (mul (mul x x) (0.5:t))
end
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Reals.Rbasic_fun.
Require Reals.R_sqrt.
Require Reals.Rtrigo_def.
Require Reals.Rtrigo1.
Require Reals.Ratan.
Require BuiltIn.
Require real.Real.
Require real.RealInfix.
Require real.Abs.
Require real.FromInt.
Require int.Int.
Require real.Square.
Require real.Trigonometry.
Require floating_point.Rounding.
Require floating_point.SingleFormat.
Require floating_point.Single.
(* Why3 assumption *)
Definition unit := unit.
Require Import Interval.Interval_tactic.
(* Why3 goal *)
Theorem WP_parameter_my_cosine : forall (x:floating_point.SingleFormat.single),
((Reals.Rbasic_fun.Rabs (floating_point.Single.value x)) <= (1 / 32)%R)%R ->
((Reals.Rbasic_fun.Rabs ((1%R - (((floating_point.Single.value x) * (floating_point.Single.value x))%R * (05 / 10)%R)%R)%R - (Reals.Rtrigo_def.cos (floating_point.Single.value x)))%R) <= (1 / 16777216)%R)%R.
(* Why3 intros x h1. *)
(* YOU MAY EDIT THE PROOF BELOW *)
intros x H.
interval with (i_bisect_diff (Single.value x)).
Qed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="1" name="Gappa" version="1.2.0" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="12" steplimit="0" memlimit="4000"/>
<prover id="3" name="Coq" version="8.6" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="4" name="Z3" version="4.4.1" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="5" name="Alt-Ergo" version="1.30" alternative="alt" timelimit="2" steplimit="0" memlimit="4000"/>
<file name="../my_cosine.mlw" expanded="true">
<theory name="M" sum="e6984a9af2ab6c45ac0e8af4e992df4e" expanded="true">
<goal name="WP_parameter my_cosine" expl="VC for my_cosine">
<transf name="split_goal_wp">
<goal name="WP_parameter my_cosine.1" expl="1. assertion">
<proof prover="2" timelimit="5" memlimit="1000"><result status="valid" time="0.17"/></proof>
<proof prover="3" timelimit="5" memlimit="1000" edited="my_cosine_M_WP_parameter_my_cosine_1.v"><result status="valid" time="1.79"/></proof>
</goal>
<goal name="WP_parameter my_cosine.2" expl="2. floating-point overflow">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter my_cosine.3" expl="3. floating-point overflow">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter my_cosine.4" expl="4. floating-point overflow">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter my_cosine.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="IEEEfloat" sum="c893577268cab3bfe222359ad1fe8705" expanded="true">
<goal name="WP_parameter my_cosine" expl="VC for my_cosine" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.99" steps="1636"/></proof>
</goal>
<goal name="WP_parameter my_cosine.2" expl="2. assertion">
<proof prover="3" edited="my_cosine_IEEEfloat_WP_parameter_my_cosine_1.v"><result status="valid" time="1.87"/></proof>
</goal>
<goal name="WP_parameter my_cosine.3" expl="3. floating-point overflow">
<proof prover="0"><result status="valid" time="1.49" steps="2000"/></proof>
</goal>
<goal name="WP_parameter my_cosine.4" expl="4. floating-point overflow">
<proof prover="0"><result status="valid" time="0.24" steps="312"/></proof>
</goal>
<goal name="WP_parameter my_cosine.5" expl="5. floating-point overflow">
<proof prover="0"><result status="timeout" time="1.99"/></proof>
<proof prover="1" timelimit="12" obsolete="true"><result status="unknown" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.19"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
</goal>
<goal name="WP_parameter my_cosine.6" expl="6. postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="1.98"/></proof>
<proof prover="1"><result status="unknown" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.16"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Combined" sum="08dfc24481780ce0dd81f93fbcf0e3b2" expanded="true">
<goal name="WP_parameter my_cosine" expl="VC for my_cosine" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.51" steps="1636"/></proof>
</goal>
<goal name="WP_parameter my_cosine.2" expl="2. assertion">
<proof prover="3" edited="my_cosine_Combined_WP_parameter_my_cosine_1.v"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="WP_parameter my_cosine.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="1.63" steps="2019"/></proof>
</goal>
<goal name="WP_parameter my_cosine.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.16" steps="160"/></proof>
</goal>
<goal name="WP_parameter my_cosine.5" expl="5. precondition">
<proof prover="0"><result status="valid" time="0.26" steps="350"/></proof>
</goal>
<goal name="WP_parameter my_cosine.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.15" steps="236"/></proof>
</goal>
<goal name="WP_parameter my_cosine.7" expl="7. precondition" expanded="true">
<proof prover="0"><result status="timeout" time="1.98"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="2.00"/></proof>
</goal>
<goal name="WP_parameter my_cosine.8" expl="8. precondition" expanded="true">
<proof prover="0"><result status="timeout" time="3.99"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="2.00"/></proof>
</goal>
<goal name="WP_parameter my_cosine.9" expl="9. postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="unknown" time="0.02"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="2.00"/></proof>
<proof prover="5" obsolete="true"><result status="timeout" time="2.00"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
module ExpOld
end
module Exp
use import ieee_float.Float64
use import real.Abs
use import real.ExpLog
use import real.Real
val ( +. ) (x y : t) : t
requires {t'isFinite x}
requires {t'isFinite y}
requires {"expl:no_overflow" t'isFinite (x .+ y)}
ensures {result = x .+ y}
val ( *. ) (x y : t) : t
requires {t'isFinite x}
requires {t'isFinite y}
requires {"expl:no_overflow" t'isFinite (x .* y)}
ensures {result = x .* y}
let my_exp (x: t) : t
requires { t'isFinite x}
requires { .- (1.0:t) .<= x .<= (1.0:t)}
requires {abs (t'real x) <= 1.0}
ensures { abs (t'real result - exp (t'real x)) <= 0x1p-4} (* 1 * 2 ^ - 4 *)
=
assert {
let x = t'real x in
abs(0.9890365552 + 1.130258690*x +
0.5540440796*x*x - exp(x)) <= 0x0.FFFFp-4};
(0x1.FA62FFD643D6Ep-1:t) +. (0x1.2158A22D91DE9p0:t) *. x +.
(0x1.1BABAA64D94DBp-1:t) *. x *. x
end
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="1" name="MetiTarski" version="2.4" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="3" name="Gappa" version="1.2.0" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="4" name="Z3" version="4.4.1" timelimit="2" steplimit="0" memlimit="4000"/>
<file name="../my_exp.mlw" expanded="true">
<theory name="Exp" sum="ce3f4a2437a6c6dcbb2818f19d8fed1b" expanded="true">
<goal name="WP_parameter my_exp" expl="VC for my_exp" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter my_exp.1" expl="1. assertion" expanded="true">
<proof prover="0" edited="my_exp_Exp_WP_parameter_my_exp_1.v"><result status="valid" time="1.53"/></proof>
<proof prover="1"><result status="unknown" time="0.10"/></proof>
</goal>
<goal name="WP_parameter my_exp.2" expl="2. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.04" steps="84"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter my_exp.3" expl="3. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.04" steps="82"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter my_exp.4" expl="4. no_overflow" expanded="true">
<proof prover="2"><result status="valid" time="0.19" steps="270"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
</goal>
<goal name="WP_parameter my_exp.5" expl="5. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.05" steps="85"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter my_exp.6" expl="6. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.04" steps="85"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter my_exp.7" expl="7. no_overflow" expanded="true">
<proof prover="2"><result status="valid" time="0.61" steps="480"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
</goal>
<goal name="WP_parameter my_exp.8" expl="8. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.05" steps="88"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter my_exp.9" expl="9. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.06" steps="86"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter my_exp.10" expl="10. no_overflow" expanded="true">
<proof prover="2"><result status="valid" time="0.29" steps="359"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
</goal>
<goal name="WP_parameter my_exp.11" expl="11. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.04" steps="91"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter my_exp.12" expl="12. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.05" steps="89"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter my_exp.13" expl="13. no_overflow" expanded="true">
<proof prover="2"><result status="timeout" time="1.98"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
</goal>
<goal name="WP_parameter my_exp.14" expl="14. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.05" steps="92"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter my_exp.15" expl="15. precondition" expanded="true">
<proof prover="2"><result status="valid" time="0.05" steps="92"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter my_exp.16" expl="16. no_overflow" expanded="true">
<proof prover="2"><result status="timeout" time="1.97"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
</goal>
<goal name="WP_parameter my_exp.17" expl="17. postcondition" expanded="true">
<proof prover="2"><result status="timeout" time="1.99"/></proof>
<proof prover="3"><result status="unknown" time="0.06"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -16,8 +16,17 @@
point support will leave them uninterpreted.
*)
(** {2 Rounding Modes} *)
theory RoundingMode
type mode = RNE | RNA | RTP | RTN | RTZ
(** {h <ul>
<li>RNE : Round Nearest ties to Even
<li>RNA : Round Nearest ties to Away
<li>RTP : Round Towards Positive
<li>RTN : Round Towards Negative
<li>RTZ : Round Towards Zero
</ul} *)
predicate to_nearest (m:mode) = m = RNE \/ m = RNA
end
......@@ -32,31 +41,24 @@ theory GenericFloat
use import real.RealInfix
use export RoundingMode
(*********************************************************************)
(* {2 PART I - PUBLIC INTERFACE} *)
(*********************************************************************)
(** {2 Part I - Public Interface} *)
(* the number of bits in the exponent. *)
constant eb : int
(* the number of bits in the significand, including the hidden bit. *)
(** the number of bits in the exponent. *)
constant sb : int
(** the number of bits in the significand, including the hidden bit. *)
axiom eb_gt_1: 1 < eb
axiom sb_gt_1: 1 < sb
(* {3 Sorts} *)
(** {3 Sorts} *)
type t
(* RNE : Round Nearest Ties To Even
RNA : Round Nearest Ties To Away
RTP : Round Toward Positive
RTN : Round Toward Negative
RTZ : Round Toward Zero *)
(** {3 Constructors and Constants} *)
(* {3 Constructors and Constants} *)
constant zeroF : t (* +0.0 *)
constant zeroF : t (** +0.0 *)
(* exp_bias = 2^(sb - 1) - 1 *)
(* max_finite_exp = 2^sb - 2 - exp_bias = exp_bias *)
(* max_significand = (2^eb + 2^eb - 1) * 2^(1-eb) *)
......@@ -64,7 +66,7 @@ theory GenericFloat
(* [m;x] = ( 1 + m * 2^(1-eb) ) * 2^( x - exp_bias ) *)
(* max_value = [2^(eb-1); 2^sb - 2] *)
(* {3 Operators} *)
(** {3 Operators} *)
function abs t : t
function neg t : t (* fp.neg *)
......@@ -110,7 +112,7 @@ theory GenericFloat
predicate (.>) (x:t) (y:t) = gt x y
predicate (.=) (x:t) (y:t) = eq x y
(* {3 Classification of numbers} *)
(** {3 Classification of numbers} *)
predicate is_normal t
predicate is_subnormal t
......@@ -120,7 +122,7 @@ theory GenericFloat
predicate is_positive t
predicate is_negative t
(* helper predicate for zeros, normals and subnormals. not defined
(** helper predicate for zeros, normals and subnormals. not defined
so that the axiomatisation below can use it without talking about
subnormals *)
predicate is_finite t
......@@ -136,7 +138,7 @@ theory GenericFloat
axiom is_not_finite: forall x:t.
not (is_finite x) <-> (is_infinite x \/ is_nan x)
(* {3 Conversions from other sorts} *)
(** {3 Conversions from other sorts} *)
(* from bitvec binary interchange *)
(* partly done with from_binary (for literals only) *)
......@@ -146,25 +148,23 @@ theory GenericFloat
(* from unsigned integer bitvector - see Float_BV_Converter *)
(* from signed integer bitvector *)
(* {3 Conversions to other sorts} *)
(** {3 Conversions to other sorts} *)
(* to unsigned integer bitvector - see Float_BV_Converter *)
(* to signed integer bitvector *)
(* to real *)
function to_real t : real
(*********************************************************************)
(* {2 PART II - PRIVATE AXIOMATISATION} *)
(*********************************************************************)
(** {2 Part II - Private Axiomatisation} *)
(* {3 Constructors and Constants} *)
(** {3 Constructors and Constants} *)
axiom zeroF_is_positive : is_positive zeroF
axiom zeroF_is_zero : is_zero zeroF
axiom zero_to_real : forall x [is_zero x].
is_zero x <-> is_finite x /\ to_real x = 0.0
(* {3 Conversions from other sorts} *)
(** {3 Conversions from other sorts} *)
(* with mathematical int *)
(* note that these conversions do not feature in SMTLIB *)
......@@ -177,7 +177,7 @@ theory GenericFloat
(* also note that this function never yields a subnormal, or a NaN, or -0 *)
function of_int (m:mode) (x:int) : t
(* {3 Conversions to other sorts} *)
(** {3 Conversions to other sorts} *)
(* Intended semantics for to_int are the same as (_ fp.to_sbv) with a *)
(* suitably sized bitvector. Safe minimum sizes are given below: *)
......@@ -193,7 +193,7 @@ theory GenericFloat
axiom zero_of_int : forall m. zeroF = of_int m 0
(* {3 Arithmetic} *)
(** {3 Arithmetic} *)
(* The intended meaning for round is the rounding for floating point as *)
(* described on p17 of IEEE-754. For results where the corresponding *)
......@@ -355,7 +355,7 @@ theory GenericFloat
predicate product_sign (z x y: t) =
(same_sign x y -> is_positive z) /\ (diff_sign x y -> is_negative z)
(** overflow *)
(** {3 Overflow} *)
(* This predicate is used to tell what is the result of a rounding
in case of overflow in the axioms specifying add/sub/mul and fma
......@@ -774,6 +774,8 @@ theory GenericFloat
is_finite (roundToIntegral m x)
end
(** {2 Conversions to/from bitvectors} *)
theory Float_BV_Converter
use bv.BV8
use bv.BV16
......@@ -828,6 +830,8 @@ theory Float_BV_Converter
to_real (of_ubv64 m x) = round m (FromInt.from_int (BV64.t'int x))
end
(** {2 Standard simple precision floats (32 bits)} *)
theory Float32
use int.Int
use import real.Real
......@@ -861,6 +865,8 @@ theory Float32
x - 0x1p-23 * Abs.abs(x) - 0x1p-149 <= round m x <= x + 0x1p-23 * Abs.abs(x) + 0x1p-149
end
(** {2 Standard double precision floats (64 bits)} *)
theory Float64
use int.Int
use import real.Real
......@@ -894,6 +900,8 @@ theory Float64
x - 0x1p-52 * Abs.abs(x) - 0x1p-1074 <= round m x <= x + 0x1p-52 * Abs.abs(x) + 0x1p-1074
end
(** {2 Conversions between float formats} *)
theory FloatConverter
use Float64
......
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