Correctness of normal finite quotient rounding

Optimized finite-division backends share normalSpec? as their natural-number normal-result specification. For conventional IEEE descriptors, normalSpec_eq_roundRatScaled_of_some proves agreement with exact nearest-even rational rounding when scaling the numerator requires a nonnegative left shift. That shift bound is a caller obligation, not a check made by normalSpec?.

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.normalSpec? (fmt : FloatFormat) (sign : Bool) (num den : ℕ) (exponent : ℤ) : Option (Model fmt)

Candidate specification for a normal finite quotient.

Zero inputs and exponents outside the supported normal range return none. Agreement with exact rational rounding requires fmt.isIEEE = true and RationalBinary.floorLog2 num den ≤ Int.ofNat fmt.fracWidth; the latter ensures that the numerator scaling is a left shift. Dispatchers use the complete rational implementation when a candidate declines.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteQuotientRound.normalSpec_eq_roundRatScaled_of_some (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (num den : ℕ) (exponent : ℤ) (result : Model fmt) (hshiftNonnegative : 0 ≤ Int.ofNat fmt.fracWidth - Numerics.RationalBinary.floorLog2 num den) (hresult : normalSpec? fmt sign num den exponent = some result) : result = roundRatScaled fmt sign num den exponent

When numerator scaling is a nonnegative left shift, a successful normal quotient agrees with conventional IEEE nearest-even rational rounding.