Native binary64 fused multiply-add runtime

The accepted paths align finite normal operands in two native limbs and round the sum or difference once. An addend whose scale is at most 62 bits above the product's is aligned exactly, and every other scale difference goes through a sticky bit. Declined cases use the generic exact finite kernel. Fma.Proof has the proofs.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.alignFmaAddend (mantissa : UInt64) (shift : ℕ) : Numerics.FixedWord.UInt128

Shift a normal binary64 significand left by shift bits into the product's two-word coordinate, where shift is the addend's scale above the product's.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaLeading (magnitude : Numerics.FixedWord.UInt128) : UInt64

Leading-bit position of a binary64 FMA magnitude, which needs at most 116 bits.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaNormalSameSignWord? (xBits yBits zBits : UInt64) : Option UInt64

Try the normal binary64 FMA path when the product and addend have the same sign and the addend's scale is at most 62 bits above the product's, on storage words.

The accepted magnitude xMantissa * yMantissa + zMantissa * 2^shift is exact and below 2^116, so the result is rounded once.

@[inline]

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

fmaNormalSameSignWord? as a model value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaNormalOppositeSignWord? (xBits yBits zBits : UInt64) : Option UInt64

Try the normal binary64 FMA path when the product and addend have opposite signs and the addend's scale is at most 62 bits above the product's, on storage words.

It declines exact cancellation and differences whose leading bit is below position 53. The product rounder checks the result exponent, and declined cases use the generic finite kernel.

@[inline]

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

fmaNormalOppositeSignWord? as a model value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaJammedWord? (xBits yBits zBits : UInt64) : Option UInt64

Normal binary64 FMA for addends outside the exact window, on storage words.

An addend whose scale is gap positions below the product's is shifted right with a sticky bit into the product's coordinate. An addend more than 62 positions above keeps three guard positions, and the product is shifted right with a sticky bit below them. Either way the sticky magnitude rounds like the exact sum, because the dominant operand leaves more than fracWidth + 2 bits above the discarded positions.

@[inline]

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

fmaJammedWord? as a model value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaNormalWord? (xBits yBits zBits : UInt64) : Option UInt64

Native normal binary64 FMA on storage words, trying the same-sign, opposite-sign and sticky paths in turn. Carriers that store binary64 as a UInt64 call this word form.

@[inline]

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

fmaNormalWord? as a model value.

@[inline]

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

Finite binary64 FMA through the native normal paths, falling back to fmaFiniteComponents?.