TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.FP8.E4M3FN

OCP FP8 E4M3FN #

FloatLib.Floats.E4M3FN is OCP E4M3FN with a direct UInt8 runtime carrier, and E4M3FN.Family is its type-level identity. 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 because an eight-bit ternary table would contain 16,777,216 entries.

The binary-interchange descriptor specifies the format and its kernels. It is not stored in an E4M3FN value.

Reference #

source
inductive FloatLib.Floats.E4M3FN.Family :
Type

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

    Instances For
      source
      theorem FloatLib.Floats.E4M3FN.width_le_eight :
      Formats.BinaryInterchange.FloatFormat.e4m3fn.bitWidth ≤ 8

      The E4M3FN encoding fits in its direct byte carrier.

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

      Certified direct-byte E4M3FN addition table.

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

        Certified direct-byte E4M3FN subtraction table.

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

          Certified direct-byte E4M3FN multiplication table.

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

            Certified direct-byte E4M3FN division table.

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

              Certified direct-byte E4M3FN square-root table.

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

                Package the five dense byte tables with the proved arithmetic FMA baseline. The tables total about 256 KiB, and keeping the single-rounding model kernel avoids a 16 MiB FMA table.

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

                OCP FP8 E4M3FN: 4 exponent and 3 fraction bits with bias 7, no infinity, and NaN only at the two all-ones codes. Values are stored in one byte, and balanced and throughput planning answer the five basic operations from certified byte tables.

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

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

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

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

                    Read the complete OCP E4M3FN encoding byte.

                    Instances For