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 arbitrary-length raw block family. Conversion selects the recommended max-binade scale, and the 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 keeps every individual NaN, infinity, and finite neighbor.

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} (input : Vector Numerics.SignedRat 32) (overflow : Numerics.OverflowMode := Numerics.OverflowMode.saturate) :
            Standard profile

            Quantize finite exact inputs, saturating by default. (overflow := .native) selects the FP8 OVF element 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. Block conversions test range flags against the exact endpoint and do not follow the binary scalar convention of testing after rounding.

              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 covers an unrepresentable shared scale or a normalized lane outside its exact finite range, and 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} (overflow : Numerics.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} (overflow : Numerics.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.