Correctness of native one-word finite fused multiply-add

Under Eligible, every accepted result of Fma.Runtime agrees with the exact finite kernel. fmaFields_refines matches the four alignment branches of fmaFields? with FiniteScaleAdd.roundSum at round offset 0, reusing the one-word addition lemmas for the rounder, the aligned combination, and the sticky alignment. fmaFinite_refines then identifies the decoded fields with the IEEE branch of FiniteKernel.Internal.fmaComponents.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFma.productShiftLimit_toNat (fmt : FloatFormat) (hfracWidth : fmt.fracWidth ≤ 29) : (productShiftLimit fmt).toNat = 61 - 2 * fmt.fracWidth

The product shift limit is exact when fracWidth ≤ 29.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFma.fmaFields_refines (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (hexpWidth : fmt.expWidth ≤ 30) (hfracWidth : fmt.fracWidth ≤ 29) (productSign : Bool) (product productScale : UInt64) (addendSign : Bool) (addend addendScale : UInt64) (hproduct : product.toNat < 2 ^ (2 * fmt.fracWidth + 2)) (haddend : addend.toNat < 2 ^ (fmt.fracWidth + 1)) (hproductScale : productScale.toNat < 2 ^ 33) (haddendScale : addendScale.toNat < 2 ^ 33) (result : Model fmt) (hresult : fmaFields? fmt productSign product productScale addendSign addend addendScale = some result) : result = 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 product has at most 2 * fracWidth + 2 bits, the addend at most fracWidth + 1, and both scales are below 2 ^ 33. The machine-word transfer needs nothing else.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordFma.fmaFinite_refines {fmt : FloatFormat} (heligible : Eligible fmt) (x y z result : Model fmt) (hresult : fmaFinite? x y z = some result) : FiniteKernel.fma? x y z = some result

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

Declines fall outside the statement, and the dispatcher handles them with the native-storage component kernel or the exact implementation. Only the capacity contract Eligible is assumed of the format.