TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FiniteOnly.E5M2FNUZ

Finite-only E5M2FNUZ #

FloatLib.Floats.E5M2FNUZ gives the ONNX finite, NaN-supporting, unsigned-zero E5M2 variant a distinct Lean type, with type-level identity E5M2FNUZ.Family. That 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. The latency policy uses the exact arithmetic baseline. Fused multiply-add uses the proved generic single-rounding kernel.

Reference #

source
inductive FloatLib.Floats.E5M2FNUZ.Family :
Type

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

    Instances For
      source
      theorem FloatLib.Floats.E5M2FNUZ.width_le_eight :
      Formats.BinaryInterchange.FloatFormat.e5m2fnuz.bitWidth ≤ 8

      The E5M2FNUZ encoding fits in its direct byte carrier.

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

      Certified direct-byte E5M2FNUZ addition table.

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

        Certified direct-byte E5M2FNUZ subtraction table.

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

          Certified direct-byte E5M2FNUZ multiplication table.

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

            Certified direct-byte E5M2FNUZ division table.

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

              Certified direct-byte E5M2FNUZ square-root table.

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

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

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

                ONNX E5M2FNUZ: 5 exponent and 2 fraction bits with bias 16, 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.E5M2FNUZ.ofNatBits (bits : ℕ) :
                  E5M2FNUZ

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

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

                    Read the complete E5M2FNUZ encoding byte.

                    Instances For