Shared native-word product finishing

The one-word and two-word multiplication kernels use different representations for the exact product. After rounding that product to a UInt64 significand, both kernels perform the same carry adjustment, overflow test, and field packing. Keeping that final stage here gives the two backends one executable definition as well as one proof.

finishWord returns a word rather than an Option; its caller chooses a decline marker outside the valid packed range. Both definitions request inlining. The overflow threshold and exponent offset are formed from NativeSmallWord.biasWord using machine-word arithmetic.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeWordProduct.finish? (fmt : FloatFormat) (sign : Bool) (position rounded : UInt64) : Option (Model fmt)

Finish a rounded native-word product already in the normal range, declining on overflow.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeWordProduct.finishWord (fmt : FloatFormat) (decline : UInt64) (sign : Bool) (position rounded : UInt64) : UInt64

Finish a rounded native-word product without constructing an Option.

On overflow the function returns decline; otherwise it returns the packed storage word.