Correctness of two-word fused multiply-add

Every accepted result of Fma.Runtime is the exact finite kernel's answer. The proof follows the one-word FMA proof: fmaFieldsWords_refines matches the alignment branches of fmaFieldsWords? with FiniteScaleAdd.roundSum at round offset 0. Four-word magnitudes are reduced to two words with normalizeJam128, which FiniteProductRound.round_shiftRightJam shows does not change the rounding, and then go through the two-word rounder of Addition.Proof. The sticky alignments reuse the natural-number lemmas of the one-word addition kernel.

Rounding four-word magnitudes

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

A four-word magnitude rounds like its sticky two-word normalization.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundAlignedProductWords_refines {fmt : FloatFormat} (h : Eligible fmt) (leftSign rightSign : Bool) (left right : Numerics.FixedWord.UInt256) (scale : UInt64) (hright : right.toNat ≠ 0) (hsum : left.toNat + right.toNat < 2 ^ 256) (hscale : scale.toNat < 2 ^ 62) (words : Numerics.FixedWord.UInt128) (hresult : roundAlignedProductWords? fmt leftSign rightSign left right scale = some words) : ofWords fmt words = FiniteScaleAdd.roundMagnitudes fmt 0 leftSign rightSign left.toNat right.toNat scale.toNat

An accepted aligned four-word combination is the exact signed-magnitude combination.

Sticky alignments

Field fused multiply-add

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fmaFieldsWords_refines {fmt : FloatFormat} (h : Eligible fmt) (hfracWidth : fmt.fracWidth ≤ 120) (productSign : Bool) (product : Numerics.FixedWord.UInt256) (productScale : UInt64) (addendSign : Bool) (addend : Numerics.FixedWord.UInt128) (addendScale : UInt64) (hproduct : product.toNat < 2 ^ (2 * fmt.fracWidth + 2)) (haddend : addend.toNat < 2 ^ (fmt.fracWidth + 1)) (hproductScale : productScale.toNat < 2 ^ 34) (haddendScale : addendScale.toNat < 2 ^ 34) (words : Numerics.FixedWord.UInt128) (hresult : fmaFieldsWords? fmt productSign product productScale addendSign addend addendScale = some words) : ofWords fmt words = FiniteScaleAdd.roundSum fmt 0 productSign addendSign product.toNat productScale.toNat addend.toNat addendScale.toNat

An accepted field FMA is the exact kernel's rounded sum of the product and the addend.

The hypotheses give the product at most 2 * fracWidth + 2 bits and the addend at most fracWidth + 1, with both scales below 2 ^ 34 and at most 120 fraction bits.

Storage words and model entry points

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fmaFiniteWords_refines {fmt : FloatFormat} (h : Eligible fmt) (x y z : Model fmt) (words : Numerics.FixedWord.UInt128) (hresult : fmaFiniteWords? fmt (toWords x) (toWords y) (toWords z) = some words) : FiniteKernel.fma? x y z = some (ofWords fmt words)

An accepted two-word FMA is the exact compact finite kernel's answer.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fmaFinite?_of_words {fmt : FloatFormat} (x y z : Model fmt) (words : Numerics.FixedWord.UInt128) (hwords : fmaFiniteWords? fmt (toWords x) (toWords y) (toWords z) = some words) : fmaFinite? x y z = some (ofWords fmt words)

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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fmaFinite_eq {fmt : FloatFormat} (h : Eligible fmt) (x y z : Model fmt) : fmaFinite? x y z = FiniteKernel.fma? x y z

Two-word fused multiply-add and the generic finite kernel agree on every input.