Correctness of two-word normal multiplication

The runtime kernel multiplies two normal significands exactly in four native words, rounds the product of at most 2 * fracWidth + 2 bits to nearest-even, and packs a normal result. Subnormal operands and results, overflow, NaNs, and infinities are left to the operation dispatcher.

roundNormalProduct_refines is shared with the fused multiply-add kernel: it accepts any four-limb magnitude in [2^(2 * fracWidth), 2^(2 * fracWidth + 3)) together with its leading-bit position, which covers both the product and the aligned product-plus-addend sum.

Threshold words

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.normalThreshold_toNat {fmt : FloatFormat} (h : Eligible fmt) : (UInt64.ofNat (fmt.bias + 2 * fmt.fracWidth - 1)).toNat = fmt.bias + 2 * fmt.fracWidth - 1

The first normal leading-bit position fits a native word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.overflowThreshold_toNat {fmt : FloatFormat} (h : Eligible fmt) : (UInt64.ofNat (3 * fmt.bias + 2 * fmt.fracWidth - 2)).toNat = 3 * fmt.bias + 2 * fmt.fracWidth - 2

The largest finite normal leading-bit position fits a native word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.exponentOffset_toNat {fmt : FloatFormat} (h : Eligible fmt) : (UInt64.ofNat (fmt.bias + 2 * fmt.fracWidth - 2)).toNat = fmt.bias + 2 * fmt.fracWidth - 2

The product exponent offset fits a native word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fracWidth_toNat {fmt : FloatFormat} (h : Eligible fmt) : (UInt64.ofNat fmt.fracWidth).toNat = fmt.fracWidth

The fraction width fits a native word.

Rounding a four-limb magnitude

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundNormalProduct_refines {fmt : FloatFormat} (h : Eligible fmt) (sign : Bool) (xExponent yExponent : UInt64) (product : Numerics.FixedWord.UInt256) (leading : UInt64) (hxExponent : 0 < xExponent.toNat ∧ xExponent.toNat < fmt.expAllOnesNat) (hyExponent : 0 < yExponent.toNat ∧ yExponent.toNat < fmt.expAllOnesNat) (hleading : leading.toNat = product.toNat.log2) (hleadingRange : 2 * fmt.fracWidth ≤ leading.toNat ∧ leading.toNat ≤ 2 * fmt.fracWidth + 2) (hproductLower : 2 ^ (2 * fmt.fracWidth) ≤ product.toNat) (result : Model fmt) (hresult : roundNormalProduct? sign xExponent yExponent product leading = some result) : result = FiniteProductRound.round fmt sign product.toNat (xExponent.toNat - 1 + (yExponent.toNat - 1))

The fixed-limb normal branch agrees with generic unsigned product rounding.

Normal products

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.mulNormalLimb_refines {fmt : FloatFormat} (h : Eligible fmt) (x y result : Model fmt) (hresult : mulNormalLimb? x y = some result) : FiniteKernel.mul? x y = some result

Every result accepted by the pair multiplication kernel equals the exact finite kernel.