TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E3M2

OCP MX E3M2 #

FloatLib.Floats.E3M2 is a six-bit finite floating element from the OCP microscaling specification, with type-level identity E3M2.Family. 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, and 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.E3M2.Family :
Type

Type-level identity of E3M2, selecting its descriptor, carrier, and kernels.

    Instances For
      source
      theorem FloatLib.Floats.E3M2.width_le_eight :
      Formats.BinaryInterchange.FloatFormat.e3m2.bitWidth ≤ 8

      The E3M2 encoding fits in its direct byte carrier.

      source
      def FloatLib.Floats.E3M2.addTable :
      ExecFloat.Backend.TinyTable.CertifiedBinary (Formats.BinaryInterchange.StaticByte.encoding Formats.BinaryInterchange.FloatFormat.e3m2 width_le_eight) Formats.BinaryInterchange.Model.Spec.add

      Certified E3M2 addition table.

      Instances For
        source
        def FloatLib.Floats.E3M2.subTable :
        ExecFloat.Backend.TinyTable.CertifiedBinary (Formats.BinaryInterchange.StaticByte.encoding Formats.BinaryInterchange.FloatFormat.e3m2 width_le_eight) Formats.BinaryInterchange.Model.Spec.sub

        Certified E3M2 subtraction table.

        Instances For
          source
          def FloatLib.Floats.E3M2.mulTable :
          ExecFloat.Backend.TinyTable.CertifiedBinary (Formats.BinaryInterchange.StaticByte.encoding Formats.BinaryInterchange.FloatFormat.e3m2 width_le_eight) Formats.BinaryInterchange.Model.Spec.mul

          Certified E3M2 multiplication table.

          Instances For
            source
            def FloatLib.Floats.E3M2.divTable :
            ExecFloat.Backend.TinyTable.CertifiedBinary (Formats.BinaryInterchange.StaticByte.encoding Formats.BinaryInterchange.FloatFormat.e3m2 width_le_eight) Formats.BinaryInterchange.Model.Spec.div

            Certified E3M2 division table.

            Instances For
              source
              def FloatLib.Floats.E3M2.sqrtTable :
              ExecFloat.Backend.TinyTable.CertifiedUnary (Formats.BinaryInterchange.StaticByte.encoding Formats.BinaryInterchange.FloatFormat.e3m2 width_le_eight) Formats.BinaryInterchange.Model.Spec.sqrt

              Certified E3M2 square-root table.

              Instances For
                source
                def FloatLib.Floats.E3M2.fmaTable :
                ExecFloat.Backend.TinyTable.CertifiedTernary (Formats.BinaryInterchange.StaticByte.encoding Formats.BinaryInterchange.FloatFormat.e3m2 width_le_eight) Formats.BinaryInterchange.Model.Spec.fma

                Certified E3M2 fused-multiply-add table.

                Instances For
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.E3M2.instFamilyFamily :
                  Formats.BinaryInterchange.StaticByte.Family Family
                  source
                  @[instance_reducible]
                  instance FloatLib.Floats.E3M2.instFamilyInfoFamily :
                  Formats.BinaryInterchange.StaticByte.FamilyInfo Family
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.E3M2.instTablePlanFamily :
                  Formats.BinaryInterchange.StaticByte.Plans.TablePlan Family
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.E3M2.instFmaFamily [planning : ExecFloat.Backend.PolicyFor Family] :
                  ExecFloat.Fma Family
                  source
                  @[reducible, inline]
                  abbrev FloatLib.Floats.E3M2 :
                  Type

                  OCP MX FP6 E3M2 element: 3 exponent and 2 fraction bits with bias 3, every code finite, stored in the low six bits of a byte. Throughput planning answers all six operations from certified byte tables.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.E3M2.ofNatBits (bits : ℕ) :
                    E3M2

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

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

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

                      Instances For