Executable word-specialized fused multiply-add dispatch

Generic and word-specialized dispatchers compute fused multiply-add. Their refinement theorems live in FmaWord.Proof.

def FloatLib.Floats.Formats.BinaryInterchange.Model.FmaBackend.generic {fmt : FloatFormat} (x y z : Model fmt) : Model fmt

Width-generic compiled FMA.

The exceptional-value dispatcher stays explicit, while the all-finite path decodes each operand once and uses the compact finite kernel.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FmaBackend.word {fmt : FloatFormat} (x y z : Model fmt) : Model fmt

Compiled implementation of fma.

Binary32 and binary64 finite operands use native-word decoding and still round only once. Other eligible one-word IEEE formats use the reusable native-storage decoder. Declined and unsupported cases follow the format-generic implementation. The dispatcher is specialized on the descriptor, as described in Dispatch.Add.Runtime.