Native binary32 product rounding #
The machine-word product rounder serves multiplication, aligned addition, and fused
multiply-add. Its correctness theorem lives in Rounding.Proof, keeping execution-only imports
independent of the proof development.
@[inline]
def
FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundProduct
(sign : Bool)
(product scale : UInt64)
:
Round the signed magnitude product * 2^(scale - 298) to binary32, with sign sign and
subtraction in Int.
Correctness holds for every UInt64 magnitude when scale ≤ 506; callers establish this bound.
In particular, finite multiplication supplies a product below 2^48.