Executable word-specialized fused multiply-add dispatch

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

@[specialize #[0]]

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

Width-generic compiled FMA.

The all-finite path decodes each operand once and uses the compact finite kernel. NaN, infinite and invalid cases are resolved in this body.

@[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 one-word IEEE formats with at most 30 exponent and 29 fraction bits first try the UInt64 kernel NativeSmallWordFma. If it declines, they and the remaining one-word formats use the reusable native-storage decoder. Declined and unsupported cases fall back to generic. The dispatcher is specialized on the descriptor, as described in Dispatch.Add.Runtime.