Commit dc7b98b7 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix a few issues with the IEEE-754 formalization.

- to_real x = 0 does not imply is_zero x, unless x is finite.
- Add missing triggers.
- Move any property related to signed zeros from "_finite" to "_special".
- Fix incorrect signed zeros for addition, subtraction, and FMA.
- Remove inconsistent signs of NaN for negation, multiplication, and division.
- Add specification for special values of abs.
- Fix useless specification for sqrt(+oo).
parent a04e9bdc
(** {1 Formalization of Floating-Point Arithmetic}
Full float theory (with infinities and NaN) only RNE rounding mode.
Special values are not axiomatized.
Full float theory (with infinities and NaN).
A note on intended semantics: we use the same idea as the SMTLIB floating
point theory, that defers any inconsistencies to the "parent" document.
Hence, in doubt, the correct axiomatisation is one that implements
[BTRW14] "An Automatable Formal Semantics for IEEE-754 Floating-Point
Arithmetic", which in turn defers any inconsistencies to IEE-754.
Arithmetic", which in turn defers any inconsistencies to IEEE-754.
This theory is split into two parts: the first part talks about IEEE
operations and this is what you should use as a user, the second part is
......@@ -168,7 +167,7 @@ theory GenericFloat
axiom zeroF_to_real : to_real zeroF = 0.0
axiom half_to_real : to_real half = 0.5
axiom zero_to_real : forall x. is_zero x <-> to_real x = 0.0
axiom zero_to_real : forall x. is_zero x <-> is_finite x /\ to_real x = 0.0
(* {3 Conversions from other sorts} *)
......@@ -363,6 +362,9 @@ theory GenericFloat
(is_finite x /\ is_finite y /\ same_sign x y) ->
to_real x *. to_real y >=. 0.0
predicate product_sign (z x y: t) =
(same_sign x y -> is_positive z) /\ (diff_sign x y -> is_negative z)
(** overflow *)
(* This predicate tells what is the result of a rounding in case
......@@ -388,64 +390,56 @@ theory GenericFloat
(** {3 binary operations} *)
axiom add_finite: forall m:mode, x y:t [add m x y].
is_finite x -> is_finite y -> no_overflow m (to_real x +. to_real y) ->
is_finite x -> is_finite y -> no_overflow m (to_real x +. to_real y) ->
is_finite (add m x y) /\
to_real (add m x y) = round m (to_real x +. to_real y) /\
sign_zero_result m (add m x y)
to_real (add m x y) = round m (to_real x +. to_real y)
axiom sub_finite: forall m:mode, x y:t.
is_finite x -> is_finite y -> no_overflow m (to_real x -. to_real y) ->
axiom sub_finite: forall m:mode, x y:t [sub m x y].
is_finite x -> is_finite y -> no_overflow m (to_real x -. to_real y) ->
is_finite (sub m x y) /\
to_real (sub m x y) = round m (to_real x -. to_real y) /\
sign_zero_result m (sub m x y)
to_real (sub m x y) = round m (to_real x -. to_real y)
axiom mul_finite: forall m:mode, x y:t.
is_finite x -> is_finite y -> no_overflow m (to_real x *. to_real y) ->
axiom mul_finite: forall m:mode, x y:t [mul m x y].
is_finite x -> is_finite y -> no_overflow m (to_real x *. to_real y) ->
is_finite (mul m x y) /\
to_real (mul m x y) = round m (to_real x *. to_real y)
axiom div_finite: forall m:mode, x y:t.
is_finite x -> is_finite y -> no_overflow m (to_real x /. to_real y) /\ not is_zero y ->
axiom div_finite: forall m:mode, x y:t [div m x y].
is_finite x -> is_finite y ->
no_overflow m (to_real x /. to_real y) -> not is_zero y ->
is_finite (div m x y) /\
to_real (div m x y) = round m (to_real x /. to_real y)
axiom neg_finite: forall x:t.
is_finite x -> is_finite (neg x) /\
axiom neg_finite: forall x:t [neg x].
is_finite x ->
is_finite (neg x) /\
to_real (neg x) = -. to_real x
axiom abs: forall x:t.
is_finite x ->
axiom abs_finite: forall x:t [abs x].
is_finite x ->
is_finite (abs x) /\
to_real (abs x) = Abs.abs (to_real x) /\
is_positive (abs x)
predicate product_sign (z x y: t) =
(same_sign x y -> is_positive z) /\ (diff_sign x y -> is_negative z)
axiom fma_finite: forall m:mode, x y z:t [fma m x y z].
is_finite x -> is_finite y -> is_finite z ->
no_overflow m (to_real x *. to_real y +. to_real z) ->
is_finite (fma m x y z) /\
to_real (fma m x y z) = round m (to_real x *. to_real y +. to_real z)
axiom fma_finite: forall m:mode, x y z:t.
let r = fma m x y z in
(is_finite x /\ is_finite y /\ is_finite z /\
no_overflow m (to_real x *. to_real y +. to_real z)
-> is_finite r /\
to_real r = round m (to_real x *. to_real y +. to_real z) /\
(if product_sign z x y then same_sign r z
else sign_zero_result m r))
(* /!\ externazile square root ? more generally, externalyse any part
(* /!\ externalize square root? more generally, externalize any part
that needs another theory ? /!\ *)
use real.Square
axiom sqrt_finite: forall m:mode, x:t.
let r = sqrt m x in
is_finite x ->
(is_zero x -> is_finite r /\ is_zero r /\ same_sign r x)
/\ (x .> zeroF
-> is_finite r /\ to_real r = round m (Square.sqrt (to_real x)) /\ is_positive r)
axiom sqrt_finite: forall m:mode, x:t [sqrt m x].
is_finite x -> x .>= zeroF ->
is_finite (sqrt m x) /\
to_real (sqrt m x) = round m (Square.sqrt (to_real x))
predicate same_sign_real (x:t) (r:real) =
(is_positive x /\ r >. 0.0) \/ (is_negative x /\ r <. 0.0)
axiom add_special: forall m:mode, x y:t.
axiom add_special: forall m:mode, x y:t [add m x y].
let r = add m x y in
(is_nan x \/ is_nan y -> is_nan r)
/\
......@@ -460,6 +454,9 @@ theory GenericFloat
/\
(is_finite x /\ is_finite y /\ not no_overflow m (to_real x +. to_real y)
-> same_sign_real r (to_real x +. to_real y) /\ overflow_value m r)
/\
(is_finite x /\ is_finite y
-> if same_sign x y then same_sign r x else sign_zero_result m r)
(*
constant min_normalized_double : real = 0x1p-1022
......@@ -510,7 +507,7 @@ theory GenericFloat
(Abs.abs(to_real x) <=. min_normalized -.>
Abs.abs(to_real res -. (-. to_real x)) <=. eta_normalized)) *)
axiom sub_special: forall m:mode, x y:t.
axiom sub_special: forall m:mode, x y:t [sub m x y].
let r = sub m x y in
(is_nan x \/ is_nan y -> is_nan r)
/\
......@@ -526,8 +523,11 @@ theory GenericFloat
(is_finite x /\ is_finite y /\ not no_overflow m (to_real x -. to_real y)
-> same_sign_real r (to_real x -. to_real y)
/\ overflow_value m r)
/\
(is_finite x /\ is_finite y
-> if diff_sign x y then same_sign r x else sign_zero_result m r)
axiom mul_special: forall m:mode, x y:t.
axiom mul_special: forall m:mode, x y:t [mul m x y].
let r = mul m x y in
(is_nan x \/ is_nan y -> is_nan r)
/\ (is_zero x /\ is_infinite y -> is_nan r)
......@@ -539,9 +539,9 @@ theory GenericFloat
/\ (is_infinite x /\ is_infinite y -> is_infinite r)
/\ (is_finite x /\ is_finite y /\ not no_overflow m (to_real x *. to_real y)
-> overflow_value m r)
/\ product_sign r x y
/\ (not is_nan r -> product_sign r x y)
axiom div_special: forall m:mode, x y:t.
axiom div_special: forall m:mode, x y:t [div m x y].
let r = div m x y in
(is_nan x \/ is_nan y -> is_nan r)
/\ (is_finite x /\ is_infinite y -> is_zero r)
......@@ -553,15 +553,20 @@ theory GenericFloat
/\ (is_finite x /\ is_zero y /\ not (is_zero x)
-> is_infinite r)
/\ (is_zero x /\ is_zero y -> is_nan r)
/\ product_sign r x y
/\ (not is_nan r -> product_sign r x y)
axiom neg_special: forall x:t [neg x].
(is_nan x -> is_nan (neg x))
/\ (is_infinite x -> is_infinite (neg x))
/\ (not is_nan x -> diff_sign x (neg x))
axiom neg_special: forall x:t.
(is_nan x -> is_nan (.- x))
/\ (is_infinite x -> is_infinite (.- x))
/\ diff_sign x (.- x)
axiom abs_special: forall x:t [abs x].
(is_nan x -> is_nan (abs x))
/\ (is_infinite x -> is_infinite (abs x))
/\ (not is_nan x -> is_positive (abs x))
axiom fma_special: forall m:mode, x y z:t.
let r = fma m x y z in
axiom fma_special: forall m:mode, x y z:t [fma m x y z].
let r = fma m x y z in
(is_nan x \/ is_nan y \/ is_nan z -> is_nan r)
/\ (is_zero x /\ is_infinite y -> is_nan r)
/\ (is_infinite x /\ is_zero y -> is_nan r)
......@@ -586,13 +591,19 @@ theory GenericFloat
not no_overflow m (to_real x *. to_real y +. to_real z)
-> same_sign_real r (to_real x *. to_real y +. to_real z)
/\ overflow_value m r)
axiom sqrt_special: forall m:mode, x:t.
let r = sqrt m x in
(is_nan x -> is_nan r)
/\ (is_plus_infinity x -> is_plus_infinity x)
/\ (is_finite x /\ is_finite y /\ is_finite z
-> if product_sign z x y then same_sign r z
else (to_real x *. to_real y +. to_real z = 0.0 ->
if m = RTN then is_negative r else is_positive r))
axiom sqrt_special: forall m:mode, x:t [sqrt m x].
let r = sqrt m x in
(is_nan x -> is_nan r)
/\ (is_plus_infinity x -> is_plus_infinity r)
/\ (is_minus_infinity x -> is_nan r)
/\ (is_finite x /\ to_real x <. 0.0 -> is_nan r)
/\ (is_zero x -> same_sign r x)
/\ (is_finite x /\ to_real x >. 0.0 -> is_positive r)
(* magic axioms *)
......
Supports Markdown
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