Two-word finite addition and subtraction

The two-word counterpart of NativeSmallWordAdd: both operands are decoded from their storage words into a sign, a compact finite scale, and a two-word significand. Scales at most shiftLimit apart are aligned exactly by a left shift, while larger gaps keep three guard positions and a sticky bit below the higher operand. The signed magnitudes are combined and rounded once to nearest even, and the normal result is packed into storage words. Every intermediate fits two words because an eligible significand has at most 126 bits. Refinement proofs live in Addition.Proof.

The kernel returns none for exceptional or zero operands, a sticky alignment whose higher operand is subnormal, a magnitude below the normal threshold before rounding, and overflow after rounding. Exact cancellation returns positive zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.alignOffset (fmt : FloatFormat) : UInt64

Offset from a compact finite scale to the product rounder's coordinate: fmt.exponentBias + fmt.fracWidth - 1, the value of FiniteKernel.finiteScaleOffset fmt.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.shiftLimit (fmt : FloatFormat) : UInt64

Largest alignment shift that is done exactly, by a left shift. A significand has at most fracWidth + 1 bits, so shifting it left by 126 - fracWidth keeps it below 2 ^ 127 and the same-sign sum of two significands below 2 ^ 128.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.finishWords? (fmt : FloatFormat) (sign : Bool) (position : UInt64) (rounded : Numerics.FixedWord.UInt128) : Option Numerics.FixedWord.UInt128

Finish a rounded two-word significand already in the normal range: normalize a rounding carry, decline overflow, and pack the storage words.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundMagnitudeWords? (fmt : FloatFormat) (offset : UInt64) (sign : Bool) (magnitude : Numerics.FixedWord.UInt128) (scale : UInt64) : Option Numerics.FixedWord.UInt128

Round a nonzero two-word magnitude at an unsigned scale to the storage words of a normal result, or decline.

An accepted result decodes to FiniteScaleAdd.roundMagnitude fmt offset sign magnitude scale. Addition passes alignOffset fmt, so its scales are compact finite scales, and fused multiply-add passes 0. The magnitude is rounded to fracWidth + 1 bits with ties to even, and carry, overflow, and packing follow FiniteProductRound.round. Magnitudes below the normal threshold and results that overflow return none.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundAlignedWords? (fmt : FloatFormat) (offset : UInt64) (leftSign rightSign : Bool) (left right : Numerics.FixedWord.UInt128) (scale : UInt64) : Option Numerics.FixedWord.UInt128

Combine two nonzero signed magnitudes aligned at one scale and round once.

Its branches are those of FiniteScaleAdd.roundMagnitudes. Same-sign callers keep left + right below 2 ^ 128. Exact cancellation of opposite signs is positive zero.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.jammedMagnitudeWords (sameSign : Bool) (high low : Numerics.FixedWord.UInt128) (gap : UInt64) : Numerics.FixedWord.UInt128

The sticky magnitude for a higher-scale significand high and a lower low that lie gap ≥ 3 scale positions apart: high shifted left by three guard positions, combined with low shifted right by gap - 3, with the lowest bit set when that shift discards a nonzero bit.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundJammedWords? (fmt : FloatFormat) (offset : UInt64) (highSign lowSign : Bool) (high low : Numerics.FixedWord.UInt128) (gap scale : UInt64) : Option Numerics.FixedWord.UInt128

Round the signed sum of a significand high with at least fracWidth + 1 bits and a lower low that lie gap scale positions apart, through jammedMagnitudeWords at scale scale + (gap - 3). Callers keep low at most 2 ^ (fracWidth + gap - 1). A high below the implicit bit or at least 2 ^ 124, and gaps below three, decline. The 2 ^ 124 bound keeps the same-sign sticky sum below 2 ^ 128.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.addFieldsWords? (fmt : FloatFormat) (xSign : Bool) (xExponent : UInt64) (xMantissa : Numerics.FixedWord.UInt128) (ySign : Bool) (yExponent : UInt64) (yMantissa : Numerics.FixedWord.UInt128) : Option Numerics.FixedWord.UInt128

Add two decoded finite operands in two-word arithmetic, or decline.

Each operand is a sign, its stored biased exponent, and its two-word significand including the implicit bit of a normal value. Zero operands return none.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.finiteMantissaWords (fmt : FloatFormat) (exponent high low : UInt64) : Numerics.FixedWord.UInt128

The two-word significand of a finite value: its fraction, with the implicit bit when normal.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.addFiniteWords? (fmt : FloatFormat) (x y : Numerics.FixedWord.UInt128) (negateRight : Bool) : Option Numerics.FixedWord.UInt128

Two-word finite addition, or subtraction when negateRight is set, on storage words.

An exceptional operand (an all-ones exponent field) returns none. The right operand's sign is toggled by negateRight. Addition.Proof.addFiniteWords_refines relates every accepted result to FiniteKernel.add?.

Model entry points

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.addFinite? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Evaluate finite two-word addition on model values.

The storage-word kernel runs first. Every remaining finite case uses the width-generic exact kernel, and exceptional inputs return none to the operation dispatcher. @[specialize fmt] lets descriptor-dependent constants simplify at closed-format call sites without asking callers to inline this candidate chain.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.subFinite? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Evaluate finite two-word subtraction on model values.

The storage-word kernel toggles the right sign. Every remaining finite case uses generic exact addition with a negated right operand, and exceptional inputs return none to the dispatcher.