7.2. Wide-word `UInt64` operations🔗

These operations treat a UInt64 as a digit in radix R = 2^64. UInt64.word names that radix, and the two structural facts below (every word is below the radix, and ofNat reduces modulo it) connect machine words to Nat reasoning.

def

UInt64.word : Nat
UInt64.word : Nat

The radix for a single UInt64 word.

theorem

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

Every UInt64 value is strictly below the word radix.

The multiply primitives compute the full two-word product of two words: UInt64.mulHi is the high half and UInt64.mulFull returns both halves at once.

def

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

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

def

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

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

Add- and subtract-with-carry thread a carry (resp. borrow) bit so that multi-word sums and differences chain across words.

def

UInt64.addCarry (a b : UInt64) (cin : Bool) : UInt64 × Bool
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.

def

UInt64.subBorrow (a b : UInt64) (bin : Bool) : UInt64 × Bool
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.

Each primitive comes with the Nat-level laws downstream proofs use: the low word is the exact result reduced modulo R, and the carry or borrow bit records exactly whether the exact result overflowed the single-word range.

theorem

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

Low-word projection of addCarry as Nat reduction modulo 2^64.

theorem

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

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

theorem

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

Low-word projection of 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)
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 subBorrow is set exactly when the subtrahend is larger.

These four operations are @[extern]-backed for speed, so they run through a C implementation in compiled code. The laws above are stated about their Lean definitions.

7.2. Wide-word UInt64 operations🔗

7.2. Wide-word `UInt64` operations🔗