Format-parameterized binary arithmetic runtime

Each of the six IEEE arithmetic operations has one name with two options, a rounding direction mode (nearest-even by default) and status, which selects whether the result is the delivered value or the complete IEEEOutcome with the five exception flags and the ternary value:

Model.sqrt x
Model.sqrt x (mode := .up)
Model.sqrt x (mode := .up) (status := true)

With open FloatLib.Rounding, the mode can be written (mode := up).

Each operation is a small @[macro_inline] selector. It tests status first, so a value call never computes flags, and then mode: nearest-even goes straight to the dispatched kernel in Model.Internal.Nearest, the other directions to Model.Internal.Directed, and status calls to Model.Internal.Status. With literal options the compiler keeps only the selected kernel call. Square root also sends nearest-away to the nearest-even kernel, since an exact square root is never a tie.

This module contains only executable definitions, and their refinement theorems live in Arithmetic.Proof and Status.Proof.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.add {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE addition, rounded in mode (nearest-even by default). With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sub {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE subtraction, rounded in mode (nearest-even by default). With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.mul {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE multiplication, rounded in mode (nearest-even by default). With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.div {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE division, rounded in mode (nearest-even by default). With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt {fmt : FloatFormat} (x : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE square root, rounded in mode (nearest-even by default). With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.fma {fmt : FloatFormat} (x y z : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE fused multiply-add x * y + z with one rounding in mode (nearest-even by default). With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value.