Direct packed-pair posit multiplication runtime #
The packed-pair multiplication kernel returns posit codes for configured values stored in two
native limbs. Range and semantic refinement proofs live in Mul.Proof.
@[noinline]
def
FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.mulCode
{format : Format}
(_heligible : NativeLimb.Eligible format)
(left right : Numerics.FixedWord.UInt128)
:
Decode two packed operands, multiply their significands in four native limbs, and return the complete result encoding in two native limbs.
The exact product is normalized with a sticky low bit before rounding. Significands, the product,
and the result code stay in fixed-width carriers; exponents and bit counts use Int and Nat.