Native one-word finite division

The native normal-division path serves conventional IEEE formats whose storage and quotient intermediates fit in UInt64. Refinement proofs and the exact-rational specification live in Div.Proof.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordDiv.roundNormalNative? (fmt : FloatFormat) (sign : Bool) (num den : UInt64) (exponent : ℤ) : Option (Model fmt)

Round and pack a normal quotient with UInt64 significands and an Int exponent.

For nonzero significands within the eligible format's width, the function declines if the leading exponent is outside the normal range before rounding or exceeds its upper bound after rounding. The public dispatcher handles these cases. The normal exponent bounds 1 - bias and bias and the encoding offset come from NativeSmallWord.biasInt, so the descriptor contributes no Nat power or shift per call.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordDiv.divNormal? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Decode two normal finite operands and try the one-word quotient path.

The function deliberately declines for zero, subnormal, and exceptional operands. The public dispatcher retains the exact arbitrary-precision implementation for every declined case.