TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FiniteOnly.E4M3FNUZ

Finite-only E4M3FNUZ #

E4M3FNUZ is a nominal eight-bit format with finite values, one NaN encoding, and unsigned zero. 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; 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; latency uses the exact arithmetic baseline. Fused multiply-add uses the proved generic single-rounding kernel.

Reference #

source
inductive FloatLib.Floats.Formats.FiniteOnly.E4M3FNUZ :
Type

Finite E4M3FNUZ with one NaN code, unsigned zero, and direct byte storage.

    Instances For
      source
      theorem FloatLib.Floats.Formats.FiniteOnly.e4m3fnuz_width_le_eight :
      BinaryInterchange.FloatFormat.e4m3fnuz.bitWidth ≤ 8

      The E4M3FNUZ encoding fits in its direct byte carrier.

      source
      def FloatLib.Floats.Formats.FiniteOnly.e4m3fnuzAddTable :
      ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fnuz e4m3fnuz_width_le_eight) BinaryInterchange.Model.Spec.add

      Certified direct-byte E4M3FNUZ addition table.

      Instances For
        source
        def FloatLib.Floats.Formats.FiniteOnly.e4m3fnuzSubTable :
        ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fnuz e4m3fnuz_width_le_eight) BinaryInterchange.Model.Spec.sub

        Certified direct-byte E4M3FNUZ subtraction table.

        Instances For
          source
          def FloatLib.Floats.Formats.FiniteOnly.e4m3fnuzMulTable :
          ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fnuz e4m3fnuz_width_le_eight) BinaryInterchange.Model.Spec.mul

          Certified direct-byte E4M3FNUZ multiplication table.

          Instances For
            source
            def FloatLib.Floats.Formats.FiniteOnly.e4m3fnuzDivTable :
            ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fnuz e4m3fnuz_width_le_eight) BinaryInterchange.Model.Spec.div

            Certified direct-byte E4M3FNUZ division table.

            Instances For
              source
              def FloatLib.Floats.Formats.FiniteOnly.e4m3fnuzSqrtTable :
              ExecFloat.Backend.TinyTable.CertifiedUnary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e4m3fnuz e4m3fnuz_width_le_eight) BinaryInterchange.Model.Spec.sqrt

              Certified direct-byte E4M3FNUZ square-root table.

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

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

                source
                @[instance_reducible]
                instance FloatLib.Floats.Formats.FiniteOnly.instFamilyInfoE4M3FNUZ :
                BinaryInterchange.StaticByte.FamilyInfo E4M3FNUZ
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.Formats.FiniteOnly.instTablePlanE4M3FNUZ :
                BinaryInterchange.StaticByte.Plans.TablePlan E4M3FNUZ
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.Formats.FiniteOnly.instFmaE4M3FNUZ [planning : ExecFloat.Backend.PolicyFor E4M3FNUZ] :
                ExecFloat.Fma E4M3FNUZ
                source
                @[inline]
                def FloatLib.Floats.Formats.FiniteOnly.E4M3FNUZ.ofNatBits (bits : ℕ) :
                ExecFloat E4M3FNUZ

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

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

                  Read the complete E4M3FNUZ encoding byte.

                  Instances For