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)

Specification of the successful normal-product path.

The word backends use different integer representations, but their successful normal results all have this format-independent meaning. Keeping it here stops 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 normalSpec? result is the result of the arbitrary-precision product rounder round.

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_shiftRightJam (fmt : FloatFormat) (sign : Bool) (product scale jam : ℕ) (hleading : jam + fmt.fracWidth + 2 ≤ product.log2) : round fmt sign (Numerics.shiftRightJam product jam) (scale + jam) = round fmt sign product scale

Compressing low bits into a sticky bit preserves the rounded encoding when two bits remain below the destination significand. The same bound covers normal and subnormal rounding.

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.