Deterministic nearest-even shift rounding #

Power-of-two nearest-even rounding shared by binary floating-point, fixed-point, and other quantized representations. Guard, parity, and sticky bits decide rounding without constructing a halfway marker.

source

@[inline]

def FloatLib.Numerics.shiftRightRemainder (value shift : ℕ) :

ℕ

Remainder discarded by shifting a natural number right.

Writing the operation this way avoids constructing 2^shift. When shift exceeds the input's bit length, the quotient is zero and the remainder is the original value.

Instances For

source

theorem FloatLib.Numerics.shiftRightRemainder_eq_mod (value shift : ℕ) :

shiftRightRemainder value shift = value % 2 ^ shift

The bits discarded by a right shift are exactly the remainder modulo 2^shift.

source

@[inline]

def FloatLib.Numerics.roundShiftRightEven (value shift : ℕ) :

ℕ

Round value / 2^shift to the nearest natural number, breaking exact halfway cases toward even.

This is the power-of-two specialization of roundQuotientEven. It belongs in the common quantization layer because binary floats, P3109 formats, and fixed-point kernels all discard low binary digits in the same way. The guard bit decides whether rounding can increase the quotient. The first shift retains the guard bit alongside the quotient. Only a set guard bit with an even quotient requires checking whether shifting those retained bits back recovers the original value. One low-byte extraction supplies both the guard bit and the quotient's parity.

Instances For

source

@[simp]

theorem FloatLib.Numerics.roundShiftRightEven_zero (value : ℕ) :

roundShiftRightEven value 0 = value

Shifting by no bits leaves the value unchanged.

source

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.

source

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.

source

theorem FloatLib.Numerics.roundShiftRightEven_def (value shift : ℕ) :

roundShiftRightEven value shift = if (shift == 0) = true then value else have quotient := value.shiftRight shift; have remainder := value - quotient.shiftLeft shift; have half := 2 ^ (shift - 1); if remainder < half then quotient else if half < remainder then quotient + 1 else if (quotient % 2 == 0) = true then quotient else quotient + 1

Nearest-even shift rounding in quotient/remainder form.

source

theorem FloatLib.Numerics.roundShiftRightEven_eq_roundQuotientEven (value shift : ℕ) :

roundShiftRightEven value shift = roundQuotientEven value (2 ^ shift)

Nearest-even shifting is nearest-even division by the corresponding power of two.

source

theorem FloatLib.Numerics.shiftRight_le_roundShiftRightEven (value shift : ℕ) :

value.shiftRight shift ≤ roundShiftRightEven value shift

Nearest-even shift rounding is never below the floor quotient.

source

theorem FloatLib.Numerics.roundShiftRightEven_le_shiftRight_add1 (value shift : ℕ) :

roundShiftRightEven value shift ≤ value.shiftRight shift + 1