Correctness of native one-word finite multiplication

The one-word kernel declines with a high-bit sentinel outside its guarded normal-result region. The sentinel never collides with a valid packed result, and the main refinement identifies every accepted result with the format-generic finite multiplication kernel.

Mul.Runtime has a word-valued and an optional entry point. Because they agree, the dispatcher can use the sentinel form and fall back to the generic implementation on a decline.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.declineWord_toNat : declineWord.toNat = 2 ^ 63

Natural-number value of the one-word decline sentinel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.roundNormalProductWord_decode (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (hstorage : fmt.bitWidth ≤ 63) (sign : Bool) (xExponent yExponent xMantissa yMantissa : UInt64) : (if (roundNormalProductWord fmt sign xExponent yExponent xMantissa yMantissa == declineWord) = true then none else some (NativeSmallWord.ofWord (roundNormalProductWord fmt sign xExponent yExponent xMantissa yMantissa))) = roundNormalProduct? fmt sign xExponent yExponent xMantissa yMantissa

The word-valued normal-product result decodes to the optional result.

Since the high decline bit is outside every eligible storage word, successful packed results cannot collide with the sentinel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.roundNormalProduct_refines (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (hexpWidth : fmt.expWidth ≤ 30) (hfracWidth : fmt.fracWidth ≤ 31) (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 native normal-product round agrees with the exact finite-product rounder.

Its hypotheses are the machine-capacity and normalized-input bounds that the UInt64 implementation needs, and nothing more.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.mulNormalWord_decode {fmt : FloatFormat} (heligible : Eligible fmt) (x y : Model fmt) : (if (mulNormalWord x y == declineWord) = true then none else some (NativeSmallWord.ofWord (mulNormalWord x y))) = mulNormal? x y

The flat sentinel-tagged word result decodes to the optional result mulNormal?.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.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 one-word normal multiplication agrees with the compact finite kernel.

The native path handles only normal IEEE operands whose intermediate fields fit in one word. Every other input returns none, and callers fall back to the exact kernel.