TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Arithmetic.Word.Packed.SignedSum.Proof

Correctness of packed one-word Posit signed sums #

Scalar alignment and signed-magnitude arithmetic are used exactly when the intermediate fits one word. Capacity failures continue in the common proved two-limb engine. These theorems establish that every branch returns the same direct exact-dyadic code.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundWideFieldsWord_toNat (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : UInt64) (rightExponent : ℤ) :
(roundWideFieldsWord format heligible leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent).toNat = NativeWordRounding.GuardSticky.DyadicTarget.roundCodeNat format heligible (Numerics.Dyadic.addFields leftNegative leftSignificand.toNat leftExponent rightNegative rightSignificand.toNat rightExponent)

Continuing a one-word sum in the two-limb engine preserves the direct exact code.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundAlignedFieldsWord_toNat (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (rightNegative : Bool) (rightSignificand : UInt64) (exponent : ℤ) (hleft : leftSignificand ≠ 0) (hright : rightSignificand ≠ 0) :
(roundAlignedFieldsWord format heligible leftNegative leftSignificand rightNegative rightSignificand exponent).toNat = NativeWordRounding.GuardSticky.DyadicTarget.roundCodeNat format heligible (Numerics.Dyadic.addFields leftNegative leftSignificand.toNat exponent rightNegative rightSignificand.toNat exponent)

Scalar signed-magnitude accumulation rounds the exact aligned dyadic sum.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundFieldsWord_toNat (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : UInt64) (rightExponent : ℤ) :
(roundFieldsWord format heligible leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent).toNat = NativeWordRounding.GuardSticky.DyadicTarget.roundCodeNat format heligible (Numerics.Dyadic.addFields leftNegative leftSignificand.toNat leftExponent rightNegative rightSignificand.toNat rightExponent)

Scalar alignment and the two-limb continuation round the same exact dyadic sum.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.addWordsCodeWordValid_toNat {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
(addWordsCodeWordValid heligible left right hleft hright).toNat = addWordsCodeFlatValid heligible left right hleft hright

Packed native addition returns the flattened exact addition code.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.subWordsCodeWordValid_toNat {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
(subWordsCodeWordValid heligible left right hleft hright).toNat = subWordsCodeFlatValid heligible left right hleft hright

Packed native subtraction returns the flattened exact subtraction code.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundWideFmaFieldsWord_toNat (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : UInt64) (rightExponent : ℤ) (addendNegative : Bool) (addendSignificand : UInt64) (addendExponent : ℤ) :
(roundWideFmaFieldsWord format heligible leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent addendNegative addendSignificand addendExponent).toNat = NativeWordRounding.GuardSticky.DyadicTarget.roundCodeNat format heligible (Numerics.Dyadic.fmaFields leftNegative leftSignificand.toNat leftExponent rightNegative rightSignificand.toNat rightExponent addendNegative addendSignificand.toNat addendExponent)

Continuing a genuine two-limb product preserves the direct exact fused code.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundFmaFieldsWord_toNat (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : UInt64) (rightExponent : ℤ) (addendNegative : Bool) (addendSignificand : UInt64) (addendExponent : ℤ) :
(roundFmaFieldsWord format heligible leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent addendNegative addendSignificand addendExponent).toNat = NativeWordRounding.GuardSticky.DyadicTarget.roundCodeNat format heligible (Numerics.Dyadic.fmaFields leftNegative leftSignificand.toNat leftExponent rightNegative rightSignificand.toNat rightExponent addendNegative addendSignificand.toNat addendExponent)

Capacity-directed fused accumulation implements exact FMA.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.fmaWordsCodeWordValid_toNat {format : Format} (heligible : NativeWord.Eligible format) (left right addend : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) (haddend : addend.toNat < format.modulus) :
(fmaWordsCodeWordValid heligible left right addend hleft hright haddend).toNat = fmaWordsCodeFlatValid heligible left right addend hleft hright haddend

Packed native FMA returns the flattened exact fused code.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.addWordsCodeWordValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
(addWordsCodeWordValid heligible left right hleft hright).toNat < format.modulus

Every packed native addition result is a complete in-range Posit encoding.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.subWordsCodeWordValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
(subWordsCodeWordValid heligible left right hleft hright).toNat < format.modulus

Every packed native subtraction result is a complete in-range Posit encoding.

source
theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.fmaWordsCodeWordValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (left right addend : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) (haddend : addend.toNat < format.modulus) :
(fmaWordsCodeWordValid heligible left right addend hleft hright haddend).toNat < format.modulus

Every packed native FMA result is a complete in-range Posit encoding.