Verified fixed-limb significand products

mul128_toNat proves the full 128 × 128 → 256 product correct using the mul64_toNat theorem from Core.Proof.UInt128. The addition theorems reconstruct the sum from its low limbs and outgoing carry. The UInt256 lemmas describe widening, projection, and leading-bit selection.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_ofUInt128 (value : UInt128) : (ofUInt128 value).toNat = value.toNat

Embedding a two-limb value in four limbs preserves its mathematical value.

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_ofUInt128ShiftedLeft (value : UInt128) (shift : ℕ) (hlower : 64 < shift) (hupper : shift < 128) : (ofUInt128ShiftedLeft value shift).toNat = value.toNat <<< shift

ofUInt128ShiftedLeft agrees with <<< for shifts strictly between 64 and 128.

theorem FloatLib.Numerics.FixedWord.UInt256.low128_toNat_of_lt (value : UInt256) (hvalue : value.toNat < 2 ^ 128) : value.low128.toNat = value.toNat

A four-limb value below 2^128 keeps its whole value under low128.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_eq_zero_iff (value : UInt256) : value.toNat = 0 ↔ value = { limb3 := 0, limb2 := 0, limb1 := 0, limb0 := 0 }

A four-limb value has mathematical value zero exactly when every limb is zero.

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_injective : Function.Injective toNat

A four-word value is determined by its natural-number interpretation.

theorem FloatLib.Numerics.FixedWord.add64_toNat (x y : UInt64) : have result := add64 x y; result.value.toNat + result.carry.toNat * 2 ^ 64 = x.toNat + y.toNat

Native addition with carry represents the natural-number sum.

theorem FloatLib.Numerics.FixedWord.add64_carry_le_one (x y : UInt64) : (add64 x y).carry.toNat ≤ 1

add64 returns a carry of zero or one.

theorem FloatLib.Numerics.FixedWord.addCarry64_toNat (x y carry : UInt64) : have result := addCarry64 x y carry; result.value.toNat + result.carry.toNat * 2 ^ 64 = x.toNat + y.toNat + carry.toNat

addCarry64 represents natural-number addition with an incoming carry.

theorem FloatLib.Numerics.FixedWord.addCarry64_carry_le_one (x y carry : UInt64) (hcarry : carry.toNat ≤ 1) : (addCarry64 x y carry).carry.toNat ≤ 1

If the incoming carry of addCarry64 is a bit, so is the outgoing carry.

theorem FloatLib.Numerics.FixedWord.add128_toNat (x y : UInt128) : have result := add128 x y; result.value.toNat + result.carry.toNat * 2 ^ 128 = x.toNat + y.toNat

add128 represents natural-number addition, including its carry above bit 127.

theorem FloatLib.Numerics.FixedWord.add128_carry_le_one (x y : UInt128) : (add128 x y).carry.toNat ≤ 1

add128 returns a carry of zero or one.

theorem FloatLib.Numerics.FixedWord.add128_carry_eq_zero_of_lt (x y : UInt128) (hfit : x.toNat + y.toNat < 2 ^ 128) : (add128 x y).carry = 0

A 128-bit addition has no carry when its mathematical sum fits in 128 bits.

theorem FloatLib.Numerics.FixedWord.add128_value_toNat_of_carry_zero (x y : UInt128) (hcarry : (add128 x y).carry = 0) : (add128 x y).value.toNat = x.toNat + y.toNat

When add128 returns a zero carry, its value limbs hold the whole sum.

theorem FloatLib.Numerics.FixedWord.add128_value_toNat_of_lt (x y : UInt128) (hfit : x.toNat + y.toNat < 2 ^ 128) : (add128 x y).value.toNat = x.toNat + y.toNat

The low two limbs of add128 contain the ordinary sum whenever that sum fits in 128 bits.

Fixed-limb midpoint, significand, and remainder kernels all need this fact, so it lives next to add128 instead of in backend-local copies of the same carry argument.

theorem FloatLib.Numerics.FixedWord.add256_toNat (x y : UInt256) : have result := add256 x y; result.value.toNat + result.carry.toNat * 2 ^ 256 = x.toNat + y.toNat

add256 represents natural-number addition, including its carry above bit 255.

theorem FloatLib.Numerics.FixedWord.add256_value_toNat_of_carry_zero (x y : UInt256) (hcarry : (add256 x y).carry = 0) : (add256 x y).value.toNat = x.toNat + y.toNat

When add256 returns a zero carry, its value limbs hold the whole sum.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt256.log2_toNat (value : UInt256) : value.log2 = value.toNat.log2

Native four-limb leading-bit selection agrees with Nat.log2.

theorem FloatLib.Numerics.FixedWord.UInt256.toNat_lt (value : UInt256) : value.toNat < 2 ^ 256

Every four-word unsigned value is below 2^256.

@[simp]

theorem FloatLib.Numerics.FixedWord.mul128_toNat (x y : UInt128) : (mul128 x y).toNat = x.toNat * y.toNat

mul128 computes the full mathematical product of its operands.