This module exists to provide the very basic BitVec definitions required for Init.Data.UInt.BasicAux.

@[match_pattern]

def BitVec.ofNat (n i : Nat) : BitVec n

The BitVec with value i mod 2^n.

Conventions for notations in identifiers:

• The recommended spelling of 0#n in identifiers is zero (not ofNat_zero).

• The recommended spelling of 1#n in identifiers is one (not ofNat_one).

Equations

• BitVec.ofNat n i = { toFin := Fin.ofNat' (2 ^ n) i }

instance BitVec.instOfNat {n i : Nat} : OfNat (BitVec n) i

Equations

• BitVec.instOfNat = { ofNat := BitVec.ofNat n i }

theorem BitVec.isLt {w : Nat} (x : BitVec w) : x.toNat < 2 ^ w

Return the bound in terms of toNat.

def BitVec.add {n : Nat} (x y : BitVec n) : BitVec n

Addition for bit vectors. This can be interpreted as either signed or unsigned addition modulo 2^n.

SMT-Lib name: bvadd.

Equations

• x.add y = BitVec.ofNat n (x.toNat + y.toNat)

instance BitVec.instAdd {n : Nat} : Add (BitVec n)

Equations

• BitVec.instAdd = { add := BitVec.add }

def BitVec.sub {n : Nat} (x y : BitVec n) : BitVec n

Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction modulo 2^n.

Equations

• x.sub y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)

instance BitVec.instSub {n : Nat} : Sub (BitVec n)

Equations

• BitVec.instSub = { sub := BitVec.sub }