64-bit Word Arithmetic

This file defines 64-bit words and their arithmetic operations, corresponding to the word operations in HOL Light.

Main Definitions

• Word64 - 64-bit words (alias for BitVec 64)
• val - Convert word to natural number
• word - Convert natural number to word (with modulo)
• Arithmetic operations with carry/borrow

References

Source: HOL Light's Library/words.ml Related: s2n-bignum/common/bignum.ml (VAL_WORD_BIGDIGIT, etc.)

@[reducible, inline]

abbrev Bignum.Word64 : Type

A 64-bit word, represented as a bitvector.

Equations

• Bignum.Word64 = BitVec 64

def Bignum.Word64.val (w : Word64) : Nat

Convert a Word64 to a natural number.

Corresponds to HOL Light's val : (N)word -> num

Equations

• w.val = BitVec.toNat w

def Bignum.Word64.ofNat (n : Nat) : Word64

Convert a natural number to a Word64 (with implicit modulo 2^64).

Corresponds to HOL Light's word : num -> (N)word

Equations

• Bignum.Word64.ofNat n = BitVec.ofNat 64 n

def Bignum.Word64.addWithCarry (x y : Word64) : Word64 × Nat

Word addition with carry out.

Returns (sum, carry) where:

• sum = (x + y) % 2^64
• carry = 1 if x + y >= 2^64, else 0

This models the ARM ADDS instruction behavior.

Equations

• x.addWithCarry y = (Bignum.Word64.ofNat (x.val + y.val), if x.val + y.val ≥ 2 ^ 64 then 1 else 0)

def Bignum.Word64.adcWithCarry (x y : Word64) (carry_in : Nat) : Word64 × Nat

Word addition with carry in and carry out.

Returns (sum, carry_out) where:

• sum = (x + y + carry_in) % 2^64
• carry_out = 1 if x + y + carry_in >= 2^64, else 0

This models the ARM ADCS instruction behavior.

Equations

• x.adcWithCarry y carry_in = (Bignum.Word64.ofNat (x.val + y.val + carry_in), if x.val + y.val + carry_in ≥ 2 ^ 64 then 1 else 0)

def Bignum.Word64.subWithBorrow (x y : Word64) : Word64 × Nat

Word subtraction with borrow out.

Returns (diff, borrow) where:

• diff = (x - y) % 2^64
• borrow = 1 if x < y, else 0

This models the ARM SUBS instruction behavior.

Equations

• x.subWithBorrow y = (Bignum.Word64.ofNat (x.val - y.val), if x.val < y.val then 1 else 0)

def Bignum.Word64.sbcWithBorrow (x y : Word64) (borrow_in : Nat) : Word64 × Nat

Word subtraction with borrow in and borrow out.

Returns (diff, borrow_out) where:

• diff = (x - y - borrow_in) % 2^64
• borrow_out = 1 if x < y + borrow_in, else 0

This models the ARM SBCS instruction behavior.

Equations

• x.sbcWithBorrow y borrow_in = (Bignum.Word64.ofNat (x.val - y.val - borrow_in), if x.val < y.val + borrow_in then 1 else 0)

theorem Bignum.val_ofNat_of_lt {n : Nat} (h : n < 2 ^ 64) : (Word64.ofNat n).val = n

The value of a word constructed from a natural number that's already bounded by 2^64 equals that natural number.

Corresponds to HOL Light's VAL_WORD_EQ and related theorems.

Source: Related to s2n-bignum/common/bignum.ml:29-31 (VAL_WORD_BIGDIGIT)

theorem Bignum.val_ofNat (n : Nat) : (Word64.ofNat n).val = n % 2 ^ 64

Converting to word and back gives modulo 2^64.

theorem Bignum.val_lt (w : Word64) : w.val < 2 ^ 64

Word values are always bounded by 2^64.