TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Native-word addition for generic binary32 #

The nonzero finite path extracts fields and packs the result with UInt32 and UInt64. Non-finite IEEE policy remains outside this module; the entry points return none when either operand is a NaN or infinity. Correctness lives in Addition.Proof.

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

Finite binary32 addition through exact dyadic coordinates.

none means at least one operand is a NaN or infinity; the caller applies the generic IEEE special-value policy in that case.

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

    Machine-word implementation of finite binary32 addition.

    When exponent alignment fits in 39 bits, both exact significands and their sum fit in one UInt64. At larger gaps the smaller finite significand is strictly below half an ulp, so nearest-even rounding returns the dominant operand directly.

    Instances For