TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E2M1

OCP MX E2M1 #

FloatLib.Floats.E2M1 is the four-bit floating element used by OCP microscaling formats, with type-level identity E2M1.Family. It stores its code in the low four bits of a UInt8, and the high-bit invariant is erased at runtime. Balanced and throughput planning select exhaustive proved tables for all six operations, including the 4,096-entry fused-multiply-add table. Latency planning selects arithmetic kernels.

This package implements the scalar element format. OCP block semantics and scale selection are defined under FloatLib.Floats.Formats.OCP.MX.Standard.

Reference #

source
inductive FloatLib.Floats.E2M1.Family :
Type

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

    Instances For
      source
      theorem FloatLib.Floats.E2M1.width_le_eight :
      Formats.BinaryInterchange.FloatFormat.e2m1.bitWidth ≤ 8

      The E2M1 encoding fits in its direct byte carrier.

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

      Certified direct-byte E2M1 addition table.

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

        Certified direct-byte E2M1 subtraction table.

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

          Certified direct-byte E2M1 multiplication table.

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

            Certified direct-byte E2M1 division table.

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

              Certified direct-byte E2M1 square-root table.

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

                Certified direct-byte E2M1 fused-multiply-add table.

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

                  OCP MX FP4 E2M1 element: 2 exponent bits and 1 fraction bit with bias 1, every code finite, stored in the low four bits of a byte. Under balanced and throughput planning, arithmetic, including fused multiply-add, reads certified byte tables.

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

                    Construct E2M1 from a natural pattern, reduced to four bits.

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

                      Read the byte whose low four bits contain the E2M1 code.

                      Instances For