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

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

Sticky alignment outside the exact windows

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

Word-level fused multiply-add equals the exact-dyadic fmaFinite?.