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

@[instance_reducible]

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

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

Return the bound in terms of toNat.

def BitVec.ofNatClamp (w n : Nat) : BitVec w

Converts a natural number to a bitvector of width w, returning the largest representable value if the number is too large.

Returns 2^w - 1 for natural numbers greater than or equal to 2^w.

@[implicit_reducible]

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

Adds two bitvectors. This can be interpreted as either signed or unsigned addition modulo 2^n. Usually accessed via the + operator.

SMT-LIB name: bvadd.

@[instance_reducible]

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

@[implicit_reducible]

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

Subtracts one bitvector from another. This can be interpreted as either signed or unsigned subtraction modulo 2^n. Usually accessed via the - operator.

@[instance_reducible]

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