Verified wide-limb fused multiply-add

An accepted result is the compact finite kernel FiniteKernel.fma? on the operand models (fmaNormal?_refines): the exact limb product is the product of the decoded significands, and the alignment core computes the unsigned-scale exact sum FiniteScaleAdd.roundSum that FiniteKernel.fmaComponentsImpl evaluates. toModel_fma then closes with the reference operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.fmaNormal?_refines {fmt : FloatFormat} (h : Eligible fmt) (x y z r : Value fmt) (hr : fmaNormal? fmt x y z = some r) : FiniteKernel.fma? (toModel x) (toModel y) (toModel z) = some (toModel r)

An accepted normal fused multiply-add is the compact finite kernel on the operand models.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_fma {fmt : FloatFormat} (h : Eligible fmt) (x y z : Value fmt) : toModel (fma fmt x y z) = Spec.fma (toModel x) (toModel y) (toModel z)

Wide-limb fused multiply-add is the reference fused multiply-add of the operand models.