TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E3M2

OCP MX E3M2 #

E3M2 is a six-bit finite floating element from the OCP microscaling specification. Its direct runtime carrier is a byte with an erased < 64 invariant. For addition, subtraction, multiplication, division, and square root, balanced and throughput planning select exhaustive proved tables; latency planning selects arithmetic kernels. Fused multiply-add keeps both a table and the generic proved kernel: throughput planning selects the table, while balanced and latency-oriented planning avoid its larger lookup footprint.

Reference #

source
inductive FloatLib.Floats.Formats.OCP.MX.E3M2 :
Type

OCP MX E3M2 six-bit element format with byte-backed storage.

    Instances For
      source
      theorem FloatLib.Floats.Formats.OCP.MX.e3m2_width_le_eight :
      BinaryInterchange.FloatFormat.e3m2.bitWidth ≤ 8

      The E3M2 encoding fits in its direct byte carrier.

      source
      def FloatLib.Floats.Formats.OCP.MX.e3m2AddTable :
      ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e3m2 e3m2_width_le_eight) BinaryInterchange.Model.Spec.add

      Certified E3M2 addition table.

      Instances For
        source
        def FloatLib.Floats.Formats.OCP.MX.e3m2SubTable :
        ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e3m2 e3m2_width_le_eight) BinaryInterchange.Model.Spec.sub

        Certified E3M2 subtraction table.

        Instances For
          source
          def FloatLib.Floats.Formats.OCP.MX.e3m2MulTable :
          ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e3m2 e3m2_width_le_eight) BinaryInterchange.Model.Spec.mul

          Certified E3M2 multiplication table.

          Instances For
            source
            def FloatLib.Floats.Formats.OCP.MX.e3m2DivTable :
            ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e3m2 e3m2_width_le_eight) BinaryInterchange.Model.Spec.div

            Certified E3M2 division table.

            Instances For
              source
              def FloatLib.Floats.Formats.OCP.MX.e3m2SqrtTable :
              ExecFloat.Backend.TinyTable.CertifiedUnary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e3m2 e3m2_width_le_eight) BinaryInterchange.Model.Spec.sqrt

              Certified E3M2 square-root table.

              Instances For
                source
                def FloatLib.Floats.Formats.OCP.MX.e3m2FmaTable :
                ExecFloat.Backend.TinyTable.CertifiedTernary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e3m2 e3m2_width_le_eight) BinaryInterchange.Model.Spec.fma

                Certified E3M2 fused-multiply-add table.

                Instances For
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instFamilyE3M2 :
                  BinaryInterchange.StaticByte.Family E3M2
                  source
                  @[instance_reducible]
                  instance FloatLib.Floats.Formats.OCP.MX.instFamilyInfoE3M2 :
                  BinaryInterchange.StaticByte.FamilyInfo E3M2
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instTablePlanE3M2 :
                  BinaryInterchange.StaticByte.Plans.TablePlan E3M2
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instFmaE3M2 [planning : ExecFloat.Backend.PolicyFor E3M2] :
                  ExecFloat.Fma E3M2
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.OCP.MX.E3M2.ofNatBits (bits : ℕ) :
                  ExecFloat E3M2

                  Construct E3M2 from a natural pattern, reduced to six bits.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.OCP.MX.E3M2.toUInt8 (value : ExecFloat E3M2) :
                    UInt8

                    Read the byte whose low six bits contain the E3M2 code.

                    Instances For