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 Round.Proof.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 demands.

addNormal?_refines decodes two normal stored values into the core and identifies the result with FiniteKernel.add?; 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

Positive zero from the packing kernel.

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 }

The decoded components of a normal stored value.

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 }

The decoded components of a normal stored value, possibly negated.

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.