Shared proof for finishing a native-word product

The one-word and two-word multiplication kernels differ in how they form and round an exact product. Once they have a rounded UInt64 significand, however, carry handling, overflow testing, and field packing are identical. This module proves that common final stage once.

The theorem is deliberately about the finishing stage only. Product construction remains in each backend, where the machine representation and its capacity bounds are materially different.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeWordProduct.finishWord_decode (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (decline : UInt64) (hdecline : 2 ^ fmt.bitWidth ≤ decline.toNat) (sign : Bool) (position rounded : UInt64) : (if (finishWord fmt decline sign position rounded == decline) = true then none else some (NativeSmallWord.ofWord (finishWord fmt decline sign position rounded))) = finish? fmt sign position rounded

The word-valued finishing function decodes to the optional finishing function.

The only condition on the caller's decline marker is that it lies above every valid packed word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeWordProduct.finish_eq (fmt : FloatFormat) (hwidth : fmt.bitWidth ≤ 64) (sign : Bool) (position rounded : UInt64) (positionNat roundedNat : ℕ) (hposition : position.toNat = positionNat) (hpositionAdd : (position + 1).toNat = positionNat + 1) (hrounded : rounded.toNat = roundedNat) (hnormal : fmt.bias + 2 * fmt.fracWidth - 1 ≤ positionNat) (hhidden : (NativeSmallWord.hiddenBit fmt).toNat = 2 ^ fmt.fracWidth) (hcarryBit : (NativeSmallWord.carryBit fmt).toNat = 2 ^ (fmt.fracWidth + 1)) (hroundedLower : 2 ^ fmt.fracWidth ≤ roundedNat) : finish? fmt sign position rounded = let carry := roundedNat = pow2 (fmt.fracWidth + 1); have normalizedPosition := if carry then positionNat + 1 else positionNat; have overflowThreshold := 3 * fmt.bias + 2 * fmt.fracWidth - 2; if overflowThreshold < normalizedPosition then none else have normalizedMantissa := if carry then pow2 fmt.fracWidth else roundedNat; have exponentOffset := fmt.bias + 2 * fmt.fracWidth - 2; some (ofFields fmt sign (normalizedPosition - exponentOffset) (normalizedMantissa - pow2 fmt.fracWidth))

Native carry, overflow, and packing agree with the natural-number normal-result specification.

Callers supply the representation facts for their product implementation: the natural values of the position and rounded significand, the no-wrap fact for incrementing the position, and the implicit and carry bits as machine words. The overflow threshold and exponent offset are computed from biasWord, whose value follows from the width bound alone.