module MultiplicationSingle
  use real.RealInfix
  use real.Abs
  use ufloat.USingle
  use ufloat.USingleLemmas

  let multiplication_errors_basic (a b c : usingle)
    ensures {
      let exact = to_real a *. to_real b *. to_real c in
      abs (to_real result -. exact) <=.
      (2. +. eps) *. eps *. abs exact +. eta *. (abs (to_real c) *. (1. +. eps) +. 1.)
    }
  = a **. b **. c

  let multiplication_errors (a b c d e f: usingle)
  ensures {
    let t = 1.0 +. eps in
    let t3 = eps +. (eps *. t) in
    let t4 = to_real d *. (to_real e *. to_real f) in
    let t5 = (to_real a *. to_real b) *. to_real c in
    let t6 = ((eta *. abs (to_real d)) *. t) +. eta in
    let t7 = ((eta *. abs (to_real c)) *. t) +. eta in
    let exact = t5 *. t4 in
    abs (to_real result -. exact) <=.
      (* Relative part of the error *)
      (eps +. (t3 +. t3 +. (t3 *. t3)) *. t) *. abs exact +.
      (* Absolute part of the error *)
      ((t6 +. t6 *. t3) *. abs t5 +.
       (t7 +. t7 *. t3) *. abs t4 +. t7 *. t6)
        *. t +. eta
    }
  = (a **. b **. c) **. (d **. (e **. f))

end

module MultiplicationDouble
  use real.RealInfix
  use real.Abs
  use ufloat.UDouble
  use ufloat.UDoubleLemmas

  let multiplication_errors_basic (a b c : udouble)
    ensures {
      let exact = to_real a *. to_real b *. to_real c in
      abs (to_real result -. exact) <=.
      (2. +. eps) *. eps *. abs exact +. eta *. (abs (to_real c) *. (1. +. eps) +. 1.)
    }
  = a **. b **. c

  let multiplication_errors (a b c d e f: udouble)
  ensures {
    let t = 1.0 +. eps in
    let t3 = eps +. (eps *. t) in
    let t4 = to_real d *. (to_real e *. to_real f) in
    let t5 = (to_real a *. to_real b) *. to_real c in
    let t6 = ((eta *. abs (to_real d)) *. t) +. eta in
    let t7 = ((eta *. abs (to_real c)) *. t) +. eta in
    let exact = t5 *. t4 in
    abs (to_real result -. exact) <=.
      (* Relative part of the error *)
      (eps +. (t3 +. t3 +. (t3 *. t3)) *. t) *. abs exact +.
      (* Absolute part of the error *)
      ((t6 +. t6 *. t3) *. abs t5 +.
       (t7 +. t7 *. t3) *. abs t4 +. t7 *. t6)
        *. t +. eta
    }
  = (a **. b **. c) **. (d **. (e **. f))
end
