TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E2M3

OCP MX E2M3 #

E2M3 is a six-bit finite floating element from the OCP microscaling specification. The runtime carrier is a UInt8 with an erased proof that the code is below 64. 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.E2M3 :
Type

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

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

      The E2M3 encoding fits in its direct byte carrier.

      source
      def FloatLib.Floats.Formats.OCP.MX.e2m3AddTable :
      ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e2m3 e2m3_width_le_eight) BinaryInterchange.Model.Spec.add

      Certified E2M3 addition table.

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

        Certified E2M3 subtraction table.

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

          Certified E2M3 multiplication table.

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

            Certified E2M3 division table.

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

              Certified E2M3 square-root table.

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

                Certified E2M3 fused-multiply-add table.

                Its generation equation is opaque, so importing this package does not normalize the 262,144 entries.

                Instances For
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instFamilyE2M3 :
                  BinaryInterchange.StaticByte.Family E2M3
                  source
                  @[instance_reducible]
                  instance FloatLib.Floats.Formats.OCP.MX.instFamilyInfoE2M3 :
                  BinaryInterchange.StaticByte.FamilyInfo E2M3
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instTablePlanE2M3 :
                  BinaryInterchange.StaticByte.Plans.TablePlan E2M3
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instFmaE2M3 [planning : ExecFloat.Backend.PolicyFor E2M3] :
                  ExecFloat.Fma E2M3
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.OCP.MX.E2M3.ofNatBits (bits : ℕ) :
                  ExecFloat E2M3

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

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

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

                    Instances For