Correctness of two-word finite addition

Under Eligible, every accepted result of Addition.Runtime is the exact finite kernel's answer. The proof follows the one-word addition proof NativeSmallWordAdd: the two-word rounder computes the natural-number normal specification NativeSmallWordAdd.normalSpec?, the aligned and sticky combinations match FiniteScaleAdd.roundMagnitudes, and the decoded storage fields are those of FiniteKernel.decode?. The natural-number lemmas about sticky alignment are shared with the one-word kernel.

Constants

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.alignOffset_toNat {fmt : FloatFormat} (h : Eligible fmt) : (alignOffset fmt).toNat = FiniteKernel.finiteScaleOffset fmt

alignOffset equals FiniteKernel.finiteScaleOffset as a natural number.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.shiftLimit_toNat {fmt : FloatFormat} (h : Eligible fmt) : (shiftLimit fmt).toNat = 126 - fmt.fracWidth

shiftLimit equals 126 - fracWidth as a natural number.

Rounding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.finishWords_eq {fmt : FloatFormat} (h : Eligible fmt) (sign : Bool) (position : UInt64) (rounded : Numerics.FixedWord.UInt128) (positionNat roundedNat : ℕ) (hposition : position.toNat = positionNat) (hpositionAdd : (position + 1).toNat = positionNat + 1) (hrounded : rounded.toNat = roundedNat) (hnormal : fmt.bias + 2 * fmt.fracWidth - 1 ≤ positionNat) (hroundedLower : 2 ^ fmt.fracWidth ≤ roundedNat) (hroundedUpper : roundedNat ≤ 2 ^ (fmt.fracWidth + 1)) : Option.map (ofWords fmt) (finishWords? fmt sign position rounded) = let carry := roundedNat = pow2 (fmt.fracWidth + 1); have normalizedPosition := if carry then positionNat + 1 else positionNat; if 3 * fmt.bias + 2 * fmt.fracWidth - 2 < normalizedPosition then none else have normalizedMantissa := if carry then pow2 fmt.fracWidth else roundedNat; some (ofFields fmt sign (normalizedPosition - (fmt.bias + 2 * fmt.fracWidth - 2)) (normalizedMantissa - pow2 fmt.fracWidth))

Carry normalization, overflow, and packing agree with the generic rounder's normal branch.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundMagnitudeWords_eq_normalSpec {fmt : FloatFormat} (h : Eligible fmt) (offset : UInt64) (sign : Bool) (magnitude : Numerics.FixedWord.UInt128) (scale : UInt64) (hmagnitude : magnitude.toNat ≠ 0) (hscale : scale.toNat + offset.toNat < 2 ^ 63) : Option.map (ofWords fmt) (roundMagnitudeWords? fmt offset sign magnitude scale) = NativeSmallWordAdd.normalSpec? fmt sign magnitude.toNat (scale.toNat + offset.toNat)

The two-word rounder computes the natural-number normal specification of the one-word kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundMagnitudeWords_refines {fmt : FloatFormat} (h : Eligible fmt) (offset : UInt64) (sign : Bool) (magnitude : Numerics.FixedWord.UInt128) (scale : UInt64) (hmagnitude : magnitude.toNat ≠ 0) (hscale : scale.toNat + offset.toNat < 2 ^ 63) (words : Numerics.FixedWord.UInt128) (hresult : roundMagnitudeWords? fmt offset sign magnitude scale = some words) : ofWords fmt words = FiniteScaleAdd.roundMagnitude fmt offset.toNat sign magnitude.toNat scale.toNat

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

Signed magnitudes

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.ofWords_zero {fmt : FloatFormat} : ofWords fmt { hi := 0, lo := 0 } = zero fmt false

All-zero storage words are positive zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundAlignedWords_refines {fmt : FloatFormat} (h : Eligible fmt) (offset : UInt64) (leftSign rightSign : Bool) (left right : Numerics.FixedWord.UInt128) (scale : UInt64) (hright : right.toNat ≠ 0) (hsum : left.toNat + right.toNat < 2 ^ 128) (hscale : scale.toNat + offset.toNat < 2 ^ 63) (words : Numerics.FixedWord.UInt128) (hresult : roundAlignedWords? fmt offset leftSign rightSign left right scale = some words) : ofWords fmt words = 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.

Sticky alignment

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundJammedWords_refines {fmt : FloatFormat} (h : Eligible fmt) (offset : UInt64) (highSign lowSign : Bool) (high low : Numerics.FixedWord.UInt128) (gap scale : UInt64) (hlow : low.toNat ≤ 2 ^ (fmt.fracWidth + gap.toNat - 1)) (hlowNe : low.toNat ≠ 0) (hscale : scale.toNat + gap.toNat + offset.toNat < 2 ^ 63) (words : Numerics.FixedWord.UInt128) (hresult : roundJammedWords? fmt offset highSign lowSign high low gap scale = some words) : ofWords fmt words = 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.

Field addition

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.addFieldsWords_refines {fmt : FloatFormat} (h : Eligible fmt) (xSign : Bool) (xExponent : UInt64) (xMantissa : Numerics.FixedWord.UInt128) (ySign : Bool) (yExponent : UInt64) (yMantissa : Numerics.FixedWord.UInt128) (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)) (words : Numerics.FixedWord.UInt128) (hresult : addFieldsWords? fmt xSign xExponent xMantissa ySign yExponent yMantissa = some words) : ofWords fmt words = FiniteKernel.addFields fmt xSign xExponent.toNat xMantissa.toNat ySign yExponent.toNat yMantissa.toNat

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

Storage-word decoding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.finiteMantissaWords_toNat {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) : (finiteMantissaWords fmt (expField fmt (toWords x).hi) (toWords x).hi (toWords x).lo).toNat = FiniteKernel.decodeMantissa fmt x.expField x.fracField

The two-word significand of a stored value is the generic kernel's decoded significand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.finiteMantissaWords_lt {fmt : FloatFormat} (h : Eligible fmt) (exponent high low : UInt64) : (finiteMantissaWords fmt exponent high low).toNat < 2 ^ (fmt.fracWidth + 1)

A decoded two-word significand has at most fracWidth + 1 bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.decode_of_finite {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) (hfinite : expField fmt (toWords x).hi ≠ expAllOnes fmt) : FiniteKernel.decode? x = some { sign := signBit fmt (toWords x).hi, exponent := (expField fmt (toWords x).hi).toNat, mantissa := (finiteMantissaWords fmt (expField fmt (toWords x).hi) (toWords x).hi (toWords x).lo).toNat }

The generic finite decoder sees the fields the two-word kernel reads from the storage words.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.decode_neg_of_finite {fmt : FloatFormat} (h : Eligible fmt) (y : Model fmt) (hfinite : expField fmt (toWords y).hi ≠ expAllOnes fmt) : FiniteKernel.decode? y.neg = some { sign := !signBit fmt (toWords y).hi, exponent := (expField fmt (toWords y).hi).toNat, mantissa := (finiteMantissaWords fmt (expField fmt (toWords y).hi) (toWords y).hi (toWords y).lo).toNat }

Negating a finite value keeps its stored exponent and significand and toggles its sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.addFiniteWords_refines {fmt : FloatFormat} (h : Eligible fmt) (x y : Model fmt) (negateRight : Bool) (words : Numerics.FixedWord.UInt128) (hresult : addFiniteWords? fmt (toWords x) (toWords y) negateRight = some words) : FiniteKernel.add? x (if negateRight = true then y.neg else y) = some (ofWords fmt words)

An accepted two-word sum or difference is the answer of the compact finite kernel FiniteKernel.add?.

negateRight selects subtraction: the kernel toggles the right sign on the storage word, and the theorem states the corresponding claim about neg y.

Model entry points

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.addFinite?_of_words {fmt : FloatFormat} (x y : Model fmt) (words : Numerics.FixedWord.UInt128) (h : addFiniteWords? fmt (toWords x) (toWords y) false = some words) : addFinite? x y = some (ofWords fmt words)

An accepted storage-word sum is the model-level two-word sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.subFinite?_of_words {fmt : FloatFormat} (x y : Model fmt) (words : Numerics.FixedWord.UInt128) (h : addFiniteWords? fmt (toWords x) (toWords y) true = some words) : subFinite? x y = some (ofWords fmt words)

An accepted storage-word difference is the model-level two-word difference.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.addFinite_eq {fmt : FloatFormat} (h : Eligible fmt) (x y : Model fmt) : addFinite? x y = FiniteKernel.add? x y

Two-word addition and the generic finite kernel agree on every input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.subFinite_eq {fmt : FloatFormat} (h : Eligible fmt) (x y : Model fmt) : subFinite? x y = FiniteKernel.add? x y.neg

Two-word subtraction and generic addition of the negated right operand agree.