Wide-limb multiplication runtime

Normal operands are multiplied exactly by the schoolbook limb product and passed to roundNormal? for one rounding. Normal inputs can still be declined: the product's leading position must reach the normal range before rounding, and its position after rounding carry must stay in the finite range. In particular, the lower check can decline a product that would round up to the smallest normal value. Zero, subnormal, and exceptional operands are also declined. The total operation computes every declined case with Model.Spec.mul through the model codec; Multiplication.Proof proves agreement on all operands.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.mulNormal? (fmt : FloatFormat) (x y : Value fmt) : Option (Value fmt)

Try multiplication of two normal stored values.

With position = product.log2 + (xExponent.toNat - 1) + (yExponent.toNat - 1), acceptance also requires fmt.bias + 2 * fmt.fracWidth - 1 ≤ position and normalizedPosition ≤ 3 * fmt.bias + 2 * fmt.fracWidth - 2, where rounding carry increments position to obtain normalizedPosition. See roundNormal?.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.mul (fmt : FloatFormat) (x y : Value fmt) : Value fmt

Wide-limb multiplication with the reference operation for declined cases.