Nearest-even rounding through guard and sticky bits

The width-generic rounder Numerics.roundShiftRightEven compares the discarded remainder with the halfway value 2^(shift - 1). Limb kernels can avoid constructing that value by using three Boolean tests: the guard bit just below the kept quotient, whether any lower bit is set, and the parity of the quotient. This module proves that restatement and its consequences for the sticky-bit normalisation used by addition and fused multiply-add.

• roundShiftRightEven_eq_guard_sticky is the three-bit form of nearest-even rounding.
• roundShiftRightEven_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. Applying this to an addition result requires a separate 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.mod_two_pow_succ_eq (x t : ℕ) : x % 2 ^ (t + 1) = x % 2 ^ t + 2 ^ t * if x.testBit t = true then 1 else 0

The remainder of a shift splits into the sticky bits and the guard bit.

theorem FloatLib.Numerics.roundShiftRightEven_eq_guard_sticky (x s : ℕ) (hs : 0 < s) : roundShiftRightEven x s = x / 2 ^ s + if (x.testBit (s - 1) && (decide (x % 2 ^ (s - 1) ≠ 0) || x.testBit s)) = true then 1 else 0

Nearest-even rounding in guard-and-sticky form.

The quotient is incremented exactly when the guard bit is set and either a sticky bit is set or the quotient is odd.

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 of a natural number.

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.roundShiftRightEven_shiftRightJam (x j s : ℕ) (hj : j + 2 ≤ s) : roundShiftRightEven (shiftRightJam x j) (s - j) = roundShiftRightEven x s

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

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.

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.

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.