Two-word fused multiply-add runtime

Normal inputs whose product and addend have the same sign and the supported alignment use a four-word exact sum and one nearest-even rounding step. The complete finite candidate chain then uses the width-generic exact kernel for other finite inputs. Correctness proofs live in Fma.Proof.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.alignFmaAddend (fmt : FloatFormat) (mantissa : Numerics.FixedWord.UInt128) : Numerics.FixedWord.UInt256

Shift a normal significand by fracWidth bits into the product's four-word coordinate.

@[inline]

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

Try the all-native same-sign, exactly aligned normal FMA path.

The sign test uses the public carrier's most-significant bit before native-word decoding, keeping declined opposite-sign cases cheap. The addend is accepted when its scale equals the product scale plus fracWidth, so both operands share the four-word coordinate of the product rounder.

@[specialize #[0]]

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

Evaluate finite two-word fused multiply-add.

The aligned fixed-limb kernel is attempted first. Every remaining finite case uses the generic one-rounding exact kernel; exceptional inputs are reported as none to the dispatcher. Descriptor specialization follows the pattern described in Dispatch.Add.Runtime.