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, and 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.Internal.increment (value : UInt128) : UInt128

UInt128.increment with the low-word carry kept as a native word.

@[csimp]

theorem FloatLib.Numerics.FixedWord.UInt128.increment_eq_internal : increment = Internal.increment

Compiled code runs UInt128.increment as UInt128.Internal.increment. The two are equal by rfl.

@[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, the quotient is incremented 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.UInt128.roundShiftRightEven128 (value : UInt128) (shift : ℕ) : UInt128

Round a two-limb value right by shift using round-to-nearest, ties-to-even, keeping both limbs.

The kernel is meaningful for 0 < shift < 64, the contract of UInt128.roundShiftRightEven128_toNat.

@[inline]

def FloatLib.Numerics.FixedWord.UInt128.jamCombine (sameSign exact : Bool) (A q : UInt128) : UInt128

FixedWord.jamCombine on two-word values (UInt128.jamCombine_toNat).

@[inline]

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

Low 128 bits of a four-word right shift.

Shifts at and beyond 256 return zero. A caller that needs the complete quotient must show that no nonzero bit remains above the returned two-word window. The 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.

For the floating-point formulation, see Sylvie Boldo and Guillaume Melquiond, "Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd" (2008), §III-C, Theorem 3. The fixed-grid statement used here is FloatLib.Numerics.roundShiftRightEven_shiftRightJam.

@[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 below 2^128 use a zero shift. Wider values keep their leading bit at position 127.

@[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, because 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 these hypotheses. Two-word products call this with shifts fracWidth or fracWidth + 1, which is 112 or 113 for binary128.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.complement (value : UInt256) : UInt256

Bitwise complement of a four-word value.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.sub (x y : UInt256) : UInt256

Subtract two four-word values modulo 2^256 by adding the two's complement of the subtrahend. sub_toNat gives the natural-number difference when the subtrahend is at most the minuend.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.less (x y : UInt256) : Bool

Compare two four-word values.

@[inline]

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

Set the least-significant bit of a four-word value.

@[inline]

def FloatLib.Numerics.FixedWord.UInt256.double (value : UInt256) : UInt256

Double a four-word value modulo 2^256.

@[inline]

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

Embed a two-word value shifted left by shift < 128 bits into four words. Every shift below 128 is supported, including those UInt256.ofUInt128ShiftedLeft does not cover.