Correctness of multiplication backends

Every route through the multiplication dispatcher meets Spec.mul: binary32, binary64, fixed-pair, parameterized one-word, two-word, and generic implementations differ only in storage and execution strategy.

Each fast kernel may decline when its structural or finite-input preconditions fail. The proof shows that accepted results refine Spec.mul and that every decline reaches generic. Runtime clients can import Mul.Runtime without loading these theorems.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.MulBackend.generic_eq_spec {fmt : FloatFormat} (x y : Model fmt) : generic x y = Spec.mul x y

Compact generic multiplication preserves the public exact-dyadic operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.MulBackend.word_eq_spec {fmt : FloatFormat} (x y : Model fmt) : word x y = Spec.mul x y

Multiplication through the native fixed-format and parameterized one- and two-word kernels agrees with Spec.mul.