UInt128: 128-bit integers

Definitions and basics

@[unbox]

structure UInt128 : Type

• lo : UInt64
• hi : UInt64

theorem UInt128.ext {x y : UInt128} (lo : x.lo = y.lo) (hi : x.hi = y.hi) : x = y

theorem UInt128.ext_iff {x y : UInt128} : x = y ↔ x.lo = y.lo ∧ x.hi = y.hi

instance instDecidableEqUInt128 : DecidableEq UInt128

Equations

• instDecidableEqUInt128 = instDecidableEqUInt128.decEq

def instDecidableEqUInt128.decEq (x✝ x✝¹ : UInt128) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqUInt128.decEq { lo := a, hi := a_1 } { lo := b, hi := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def instBEqUInt128.beq : UInt128 → UInt128 → Bool

Equations

• instBEqUInt128.beq { lo := a, hi := a_1 } { lo := b, hi := b_1 } = (a == b && a_1 == b_1)
• instBEqUInt128.beq x✝¹ x✝ = false

instance instBEqUInt128 : BEq UInt128

Equations

• instBEqUInt128 = { beq := instBEqUInt128.beq }

def UInt128.size : ℕ

Equations

• UInt128.size = 2 ^ 128

def UInt128.max : UInt128

Equations

• UInt128.max = { lo := UInt64.max, hi := UInt64.max }

instance instZeroUInt128 : Zero UInt128

Equations

• instZeroUInt128 = { zero := { lo := 0, hi := 0 } }

instance instOneUInt128 : One UInt128

Equations

• instOneUInt128 = { one := { lo := 1, hi := 0 } }

@[irreducible]

def UInt128.toNat (x : UInt128) : ℕ

Equations

• x.toNat = x.hi.toNat <<< 64 + x.lo.toNat

def UInt128.toReal (x : UInt128) : ℝ

Equations

• ↑x = ↑x.toNat

instance instCoeUInt128Real : Coe UInt128 ℝ

Equations

• instCoeUInt128Real = { coe := UInt128.toReal }

@[simp]

theorem UInt128.toNat_zero : toNat 0 = 0

@[simp]

theorem UInt128.toNat_one : toNat 1 = 1

@[simp]

theorem UInt128.zero_lo : lo 0 = 0

@[simp]

theorem UInt128.zero_hi : hi 0 = 0

@[simp]

theorem UInt128.max_lo : max.lo = UInt64.max

@[simp]

theorem UInt128.max_hi : max.hi = UInt64.max

theorem UInt128.max_eq_pow_sub_one : max.toNat = 2 ^ 128 - 1

theorem UInt128.toNat_def {x : UInt128} : x.toNat = x.hi.toNat * 2 ^ 64 + x.lo.toNat

@[simp]

theorem UInt128.toReal_zero : ↑0 = 0

@[simp]

theorem UInt128.toReal_one : ↑1 = 1

theorem UInt128.lt_size (x : UInt128) : x.toNat < 2 ^ 128

theorem UInt128.coe_nonneg (x : UInt128) : 0 ≤ ↑x

theorem UInt128.coe_lt_size (x : UInt128) : ↑x < 2 ^ 128

noncomputable instance instCoeTailUInt128ZMod {n : ℕ} : CoeTail UInt128 (ZMod n)

Equations

• instCoeTailUInt128ZMod = { coe := fun (x : UInt128) => ↑x.toNat }

@[simp]

theorem UInt128.toNat_max : max.toNat = 2 ^ 128 - 1

@[simp]

theorem Nat.mod_mul_eq_mul_mod_128 (a : ℕ) : a * 2 ^ 64 % 2 ^ 128 = a % 2 ^ 64 * 2 ^ 64

@[simp]

theorem UInt128.toNat_mod_pow_eq_lo (x : UInt128) : x.toNat % 2 ^ 64 = x.lo.toNat

@[simp]

theorem UInt128.toNat_div_pow_eq_hi (x : UInt128) : x.toNat / 2 ^ 64 = x.hi.toNat

theorem UInt128.eq_iff_toNat_eq (x y : UInt128) : x = y ↔ x.toNat = y.toNat

theorem UInt128.eq_zero_iff (x : UInt128) : x = 0 ↔ x.toNat = 0

theorem UInt128.ne_zero_iff (x : UInt128) : x ≠ 0 ↔ x.toNat ≠ 0

@[simp]

theorem UInt128.toNat_lo {x : UInt128} (h : x.toNat < 2 ^ 64) : x.lo.toNat = x.toNat

def UInt128.blt (x y : UInt128) : Bool

Equations

• x.blt y = (decide (x.hi < y.hi) || x.hi == y.hi && decide (x.lo < y.lo))

instance instLawfulBEqUInt128 : LawfulBEq UInt128

UInt128 has nice equality

@[simp]

theorem UInt128.toNat_lt (x : UInt128) : x.toNat < 2 ^ 128

Wrap around conversion from ℕ, ℤ to UInt128

@[irreducible]

def UInt128.ofNat (x : ℕ) : UInt128

Equations

• UInt128.ofNat x = { lo := UInt64.ofNat x, hi := UInt64.ofNat (x / 2 ^ 64) }

@[irreducible]

def UInt128.ofInt (x : ℤ) : UInt128

Equations

• UInt128.ofInt x = { lo := UInt64.ofInt x, hi := UInt64.ofInt (x / 2 ^ 64) }

@[simp]

theorem UInt128.toNat_ofNat (x : ℕ) : (ofNat x).toNat = x % 2 ^ 128

@[simp]

theorem UInt128.ofInt_toInt (x : UInt128) : ofInt ↑x.toNat = x

@[simp]

theorem UInt128.toInt_ofInt (x : ℤ) : ↑(ofInt x).toNat = x % 2 ^ 128

@[simp]

theorem UInt128.ofInt_zero : ofInt 0 = 0

@[simp]

theorem UInt128.ofInt_pow : ofInt (2 ^ 128) = 0

128-bit increment

@[irreducible]

def UInt128.succ (x : UInt128) : UInt128

Equations

• x.succ = { lo := x.lo + 1, hi := x.hi + bif x.lo + 1 == 0 then 1 else 0 }

@[simp]

theorem UInt128.succ_max : max.succ = 0

theorem UInt128.toNat_succ {x : UInt128} (h : x.toNat ≠ 2 ^ 128 - 1) : x.succ.toNat = x.toNat + 1

theorem UInt128.toNat_succ' (x : UInt128) : x.succ.toNat = if x.toNat = 2 ^ 128 - 1 then 0 else x.toNat + 1

theorem UInt128.coe_succ {x : UInt128} (h : ↑x ≠ 2 ^ 128 - 1) : ↑x.succ = ↑x + 1

Complement

instance instComplementUInt128 : Complement UInt128

Equations

• instComplementUInt128 = { complement := fun (x : UInt128) => { lo := ~~~x.lo, hi := ~~~x.hi } }

theorem UInt128.complement_def (x : UInt128) : ~~~x = { lo := ~~~x.lo, hi := ~~~x.hi }

@[simp]

theorem UInt128.complement_zero : ~~~0 = max

theorem UInt128.toNat_complement {x : UInt128} : (~~~x).toNat = 2 ^ 128 - 1 - x.toNat

Twos complement negation

instance instNegUInt128 : Neg UInt128

Equations

• instNegUInt128 = { neg := fun (x : UInt128) => (~~~x).succ }

theorem UInt128.neg_def (x : UInt128) : -x = (~~~x).succ

@[simp]

theorem UInt128.neg_zero : -0 = 0

theorem UInt128.toNat_neg (x : UInt128) : (-x).toNat = if x = 0 then 0 else 2 ^ 128 - x.toNat

@[simp]

theorem UInt128.neg_ofInt (x : ℤ) : -ofInt x = ofInt (-x)

ofInt commutes with -

128-bit addition and (twos complement) subtraction

@[irreducible]

def UInt128.add (x y : UInt128) : UInt128

Equations

• x.add y = match addc x.lo y.lo with | (x0, x1) => { lo := x0, hi := x1 + x.hi + y.hi }

instance instAddUInt128 : Add UInt128

Equations

• instAddUInt128 = { add := UInt128.add }

instance instSubUInt128 : Sub UInt128

Equations

• instSubUInt128 = { sub := fun (x y : UInt128) => x + -y }

theorem UInt128.add_def (x y : UInt128) : x + y = x.add y

theorem UInt128.sub_def (x y : UInt128) : x - y = x + -y

theorem UInt128.toNat_add (x y : UInt128) : (x + y).toNat = (x.toNat + y.toNat) % 2 ^ 128

add is modular

@[simp]

theorem UInt128.add_ofInt (x y : ℤ) : ofInt x + ofInt y = ofInt (x + y)

ofInt commutes with +

@[simp]

theorem UInt128.sub_ofInt (x y : ℤ) : ofInt x - ofInt y = ofInt (x - y)

ofInt commutes with -

instance instAddCommGroupUInt128 : AddCommGroup UInt128

UInt128 inherits the additive group structure from ℤ

Equations

• One or more equations did not get rendered due to their size.

64 → 128 bit multiplication

We define the product of two UInt64s, as a 128-bit int. Let s = 2^32. Then we have

x = x1 s + x0 y = y1 s + y0 x y = x1 y1 s^2 + (x1 y0 + x0 y1) s + x0 y0

Using addc, we have

x y = x1 y1 s^2 + (x1 y0 + x0 y1) s + x0 y0 a1, a3 = addc (x1 y0) (x0 y1) x y = (a3 s + x1 y1) s^2 + a1 s + x0 y0 b1, b2 = split a1 x y = (a3 s + x1 y1 + b2) s^2 + b1 s + x0 y0 c0, c2 = addc (x0 y0) b1 x y = (a3 s + x1 y1 + b2 + c2) s^2 + c0

@[irreducible]

def mul128 (x y : UInt64) : UInt128

All the bits of two UInt64 multiplied together

Equations

• One or more equations did not get rendered due to their size.

theorem mul_lt_32 {x y : ℕ} (xl : x < 2 ^ 32) (yl : y < 2 ^ 32) : x * y < UInt64.size

theorem toNat_mul128_mod (x y : UInt64) : (mul128 x y).toNat % 2 ^ 128 = x.toNat * y.toNat % 2 ^ 128

mul128 is correct mod 2^128

@[simp]

theorem toNat_mul128 (x y : UInt64) : (mul128 x y).toNat = x.toNat * y.toNat

mul128 is correct

128 bit shifting

@[irreducible]

def UInt128.shiftLeft (x : UInt128) (s : UInt64) : UInt128

Multiply by 2^(s % 128), discarding overflow bits

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def UInt128.shiftRight (x : UInt128) (s : UInt64) : UInt128

Divide by 2^(s % 128), rounding down

Equations

• One or more equations did not get rendered due to their size.

instance instHShiftLeftUInt128UInt64 : HShiftLeft UInt128 UInt64 UInt128

Equations

• instHShiftLeftUInt128UInt64 = { hShiftLeft := fun (x : UInt128) (s : UInt64) => x.shiftLeft s }

instance instHShiftRightUInt128UInt64 : HShiftRight UInt128 UInt64 UInt128

Equations

• instHShiftRightUInt128UInt64 = { hShiftRight := fun (x : UInt128) (s : UInt64) => x.shiftRight s }

theorem UInt128.shiftLeft_def (x : UInt128) (s : UInt64) : x <<< s = x.shiftLeft s

theorem UInt128.shiftRight_def (x : UInt128) (s : UInt64) : x >>> s = x.shiftRight s

@[irreducible]

def UInt128.shiftRightRound (x : UInt128) (s : UInt64) (up : Bool) : UInt128

Divide by 2^s, rounding up or down

Equations

• x.shiftRightRound s up = bif s == 0 then x else bif decide (128 ≤ s) then bif x == 0 || !up then 0 else 1 else have y := x >>> s; bif up && x != y <<< s then y.succ else y

@[irreducible]

def UInt128.shiftLeftSaturate (x : UInt128) (s : UInt64) : UInt128

Multiply by 2^s, saturating at UInt128.max if we overflow

Equations

• x.shiftLeftSaturate s = bif bif decide (128 ≤ s) then x != 0 else s != 0 && x >>> (128 - s) != 0 then UInt128.max else x <<< s

theorem UInt128.testBit_eq {x : UInt128} {i : ℕ} : x.toNat.testBit i = if i < 64 then x.lo.toNat.testBit i else x.hi.toNat.testBit (i - 64)

testBit for UInt128

theorem UInt128.testBit_eq_zero {x : UInt128} {i : ℕ} (h : 128 ≤ i) : x.toNat.testBit i = false

testBit is zero for large i

theorem tb_eq {x : UInt64} {i j : ℕ} (ij : i = j ∨ 64 ≤ i ∧ 64 ≤ j) : x.toNat.testBit i = x.toNat.testBit j

theorem tb_ne {x y : UInt64} {i j : ℕ} (il : 64 ≤ i) (jl : 64 ≤ j) : x.toNat.testBit i = y.toNat.testBit j

theorem false_tb {x : UInt64} {i : ℕ} (il : 64 ≤ i) : false = x.toNat.testBit i

theorem tb_false {x : UInt64} {i : ℕ} (il : 64 ≤ i) : x.toNat.testBit i = false

theorem p64 : UInt64.toNat 64 = 64

theorem p127 : UInt64.toNat 127 = 127

theorem p128 : UInt64.toNat 128 = 128

theorem p64s : (2 ^ 64 - 1).toNat = 2 ^ 64 - 1

theorem ts0 {t : ℕ} (h : t < 64) : t < UInt64.size

theorem ts1 {t : ℕ} (h : t < 128) : t < UInt64.size

theorem shift0 {t : ℕ} (t0 : t ≠ 0) (t64 : t < 64) : (64 - UInt64.ofNat t).toNat % 64 = 64 - t

theorem t127 {t : ℕ} (h : t < 128) : t &&& 127 = t

theorem t127' {t : ℕ} (h : t < 128) : UInt64.ofNat t &&& 127 = UInt64.ofNat t

theorem e0 {t : ℕ} (t0 : t ≠ 0) (t64 : t < 64) : (64 - UInt64.ofNat t).toNat % 64 = 64 - t

theorem e1 {t : ℕ} (h : t < 64) : 64 - (64 - t) = t

theorem e2 {t i : ℕ} (h : t < 64) : i - (64 - t) = i + t - 64

theorem e3 {t : ℕ} (t64 : 64 ≤ t) (t128 : t < 128) : (UInt64.ofNat t - 64).toNat % 64 = t - 64

theorem e4 {t i : ℕ} (h : 64 ≤ t) : i + (t - 64) = i + t - 64

theorem e6 {t : ℕ} (t0 : t ≠ 0) (t64 : t < 64) : (64 - UInt64.ofNat t).toNat % 64 = 64 - t

theorem e7 {t i : ℕ} (hi : 64 ≤ i) (ht : t < 64) : i - 64 + (64 - t) = i - t

theorem e8 {t i : ℕ} (ht : 64 ≤ t) : i - 64 - (t - 64) = i - t

theorem e9 {t : ℕ} (h : t < 128) : (128 - UInt64.ofNat t).toNat = 128 - t

theorem e10 : 128 &&& 127 = 0

theorem a1 {t i : ℕ} (t0 : t ≠ 0) (i64 : i < 64) : i + t - 64 < t

theorem a2 {x : UInt128} {t : ℕ} {x0 : x ≠ 0} (h : 128 ≤ t) : ¬x.toNat * 2 ^ t ≤ 2 ^ 128 - 1

theorem a4 {t i : ℕ} (hi : i < 64) (ht : 64 ≤ t) : ¬t ≤ i

theorem a5 {t i : ℕ} (hi : i < 64) (ti : t < 64) : i - t < 64 - t

theorem UInt128.toNat_shiftLeft (x : UInt128) {s : UInt64} (sl : s < 128) : (x <<< s).toNat = x.toNat * 2 ^ s.toNat % 2 ^ 128

shiftLeft is multiplication mod 2^128.

theorem UInt128.toNat_shiftLeft' (x : UInt128) {s : UInt64} : (x <<< s).toNat = x.toNat * 2 ^ (s.toNat % 128) % 2 ^ 128

shiftLeft is multiplication mod 2^128.

@[simp]

theorem UInt128.shiftLeft_zero (x : UInt128) : x <<< 0 = x

Shifting left by zero does nothing

@[simp]

theorem UInt128.zero_shiftLeft (s : UInt64) : 0 <<< s = 0

Shifting zero does nothing

theorem UInt128.toNat_shiftRight (x : UInt128) {s : UInt64} (sl : s < 128) : (x >>> s).toNat = x.toNat / 2 ^ s.toNat

shiftRight rounds down

theorem UInt128.toNat_shiftRight' (x : UInt128) {s : UInt64} : (x >>> s).toNat = x.toNat / 2 ^ (s.toNat % 128)

shiftRight rounds down

theorem UInt128.coe_shiftRight (x : UInt128) {s : UInt64} (sl : s < 128) : ↑(x >>> s) = ↑(x.toNat / 2 ^ s.toNat)

theorem UInt128.toInt_shiftRightRound (x : UInt128) (s : UInt64) (up : Bool) : ↑(x.shiftRightRound s up).toNat = (↑x.toNat).rdiv (2 ^ s.toNat) up

shiftRightRound.toNat = rdiv

theorem UInt128.approx_shiftRightRound (x : UInt128) (s : UInt64) (up : Bool) : Rounds (↑(x.shiftRightRound s up)) (↑x / 2 ^ s.toNat) up

shiftRightRound rounds as desired

theorem UInt128.toNat_shiftLeftSaturate {x : UInt128} {s : UInt64} : (x.shiftLeftSaturate s).toNat = min (x.toNat * 2 ^ s.toNat) max.toNat

theorem UInt128.shiftLeftSaturate_eq {x : UInt128} {s : UInt64} : x.shiftLeftSaturate s = ofNat (min (x.toNat * 2 ^ s.toNat) max.toNat)

@[simp]

theorem UInt128.zero_shiftRight {s : UInt64} : 0 >>> s = 0

@[simp]

theorem UInt128.zero_shiftRightRound {s : UInt64} {up : Bool} : shiftRightRound 0 s up = 0

@[simp]

theorem UInt128.shiftRightRound_zero {x : UInt128} {up : Bool} : x.shiftRightRound 0 up = x

log2

@[irreducible]

def UInt128.log2 (x : UInt128) : UInt64

Equations

• x.log2 = bif x.hi == 0 then x.lo.fast_log2 else x.hi.fast_log2 + 64

@[simp]

theorem UInt128.toNat_log2 (x : UInt128) : x.log2.toNat = x.toNat.log2

@[simp]

theorem UInt128.log2_le_127 (x : UInt128) : x.log2 ≤ 127

@[simp]

theorem UInt128.log2_le_127' (x : UInt128) : x.toNat.log2 ≤ 127

@[simp]

theorem UInt128.log2_zero : log2 0 = 0

@[simp]

theorem UInt128.toNat_lo_of_log2_lt {x : UInt128} (h : x.toNat.log2 < 64) : x.lo.toNat = x.toNat

theorem UInt128.toNat_hi_shiftRightRound_le_hi {y s : UInt64} {up : Bool} : ({ lo := 0, hi := y }.shiftRightRound s up).hi.toNat ≤ y.toNat

Shifting some high bits down produces a small value