Executable multiplication backends

The generic path computes exact finite products and owns the complete exceptional-value policy. The dispatcher opportunistically uses native binary32 or binary64, fixed-pair limbs, and parameterized one- or two-word kernels when their structural capabilities apply.

Every specialized routine is partial by design: a declined case is handled by the one exact generic implementation. Mul.Proof establishes that successful fast paths and the baseline all implement the same public specification.

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; exceptional operands retain 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.

Each specialized kernel is selected by a structural capability and returns only a partial fast result. 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. After the binary64 candidate chain is exhausted, and on every other declined route, generic supplies the result. The dispatcher is specialized on the descriptor, as described in Dispatch.Add.Runtime.