Correctness of native one-word finite addition

Under Eligible, every accepted result of Add.Runtime agrees with the exact finite kernel. addFinite_refines also covers subtraction by identifying the toggled right sign with neg y. A declined input is handled by the dispatcher's generic fallback.

normalSpec? describes the normal branch of FiniteProductRound.round. The proof transfers native rounding to this specification using the shared carry and packing theorem NativeWordProduct.finish_eq, then treats signed magnitudes, exponent alignment, and decoding.

Natural-number specification of the normal rounding path

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

The normal branch of FiniteProductRound.round, declining instead of producing a subnormal or an infinite result.

For a nonzero magnitude, this rounds the value with sign sign and magnitude magnitude * 2 ^ (scale - 2 * ieeeSubnormalAlignExp fmt), interpreting subtraction in Int. normalSpec_refines identifies each accepted answer with the total product rounder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.normalSpec_refines (fmt : FloatFormat) (sign : Bool) (magnitude scale : ℕ) (hmagnitude : magnitude ≠ 0) (result : Model fmt) (hresult : normalSpec? fmt sign magnitude scale = some result) : result = FiniteProductRound.round fmt sign magnitude scale

A some answer of the normal specification is the arbitrary-precision rounder's result.

Machine-word rounding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.alignOffset_toNat (fmt : FloatFormat) (hexpWidth : fmt.expWidth ≤ 30) (hfracWidth : fmt.fracWidth ≤ 61) : (alignOffset fmt).toNat = fmt.exponentBias + fmt.fracWidth - 1

The alignment offset is exact when expWidth ≤ 30 and fracWidth ≤ 61.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.shiftLimit_toNat (fmt : FloatFormat) (hfracWidth : fmt.fracWidth ≤ 61) : (shiftLimit fmt).toNat = 62 - fmt.fracWidth

The alignment shift limit is exact when fracWidth ≤ 61.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundMagnitude_eq_normalSpec (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (hexpWidth : fmt.expWidth ≤ 30) (hfracWidth : fmt.fracWidth ≤ 61) (sign : Bool) (magnitude scale : UInt64) (hmagnitude : magnitude ≠ 0) (hscale : scale.toNat < 2 ^ 31) : roundMagnitude? fmt sign magnitude scale = normalSpec? fmt sign magnitude.toNat (scale.toNat + (fmt.exponentBias + fmt.fracWidth - 1))

The machine-word rounder computes the natural-number normal specification.

The magnitude is nonzero and the scale is bounded by the exponent range, so no intermediate position, shift, or increment wraps around the word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundMagnitude_refines (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (hexpWidth : fmt.expWidth ≤ 30) (hfracWidth : fmt.fracWidth ≤ 61) (sign : Bool) (magnitude scale : UInt64) (hmagnitude : magnitude ≠ 0) (hscale : scale.toNat < 2 ^ 31) (result : Model fmt) (hresult : roundMagnitude? fmt sign magnitude scale = some result) : result = FiniteScaleAdd.roundMagnitude fmt (FiniteKernel.finiteScaleOffset fmt) sign magnitude.toNat scale.toNat

An accepted machine-word rounding is the unsigned-scale rounding of the exact kernel.

Signed magnitudes and alignment

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundAligned_refines (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (hexpWidth : fmt.expWidth ≤ 30) (hfracWidth : fmt.fracWidth ≤ 61) (leftSign rightSign : Bool) (left right scale : UInt64) (hleft : left ≠ 0) (hright : right ≠ 0) (hsum : left.toNat + right.toNat < 2 ^ 64) (hscale : scale.toNat < 2 ^ 31) (result : Model fmt) (hresult : roundAligned? fmt leftSign rightSign left right scale = some result) : result = FiniteScaleAdd.roundMagnitudes fmt (FiniteKernel.finiteScaleOffset fmt) leftSign rightSign left.toNat right.toNat scale.toNat

An accepted aligned combination is the exact kernel's signed-magnitude combination.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.finiteScale_toNat_eq_scale (exponent : UInt64) : (Numerics.FixedWord.finiteScale exponent).toNat = FiniteKernel.scale exponent.toNat

The machine-word finite scale is the compact finite scale of the exact kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.addFields_refines (fmt : FloatFormat) (hieee : fmt.isIEEE = true) (hwidth : fmt.bitWidth ≤ 64) (hexpWidth : fmt.expWidth ≤ 30) (hfracWidth : fmt.fracWidth ≤ 61) (xSign : Bool) (xExponent xMantissa : UInt64) (ySign : Bool) (yExponent yMantissa : UInt64) (hxExponent : xExponent.toNat < 2 ^ fmt.expWidth) (hyExponent : yExponent.toNat < 2 ^ fmt.expWidth) (hxMantissa : xMantissa.toNat < 2 ^ (fmt.fracWidth + 1)) (hyMantissa : yMantissa.toNat < 2 ^ (fmt.fracWidth + 1)) (result : Model fmt) (hresult : addFields? fmt xSign xExponent xMantissa ySign yExponent yMantissa = some result) : result = FiniteKernel.addFields fmt xSign xExponent.toNat xMantissa.toNat ySign yExponent.toNat yMantissa.toNat

An accepted field addition is the exact unsigned-scale sum of the same fields.

The exponent bounds keep every scale below 2 ^ 31 and the significand bounds keep the aligned same-sign sum below 2 ^ 64, which is all the machine-word transfer needs.

Storage-word decoding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.decode_of_finite {fmt : FloatFormat} (hieee : fmt.isIEEE = true) (hwidth : fmt.bitWidth ≤ 64) (x : Model fmt) (hfinite : NativeSmallWord.exponentField fmt (NativeSmallWord.toWord x) ≠ NativeSmallWord.exponentMask fmt) : FiniteKernel.decode? x = some { sign := NativeSmallWord.signField fmt (NativeSmallWord.toWord x), exponent := (NativeSmallWord.exponentField fmt (NativeSmallWord.toWord x)).toNat, mantissa := (NativeSmallWordFinite.finiteMantissa fmt (NativeSmallWord.exponentField fmt (NativeSmallWord.toWord x)) (NativeSmallWord.fractionField fmt (NativeSmallWord.toWord x))).toNat }

The generic finite decoder sees the fields the one-word kernel extracts from a finite word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.decode_neg_of_finite {fmt : FloatFormat} (hieee : fmt.isIEEE = true) (hwidth : fmt.bitWidth ≤ 64) (y : Model fmt) (hfinite : NativeSmallWord.exponentField fmt (NativeSmallWord.toWord y) ≠ NativeSmallWord.exponentMask fmt) : FiniteKernel.decode? y.neg = some { sign := !NativeSmallWord.signField fmt (NativeSmallWord.toWord y), exponent := (NativeSmallWord.exponentField fmt (NativeSmallWord.toWord y)).toNat, mantissa := (NativeSmallWordFinite.finiteMantissa fmt (NativeSmallWord.exponentField fmt (NativeSmallWord.toWord y)) (NativeSmallWord.fractionField fmt (NativeSmallWord.toWord y))).toNat }

Negating a finite word keeps its exponent and fraction fields and toggles its sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.exponentField_toNat_lt {fmt : FloatFormat} (hwidth : fmt.bitWidth ≤ 64) (x : Model fmt) : (NativeSmallWord.exponentField fmt (NativeSmallWord.toWord x)).toNat < 2 ^ fmt.expWidth

The exponent field of a one-word value is a stored exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.finiteMantissa_toNat_lt {fmt : FloatFormat} (hwidth : fmt.bitWidth ≤ 64) (x : Model fmt) : (NativeSmallWordFinite.finiteMantissa fmt (NativeSmallWord.exponentField fmt (NativeSmallWord.toWord x)) (NativeSmallWord.fractionField fmt (NativeSmallWord.toWord x))).toNat < 2 ^ (fmt.fracWidth + 1)

The finite significand of a one-word value has at most fracWidth + 1 bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.addFinite_refines {fmt : FloatFormat} (heligible : Eligible fmt) (x y result : Model fmt) (negateRight : Bool) (hresult : addFinite? x y negateRight = some result) : FiniteKernel.add? x (if negateRight = true then y.neg else y) = some result

An accepted one-word addition, or subtraction, is the exact compact finite kernel's answer.

negateRight selects subtraction: the kernel toggled the right sign in machine words, and the theorem states the corresponding claim about neg y. Every decline is outside the statement; the dispatcher uses the exact implementation for it. The hypothesis is the kernel's own capacity contract Eligible: IEEE encoding, at most 64 total bits, at most 30 exponent bits, and at most 61 fraction bits.