TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.FixedLimb.Pair.Multiplication.Runtime

Two-word multiplication runtime #

The partial four-limb product kernel multiplies normal operands in every eligible two-word layout. The operation dispatcher handles declined cases, and refinement proofs are in Multiplication.Proof.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.multiplyLimbs (x y : Numerics.FixedWord.UInt128) :
Numerics.FixedWord.UInt256

Multiply two two-word values into four limbs.

Keeping each column sum and carry as a native word avoids boxing the polymorphic AddResult values used by mul128. The four output words are those of mul128.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundProduct (value : Numerics.FixedWord.UInt256) (shift : ℕ) :
    Numerics.FixedWord.UInt128

    Round like UInt256.roundShiftRightEven128, keeping the increment and its carry as scalar words. The rounding contract needs 64 < shift < 128, but the function agrees with that kernel for every shift.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundNormalProductWords? (fmt : FloatFormat) (sign : Bool) (xExponent yExponent : UInt64) (product : Numerics.FixedWord.UInt256) (leading : UInt64) :
      Option Numerics.FixedWord.UInt128

      Round and pack a four-limb normal product whose leading set bit is at position leading, returning the two storage words of an accepted result.

      The product of two normal significands is rounded to fracWidth + 1 bits by shifting out leading - fracWidth bits with ties to even. A magnitude below the normal range, or a rounded result above the largest finite exponent, is declined.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundNormalProduct? {fmt : FloatFormat} (sign : Bool) (xExponent yExponent : UInt64) (product : Numerics.FixedWord.UInt256) (leading : UInt64) :
        Option (Model fmt)

        roundNormalProductWords? as a model value.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundNormalLimb? {fmt : FloatFormat} (sign : Bool) (xExponent yExponent : UInt64) (xMantissa yMantissa : Numerics.FixedWord.UInt128) :
          Option (Model fmt)

          Multiply two decoded normal significands in fixed limbs.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.mulNormalWords? (fmt : FloatFormat) (x y : Numerics.FixedWord.UInt128) :
            Option Numerics.FixedWord.UInt128

            Decode two values given by their storage words and try the fixed-limb normal product, returning the storage words of an accepted product. Two-word carriers call this form, so an accepted product never becomes a model value.

            Instances For
              source
              @[specialize #[0]]
              def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.mulNormalLimb? {fmt : FloatFormat} (x y : Model fmt) :
              Option (Model fmt)

              mulNormalWords? on the storage words of two model values, as a model value.

              Descriptor specialization follows the pattern described in Dispatch.Add.Runtime.

              Instances For