Verified wide-limb addition and subtraction

The central theorem is alignOrdered?_refines: an accepted result of the alignment core is the unsigned-scale exact sum FiniteScaleAdd.roundSum of the two signed magnitudes. Its proof follows the two routes of the kernel. On the jammed route the limb value of the combined significand is shiftRightJam of the exact aligned sum or difference (shiftRightJam_add_mul_two_pow, shiftRightJam_mul_two_pow_sub), and the exact value has enough bits above the jam for roundNormal?_jammed. On the exact route the limb value is the exact sum or difference and roundNormal?_exact applies. Equal magnitudes of opposite sign give positive zero, as the specification requires.

addNormal?_refines decodes two normal stored values into the core and identifies the result with FiniteKernel.add?, and toModel_add and toModel_sub finish with the reference operations.

Rounding helpers

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.roundNormal?_exact {fmt : FloatFormat} (hexp : fmt.expWidth ≤ 32) (sign : Bool) (S : Numerics.LimbArray) (T scale : ℕ) (hS : S.toNat = T) (hT : T ≠ 0) (r : Value fmt) (hr : roundNormal? fmt sign S 0 scale = some r) : toModel r = FiniteProductRound.round fmt sign T scale

An accepted rounding of an exact significand is the exact rounder.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.roundNormal?_jammed {fmt : FloatFormat} (hexp : fmt.expWidth ≤ 32) (sign : Bool) (S : Numerics.LimbArray) (T jam scale : ℕ) (hS : S.toNat = Numerics.shiftRightJam T jam) (hbig : 2 ^ (fmt.fracWidth + jam + 2) ≤ T) (r : Value fmt) (hr : roundNormal? fmt sign S jam scale = some r) : toModel r = FiniteProductRound.round fmt sign T scale

An accepted rounding of a jammed significand is the exact rounder on the exact value.

The alignment core

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_pack_zero {fmt : FloatFormat} (hexp : fmt.expWidth ≤ 32) : toModel (pack fmt false 0 (Numerics.LimbArray.zero 0)) = posZero fmt

Packing a zero significand with a clear sign bit gives positive zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.zero_false (fmt : FloatFormat) : zero fmt false = posZero fmt

A zero with a false sign bit is positive zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.alignOrdered?_refines {fmt : FloatFormat} (h : Eligible fmt) (roundOffset : ℕ) (aSign : Bool) (a : Numerics.LimbArray) (sa : ℕ) (bSign : Bool) (b : Numerics.LimbArray) (sb : ℕ) (hsb : sb ≤ sa) (ha : 2 ^ fmt.fracWidth ≤ a.toNat) (hb : 2 ^ fmt.fracWidth ≤ b.toNat) (r : Value fmt) (hr : alignOrdered? fmt roundOffset aSign a sa bSign b sb = some r) : toModel r = FiniteScaleAdd.roundSum fmt roundOffset bSign aSign b.toNat sb a.toNat sa

An accepted result of the ordered alignment core is the unsigned-scale exact sum of its operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.alignAndRound?_refines {fmt : FloatFormat} (h : Eligible fmt) (roundOffset : ℕ) (aSign : Bool) (a : Numerics.LimbArray) (sa : ℕ) (bSign : Bool) (b : Numerics.LimbArray) (sb : ℕ) (ha : 2 ^ fmt.fracWidth ≤ a.toNat) (hb : 2 ^ fmt.fracWidth ≤ b.toNat) (r : Value fmt) (hr : alignAndRound? fmt roundOffset aSign a sa bSign b sb = some r) : toModel r = FiniteScaleAdd.roundSum fmt roundOffset aSign bSign a.toNat sa b.toNat sb

An accepted result of the alignment core is the unsigned-scale exact sum of its operands.

Addition and subtraction of stored values

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.decode?_normal {fmt : FloatFormat} (h : Eligible fmt) (v : Value fmt) (hfinite : expField v ≠ fmt.expAllOnesNat) (hnormal : expField v ≠ 0) : FiniteKernel.decode? (toModel v) = some { sign := signBit v, exponent := expField v, mantissa := (normalMantissa v).toNat }

A normal stored value decodes to its sign, exponent field, and normal significand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.decode?_signed {fmt : FloatFormat} (h : Eligible fmt) (negate : Bool) (v : Value fmt) (hfinite : expField v ≠ fmt.expAllOnesNat) (hnormal : expField v ≠ 0) : FiniteKernel.decode? (if negate = true then (toModel v).neg else toModel v) = some { sign := signBit v ^^ negate, exponent := expField v, mantissa := (normalMantissa v).toNat }

Decoding a normal stored value, possibly negated, flips its sign when negate is set.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.addNormal?_refines {fmt : FloatFormat} (h : Eligible fmt) (negateY : Bool) (x y r : Value fmt) (hr : addNormal? fmt negateY x y = some r) : FiniteKernel.add? (toModel x) (if negateY = true then (toModel y).neg else toModel y) = some (toModel r)

An accepted normal sum is the compact finite addition of the operand models.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_add {fmt : FloatFormat} (h : Eligible fmt) (x y : Value fmt) : toModel (add fmt x y) = Spec.add (toModel x) (toModel y)

Wide-limb addition is the reference addition of the operand models.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_sub {fmt : FloatFormat} (h : Eligible fmt) (x y : Value fmt) : toModel (sub fmt x y) = Spec.sub (toModel x) (toModel y)

Wide-limb subtraction is the reference subtraction of the operand models.