Direct packed-pair posit subtraction runtime #
Subtraction reverses the right operand's sign and uses the shared signed-sum kernel. Significands
stay in UInt128 when alignment and accumulation fit; larger intermediates use exact dyadic
arithmetic. The result is a two-limb code. Range and refinement proofs are in Sub.Proof.
@[noinline]
def
FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.subCode
{format : Format}
(heligible : NativeLimb.Eligible format)
(left right : Numerics.FixedWord.UInt128)
:
Decode two packed operands, subtract exactly, and return the complete two-limb encoding.