Verified wide-limb multiplication

An accepted normal product is the compact finite kernel FiniteKernel.mul? on the models of the operands (mulNormal?_refines): the operands decode to their limb significands (Core.Proof.decode?_toModel), the schoolbook product is exact (LimbArray.toNat_mul), and the limb rounder is the exact rounder (Round.Proof). The total operation then equals Model.Spec.mul because both its branches do: the accepted branch through Finite.Proof.spec_mul_of_mul?_eq_some, the declined branch through the codec laws.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.mulNormal?_refines {fmt : FloatFormat} (h : Eligible fmt) (x y r : Value fmt) (hr : mulNormal? fmt x y = some r) : FiniteKernel.mul? (toModel x) (toModel y) = some (toModel r)

An accepted normal product is the compact finite multiplication of the operand models.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_mul {fmt : FloatFormat} (h : Eligible fmt) (x y : Value fmt) : toModel (mul fmt x y) = Spec.mul (toModel x) (toModel y)

Wide-limb multiplication is the reference multiplication of the operand models.