examples_in_progress/my_cosine.mlw

   1
   2 (* Approximated cosine *)
   3
   4 module M
   5
   6   use real.RealInfix
   7   use real.Abs
   8   use real.Trigonometry
   9   use floating_point.Rounding
  10   use floating_point.Single
  11
  12   val single_of_real_exact (x: real) : single
  13     ensures { value result = x }
  14
  15   val add (x y: single) : single
  16     requires { [@expl:floating-point overflow]
  17                no_overflow NearestTiesToEven ((value x) +. (value y)) }
  18     ensures  { value result = round NearestTiesToEven ((value x) +. (value y))}
  19
  20   val sub (x y: single) : single
  21     requires { [@expl:floating-point overflow]
  22                no_overflow NearestTiesToEven ((value x) -. (value y)) }
  23     ensures  { value result = round NearestTiesToEven ((value x) -. (value y))}
  24
  25   val mul (x y: single) : single
  26     requires { [@expl:floating-point overflow]
  27                no_overflow NearestTiesToEven ((value x) *. (value y)) }
  28     ensures  { value result = round NearestTiesToEven ((value x) *. (value y))}
  29
  30   let my_cosine (x:single) : single
  31     requires { abs (value x) <=. 0x1p-5 }
  32     ensures { abs (value result -. cos (value x)) <=. 0x1p-23 }
  33   = assert {
  34       abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
  35     };
  36     sub (single_of_real_exact 1.0) (mul (mul x x) (single_of_real_exact 0.5))
  37
  38 end
  39
  40
  41
  42 module IEEEfloat
  43
  44   use real.RealInfix
  45   use real.Abs
  46   use real.Trigonometry
  47   use ieee_float.Float32
  48
  49   val add (x y: t) : t
  50     requires { [@expl:floating-point overflow] t'isFinite (x .+ y) }
  51     ensures  { result = x .+ y }
  52
  53   val sub (x y: t) : t
  54     requires { [@expl:floating-point overflow] t'isFinite (x .- y)}
  55     ensures  { result = x .- y }
  56
  57   val mul (x y: t) : t
  58     requires { [@expl:floating-point overflow] t'isFinite (x .* y)}
  59     ensures  { result = x .* y }
  60
  61   let my_cosine (x:t) : t
  62     requires { Float32.abs x .<= (0x1p-5:t) }
  63     ensures  { Abs.abs (t'real result -. cos (t'real x)) <=. 0x1p-23 }
  64   = assert { Abs.abs (t'real x) <=. 0x1p-5 };
  65     assert {
  66       Abs.abs (1.0 -. (t'real x) *. (t'real x) *. 0.5 -. cos (t'real x)) <=. 0x1p-24
  67     };
  68     sub (1.0:t) (mul (mul x x) (0.5:t))
  69
  70 end
  71
  72
  73 module Combined
  74
  75   use real.RealInfix
  76   use real.Abs
  77   use real.Trigonometry
  78   use mach.float.Single
  79
  80   let my_cosine (x:t) : t
  81     requires { abs x .<= (0x1p-5:t) }
  82     ensures  { Abs.abs (t'real result -. cos (t'real x)) <=. 0x1p-23 }
  83   = assert { Abs.abs (t'real x) <=. 0x1p-5 };
  84     assert {
  85       Abs.abs (1.0 -. (t'real x) *. (t'real x) *. 0.5 -. cos (t'real x)) <=. 0x1p-24
  86     };
  87     safe_sub (1.0:t) (safe_mul (safe_mul x x) (0.5:t))
  88
  89 end