Two-word multiplication runtime

The partial four-limb product kernel multiplies normal operands in every eligible two-word layout. The operation dispatcher owns the exact baseline for declined cases. Refinement proofs are isolated in Multiplication.Proof.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundNormalProduct? {fmt : FloatFormat} (sign : Bool) (xExponent yExponent : UInt64) (product : Numerics.FixedWord.UInt256) (leading : UInt64) : Option (Model fmt)

Round and pack a four-limb normal product whose leading set bit is at position leading.

The product of two normal significands, or the aligned sum used by fused multiply-add, is rounded to fracWidth + 1 bits by shifting out leading - fracWidth bits with ties to even. A magnitude below the normal range, or a rounded result above the largest finite exponent, is declined.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundNormalLimb? {fmt : FloatFormat} (sign : Bool) (xExponent yExponent : UInt64) (xMantissa yMantissa : Numerics.FixedWord.UInt128) : Option (Model fmt)

Multiply two decoded normal significands in fixed limbs.

@[specialize #[0]]

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

Decode two values and try the fixed-limb normal product.

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