Correctness of word-specialized fused multiply-add dispatch

Fused multiply-add forms the exact product-plus-addend before one rounding step. The refinements here establish that contract for the binary32, binary64, one-word UInt64, and native-storage kernels.

Accepted kernel results and the generic fallback all agree with Spec.fma, including its exceptional-value policy.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FmaBackend.generic_eq_spec {fmt : FloatFormat} (x y z : Model fmt) : generic x y z = Spec.fma x y z

Compact generic FMA preserves the public exact-dyadic operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FmaBackend.word_eq_spec {fmt : FloatFormat} (x y z : Model fmt) : word x y z = Spec.fma x y z

Word-specialized fused multiply-add agrees with Spec.fma.