floating_point.why 5.1 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2


MARCHE Claude's avatar
MARCHE Claude committed
3
(* definition of IEEE-754 rounding modes *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5
theory Rounding

MARCHE Claude's avatar
MARCHE Claude committed
6
  type mode = NearestTiesToEven | ToZero | Up | Down | NearTiesToAway
MARCHE Claude's avatar
MARCHE Claude committed
7 8 9 10
    (** nearest ties to even, to zero, upward, downward, nearest ties to away *)

end

MARCHE Claude's avatar
MARCHE Claude committed
11 12 13

(* handling of IEEE-754 special values +\infty, -\infty, NaN, +0, -0 *)
theory SpecialValues
Andrei Paskevich's avatar
Andrei Paskevich committed
14 15

  type class = Finite | Infinite | NaN
MARCHE Claude's avatar
MARCHE Claude committed
16 17 18 19 20

  type sign = Neg | Pos

  use import real.Real

21
  inductive same_sign_real sign real =
22 23
    | Neg_case: forall x:real. x < 0.0 -> same_sign_real Neg x
    | Pos_case: forall x:real. x > 0.0 -> same_sign_real Pos x
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26

end

MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30 31
theory GenFloat

  use import Rounding
  use import real.Real
  use import real.Abs
32 33
  use import real.FromInt
  use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
34 35 36

  type t

Andrei Paskevich's avatar
Andrei Paskevich committed
37 38
  function round mode real : real
  function round_logic mode real : t
MARCHE Claude's avatar
MARCHE Claude committed
39

Andrei Paskevich's avatar
Andrei Paskevich committed
40 41 42
  function value t : real
  function exact t : real
  function model t : real
MARCHE Claude's avatar
MARCHE Claude committed
43

Andrei Paskevich's avatar
Andrei Paskevich committed
44 45
  function round_error (x : t) : real = abs (value x - exact x)
  function total_error (x : t) : real = abs (value x - model x)
MARCHE Claude's avatar
MARCHE Claude committed
46

Andrei Paskevich's avatar
Andrei Paskevich committed
47
  function max : real
MARCHE Claude's avatar
MARCHE Claude committed
48

Andrei Paskevich's avatar
Andrei Paskevich committed
49
  predicate no_overflow (m:mode) (x:real) = abs (round m x) <= max
MARCHE Claude's avatar
MARCHE Claude committed
50 51

  axiom Bounded_real_no_overflow :
52
    forall m:mode, x:real. abs x <= max -> no_overflow m x
MARCHE Claude's avatar
MARCHE Claude committed
53 54

  axiom Round_monotonic :
55
    forall m:mode, x y:real. x <= y -> round m x <= round m y
MARCHE Claude's avatar
MARCHE Claude committed
56

57 58 59 60 61 62 63 64 65
  axiom Round_idempotent :
    forall m1 m2:mode, x:real. round m1 (round m2 x) = round m2 x

  axiom Round_value :
    forall m:mode, x:t. round m (value x) = value x

  axiom Bounded_value :
    forall x:t. abs (value x) <= max

Andrei Paskevich's avatar
Andrei Paskevich committed
66
  function max_representable_integer : int
MARCHE Claude's avatar
MARCHE Claude committed
67 68 69

  axiom Exact_rounding_for_integers:
    forall m:mode,i:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
70
      Int.(<=) (Int.(-_) max_representable_integer) i /\
71 72
      Int.(<=) i max_representable_integer ->
        round m (from_int i) = from_int i
MARCHE Claude's avatar
MARCHE Claude committed
73 74

  (* rounding up and down *)
Andrei Paskevich's avatar
Andrei Paskevich committed
75
  axiom Round_down_le:
76
    forall x:real. round Down x <= x
Andrei Paskevich's avatar
Andrei Paskevich committed
77
  axiom Round_up_ge:
78
    forall x:real. round Up x >= x
Andrei Paskevich's avatar
Andrei Paskevich committed
79
  axiom Round_down_neg:
80 81 82
    forall x:real. round Down (-x) = - round Up x
  axiom Round_up_neg:
    forall x:real. round Up (-x) = - round Down x
MARCHE Claude's avatar
MARCHE Claude committed
83

MARCHE Claude's avatar
MARCHE Claude committed
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
end

theory Single

  type single

  function max_single : real = 0x1.FFFFFEp127
  function max_int : int = 16777216 (* 2^24 *)

  clone export GenFloat with
    type t = single,
    function max = max_single,
    function max_representable_integer = max_int

end



theory Double

  type double

  function max_double : real = 0x1.FFFFFFFFFFFFFp1023
  function max_int : int = 9007199254740992 (* 2^23 *)

  clone export GenFloat with
    type t = double,
    function max = max_double,
    function max_representable_integer = max_int

end



theory GenFloatFull

MARCHE Claude's avatar
MARCHE Claude committed
120
  use import SpecialValues
MARCHE Claude's avatar
MARCHE Claude committed
121 122 123 124
  use import Rounding
  use import real.Real

  clone export GenFloat
MARCHE Claude's avatar
MARCHE Claude committed
125 126

  (* special values *)
Andrei Paskevich's avatar
Andrei Paskevich committed
127
  function class t : class
MARCHE Claude's avatar
MARCHE Claude committed
128

MARCHE Claude's avatar
MARCHE Claude committed
129 130 131 132
  predicate is_finite (x:t) = class x = Finite
  predicate is_infinite (x:t) = class x = Infinite
  predicate is_NaN (x:t) = class x = NaN
  predicate is_not_NaN (x:t) = is_finite x \/ is_infinite x
133 134 135 136 137 138 139

  lemma is_not_NaN: forall x:t. is_not_NaN x <-> not (is_NaN x)

  function sign t  : sign

  predicate same_sign (x:t) (y:t)  = sign x = sign y

MARCHE Claude's avatar
MARCHE Claude committed
140 141 142 143 144 145
  predicate is_minus_infinity (x:t) = is_infinite x /\ sign x = Neg
  predicate is_plus_infinity (x:t) = is_infinite x /\ sign x = Pos
  predicate is_gen_zero (x:t) = is_finite x /\ value x = 0.0
  predicate is_gen_zero_plus (x:t) = is_gen_zero x /\ sign x = Pos
  predicate is_gen_zero_minus (x:t) = is_gen_zero x /\ sign x = Neg

MARCHE Claude's avatar
MARCHE Claude committed
146
  predicate le_full (x:t) (y:t) =
147 148 149 150
    (is_finite x /\ is_finite y /\ value x <= value y)
    \/ (is_minus_infinity x /\ is_not_NaN y)
    \/ (is_not_NaN x /\ is_plus_infinity y)

MARCHE Claude's avatar
MARCHE Claude committed
151
  predicate lt_full (x:t) (y:t) =
152 153 154 155
    (is_finite x /\ is_finite y /\ value x < value y)
    \/ (is_minus_infinity x /\ is_not_NaN y /\ not (is_minus_infinity y))
    \/ (is_not_NaN x /\ not (is_plus_infinity x) /\ is_plus_infinity y)

MARCHE Claude's avatar
MARCHE Claude committed
156
  predicate ge_full (x:t) (y:t) = le_full y x
157

MARCHE Claude's avatar
MARCHE Claude committed
158
  predicate gt_full (x:t) (y:t) = lt_full y x
159

MARCHE Claude's avatar
MARCHE Claude committed
160
  predicate eq_full (x:t) (y:t) =
161 162 163 164
    is_not_NaN x /\ is_not_NaN y /\
      ((is_finite x /\ is_finite y /\ value x = value y) \/
       (is_infinite x /\ is_infinite y /\ same_sign x y))

MARCHE Claude's avatar
MARCHE Claude committed
165
  predicate ne_full (x:t) (y:t) = not (eq_full x y)
166

MARCHE Claude's avatar
MARCHE Claude committed
167 168
  lemma le_lt_full_trans:
    forall x y z:t. le_full x y /\ lt_full y z -> lt_full x z
169

MARCHE Claude's avatar
MARCHE Claude committed
170 171
  lemma lt_le_full_trans:
    forall x y z:t. lt_full x y /\ le_full y z -> lt_full x z
172

MARCHE Claude's avatar
MARCHE Claude committed
173 174
  lemma le_ge_full_asym:
    forall x y:t. le_full x y /\ ge_full x y -> eq_full x y
175

MARCHE Claude's avatar
MARCHE Claude committed
176 177
  lemma not_lt_ge_full: forall x y:t.
    not (lt_full x y) /\ is_not_NaN x /\ is_not_NaN y -> ge_full x y
178

MARCHE Claude's avatar
MARCHE Claude committed
179 180
  lemma not_gt_le_full: forall x y:t.
    not (gt_full x y) /\ is_not_NaN x /\ is_not_NaN y -> le_full x y
MARCHE Claude's avatar
MARCHE Claude committed
181

MARCHE Claude's avatar
MARCHE Claude committed
182 183
end

MARCHE Claude's avatar
MARCHE Claude committed
184

MARCHE Claude's avatar
MARCHE Claude committed
185 186 187


theory SingleFull
MARCHE Claude's avatar
MARCHE Claude committed
188 189 190

  type single

Andrei Paskevich's avatar
Andrei Paskevich committed
191 192
  function max_single : real = 0x1.FFFFFEp127
  function max_int : int = 16777216 (* 2^24 *)
MARCHE Claude's avatar
MARCHE Claude committed
193

MARCHE Claude's avatar
MARCHE Claude committed
194
  clone export GenFloatFull with
Andrei Paskevich's avatar
Andrei Paskevich committed
195 196 197
    type t = single,
    function max = max_single,
    function max_representable_integer = max_int
MARCHE Claude's avatar
MARCHE Claude committed
198 199 200

end

MARCHE Claude's avatar
MARCHE Claude committed
201 202


MARCHE Claude's avatar
MARCHE Claude committed
203
theory DoubleFull
MARCHE Claude's avatar
MARCHE Claude committed
204 205 206

  type double

Andrei Paskevich's avatar
Andrei Paskevich committed
207 208
  function max_double : real = 0x1.FFFFFFFFFFFFFp1023
  function max_int : int = 9007199254740992 (* 2^23 *)
MARCHE Claude's avatar
MARCHE Claude committed
209

MARCHE Claude's avatar
MARCHE Claude committed
210
  clone export GenFloatFull with
Andrei Paskevich's avatar
Andrei Paskevich committed
211 212 213
    type t = double,
    function max = max_double,
    function max_representable_integer = max_int
MARCHE Claude's avatar
MARCHE Claude committed
214 215

end