Verified two-limb rounding

These theorems connect the native UInt128 shifts, increments, and nearest-even rounding operations to their natural-number meanings.

The runtime uses two UInt64 limbs; the proof model interprets them as one Nat. Carry propagation, cross-limb shifts, low-bit insertion, and ties-to-even rounding preserve that interpretation under the stated capacity bounds.

Limb-local primitives

theorem FloatLib.Numerics.FixedWord.UInt128.increment_toNat (value : UInt128) (hfit : value.toNat + 1 < 2 ^ 128) : value.increment.toNat = value.toNat + 1

Mathematical value of two-limb increment when it does not overflow.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt128.setLowBit_toNat (value : UInt128) : value.setLowBit.toNat = value.toNat ||| 1

Setting the low bit of a two-limb value agrees with natural-number bitwise OR.

Cross-limb shifts

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt128.shiftRightOne_toNat (value : UInt128) : value.shiftRightOne.toNat = value.toNat / 2

The native two-word shift is exact division by two.

Nearest-even right shifts

theorem FloatLib.Numerics.FixedWord.UInt128.roundShiftRightOneEven_toNat (value : UInt128) (hfit : value.toNat / 2 + 1 < 2 ^ 128) : value.roundShiftRightOneEven.toNat = Numerics.roundShiftRightEven value.toNat 1

Native one-bit nearest-even rounding agrees with the mathematical rounder.

theorem FloatLib.Numerics.FixedWord.UInt128.shiftRightLow_toNat (value : UInt128) (shift : ℕ) (hpositive : 0 < shift) (hshift : shift < 64) (hhigh : value.hi.toNat < 2 ^ shift) : (value.shiftRightLow shift).toNat = value.toNat >>> shift

When the shifted result fits one limb, shiftRightLow is the mathematical right shift of the two-limb input.

theorem FloatLib.Numerics.FixedWord.UInt128.roundShiftRightEven_toNat (value : UInt128) (shift : ℕ) (hpositive : 0 < shift) (hshift : shift < 64) (hhigh : value.hi.toNat < 2 ^ shift) (hincrementFit : value.toNat >>> shift + 1 < 2 ^ 64) : (value.roundShiftRightEven shift).toNat = Numerics.roundShiftRightEven value.toNat shift

The one-limb result of native two-limb nearest-even rounding agrees with the common mathematical rounder whenever the stated bounds exclude overflow.