TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.Full.Sqrt.Runtime

Native binary64 square-root runtime #

Positive finite inputs are scaled to a 105- or 106-bit radicand held in two UInt64 limbs. A 53-step restoring square-root loop computes the floor root and remainder using native words. The remainder classifies the nearest-even result directly, after which the binary64 exponent and fraction are packed without constructing a generic unpacked-float model.

Correctness proofs and the Nat.sqrt model are isolated in Sqrt.Proof.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.shiftedRadicand (mantissa : UInt64) (shift : ℕ) :
Numerics.FixedWord.UInt128

Shift a binary64 significand into two limbs; callers supply a positive shift below 128 and a result that fits in 128 bits.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.digitAt (radicand : Numerics.FixedWord.UInt128) (index : ℕ) :
    UInt64

    Read a base-four digit of a two-limb radicand, for an index below 64.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootStep (digit : UInt64) (state : Numerics.FixedWord.RestoringRootState UInt64) :
      Numerics.FixedWord.RestoringRootState UInt64

      Consume one base-four digit in the restoring square-root recurrence.

      For the binary64 radicands constructed above, 53 iterations produce a 53-bit floor root. The remainder and trial divisor remain below one native word.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootLoop (radicand : Numerics.FixedWord.UInt128) :
        ℕ → Numerics.FixedWord.RestoringRootState UInt64 → Numerics.FixedWord.RestoringRootState UInt64

        Consume a requested number of radicand digits from most significant to least significant.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.rootAndRemainder (mantissa : UInt64) (shift : ℕ) :
          Numerics.FixedWord.RestoringRootState UInt64

          Compute the floor root and exact remainder of a binary64-sized scaled radicand.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.sqrtPositiveFiniteCore (mantissa scale : UInt64) :
            UInt64

            Direct positive-finite binary64 square root.

            For a nonzero significand below 2^53 and a scale at most 2045, the input value is mantissa * 2^(scale - 1074), with subtraction in the exponent interpreted in Int. Parity chooses a 105- or 106-bit integer radicand. Its square root cannot be a half-integer, so remainder ≤ root is precisely the round-down condition.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.sqrtPositiveFinite (exponent fraction : UInt64) :
              UInt64

              Decode binary64 fields and run the bounded positive-finite square-root kernel.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.sqrt (x : Value) :
                Value

                Native binary64 square root, including IEEE exceptional-value behavior.

                Instances For