TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Kernels.FixedWord.RestoringSqrt.Runtime

Fixed-word restoring square-root runtime #

The restoring loop consumes a four-word radicand two bits at a time and retains the root and remainder in two words. RestoringSqrt.Proof proves exactness under the digit-count and capacity bounds stated below.

source
@[inline]
def FloatLib.Numerics.FixedWord.RestoringSquareRoot.shiftLeftOne (value : UInt128) :
UInt128

Shift a two-word value left by one bit, discarding overflow.

Instances For
    source
    @[inline]
    def FloatLib.Numerics.FixedWord.RestoringSquareRoot.shiftLeftTwo (value : UInt128) :
    UInt128

    Shift a two-word value left by two bits, discarding overflow.

    Instances For
      source
      @[inline]
      def FloatLib.Numerics.FixedWord.RestoringSquareRoot.digitAt (radicand : UInt256) (index : ℕ) :
      UInt64

      Read base-four digit index from a four-word radicand, for index < 128.

      Instances For
        source
        @[inline]
        def FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootStep (digit : UInt64) (state : RestoringRootState UInt128) :
        RestoringRootState UInt128

        One base-four restoring square-root step.

        Instances For
          source
          @[inline]
          def FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootLoop (radicand : UInt256) :
          ℕ → RestoringRootState UInt128 → RestoringRootState UInt128

          Consume base-four digits from most significant to least significant.

          Instances For
            source
            def FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootLoopWords (radicand : UInt256) :
            ℕ → UInt64 → UInt64 → UInt64 → UInt64 → RestoringRootState UInt128

            Consume base-four digits with four word accumulators, constructing only the final state.

            Instances For
              source
              @[inline]
              def FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootLoopImpl (radicand : UInt256) (steps : ℕ) (state : RestoringRootState UInt128) :
              RestoringRootState UInt128

              The word-accumulator implementation of rootLoop, including its wrapping arithmetic.

              Instances For
                source
                @[inline]
                def FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootAndRemainder (radicand : UInt256) (steps : ℕ) :
                RestoringRootState UInt128

                Compute the floor root and exact square remainder from the requested base-four digits.

                The digit count fixes the verified capacity: rootAndRemainder_spec covers radicands below 2^(2 * steps) for any digit count from 64 to 125. Larger radicands lose their leading digits, so the result need not be the root of the original radicand.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Numerics.FixedWord.RestoringSquareRoot.rootAndRemainderImpl (radicand : UInt256) (steps : ℕ) :
                  RestoringRootState UInt128

                  Run the word-accumulator loop from zero root and remainder.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Numerics.FixedWord.RestoringSquareRoot.roundRoot (state : RestoringRootState UInt128) :
                    UInt128

                    Round a floor root to the nearest integer root.

                    The root increments exactly when the remainder exceeds the root, which is the midpoint test for the square. roundRoot_toNat verifies this for every digit count from 64 to 125.

                    Instances For