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, and reusable small-word kernels.

Accepted kernel results and the generic fallback all agree with Spec.fma, including its exceptional-value policy. Runtime clients can import FmaWord.Runtime separately.

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

Native-word or generic fused multiply-add preserves the logical operation.