Direct packed-pair posit fused multiply-add runtime #
The packed-pair fused multiply-add kernel returns posit codes for configured values stored in
two native limbs. Range and semantic refinement proofs live in Fma.Proof.
@[noinline]
def
FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.fmaCode
{format : Format}
(heligible : NativeLimb.Eligible format)
(left right addend : Numerics.FixedWord.UInt128)
:
Decode three operands, form the exact product in four native limbs, add without intermediate rounding, and return the result code.
The product crosses to the shared arbitrary-precision sum only once. This avoids allocating two input dyadics and avoids generic big-integer multiplication.