Executable directed rounding

Exact rational intermediates support the six IEEERoundingMode choices. Together with the dyadic rounders of Rounding.Directed.Dyadic, they implement the directed kernels of addition, subtraction, multiplication, division, fused multiply-add, and square root in Model.Internal.Directed. Model.add x y (mode := .up) and its siblings in Arithmetic.Runtime call them for every direction except nearest-even. roundRatNearestAwayScaled and its tie test rationalIsGridTieScaled are the rational twins of the dyadic nearest-away rounder.

Rounding thresholds, signed-zero behavior, and exceptional results follow the FloatFormat descriptor. DirectedSemantics proves the real and extended-real correctness theorems, with their format and input hypotheses.

Directed rounding of exact rationals

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled (fmt : FloatFormat) (roundMagnitudeUp sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round a scaled positive rational magnitude to the adjacent lower or upper representable magnitude.

roundMagnitudeUp = false selects the lower magnitude and true selects the upper magnitude. The sign parameter supplies the sign to the format's packing, zero, and overflow constructors.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalIsGridTieScaled (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) : Bool

Whether the scaled rational (numerator / denominator) * 2^exponent lies exactly halfway between two adjacent values of the binary grid of fmt with gradual underflow and no upper exponent bound.

This is the rational twin of dyadicIsGridTie, on the same grid. The rational is scaled as roundRatScaledGeneral scales it, to the subnormal spacing below the normal range and to fracWidth + 1 significant bits above it, and it is a tie when twice the remainder of that quotient equals its denominator. A zero numerator or denominator is never a tie. A magnitude below half the least subnormal is recognized from its leading exponent alone, so the subnormal shift stays bounded by the operand widths and the destination precision.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatNearestAwayScaled (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round an exact scaled signed rational to nearest with ties away from zero, IEEE 754-2019 roundTiesToAway.

This is the rational twin of roundDyadicNearestAway. Off a grid tie it is nearest-even rounding, roundRatScaled. At a tie the magnitude rounds up with roundRatMagnitudeDirectedScaled. A zero denominator is never a tie and takes the result of roundRatScaled.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.roundRatScaled (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round the exact scaled signed rational ±(numerator / denominator) * 2^exponent in the direction mode. Nearest-even is Model.roundRatScaled.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.roundRat (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) : Model fmt

Round the exact signed rational ±numerator / denominator in the direction mode. Nearest-even is Model.roundRat.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatDownScaled (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round an exact scaled signed rational toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatUpScaled (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Model fmt

Round an exact scaled signed rational toward positive infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatDown (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) : Model fmt

Round an exact signed rational toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatUp (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) : Model fmt

Round an exact signed rational toward positive infinity.

Arithmetic under an explicit rounding direction

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.zeroForExactSum (fmt : FloatFormat) (mode : IEEERoundingMode) (leftSign rightSign : Bool) : Model fmt

Zero for an exactly cancelling addition under mode. It requests the sign IEEERoundingMode.zeroSumSign, and zero delivers positive zero instead in a format without a signed zero.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.add {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : Model fmt

IEEE addition in rounding direction mode, the kernel of Model.add x y (mode := mode).

Nearest-even addition is the dispatched Nearest.add, and every other direction rounds the exact dyadic sum once.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.sub {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : Model fmt

IEEE subtraction in rounding direction mode, the kernel of Model.sub x y (mode := mode): directed addition of the negated right operand.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.mul {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : Model fmt

IEEE multiplication in rounding direction mode, the kernel of Model.mul x y (mode := mode).

Nearest-even multiplication is the dispatched Nearest.mul, and every other direction rounds the exact dyadic product once.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.div {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : Model fmt

IEEE division in rounding direction mode, the kernel of Model.div x y (mode := mode).

Nearest-even division is the dispatched Nearest.div, and every other direction rounds the exact scaled rational quotient once.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.fma {fmt : FloatFormat} (mode : IEEERoundingMode) (x y z : Model fmt) : Model fmt

IEEE fused multiply-add in rounding direction mode, the kernel of Model.fma x y z (mode := mode).

Nearest-even FMA is the dispatched Nearest.fma, and every other direction rounds the exact dyadic x * y + z once.

Directed square root

structure FloatLib.Floats.Formats.BinaryInterchange.Model.SqrtDyadicBracket : Type

Dyadic endpoint pair used to enclose a nonnegative square root.

• lower : Numerics.Dyadic

  Lower endpoint.

• upper : Numerics.Dyadic

  Upper endpoint.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtDyadicBracket (fmt : FloatFormat) (value : Numerics.Dyadic) : SqrtDyadicBracket

Compute a dyadic enclosure of the square root of a nonnegative exact dyadic.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.sqrt {fmt : FloatFormat} (mode : IEEERoundingMode) (x : Model fmt) : Model fmt

IEEE square root in rounding direction mode, the kernel of Model.sqrt x (mode := mode).

Both nearest modes use the dispatched nearest-even Nearest.sqrt. The exact square root of a value of the format is never halfway between two adjacent values of the format's grid, because the square of such a midpoint is not a value of the format: in a normal binade its odd part has more significant bits than any significand, and below the normal range it is not a multiple of the least subnormal. Nearest-away rounding therefore never meets a tie here. The directed modes round an endpoint of sqrtDyadicBracket: the upper one when the positive result rounds up, toward positive infinity or away from zero, and the lower one otherwise.