TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E2M1

OCP MX E2M1 #

E2M1 is the four-bit floating element used by OCP microscaling formats. This nominal package stores its code in the low four bits of a UInt8; 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.Formats.OCP.MX.E2M1 :
Type

OCP MX E2M1 four-bit element format with byte-backed storage.

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

      The E2M1 encoding fits in its direct byte carrier.

      source
      def FloatLib.Floats.Formats.OCP.MX.e2m1AddTable :
      ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e2m1 e2m1_width_le_eight) BinaryInterchange.Model.Spec.add

      Certified direct-byte E2M1 addition table.

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

        Certified direct-byte E2M1 subtraction table.

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

          Certified direct-byte E2M1 multiplication table.

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

            Certified direct-byte E2M1 division table.

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

              Certified direct-byte E2M1 square-root table.

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

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

                Instances For
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instFamilyE2M1 :
                  BinaryInterchange.StaticByte.Family E2M1
                  source
                  @[instance_reducible]
                  instance FloatLib.Floats.Formats.OCP.MX.instFamilyInfoE2M1 :
                  BinaryInterchange.StaticByte.FamilyInfo E2M1
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instTablePlanE2M1 :
                  BinaryInterchange.StaticByte.Plans.TablePlan E2M1
                  source
                  @[instance_reducible, always_inline]
                  instance FloatLib.Floats.Formats.OCP.MX.instFmaE2M1 [planning : ExecFloat.Backend.PolicyFor E2M1] :
                  ExecFloat.Fma E2M1
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.OCP.MX.E2M1.ofNatBits (bits : ℕ) :
                  ExecFloat E2M1

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

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

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

                    Instances For