TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FiniteOnly.E4M3FNUZ

Finite-only E4M3FNUZ #

FloatLib.Floats.E4M3FNUZ is an eight-bit format with finite values, one NaN encoding, and unsigned zero, and E4M3FNUZ.Family is its type-level identity. Its name records the conventions used by the ONNX float8 specification: F excludes infinity, N retains NaN, and UZ identifies the unsigned-zero encoding. These choices belong to this format package, and the universal executable interface assumes none of them.

The runtime carrier is one UInt8. Balanced and throughput policies select exhaustive proved byte tables for addition, subtraction, multiplication, division, and square root. The latency policy uses the exact arithmetic baseline. Fused multiply-add uses the proved generic single-rounding kernel.

Reference #

source
inductive FloatLib.Floats.E4M3FNUZ.Family :
Type

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

    Instances For
      source
      theorem FloatLib.Floats.E4M3FNUZ.width_le_eight :
      Formats.BinaryInterchange.FloatFormat.e4m3fnuz.bitWidth ≤ 8

      The E4M3FNUZ encoding fits in its direct byte carrier.

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

      Certified direct-byte E4M3FNUZ addition table.

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

        Certified direct-byte E4M3FNUZ subtraction table.

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

          Certified direct-byte E4M3FNUZ multiplication table.

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

            Certified direct-byte E4M3FNUZ division table.

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

              Certified direct-byte E4M3FNUZ square-root table.

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

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

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

                ONNX E4M3FNUZ, the FP8 format of AMD accelerators: 4 exponent and 3 fraction bits with bias 8, one zero, no infinity, and the negative-zero code as the sole NaN. Values are stored in one byte and their arithmetic reads certified byte tables.

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

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

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

                    Read the complete E4M3FNUZ encoding byte.

                    Instances For