Correctness of native-word fused multiply-add for generic binary32

The direct UInt64 fused multiply-add kernel agrees with its exact-dyadic finite specification. Runtime clients can import Fma.Runtime without the alignment, packing, and rounding proof developments.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fmaFiniteImpl_eq (x y z : Value) : fmaFiniteImpl? x y z = fmaFinite? x y z

The guarded UInt64 fused multiply-add kernel equals the generic exact-dyadic finite implementation.