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) (offset : UInt64) (sign : Bool) (magnitude scale : UInt64) (hmagnitude : magnitude ≠ 0) (hscale : scale.toNat + offset.toNat < 2 ^ 62) : roundMagnitude? fmt offset sign magnitude scale = normalSpec? fmt sign magnitude.toNat (scale.toNat + offset.toNat)

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

With a nonzero magnitude and a scale bounded by the exponent range, 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) (offset : UInt64) (sign : Bool) (magnitude scale : UInt64) (hmagnitude : magnitude ≠ 0) (hscale : scale.toNat + offset.toNat < 2 ^ 62) (result : Model fmt) (hresult : roundMagnitude? fmt offset sign magnitude scale = some result) : result = FiniteScaleAdd.roundMagnitude fmt offset.toNat 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) (offset : UInt64) (leftSign rightSign : Bool) (left right scale : UInt64) (hleft : left ≠ 0) (hright : right ≠ 0) (hsum : left.toNat + right.toNat < 2 ^ 64) (hscale : scale.toNat + offset.toNat < 2 ^ 62) (result : Model fmt) (hresult : roundAligned? fmt offset leftSign rightSign left right scale = some result) : result = FiniteScaleAdd.roundMagnitudes fmt offset.toNat 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.

Sticky alignment for large scale gaps

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.alignedMagnitude_lower (width high low gap : ℕ) (sameSign : Bool) (hhighLower : 2 ^ width ≤ high) (hlow : low ≤ 2 ^ (width + gap - 1)) (hgap : 3 ≤ gap) : 2 ^ (width + gap - 1) ≤ if sameSign = true then high * 2 ^ gap + low else high * 2 ^ gap - low

With a normal larger significand and a small enough lower operand, the exact aligned magnitude has its leading bit at least at width + gap - 1.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundMagnitude_shiftRightJam (fmt : FloatFormat) (roundOffset : ℕ) (highSign lowSign : Bool) (high low gap scale : ℕ) (hhighLower : 2 ^ fmt.fracWidth ≤ high) (hlow : low ≤ 2 ^ (fmt.fracWidth + gap - 1)) (hgap : 3 ≤ gap) : roundMagnitude fmt roundOffset highSign (Numerics.shiftRightJam (if (highSign == lowSign) = true then high * 2 ^ gap + low else high * 2 ^ gap - low) (gap - 3)) (scale + (gap - 3)) = roundMagnitudes fmt roundOffset highSign lowSign (high <<< gap) low scale

With a normal larger significand, three guard positions and a sticky bit round like the exact sum: the exact magnitude keeps at least fracWidth + 2 bits above the jammed positions.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundJammed_refines (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (hexpWidth : fmt.expWidth ≤ 30) (hfracWidth : fmt.fracWidth ≤ 61) (offset : UInt64) (highSign lowSign : Bool) (high low gap scale : UInt64) (hlow : low.toNat ≤ 2 ^ (fmt.fracWidth + gap.toNat - 1)) (hlowNe : low ≠ 0) (hscale : scale.toNat + gap.toNat + offset.toNat < 2 ^ 62) (result : Model fmt) (hresult : roundJammed? fmt offset highSign lowSign high low gap scale = some result) : result = FiniteScaleAdd.roundMagnitudes fmt offset.toNat highSign lowSign (high.toNat <<< gap.toNat) low.toNat scale.toNat

An accepted sticky alignment is the exact signed-magnitude combination of the same fields.

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.

With negateRight set the kernel toggles the right sign in machine words, and the theorem states the claim for neg y. Declines fall outside the statement, and the dispatcher handles them with the exact implementation. Only the capacity contract Eligible is assumed of the format.

Storage-word entry points

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.ofWord_zeroWord {fmt : FloatFormat} (hwidth : fmt.bitWidth ≤ 64) (sign : Bool) : NativeSmallWord.ofWord (zeroWord fmt sign) = zero fmt sign

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundMagnitude?_eq_map (fmt : FloatFormat) (offset : UInt64) (sign : Bool) (magnitude scale : UInt64) : roundMagnitude? fmt offset sign magnitude scale = Option.map NativeSmallWord.ofWord (roundMagnitudeWord? fmt offset sign magnitude scale)

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundAligned?_eq_map {fmt : FloatFormat} (hwidth : fmt.bitWidth ≤ 64) (offset : UInt64) (leftSign rightSign : Bool) (left right scale : UInt64) : roundAligned? fmt offset leftSign rightSign left right scale = Option.map NativeSmallWord.ofWord (roundAlignedWord? fmt offset leftSign rightSign left right scale)

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.roundJammed?_eq_map (fmt : FloatFormat) (offset : UInt64) (highSign lowSign : Bool) (high low gap scale : UInt64) : roundJammed? fmt offset highSign lowSign high low gap scale = Option.map NativeSmallWord.ofWord (roundJammedWord? fmt offset highSign lowSign high low gap scale)

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.addFields?_eq_map {fmt : FloatFormat} (hwidth : fmt.bitWidth ≤ 64) (xSign : Bool) (xExponent xMantissa : UInt64) (ySign : Bool) (yExponent yMantissa : UInt64) : addFields? fmt xSign xExponent xMantissa ySign yExponent yMantissa = Option.map NativeSmallWord.ofWord (addFieldsWord? fmt xSign xExponent xMantissa ySign yExponent yMantissa)

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordAdd.addFinite?_ofWord {fmt : FloatFormat} (hwidth : fmt.bitWidth ≤ 64) {xBits yBits : UInt64} (hx : xBits.toNat < 2 ^ fmt.bitWidth) (hy : yBits.toNat < 2 ^ fmt.bitWidth) (negateRight : Bool) : addFinite? (NativeSmallWord.ofWord xBits) (NativeSmallWord.ofWord yBits) negateRight = Option.map NativeSmallWord.ofWord (addFiniteWord? fmt xBits yBits negateRight)

On storage words below the radix, addFinite? is the ofWord image of addFiniteWord?.