Correctness of two-word fused multiply-add

The specialized path accepts normal operands when the product and addend have the same sign and the addend's scale is exactly the product scale plus fracWidth. Their sum fits in a UInt256 accumulator and is rounded once using the product rounder.

fmaNormalSameSignAligned_refines identifies accepted results with the generic finite kernel. fmaFinite_eq extends the equality to the complete candidate chain, which uses the generic implementation on all other inputs. Runtime clients can import Fma.Runtime separately.

Fixed-limb representation lemmas

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.addendOffset_toNat {fmt : FloatFormat} (h : Eligible fmt) : (UInt64.ofNat (fmt.bias + fmt.fracWidth - 1)).toNat = fmt.bias + fmt.fracWidth - 1

The scale offset of the addend fits a native word.

Normalization and nearest-even rounding

Equal-sign aligned fast path

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fmaNormalSameSignAligned_refines {fmt : FloatFormat} (h : Eligible fmt) (x y z result : Model fmt) (hresult : fmaNormalSameSignAligned? x y z = some result) : FiniteKernel.fma? x y z = some result

Every result accepted by the aligned pair FMA kernel equals the exact finite kernel.

Complete finite dispatcher

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

The two-word finite FMA chain equals the width-generic exact finite kernel.