TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Format.Catalog

Standard and low-precision binary formats #

Named FloatFormat descriptors cover IEEE interchange formats, common machine-learning formats, and a 256-bit IEEE-style layout. They are all values of the same FloatFormat structure used by custom formats; no operation or theorem is duplicated for a named encoding.

References #

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.SameLayout (left right : FloatFormat) :
Prop

Structural equality of two binary-interchange layouts.

Backend capabilities should depend on these computational fields rather than descriptor names. The proof fields in FloatFormat are propositions, so matching the stored layout recovers full descriptor equality.

Instances For
    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.eq_of_sameLayout {left right : FloatFormat} (h : left.SameLayout right) :
    left = right

    Two descriptors with the same stored layout are equal.

    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary16 :
    FloatFormat

    IEEE binary16, commonly called half precision.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.bfloat16 :
      FloatFormat

      Bfloat16, with the normal exponent range of binary32 and eight significand bits.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 :
        FloatFormat

        IEEE binary32, commonly called single precision.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary64 :
          FloatFormat

          IEEE binary64, commonly called double precision.

          Instances For
            source
            @[simp]
            theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.isIEEE_binary16 :
            binary16.isIEEE = true

            Binary16 uses the IEEE exceptional-value encoding.

            source
            @[simp]
            theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.isIEEE_bfloat16 :
            bfloat16.isIEEE = true

            Bfloat16 uses the IEEE exceptional-value encoding.

            source
            @[simp]
            theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.isIEEE_binary32 :
            binary32.isIEEE = true

            Binary32 uses the IEEE exceptional-value encoding.

            source
            @[simp]
            theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.isIEEE_binary64 :
            binary64.isIEEE = true

            Binary64 uses the IEEE exceptional-value encoding.

            source
            @[reducible, inline]
            abbrev FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.IsBinary32 (fmt : FloatFormat) :
            Prop

            Structural capability for the binary32 native backend.

            The theorem below recovers full descriptor equality before any carrier cast.

            Instances For
              source
              theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.eq_binary32_of_isBinary32 {fmt : FloatFormat} (h : fmt.IsBinary32) :
              fmt = binary32

              A format with the binary32 storage layout is binary32.

              source
              @[reducible, inline]
              abbrev FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.IsBinary64 (fmt : FloatFormat) :
              Prop

              Structural capability for the binary64 native-storage backend.

              Instances For
                source
                theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.eq_binary64_of_isBinary64 {fmt : FloatFormat} (h : fmt.IsBinary64) :
                fmt = binary64

                A format with the binary64 storage layout is binary64.

                source
                @[simp]
                theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.isBinary32_binary32 :
                binary32.IsBinary32

                The named binary32 descriptor satisfies its data-only backend predicate.

                source
                @[simp]
                theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.not_isBinary64_binary32 :
                ¬binary32.IsBinary64

                Binary32 does not satisfy the binary64 backend predicate.

                source
                @[simp]
                theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.not_isBinary32_binary64 :
                ¬binary64.IsBinary32

                Binary64 does not satisfy the binary32 backend predicate.

                source
                @[simp]
                theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.isBinary64_binary64 :
                binary64.IsBinary64

                The named binary64 descriptor satisfies its data-only backend predicate.

                source
                @[inline]
                def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary128 :
                FloatFormat

                IEEE binary128, commonly called quadruple precision.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary256 :
                  FloatFormat

                  A named 256-bit IEEE-style layout with a 237-bit significand.

                  It uses 19 exponent bits and 236 stored fraction bits. Arbitrary wider layouts remain available by constructing FloatFormat directly.

                  Instances For
                    source
                    @[simp]
                    theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.isIEEE_binary128 :
                    binary128.isIEEE = true

                    Binary128 uses the IEEE exceptional-value encoding.

                    source
                    @[simp]
                    theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.isIEEE_binary256 :
                    binary256.isIEEE = true

                    The binary256 profile uses the IEEE-style exceptional-value encoding.

                    Low-precision and finite-only formats #

                    source
                    @[inline]
                    def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.e5m2 :
                    FloatFormat

                    OCP/ONNX E5M2: bias 15 with IEEE-style infinities and NaNs.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.tf32 :
                      FloatFormat

                      Compact semantic TensorFloat-32 layout with eight exponent and ten fraction bits.

                      Instances For
                        source
                        @[inline]
                        def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.e4m3fn :
                        FloatFormat

                        OCP/ONNX E4M3FN: bias 7, no infinity, maximum fraction at maximum exponent is NaN.

                        Instances For
                          source
                          @[inline]
                          def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.e4m3fnuz :
                          FloatFormat

                          ONNX E4M3FNUZ: bias 8, one zero, and the negative-zero word as the sole NaN.

                          Instances For
                            source
                            @[inline]
                            def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.e5m2fnuz :
                            FloatFormat

                            ONNX E5M2FNUZ: bias 16, one zero, and the negative-zero word as the sole NaN.

                            Instances For
                              source
                              @[inline]
                              def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.e2m1 :
                              FloatFormat

                              OCP MX FP4 E2M1: bias 1 with every stored word finite.

                              Instances For
                                source
                                @[inline]
                                def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.e2m3 :
                                FloatFormat

                                OCP MX FP6 E2M3 element format with every stored word finite.

                                Instances For
                                  source
                                  @[inline]
                                  def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.e3m2 :
                                  FloatFormat

                                  OCP MX FP6 E3M2 element format with every stored word finite.

                                  Instances For