TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.TwoWordMul.Proof

Correctness of native two-word finite multiplication #

The executable 64 x 64 -> 128 normal-product tier lives in TwoWordMul.Runtime. Its refinement theorem identifies every successful native result with the exact format-generic product rounder. The proof separates the two-word product and its leading-bit bounds from the shared one-word carry and packing stage. Declined inputs remain the dispatcher's responsibility.

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

Binary64 is the standard specialization of the reusable two-word capacity tier.

source
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.

source
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 for one-storage-word IEEE formats with precisions 33 through 62. Exceptional operands and boundary results return none and retain the generic path.