Executable unsigned-scale exact addition

These kernels align and combine signed magnitudes in an unsigned scale coordinate before entering the product rounder. ScaleAdd.Proof proves agreement with exact dyadic addition and rounding for conventional IEEE descriptors.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.exponent (fmt : FloatFormat) (scale roundOffset : ℕ) : ℤ

Numerics.Dyadic exponent represented by an unsigned scale accepted by FiniteProductRound.round.

The rounder interprets its scale relative to twice the IEEE subnormal alignment offset. The additional roundOffset lets ordinary addition use one-offset coordinates while FMA uses two-offset product coordinates.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundMagnitude (fmt : FloatFormat) (roundOffset : ℕ) (sign : Bool) (mantissa scale : ℕ) : Model fmt

Round one signed magnitude from an unsigned scale.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundMagnitudes (fmt : FloatFormat) (roundOffset : ℕ) (leftSign rightSign : Bool) (left right scale : ℕ) : Model fmt

Combine nonzero signed magnitudes at one shared unsigned scale and round once.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.FiniteScaleAdd.roundSum (fmt : FloatFormat) (roundOffset : ℕ) (leftSign rightSign : Bool) (leftMantissa leftScale rightMantissa rightScale : ℕ) : Model fmt

Align two signed magnitudes in an unsigned scale coordinate and round their exact sum once.