Shared native-word product finishing

The one-word and two-word multiplication kernels represent the exact product differently. After rounding it to a UInt64 significand, both do the same carry adjustment, overflow test and field packing, so that final stage lives here with one executable definition and one proof.

finish? is finishWord? mapped to model values. finishWord returns a word in place of an Option, and its caller picks a decline marker outside the valid packed range. The overflow threshold and exponent offset are computed from NativeSmallWord.biasWord in machine-word arithmetic.

@[inline]

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

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

Carriers that store the encoding as a UInt64 use this form so an accepted result never becomes an exact-width model value.

@[inline]

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

finishWord? as a model value.

@[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 building an Option.

It returns decline on overflow and the packed storage word otherwise.