TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Configured standard OCP MX destinations #

ExecFloat.OCP.MX.Standard profile is a constrained 32-lane destination on the common carrier. It is separate from the existing arbitrary-length raw block family. Conversion selects the recommended max-binade scale; explicit element SAT/OVF policy is the conversion context.

The generic exact domain is a vector of signed rationals. A stored block containing non-finite lanes has no value in that domain and is summarized as NaN. The lane-wise decode accessor retains all individual NaNs, infinities, and finite neighbors.

source
inductive FloatLib.Floats.ExecFloat.OCP.MX.Standard.Family (profile : Formats.OCP.MX.Standard.Profile) :
Type

Identity of a standard MX block with one of the six concrete element profiles.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.ExecFloat.OCP.MX.Standard.instEncodedFormatFamily (profile : Formats.OCP.MX.Standard.Profile) :
    Numerics.EncodedFormat (Family profile)
    source
    @[instance_reducible]
    instance FloatLib.Floats.ExecFloat.OCP.MX.Standard.instFormatSemanticsFamily (profile : Formats.OCP.MX.Standard.Profile) :
    Numerics.FormatSemantics (Family profile)
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.ExecFloat.OCP.MX.Standard (profile : Formats.OCP.MX.Standard.Profile) :
    Type

    One E8M0 scale and exactly 32 elements of a concrete OCP MX 1.0 profile.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.OCP.MX.Standard.ofCode {profile : Formats.OCP.MX.Standard.Profile} (block : Formats.OCP.MX.Standard.Block profile) :
      Standard profile

      Wrap a complete valid standard block without numerical conversion.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.OCP.MX.Standard.toCode {profile : Formats.OCP.MX.Standard.Profile} (value : Standard profile) :
        Formats.OCP.MX.Standard.Block profile

        Recover the complete scale and fixed-length element storage.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.ExecFloat.OCP.MX.Standard.decode {profile : Formats.OCP.MX.Standard.Profile} (value : Standard profile) :
          Vector (Numerics.NumericalValue Numerics.SignedRat) 32

          Exact lane-wise observation, retaining element-local non-finite values.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.ExecFloat.OCP.MX.Standard.quantize {profile : Formats.OCP.MX.Standard.Profile} (mode : Formats.OCP.MX.Standard.OverflowMode) (input : Vector Numerics.SignedRat 32) :
            Standard profile

            Direct quantization of finite exact inputs under the chosen FP8 overflow mode.

            Instances For
              source
              def FloatLib.Floats.ExecFloat.OCP.MX.Standard.Conversion.outsideFinite {profile : Formats.OCP.MX.Standard.Profile} (value : Numerics.SignedRat) :
              Bool

              Whether a normalized lane lies outside its signed finite endpoint. For these block conversions, range flags use the exact endpoint test, not the binary scalar after-rounding convention.

              Instances For
                source
                def FloatLib.Floats.ExecFloat.OCP.MX.Standard.Conversion.status {profile : Formats.OCP.MX.Standard.Profile} (input : Vector Numerics.SignedRat 32) (rounded : Standard profile) :
                ConversionStatus

                Conversion flags. overflow includes an unrepresentable shared scale or a normalized lane outside its exact finite range; saturated records such a lane stored at its finite endpoint. underflow records a nonzero input lane becoming zero. inexact compares complete signed finite observations, including zero signs.

                Instances For
                  source
                  def FloatLib.Floats.ExecFloat.OCP.MX.Standard.Conversion.run {profile : Formats.OCP.MX.Standard.Profile} (mode : Formats.OCP.MX.Standard.OverflowMode) :
                  Numerics.NumericalValue (Vector Numerics.SignedRat 32) → ConversionOutcome (Standard profile)

                  Convert one exact block observation, recording exceptional sources with a NaN scale.

                  Instances For
                    source
                    def FloatLib.Floats.ExecFloat.OCP.MX.Standard.Conversion.spec {profile : Formats.OCP.MX.Standard.Profile} (mode : Formats.OCP.MX.Standard.OverflowMode) (input : Numerics.NumericalValue (Vector Numerics.SignedRat 32)) (outcome : ConversionOutcome (Standard profile)) :
                    Prop

                    Destination specification uses the numerical lane-rounding relation at the selected scale.

                    Instances For
                      source
                      @[instance_reducible]
                      instance FloatLib.Floats.ExecFloat.OCP.MX.Standard.Conversion.exactDecoder {profile : Formats.OCP.MX.Standard.Profile} :
                      ExactDecoder (Standard profile) (Vector Numerics.SignedRat 32)

                      Finite block conversion exposes exact signed rationals through the shared source capability.