Shared proofs for native normal operand pairs

Several one-word kernels start the same way: they reject zero, subnormal and exceptional operands, then expose two normalized significands and their biased exponents. Small.Core.Runtime has the executable decoder, and this module proves its common contract once.

View records the generic decoder results together with the bounds the fixed-word rounders need, so the multiplication and division proofs don't repeat the storage-field and exceptional-value arguments. No executable definition depends on this module.

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

Fields and decoder facts 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

A successful withNormalPair? call yields a View whose fields are the ones passed to the kernel.

Since the kernel stays generic, the view serves 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

A normal-pair kernel that rounds like FiniteProductRound.round refines FiniteKernel.mul?.

Because the shared view handles the native decoding, kernel_refines only covers the product and its rounding.