Executable unsigned-scale rounding for finite products

This arbitrary-precision kernel rounds a finite product directly from its unsigned field scale. For conventional IEEE descriptors, ProductRound.Proof proves agreement with the public dyadic rounder.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteProductRound.round (fmt : FloatFormat) (sign : Bool) (product scale : ℕ) : Model fmt

Round the magnitude product * 2^(scale - 2 * ieeeSubnormalAlignExp fmt) with sign sign.

The exponent subtraction is interpreted in Int. The numerical refinement assumes a conventional IEEE descriptor.

The thresholds are written in the same unsigned coordinate:

• bias + 2 * fracWidth - 1 is the first normal leading-bit position;
• 3 * bias + 2 * fracWidth - 2 is the largest finite normal leading-bit position.