Two-word division runtime

A radix-2^32 quotient candidate is checked with an independent Euclidean certificate. A rejected candidate is replaced by the fixed-word restoring result, whose equality to the logical divider is proved in CertifiedDivision.Proof. The selected quotient and remainder are then rounded and packed. This module holds only the partial kernel for eligible two-word layouts, and the dispatcher handles every case outside its normal finite range.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.divNormalWords? (fmt : FloatFormat) (xWords yWords : Numerics.FixedWord.UInt128) : Option Numerics.FixedWord.UInt128

Try certified fixed-word division for two normal operands given by their storage words, returning the storage words of an accepted quotient. Two-word carriers call this form, so an accepted quotient never becomes a model value.

@[specialize #[0]]

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

divNormalWords? on the storage words of two model values, as a model value.

Descriptor specialization follows the pattern described in Dispatch.Add.Runtime.