Direct packed-pair posit addition runtime #
Addition uses the shared signed-sum kernel for posits stored in two native limbs. Significands
stay in UInt128 when alignment and addition fit; larger intermediates use exact dyadic
arithmetic. The result is a two-limb code. Range and refinement proofs are in Add.Proof.
@[noinline]
def
FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.addCode
{format : Format}
(heligible : NativeLimb.Eligible format)
(left right : Numerics.FixedWord.UInt128)
:
Decode two packed operands, add exactly, and return the complete two-limb encoding.