Floating-Point Computations with overflow check

The following functions could be used to encode floating-point operations in programs, in the case where one wants to forbids overflows.

Each function comes with two pre-conditions and two post-conditions, one using interpretation in real numbers, one using the predicate t'isFinite from the ieee_float library. The second form should be better with a prover that has built-in support for floating-point numbers.

Single-precision floats

module Single

  use real.RealInfix
  use export ieee_float.Float32

  predicate add_pre_ieee (x:t) (y:t) =
    t'isFinite (x .+ y)

  predicate add_post_ieee (x:t) (y:t) (r:t) =
    r = x .+ y

  predicate add_pre_real (x:t) (y:t) =
    no_overflow RNE (t'real x +. t'real y)

  predicate add_post_real (x:t) (y:t) (r:t) =
    t'real r = round RNE (t'real x +. t'real  y)

  val safe_add (x y: t) : t
    requires { [@expl:finite floating-point number] t'isFinite x }
    requires { [@expl:finite floating-point number] t'isFinite y }
    requires { [@expl:floating-point overflow]
               add_pre_ieee x y \/ add_pre_real x y }
    ensures  { t'isFinite result }
    ensures  { add_post_ieee x y result /\ add_post_real x y result }

  predicate sub_pre_ieee (x:t) (y:t) =
    t'isFinite (x .- y)

  predicate sub_post_ieee (x:t) (y:t) (r:t) =
    r =  x .- y

  predicate sub_pre_real (x:t) (y:t) =
    no_overflow RNE (t'real x -. t'real y)

  predicate sub_post_real (x:t) (y:t) (r:t) =
    t'real r = round RNE (t'real x -. t'real  y)

  val safe_sub (x y: t) : t
    requires { [@expl:finite floating-point number] t'isFinite x }
    requires { [@expl:finite floating-point number] t'isFinite y }
    requires { [@expl:floating-point overflow]
               sub_pre_ieee x y \/ sub_pre_real x y }
    ensures  { t'isFinite result }
    ensures  { sub_post_ieee x y result /\ sub_post_real x y result }

  predicate mul_pre_ieee (x:t) (y:t) =
    t'isFinite (x .* y)

  predicate mul_post_ieee (x:t) (y:t) (r:t) =
    r =  x .* y

  predicate mul_pre_real (x:t) (y:t) =
    no_overflow RNE (t'real x *. t'real y)

  predicate mul_post_real (x:t) (y:t) (r:t) =
    t'real r = round RNE (t'real x *. t'real  y)

  val safe_mul (x y: t) : t
    requires { [@expl:finite floating-point number] t'isFinite x }
    requires { [@expl:finite floating-point number] t'isFinite y }
    requires { [@expl:floating-point overflow]
               mul_pre_ieee x y \/ mul_pre_real x y }
    ensures  { t'isFinite result }
    ensures  { mul_post_ieee x y result /\ mul_post_real x y result }

  predicate div_pre_ieee (x:t) (y:t) =
    t'isFinite (x ./ y)

  predicate div_post_ieee (x:t) (y:t) (r:t) =
    r =  x ./ y

  predicate div_pre_real (x:t) (y:t) =
    no_overflow RNE (t'real x /. t'real y)

  predicate div_post_real (x:t) (y:t) (r:t) =
    t'real r = round RNE (t'real x /. t'real  y)

  val safe_div (x y: t) : t
    requires { [@expl:finite floating-point number] t'isFinite x }
    requires { [@expl:finite floating-point number] t'isFinite y }
    requires { [@expl:non-zero floating-point number] not (is_zero y) }
    requires { [@expl:floating-point overflow]
               div_pre_ieee x y \/ div_pre_real x y }
    ensures  { t'isFinite result }
    ensures  { div_post_ieee x y result /\ div_post_real x y result }

end

Double-precision floats

module Double

  use real.RealInfix
  use export ieee_float.Float64

  predicate add_pre_ieee (x:t) (y:t) =
    t'isFinite (x .+ y)

  predicate add_post_ieee (x:t) (y:t) (r:t) =
    r =  x .+ y

  predicate add_pre_real (x:t) (y:t) =
    no_overflow RNE (t'real x +. t'real y)

  predicate add_post_real (x:t) (y:t) (r:t) =
    t'real r = round RNE (t'real x +. t'real  y)

  val safe_add (x y: t) : t
    requires { [@expl:finite floating-point number] t'isFinite x }
    requires { [@expl:finite floating-point number] t'isFinite y }
    requires { [@expl:floating-point overflow]
               add_pre_ieee x y \/ add_pre_real x y }
    ensures  { t'isFinite result }
    ensures  { add_post_ieee x y result /\ add_post_real x y result }

  predicate sub_pre_ieee (x:t) (y:t) =
    t'isFinite (x .- y)

  predicate sub_post_ieee (x:t) (y:t) (r:t) =
    r =  x .- y

  predicate sub_pre_real (x:t) (y:t) =
    no_overflow RNE (t'real x -. t'real y)

  predicate sub_post_real (x:t) (y:t) (r:t) =
    t'real r = round RNE (t'real x -. t'real  y)

  val safe_sub (x y: t) : t
    requires { [@expl:finite floating-point number] t'isFinite x }
    requires { [@expl:finite floating-point number] t'isFinite y }
    requires { [@expl:floating-point overflow]
               sub_pre_ieee x y \/ sub_pre_real x y }
    ensures  { t'isFinite result }
    ensures  { sub_post_ieee x y result /\ sub_post_real x y result }

  predicate mul_pre_ieee (x:t) (y:t) =
    t'isFinite (x .* y)

  predicate mul_post_ieee (x:t) (y:t) (r:t) =
    r =  x .* y

  predicate mul_pre_real (x:t) (y:t) =
    no_overflow RNE (t'real x *. t'real y)

  predicate mul_post_real (x:t) (y:t) (r:t) =
    t'real r = round RNE (t'real x *. t'real  y)

  val safe_mul (x y: t) : t
    requires { [@expl:finite floating-point number] t'isFinite x }
    requires { [@expl:finite floating-point number] t'isFinite y }
    requires { [@expl:floating-point overflow]
               mul_pre_ieee x y \/ mul_pre_real x y }
    ensures  { t'isFinite result }
    ensures  { mul_post_ieee x y result /\ mul_post_real x y result }

  predicate div_pre_ieee (x:t) (y:t) =
    t'isFinite (x ./ y)

  predicate div_post_ieee (x:t) (y:t) (r:t) =
    r =  x ./ y

  predicate div_pre_real (x:t) (y:t) =
    no_overflow RNE (t'real x /. t'real y)

  predicate div_post_real (x:t) (y:t) (r:t) =
    t'real r = round RNE (t'real x /. t'real  y)

  val safe_div (x y: t) : t
    requires { [@expl:finite floating-point number] t'isFinite x }
    requires { [@expl:finite floating-point number] t'isFinite y }
    requires { [@expl:non-zero floating-point number] not (is_zero y) }
    requires { [@expl:floating-point overflow]
               div_pre_ieee x y \/ div_pre_real x y }
    ensures  { t'isFinite result }
    ensures  { div_post_ieee x y result /\ div_post_real x y result }

end