def UInt64.word : Nat

The radix for a single UInt64 word.

Equations

• UInt64.word = 2 ^ 64

theorem UInt64.word_pos : 0 < word

The UInt64 word radix is positive.

theorem UInt64.toNat_lt_word (a : UInt64) : a.toNat < word

Every UInt64 value is strictly below the word radix.

theorem UInt64.toNat_ofNat_mod_word (n : Nat) : (ofNat n).toNat = n % word

UInt64.ofNat reduces Nat values modulo the word radix.

@[extern lean_hex_uint64_mul_hi]

def UInt64.mulHi (a b : UInt64) : UInt64

The high 64 bits of the product a * b, viewed in radix 2^64.

Equations

• a.mulHi b = UInt64.ofNat (a.toNat * b.toNat / UInt64.word)

@[extern lean_hex_uint64_mul_full]

def UInt64.mulFull (a b : UInt64) : UInt64 × UInt64

The full UInt64 × UInt64 product, split into high and low radix-2^64 words.

Equations

• a.mulFull b = (UInt64.ofNat (a.toNat * b.toNat / UInt64.word), UInt64.ofNat (a.toNat * b.toNat))

@[extern lean_hex_uint64_add_carry]

def UInt64.addCarry (a b : UInt64) (cin : Bool) : UInt64 × Bool

Add a, b, and an incoming carry bit, returning the wrapped low word and the outgoing carry bit.

Equations

• a.addCarry b cin = (UInt64.ofNat (a.toNat + b.toNat + cin.toNat), decide (UInt64.word ≤ a.toNat + b.toNat + cin.toNat))

@[extern lean_hex_uint64_sub_borrow]

def UInt64.subBorrow (a b : UInt64) (bin : Bool) : UInt64 × Bool

Subtract b and an incoming borrow bit from a, returning the wrapped low word and the outgoing borrow bit.

Equations

• a.subBorrow b bin = if b.toNat + bin.toNat ≤ a.toNat then (UInt64.ofNat (a.toNat - (b.toNat + bin.toNat)), false) else (UInt64.ofNat (UInt64.word + a.toNat - (b.toNat + bin.toNat)), true)

@[simp]

theorem UInt64.toNat_addCarry_fst (a b : UInt64) (cin : Bool) : (a.addCarry b cin).fst.toNat = (a.toNat + b.toNat + cin.toNat) % word

Low-word projection of UInt64.addCarry as natural-number reduction modulo 2^64.

theorem UInt64.addCarry_snd (a b : UInt64) (cin : Bool) : (a.addCarry b cin).snd = decide (word ≤ a.toNat + b.toNat + cin.toNat)

The outgoing carry bit of UInt64.addCarry is set exactly when the exact sum overflows.

theorem UInt64.addCarry_snd_eq_true (a b : UInt64) (cin : Bool) : (a.addCarry b cin).snd = true ↔ word ≤ a.toNat + b.toNat + cin.toNat

The outgoing carry bit is true exactly when exact add-with-carry overflows.

theorem UInt64.addCarry_snd_eq_false (a b : UInt64) (cin : Bool) : (a.addCarry b cin).snd = false ↔ a.toNat + b.toNat + cin.toNat < word

The outgoing carry bit is false exactly when exact add-with-carry fits in one word.

theorem UInt64.addCarry_eq_of_no_overflow (a b : UInt64) (cin : Bool) (h : a.toNat + b.toNat + cin.toNat < word) : a.addCarry b cin = (ofNat (a.toNat + b.toNat + cin.toNat), false)

If exact add-with-carry does not overflow, addCarry returns the exact low word.

theorem UInt64.addCarry_fst_eq_of_no_overflow (a b : UInt64) (cin : Bool) (h : a.toNat + b.toNat + cin.toNat < word) : (a.addCarry b cin).fst = ofNat (a.toNat + b.toNat + cin.toNat)

If exact add-with-carry does not overflow, the low word is the exact sum.

theorem UInt64.addCarry_eq_of_overflow (a b : UInt64) (cin : Bool) (h : word ≤ a.toNat + b.toNat + cin.toNat) : a.addCarry b cin = (ofNat (a.toNat + b.toNat + cin.toNat), true)

If exact add-with-carry overflows, addCarry returns the wrapped low word and carry bit.

theorem UInt64.addCarry_fst_eq_of_overflow (a b : UInt64) (cin : Bool) (h : word ≤ a.toNat + b.toNat + cin.toNat) : (a.addCarry b cin).fst = ofNat (a.toNat + b.toNat + cin.toNat)

If exact add-with-carry overflows, the low word is the wrapped exact sum.

@[simp]

theorem UInt64.toNat_subBorrow_fst (a b : UInt64) (bin : Bool) : (a.subBorrow b bin).fst.toNat = (word + a.toNat - (b.toNat + bin.toNat)) % word

Low-word projection of UInt64.subBorrow after one-word wrapping.

theorem UInt64.subBorrow_snd (a b : UInt64) (bin : Bool) : (a.subBorrow b bin).snd = decide (a.toNat < b.toNat + bin.toNat)

The outgoing borrow bit of UInt64.subBorrow is set exactly when the subtrahend is larger.

theorem UInt64.subBorrow_snd_eq_true (a b : UInt64) (bin : Bool) : (a.subBorrow b bin).snd = true ↔ a.toNat < b.toNat + bin.toNat

The outgoing borrow bit is true exactly when the subtrahend is larger.

theorem UInt64.subBorrow_snd_eq_false (a b : UInt64) (bin : Bool) : (a.subBorrow b bin).snd = false ↔ b.toNat + bin.toNat ≤ a.toNat

The outgoing borrow bit is false exactly when subtraction does not borrow.

theorem UInt64.subBorrow_eq_of_no_borrow (a b : UInt64) (bin : Bool) (h : b.toNat + bin.toNat ≤ a.toNat) : a.subBorrow b bin = (ofNat (a.toNat - (b.toNat + bin.toNat)), false)

If subtraction does not borrow, subBorrow returns the exact difference.

theorem UInt64.subBorrow_fst_eq_of_no_borrow (a b : UInt64) (bin : Bool) (h : b.toNat + bin.toNat ≤ a.toNat) : (a.subBorrow b bin).fst = ofNat (a.toNat - (b.toNat + bin.toNat))

If subtraction does not borrow, the low word is the exact difference.

theorem UInt64.subBorrow_eq_of_borrow (a b : UInt64) (bin : Bool) (h : a.toNat < b.toNat + bin.toNat) : a.subBorrow b bin = (ofNat (word + a.toNat - (b.toNat + bin.toNat)), true)

If subtraction borrows, subBorrow returns the one-word wrapped difference.

theorem UInt64.subBorrow_fst_eq_of_borrow (a b : UInt64) (bin : Bool) (h : a.toNat < b.toNat + bin.toNat) : (a.subBorrow b bin).fst = ofNat (word + a.toNat - (b.toNat + bin.toNat))

If subtraction borrows, the low word is the wrapped difference.

theorem UInt64.toNat_mulHi (a b : UInt64) : (a.mulHi b).toNat = a.toNat * b.toNat / word

mulHi agrees with Nat-level division by 2^64.

theorem UInt64.toNat_mulFull (a b : UInt64) : match a.mulFull b with | (hi, lo) => hi.toNat = a.toNat * b.toNat / word ∧ lo.toNat = a.toNat * b.toNat % word

mulFull agrees with Nat-level division and remainder by 2^64.

theorem UInt64.mulFull_eq_mulHi_mul (a b : UInt64) : a.mulFull b = (a.mulHi b, a * b)

mulFull returns the same high word as mulHi and the same low word as ordinary wrapped UInt64 multiplication, while computing both halves in one extern call.

@[simp]

theorem UInt64.mulFull_fst_eq_mulHi (a b : UInt64) : (a.mulFull b).fst = a.mulHi b

The high component of mulFull is the same value returned by mulHi.

@[simp]

theorem UInt64.mulFull_snd_eq_mul (a b : UInt64) : (a.mulFull b).snd = a * b

The low component of mulFull is ordinary wrapped UInt64 multiplication.

@[simp]

theorem UInt64.toNat_mulFull_fst (a b : UInt64) : (a.mulFull b).fst.toNat = a.toNat * b.toNat / word

Nat-level view of the high component returned by mulFull.

@[simp]

theorem UInt64.toNat_mulFull_snd (a b : UInt64) : (a.mulFull b).snd.toNat = a.toNat * b.toNat % word

Nat-level view of the low component returned by mulFull.

theorem UInt64.mulHi_mulLo (a b : UInt64) : (a.mulHi b).toNat * word + (a * b).toNat = a.toNat * b.toNat

Splitting the product into high and low words reconstructs the original Nat-level product.

theorem UInt64.mulLo_add_mulHi (a b : UInt64) : (a * b).toNat + (a.mulHi b).toNat * word = a.toNat * b.toNat

Low-word-first product reconstruction for callers that encode a two-word value as lo + hi * word.

theorem UInt64.mulFull_snd_add_fst (a b : UInt64) : (a.mulFull b).snd.toNat + (a.mulFull b).fst.toNat * word = a.toNat * b.toNat

The components returned by mulFull reconstruct the original Nat-level product in low-word-first order.

theorem UInt64.toNat_addCarry (a b : UInt64) (cin : Bool) : match a.addCarry b cin with | (s, cout) => s.toNat + cout.toNat * word = a.toNat + b.toNat + cin.toNat

addCarry represents exact Nat addition split into a low word and a carry bit.

theorem UInt64.toNat_addCarry_proj (a b : UInt64) (cin : Bool) : (a.addCarry b cin).fst.toNat + (a.addCarry b cin).snd.toNat * word = a.toNat + b.toNat + cin.toNat

Projection-form reconstruction for addCarry, suitable for equation-style automation.

theorem UInt64.toNat_subBorrow (a b : UInt64) (bin : Bool) : match a.subBorrow b bin with | (d, bout) => d.toNat + (b.toNat + bin.toNat) = a.toNat + bout.toNat * word

subBorrow represents exact subtraction with borrow after one-word wrapping.

theorem UInt64.toNat_subBorrow_proj (a b : UInt64) (bin : Bool) : (a.subBorrow b bin).fst.toNat + (b.toNat + bin.toNat) = a.toNat + (a.subBorrow b bin).snd.toNat * word

Projection-form reconstruction for subBorrow, suitable for equation-style automation.