bench/check-ce/floats.mlw

   1 theory T32
   2
   3   use ieee_float.Float32
   4
   5   goal g1 : forall x:t. t'isFinite x -> eq x (0.0:t)
   6
   7   goal g2 : forall x:t. t'isFinite x -> eq x (1.25:t)
   8
   9   goal g3 : forall x:t. not (eq x (0.0:t))
  10
  11   goal g4 : forall x:t. not (eq x (1.25:t))
  12
  13   goal g5 : forall x:t. not (ge x (4.25:t))
  14
  15   goal g6 : forall x:t. eq x x
  16
  17   goal g7 : forall x:t. t'isFinite x -> gt (add RNE x (1.0:t)) x
  18
  19   goal g8 : forall x:t. not (eq x (div RNE (1.0:t) (0.0:t)))
  20
  21   goal g9 : forall x:t. gt x (0.0:t) -> gt (div RNE x (2.0:t)) (0.0:t)
  22   (** should give the smallest positive, i.e., 2^{-149} *)
  23
  24   goal g10: forall x:t. not (ge (mul RNE (10.0:t) x) (1.0:t) /\ (le (mul RTZ (10.0:t) x) (1.0:t)))
  25
  26   goal g11: forall x:t. not (eq x (0x1p-126:t))
  27   (** 2^{-126} is normal *)
  28
  29   goal g12: forall x:t. not (eq x (0x0.FFFFFEp-126:t))
  30   (** prec of 2^{-126} is subnormal *)
  31
  32   goal g13: forall x:t. not (eq x (0x1p-127:t))
  33   (** 2^{-127} is subnormal *)
  34
  35 end
  36
  37 theory T64
  38
  39   use ieee_float.Float64
  40
  41   goal g1 : forall x:t. t'isFinite x -> eq x (0.0:t)
  42
  43   goal g2 : forall x:t. t'isFinite x -> eq x (1.25:t)
  44
  45   goal g3 : forall x:t. not (eq x (0.0:t))
  46
  47   goal g4 : forall x:t. not (eq x (1.25:t))
  48
  49   goal g5 : forall x:t. not (ge x (4.25:t))
  50
  51   goal g6 : forall x:t. eq x x
  52
  53   goal g7 : forall x:t. t'isFinite x -> gt (add RNE x (1.0:t)) x
  54
  55   goal g8 : forall x:t. not (eq x (div RNE (1.0:t) (0.0:t)))
  56
  57   goal g9 : forall x:t. gt x (0.0:t) -> gt (div RNE x (2.0:t)) (0.0:t)
  58   (** should give the smallest positive, i.e., 2^{-1074} *)
  59
  60   goal g10: forall x:t. not (ge (mul RNE (10.0:t) x) (1.0:t) /\ (le (mul RTZ (10.0:t) x) (1.0:t)))
  61
  62   goal g11: forall x:t. not (eq x (0x1p-1022:t))
  63   (** 2^{-1022} is normal *)
  64
  65   goal g12: forall x:t. not (eq x (0x0.FFFFFFFFFFFFFp-1022:t))
  66   (** prec of 2^{-1022} is subnormal *)
  67
  68   goal g13: forall x:t. not (eq x (0x1p-1023:t))
  69   (** 2^{-1023} is subnormal *)
  70
  71 end