Two-word addition runtime

The two-word addition runtime combines the same-exponent kernel with a complete finite candidate chain for every eligible layout. Correctness theorems are isolated in Addition.Proof.

@[inline]

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

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

The two largest exponent fields are rejected so incrementing the accepted exponent always remains finite. The sum of two fracWidth + 1-bit significands fits in the two-word accumulator.

@[specialize #[0]]

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

Evaluate finite two-word addition.

The fixed-limb same-exponent kernel is attempted first. Every remaining finite case uses the width-generic exact kernel; exceptional inputs are reported as none to the operation dispatcher. The @[specialize fmt] annotation enables descriptor-dependent constants to be simplified at closed-format call sites without requesting that callers inline this candidate chain.