# Documentation

## Init.Data.BitVec.Basic

We define bitvectors. We choose the Fin representation over others for its relative efficiency (Lean has special support for Nat), alignment with UIntXY types which are also represented with Fin, 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-LIBv2.

structure BitVec (w : Nat) :

A bitvector of the specified width.

This is represented as the underlying Nat number in both the runtime and the kernel, inheriting all the special support for Nat.

• ofFin :: (
• toFin : Fin (2 ^ w)

Interpret a bitvector as a number less than 2^w. O(1), because we use Fin as the internal representation of a bitvector.

• )
Instances For
@[reducible, inline, deprecated]
abbrev Std.BitVec (w : Nat) :
Equations
Instances For
def BitVec.decEq {n : Nat} (a : ) (b : ) :
Decidable (a = b)
Equations
• a.decEq b = match a, b with | { toFin := n_1 }, { toFin := m } => if h : n_1 = m then else
Instances For
instance instDecidableEqBitVec {n : Nat} :
Equations
• instDecidableEqBitVec = BitVec.decEq
@[match_pattern]
def BitVec.ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) :

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

Equations
• i#'p = { toFin := i, p }
Instances For
@[match_pattern]
def BitVec.ofNat (n : Nat) (i : Nat) :

The BitVec with value i mod 2^n.

Equations
• i#n = { toFin := }
Instances For
instance BitVec.instOfNat {n : Nat} {i : Nat} :
OfNat () i
Equations
• BitVec.instOfNat = { ofNat := i#n }
instance BitVec.natCastInst {w : Nat} :
Equations
• BitVec.natCastInst = { natCast := }
def BitVec.toNat {n : Nat} (a : ) :

Given a bitvector a, return the underlying Nat. This is O(1) because BitVec is a (zero-cost) wrapper around a Nat.

Equations
• a.toNat = a.toFin
Instances For
theorem BitVec.isLt {w : Nat} (x : ) :
x.toNat < 2 ^ w

Return the bound in terms of toNat.

@[deprecated BitVec.isLt]
theorem BitVec.toNat_lt {n : Nat} (x : ) :
x.toNat < 2 ^ n
@[simp]
theorem BitVec.ofNat_eq_ofNat {n : Nat} {i : Nat} :
= i#n

Theorem for normalizing the bit vector literal representation.

@[simp]
theorem BitVec.natCast_eq_ofNat (w : Nat) (x : Nat) :
x = x#w

All empty bitvectors are equal

Equations
@[reducible, inline]
abbrev BitVec.nil :

The empty bitvector

Equations
Instances For
theorem BitVec.eq_nil (x : ) :

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

def BitVec.zero (n : Nat) :

Return a bitvector 0 of size n. This is the bitvector with all zero bits.

Equations
• = 0#'
Instances For
Equations
• BitVec.instInhabited = { default := }
def BitVec.allOnes (n : Nat) :

Bit vector of size n where all bits are 1s

Equations
• = (2 ^ n - 1)#'
Instances For
@[inline]
def BitVec.getLsb {w : Nat} (x : ) (i : Nat) :

Return the i-th least significant bit or false if i ≥ w.

Equations
• x.getLsb i = x.toNat.testBit i
Instances For
@[inline]
def BitVec.getMsb {w : Nat} (x : ) (i : Nat) :

Return the i-th most significant bit or false if i ≥ w.

Equations
Instances For
@[inline]
def BitVec.msb {n : Nat} (a : ) :

Return most-significant bit in bitvector.

Equations
• a.msb = a.getMsb 0
Instances For
def BitVec.toInt {n : Nat} (a : ) :

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

Equations
• a.toInt = if 2 * a.toNat < 2 ^ n then a.toNat else a.toNat - (2 ^ n)
Instances For
def BitVec.ofInt (n : Nat) (i : Int) :

The BitVec with value (2^n + (i mod 2^n)) mod 2^n.

Equations
Instances For
instance BitVec.instIntCast {w : Nat} :
Equations
• BitVec.instIntCast = { intCast := }

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

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

Unexpander for bit vector literals.

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

Notation for bit vector 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.
Instances For

Unexpander for bit vector literals without truncation.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def BitVec.toHex {n : Nat} (x : ) :

Convert bitvector into a fixed-width hex number.

Equations
Instances For
instance BitVec.instRepr {n : Nat} :
Repr ()
Equations
instance BitVec.instToString {n : Nat} :
Equations
• BitVec.instToString = { toString := fun (a : ) => toString (repr a) }
def BitVec.add {n : Nat} (x : ) (y : ) :

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 = (x.toNat + y.toNat)#n
Instances For
instance BitVec.instAdd {n : Nat} :
Equations
def BitVec.sub {n : Nat} (x : ) (y : ) :

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

Equations
• x.sub y = (x.toNat + (2 ^ n - y.toNat))#n
Instances For
instance BitVec.instSub {n : Nat} :
Sub ()
Equations
• BitVec.instSub = { sub := BitVec.sub }
def BitVec.neg {n : Nat} (x : ) :

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

SMT-Lib name: bvneg.

Equations
• x.neg = (2 ^ n - x.toNat)#n
Instances For
instance BitVec.instNeg {n : Nat} :
Neg ()
Equations
• BitVec.instNeg = { neg := BitVec.neg }
def BitVec.abs {n : Nat} (s : ) :

Return the absolute value of a signed bitvector.

Equations
• s.abs = if s.msb = true then s.neg else s
Instances For
def BitVec.mul {n : Nat} (x : ) (y : ) :

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

SMT-Lib name: bvmul.

Equations
• x.mul y = (x.toNat * y.toNat)#n
Instances For
instance BitVec.instMul {n : Nat} :
Mul ()
Equations
• BitVec.instMul = { mul := BitVec.mul }
def BitVec.udiv {n : Nat} (x : ) (y : ) :

Unsigned division for bit vectors using the Lean convention where division by zero returns zero.

Equations
• x.udiv y = (x.toNat / y.toNat)#'
Instances For
instance BitVec.instDiv {n : Nat} :
Div ()
Equations
• BitVec.instDiv = { div := BitVec.udiv }
def BitVec.umod {n : Nat} (x : ) (y : ) :

Unsigned modulo for bit vectors.

SMT-Lib name: bvurem.

Equations
• x.umod y = (x.toNat % y.toNat)#'
Instances For
instance BitVec.instMod {n : Nat} :
Mod ()
Equations
• BitVec.instMod = { mod := BitVec.umod }
def BitVec.smtUDiv {n : Nat} (x : ) (y : ) :

Unsigned division for bit vectors using the SMT-Lib convention where division by zero returns the allOnes bitvector.

SMT-Lib name: bvudiv.

Equations
• x.smtUDiv y = if y = 0 then else x.udiv y
Instances For
def BitVec.sdiv {n : Nat} (s : ) (t : ) :

Signed t-division for bit vectors using the Lean convention where division by zero returns zero.

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

Equations
Instances For
def BitVec.smtSDiv {n : Nat} (s : ) (t : ) :

Signed division for bit vectors using SMTLIB rules for division by zero.

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

SMT-Lib name: bvsdiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def BitVec.srem {n : Nat} (s : ) (t : ) :

Remainder for signed division rounding to zero.

SMT_Lib name: bvsrem.

Equations
Instances For
def BitVec.smod {m : Nat} (s : ) (t : ) :

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.
Instances For
def BitVec.ofBool (b : Bool) :

Turn a Bool into a bitvector of length 1

Equations
• = bif b then 1 else 0
Instances For
@[simp]
@[simp]
def BitVec.fill (w : Nat) (b : Bool) :

Fills a bitvector with w copies of the bit b.

Equations
• = bif b then -1 else 0
Instances For
def BitVec.ult {n : Nat} (x : ) (y : ) :

Unsigned less-than for bit vectors.

SMT-Lib name: bvult.

Equations
Instances For
instance BitVec.instLT {n : Nat} :
LT ()
Equations
• BitVec.instLT = { lt := fun (x x_1 : ) => x.toNat < x_1.toNat }
instance BitVec.instDecidableLt {n : Nat} (x : ) (y : ) :
Decidable (x < y)
Equations
def BitVec.ule {n : Nat} (x : ) (y : ) :

Unsigned less-than-or-equal-to for bit vectors.

SMT-Lib name: bvule.

Equations
Instances For
instance BitVec.instLE {n : Nat} :
LE ()
Equations
• BitVec.instLE = { le := fun (x x_1 : ) => x.toNat x_1.toNat }
instance BitVec.instDecidableLe {n : Nat} (x : ) (y : ) :
Equations
def BitVec.slt {n : Nat} (x : ) (y : ) :

Signed less-than for bit vectors.

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


SMT-Lib name: bvslt.

Equations
Instances For
def BitVec.sle {n : Nat} (x : ) (y : ) :

Signed less-than-or-equal-to for bit vectors.

SMT-Lib name: bvsle.

Equations
Instances For
@[inline]
def BitVec.cast {n : Nat} {m : Nat} (eq : n = m) (i : ) :

cast eq i embeds i into an equal BitVec type.

Equations
Instances For
@[simp]
theorem BitVec.cast_ofNat {n : Nat} {m : Nat} (h : n = m) (x : Nat) :
BitVec.cast h x#n = x#m
@[simp]
theorem BitVec.cast_cast {n : Nat} {m : Nat} {k : Nat} (h₁ : n = m) (h₂ : m = k) (x : ) :
BitVec.cast h₂ (BitVec.cast h₁ x) =
@[simp]
theorem BitVec.cast_eq {n : Nat} (h : n = n) (x : ) :
= x
def BitVec.extractLsb' {n : Nat} (start : Nat) (len : Nat) (a : ) :
BitVec len

Extraction of bits start to start + len - 1 from a bit vector of size n to yield a new bitvector of size len. If start + len > n, then the vector will be zero-padded in the high bits.

Equations
Instances For
def BitVec.extractLsb {n : Nat} (hi : Nat) (lo : Nat) (a : ) :
BitVec (hi - lo + 1)

Extraction of bits hi (inclusive) down to lo (inclusive) from a bit vector of size n to yield a new bitvector of size hi - lo + 1.

SMT-Lib name: extract.

Equations
Instances For
def BitVec.zeroExtend' {n : Nat} {w : Nat} (le : n w) (x : ) :

A version of zeroExtend that requires a proof, but is a noop.

Equations
• = x.toNat#'
Instances For
def BitVec.shiftLeftZeroExtend {w : Nat} (msbs : ) (m : Nat) :
BitVec (w + m)

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

Equations
• msbs.shiftLeftZeroExtend m = let shiftLeftLt := ; (msbs.toNat <<< m)#'
Instances For
def BitVec.zeroExtend {w : Nat} (v : Nat) (x : ) :

Zero extend vector x of length w by adding zeros in the high bits until it has length v. If v < w then it truncates the high bits instead.

SMT-Lib name: zero_extend.

Equations
• = if h : w v then else x.toNat#v
Instances For
@[reducible, inline]
abbrev BitVec.truncate {w : Nat} (v : Nat) (x : ) :

Truncate the high bits of bitvector x of length w, resulting in a vector of length v. If v > w then it zero-extends the vector instead.

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

Sign extend a vector of length w, extending with i additional copies of the most significant bit in x. If x is an empty vector, then the sign is treated as zero.

SMT-Lib name: sign_extend.

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

Bitwise AND for bit vectors.

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


SMT-Lib name: bvand.

Equations
• x.and y = (x.toNat &&& y.toNat)#'
Instances For
instance BitVec.instAndOp {w : Nat} :
Equations
• BitVec.instAndOp = { and := BitVec.and }
def BitVec.or {n : Nat} (x : ) (y : ) :

Bitwise OR for bit vectors.

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


SMT-Lib name: bvor.

Equations
• x.or y = (x.toNat ||| y.toNat)#'
Instances For
instance BitVec.instOrOp {w : Nat} :
OrOp ()
Equations
• BitVec.instOrOp = { or := BitVec.or }
def BitVec.xor {n : Nat} (x : ) (y : ) :

Bitwise XOR for bit vectors.

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


SMT-Lib name: bvxor.

Equations
• x.xor y = (x.toNat ^^^ y.toNat)#'
Instances For
instance BitVec.instXor {w : Nat} :
Xor ()
Equations
• BitVec.instXor = { xor := BitVec.xor }
def BitVec.not {n : Nat} (x : ) :

Bitwise NOT for bit vectors.

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


SMT-Lib name: bvnot.

Equations
• x.not =
Instances For
Equations
• BitVec.instComplement = { complement := BitVec.not }
def BitVec.shiftLeft {n : Nat} (a : ) (s : Nat) :

Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is equivalent to a * 2^s, modulo 2^n.

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

Equations
• a.shiftLeft s = (a.toNat <<< s)#n
Instances For
Equations
• BitVec.instHShiftLeftNat = { hShiftLeft := BitVec.shiftLeft }
def BitVec.ushiftRight {n : Nat} (a : ) (s : Nat) :

(Logical) right shift for bit vectors. The high bits are filled with zeros. As a numeric operation, this is equivalent to a / 2^s, rounding down.

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

Equations
• a.ushiftRight s = (a.toNat >>> s)#'
Instances For
Equations
• BitVec.instHShiftRightNat = { hShiftRight := BitVec.ushiftRight }
def BitVec.sshiftRight {n : Nat} (a : ) (s : Nat) :

Arithmetic right shift for bit vectors. The high bits are filled with the most-significant bit. As a numeric operation, this is equivalent to a.toInt >>> s.

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

Equations
Instances For
instance BitVec.instHShiftLeft {m : Nat} {n : Nat} :
HShiftLeft () () ()
Equations
• BitVec.instHShiftLeft = { hShiftLeft := fun (x : ) (y : ) => x <<< y.toNat }
instance BitVec.instHShiftRight {m : Nat} {n : Nat} :
HShiftRight () () ()
Equations
• BitVec.instHShiftRight = { hShiftRight := fun (x : ) (y : ) => x >>> y.toNat }
def BitVec.rotateLeft {w : Nat} (x : ) (n : Nat) :

Rotate left for bit vectors. All the bits of x are shifted to higher positions, with the top n bits wrapping around to fill the low bits.

rotateLeft  0b0011#4 3 = 0b1001


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

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

Rotate right for bit vectors. All the bits of x are shifted to lower positions, with the bottom n bits wrapping around to fill the high bits.

rotateRight 0b01001#5 1 = 0b10100


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

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

Concatenation of bitvectors. This uses the "big endian" convention that the more significant input is on the left, so 0xAB#8 ++ 0xCD#8 = 0xABCD#16.

SMT-Lib name: concat.

Equations
Instances For
instance BitVec.instHAppendHAddNat {w : Nat} {v : Nat} :
HAppend () () (BitVec (w + v))
Equations
• BitVec.instHAppendHAddNat = { hAppend := BitVec.append }
def BitVec.replicate {w : Nat} (i : Nat) :
BitVec (w * i)

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

Equations
Instances For

### 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 : ) (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 ++
Instances For
def BitVec.cons {n : Nat} (msb : Bool) (lsbs : ) :
BitVec (n + 1)

Prepend a single bit to the front of a bitvector, using big endian order (see append). That is, the new bit is the most significant bit.

Equations
Instances For
theorem BitVec.append_ofBool {w : Nat} (msbs : ) (lsb : Bool) :
msbs ++ = msbs.concat lsb
theorem BitVec.ofBool_append {w : Nat} (msb : Bool) (lsbs : ) :
++ lsbs = BitVec.cast (BitVec.cons msb lsbs)

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

@[simp]
theorem BitVec.append_eq {w : Nat} {v : Nat} (x : ) (y : ) :
x.append y = x ++ y
@[simp]
theorem BitVec.shiftLeft_eq {w : Nat} (x : ) (n : Nat) :
x.shiftLeft n = x <<< n
@[simp]
theorem BitVec.ushiftRight_eq {w : Nat} (x : ) (n : Nat) :
x.ushiftRight n = x >>> n
@[simp]
theorem BitVec.not_eq {w : Nat} (x : ) :
x.not = ~~~x
@[simp]
theorem BitVec.and_eq {w : Nat} (x : ) (y : ) :
x.and y = x &&& y
@[simp]
theorem BitVec.or_eq {w : Nat} (x : ) (y : ) :
x.or y = x ||| y
@[simp]
theorem BitVec.xor_eq {w : Nat} (x : ) (y : ) :
x.xor y = x ^^^ y
@[simp]
theorem BitVec.neg_eq {w : Nat} (x : ) :
x.neg = -x
@[simp]
theorem BitVec.add_eq {w : Nat} (x : ) (y : ) :
x.add y = x + y
@[simp]
theorem BitVec.sub_eq {w : Nat} (x : ) (y : ) :
x.sub y = x - y
@[simp]
theorem BitVec.mul_eq {w : Nat} (x : ) (y : ) :
x.mul y = x * y
@[simp]
theorem BitVec.zero_eq {n : Nat} :
= 0#n
def BitVec.ofBoolListBE (bs : ) :
BitVec bs.length

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

Equations
Instances For
def BitVec.ofBoolListLE (bs : ) :
BitVec bs.length

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

Equations
Instances For