Correctness of packed two-limb Posit sums

Native decoding, alignment, signed-magnitude accumulation, and rounding implement exact dyadic addition and subtraction. The capacity branch is used only when an aligned intermediate genuinely exceeds two limbs; it shares the same exact semantics.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.SignedSum.roundCapacityFieldsWord_toNat (format : Format) (heligible : NativeLimb.Eligible format) (leftNegative : Bool) (leftSignificand : Numerics.FixedWord.UInt128) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : Numerics.FixedWord.UInt128) (rightExponent : ℤ) : (roundCapacityFieldsWord format heligible leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent).toNat = NativeLimbRounding.roundCodeNat format heligible (Numerics.Dyadic.addFields leftNegative leftSignificand.toNat leftExponent rightNegative rightSignificand.toNat rightExponent)

Converting an exact capacity result back to two limbs preserves its complete code.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.SignedSum.roundAlignedFieldsWord_toNat (format : Format) (heligible : NativeLimb.Eligible format) (leftNegative : Bool) (leftSignificand : Numerics.FixedWord.UInt128) (rightNegative : Bool) (rightSignificand : Numerics.FixedWord.UInt128) (exponent : ℤ) (hleft : leftSignificand.toNat ≠ 0) (hright : rightSignificand.toNat ≠ 0) : (roundAlignedFieldsWord format heligible leftNegative leftSignificand rightNegative rightSignificand exponent).toNat = NativeLimbRounding.roundCodeNat format heligible (Numerics.Dyadic.addFields leftNegative leftSignificand.toNat exponent rightNegative rightSignificand.toNat exponent)

The aligned two-limb signed-magnitude kernel rounds the exact common-exponent sum.

The caller handles zero operands before alignment. Same-sign overflow is the only branch whose exact magnitude can require more than 128 bits.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.SignedSum.roundFieldsWord_toNat (format : Format) (heligible : NativeLimb.Eligible format) (leftNegative : Bool) (leftSignificand : Numerics.FixedWord.UInt128) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : Numerics.FixedWord.UInt128) (rightExponent : ℤ) : (roundFieldsWord format heligible leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent).toNat = NativeLimbRounding.roundCodeNat format heligible (Numerics.Dyadic.addFields leftNegative leftSignificand.toNat leftExponent rightNegative rightSignificand.toNat rightExponent)

Native exponent alignment and its exact capacity branch round the same dyadic sum.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.SignedSum.addWordsCodeWord_toNat {format : Format} (heligible : NativeLimb.Eligible format) (left right : Numerics.FixedWord.UInt128) : (addWordsCodeWord heligible left right).toNat = Boundary.binaryCode format.signMaskNat (fun (leftValue rightValue : Numerics.Dyadic) => NativeLimbRounding.roundCodeNat format heligible (leftValue.add rightValue)) (NativeLimb.toDyadic? format left) (NativeLimb.toDyadic? format right)

Packed two-limb addition returns the exact complete Posit code.

theorem FloatLib.Floats.Formats.Posit.Model.NativeLimbPacked.SignedSum.subWordsCodeWord_toNat {format : Format} (heligible : NativeLimb.Eligible format) (left right : Numerics.FixedWord.UInt128) : (subWordsCodeWord heligible left right).toNat = Boundary.binaryCode format.signMaskNat (fun (leftValue rightValue : Numerics.Dyadic) => NativeLimbRounding.roundCodeNat format heligible (leftValue.sub rightValue)) (NativeLimb.toDyadic? format left) (NativeLimb.toDyadic? format right)

Packed two-limb subtraction returns the exact complete Posit code.