Shared bounds for native-word quotient kernels

The one-word and binary64 division backends use different packing code, but they normalize the same exact rational quotient. This module proves the representation-independent facts once:

• the normalization shift is nonnegative,
• the rounded significand lies in [2^fracWidth, 2^(fracWidth + 1)], and
• the restoring quotient and its carry bit fit in the UInt64 kernel.

The shift and significand bounds precede the representation-specific estimates. A direct shifted numerator fits below bit 63 when 2 * (fracWidth + 1) ≤ 63; the quotient and a possible rounding increment fit below bit 63 under the weaker condition fracWidth ≤ 61.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeWordQuotient.normalShift_eq (fmt : FloatFormat) (num den : UInt64) (hnum : num ≠ 0) (hnumFit : num.toNat < 2 ^ (fmt.fracWidth + 1)) : have rationalExponent := Numerics.FixedWord.RestoringQuotient.floorLog2RatWord num den; have shift := (Int.ofNat fmt.fracWidth - rationalExponent).toNat; Int.ofNat shift = Int.ofNat fmt.fracWidth - rationalExponent

The normalizing shift computed by the native kernel is the corresponding integer difference.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeWordQuotient.normalShift_bounds (fmt : FloatFormat) (num den : UInt64) (hnum : num ≠ 0) (hden : den ≠ 0) (hnumFit : num.toNat < 2 ^ (fmt.fracWidth + 1)) (hdenFit : den.toNat < 2 ^ (fmt.fracWidth + 1)) (hbudget : 2 * (fmt.fracWidth + 1) ≤ 63) : have rationalExponent := Numerics.FixedWord.RestoringQuotient.floorLog2RatWord num den; have shift := (Int.ofNat fmt.fracWidth - rationalExponent).toNat; shift < 64 ∧ num.toNat <<< shift < 2 ^ 63

The normalized numerator and its shift fit the signed-width budget used by the UInt64 quotient kernel.

The condition 2 * (fracWidth + 1) ≤ 63 is the representation boundary for this direct shifted numerator path. It is satisfied by binary32 and other narrow formats; wider one-word formats use the restoring loop without first materializing the whole shifted numerator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeWordQuotient.roundedMantissa_bounds (fmt : FloatFormat) (num den : UInt64) (hnum : num ≠ 0) (hden : den ≠ 0) (hnumFit : num.toNat < 2 ^ (fmt.fracWidth + 1)) : have rationalExponent := Numerics.FixedWord.RestoringQuotient.floorLog2RatWord num den; have shift := (Int.ofNat fmt.fracWidth - rationalExponent).toNat; 2 ^ fmt.fracWidth ≤ Numerics.roundQuotientEven (num.toNat <<< shift) den.toNat ∧ Numerics.roundQuotientEven (num.toNat <<< shift) den.toNat ≤ 2 ^ (fmt.fracWidth + 1)

Normalized nearest-even quotient rounding stays within the expected significand interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeWordQuotient.quotient_lt_two_pow_63 (fmt : FloatFormat) (num den : UInt64) (hnum : num ≠ 0) (hden : den ≠ 0) (hnumFit : num.toNat < 2 ^ (fmt.fracWidth + 1)) (hfracWidth : fmt.fracWidth ≤ 61) : have rationalExponent := Numerics.FixedWord.RestoringQuotient.floorLog2RatWord num den; have shift := (Int.ofNat fmt.fracWidth - rationalExponent).toNat; num.toNat <<< shift / den.toNat + 1 < 2 ^ 63

The restoring quotient and a possible rounding increment fit below bit 63.

The bound fracWidth ≤ 61 leaves room for a significand carry and a possible rounding increment without using bit 63.