Width-generic wide-limb division

Finite inputs are decoded from their limb fields. Division uses one arbitrary-precision integer quotient, fusing significand scaling with the extra bit needed for nearest-even rounding. For normal operands, a significand comparison determines the ratio's leading exponent. Subnormal operands use the general leading-exponent computation and the same certified rounder.

The finite path includes zero operands, subnormal results, underflow, and overflow in every rounding direction. Only non-finite operands use the reference operation, whose value result does not depend on the rounding direction. Division.Proof proves the refinement through the codec.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.divisionMantissa {fmt : FloatFormat} (value : Value fmt) : ℕ

Integer significand read from a stored value, including subnormal and zero significands.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.divisionRatioExponent {fmt : FloatFormat} (x y : Value fmt) (num den : ℕ) : ℤ

The ratio exponent needs only a comparison when both significands are normalized.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.divFinite? (fmt : FloatFormat) (x y : Value fmt) (mode : IEEERoundingMode) : Option (Value fmt)

Try finite wide-limb division, in any rounding direction and without a precision bound.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.div (fmt : FloatFormat) (x y : Value fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : Value fmt

Total wide-limb division rounded in mode, nearest-even by default, with the reference exceptional-value policy. The configured wide-limb backend uses the default.