Native one-word finite addition

The native addition path serves conventional IEEE formats whose storage word, exponent range, and aligned significand sum fit in UInt64 (Eligible). It is the word-tier counterpart of the arbitrary-precision kernel FiniteScaleAdd.roundSum: both operands are decoded from the storage word into a sign, a nonnegative scale, and an integer significand; the significands are aligned by a left shift; the signed magnitudes are combined; and the result is rounded to nearest even and packed. Significand arithmetic uses UInt64; format coordinates and shift counts also use Nat. Refinement proofs live in Add.Proof.

The kernel returns none for exceptional or zero operands, alignment shifts exceeding the word budget, a magnitude below the normal threshold before rounding, or overflow after rounding. The dispatcher then uses the exact generic implementation. Exact cancellation is accepted and returns positive zero.

The functions mirror the branch structure of FiniteScaleAdd.roundMagnitudes and FiniteScaleAdd.roundSum step for step. Keeping the two shapes aligned is what makes the refinement proof a transfer of natural-number values through UInt64.toNat.

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.Eligible (fmt : FloatFormat) : Prop

Capacity contract of the one-word addition kernel.

The IEEE condition selects the exact binary semantics. The width bounds keep every storage word, scale, and aligned significand in UInt64: a significand has at most fracWidth + 1 ≤ 62 bits, so the same-sign sum of two aligned significands fits after any alignment shift accepted by shiftLimit. These bounds include binary64; formats with more than 30 exponent bits are excluded.

@[instance_reducible, inline]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.instDecidableEligible (fmt : FloatFormat) : Decidable (Eligible fmt)

Addition eligibility is decided from the descriptor fields; the conditional form is inlined and can be simplified for a closed format (see NativeSmallWord.StorageEligible).

@[inline]

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

Nonnegative scale offset separating the compact finite scale from the product rounder's coordinate: fmt.exponentBias + fmt.fracWidth - 1, the value of FiniteKernel.finiteScaleOffset fmt as one machine word.

For every format that fits one machine word this constant is exact because the bias is below 2 ^ expWidth.

@[inline]

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

Largest exponent-alignment shift the one-word kernel accepts.

A significand has at most fracWidth + 1 bits. Shifting the larger-scale operand left by at most 62 - fracWidth bits keeps it below 2 ^ 63, so the same-sign sum of both significands is still below 2 ^ 64 and no machine-word addition can wrap. Larger shifts decline to the exact kernel.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundMagnitude? (fmt : FloatFormat) (sign : Bool) (magnitude scale : UInt64) : Option (Model fmt)

Round a nonzero magnitude at an unsigned scale to a normal result, or decline.

The exact magnitude is magnitude * 2 ^ (scale - offset), where offset = fmt.exponentBias + fmt.fracWidth - 1 and subtraction is in Int; sign supplies its sign. This is the coordinate of FiniteScaleAdd.roundMagnitude. The function reproduces the normal branch of FiniteProductRound.round in machine words: it finds the leading bit, rounds the significand to fracWidth + 1 bits with ties to even, and hands carry, overflow, and packing to the shared NativeWordProduct.finish?. Magnitudes below the normal threshold before rounding and values that overflow after rounding return none.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundAligned? (fmt : FloatFormat) (leftSign rightSign : Bool) (left right scale : UInt64) : Option (Model fmt)

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

The four branches are those of FiniteScaleAdd.roundMagnitudes: same signs add the magnitudes, equal opposite magnitudes cancel to positive zero, and otherwise the larger magnitude determines the sign of the difference. Same-sign callers must keep left + right below 2 ^ 64; opposite-sign subtraction cannot wrap.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.addFields? (fmt : FloatFormat) (xSign : Bool) (xExponent xMantissa : UInt64) (ySign : Bool) (yExponent yMantissa : UInt64) : Option (Model fmt)

Add two decoded finite operands in machine words, or decline.

Each operand is a sign, its stored biased exponent, and its integer significand including the implicit bit of a normal value. The scales are the compact finite scales of FiniteKernel.scale, so the operand with the larger scale is shifted left before the signed magnitudes are combined. Zero operands and alignment shifts above shiftLimit fmt return none; the exact kernel handles them.

@[inline]

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

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

Both operands are decoded with the shared one-word field extractors. An exceptional operand (an all-ones exponent field) returns none. The right operand's sign is toggled by negateRight, so subtraction never materializes a negated model value. Every accepted result is proved equal to FiniteKernel.add? x y, respectively FiniteKernel.add? x (neg y), in Add.Proof.