TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E8M0.Core

Exponent-only scaling formats #

OCP microscaling uses E8M0 for a scale shared by a block of narrow elements. E8M0 is not a member of the sign/exponent/fraction family: it has no sign bit, no zero, and no explicit fraction. Codes 0 through 254 denote powers of two from 2^-127 through 2^127; code 255 is NaN.

Keeping this scale type beside, rather than inside, FloatFormat prevents artificial optional fields and invalid combinations in the ordinary float API.

References:

source
def FloatLib.Floats.Formats.OCP.MX.E8M0 :
Type

Exact E8M0 storage word.

The transparent definition has the same compiled representation as BitVec 8, while retaining the exponent-only format identity for proof-aware type inspection.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.OCP.MX.instReprE8M0 :
    Repr E8M0
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.OCP.MX.instBEqE8M0 :
    BEq E8M0
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.OCP.MX.instDecidableEqE8M0 :
    DecidableEq E8M0
    source
    def FloatLib.Floats.Formats.OCP.MX.E8M0.bias :
    ℤ

    E8M0 exponent bias.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.OCP.MX.E8M0.ofNatBits (bits : ℕ) :
      E8M0

      Construct an E8M0 word from its raw code.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.OCP.MX.E8M0.toNatBits (x : E8M0) :
        ℕ

        Raw code as a natural number.

        Instances For
          source
          @[simp]
          theorem FloatLib.Floats.Formats.OCP.MX.E8M0.ofNatBits_toNatBits (value : E8M0) :
          ofNatBits value.toNatBits = value

          Re-encoding an E8M0 word's complete byte pattern preserves it.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.OCP.MX.E8M0.toNatBits_ofNatBits_of_lt (bits : ℕ) (bits_lt : bits < 2 ^ 8) :
          (ofNatBits bits).toNatBits = bits

          An in-range byte pattern is unchanged by E8M0 encoding.

          source
          @[inline]
          def FloatLib.Floats.Formats.OCP.MX.E8M0.isNaN (x : E8M0) :
          Bool

          The sole NaN encoding (0xff).

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.OCP.MX.E8M0.exponent? (x : E8M0) :
            Option ℤ

            Unbiased power-of-two exponent, or none for NaN.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.OCP.MX.E8M0.toDyadic? (x : E8M0) :
              Option Numerics.Dyadic

              Exact positive dyadic scale, or none for NaN.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.OCP.MX.E8M0.scaleDyadic? (scale : E8M0) (value : Numerics.Dyadic) :
                Option Numerics.Dyadic

                Apply an E8M0 scale to an exact dyadic by adding its power-of-two exponent.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.OCP.MX.E8M0.decodeElement? {fmt : BinaryInterchange.FloatFormat} (scale : E8M0) (x : BinaryInterchange.Model fmt) :
                  Option Numerics.Dyadic

                  Decode and scale one element of a microscaling block.

                  none records either the E8M0 NaN code or a non-finite element. The operation is exact: scaling by a power of two changes only the dyadic exponent.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.OCP.MX.E8M0.decodeBlock? {fmt : BinaryInterchange.FloatFormat} (scale : E8M0) (values : Array (BinaryInterchange.Model fmt)) :
                    Option (Array Numerics.Dyadic)

                    Exact mathematical decoding of a microscaling block with one shared E8M0 scale.

                    This function decodes an already encoded block; it does not choose the shared scale. An empty array succeeds without inspecting the scale. On a nonempty array, a NaN scale or any non-finite element causes decoding to fail.

                    Instances For
                      source
                      def FloatLib.Floats.Formats.OCP.MX.E8M0.ofExponent? (exponent : ℤ) :
                      Option E8M0

                      Encode an in-range exponent; return none outside [-127, 127].

                      Instances For
                        source
                        def FloatLib.Floats.Formats.OCP.MX.E8M0.ofExponentSaturating (exponent : ℤ) :
                        E8M0

                        Encode an exponent after clamping it to the finite E8M0 range.

                        Instances For
                          source
                          theorem FloatLib.Floats.Formats.OCP.MX.E8M0.toDyadic?_significand_eq_one {x : E8M0} {value : Numerics.Dyadic} (hx : x.toDyadic? = some value) :
                          value.significand = 1

                          Every successfully decoded E8M0 scale has significand one.

                          source
                          theorem FloatLib.Floats.Formats.OCP.MX.E8M0.toDyadic?_negative_eq_false {x : E8M0} {value : Numerics.Dyadic} (hx : x.toDyadic? = some value) :
                          value.negative = false

                          Every successfully decoded E8M0 scale has its sign bit clear.