TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Rounding.SquareRoot.Direct.Runtime

Executable direct posit square-root packing #

The square root of an exact dyadic need not be dyadic. This module scales the source by an even power of two, computes its integer square root, and jams the exact square remainder into the low bit of a prefix with enough bits for the destination format. The ordinary direct Posit packer then performs the complete guard/sticky rounding step.

The kernel is width-generic. Its equality to exact square-root rounding is proved in Direct.Proof.

source
@[inline]
def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.prefixPrecision (format : Format) :
ℕ

Number of generated square-root fraction bits.

A Posit has payloadBits bits below its sign. Generating the root to that precision leaves enough exponent/fraction stream for every possible guard bit; the jammed low bit records whether the exact root has any later nonzero digit.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.exponentParity (radicand : Numerics.Dyadic) :
    ℕ

    Parity of the source dyadic exponent, represented as zero or one.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.scaledRadicand (precision : ℕ) (radicand : Numerics.Dyadic) :
      ℕ

      Integer radicand whose square root carries precision generated fraction bits.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.truncatedRoot (precision : ℕ) (radicand : Numerics.Dyadic) :
        ℕ

        Truncated integer square root at the requested fractional precision.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.squareRemainder (precision : ℕ) (radicand : Numerics.Dyadic) :
          ℕ

          Exact square remainder left by the truncated integer root.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.prefixAtPrecision (precision : ℕ) (radicand : Numerics.Dyadic) :
            Numerics.Dyadic

            Generate a normalized square-root prefix at an explicit fractional precision.

            Writing the source exponent as 2q + r, where r is zero or one, reduces the operation to an integer square root of significand * 2^(r + 2 * precision). The Euclidean square remainder determines whether the exact root continues beyond the generated prefix.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.rootPrefix (format : Format) (radicand : Numerics.Dyadic) :
              Numerics.Dyadic

              Generate the destination-width normalized square-root prefix.

              The policy depends only on representable precision, not on a named storage backend or special format width.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.roundCode (format : Format) (radicand : Numerics.Dyadic) :
                ℕ

                Round a nonnegative square root directly from its normalized prefix and exact sticky bit.

                Integer square-root and remainder calculations determine the prefix; the shared guard/sticky packer selects the final code. This helper returns zero for zero or negative inputs.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.Posit.Model.DirectDyadicSquareRoot.round (format : Format) (radicand : Numerics.Dyadic) :
                  Model format

                  Pack the code selected by direct prefix square-root rounding.

                  Instances For