Correctness of native one-word finite multiplication

The one-word kernel uses a high-bit sentinel to decline cases outside its guarded normal-result region. The sentinel proof rules out collisions with valid packed results, and the main refinement identifies every successful proposal with the format-generic finite multiplication kernel.

Mul.Runtime contains the word-valued and optional entry points. Their agreement theorem allows the dispatcher to use the sentinel interface and continue 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

Decode the word-valued normal-product result to the optional result.

The high decline bit is outside every eligible storage word, so 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.

The hypotheses state only the machine-capacity and normalized-input bounds needed by the UInt64 implementation.

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

Decode the flat tagged execution result back to the proof-facing optional result.

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 deliberately handles only normal IEEE operands whose intermediate fields fit in one word. Every other input returns none, so callers can retain the exact baseline.