TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Native-word finite multiplication for generic binary32 #

Finite binary32 significands occupy at most 24 bits, so their exact product fits in one UInt64. Special-value policy remains outside this module; both entry points return none for a NaN or infinity. Correctness lives in Multiplication.Proof.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.mulFinite? (x y : Value) :
Option Value

Finite multiplication through exact dyadic coordinates.

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

    Machine-word implementation of finite binary32 multiplication.

    Each operand magnitude is mantissa * 2^(scale - 149), with subtraction interpreted in Int. The runtime uses unsigned scales throughout normalization and rounding.

    Instances For