Verified four-limb rounding

These theorems connect four-limb shifts, sticky-bit normalization, and nearest-even rounding to their natural-number meanings. Multiplication and fused-operation backends can reuse this layer without converting compiled arithmetic to Nat.

theorem FloatLib.Numerics.FixedWord.UInt256.hasNonzeroBelow_eq (value : UInt256) (width : ℕ) : value.hasNonzeroBelow width = (value.toNat % 2 ^ width != 0)

The fixed-limb low-bit predicate agrees with the natural-number remainder test at every width.

Widths above the four-limb capacity inspect the complete value, matching reduction modulo any power of two at least 2^256.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat_of_lt64 (value : UInt256) (shift : ℕ) (hpositive : 0 < shift) (hshift : shift < 64) (htopWord : value.limb3 = 0) (htopBits : value.limb2.toNat < 2 ^ shift) : (value.shiftRight128 shift).toNat = value.toNat >>> shift

Four-limb shifting by less than one word agrees with >>> when the quotient fits two limbs.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat_of_eq64 (value : UInt256) (htopWord : value.limb3 = 0) : (value.shiftRight128 64).toNat = value.toNat >>> 64

When the top limb is zero, a one-word shift selects the middle two limbs.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat (value : UInt256) (shift : ℕ) (hlarge : 64 < shift) (hshift : shift < 128) (htop : value.limb3.toNat < 2 ^ (shift - 64)) : (value.shiftRight128 shift).toNat = value.toNat >>> shift

Four-limb shifting agrees with mathematical right shift when the result fits two limbs.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat_of_eq128 (value : UInt256) : (value.shiftRight128 128).toNat = value.toNat >>> 128

A two-word shift selects the upper two limbs.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRight128_toNat_of_quotient_lt (value : UInt256) (shift : ℕ) (hfit : value.toNat / 2 ^ shift < 2 ^ 128) : (value.shiftRight128 shift).toNat = value.toNat / 2 ^ shift

A four-limb shift is floor division whenever its quotient fits in the returned two-limb carrier.

Clients need only this fit condition, never the native word-boundary cases. Normalization and later fixed-limb kernels use it.

theorem FloatLib.Numerics.FixedWord.UInt256.shiftRightJam128_toNat (value : UInt256) (shift : ℕ) (hquotient : (value.shiftRight128 shift).toNat = value.toNat / 2 ^ shift) (hdiscarded : value.hasNonzeroBelow shift = (value.toNat % 2 ^ shift != 0)) : (value.shiftRightJam128 shift).toNat = shiftRightJam value.toNat shift

The fixed-limb jam operation refines the representation-independent operation once its quotient and discarded-bit test have been established.

theorem FloatLib.Numerics.FixedWord.UInt256.normalizationShift128_le (value : UInt256) : value.normalizationShift128 ≤ 128

Four-to-two-limb normalization never discards more than 128 bits.

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_lt_pow_normalizationShift128_add (value : UInt256) : value.toNat < 2 ^ (value.normalizationShift128 + 128)

A four-limb value fits below the normalization window selected from its leading bit.

theorem FloatLib.Numerics.FixedWord.UInt256.normalizationQuotient128_lt (value : UInt256) : value.toNat / 2 ^ value.normalizationShift128 < 2 ^ 128

The quotient selected by four-to-two-limb normalization fits in two limbs.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt256.normalizeJam128_toNat (value : UInt256) : value.normalizeJam128.toNat = shiftRightJam value.toNat value.normalizationShift128

Native four-to-two-limb normalization refines representation-independent shift-with-jam.

The quotient fits in two limbs, and the low bit records the OR of the quotient's low bit and the discarded suffix's sticky bit.

theorem FloatLib.Numerics.FixedWord.UInt256.normalizeJam128_toNat_eq_zero_iff (value : UInt256) : value.normalizeJam128.toNat = 0 ↔ value.toNat = 0

Four-to-two-limb normalization is zero exactly when its input is zero.

theorem FloatLib.Numerics.FixedWord.UInt256.roundShiftRightEven128_toNat (value : UInt256) (shift : ℕ) (hlarge : 64 < shift) (hshift : shift < 128) (htop : value.limb3.toNat < 2 ^ (shift - 64)) (hincrementFit : value.toNat >>> shift + 1 < 2 ^ 128) : (value.roundShiftRightEven128 shift).toNat = Numerics.roundShiftRightEven value.toNat shift

Four-limb nearest-even rounding agrees with the generic natural-number rounder.

Four-word subtraction, comparison, and widening

theorem FloatLib.Numerics.FixedWord.UInt256.complement_toNat (value : UInt256) : value.complement.toNat = 2 ^ 256 - 1 - value.toNat

The four-word complement is 2^256 - 1 - value.

theorem FloatLib.Numerics.FixedWord.add256_value_toNat (x y : UInt256) : (add256 x y).value.toNat = (x.toNat + y.toNat) % 2 ^ 256

The value limbs of add256 hold the sum modulo 2^256.

theorem FloatLib.Numerics.FixedWord.UInt256.sub_toNat (x y : UInt256) (hordered : y.toNat ≤ x.toNat) : (x.sub y).toNat = x.toNat - y.toNat

Four-word subtraction agrees with Nat subtraction when the subtrahend is at most the minuend.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt256.less_eq_true_iff (x y : UInt256) : x.less y = true ↔ x.toNat < y.toNat

Native four-word comparison agrees with comparison of mathematical values.

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

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

theorem FloatLib.Numerics.FixedWord.UInt256.double_toNat (value : UInt256) (hvalue : value.toNat < 2 ^ 255) : value.double.toNat = value.toNat * 2

Doubling a four-limb value below 2^255 agrees with Nat doubling.

theorem FloatLib.Numerics.FixedWord.UInt128.shiftLeft256_toNat (value : UInt128) (shift : ℕ) (hshift : shift < 128) : (value.shiftLeft256 shift).toNat = value.toNat <<< shift

The widening shuffle agrees with <<< for every shift below 128.