TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Native binary32 square root #

Positive finite inputs are scaled to a 47- or 48-bit radicand, so the exact floor square root and nearest-even decision fit entirely in UInt64. The complete operation retains IEEE NaN, infinity, negative-input, and signed-zero behavior. Correctness lives in Sqrt.Proof.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.sqrtPositiveFiniteCore (mantissa scale : UInt64) :
UInt32

Round the square root of a positive finite binary32 mantissa and scale.

For 0 < mantissa < 2^24 and scale ≤ 253, the input value is mantissa * 2^(scale - 149), with subtraction in Int. The selected shift places its square root in the 24-bit binary32 significand range before the final nearest-even decision.

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

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

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

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

      Instances For