Deterministic nearest-even shift rounding #

Power-of-two nearest-even rounding shared by binary floating-point, fixed-point, and other quantized representations. The executable path avoids constructing an enormous halfway marker when the shift exceeds the input bit length.

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. A bit-length check returns zero before constructing the halfway marker 2^(shift - 1) when the shift is too large.

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.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.

The runtime definition has an extra branch returning 0 when shift exceeds the bit length of value; it exists only to avoid allocating an enormous halfway marker. That branch is invisible here because the quotient is then zero and the discarded value lies strictly below half, so proofs can work with the plain quotient/remainder equation.

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

Nearest-even shift rounding is at most one above the floor quotient.