Correctness of native two-word finite multiplication

Every accepted result of the 64 x 64 -> 128 normal-product tier in TwoWordMul.Runtime is the exact format-generic product rounding. The proof separates the two-word product and its leading-bit bounds from the shared one-word carry and packing stage. The dispatcher handles declined inputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.binary64_eligible : Eligible FloatFormat.binary64

Binary64 satisfies the two-word capacity contract.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.roundNormalProduct_refines (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (hexpWidth : fmt.expWidth ≤ 31) (hfracLower : 32 ≤ fmt.fracWidth) (hfracUpper : fmt.fracWidth ≤ 62) (sign : Bool) (xExponent yExponent xMantissa yMantissa : UInt64) (hxExponent : 0 < xExponent.toNat ∧ xExponent.toNat < 2 ^ fmt.expWidth) (hyExponent : 0 < yExponent.toNat ∧ yExponent.toNat < 2 ^ fmt.expWidth) (hxMantissa : 2 ^ fmt.fracWidth ≤ xMantissa.toNat ∧ xMantissa.toNat < 2 ^ (fmt.fracWidth + 1)) (hyMantissa : 2 ^ fmt.fracWidth ≤ yMantissa.toNat ∧ yMantissa.toNat < 2 ^ (fmt.fracWidth + 1)) (result : Model fmt) (hresult : roundNormalProduct? fmt sign xExponent yExponent xMantissa yMantissa = some result) : result = FiniteProductRound.round fmt sign (xMantissa.toNat * yMantissa.toNat) (xExponent.toNat - 1 + (yExponent.toNat - 1))

A successful two-word normal-product round agrees with the exact finite-product rounder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.mulNormal_refines {fmt : FloatFormat} (heligible : Eligible fmt) (x y result : Model fmt) (hresult : mulNormal? x y = some result) : FiniteKernel.mul? x y = some result

A successful two-word normal multiplication agrees with the compact finite kernel.

The native tier handles normal operands of one-storage-word IEEE formats with fraction widths 32 through 62. Zero, subnormal and exceptional operands and boundary results return none and take the generic path.

Storage-word entry points

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeTwoWordMul.mulNormal?_ofWord {fmt : FloatFormat} {xBits yBits : UInt64} (hx : xBits.toNat < 2 ^ fmt.bitWidth) (hy : yBits.toNat < 2 ^ fmt.bitWidth) : mulNormal? (NativeSmallWord.ofWord xBits) (NativeSmallWord.ofWord yBits) = Option.map NativeSmallWord.ofWord (mulNormalWord? fmt xBits yBits)

On storage words below the radix, mulNormal? is the ofWord image of mulNormalWord?.