Verified fixed-limb differences

The helpers of Difference.Runtime compare, subtract, normalize, and shift two-word unsigned values without converting the executable path to Nat. The theorems here give their mathematical values for format-specific subtraction proofs.

@[simp]

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

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

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt128.compare_eq_toNat_compare_toNat (x y : UInt128) : x.compare y = Ord.compare x.toNat y.toNat

Native three-way comparison agrees with comparison of mathematical values.

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

Ordered two-word subtraction agrees with natural-number subtraction.

@[simp]

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

Native two-word leading-bit selection agrees with Nat.log2.

@[simp]

theorem FloatLib.Numerics.FixedWord.UInt128.shiftRight_toNat (value : UInt128) (shift : ℕ) : (value.shiftRight shift).toNat = value.toNat / 2 ^ shift

Native two-word right shift, defined for every shift, is floor division by a power of two.

theorem FloatLib.Numerics.FixedWord.UInt128.singleBit_toNat_of_lt (index : ℕ) (hindex : index < 128) : (singleBit index).toNat = 2 ^ index

A bounded native one-hot value represents the corresponding power of two.

theorem FloatLib.Numerics.FixedWord.UInt128.shiftLeft_toNat (value : UInt128) (shift : ℕ) (hshift : shift < 128) (hfit : value.toNat <<< shift < 2 ^ 128) : (value.shiftLeft shift).toNat = value.toNat <<< shift

A two-word left shift that does not overflow agrees with the natural-number shift.

theorem FloatLib.Numerics.FixedWord.UInt128.shiftLeft_of_ge (value : UInt128) (shift : ℕ) (hshift : 128 ≤ shift) : value.shiftLeft shift = { hi := 0, lo := 0 }

Shifting a two-word value left by at least the carrier width returns zero.

theorem FloatLib.Numerics.FixedWord.UInt128.shiftRight_shiftLeft_beq (low : UInt128) (d : ℕ) (hlowNe : low.toNat ≠ 0) : ((low.shiftRight d).shiftLeft d == low) = decide (low.toNat % 2 ^ d = 0)

Shifting a nonzero two-word value right and back left returns it exactly when the shift drops only zero bits.