TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Generic.ScaledSqrt.Runtime

Integer square roots at the rounding scale #

Discarding twice as many radicand bits as root bits preserves the truncated root. One retained root bit and an exact square comparison recover the round and sticky bits without constructing the full root or shifting it one bit at a time.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.ScaledSqrt.accuracy (radicand root : ℕ) :
Float.Model.UnpackedFloat.Accuracy

Accuracy of an integer square root, from its exact nonnegative remainder.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.ScaledSqrt.shifted (radicand shift : ℕ) :
    Float.Model.UnpackedFloat.ExtendedMantissa

    The integer square root after a right shift, retaining exact round and sticky bits.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.ScaledSqrt.round (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign) (radicand : ℕ) (exponent : ℤ) :
      Float.Model.UnpackedFloat

      Round a scaled integer square root through the unpacked model's normalization rules.

      Instances For