Two-limb posit arithmetic runtime

These kernels decode each finite operand once, perform the exact dyadic operation, and use the two-limb rounding backends through Posit128. Division reuses the shared width-generic quotient-prefix kernel through divWords. The packed square-root adapter likewise reuses the width-generic root-prefix kernel.

Refinement to the representation-independent Posit Standard operations lives in Arithmetic.Proof.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimbArithmetic.add {format : Format} (heligible : NativeLimb.Eligible format) (left right : Model format) : Model format

Exact dyadic addition followed by certified two-limb standard rounding.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimbArithmetic.sub {format : Format} (heligible : NativeLimb.Eligible format) (left right : Model format) : Model format

Exact dyadic subtraction followed by certified two-limb standard rounding.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimbArithmetic.mul {format : Format} (heligible : NativeLimb.Eligible format) (left right : Model format) : Model format

Exact dyadic multiplication followed by certified two-limb standard rounding.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimbArithmetic.divWords (format : Format) (left right : Numerics.FixedWord.UInt128) : Model format

Decode two stored pair words and divide them with the shared width-generic quotient-prefix kernel.

This function is a carrier adapter, not a separate fixed-limb divider.

@[noinline]

def FloatLib.Floats.Formats.Posit.Model.NativeLimbArithmetic.fma {format : Format} (heligible : NativeLimb.Eligible format) (left right addend : Model format) : Model format

Exact fused multiplication and addition with one certified two-limb rounding step.