TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.Runtime

Exact accumulation for standard MX dot products #

OCP's Microscaling Formats (MX) Specification, version 1.0, September 2023, §6.1 leaves internal precision and operation order implementation-defined. This implementation multiplies decoded lanes and accumulates in exact rational arithmetic. dotGeneral rounds once to IEEE binary32, after summing every block, as the scalar destination recommended by §6.2. The two operands may use different concrete element profiles.

Finite values outside binary32 range remain exact until the final rounding, consistently with the decoding choice permitted by §5.1. No lane product or partial block sum overflows or underflows. E8M0 exponents are bounded; accumulator growth depends on the number of blocks.

Exceptional arithmetic uses canonical NaN propagation, 0 * infinity = NaN, signed infinity products, and infinity + -infinity = NaN. The reduction starts at positive zero and uses increasing lane and block order. Every exact zero sum, including the empty dot, becomes positive zero; a negative nonzero sum that underflows retains its negative sign. NaN payloads and floating-point status flags are not returned by this value-only operation.

Reference: §§5.1, 6.1, and 6.2 of https://www.opencompute.org/documents/ocp-microscaling-formats-mx-v1-0-spec-final-pdf.

source
def FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.add :
Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact extended-rational addition with canonical NaN and opposite-infinity cancellation.

Instances For
    source
    def FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.mul :
    Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

    Exact products; a finite zero times either infinity is invalid.

    Instances For
      source
      def FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.sum (values : List (Numerics.NumericalValue ℚ)) :
      Numerics.NumericalValue ℚ

      Ordered exact reduction with a positive-zero identity.

      Instances For
        source
        def FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.roundFloat32 :
        Numerics.NumericalValue ℚ → BinaryInterchange.Model BinaryInterchange.FloatFormat.binary32

        One software nearest-even projection, with IEEE binary32 overflow and canonical specials.

        Instances For
          source
          def FloatLib.Floats.Formats.OCP.MX.Standard.dotExact {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) :
          Numerics.NumericalValue ℚ

          Exact §6.1 dot of two 32-lane blocks, possibly with different element profiles.

          Instances For
            source
            def FloatLib.Floats.Formats.OCP.MX.Standard.dot {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) :
            BinaryInterchange.Model BinaryInterchange.FloatFormat.binary32

            One block dot with a single binary32 destination rounding.

            Instances For
              source
              def FloatLib.Floats.Formats.OCP.MX.Standard.dotGeneralExact {leftProfile rightProfile : Profile} {n : ℕ} (left : Vector (Block leftProfile) n) (right : Vector (Block rightProfile) n) :
              Numerics.NumericalValue ℚ

              Exact sum of all block dots; no block result is rounded before this reduction.

              Instances For
                source
                def FloatLib.Floats.Formats.OCP.MX.Standard.dotGeneral {leftProfile rightProfile : Profile} {n : ℕ} (left : Vector (Block leftProfile) n) (right : Vector (Block rightProfile) n) :
                BinaryInterchange.Model BinaryInterchange.FloatFormat.binary32

                General §6.2 dot, rounded to binary32 once after exact accumulation across all blocks.

                Instances For