TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E8M0.Block

Block-scaled numerical systems #

Microscaling formats store one E8M0 scale beside a block of low-precision element codes. The block is therefore the numerical code: an element word by itself does not carry its complete magnitude. This module exposes that joint representation through NumericalSystem and interprets successful decoding as an array of exact dyadic values.

source
structure FloatLib.Floats.Formats.OCP.MX.BlockCode (fmt : BinaryInterchange.FloatFormat) :
Type

One shared E8M0 scale and its policy-aware element codes.

  • scale : E8M0

    Shared E8M0 exponent code for the complete block.

  • values : Array (BinaryInterchange.Model fmt)

    Element codes interpreted relative to the shared scale.

Instances For
    source
    def FloatLib.Floats.Formats.OCP.MX.instDecidableEqBlockCode.decEq {fmt✝ : BinaryInterchange.FloatFormat} (x✝ x✝¹ : BlockCode fmt✝) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.OCP.MX.instDecidableEqBlockCode {fmt✝ : BinaryInterchange.FloatFormat} :
      DecidableEq (BlockCode fmt✝)
      source
      def FloatLib.Floats.Formats.OCP.MX.instReprBlockCode.repr {fmt✝ : BinaryInterchange.FloatFormat} :
      BlockCode fmt✝ → ℕ → Std.Format
      Instances For
        source
        @[instance_reducible]
        instance FloatLib.Floats.Formats.OCP.MX.instReprBlockCode {fmt✝ : BinaryInterchange.FloatFormat} :
        Repr (BlockCode fmt✝)
        source
        @[inline]
        def FloatLib.Floats.Formats.OCP.MX.BlockCode.decode? {fmt : BinaryInterchange.FloatFormat} (block : BlockCode fmt) :
        Option (Array Numerics.Dyadic)

        Decode the jointly stored scale and element words.

        Instances For
          source
          def FloatLib.Floats.Formats.OCP.MX.blockSystem (fmt : BinaryInterchange.FloatFormat) :
          Numerics.NumericalSystem

          Exact semantics of an E8M0-scaled block.

          Instances For
            source
            theorem FloatLib.Floats.Formats.OCP.MX.blockSystem_represents_iff {fmt : BinaryInterchange.FloatFormat} (block : BlockCode fmt) (values : Array Numerics.Dyadic) :
            (blockSystem fmt).Represents block values ↔ block.decode? = some values

            A block represents an exact dyadic array precisely when its joint decoder succeeds.

            source
            @[reducible, inline]
            abbrev FloatLib.Floats.Formats.OCP.MX.BlockAtFinite (fmt : BinaryInterchange.FloatFormat) (values : Array Numerics.Dyadic) :
            Type

            A successfully decoded block with an erased proof of its exact dyadic array.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.OCP.MX.BlockCode.atFinite {fmt : BinaryInterchange.FloatFormat} {values : Array Numerics.Dyadic} (block : BlockCode fmt) (hdecode : block.decode? = some values) :
              BlockAtFinite fmt values

              Attach a successful joint-decoding proof to a block code.

              Instances For
                source
                theorem FloatLib.Floats.Formats.OCP.MX.BlockCode.decode_refines (fmt : BinaryInterchange.FloatFormat) :
                Numerics.Operation.Checked1 (blockSystem fmt) (Numerics.NumericalSystem.exact (Array Numerics.Dyadic)) decode? fun (values : (blockSystem fmt).Scalar) => Numerics.NumericalValue.finite values

                Joint block decoding is a checked exact operation.