Wide-limb addition and subtraction runtime

alignAndRound? combines two signed magnitudes given at unsigned scales, the shared core of addition, subtraction, and fused multiply-add. After ordering the operands by scale it takes one of two routes.

• When the scale difference d is at least three and the higher-scale operand dominates, the lower operand is shifted right by d - 3 bits and the higher operand is shifted left by three. The discarded tail supplies a sticky bit after addition, or a borrow and sticky bit after subtraction. The dominance bound leaves enough bits above the jammed position for roundShiftRightEven_shiftRightJam to preserve the final nearest-even result.
• Otherwise the exact sum or difference is formed in limbs; cancellation is exact.

Both routes end in roundNormal?. addNormal? decodes two normal stored values into this core; add and sub use Model.Spec.add and Model.Spec.sub, respectively, for declined cases. Addition.Proof proves that they equal Model.Spec.add and Model.Spec.sub.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.alignOrdered? (fmt : FloatFormat) (roundOffset : ℕ) (aSign : Bool) (a : Numerics.LimbArray) (sa : ℕ) (bSign : Bool) (b : Numerics.LimbArray) (sb : ℕ) : Option (Value fmt)

Combine two nonzero signed magnitudes whose scales satisfy sb ≤ sa.

The value computed is (aSign, a * 2^sa) + (bSign, b * 2^sb) at unsigned scale sb, rounded by roundNormal? with the given rounding offset. Both magnitudes are expected to be at least 2^fracWidth; Addition.Proof.alignOrdered?_refines states the contract.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.alignAndRound? (fmt : FloatFormat) (roundOffset : ℕ) (aSign : Bool) (a : Numerics.LimbArray) (sa : ℕ) (bSign : Bool) (b : Numerics.LimbArray) (sb : ℕ) : Option (Value fmt)

Combine two nonzero signed magnitudes at arbitrary unsigned scales.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.addNormal? (fmt : FloatFormat) (negateY : Bool) (x y : Value fmt) : Option (Value fmt)

Add two normal stored values, negating the second when negateY holds; other cases are declined.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.add (fmt : FloatFormat) (x y : Value fmt) : Value fmt

Wide-limb addition with the reference operation for declined cases.

def FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.sub (fmt : FloatFormat) (x y : Value fmt) : Value fmt

Wide-limb subtraction with the reference operation for declined cases.