Branch equations for nearest-even rational packing

roundRatScaled rejects a zero denominator, returns a signed zero for a zero numerator, and otherwise selects an overflow, underflow, subnormal, normal, or carry-out result from the leading exponent of the quotient. The equations below describe each positive-magnitude branch of the IEEE path in terms of the descriptor's semantic exponent bounds. They are used in the finiteness and rounded-real proofs.

Positive packing branches

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_false_eq_of_isIEEE (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : roundRatScaled fmt false numerator denominator exponent = have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator; have totalExponent := rationalExponent + exponent; if fmt.maxNormalExponent < totalExponent then posInf fmt else if totalExponent < fmt.minSubnormalExponent - 1 then posZero fmt else if totalExponent < fmt.minNormalExponent then have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp); have rounded := Numerics.roundQuotientEven scaled.1 scaled.2; if rounded = 0 then posZero fmt else if pow2 fmt.fracWidth ≤ rounded then ofFields fmt false 1 0 else ofFields fmt false 0 rounded else have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent); have rounded := Numerics.roundQuotientEven scaled.1 scaled.2; if rounded = pow2 (fmt.fracWidth + 1) then if fmt.maxNormalExponent < totalExponent + 1 then posInf fmt else ofFields fmt false (totalExponent + 1 + Int.ofNat fmt.exponentBias).toNat 0 else ofFields fmt false (totalExponent + Int.ofNat fmt.exponentBias).toNat (rounded - pow2 fmt.fracWidth)

The IEEE path of roundRatScaled on a positive nonzero rational, with every executable test rewritten to the descriptor's semantic exponent bounds and to propositional conditions.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_false_eq_posInf_of_maxNormal_lt (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hoverflow : fmt.maxNormalExponent < Numerics.RationalBinary.floorLog2 numerator denominator + exponent) : roundRatScaled fmt false numerator denominator exponent = posInf fmt

Positive nearest-even packing overflows to positive infinity above the normal range.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_false_eq_posZero_of_lt_minSubnormal_sub_one (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hmax : Numerics.RationalBinary.floorLog2 numerator denominator + exponent ≤ fmt.maxNormalExponent) (hunderflow : Numerics.RationalBinary.floorLog2 numerator denominator + exponent < fmt.minSubnormalExponent - 1) : roundRatScaled fmt false numerator denominator exponent = posZero fmt

Below half of the smallest subnormal, positive nearest-even packing returns positive zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_false_eq_subnormal (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hlow : fmt.minSubnormalExponent - 1 ≤ Numerics.RationalBinary.floorLog2 numerator denominator + exponent) (hhigh : Numerics.RationalBinary.floorLog2 numerator denominator + exponent < fmt.minNormalExponent) : roundRatScaled fmt false numerator denominator exponent = if Numerics.roundQuotientEven (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp)).1 (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp)).2 = 0 then posZero fmt else if pow2 fmt.fracWidth ≤ Numerics.roundQuotientEven (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp)).1 (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp)).2 then ofFields fmt false 1 0 else ofFields fmt false 0 (Numerics.roundQuotientEven (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp)).1 (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp)).2)

In the subnormal range, positive nearest-even packing rounds the quotient on the subnormal grid and promotes a full mantissa to the smallest normal value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_false_eq_normal_of_ne_carry (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hnormal : fmt.minNormalExponent ≤ Numerics.RationalBinary.floorLog2 numerator denominator + exponent) (hmax : Numerics.RationalBinary.floorLog2 numerator denominator + exponent ≤ fmt.maxNormalExponent) (hcarry : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - Numerics.RationalBinary.floorLog2 numerator denominator); Numerics.roundQuotientEven scaled.1 scaled.2 ≠ pow2 (fmt.fracWidth + 1)) : roundRatScaled fmt false numerator denominator exponent = ofFields fmt false (Numerics.RationalBinary.floorLog2 numerator denominator + exponent + Int.ofNat fmt.exponentBias).toNat (Numerics.roundQuotientEven (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - Numerics.RationalBinary.floorLog2 numerator denominator)).1 (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - Numerics.RationalBinary.floorLog2 numerator denominator)).2 - pow2 fmt.fracWidth)

In the normal range without a carry-out, positive nearest-even packing stores the rounded mantissa at the leading exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_false_eq_normal_of_carry (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hnormal : fmt.minNormalExponent ≤ Numerics.RationalBinary.floorLog2 numerator denominator + exponent) (hcarry : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - Numerics.RationalBinary.floorLog2 numerator denominator); Numerics.roundQuotientEven scaled.1 scaled.2 = pow2 (fmt.fracWidth + 1)) (hcarryMax : Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1 ≤ fmt.maxNormalExponent) : roundRatScaled fmt false numerator denominator exponent = ofFields fmt false (Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1 + Int.ofNat fmt.exponentBias).toNat 0

A carry-out whose incremented exponent still fits stores the smallest mantissa one binade higher.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatScaled_false_eq_posInf_of_carry (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hnormal : fmt.minNormalExponent ≤ Numerics.RationalBinary.floorLog2 numerator denominator + exponent) (hmax : Numerics.RationalBinary.floorLog2 numerator denominator + exponent ≤ fmt.maxNormalExponent) (hcarry : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - Numerics.RationalBinary.floorLog2 numerator denominator); Numerics.roundQuotientEven scaled.1 scaled.2 = pow2 (fmt.fracWidth + 1)) (hcarryOverflow : fmt.maxNormalExponent < Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1) : roundRatScaled fmt false numerator denominator exponent = posInf fmt

A carry-out past the largest normal exponent overflows to positive infinity.