Fixed-limb rounding

Two- and four-limb shifts and nearest-even rounding, with guard, sticky, and carry results. Fixed tuples give these small kernels a statically sized representation. Callers handle exponents and packing; LimbRound.Proof relates the operations to natural-number arithmetic.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.increment (value : UInt128) : UInt128

Increment modulo 2^128, propagating the low-word carry.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.setLowBit (value : UInt128) : UInt128

Set the least-significant bit of a two-limb value.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.shiftRightOne (value : UInt128) : UInt128

Shift a two-word value right by one bit.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.roundShiftRightOneEven (value : UInt128) : UInt128

Round a two-word value right by one bit using round-to-nearest, ties-to-even.

For a one-bit shift, incrementing is required exactly when the two low input bits are 11.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.shiftRightLow (value : UInt128) (shift : ℕ) : UInt64

Low 64 bits of a right shift by an amount strictly between zero and 64.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.roundShiftRightEven (value : UInt128) (shift : ℕ) : UInt64

Round a two-limb value right by shift, returning a single native word.

The kernel is meaningful for 0 < shift < 64 with value.hi < 2^shift, so that the quotient fits one word, and callers also keep the incremented quotient below 2^64. roundShiftRightEven_toNat states these hypotheses.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.shiftRight128 (value : UInt256) (shift : ℕ) : UInt128

Low 128 bits of a four-word right shift.

The operation is total: shifts at and beyond 256 return zero. Callers that need the complete quotient establish separately that no nonzero bit remains above the returned two-word window. The explicit limb ranges avoid the modulo reduction performed by native machine-word shifts.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.hasNonzeroBelow (value : UInt256) (width : ℕ) : Bool

Test whether any of the lowest width bits of a four-word value is nonzero.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.shiftRightJam128 (value : UInt256) (shift : ℕ) : UInt128

Shift right into two words, setting the low bit if any bit below the shift position is nonzero.

When the shifted quotient fits in two words, this is round-to-odd, or sticky, normalization. It preserves nearest-even rounding when the final rounder discards at least two more bits.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.normalizationShift128 (value : UInt256) : ℕ

Number of low bits discarded when reducing a four-limb value to a normalized two-limb value.

Values already fitting below bit 128 use a zero shift. Wider values retain their leading bit at position 127, independently of the arithmetic operation that produced them.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.normalizeJam128 (value : UInt256) : UInt128

Normalize a four-limb value into two limbs while jamming every discarded one bit into bit zero.

The result retains the leading 128-bit window, with its low bit ORed with the sticky bit of the discarded suffix. This preserves nearest-even rounding when the final rounder discards at least two more bits.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.roundShiftRightEven128 (value : UInt256) (shift : ℕ) : UInt128

Round a four-limb value right by shift, returning a two-limb result.

The kernel is only valid for 64 < shift < 128: the discarded field is read from limb1 and limb0, and the halfway marker is built inside limb1. Callers also keep value.limb3 < 2^(shift - 64) and the incremented quotient below 2^128, so that shiftRight128 returns the complete quotient. roundShiftRightEven128_toNat states exactly these hypotheses. Two-word products call this with shifts fracWidth or fracWidth + 1, which is 112 or 113 for binary128.