examples/numeric/exp_log.mlw

   1 module ExpLogSingle
   2   use real.RealInfix
   3   use real.Abs
   4   use real.ExpLog
   5   use ufloat.USingle
   6   use ufloat.USingleLemmas
   7
   8   constant log_error:real
   9   axiom log_error_bounds : 0. <=. log_error <=. 1.
  10   constant log_cst_error:real
  11   axiom log_cst_error_bounds : 0. <=. log_cst_error <=. 1.
  12   val function log_approx (x:usingle) : usingle
  13     requires { 0. <. to_real x }
  14     ensures {
  15       abs (to_real result -. log (to_real x)) <=. abs (log (to_real x)) *. log_error +. log_cst_error
  16     }
  17
  18   constant log2_error:real
  19   axiom log2_error_bounds : 0. <=. log2_error <=. 1.
  20   val function log2_approx (x:usingle) : usingle
  21     requires { 0. <. to_real x }
  22     ensures {
  23       abs (to_real result -. log2 (to_real x)) <=. abs (log2 (to_real x)) *. log2_error
  24     }
  25
  26   constant log10_error:real
  27   axiom log10_error_bounds : 0. <=. log10_error <=. 1.
  28   val function log10_approx (x:usingle) : usingle
  29     requires { 0. <. to_real x }
  30     ensures {
  31       abs (to_real result -. log10 (to_real x)) <=. abs (log10 (to_real x)) *. log10_error
  32     }
  33
  34   constant exp_error:real
  35   axiom exp_error_bounds : 0. <=. exp_error <=. 0x1p-2
  36   val function exp_approx (x:usingle) : usingle
  37     ensures {
  38       abs (to_real result -. exp (to_real x)) <=. exp_error *. exp (to_real x)
  39     }
  40
  41   let ghost example1 (x y : usingle)
  42     ensures {
  43     let t = log (exp (to_real y)) in
  44     let t1 = log (exp (to_real x)) in
  45     let t2 =
  46       ((1.0 +. eps) +. log_error)
  47       *. (((-. log (1.0 -. exp_error)) *. (1.0 +. log_error))
  48           +. log_cst_error)
  49     in
  50     abs (to_real result -. (t1 +. t))
  51     <=. ((((log_error +. log_error) +. eps) *. (abs t1 +. abs t))
  52          +. (t2 +. t2))
  53     }
  54   = log_approx (exp_approx(x)) ++. log_approx (exp_approx(y))
  55
  56   let ghost example2 (x y : usingle)
  57     ensures {
  58       let exact = log(exp(to_real x) +. exp (to_real y)) in
  59       abs (to_real result -. exact)
  60       <=. abs exact *. log_error
  61          +. ((-. log (1.0 -. ((2. *. exp_error) +. eps))) *. (1.0 +. log_error)) +. log_cst_error
  62     }
  63   = log_approx (exp_approx(x) ++. exp_approx(y))
  64
  65   let ghost example3 (x y : usingle)
  66     requires { 0. <. to_real x }
  67     requires { 0. <. to_real y }
  68     ensures {
  69       let exact = log2(to_real x +. to_real y) in
  70       abs (to_real result -. exact)
  71       <=. abs exact *. log2_error
  72          +. ((-. log2 (1.0 -. (eps))) *. (1.0 +. log2_error))
  73     }
  74   = log2_approx (x ++. y)
  75
  76   let ghost example4 (x y : usingle)
  77     requires { 0. <. to_real x }
  78     requires { 0. <. to_real y }
  79     ensures {
  80       let exact = log10(to_real x +. to_real y) in
  81       abs (to_real result -. exact)
  82       <=. abs exact *. log10_error
  83          +. ((-. log10 (1.0 -. (eps))) *. (1.0 +. log10_error))
  84     }
  85   = log10_approx (x ++. y)
  86
  87 end
  88
  89 module ExpLogDouble
  90   use real.RealInfix
  91   use real.Abs
  92   use real.ExpLog
  93   use ufloat.UDouble
  94   use ufloat.UDoubleLemmas
  95
  96   constant log_error:real
  97   axiom log_error_bounds : 0. <=. log_error <=. 1.
  98   constant log_cst_error:real
  99   axiom log_cst_error_bounds : 0. <=. log_cst_error <=. 1.
 100   val function log_approx (x:udouble) : udouble
 101     requires { 0. <. to_real x }
 102     ensures {
 103       abs (to_real result -. log (to_real x)) <=. abs (log (to_real x)) *. log_error +. log_cst_error
 104     }
 105
 106   constant log2_error:real
 107   axiom log2_error_bounds : 0. <=. log2_error <=. 1.
 108   val function log2_approx (x:udouble) : udouble
 109     requires { 0. <. to_real x }
 110     ensures {
 111       abs (to_real result -. log2 (to_real x)) <=. abs (log2 (to_real x)) *. log2_error
 112     }
 113
 114   constant log10_error:real
 115   axiom log10_error_bounds : 0. <=. log10_error <=. 1.
 116   val function log10_approx (x:udouble) : udouble
 117     requires { 0. <. to_real x }
 118     ensures {
 119       abs (to_real result -. log10 (to_real x)) <=. abs (log10 (to_real x)) *. log10_error
 120     }
 121
 122   constant exp_error:real
 123   axiom exp_error_bounds : 0. <=. exp_error <=. 0x1p-3
 124   val function exp_approx (x:udouble) : udouble
 125     ensures {
 126       abs (to_real result -. exp (to_real x)) <=. exp_error *. exp (to_real x)
 127     }
 128
 129   let ghost example1 (x y : udouble)
 130     ensures {
 131     let t = log (exp (to_real y)) in
 132     let t1 = log (exp (to_real x)) in
 133     let t2 =
 134       ((1.0 +. eps) +. log_error)
 135       *. (((-. log (1.0 -. exp_error)) *. (1.0 +. log_error))
 136           +. log_cst_error)
 137     in
 138     abs (to_real result -. (t1 +. t))
 139     <=. ((((log_error +. log_error) +. eps) *. (abs t1 +. abs t))
 140          +. (t2 +. t2))
 141     }
 142   = log_approx (exp_approx(x)) ++. log_approx (exp_approx(y))
 143
 144   let ghost example2 (x y : udouble)
 145     ensures {
 146       let exact = log(exp(to_real x) +. exp (to_real y)) in
 147       abs (to_real result -. exact)
 148       <=. abs exact *. log_error
 149          +. ((-. log (1.0 -. ((2. *. exp_error) +. eps))) *. (1.0 +. log_error)) +. log_cst_error
 150     }
 151   = log_approx (exp_approx(x) ++. exp_approx(y))
 152
 153   let ghost example3 (x y : udouble)
 154     requires { 0. <. to_real x }
 155     requires { 0. <. to_real y }
 156     ensures {
 157       let exact = log2(to_real x +. to_real y) in
 158       abs (to_real result -. exact)
 159       <=. abs exact *. log2_error
 160          +. ((-. log2 (1.0 -. (eps))) *. (1.0 +. log2_error))
 161     }
 162   = log2_approx (x ++. y)
 163
 164   let ghost example4 (x y : udouble)
 165     requires { 0. <. to_real x }
 166     requires { 0. <. to_real y }
 167     ensures {
 168       let exact = log10(to_real x +. to_real y) in
 169       abs (to_real result -. exact)
 170       <=. abs exact *. log10_error
 171          +. ((-. log10 (1.0 -. (eps))) *. (1.0 +. log10_error))
 172     }
 173   = log10_approx (x ++. y)
 174
 175 end