TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E2M3

OCP MX E2M3 #

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

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

    Instances For
      source
      theorem FloatLib.Floats.E2M3.width_le_eight :
      Formats.BinaryInterchange.FloatFormat.e2m3.bitWidth ≤ 8

      The E2M3 encoding fits in its direct byte carrier.

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

      Certified E2M3 addition table.

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

        Certified E2M3 subtraction table.

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

          Certified E2M3 multiplication table.

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

            Certified E2M3 division table.

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

              Certified E2M3 square-root table.

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

                Certified E2M3 fused-multiply-add table.

                The table is generated lazily at its first lookup, so importing this package does not compute its 262,144 entries.

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

                  OCP MX FP6 E2M3 element: 2 exponent and 3 fraction bits with bias 1, 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.E2M3.ofNatBits (bits : ℕ) :
                    E2M3

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

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

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

                      Instances For