Branch equations for directed rational packing #
roundRatMagnitudeDirectedScaled checks the denominator and zero before choosing an overflow,
underflow, subnormal, normal, or carry-out result. The equations below isolate its
positive-magnitude branches for the directed bound proofs. Sign restoration is proved separately.
Positive packing branches #
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_eq
(fmt : FloatFormat)
(roundUp : Bool)
(numerator denominator : ℕ)
(exponent : ℤ)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
:
roundRatMagnitudeDirectedScaled fmt roundUp false numerator denominator exponent = have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator;
have totalExponent := rationalExponent + exponent;
if fmt.maxNormalExponent < totalExponent then directedOverflow fmt false roundUp
else if totalExponent < fmt.minSubnormalExponent then if roundUp = true then posMinSubnormal fmt else zero fmt false
else if totalExponent < fmt.minNormalExponent then
have scaled :=
Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp);
have rounded := roundQuotDirected roundUp scaled.1 scaled.2;
if rounded = 0 then zero fmt false
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 := roundQuotDirected roundUp scaled.1 scaled.2;
have normalizedExponent := if rounded = pow2 (fmt.fracWidth + 1) then totalExponent + 1 else totalExponent;
have normalizedMantissa := if rounded = pow2 (fmt.fracWidth + 1) then pow2 fmt.fracWidth else rounded;
have encodedExponent := (normalizedExponent + Int.ofNat fmt.exponentBias).toNat;
have fraction := normalizedMantissa - pow2 fmt.fracWidth;
if fmt.maxNormalExponent < normalizedExponent then directedOverflow fmt false roundUp
else if (decide (encodedExponent > fmt.maxFiniteExpField) || encodedExponent == fmt.maxFiniteExpField && decide (fraction > fmt.maxFiniteFracField)) = true then
directedOverflow fmt false roundUp
else ofFields fmt false encodedExponent fraction
Positive directed packing of a nonzero rational, exposing the exponent, significand, and finite-field guards.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_eq_overflow
(fmt : FloatFormat)
(roundUp : Bool)
(numerator denominator : ℕ)
(exponent : ℤ)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
(hoverflow : fmt.maxNormalExponent < Numerics.RationalBinary.floorLog2 numerator denominator + exponent)
:
roundRatMagnitudeDirectedScaled fmt roundUp false numerator denominator exponent = directedOverflow fmt false roundUp
Above the largest normal exponent, positive directed packing returns the directed overflow result.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_eq_underflow
(fmt : FloatFormat)
(roundUp : Bool)
(numerator denominator : ℕ)
(exponent : ℤ)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
(hmax : Numerics.RationalBinary.floorLog2 numerator denominator + exponent ≤ fmt.maxNormalExponent)
(hunderflow : Numerics.RationalBinary.floorLog2 numerator denominator + exponent < fmt.minSubnormalExponent)
:
Below the smallest subnormal exponent, positive directed packing returns the smallest subnormal when rounding up and zero when rounding down.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_eq_subnormal_down
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
(hmax : Numerics.RationalBinary.floorLog2 numerator denominator + exponent ≤ fmt.maxNormalExponent)
(hlow : fmt.minSubnormalExponent ≤ Numerics.RationalBinary.floorLog2 numerator denominator + exponent)
(hhigh : Numerics.RationalBinary.floorLog2 numerator denominator + exponent < fmt.minNormalExponent)
:
have scaled :=
Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp);
have rounded := roundQuotDirected false scaled.1 scaled.2;
roundRatMagnitudeDirectedScaled fmt false false numerator denominator exponent = ofFields fmt false 0 rounded
In the subnormal range, positive downward packing stores the truncated quotient as a subnormal.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_eq_subnormal_up
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(hnumerator : numerator ≠ 0)
(hdenominator : denominator ≠ 0)
(hmax : Numerics.RationalBinary.floorLog2 numerator denominator + exponent ≤ fmt.maxNormalExponent)
(hlow : fmt.minSubnormalExponent ≤ Numerics.RationalBinary.floorLog2 numerator denominator + exponent)
(hhigh : Numerics.RationalBinary.floorLog2 numerator denominator + exponent < fmt.minNormalExponent)
:
have scaled :=
Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp);
have rounded := roundQuotDirected true scaled.1 scaled.2;
roundRatMagnitudeDirectedScaled fmt true false numerator denominator exponent = if pow2 fmt.fracWidth ≤ rounded then ofFields fmt false 1 0 else ofFields fmt false 0 rounded
In the subnormal range, positive upward packing stores the ceiling quotient as a subnormal, or the smallest normal value when the quotient fills the mantissa.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_eq_normal_down
(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)
:
have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator;
have totalExponent := rationalExponent + exponent;
have scaled :=
Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent);
have rounded := roundQuotDirected false scaled.1 scaled.2;
roundRatMagnitudeDirectedScaled fmt false false numerator denominator exponent = ofFields fmt false (totalExponent + Int.ofNat fmt.exponentBias).toNat (rounded - pow2 fmt.fracWidth)
In the normal range of an IEEE descriptor, positive downward packing stores the truncated mantissa at the leading exponent.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_eq_normal_up_no_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 rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator;
have scaled :=
Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent);
roundQuotDirected true scaled.1 scaled.2 ≠ pow2 (fmt.fracWidth + 1))
:
have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator;
have totalExponent := rationalExponent + exponent;
have scaled :=
Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent);
have rounded := roundQuotDirected true scaled.1 scaled.2;
roundRatMagnitudeDirectedScaled fmt true false numerator denominator exponent = ofFields fmt false (totalExponent + Int.ofNat fmt.exponentBias).toNat (rounded - pow2 fmt.fracWidth)
In the normal range of an IEEE descriptor, upward packing without a carry stores the ceiling mantissa at the leading exponent.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatMagnitudeDirectedScaled_pos_eq_normal_up_carry
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(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 rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator;
have scaled :=
Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent);
roundQuotDirected true scaled.1 scaled.2 = pow2 (fmt.fracWidth + 1))
(hcarryMax : Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1 ≤ fmt.maxNormalExponent)
:
roundRatMagnitudeDirectedScaled fmt true 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.roundRatMagnitudeDirectedScaled_pos_eq_normal_up_carry_overflow
(fmt : FloatFormat)
(numerator denominator : ℕ)
(exponent : ℤ)
(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 rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator;
have scaled :=
Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent);
roundQuotDirected true scaled.1 scaled.2 = pow2 (fmt.fracWidth + 1))
(hcarryOverflow : fmt.maxNormalExponent < Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1)
:
roundRatMagnitudeDirectedScaled fmt true false numerator denominator exponent = directedOverflow fmt false true
A carry-out past the largest normal exponent returns the directed overflow result.