We define the basic algebraic structure of bitvectors. We choose the Fin representation over others for its relative efficiency (Lean has special support for Nat), and the fact that bitwise operations on Fin are already defined. Some other possible representations are List Bool, { l : List Bool // l.length = w }, Fin w → Bool.

We define many of the bitvector operations from the QF_BV logic. of SMT-LIB v2.

@[inline, deprecated BitVec.ofNatLT (since := "2025-02-13")]

def BitVec.ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n

The BitVec with value i, given a proof that i < 2^w.

Equations

• BitVec.ofNatLt i p = i#'p

instance BitVec.natCastInst {w : Nat} : NatCast (BitVec w)

Equations

• BitVec.natCastInst = { natCast := BitVec.ofNat w }

@[simp]

theorem BitVec.ofNat_eq_ofNat {n i : Nat} : OfNat.ofNat i = BitVec.ofNat n i

Theorem for normalizing the bitvector literal representation.

@[simp]

theorem BitVec.natCast_eq_ofNat (w x : Nat) : ↑x = BitVec.ofNat w x

instance BitVec.instSubsingletonOfNatNat : Subsingleton (BitVec 0)

All empty bitvectors are equal

@[reducible, inline]

abbrev BitVec.nil : BitVec 0

The empty bitvector.

Equations

• BitVec.nil = 0

theorem BitVec.eq_nil (x : BitVec 0) : x = nil

Every bitvector of length 0 is equal to nil, i.e., there is only one empty bitvector

def BitVec.zero (n : Nat) : BitVec n

Returns a bitvector of size n where all bits are 0.

Equations

• BitVec.zero n = 0#'⋯

instance BitVec.instInhabited {n : Nat} : Inhabited (BitVec n)

Equations

• BitVec.instInhabited = { default := BitVec.zero n }

def BitVec.allOnes (n : Nat) : BitVec n

Returns a bitvector of size n where all bits are 1.

Equations

• BitVec.allOnes n = (2 ^ n - 1)#'⋯

@[inline]

def BitVec.getLsb' {w : Nat} (x : BitVec w) (i : Fin w) : Bool

Returns the ith least significant bit.

This will be renamed getLsb after the existing deprecated alias is removed.

Equations

• x.getLsb' i = x.toNat.testBit ↑i

@[inline]

def BitVec.getLsb? {w : Nat} (x : BitVec w) (i : Nat) : Option Bool

Returns the ith least significant bit, or none if i ≥ w.

Equations

• x.getLsb? i = if h : i < w then some (x.getLsb' ⟨i, h⟩) else none

@[inline]

def BitVec.getMsb' {w : Nat} (x : BitVec w) (i : Fin w) : Bool

Returns the ith most significant bit.

This will be renamed BitVec.getMsb after the existing deprecated alias is removed.

Equations

• x.getMsb' i = x.getLsb' ⟨w - 1 - ↑i, ⋯⟩

@[inline]

def BitVec.getMsb? {w : Nat} (x : BitVec w) (i : Nat) : Option Bool

Returns the ith most significant bit or none if i ≥ w.

Equations

• x.getMsb? i = if h : i < w then some (x.getMsb' ⟨i, h⟩) else none

@[inline]

def BitVec.getLsbD {w : Nat} (x : BitVec w) (i : Nat) : Bool

Returns the ith least significant bit or false if i ≥ w.

Equations

• x.getLsbD i = x.toNat.testBit i

@[inline]

def BitVec.getMsbD {w : Nat} (x : BitVec w) (i : Nat) : Bool

Returns the ith most significant bit, or false if i ≥ w.

Equations

• x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i))

@[inline]

def BitVec.msb {n : Nat} (x : BitVec n) : Bool

Returns the most significant bit in a bitvector.

Equations

• x.msb = x.getMsbD 0

instance BitVec.instGetElemNatBoolLt {w : Nat} : GetElem (BitVec w) Nat Bool fun (x : BitVec w) (i : Nat) => i < w

Equations

• BitVec.instGetElemNatBoolLt = { getElem := fun (xs : BitVec w) (i : Nat) (h : i < w) => xs.getLsb' ⟨i, h⟩ }

@[simp]

theorem BitVec.getLsb'_eq_getElem {w : Nat} (x : BitVec w) (i : Fin w) : x.getLsb' i = x[i]

We prefer x[i] as the simp normal form for getLsb'

@[simp]

theorem BitVec.getLsb?_eq_getElem? {w : Nat} (x : BitVec w) (i : Nat) : x.getLsb? i = x[i]?

We prefer x[i]? as the simp normal form for getLsb?

theorem BitVec.getElem_eq_testBit_toNat {w : Nat} (x : BitVec w) (i : Nat) (h : i < w) : x[i] = x.toNat.testBit i

@[simp]

theorem BitVec.getLsbD_eq_getElem {w : Nat} {x : BitVec w} {i : Nat} (h : i < w) : x.getLsbD i = x[i]

def BitVec.toInt {n : Nat} (x : BitVec n) : Int

Interprets the bitvector as an integer stored in two's complement form.

Equations

• x.toInt = if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)

def BitVec.ofInt (n : Nat) (i : Int) : BitVec n

Converts an integer to its two's complement representation as a bitvector of the given width n, over- and underflowing as needed.

The underlying Nat is (2^n + (i mod 2^n)) mod 2^n. Converting the bitvector back to an Int with BitVec.toInt results in the value i.bmod (2^n).

Equations

• BitVec.ofInt n i = (i % Int.ofNat (2 ^ n)).toNat#'⋯

instance BitVec.instIntCast {w : Nat} : IntCast (BitVec w)

Equations

• BitVec.instIntCast = { intCast := BitVec.ofInt w }

def BitVec.«term__#__» : Lean.ParserDescr

Notation for bitvector literals. i#n is a shorthand for BitVec.ofNat n i.

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

• One or more equations did not get rendered due to their size.

def BitVec.unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander

Unexpander for bitvector literals.

Equations

• One or more equations did not get rendered due to their size.

def BitVec.«term__#'__» : Lean.TrailingParserDescr

Notation for bitvector literals without truncation. i#'lt is a shorthand for BitVec.ofNatLT i lt.

Equations

• One or more equations did not get rendered due to their size.

def BitVec.unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander

Unexpander for bitvector literals without truncation.

Equations

• One or more equations did not get rendered due to their size.

def BitVec.toHex {n : Nat} (x : BitVec n) : String

Converts a bitvector into a fixed-width hexadecimal number with enough digits to represent it.

If n is 0, then one digit is returned. Otherwise, ⌊(n + 3) / 4⌋ digits are returned.

Equations

• x.toHex = (List.replicate ((n + 3) / 4 - (Nat.toDigits 16 x.toNat).asString.length) '0').asString ++ (Nat.toDigits 16 x.toNat).asString

def BitVec.BitVec.repr {n : Nat} (a : BitVec n) : Std.Format

BitVec representation.

Equations

• BitVec.BitVec.repr a = Std.Format.text "0x" ++ Std.Format.text a.toHex ++ Std.Format.text "#" ++ repr n

instance BitVec.instRepr {n : Nat} : Repr (BitVec n)

Equations

• BitVec.instRepr = { reprPrec := fun (a : BitVec n) (x : Nat) => BitVec.BitVec.repr a }

instance BitVec.instToString {n : Nat} : ToString (BitVec n)

Equations

• BitVec.instToString = { toString := fun (a : BitVec n) => toString (repr a) }

def BitVec.neg {n : Nat} (x : BitVec n) : BitVec n

Negation of bitvectors. This can be interpreted as either signed or unsigned negation modulo 2^n. Usually accessed via the - prefix operator.

SMT-LIB name: bvneg.

Equations

• x.neg = BitVec.ofNat n (2 ^ n - x.toNat)

instance BitVec.instNeg {n : Nat} : Neg (BitVec n)

Equations

• BitVec.instNeg = { neg := BitVec.neg }

def BitVec.abs {n : Nat} (x : BitVec n) : BitVec n

Returns the absolute value of a signed bitvector.

Equations

• x.abs = if x.msb = true then x.neg else x

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

Multiplies two bitvectors. This can be interpreted as either signed or unsigned multiplication modulo 2^n. Usually accessed via the * operator.

SMT-LIB name: bvmul.

Equations

• x.mul y = BitVec.ofNat n (x.toNat * y.toNat)

instance BitVec.instMul {n : Nat} : Mul (BitVec n)

Equations

• BitVec.instMul = { mul := BitVec.mul }

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

Raises a bitvector to a natural number power. Usually accessed via the ^ operator.

Note that this is currently an inefficient implementation, and should be replaced via an @[extern] with a native implementation. See https://github.com/leanprover/lean4/issues/7887.

Equations

• x.pow 0 = 1
• x.pow y_2.succ = x.pow y_2 * x

instance BitVec.instPowNat {n : Nat} : Pow (BitVec n) Nat

Equations

• BitVec.instPowNat = { pow := fun (x : BitVec n) (y : Nat) => x.pow y }

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

Unsigned division of bitvectors using the Lean convention where division by zero returns zero. Usually accessed via the / operator.

Equations

• x.udiv y = (x.toNat / y.toNat)#'⋯

instance BitVec.instDiv {n : Nat} : Div (BitVec n)

Equations

• BitVec.instDiv = { div := BitVec.udiv }

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

Unsigned modulo for bitvectors. Usually accessed via the % operator.

SMT-LIB name: bvurem.

Equations

• x.umod y = (x.toNat % y.toNat)#'⋯

instance BitVec.instMod {n : Nat} : Mod (BitVec n)

Equations

• BitVec.instMod = { mod := BitVec.umod }

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

Unsigned division of bitvectors using the SMT-LIB convention, where division by zero returns BitVector.allOnes n.

SMT-LIB name: bvudiv.

Equations

• x.smtUDiv y = if y = 0 then BitVec.allOnes n else x.udiv y

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

Signed T-division (using the truncating rounding convention) for bitvectors. This function obeys the Lean convention that division by zero returns zero.

Examples:

• (7#4).sdiv 2 = 3#4
• (-9#4).sdiv 2 = -4#4
• (5#4).sdiv -2 = -2#4
• (-7#4).sdiv (-2) = 3#4

Equations

• x.sdiv y = match x.msb, y.msb with | false, false => x.udiv y | false, true => (x.udiv y.neg).neg | true, false => (x.neg.udiv y).neg | true, true => x.neg.udiv y.neg

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

Signed division for bitvectors using the SMT-LIB using the SMT-LIB convention, where division by zero returns BitVector.allOnes n.

Specifically, x.smtSDiv 0 = if x >= 0 then -1 else 1

SMT-LIB name: bvsdiv.

Equations

• x.smtSDiv y = match x.msb, y.msb with | false, false => x.smtUDiv y | false, true => (x.smtUDiv y.neg).neg | true, false => (x.neg.smtUDiv y).neg | true, true => x.neg.smtUDiv y.neg

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

Remainder for signed division rounding to zero.

SMT-LIB name: bvsrem.

Equations

• x.srem y = match x.msb, y.msb with | false, false => x.umod y | false, true => x.umod y.neg | true, false => (x.neg.umod y).neg | true, true => (x.neg.umod y.neg).neg

def BitVec.smod {m : Nat} (x y : BitVec m) : BitVec m

Remainder for signed division rounded to negative infinity.

SMT-LIB name: bvsmod.

Equations

• One or more equations did not get rendered due to their size.

def BitVec.ofBool (b : Bool) : BitVec 1

Turns a Bool into a bitvector of length 1.

Equations

• BitVec.ofBool b = bif b then 1 else 0

@[simp]

theorem BitVec.ofBool_false : ofBool false = 0

@[simp]

theorem BitVec.ofBool_true : ofBool true = 1

def BitVec.fill (w : Nat) (b : Bool) : BitVec w

Fills a bitvector with w copies of the bit b.

Equations

• BitVec.fill w b = bif b then -1 else 0

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

Unsigned less-than for bitvectors.

SMT-LIB name: bvult.

Equations

• x.ult y = decide (x.toNat < y.toNat)

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

Unsigned less-than-or-equal-to for bitvectors.

SMT-LIB name: bvule.

Equations

• x.ule y = decide (x.toNat ≤ y.toNat)

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

Signed less-than for bitvectors.

SMT-LIB name: bvslt.

Examples:

• BitVec.slt 6#4 7 = true
• BitVec.slt 7#4 8 = false

Equations

• x.slt y = decide (x.toInt < y.toInt)

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

Signed less-than-or-equal-to for bitvectors.

SMT-LIB name: bvsle.

Equations

• x.sle y = decide (x.toInt ≤ y.toInt)

@[inline]

def BitVec.cast {n m : Nat} (eq : n = m) (x : BitVec n) : BitVec m

If two natural numbers n and m are equal, then a bitvector of width n is also a bitvector of width m.

Using x.cast eq should be preferred over eq ▸ x because there are special-purpose simp lemmas that can more consistently simplify BitVec.cast away.

Equations

• BitVec.cast eq x = x.toNat#'⋯

@[simp]

theorem BitVec.cast_ofNat {n m : Nat} (h : n = m) (x : Nat) : BitVec.cast h (BitVec.ofNat n x) = BitVec.ofNat m x

@[simp]

theorem BitVec.cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) : BitVec.cast h₂ (BitVec.cast h₁ x) = BitVec.cast ⋯ x

@[simp]

theorem BitVec.cast_eq {n : Nat} (h : n = n) (x : BitVec n) : BitVec.cast h x = x

def BitVec.extractLsb' {n : Nat} (start len : Nat) (x : BitVec n) : BitVec len

Extracts the bits start to start + len - 1 from a bitvector of size n to yield a new bitvector of size len. If start + len > n, then the bitvector is zero-extended.

Equations

• BitVec.extractLsb' start len x = BitVec.ofNat len (x.toNat >>> start)

def BitVec.extractLsb {n : Nat} (hi lo : Nat) (x : BitVec n) : BitVec (hi - lo + 1)

Extracts the bits from hi down to lo (both inclusive) from a bitvector, which is implicitly zero-extended if necessary.

The resulting bitvector has size hi - lo + 1.

SMT-LIB name: extract.

Equations

• BitVec.extractLsb hi lo x = BitVec.extractLsb' lo (hi - lo + 1) x

def BitVec.setWidth' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w

Increases the width of a bitvector to one that is at least as large by zero-extending it.

This is a constant-time operation because the underlying Nat is unmodified; because the new width is at least as large as the old one, no overflow is possible.

Equations

• BitVec.setWidth' le x = x.toNat#'⋯

def BitVec.shiftLeftZeroExtend {w : Nat} (msbs : BitVec w) (m : Nat) : BitVec (w + m)

Returns zeroExtend (w+n) x <<< n without needing to compute x % 2^(2+n).

Equations

• msbs.shiftLeftZeroExtend m = (msbs.toNat <<< m)#'⋯

def BitVec.setWidth {w : Nat} (v : Nat) (x : BitVec w) : BitVec v

Transforms a bitvector of length w into a bitvector of length v, padding with 0 as needed.

The specific behavior depends on the relationship between the starting width w and the final width v:

• If v > w, it is zero-extended; the high bits are padded with zeroes until the bitvector has v bits.
• If v = w, the bitvector is returned unchanged.
• If v < w, the high bits are truncated.

BitVec.setWidth, BitVec.zeroExtend, and BitVec.truncate are aliases for this operation.

SMT-LIB name: zero_extend.

Equations

• BitVec.setWidth v x = if h : w ≤ v then BitVec.setWidth' h x else BitVec.ofNat v x.toNat

@[reducible, inline]

abbrev BitVec.zeroExtend {w : Nat} (v : Nat) (x : BitVec w) : BitVec v

Transforms a bitvector of length w into a bitvector of length v, padding with 0 as needed.

The specific behavior depends on the relationship between the starting width w and the final width v:

• If v > w, it is zero-extended; the high bits are padded with zeroes until the bitvector has v bits.
• If v = w, the bitvector is returned unchanged.
• If v < w, the high bits are truncated.

BitVec.setWidth, BitVec.zeroExtend, and BitVec.truncate are aliases for this operation.

SMT-LIB name: zero_extend.

Equations

• @BitVec.zeroExtend = @BitVec.setWidth

@[reducible, inline]

abbrev BitVec.truncate {w : Nat} (v : Nat) (x : BitVec w) : BitVec v

Transforms a bitvector of length w into a bitvector of length v, padding with 0 as needed.

The specific behavior depends on the relationship between the starting width w and the final width v:

• If v > w, it is zero-extended; the high bits are padded with zeroes until the bitvector has v bits.
• If v = w, the bitvector is returned unchanged.
• If v < w, the high bits are truncated.

BitVec.setWidth, BitVec.zeroExtend, and BitVec.truncate are aliases for this operation.

SMT-LIB name: zero_extend.

Equations

• @BitVec.truncate = @BitVec.setWidth

def BitVec.signExtend {w : Nat} (v : Nat) (x : BitVec w) : BitVec v

Transforms a bitvector of length w into a bitvector of length v, padding as needed with the most significant bit's value.

If x is an empty bitvector, then the sign is treated as zero.

SMT-LIB name: sign_extend.

Equations

• BitVec.signExtend v x = BitVec.ofInt v x.toInt

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

Bitwise and for bitvectors. Usually accessed via the &&& operator.

SMT-LIB name: bvand.

Example:

• 0b1010#4 &&& 0b0110#4 = 0b0010#4

Equations

• x.and y = (x.toNat &&& y.toNat)#'⋯

instance BitVec.instAndOp {w : Nat} : AndOp (BitVec w)

Equations

• BitVec.instAndOp = { and := BitVec.and }

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

Bitwise or for bitvectors. Usually accessed via the ||| operator.

SMT-LIB name: bvor.

Example:

• 0b1010#4 ||| 0b0110#4 = 0b1110#4

Equations

• x.or y = (x.toNat ||| y.toNat)#'⋯

instance BitVec.instOrOp {w : Nat} : OrOp (BitVec w)

Equations

• BitVec.instOrOp = { or := BitVec.or }

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

Bitwise xor for bitvectors. Usually accessed via the ^^^ operator.

SMT-LIB name: bvxor.

Example:

• 0b1010#4 ^^^ 0b0110#4 = 0b1100#4

Equations

• x.xor y = (x.toNat ^^^ y.toNat)#'⋯

instance BitVec.instXor {w : Nat} : Xor (BitVec w)

Equations

• BitVec.instXor = { xor := BitVec.xor }

def BitVec.not {n : Nat} (x : BitVec n) : BitVec n

Bitwise complement for bitvectors. Usually accessed via the ~~~ prefix operator.

SMT-LIB name: bvnot.

Example:

• ~~~(0b0101#4) == 0b1010

Equations

• x.not = BitVec.allOnes n ^^^ x

instance BitVec.instComplement {w : Nat} : Complement (BitVec w)

Equations

• BitVec.instComplement = { complement := BitVec.not }

def BitVec.shiftLeft {n : Nat} (x : BitVec n) (s : Nat) : BitVec n

Shifts a bitvector to the left. The low bits are filled with zeros. As a numeric operation, this is equivalent to x * 2^s, modulo 2^n.

SMT-LIB name: bvshl except this operator uses a Nat shift value.

Equations

• x.shiftLeft s = BitVec.ofNat n (x.toNat <<< s)

instance BitVec.instHShiftLeftNat {w : Nat} : HShiftLeft (BitVec w) Nat (BitVec w)

Equations

• BitVec.instHShiftLeftNat = { hShiftLeft := BitVec.shiftLeft }

def BitVec.ushiftRight {n : Nat} (x : BitVec n) (s : Nat) : BitVec n

Shifts a bitvector to the right. This is a logical right shift - the high bits are filled with zeros.

As a numeric operation, this is equivalent to x / 2^s, rounding down.

SMT-LIB name: bvlshr except this operator uses a Nat shift value.

Equations

• x.ushiftRight s = (x.toNat >>> s)#'⋯

instance BitVec.instHShiftRightNat {w : Nat} : HShiftRight (BitVec w) Nat (BitVec w)

Equations

• BitVec.instHShiftRightNat = { hShiftRight := BitVec.ushiftRight }

def BitVec.sshiftRight {n : Nat} (x : BitVec n) (s : Nat) : BitVec n

Shifts a bitvector to the right. This is an arithmetic right shift - the high bits are filled with most significant bit's value.

As a numeric operation, this is equivalent to x.toInt >>> s.

SMT-LIB name: bvashr except this operator uses a Nat shift value.

Equations

• x.sshiftRight s = BitVec.ofInt n (x.toInt >>> s)

instance BitVec.instHShiftLeft {m n : Nat} : HShiftLeft (BitVec m) (BitVec n) (BitVec m)

Equations

• BitVec.instHShiftLeft = { hShiftLeft := fun (x : BitVec m) (y : BitVec n) => x <<< y.toNat }

instance BitVec.instHShiftRight {m n : Nat} : HShiftRight (BitVec m) (BitVec n) (BitVec m)

Equations

• BitVec.instHShiftRight = { hShiftRight := fun (x : BitVec m) (y : BitVec n) => x >>> y.toNat }

def BitVec.sshiftRight' {n m : Nat} (a : BitVec n) (s : BitVec m) : BitVec n

Shifts a bitvector to the right. This is an arithmetic right shift - the high bits are filled with most significant bit's value.

As a numeric operation, this is equivalent to a.toInt >>> s.toNat.

SMT-LIB name: bvashr.

Equations

• a.sshiftRight' s = a.sshiftRight s.toNat

def BitVec.rotateLeftAux {w : Nat} (x : BitVec w) (n : Nat) : BitVec w

Auxiliary function for rotateLeft, which does not take into account the case where the rotation amount is greater than the bitvector width.

Equations

• x.rotateLeftAux n = x <<< n ||| x >>> (w - n)

def BitVec.rotateLeft {w : Nat} (x : BitVec w) (n : Nat) : BitVec w

Rotates the bits in a bitvector to the left.

All the bits of x are shifted to higher positions, with the top n bits wrapping around to fill the vacated low bits.

SMT-LIB name: rotate_left, except this operator uses a Nat shift amount.

Example:

• (0b0011#4).rotateLeft 3 = 0b1001

Equations

• x.rotateLeft n = x.rotateLeftAux (n % w)

def BitVec.rotateRightAux {w : Nat} (x : BitVec w) (n : Nat) : BitVec w

Auxiliary function for rotateRight, which does not take into account the case where the rotation amount is greater than the bitvector width.

Equations

• x.rotateRightAux n = x >>> n ||| x <<< (w - n)

def BitVec.rotateRight {w : Nat} (x : BitVec w) (n : Nat) : BitVec w

Rotates the bits in a bitvector to the right.

All the bits of x are shifted to lower positions, with the bottom n bits wrapping around to fill the vacated high bits.

SMT-LIB name: rotate_right, except this operator uses a Nat shift amount.

Example:

• rotateRight 0b01001#5 1 = 0b10100

Equations

• x.rotateRight n = x.rotateRightAux (n % w)

def BitVec.append {n m : Nat} (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n + m)

Concatenates two bitvectors using the “big-endian” convention that the more significant input is on the left. Usually accessed via the ++ operator.

SMT-LIB name: concat.

Example:

• 0xAB#8 ++ 0xCD#8 = 0xABCD#16.

Equations

• msbs.append lsbs = msbs.shiftLeftZeroExtend m ||| BitVec.setWidth' ⋯ lsbs

instance BitVec.instHAppendHAddNat {w v : Nat} : HAppend (BitVec w) (BitVec v) (BitVec (w + v))

Equations

• BitVec.instHAppendHAddNat = { hAppend := BitVec.append }

def BitVec.replicate {w : Nat} (i : Nat) : BitVec w → BitVec (w * i)

Concatenates i copies of x into a new vector of length w * i.

Equations

• BitVec.replicate 0 x✝ = 0#0
• BitVec.replicate n.succ x✝ = BitVec.cast ⋯ (x✝ ++ BitVec.replicate n x✝)

Cons and Concat

We give special names to the operations of adding a single bit to either end of a bitvector. We follow the precedent of Vector.cons/Vector.concat both for the name, and for the decision to have the resulting size be n + 1 for both operations (rather than 1 + n, which would be the result of appending a single bit to the front in the naive implementation).

def BitVec.concat {n : Nat} (msbs : BitVec n) (lsb : Bool) : BitVec (n + 1)

Append a single bit to the end of a bitvector, using big endian order (see append). That is, the new bit is the least significant bit.

Equations

• msbs.concat lsb = msbs ++ BitVec.ofBool lsb

def BitVec.shiftConcat {n : Nat} (x : BitVec n) (b : Bool) : BitVec n

Shifts all bits of x to the left by 1 and sets the least significant bit to b.

This is a non-dependent version of BitVec.concat that does not change the total bitwidth.

Equations

• x.shiftConcat b = BitVec.truncate n (x.concat b)

def BitVec.cons {n : Nat} (msb : Bool) (lsbs : BitVec n) : BitVec (n + 1)

Prepends a single bit to the front of a bitvector, using big-endian order (see append).

The new bit is the most significant bit.

Equations

• BitVec.cons msb lsbs = BitVec.cast ⋯ (BitVec.ofBool msb ++ lsbs)

theorem BitVec.append_ofBool {w : Nat} (msbs : BitVec w) (lsb : Bool) : msbs ++ ofBool lsb = msbs.concat lsb

theorem BitVec.ofBool_append {w : Nat} (msb : Bool) (lsbs : BitVec w) : ofBool msb ++ lsbs = BitVec.cast ⋯ (cons msb lsbs)

def BitVec.twoPow (w i : Nat) : BitVec w

twoPow w i is the bitvector 2^i if i < w, and 0 otherwise. In other words, it is 2 to the power i.

From the bitwise point of view, it has the ith bit as 1 and all other bits as 0.

Equations

• BitVec.twoPow w i = 1#w <<< i

@[irreducible]

def BitVec.hash {n : Nat} (bv : BitVec n) : UInt64

Computes a hash of a bitvector, combining 64-bit words using mixHash.

Equations

• bv.hash = if n ≤ 64 then (↑bv.toFin).toUInt64 else mixHash (↑bv.toFin).toUInt64 (BitVec.setWidth (n - 64) (bv >>> 64)).hash

instance BitVec.instHashable {n : Nat} : Hashable (BitVec n)

Equations

• BitVec.instHashable = { hash := BitVec.hash }

We add simp-lemmas that rewrite bitvector operations into the equivalent notation

@[simp]

theorem BitVec.append_eq {w v : Nat} (x : BitVec w) (y : BitVec v) : x.append y = x ++ y

@[simp]

theorem BitVec.shiftLeft_eq {w : Nat} (x : BitVec w) (n : Nat) : x.shiftLeft n = x <<< n

@[simp]

theorem BitVec.ushiftRight_eq {w : Nat} (x : BitVec w) (n : Nat) : x.ushiftRight n = x >>> n

@[simp]

theorem BitVec.not_eq {w : Nat} (x : BitVec w) : x.not = ~~~x

@[simp]

theorem BitVec.and_eq {w : Nat} (x y : BitVec w) : x.and y = x &&& y

@[simp]

theorem BitVec.or_eq {w : Nat} (x y : BitVec w) : x.or y = x ||| y

@[simp]

theorem BitVec.xor_eq {w : Nat} (x y : BitVec w) : x.xor y = x ^^^ y

@[simp]

theorem BitVec.neg_eq {w : Nat} (x : BitVec w) : x.neg = -x

@[simp]

theorem BitVec.add_eq {w : Nat} (x y : BitVec w) : x.add y = x + y

@[simp]

theorem BitVec.sub_eq {w : Nat} (x y : BitVec w) : x.sub y = x - y

@[simp]

theorem BitVec.mul_eq {w : Nat} (x y : BitVec w) : x.mul y = x * y

@[simp]

theorem BitVec.udiv_eq {w : Nat} (x y : BitVec w) : x.udiv y = x / y

@[simp]

theorem BitVec.umod_eq {w : Nat} (x y : BitVec w) : x.umod y = x % y

@[simp]

theorem BitVec.zero_eq {n : Nat} : BitVec.zero n = 0#n

def BitVec.ofBoolListBE (bs : List Bool) : BitVec bs.length

Converts a list of Bools into a big-endian BitVec.

Equations

• BitVec.ofBoolListBE [] = 0#0
• BitVec.ofBoolListBE (b :: bs) = BitVec.cons b (BitVec.ofBoolListBE bs)

def BitVec.ofBoolListLE (bs : List Bool) : BitVec bs.length

Converts a list of Bools into a little-endian BitVec.

Equations

• BitVec.ofBoolListLE [] = 0#0
• BitVec.ofBoolListLE (b :: bs) = (BitVec.ofBoolListLE bs).concat b

Overflow

def BitVec.uaddOverflow {w : Nat} (x y : BitVec w) : Bool

Checks whether addition of x and y results in unsigned overflow.

SMT-LIB name: bvuaddo.

Equations

• x.uaddOverflow y = decide (x.toNat + y.toNat ≥ 2 ^ w)

def BitVec.saddOverflow {w : Nat} (x y : BitVec w) : Bool

Checks whether addition of x and y results in signed overflow, treating x and y as 2's complement signed bitvectors.

SMT-LIB name: bvsaddo.

Equations

• x.saddOverflow y = (decide (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || decide (x.toInt + y.toInt < -2 ^ (w - 1)))

def BitVec.usubOverflow {w : Nat} (x y : BitVec w) : Bool

Checks whether subtraction of x and y results in unsigned overflow.

SMT-Lib name: bvusubo.

Equations

• x.usubOverflow y = decide (x.toNat < y.toNat)

def BitVec.ssubOverflow {w : Nat} (x y : BitVec w) : Bool

Checks whether the subtraction of x and y results in signed overflow, treating x and y as 2's complement signed bitvectors.

SMT-Lib name: bvssubo.

Equations

• x.ssubOverflow y = (decide (x.toInt - y.toInt ≥ 2 ^ (w - 1)) || decide (x.toInt - y.toInt < -2 ^ (w - 1)))

def BitVec.negOverflow {w : Nat} (x : BitVec w) : Bool

Checks whether the negation of a bitvector results in overflow.

For a bitvector x with nonzero width, this only happens if x = intMin.

SMT-Lib name: bvnego.

Equations

• x.negOverflow = (x.toInt == -2 ^ (w - 1))

def BitVec.sdivOverflow {w : Nat} (x y : BitVec w) : Bool

Checks whether the signed division of x by y results in overflow. For BitVecs x and y with nonzero width, this only happens if x = intMin and y = allOnes w.

SMT-LIB name: bvsdivo.

Equations

• x.sdivOverflow y = (decide (2 ^ (w - 1) ≤ x.toInt / y.toInt) || decide (x.toInt / y.toInt < -2 ^ (w - 1)))

def BitVec.reverse {w : Nat} : BitVec w → BitVec w

Reverses the bits in a bitvector.

Equations

• x_2.reverse = x_2
• x_2.reverse = (BitVec.truncate w x_2).reverse.concat x_2.msb

def BitVec.umulOverflow {w : Nat} (x y : BitVec w) : Bool

umulOverflow x y returns true if multiplying x and y results in unsigned overflow.

SMT-Lib name: bvumulo.

Equations

• x.umulOverflow y = decide (x.toNat * y.toNat ≥ 2 ^ w)

def BitVec.smulOverflow {w : Nat} (x y : BitVec w) : Bool

smulOverflow x y returns true if multiplying x and y results in signed overflow, treating x and y as 2's complement signed bitvectors.

SMT-Lib name: bvsmulo.

Equations

• x.smulOverflow y = (decide (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || decide (x.toInt * y.toInt < -2 ^ (w - 1)))