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; compiled code is better served by left shifts. Frequently used format values therefore have shift-based implementations, with proved equalities registered for compiler substitution.

Source-level theorems use the mathematical definitions; compiler substitutions replace them with the proved shift formulas.

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

Shift-based compiled implementation of bias.

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

    Shift-based compiled implementation of ieeeMinSubnormalExponent.

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

      Compiled implementation of normalMantissaExpOffset.

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

        Shift-based compiled implementation of ieeeMaxNormalExponent.

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

          Shift-based compiled implementation of ieeeMinNormalExponent.

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

            Compiled implementation of subnormalAlignExp.

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

              Shift-based compiled implementation of expAllOnesNat.

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

                Shift-based compiled implementation of fracMaskNat.

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

                  Shift-based compiled implementation of expMaskNat.

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

                    Shift-based compiled implementation of signMaskNat.

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

                      Shift-based compiled implementation of quietBitNat.

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

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

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeMinSubnormalExponent_eq_ieeeMinSubnormalExponentImpl :
                        ieeeMinSubnormalExponent = ieeeMinSubnormalExponentImpl

                        Compiler substitution for the least-subnormal dyadic exponent.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.normalMantissaExpOffset_eq_normalMantissaExpOffsetImpl :
                        normalMantissaExpOffset = normalMantissaExpOffsetImpl

                        Compiler substitution for the normal-significand exponent offset.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeMaxNormalExponent_eq_ieeeMaxNormalExponentImpl :
                        ieeeMaxNormalExponent = ieeeMaxNormalExponentImpl

                        Compiler substitution for the greatest normal unbiased exponent.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.ieeeMinNormalExponent_eq_ieeeMinNormalExponentImpl :
                        ieeeMinNormalExponent = ieeeMinNormalExponentImpl

                        Compiler substitution for the least normal unbiased exponent.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.subnormalAlignExp_eq_subnormalAlignExpImpl :
                        subnormalAlignExp = subnormalAlignExpImpl

                        Compiler substitution for the subnormal alignment exponent.

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.expAllOnesNat_eq_expAllOnesNatImpl :
                        expAllOnesNat = expAllOnesNatImpl

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

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.fracMaskNat_eq_fracMaskNatImpl :
                        fracMaskNat = fracMaskNatImpl

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

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.expMaskNat_eq_expMaskNatImpl :
                        expMaskNat = expMaskNatImpl

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

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.signMaskNat_eq_signMaskNatImpl :
                        signMaskNat = signMaskNatImpl

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

                        source
                        @[csimp]
                        theorem FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.quietBitNat_eq_quietBitNatImpl :
                        quietBitNat = quietBitNatImpl

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