Shared proofs for native normal operand pairs

Several one-word kernels begin with the same operation: reject zero, subnormal, and exceptional operands, then expose two normalized significands and their biased exponents. The executable decoder remains in Small.Core.Runtime; this module proves its common contract once.

View records the exact generic decoder results together with the bounds needed by fixed-word rounders. Multiplication and division can therefore focus on their different arithmetic without repeating storage-field and exceptional-value arguments. No executable definition depends on this proof layer.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.NativeNormalPair.View {fmt : FloatFormat} (x y : Model fmt) : Type

Proof-facing view of two successfully decoded normal operands.

• sign : Bool

  XOR of the operand signs, as supplied to multiplicative kernels.

• xExponent : UInt64

  Biased exponent of the left operand.

• yExponent : UInt64

  Biased exponent of the right operand.

• xMantissa : UInt64

  Normalized significand of the left operand.

• yMantissa : UInt64

  Normalized significand of the right operand.

• sign_eq : self.sign = (x.signBit ^^ y.signBit)

  The native sign calculation agrees with the model fields.

• xDecode : FiniteKernel.decode? x = some { sign := x.signBit, exponent := self.xExponent.toNat, mantissa := self.xMantissa.toNat }

  The generic finite decoder sees the same left operand fields.

• yDecode : FiniteKernel.decode? y = some { sign := y.signBit, exponent := self.yExponent.toNat, mantissa := self.yMantissa.toNat }

  The generic finite decoder sees the same right operand fields.

• xExponentBounds : 0 < self.xExponent.toNat ∧ self.xExponent.toNat < 2 ^ fmt.expWidth

  The left biased exponent is a nonzero stored exponent.

• yExponentBounds : 0 < self.yExponent.toNat ∧ self.yExponent.toNat < 2 ^ fmt.expWidth

  The right biased exponent is a nonzero stored exponent.

• xMantissaBounds : 2 ^ fmt.fracWidth ≤ self.xMantissa.toNat ∧ self.xMantissa.toNat < 2 ^ (fmt.fracWidth + 1)

  The left significand has its implicit leading bit.

• yMantissaBounds : 2 ^ fmt.fracWidth ≤ self.yMantissa.toNat ∧ self.yMantissa.toNat < 2 ^ (fmt.fracWidth + 1)

  The right significand has its implicit leading bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeNormalPair.decode_normal {fmt : FloatFormat} (hieee : fmt.isIEEE = true) (hwidth : fmt.bitWidth ≤ 64) (x : Model fmt) (hnonzero : NativeSmallWord.exponentField fmt (NativeSmallWord.toWord x) ≠ 0) (hnonexceptional : NativeSmallWord.exponentField fmt (NativeSmallWord.toWord x) ≠ NativeSmallWord.exponentMask fmt) : FiniteKernel.decode? x = some { sign := x.signBit, exponent := (NativeSmallWord.exponentField fmt (NativeSmallWord.toWord x)).toNat, mantissa := (NativeSmallWord.fractionField fmt (NativeSmallWord.toWord x) ||| NativeSmallWord.hiddenBit fmt).toNat }

A native normal field decode agrees with the generic finite decoder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeNormalPair.view_of_success {fmt : FloatFormat} {α : Type} (hieee : fmt.isIEEE = true) (hwidth : fmt.bitWidth ≤ 64) (x y : Model fmt) (kernel : Bool → UInt64 → UInt64 → UInt64 → UInt64 → Option α) (result : α) (hresult : NativeSmallWord.withNormalPair? x y kernel = some result) : ∃ (view : View x y), kernel view.sign view.xExponent view.yExponent view.xMantissa view.yMantissa = some result

Extract the shared proof view from a successful native normal-pair callback.

The callback itself remains fully generic. Its caller receives the exact fields passed at runtime, their normalized bounds, and decoder equalities suitable for any binary operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeNormalPair.mul_refines {fmt : FloatFormat} (hieee : fmt.isIEEE = true) (hwidth : fmt.bitWidth ≤ 64) (kernel : Bool → UInt64 → UInt64 → UInt64 → UInt64 → Option (Model fmt)) (kernel_refines : ∀ (sign : Bool) (xExponent yExponent xMantissa yMantissa : UInt64) (result : Model fmt), 0 < xExponent.toNat ∧ xExponent.toNat < 2 ^ fmt.expWidth → 0 < yExponent.toNat ∧ yExponent.toNat < 2 ^ fmt.expWidth → 2 ^ fmt.fracWidth ≤ xMantissa.toNat ∧ xMantissa.toNat < 2 ^ (fmt.fracWidth + 1) → 2 ^ fmt.fracWidth ≤ yMantissa.toNat ∧ yMantissa.toNat < 2 ^ (fmt.fracWidth + 1) → kernel sign xExponent yExponent xMantissa yMantissa = some result → result = FiniteProductRound.round fmt sign (xMantissa.toNat * yMantissa.toNat) (xExponent.toNat - 1 + (yExponent.toNat - 1))) (x y result : Model fmt) (hresult : NativeSmallWord.withNormalPair? x y kernel = some result) : FiniteKernel.mul? x y = some result

Lift a certified normal-product callback to the generic finite multiplication kernel.

The shared view handles native decoding. The callback hypothesis is responsible only for the product representation and its final rounding.