TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.FP8.E5M2

OCP FP8 E5M2 #

OCP E5M2 has a nominal format identity and a direct UInt8 runtime carrier. Its IEEE-style infinity and NaN encodings remain properties of this format package rather than assumptions of the universal executable carrier.

For addition, subtraction, multiplication, division, and square root, balanced and throughput planning select exhaustive byte tables; latency planning selects the arithmetic kernels. Fused multiply-add uses the proved generic single-rounding kernel, avoiding a 16,777,216-entry ternary table while preserving the same independent specification.

Reference #

source
inductive FloatLib.Floats.Formats.OCP.FP8.E5M2 :
Type

OCP E5M2 FP8 with direct byte storage.

    Instances For
      source
      theorem FloatLib.Floats.Formats.OCP.FP8.e5m2_width_le_eight :
      BinaryInterchange.FloatFormat.e5m2.bitWidth ≤ 8

      The E5M2 encoding fits in its direct byte carrier.

      source
      def FloatLib.Floats.Formats.OCP.FP8.e5m2AddTable :
      ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2 e5m2_width_le_eight) BinaryInterchange.Model.Spec.add

      Certified direct-byte E5M2 addition table.

      Instances For
        source
        def FloatLib.Floats.Formats.OCP.FP8.e5m2SubTable :
        ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2 e5m2_width_le_eight) BinaryInterchange.Model.Spec.sub

        Certified direct-byte E5M2 subtraction table.

        Instances For
          source
          def FloatLib.Floats.Formats.OCP.FP8.e5m2MulTable :
          ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2 e5m2_width_le_eight) BinaryInterchange.Model.Spec.mul

          Certified direct-byte E5M2 multiplication table.

          Instances For
            source
            def FloatLib.Floats.Formats.OCP.FP8.e5m2DivTable :
            ExecFloat.Backend.TinyTable.CertifiedBinary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2 e5m2_width_le_eight) BinaryInterchange.Model.Spec.div

            Certified direct-byte E5M2 division table.

            Instances For
              source
              def FloatLib.Floats.Formats.OCP.FP8.e5m2SqrtTable :
              ExecFloat.Backend.TinyTable.CertifiedUnary (BinaryInterchange.StaticByte.encoding BinaryInterchange.FloatFormat.e5m2 e5m2_width_le_eight) BinaryInterchange.Model.Spec.sqrt

              Certified direct-byte E5M2 square-root table.

              Instances For
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.Formats.OCP.FP8.instFamilyE5M2 :
                BinaryInterchange.StaticByte.Family E5M2

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

                source
                @[instance_reducible]
                instance FloatLib.Floats.Formats.OCP.FP8.instFamilyInfoE5M2 :
                BinaryInterchange.StaticByte.FamilyInfo E5M2
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.Formats.OCP.FP8.instTablePlanE5M2 :
                BinaryInterchange.StaticByte.Plans.TablePlan E5M2
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.Formats.OCP.FP8.instFmaE5M2 [planning : ExecFloat.Backend.PolicyFor E5M2] :
                ExecFloat.Fma E5M2
                source
                @[inline]
                def FloatLib.Floats.Formats.OCP.FP8.E5M2.ofNatBits (bits : ℕ) :
                ExecFloat E5M2

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

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.OCP.FP8.E5M2.toUInt8 (value : ExecFloat E5M2) :
                  UInt8

                  Read the complete OCP E5M2 encoding byte.

                  Instances For