Executable multiplication backends

The generic path rounds exact finite products and handles every exceptional value. The dispatcher uses native binary32 or binary64, fixed-pair limbs, and parameterized one- or two-word kernels when their structural capabilities apply.

Every specialized routine may decline, and a declined case goes to generic. Mul.Proof shows that the accepted fast-path results and generic all implement the same public specification.

@[specialize #[0]]

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

Width-generic compiled multiplication.

Finite operands use the compact scale kernel, and exceptional operands keep the public NaN and infinity policy.

@[specialize #[0]]

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

Word-specialized compiled implementation of mul.

A structural capability selects each kernel, and every kernel may decline. Binary32 uses the checked narrow backend. Binary64 first tries the parameterized two-word normal-product kernel, whose 64 x 64 -> 128 product and machine-word finishing stage suit its 53-bit significands, and falls back to its fixed multiword kernel. Eligible pair layouts use the four-limb product kernel. Other conventional IEEE formats use parameterized one- and two-word normal-product kernels. Every declined route, including the end of the binary64 chain, falls back to generic. The dispatcher is specialized on the descriptor, as described in Dispatch.Add.Runtime.