Grid bounds for directed rational packing

The executable packer rescales a rational to the subnormal or normal grid, then rounds its quotient to an integer. Rescaling by a power of two and restoring that scale preserves the exact value. The bounds below describe the scaled quotient and its floor and ceiling.

Packing.Branches identifies the corresponding executable branches. Packing.Downward and Packing.Upward use these inequalities to bound the packed results.

Exact scale changes and integer bounds

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.subnormalAlignExp_add_minSubnormalExponent (fmt : FloatFormat) : Int.ofNat fmt.subnormalAlignExp + fmt.minSubnormalExponent = 0

The subnormal alignment shift is the negation of the smallest subnormal exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledRatToReal_subnormal_grid (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) : scaledRatToReal numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp) * bpow fmt.minSubnormalExponent = scaledRatToReal numerator denominator exponent

Rescaling onto the subnormal grid and back is the identity on the exact rational value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledRatToReal_normal_grid (fmt : FloatFormat) (numerator denominator : ℕ) (rationalExponent exponent : ℤ) : scaledRatToReal numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent) * bpow (rationalExponent + exponent - Int.ofNat fmt.fracWidth) = scaledRatToReal numerator denominator exponent

Rescaling onto the normal grid at a leading exponent and back is the identity on the exact rational value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleByPowerOfTwo_normal_bounds (fmt : FloatFormat) (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent); ↑(pow2 fmt.fracWidth) ≤ ↑scaled.1 / ↑scaled.2 ∧ ↑scaled.1 / ↑scaled.2 < ↑(pow2 (fmt.fracWidth + 1))

The quotient scaled to the normal grid lies in the normalized mantissa interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleByPowerOfTwo_subnormal_bounds (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (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); 1 ≤ ↑scaled.1 / ↑scaled.2 ∧ ↑scaled.1 / ↑scaled.2 < ↑(pow2 fmt.fracWidth)

In the subnormal range, the quotient scaled to the subnormal grid lies in [1, 2 ^ fracWidth).

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_normal_bounds (fmt : FloatFormat) (roundUp : Bool) (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent); pow2 fmt.fracWidth ≤ roundQuotDirected roundUp scaled.1 scaled.2 ∧ roundQuotDirected roundUp scaled.1 scaled.2 ≤ pow2 (fmt.fracWidth + 1)

Directed rounding on the normal grid stays within the closed normalized mantissa interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_subnormal_bounds (fmt : FloatFormat) (roundUp : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (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); 1 ≤ roundQuotDirected roundUp scaled.1 scaled.2 ∧ roundQuotDirected roundUp scaled.1 scaled.2 ≤ pow2 fmt.fracWidth

In the subnormal range, directed rounding on the subnormal grid lies in [1, 2 ^ fracWidth].

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_false_subnormal_lt_pow2 (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (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); roundQuotDirected false scaled.1 scaled.2 < pow2 fmt.fracWidth

Downward rounding on the subnormal grid stays strictly below the smallest normal mantissa.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_false_normal_lt_pow2_succ (fmt : FloatFormat) (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent); roundQuotDirected false scaled.1 scaled.2 < pow2 (fmt.fracWidth + 1)

Downward rounding on the normal grid never carries out of the normalized mantissa interval.

Exact real bounds on the packing grids

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_false_subnormal_value_le (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hdenominator : denominator ≠ 0) : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp); ↑(roundQuotDirected false scaled.1 scaled.2) * bpow fmt.minSubnormalExponent ≤ scaledRatToReal numerator denominator exponent

Downward quotient rounding on the subnormal grid lies below the exact scaled rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_roundQuotDirected_true_subnormal_value (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hdenominator : denominator ≠ 0) : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (exponent + Int.ofNat fmt.subnormalAlignExp); scaledRatToReal numerator denominator exponent ≤ ↑(roundQuotDirected true scaled.1 scaled.2) * bpow fmt.minSubnormalExponent

The exact scaled rational lies below upward quotient rounding on the subnormal grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected_false_normal_value_le (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hdenominator : denominator ≠ 0) : have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent); ↑(roundQuotDirected false scaled.1 scaled.2) * bpow (rationalExponent + exponent - Int.ofNat fmt.fracWidth) ≤ scaledRatToReal numerator denominator exponent

Downward quotient rounding on the normal grid lies below the exact scaled rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_roundQuotDirected_true_normal_value (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hdenominator : denominator ≠ 0) : have rationalExponent := Numerics.RationalBinary.floorLog2 numerator denominator; have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator (Int.ofNat fmt.fracWidth - rationalExponent); scaledRatToReal numerator denominator exponent ≤ ↑(roundQuotDirected true scaled.1 scaled.2) * bpow (rationalExponent + exponent - Int.ofNat fmt.fracWidth)

The exact scaled rational lies below upward quotient rounding on the normal grid.