Limb arrays: shifts and nearest-even rounding

Bit shifts of a LimbArray by an arbitrary count, with optional nearest-even rounding. A shift by k bits moves whole limbs by k / 32 and then combines adjacent limbs to shift by the remaining k % 32 bits; Array.ofFn builds each result limb from at most two source limbs.

roundShiftRightEven reads the guard bit and the sticky bits directly from the source array and increments the shifted quotient with one carry-propagating addAt; it never forms the halfway value 2^(shift - 1) that the arbitrary-precision rounder compares against. Shift.Proof proves that it agrees with Numerics.roundShiftRightEven.

@[inline]

def FloatLib.Numerics.LimbArray.shiftLeftLimb (v : LimbArray) (q r i : Nat) : UInt32

Result limb i of a left shift by 32 q + r bits, for r < 32.

def FloatLib.Numerics.LimbArray.shiftLeft (v : LimbArray) (k : Nat) : LimbArray

The value shifted left by k bits, in size + k / 32 + 1 limbs.

@[inline]

def FloatLib.Numerics.LimbArray.shiftRightLimb (v : LimbArray) (q r i : Nat) : UInt32

Result limb i of a right shift by 32 q + r bits, for r < 32.

def FloatLib.Numerics.LimbArray.shiftRight (v : LimbArray) (k : Nat) : LimbArray

The value shifted right by k bits, keeping the stored limb count.

def FloatLib.Numerics.LimbArray.roundShiftRightEven (v : LimbArray) (shift : Nat) : LimbArray

The value divided by 2^shift, rounded to nearest with ties to even.

The guard bit is bit shift - 1, the sticky bits are those below it, and the quotient is odd exactly when bit shift is set. The quotient is incremented when the guard bit is set and either a sticky bit or the quotient's low bit is set. A zero shift returns the array unchanged.