Native-word fused multiply-add for generic binary32

The fast path combines a product of at most 48 bits with the addend in one UInt64 when the alignment allows it. A same-sign addend dominating the product by more than 48 scale bits is returned unchanged, and other large gaps with a large enough dominant operand shift the smaller one right with a sticky bit. Remaining gaps use exact dyadic alignment, which preserves tie-breaking. NaN and infinity handling stays outside this module, and Fma.Proof has the proofs.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fmaFinite? (x y z : Value) : Option Value

Finite binary32 fused multiply-add through exact dyadic coordinates.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fmaExactFinite? (productSign zSign : Bool) (product productScale zMantissa zProductScale : UInt64) : Option Value

Exact finite binary32 FMA on components the native kernel has already decoded.

It handles any alignment gap without a second decode or significand product.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.isExactShift (value shift : UInt64) : Bool

Whether shift < 64 and value >>> shift discards no set bit. A native shift reduces its count modulo 64, so a count of 64 or more is never an exact shift.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fmaFiniteWord? (x y z : Value) : Option Value

Machine-word implementation of finite binary32 fused multiply-add.

The exact product has at most 48 bits. When the aligned operands also fit in one UInt64, the product and addend are combined without building dyadics. An addend dominating a same-sign product by more than 48 scale bits is returned unchanged. Larger gaps keep three guard bits of a normal addend, or the whole product when it is at least 2^46, and shift the other operand right with a sticky bit, which rounds like the exact sum. Remaining gaps use the exact path fmaExactFinite?.