TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Packed one-word Posit signed sums #

The two-limb signed-sum engine is the common fixed-carrier implementation. One-word decoded significands first use scalar alignment and signed-magnitude arithmetic whenever the exact intermediate fits one word. Exact capacity failures continue in the same common two-limb engine, which uses exact dyadic arithmetic if two limbs are insufficient. Eligible one-word formats retain the complete result in its low output limb.

Fused multiply-add uses the same rule: FixedWord.mul64 computes the exact product, a one-limb product reuses scalar signed addition, and a genuine two-limb product enters the common engine. Every branch is selected by exact carrier capacity rather than a named format or tuned width.

source
@[noinline]
def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundWideFieldsWord (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : UInt64) (rightExponent : ℤ) :
UInt64

Continue an exact one-word signed sum in the common two-limb carrier.

Instances For
    source
    @[noinline]
    def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundAlignedFieldsWord (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (rightNegative : Bool) (rightSignificand : UInt64) (exponent : ℤ) :
    UInt64

    Round two nonzero signed magnitudes already aligned at one exponent.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundFieldsWord (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : UInt64) (rightExponent : ℤ) :
      UInt64

      Round the exact sum of two decoded one-word Posit dyadics.

      Zero operands bypass alignment. Otherwise the larger-exponent significand is shifted exactly when it remains in one word. A failed scalar capacity check continues in roundWideFieldsWord.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.addWordsCodeWordValid {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
        UInt64

        Add two proved-valid packed Posit words and retain the complete result in UInt64.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.subWordsCodeWordValid {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
          UInt64

          Subtract two proved-valid packed words by reversing the right decoded sign.

          Instances For
            source
            @[noinline]
            def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundWideFmaFieldsWord (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : UInt64) (rightExponent : ℤ) (addendNegative : Bool) (addendSignificand : UInt64) (addendExponent : ℤ) :
            UInt64

            Continue a genuine two-limb fused product in the common signed-sum engine.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.roundFmaFieldsWord (format : Format) (heligible : NativeWord.Eligible format) (leftNegative : Bool) (leftSignificand : UInt64) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : UInt64) (rightExponent : ℤ) (addendNegative : Bool) (addendSignificand : UInt64) (addendExponent : ℤ) :
              UInt64

              Round an exact fused product and addend.

              A product fitting one word reuses the scalar signed-sum kernel. Otherwise the exact UInt128 product enters the common two-limb engine, including its exact-arithmetic capacity fallback.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedSignedSum.fmaWordsCodeWordValid {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) :
                UInt64

                Fused multiply-add for three proved-valid packed words, with a word-valued result.

                Instances For