TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.FP8.E5M2

OCP FP8 E5M2 #

FloatLib.Floats.E5M2 is OCP E5M2 with a direct UInt8 runtime carrier, and E5M2.Family is its type-level identity. Its IEEE-style infinity and NaN encodings are properties of this format package, and the universal executable carrier does not assume them.

For addition, subtraction, multiplication, division, and square root, balanced and throughput planning select exhaustive byte tables, and latency planning selects the arithmetic kernels. Fused multiply-add uses the proved generic single-rounding kernel, which avoids a 16,777,216-entry ternary table and meets the same specification.

Reference #

source
inductive FloatLib.Floats.E5M2.Family :
Type

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

    Instances For
      source
      theorem FloatLib.Floats.E5M2.width_le_eight :
      Formats.BinaryInterchange.FloatFormat.e5m2.bitWidth ≤ 8

      The E5M2 encoding fits in its direct byte carrier.

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

      Certified direct-byte E5M2 addition table.

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

        Certified direct-byte E5M2 subtraction table.

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

          Certified direct-byte E5M2 multiplication table.

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

            Certified direct-byte E5M2 division table.

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

              Certified direct-byte E5M2 square-root table.

              Instances For
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.E5M2.instFamilyFamily :
                Formats.BinaryInterchange.StaticByte.Family Family

                Package the five byte tables with the proved arithmetic FMA baseline.

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

                OCP FP8 E5M2: the IEEE encoding with 5 exponent and 2 fraction bits, so binary16's exponent range with infinities and NaNs. Values are stored in one byte, and balanced and throughput planning answer the five basic operations from certified byte tables.

                ExecFloat.Binary (exponentBits := 5) (fractionBits := 2) is the same format on the general binary carrier, with directed rounding and status options.

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

                  Construct OCP E5M2 from a natural bit pattern, reduced to eight bits.

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

                    Read the complete OCP E5M2 encoding byte.

                    Instances For