Directed rounding of exact dyadics

Exact signed dyadics round into a binary format under each supported IEEE rounding direction. 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.

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 points Policy.roundDyadicGeneral and Policy.roundDyadic in Rounding.Policy.Runtime delegate to roundDyadicWithRounding for the four IEEE directions, so their packed results agree with these rounders by definition. Additional rounding policies use a separate rational core whose denominator is required to be nonzero.

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

Directed rounding of exact dyadics

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.shiftRightCeilPow2 (n shift : ℕ) : ℕ

ceil(n / 2^shift) for natural numbers.

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.

@[inline]

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

Round an exact dyadic according to an IEEE rounding direction.