Agreement between the policy engine and nearest-away dyadic rounding

Policy.roundDyadic sends a nearest-away policy with native overflow and gradual underflow to the dyadic rounder roundDyadicNearestAway through Internal.Directed.roundDyadic .nearestAway. This file proves the general rational engine roundDyadicGeneral equal to that rounder on every descriptor, so the two implementations agree and the dispatch changes no result. The packed results agree, including signed zero, subnormal carry, ties at the overflow midpoint, and finite-only overflow words. Rounding.Policy.Agreement uses the theorem for its nearest-away case.

The proof compares the engine with itself under two other rounding modes. roundRatGeneralOfDenNeZero_congr_rounding says that the engine depends on its rounding mode only through the overflow direction, the decision for values below half the least subnormal, and the one quotient that the input's leading exponent selects. Off a grid tie that quotient is not a tie either, so nearest-away and nearest-even choose the same integer and the nearest-even agreement of Rounding.Policy.ScaledDyadic applies. At a grid tie the value is never below half the least subnormal, nearest-away takes the ceiling of the tied quotient, and the engine agrees with the directed policy that rounds the magnitude up, whose packed result is roundDyadicMagnitudeUp.

For status, rationalNearestAwayOverflowsScaled_eq_true_iff and rationalIsTinyAfterRoundingScaled_nearest_eq give the classifiers their real meaning, and isTinyAfterRounding_roundRatGeneralOfDenNeZero_nearestAway_eq_false shows that the engine, which Policy.roundRat uses for nearest-away conversions, never delivers a tiny result at or above underflowMidpoint.

Grid ties of exact dyadics

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.significand_ne_zero_of_dyadicIsGridTie {fmt : FloatFormat} {value : Numerics.Dyadic} (htie : dyadicIsGridTie fmt value = true) : value.significand ≠ 0

A grid tie has a nonzero significand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsGridTie_eq_false_of_far_below (fmt : FloatFormat) (value : Numerics.Dyadic) (hfar : ↑value.significand.log2 + value.exponent + 1 < fmt.minSubnormalExponent) : dyadicIsGridTie fmt value = false

A dyadic below half the least subnormal is never a grid tie: its guard bit is clear.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsGridTie_eq_true_iff (fmt : FloatFormat) (value : Numerics.Dyadic) : dyadicIsGridTie fmt value = true ↔ 2 * ((Numerics.RationalBinary.scaleByPowerOfTwo value.significand 1 (value.exponent - max fmt.minSubnormalExponent (↑value.significand.log2 + value.exponent - ↑fmt.fracWidth))).1 % (Numerics.RationalBinary.scaleByPowerOfTwo value.significand 1 (value.exponent - max fmt.minSubnormalExponent (↑value.significand.log2 + value.exponent - ↑fmt.fracWidth))).2) = (Numerics.RationalBinary.scaleByPowerOfTwo value.significand 1 (value.exponent - max fmt.minSubnormalExponent (↑value.significand.log2 + value.exponent - ↑fmt.fracWidth))).2

A dyadic is a grid tie exactly when it is a quotient tie scaled to its grid exponent.

Quotient rounding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_nearestAway_eq_roundQuotient (sign : Bool) (entropy numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : roundQuot Numerics.RoundingMode.nearestAway sign entropy numerator denominator = Numerics.roundQuotient Numerics.MagnitudeRounding.nearestAway numerator denominator

Policy nearest-away quotient rounding is roundQuotient .nearestAway for a nonzero divisor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_nearestAway_eq_nearest_of_ne (sign : Bool) (entropy entropy' numerator denominator : ℕ) (htie : 2 * (numerator % denominator) ≠ denominator) : roundQuot Numerics.RoundingMode.nearestAway sign entropy numerator denominator = roundQuot Numerics.RoundingMode.nearest sign entropy' numerator denominator

Off an exact tie, policy nearest-away and nearest-even quotient rounding agree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_nearestAway_eq_roundQuotDirected_of_tie (sign : Bool) (entropy numerator denominator : ℕ) (hdenominator : denominator ≠ 0) (htie : 2 * (numerator % denominator) = denominator) : roundQuot Numerics.RoundingMode.nearestAway sign entropy numerator denominator = roundQuotDirected true numerator denominator

At an exact tie, policy nearest-away quotient rounding takes the ceiling.

Rounding-mode congruence of the general engine

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundRatGeneralOfDenNeZero_congr_rounding (fmt : FloatFormat) (overflow : Numerics.OverflowMode) (underflow : Numerics.UnderflowMode) (rounding rounding' : Numerics.RoundingMode) (entropy entropy' : ℕ) (sign : Bool) (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) (hoverflow : overflowRoundsMagnitudeUp rounding sign = overflowRoundsMagnitudeUp rounding' sign) (htiny : numerator ≠ 0 → Numerics.RationalBinary.floorLog2 numerator denominator + 1 < fmt.minSubnormalExponent → tinyRoundsMagnitudeUp? rounding sign = tinyRoundsMagnitudeUp? rounding' sign) (hsubnormal : numerator ≠ 0 → Numerics.RationalBinary.floorLog2 numerator denominator < fmt.minNormalExponent → roundQuot rounding sign entropy (numerator.shiftLeft (fmt.exponentBias + fmt.fracWidth - 1)) denominator = roundQuot rounding' sign entropy' (numerator.shiftLeft (fmt.exponentBias + fmt.fracWidth - 1)) denominator) (hnormal : numerator ≠ 0 → fmt.minNormalExponent ≤ Numerics.RationalBinary.floorLog2 numerator denominator → Numerics.RationalBinary.floorLog2 numerator denominator ≤ fmt.maxNormalExponent → have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - Numerics.RationalBinary.floorLog2 numerator denominator); roundQuot rounding sign entropy scaled.1 scaled.2 = roundQuot rounding' sign entropy' scaled.1 scaled.2) : roundRatGeneralOfDenNeZero fmt { rounding := rounding, overflow := overflow, underflow := underflow } entropy sign numerator denominator hdenominator = roundRatGeneralOfDenNeZero fmt { rounding := rounding', overflow := overflow, underflow := underflow } entropy' sign numerator denominator hdenominator

The general engine depends on its rounding mode only through the overflow direction, the decision below half the least subnormal, and the one quotient that it rounds.

For a fixed input, two rounding modes give the same packed result when they agree on overflowRoundsMagnitudeUp, on tinyRoundsMagnitudeUp? for a value below half the least subnormal, and on roundQuot at the quotient that the leading exponent selects: the subnormal alignment below the normal range and the significand quotient within it. The entropy may differ as well.

The quotient sites of an exact dyadic

Nearest-away agreement

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadicGeneral_nearestAway_eq_roundDyadicNearestAway (fmt : FloatFormat) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadicGeneral fmt { rounding := Numerics.RoundingMode.nearestAway } entropy value = roundDyadicNearestAway fmt value

General policy rounding with nearest-away rounding, native overflow, and gradual underflow is the dyadic nearest-away rounder's complete packed result, on every descriptor.

The entropy argument is irrelevant because nearest-away rounding is deterministic.

Status classifiers

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalNearestAwayOverflowsScaled_eq_true_iff (fmt : FloatFormat) (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : rationalNearestAwayOverflowsScaled fmt numerator denominator 0 = true ↔ (overflowMidpoint fmt).toReal ≤ ↑numerator / ↑denominator

Nearest-away overflow of a nonnegative scaled rational is reaching the top finite midpoint: the midpoint itself overflows.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalIsTinyAfterRoundingScaled_nearest_eq {fmt : FloatFormat} (sign : Bool) (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) (rounded : Model fmt) : rationalIsTinyAfterRoundingScaled fmt IEEERoundingMode.nearest sign numerator denominator 0 rounded = (rounded.isTinyAfterRounding || decide (↑numerator / ↑denominator < (underflowMidpoint fmt).toReal))

With the nearest-even boundary, the tininess classifier for a nonnegative rational is a tiny delivered result or a magnitude strictly below underflowMidpoint. The midpoint itself is not tiny because nearest rounding takes it up to the smallest normal value.

Tininess of the nearest-away engine result

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.isTinyAfterRounding_roundRatGeneralOfDenNeZero_nearestAway_eq_false (fmt : FloatFormat) (overflow : Numerics.OverflowMode) (underflow : Numerics.UnderflowMode) (entropy : ℕ) (sign : Bool) (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) (hbound : (underflowMidpoint fmt).toReal ≤ ↑numerator / ↑denominator) : (roundRatGeneralOfDenNeZero fmt { rounding := Numerics.RoundingMode.nearestAway, overflow := overflow, underflow := underflow } entropy sign numerator denominator hdenominator).isTinyAfterRounding = false

Nearest-away rounding in the general engine never delivers a tiny result for an exact quotient at or above underflowMidpoint, under every overflow and underflow policy.

At that magnitude the unbounded-exponent rounding already reaches the smallest normal value. The engine then delivers the smallest normal value, a larger normal value, or an overflow value, and flush-to-zero leaves each of them unchanged.