Nearest-even rounding through guard and sticky bits

The width-generic rounder Numerics.roundShiftRightEven inspects the guard bit, retained parity, and sticky bits. Kernels can therefore compress discarded bits before rounding a sum or fused multiply-add. The proofs below establish how far that compression may go and how it interacts with alignment and subtraction.

• roundShiftRightEven_eq_guard_sticky, from Quantization.Deterministic.ShiftRight, is the three-bit form of nearest-even rounding that these proofs build on.
• roundShiftRight_shiftRightJam shows that jamming every bit below position j into one sticky bit does not change a later rounding by at least j + 2 bits, under every MagnitudeRounding rule. roundShiftRightEven_shiftRightJam is its nearest-even case. Applying this to an addition result needs a further argument relating that result to its jammed value.
• roundShiftRightEven_mul_two_pow and roundShiftRightEven_mul_two_pow_of_le relate rounding of a scaled value to rounding of the original.
• shiftRightJam_add_mul_two_pow and shiftRightJam_mul_two_pow_sub describe the jammed quotient of an aligned sum or difference in terms of the two operands, and log2_shiftRightJam locates its leading bit.

These statements apply to natural numbers independently of their storage. The fixed-word and limb-array kernels use them to justify their rounding steps.

The guard-and-sticky form

theorem FloatLib.Numerics.testBit_one_succ (i : ℕ) : Nat.testBit 1 (i + 1) = false

The number one has no bits above position zero.

theorem FloatLib.Numerics.roundShiftRightEven_le_succ (x s : ℕ) : roundShiftRightEven x s ≤ x / 2 ^ s + 1

The nearest-even quotient is at most the successor of the truncated quotient.

theorem FloatLib.Numerics.div_two_pow_le_roundShiftRightEven (x s : ℕ) : x / 2 ^ s ≤ roundShiftRightEven x s

The nearest-even quotient is at least the truncated quotient.

Jamming

theorem FloatLib.Numerics.or_one_eq (q : ℕ) : q ||| 1 = if q % 2 = 0 then q + 1 else q

Setting the low bit adds one to an even number and leaves an odd number unchanged.

theorem FloatLib.Numerics.div_two_pow_le_shiftRightJam (x j : ℕ) : x / 2 ^ j ≤ shiftRightJam x j

Jamming never decreases the truncated quotient.

theorem FloatLib.Numerics.shiftRightJam_ne_zero (x j : ℕ) (hx : 2 ^ j ≤ x) : shiftRightJam x j ≠ 0

Jamming a value with a set bit at or above the jam position gives a nonzero result.

theorem FloatLib.Numerics.roundShiftRight_shiftRightJam (rule : MagnitudeRounding) (x j s : ℕ) (hj : j + 2 ≤ s) : roundShiftRight rule (shiftRightJam x j) (s - j) = roundShiftRight rule x s

Rounding after a sticky-bit jam agrees with rounding the original value under every rule, provided the rounding keeps at least the guard bit above the jammed position.

The jam preserves the retained bits, the guard bit, and whether any lower bit is set, which are the only inputs of MagnitudeRounding.increment.

theorem FloatLib.Numerics.roundShiftRightEven_shiftRightJam (x j s : ℕ) (hj : j + 2 ≤ s) : roundShiftRightEven (shiftRightJam x j) (s - j) = roundShiftRightEven x s

The nearest-even case of roundShiftRight_shiftRightJam: if j + 2 ≤ s, jamming by j and then rounding by s - j agrees with rounding the original value by s.

theorem FloatLib.Numerics.shiftRightJam_add_mul_two_pow (A B j : ℕ) : shiftRightJam (A * 2 ^ j + B) j = if B % 2 ^ j = 0 then A + B / 2 ^ j else A + B / 2 ^ j ||| 1

The jammed quotient of an aligned sum A * 2^j + B, in terms of A and B.

theorem FloatLib.Numerics.shiftRightJam_mul_two_pow_sub (A B j : ℕ) (hB : B ≤ A * 2 ^ j) : shiftRightJam (A * 2 ^ j - B) j = if B % 2 ^ j = 0 then A - B / 2 ^ j else A - B / 2 ^ j - 1 ||| 1

The jammed quotient of an aligned difference A * 2^j - B with B ≤ A * 2^j.

theorem FloatLib.Numerics.log2_shiftRightJam (x j : ℕ) (hx : 2 ^ (j + 1) ≤ x) : (shiftRightJam x j).log2 = x.log2 - j

Jamming preserves the shifted leading-bit position when the truncated quotient is at least two.

Scaling

theorem FloatLib.Numerics.roundShiftRightEven_mul_two_pow (x k s : ℕ) : roundShiftRightEven (x * 2 ^ k) (s + k) = roundShiftRightEven x s

Rounding a value scaled by 2^k by k more bits is rounding the value.

theorem FloatLib.Numerics.roundShiftRightEven_mul_two_pow_of_le (x k s : ℕ) (hs : s ≤ k) : roundShiftRightEven (x * 2 ^ k) s = x * 2 ^ (k - s)

Rounding a value scaled by 2^k by at most k bits is exact.