TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Format.Runtime

Compiled binary format constants #

Layout proofs are easiest to read with powers such as 2 ^ fmt.expWidth, but compiled code is better served by left shifts. Frequently used format values therefore have shift-based implementations, with proved equalities registered for compiler substitution.

Theorems use the mathematical definitions, and compiled code runs the proved shift formulas.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.bias (fmt : FloatFormat) :
Nat

Shift-based compiled implementation of bias.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.ieeeMinSubnormalExponent (fmt : FloatFormat) :
    Int

    Shift-based compiled implementation of ieeeMinSubnormalExponent.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.normalMantissaExpOffset (fmt : FloatFormat) :
      Nat

      Compiled implementation of normalMantissaExpOffset.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.ieeeMaxNormalExponent (fmt : FloatFormat) :
        Nat

        Shift-based compiled implementation of ieeeMaxNormalExponent.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.ieeeMinNormalExponent (fmt : FloatFormat) :
          Int

          Shift-based compiled implementation of ieeeMinNormalExponent.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.subnormalAlignExp (fmt : FloatFormat) :
            Nat

            Compiled implementation of subnormalAlignExp.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.expAllOnesNat (fmt : FloatFormat) :
              Nat

              Shift-based compiled implementation of expAllOnesNat.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.fracMaskNat (fmt : FloatFormat) :
                Nat

                Shift-based compiled implementation of fracMaskNat.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.expMaskNat (fmt : FloatFormat) :
                  Nat

                  Shift-based compiled implementation of expMaskNat.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.signMaskNat (fmt : FloatFormat) :
                    Nat

                    Shift-based compiled implementation of signMaskNat.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Internal.quietBitNat (fmt : FloatFormat) :
                      Nat

                      Shift-based compiled implementation of quietBitNat.

                      Instances For
                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.bias_eq_internal :
                        bias = Internal.bias

                        Compiler substitution of exponent-bias exponentiation by the equivalent shift kernel.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeMinSubnormalExponent_eq_internal :
                        ieeeMinSubnormalExponent = Internal.ieeeMinSubnormalExponent

                        Compiler substitution for the least-subnormal dyadic exponent.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.normalMantissaExpOffset_eq_internal :
                        normalMantissaExpOffset = Internal.normalMantissaExpOffset

                        Compiler substitution for the normal-significand exponent offset.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeMaxNormalExponent_eq_internal :
                        ieeeMaxNormalExponent = Internal.ieeeMaxNormalExponent

                        Compiler substitution for the greatest normal unbiased exponent.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeMinNormalExponent_eq_internal :
                        ieeeMinNormalExponent = Internal.ieeeMinNormalExponent

                        Compiler substitution for the least normal unbiased exponent.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.subnormalAlignExp_eq_internal :
                        subnormalAlignExp = Internal.subnormalAlignExp

                        Compiler substitution for the subnormal alignment exponent.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.expAllOnesNat_eq_internal :
                        expAllOnesNat = Internal.expAllOnesNat

                        Compiler substitution of the all-ones exponent mask by the equivalent shift kernel.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.fracMaskNat_eq_internal :
                        fracMaskNat = Internal.fracMaskNat

                        Compiler substitution of the fraction mask by the equivalent shift kernel.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.expMaskNat_eq_internal :
                        expMaskNat = Internal.expMaskNat

                        Compiler substitution of the shifted exponent mask by the equivalent shift kernel.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.signMaskNat_eq_internal :
                        signMaskNat = Internal.signMaskNat

                        Compiler substitution of the sign mask by the equivalent shift kernel.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.quietBitNat_eq_internal :
                        quietBitNat = Internal.quietBitNat

                        Compiler substitution of the quiet-NaN bit by the equivalent shift kernel.