TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.Full.Fma.Runtime

Native binary64 fused multiply-add runtime #

The accepted paths align finite normal operands in two native limbs and round the exact sum or difference once. Declined cases retain the generic exact finite kernel. Correctness proofs are isolated in Fma.Proof.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.alignFmaAddend (mantissa : UInt64) :
Numerics.FixedWord.UInt128

Shift a normal binary64 significand into the product's two-word coordinate.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaLeading (magnitude : Numerics.FixedWord.UInt128) :
    UInt64

    Leading-bit position of a binary64 FMA magnitude, which needs at most 107 bits.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaNormalSameSignAligned? (x y z : Value) :
      Option Value

      Try the aligned normal binary64 FMA path when the product and addend have the same sign.

      The accepted exact magnitude is xMantissa * yMantissa + zMantissa * 2^52. The final result is still rounded only once.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaNormalOppositeSignAligned? (x y z : Value) :
        Option Value

        Try the aligned normal binary64 FMA path when the product and addend have opposite signs.

        Exact cancellation and differences with leading-bit position below 53 are declined. The product rounder checks the result exponent; declined cases use the generic finite kernel.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.fmaFiniteFastImpl? (x y z : Value) :
          Option Value

          Use both native aligned paths before the existing exact finite FMA kernel.

          Instances For