Shared proof for finishing a native-word product

This module proves the final stage shared by the one-word and two-word multiplication kernels: carry handling, overflow testing and field packing of a rounded UInt64 significand. Product construction stays in each backend, where the machine representation and its capacity bounds differ.

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

Decoding finishWord with its decline marker gives finish?.

The caller's decline marker only has to lie 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.