MachineTypeScript.sml 5.24 KB
Newer Older
1
(**
2
  f machine-precision as a datatype for mixed-precision computations
3 4 5 6

  @author: Raphael Monat
  @maintainer: Heiko Becker
 **)
7 8 9 10 11
open preamble miscTheory
open realTheory realLib sptreeTheory

val _ = new_theory "MachineType";

12 13
val _ = temp_overload_on("abs",``real$abs``);

14
val _ = Datatype `
Heiko Becker's avatar
Heiko Becker committed
15
  mType = M0 | M16 |  M32 | M64(* | M128 | M256 *)`;
16

17 18
val mTypeToQ_def = Define `
  mTypeToQ (m:mType) : real =
='s avatar
= committed
19
    case m of
20
      | M0 => 0
Heiko Becker's avatar
Heiko Becker committed
21
      | M16 => 1 / (2 pow 11)
22 23
      | M32 => 1 / (2 pow 24)
      | M64 => 1 / (2 pow 53)
='s avatar
= committed
24 25
      (* the epsilons below match what is used internally in daisy,
         although these value do not match the IEEE standard *)
Heiko Becker's avatar
Heiko Becker committed
26 27
      (* | M128 => 1 / (2 pow 105) *)
      (* | M256 => 1 / (2 pow 211) *)`;
28

29
val meps_def = Define `meps = mTypeToQ`;
30

31 32 33
val mTypeToQ_pos = store_thm("mTypeToQ_pos",
  ``!e. 0 <= mTypeToQ e``,
  Cases_on `e` \\ EVAL_TAC);
34

35 36 37 38 39 40
(**
  Check if machine precision m1 is more precise than machine precision m2.
  M0 is real-valued evaluation, hence the most precise.
  All others are compared by
    mTypeToQ m1 <= mTypeToQ m2
 **)
41
val isMorePrecise_def = Define `
42
  isMorePrecise (m1:mType) (m2:mType) = (mTypeToQ (m1) <= mTypeToQ (m2))`;
43

Heiko Becker's avatar
Heiko Becker committed
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
val morePrecise_def = Define `
  (morePrecise M0 _ = T) /\
  (morePrecise M16 M16 = T) /\
  (morePrecise M32 M32 = T) /\
  (morePrecise M32 M16 = T) /\
  (morePrecise M64 M0 = F) /\
  (morePrecise M64 _ = T) /\
  (morePrecise _ _ = F) `;

val morePrecise_antisym = store_thm (
  "morePrecise_antisym",
  ``!m1 m2.
      morePrecise m1 m2 /\
      morePrecise m2 m1 ==>
      m1 = m2``,
 rpt strip_tac \\ Cases_on `m1` \\ Cases_on `m2` \\ fs[morePrecise_def]);

val morePrecise_trans = store_thm (
  "morePrecise_trans",
  ``!m1 m2 m3.
      morePrecise m1 m2 /\
      morePrecise m2 m3 ==>
      morePrecise m1 m3``,
  rpt strip_tac
  \\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
  \\ fs[morePrecise_def]);

val isMorePrecise_morePrecise = store_thm (
  "isMorePrecise_morePrecise",
  ``!m1 m2.
    isMorePrecise m1 m2 = morePrecise m1 m2``,
  rpt strip_tac
  \\ Cases_on `m1` \\ Cases_on `m2`
  \\ fs[morePrecise_def, isMorePrecise_def, mTypeToQ_def]);

79 80
val M0_least_precision = store_thm ("M0_least_precision",
  ``!(m:mType).
81
      isMorePrecise m M0 ==>
82
      m = M0``,
83
  fs [isMorePrecise_def, mTypeToQ_def] \\
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
  rpt strip_tac \\
  Cases_on `m` \\
  fs []);

val M0_lower_bound  = store_thm ("M0_lower_bound",
  ``! (m:mType).
      isMorePrecise M0 m``,
  Cases_on `m` \\ EVAL_TAC);

(**
  Function computing the join of two precisions, this is the most precise type,
  in which evaluation has to be performed, e.g. addition of 32 and 64 bit floats
  has to happen in 64 bits
**)
val join_def = Define `
  join (m1:mType) (m2:mType) =
Heiko Becker's avatar
Heiko Becker committed
100
    if (isMorePrecise m1 m2) then m1 else m2`;
101

Heiko Becker's avatar
Heiko Becker committed
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
(* val M0_join_is_M0 = store_thm ("M0_join_is_M0", *)
(*   ``!m1 m2. *)
(*       join m1 m2 = M0 ==> *)
(*       (m1 = M0 /\ m2 = M0)``, *)
(*   fs [join_def, isMorePrecise_def] *)
(*   \\ rpt strip_tac *)
(*   \\ Cases_on `m1 = M0` \\ Cases_on `m2 = M0` \\ fs[] *)
(*   >- (m1 = M0 by (Cases_on `mTypeToQ m1 <= mTypeToQ M0` \\ fs[] *)
(*   \\ fs [ONCE_REWRITE_RULE [isMorePrecise_def] M0_least_precision] *)
(*   \\ Cases_on `m1` \\ fs[mTypeToQ_def] *)
(*   \\ Cases_on `m2` \\ fs[mTypeToQ_def] *)
(*   qpat_x_assum `_ = M0` *)
(*     (fn thm => fs [thm]) *)
(*   >- (Cases_on `m1` \\ fs [mTypeToQ_def]) *)
(*   >- (Cases_on `m2` \\ fs [mTypeToQ_def])); *)

val maxExponent_def = Define `
  (maxExponent (M0) = 0n) /\
  (maxExponent (M16) = 15) /\
  (maxExponent (M32) = 127) /\
  (maxExponent (M64) = 1023)
     (* | M128 => 1023 (** FIXME **) *)
     (* | M256 => 1023 *)`;

val minExponentPos_def = Define `
  (minExponentPos (M0) = 0n) /\
  (minExponentPos (M16) = 14) /\
  (minExponentPos (M32) = 126) /\
  (minExponentPos (M64) = 1022) (*/\ *)
  (* (minExponentPos (M128) = 1022) /\ (* FIXME *) *)
  (* (minExponentPos (M256) = 1022) *)`;

(**
Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
(𝛃 - 𝛃^(1 - p)) * 𝛃^(e_max)

which simplifies to 2^(e_max) for base 2
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
**)

val maxValue_def = Define `
  maxValue (m:mType) = (&(2n ** (maxExponent m))):real`;

(** Using the sign bit, the very same number is representable as a negative number,
  thus just apply negation here **)
val minValue_def = Define `
 minValue (m:mType) = inv (&(2n ** (minExponentPos m)))`;


(** Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
  𝛃^(e_min -p + 1) = 𝛃^(e_min -1) for base 2
**)

val minDenormalValue_def = Define `
Heiko Becker's avatar
Heiko Becker committed
155
  minDenormalValue (m:mType) = 1 / (2 pow (minExponentPos m - 1))`;
156 157 158 159 160

val normal_def = Define `
  normal (v:real) (m:mType) =
    (minValue m <= abs v /\ abs v <= maxValue m)`;

161 162 163 164 165 166
val denormal_def = Define `
  denormal (v:real) (m:mType) =
    case m of
      | M0 => F
      | _ => ((abs v) < (minValue m) /\ v <> 0)`;

167 168 169 170 171 172 173 174 175 176
(**
  Predicate that is true if and only if the given value v is a valid
  floating-point value according to the the type m.
  Since we use the 1 + 𝝳 abstraction, the value must either be
  in normal range or 0.
**)
val validFloatValue_def = Define `
  validFloatValue (v:real) (m:mType) =
   case m of
    | M0 => T
177
    | _ => normal v m \/ denormal v m \/ v = 0`
178

Heiko Becker's avatar
Heiko Becker committed
179 180 181 182 183 184
val validValue_def = Define `
  validValue (v:real) (m:mType) =
    case m of
      | M0 => T
      | _ => abs v <= maxValue m`;

185
val _ = export_theory();