TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Finite binary32 runtime coordinates #

Finite binary32 fields are converted into the mantissa-and-scale coordinates shared by native arithmetic kernels. For every nonzero finite value, the coordinates denote its magnitude mantissa * 2^(scale - 149), with exponent subtraction in Int. Bounds and decoder agreement live in Finite.Proof.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.finiteMantissa (exponent fraction : UInt32) :
UInt64

Decode a finite binary32 significand into one native word.

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

    Encode the finite exponent as a nonnegative scale, giving magnitude mantissa * 2^(scale - 149) with exponent subtraction in Int.

    The binary32 entry point only widens its native field; the scale rule itself is shared with every word kernel.

    Instances For