TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Native binary64 addition and subtraction runtime #

The executable binary64 dispatchers combine equal-exponent addition with signed Sterbenz subtraction. Their refinement proofs are isolated in Addition.Proof.

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

Try native same-sign addition of normal binary64 operands with the same exponent.

The sum of two 53-bit significands is rounded once to nearest-even and packed directly.

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

    Try native equal-exponent addition before the exact finite binary64 implementation.

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

      Try signed Sterbenz subtraction first, then reuse native same-exponent addition for opposite-sign subtraction. Every declined case retains the exact finite component kernel.

      Instances For