Directed rounding of exact dyadics

Exact signed dyadics round into a binary format under each IEEERoundingMode. Toward-zero, toward-positive, and toward-negative rounding are implemented by one pair of magnitude rounders, roundDyadicMagnitudeDown and roundDyadicMagnitudeUp, that the sign of the value selects between. Nearest-even delegates to Model.roundDyadic.

Two further rounders are built from the same pieces. roundDyadicAway (MPFR's MPFR_RNDA) always rounds the magnitude up. roundDyadicNearestAway (IEEE 754-2019 roundTiesToAway) is nearest-even except at an exact tie on the format's grid, which dyadicIsGridTie detects and which then rounds away from zero.

Overflow follows directedOverflow: a magnitude carried upward becomes the format's native overflow value and a magnitude carried downward becomes the largest finite value. The policy entry point Policy.roundDyadic in Rounding.Policy.Runtime delegates to Internal.Directed.roundDyadic for the six directions with native overflow and gradual underflow. Policy.roundDyadicGeneral is a separate rational core whose agreement with these rounders is proved in Rounding.Policy.Agreement.

Every threshold is derived from FloatFormat. The magnitude helpers require a positive mantissa, and the signed entry points handle zero before selecting a magnitude helper.

Directed rounding of exact dyadics

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicMagnitudeDown (fmt : FloatFormat) (sign : Bool) (mantissa : ℕ) (exponent : ℤ) : Model fmt

Round an exact positive magnitude downward, attaching sign to the result.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicMagnitudeUp (fmt : FloatFormat) (sign : Bool) (mantissa : ℕ) (exponent : ℤ) : Model fmt

Round an exact positive magnitude upward, attaching sign to the result.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicPosDown (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) : Model fmt

Round a positive exact dyadic toward negative infinity.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicPosUp (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) : Model fmt

Round a positive exact dyadic toward positive infinity.

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

Round an exact dyadic toward negative infinity.

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

Round an exact dyadic toward positive infinity.

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

Round an exact dyadic toward zero.

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

Round an exact dyadic away from zero, MPFR's MPFR_RNDA.

The magnitude rounds up and keeps its sign, so a nonzero value below the least subnormal becomes that subnormal and a magnitude carried past the largest finite value becomes the native overflow value.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsGridTie (fmt : FloatFormat) (value : Numerics.Dyadic) : Bool

Whether an exact dyadic lies exactly halfway between two adjacent values of the binary grid of fmt with gradual underflow and no upper exponent bound.

A magnitude whose leading bit has exponent L lies on a grid of spacing 2^(max fmt.minSubnormalExponent (L - fmt.fracWidth)): the subnormal spacing below the normal range and the spacing of its own binade above it, as roundDyadic rounds. The value is a tie when the bits below that spacing are exactly one half of it, as Numerics.shiftRightIsTie tests. Zero is never a tie, and neither is a magnitude below half the least subnormal, whose guard bit is clear. The grid continues past the largest finite value, so the midpoint between that value and the next grid value is a tie, and so are ties in binades above the finite range.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsGridTie_zero (fmt : FloatFormat) (sign : Bool) (exponent : ℤ) : dyadicIsGridTie fmt { negative := sign, significand := 0, exponent := exponent } = false

Zero is never a grid tie.

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

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

Off a grid tie the nearer neighbour is unique and this is nearest-even rounding, roundDyadic. At a tie both neighbours are equally near and the magnitude rounds up, as roundDyadicAway computes. Overflow and underflow therefore behave as in nearest-even rounding, except that a tie at the overflow midpoint overflows whatever the parity of the largest finite significand, and the midpoint between zero and the least subnormal rounds to that subnormal.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.roundDyadic (fmt : FloatFormat) (mode : IEEERoundingMode) (value : Numerics.Dyadic) : Model fmt

Round an exact dyadic in the direction mode, the rounding step of every directed kernel. Nearest-even is Model.roundDyadic.