Correctness of unsigned-scale product rounding

round_eq_roundDyadic identifies unsigned-scale rounding with roundDyadic for descriptors satisfying fmt.isIEEE = true. The equality covers signed zero, subnormal results, carry normalization, and overflow.

normalSpec_refines supplies the common natural-number normal-product contract used by word backends. round_normalized_sum gives the one-bit nearest-even reduction used by equal-exponent addition.

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteProductRound.normalSpec? (fmt : FloatFormat) (sign : Bool) (xExponent yExponent xMantissa yMantissa : ℕ) : Option (Model fmt)

Proof-facing specification of the successful normal-product path.

The optimized word backends use different integer representations, but successful normal results all have this format-independent meaning. Keeping the specification here prevents one specialized backend from becoming a proof dependency of another.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteProductRound.normalSpec_refines (fmt : FloatFormat) (sign : Bool) (xExponent yExponent xMantissa yMantissa : ℕ) (hproduct : xMantissa * yMantissa ≠ 0) (hleading : fmt.fracWidth ≤ (xMantissa * yMantissa).log2) (result : Model fmt) (hresult : normalSpec? fmt sign xExponent yExponent xMantissa yMantissa = some result) : result = round fmt sign (xMantissa * yMantissa) (xExponent - 1 + (yExponent - 1))

A successful normal-product specification result is exactly the arbitrary-precision product rounder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteProductRound.normalSpec_refines_of_normalized (fmt : FloatFormat) (sign : Bool) (xExponent yExponent xMantissa yMantissa : ℕ) (hxMantissa : 2 ^ fmt.fracWidth ≤ xMantissa) (hyMantissa : 2 ^ fmt.fracWidth ≤ yMantissa) (result : Model fmt) (hresult : normalSpec? fmt sign xExponent yExponent xMantissa yMantissa = some result) : result = round fmt sign (xMantissa * yMantissa) (xExponent - 1 + (yExponent - 1))

Significands at least 2 ^ fmt.fracWidth satisfy the side conditions of normalSpec_refines.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteProductRound.round_normalized_sum (fmt : FloatFormat) (sign : Bool) (exponent left right : ℕ) (hexponent : exponent < 2 * fmt.bias) (hleft : 2 ^ fmt.fracWidth ≤ left ∧ left < 2 ^ (fmt.fracWidth + 1)) (hright : 2 ^ fmt.fracWidth ≤ right ∧ right < 2 ^ (fmt.fracWidth + 1)) : round fmt sign (left + right) (exponent + (fmt.bias + fmt.fracWidth - 2)) = ofFields fmt sign (exponent + 1) (Numerics.roundShiftRightEven (left + right) 1 - pow2 fmt.fracWidth)

Adding two normalized significands at one encoded exponent discards exactly one low bit.

This is the format-independent part of equal-exponent native addition. Word backends still prove that their machine addition and packing operations represent the Nat expression below, but the rounding argument is shared by every binary descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteProductRound.round_eq_roundDyadic (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (product scale : ℕ) : round fmt sign product scale = roundDyadic fmt { negative := sign, significand := product, exponent := Int.ofNat scale - Int.ofNat (2 * fmt.ieeeSubnormalAlignExp) }

Unsigned-scale product rounding agrees with the public exact-dyadic rounder for a conventional IEEE descriptor.