TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FiniteOnly.E5M2FNUZ

Finite-only E5M2FNUZ #

E5M2FNUZ gives the ONNX finite, NaN-supporting, unsigned-zero E5M2 variant a distinct Lean type. That nominal identity prevents accidental interchange with OCP E5M2, whose infinity and signed zero behavior differs even though both formats occupy one byte.

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.E5M2FNUZ :
Type

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

    Instances For
      source
      theorem FloatLib.Floats.Formats.FiniteOnly.e5m2fnuz_width_le_eight :
      BinaryInterchange.FloatFormat.e5m2fnuz.bitWidth ≤ 8

      The E5M2FNUZ encoding fits in its direct byte carrier.

      source
      def FloatLib.Floats.Formats.FiniteOnly.e5m2fnuzAddTable :
      ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2fnuz e5m2fnuz_width_le_eight) BinaryInterchange.Model.Spec.add

      Certified direct-byte E5M2FNUZ addition table.

      Instances For
        source
        def FloatLib.Floats.Formats.FiniteOnly.e5m2fnuzSubTable :
        ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2fnuz e5m2fnuz_width_le_eight) BinaryInterchange.Model.Spec.sub

        Certified direct-byte E5M2FNUZ subtraction table.

        Instances For
          source
          def FloatLib.Floats.Formats.FiniteOnly.e5m2fnuzMulTable :
          ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2fnuz e5m2fnuz_width_le_eight) BinaryInterchange.Model.Spec.mul

          Certified direct-byte E5M2FNUZ multiplication table.

          Instances For
            source
            def FloatLib.Floats.Formats.FiniteOnly.e5m2fnuzDivTable :
            ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2fnuz e5m2fnuz_width_le_eight) BinaryInterchange.Model.Spec.div

            Certified direct-byte E5M2FNUZ division table.

            Instances For
              source
              def FloatLib.Floats.Formats.FiniteOnly.e5m2fnuzSqrtTable :
              ExecFloat.Backend.TinyTable.CertifiedUnary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2fnuz e5m2fnuz_width_le_eight) BinaryInterchange.Model.Spec.sqrt

              Certified direct-byte E5M2FNUZ square-root table.

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

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

                source
                @[instance_reducible]
                instance FloatLib.Floats.Formats.FiniteOnly.instFamilyInfoE5M2FNUZ :
                BinaryInterchange.StaticByte.FamilyInfo E5M2FNUZ
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.Formats.FiniteOnly.instTablePlanE5M2FNUZ :
                BinaryInterchange.StaticByte.Plans.TablePlan E5M2FNUZ
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.Formats.FiniteOnly.instFmaE5M2FNUZ [planning : ExecFloat.Backend.PolicyFor E5M2FNUZ] :
                ExecFloat.Fma E5M2FNUZ
                source
                @[inline]
                def FloatLib.Floats.Formats.FiniteOnly.E5M2FNUZ.ofNatBits (bits : ℕ) :
                ExecFloat E5M2FNUZ

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

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

                  Read the complete E5M2FNUZ encoding byte.

                  Instances For