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, and the proof model interprets them as one Nat. Carry propagation, cross-limb shifts, low-bit insertion, ties-to-even rounding, and the sticky combination of an aligned sum 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 one-bit shift is floor 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.

theorem FloatLib.Numerics.FixedWord.UInt128.roundShiftRightEven128_toNat (value : UInt128) (shift : ℕ) (hpositive : 0 < shift) (hshift : shift < 64) : (value.roundShiftRightEven128 shift).toNat = Numerics.roundShiftRightEven value.toNat shift

Native two-limb nearest-even rounding with a two-limb quotient agrees with the common mathematical rounder for every shift strictly between zero and 64.

theorem FloatLib.Numerics.FixedWord.UInt128.jamCombine_toNat (sameSign exact : Bool) (A q : UInt128) (B d : ℕ) (hq : q.toNat = B / 2 ^ d) (hexact : exact = decide (B % 2 ^ d = 0)) (hfit : A.toNat + q.toNat < 2 ^ 128) (hsub : sameSign = false → q.toNat + 1 ≤ A.toNat ∧ B ≤ A.toNat * 2 ^ d) : (jamCombine sameSign exact A q).toNat = shiftRightJam (if sameSign = true then A.toNat * 2 ^ d + B else A.toNat * 2 ^ d - B) d

The two-word sticky combination is the natural-number jam of the exact aligned value.