Bitvectors are fixed-width sequences of binary digits. They are frequently used in software verification, because they closely model efficient data structures and operations that are similar to hardware. A bitvector can be understood from two perspectives: as a sequence of bits, or as a number encoded by a sequence of bits. When a bitvector represents a number, it can do so as either a signed or an unsigned number. Signed numbers are represented in two's complement form.
Bitvectors are represented as a wrapper around a Fin with a suitable bound.
Because Fin itself is a wrapper around a Nat, bitvectors are able to use the kernel's special support for efficient computation with natural numbers.
BitVec (w : Nat) : Type
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.
BitVec.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.
Bitvectors are represented as a Fin with the corresponding range.
Because BitVec is a trivial wrapper around Fin and Fin is a trivial wrapper around Nat, bitvectors use the same runtime representation as Nat in compiled code.
There is an OfNat (BitVec w) n instance for all widths w and natural numbers n.
Natural number literals, including those that use hexadecimal or binary notation, may be used to represent bitvectors in contexts where the expected type is known.
When the expected type is not known, a dedicated syntax allows the width of the bitvector to be specified along with its value.
term ::= ...
| Notation for bit vector 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`).
This notation pairs a numeric literal with a term that denotes its width.
Spaces are forbidden around the #.
Literals that overflow the width of the bitvector are truncated.
Bitvectors may be represented by natural number literals, so (5 : BitVec 8) is a valid bitvector.
Additionally, a width may be specified directly in the literal:
5#8
Spaces are not allowed on either side of the #:
5 8<example>:1:2-1:3: expected end of input
5# <example>:1:3-1:4: expected no space before
A numeric literal is required to the left of the #:
(3 + 2)8<example>:1:7-1:8: expected end of input
However, a term is allowed to the right of the #:
5#(4 + 4)If the literal is too large to fit in the specified number of bits, then it is truncated:
#eval 7#2
3#2
term ::= ...
| Notation for bit vector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLT i lt`.
This notation is available only when the BitVec namespace has been opened.
Rather than an explicit width, it expects a proof that the literal value is representable by a bitvector of the corresponding width.
The bounded bitvector literal notation ensures that literals do not overflow the specified number of bits.
The notation is only available when the BitVec namespace has been opened.
open BitVec
Literals that are in bounds require a proof to that effect:
example : BitVec 8 := 1#'(⊢ 1 < 2 ^ 8 All goals completed! 🐙)
Literals that are not in bounds are not allowed:
example : BitVec 8 := 256#'(⊢ 256 < 2 ^ 8 ⊢ 256 < 2 ^ 8)
tactic 'decide' proved that the proposition 256 < 2 ^ 8 is false
In addition to the full suite of automation and tools provided by Lean for every type, the bv_decide tactic can solve many bitvector-related problems.
This tactic invokes an external automated theorem prover (cadical) and reconstructs the proof that it provides in Lean's own logic.
The resulting proofs rely only on the axiom Lean.ofReduceBool; the external prover is not part of the trusted code base.
The function popcount returns the number of set bits in a bitvector.
It can be implemented as a 32-iteration loop that tests each bit, incrementing a counter if the bit is set:
def popcount_spec (x : BitVec 32) : BitVec 32 :=
(32 : Nat).fold (init := 0) fun i _ pop =>
pop + ((x >>> i) &&& 1)
An alternative implementation of popcount is described in Hacker's Delight, Second Edition, by Henry S. Warren,
Jr. in Figure 5-2 on p. 82.
It uses low-level bitwise operations to compute the same value with far fewer operations:
def popcount (x : BitVec 32) : BitVec 32 :=
let x := x - ((x >>> 1) &&& 0x55555555)
let x := (x &&& 0x33333333) + ((x >>> 2) &&& 0x33333333)
let x := (x + (x >>> 4)) &&& 0x0F0F0F0F
let x := x + (x >>> 8)
let x := x + (x >>> 16)
let x := x &&& 0x0000003F
x
These two implementations can be proven equivalent using bv_decide:
theorem popcount_correct : popcount = popcount_spec := ⊢ popcount = popcount_spec
x:BitVec 32⊢ popcount x = popcount_spec x
x:BitVec 32⊢ ((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) + ((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32)) >>>
4 &&&
252645135#32) +
((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32)) >>>
4 &&&
252645135#32) >>>
8 +
(((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32)) >>>
4 &&&
252645135#32) +
((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32) &&& 858993459#32) +
((x - (x >>> 1 &&& 1431655765#32)) >>> 2 &&& 858993459#32)) >>>
4 &&&
252645135#32) >>>
8) >>>
16 &&&
63#32 =
(x &&& 1#32) + (x >>> 1 &&& 1#32) + (x >>> 2 &&& 1#32) + (x >>> 3 &&& 1#32) + (x >>> 4 &&& 1#32) +
(x >>> 5 &&& 1#32) +
(x >>> 6 &&& 1#32) +
(x >>> 7 &&& 1#32) +
(x >>> 8 &&& 1#32) +
(x >>> 9 &&& 1#32) +
(x >>> 10 &&& 1#32) +
(x >>> 11 &&& 1#32) +
(x >>> 12 &&& 1#32) +
(x >>> 13 &&& 1#32) +
(x >>> 14 &&& 1#32) +
(x >>> 15 &&& 1#32) +
(x >>> 16 &&& 1#32) +
(x >>> 17 &&& 1#32) +
(x >>> 18 &&& 1#32) +
(x >>> 19 &&& 1#32) +
(x >>> 20 &&& 1#32) +
(x >>> 21 &&& 1#32) +
(x >>> 22 &&& 1#32) +
(x >>> 23 &&& 1#32) +
(x >>> 24 &&& 1#32) +
(x >>> 25 &&& 1#32) +
(x >>> 26 &&& 1#32) +
(x >>> 27 &&& 1#32) +
(x >>> 28 &&& 1#32) +
(x >>> 29 &&& 1#32) +
(x >>> 30 &&& 1#32) +
(x >>> 31 &&& 1#32)
All goals completed! 🐙
BitVec.toInt {n : Nat} (x : BitVec n) : IntInterpret the bitvector as an integer stored in two's complement form.
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).
BitVec.ule {n : Nat} (x y : BitVec n) : BoolUnsigned less-than-or-equal-to for bit vectors.
SMT-LIB name: bvule.
BitVec.sle {n : Nat} (x y : BitVec n) : BoolSigned less-than-or-equal-to for bit vectors.
SMT-LIB name: bvsle.
BitVec.ult {n : Nat} (x y : BitVec n) : BoolUnsigned less-than for bit vectors.
SMT-LIB name: bvult.
These operations treat bitvectors as sequences of bits, rather than as encodings of numbers.
BitVec.cons {n : Nat} (msb : Bool)
(lsbs : BitVec n) : 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.
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.
BitVec.shiftConcat {n : Nat} (x : BitVec n)
(b : Bool) : BitVec n
x.shiftConcat b shifts all bits of x to the left by 1 and sets the least significant bit to b.
It is a non-dependent version of concat that does not change the total bitwidth.
BitVec.truncate {w : Nat} (v : Nat)
(x : BitVec w) : BitVec v
Transform x of length w into a bitvector of length v, by either:
zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
truncating the high bits, if v < w.
SMT-LIB name: zero_extend.
BitVec.setWidth {w : Nat} (v : Nat)
(x : BitVec w) : BitVec v
Transform x of length w into a bitvector of length v, by either:
zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
truncating the high bits, if v < w.
SMT-LIB name: zero_extend.
BitVec.setWidth' {n w : Nat} (le : n ≤ w)
(x : BitVec n) : BitVec w
A version of setWidth that requires a proof the new width is at least as large,
and is a computational noop.
BitVec.append {n m : Nat} (msbs : BitVec n)
(lsbs : BitVec m) : 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.
BitVec.replicate {w : Nat} (i : Nat) :
BitVec w → BitVec (w * i)
replicate i x concatenates i copies of x into a new vector of length w*i.
BitVec.rotateLeft {w : Nat} (x : BitVec w)
(n : Nat) : BitVec w
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.
BitVec.rotateRight {w : Nat} (x : BitVec w)
(n : Nat) : BitVec w
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.
BitVec.getMsbD {w : Nat} (x : BitVec w)
(i : Nat) : Bool
Return the i-th most significant bit or false if i ≥ w.
BitVec.getMsb' {w : Nat} (x : BitVec w)
(i : Fin w) : Bool
Return the i-th most significant bit.
This will be renamed getMsb after the existing deprecated alias is removed.
BitVec.getMsb? {w : Nat} (x : BitVec w)
(i : Nat) : Option Bool
Return the i-th most significant bit or none if i ≥ w.
BitVec.getLsbD {w : Nat} (x : BitVec w)
(i : Nat) : Bool
Return the i-th least significant bit or false if i ≥ w.
BitVec.getLsb' {w : Nat} (x : BitVec w)
(i : Fin w) : Bool
Return the i-th least significant bit.
This will be renamed getLsb after the existing deprecated alias is removed.
BitVec.getLsb? {w : Nat} (x : BitVec w)
(i : Nat) : Option Bool
Return the i-th least significant bit or none if i ≥ w.
These operators modify the individual bits of one or more bitvectors.
BitVec.and {n : Nat} (x y : BitVec n) : BitVec nBitwise AND for bit vectors.
0b1010#4 &&& 0b0110#4 = 0b0010#4
SMT-LIB name: bvand.
BitVec.or {n : Nat} (x y : BitVec n) : BitVec nBitwise OR for bit vectors.
0b1010#4 ||| 0b0110#4 = 0b1110#4
SMT-LIB name: bvor.
BitVec.not {n : Nat} (x : BitVec n) : BitVec nBitwise NOT for bit vectors.
~~~(0b0101#4) == 0b1010
SMT-LIB name: bvnot.
BitVec.xor {n : Nat} (x y : BitVec n) : BitVec nBitwise XOR for bit vectors.
0b1010#4 ^^^ 0b0110#4 = 0b1100#4
SMT-LIB name: bvxor.
BitVec.zeroExtend {w : Nat} (v : Nat)
(x : BitVec w) : BitVec v
Transform x of length w into a bitvector of length v, by either:
zero extending, that is, adding zeros in the high bits until it has length v, if v > w, or
truncating the high bits, if v < w.
SMT-LIB name: zero_extend.
BitVec.signExtend {w : Nat} (v : Nat)
(x : BitVec w) : BitVec v
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.
BitVec.ushiftRight {n : Nat} (x : BitVec n)
(s : Nat) : BitVec n
(Logical) right shift for bit vectors. 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.
These operators treat bitvectors as numbers. Some operations are signed, while others are unsigned. Because bitvectors are understood as two's complement numbers, addition, subtraction and multiplication coincide for the signed and unsigned interpretations.
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.
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.
BitVec.mul {n : Nat} (x y : BitVec n) : BitVec n
Multiplication for bit vectors. This can be interpreted as either signed or unsigned
multiplication modulo 2^n.
SMT-LIB name: bvmul.
BitVec.udiv {n : Nat} (x y : BitVec n) :
BitVec nUnsigned division for bit vectors using the Lean convention where division by zero returns zero.
BitVec.smtUDiv {n : Nat} (x y : BitVec n) :
BitVec n
Unsigned division for bit vectors using the
SMT-LIB convention
where division by zero returns the allOnes bitvector.
SMT-LIB name: bvudiv.
BitVec.umod {n : Nat} (x y : BitVec n) :
BitVec nUnsigned modulo for bit vectors.
SMT-LIB name: bvurem.
BitVec.neg {n : Nat} (x : BitVec n) : BitVec n
Negation for bit vectors. This can be interpreted as either signed or unsigned negation
modulo 2^n.
SMT-LIB name: bvneg.
BitVec.sdiv {n : Nat} (x y : BitVec n) :
BitVec nSigned 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
BitVec.smod {m : Nat} (x y : BitVec m) :
BitVec mRemainder for signed division rounded to negative infinity.
SMT-LIB name: bvsmod.
BitVec.srem {n : Nat} (x y : BitVec n) :
BitVec nRemainder for signed division rounding to zero.
SMT-LIB name: bvsrem.
BitVec.iunfoldr.{u_1} {w : Nat} {α : Type u_1}
(f : Fin w → α → α × Bool) (s : α) :
α × BitVec w
iunfoldr is an iterative operation that applies a function f repeatedly.
It produces a sequence of state values [s_0, s_1 .. s_w] and a bitvector
v where f i s_i = (s_{i+1}, b_i) and b_i is bit ith least-significant bit
in v (e.g., getLsb v i = b_i).
Theorems involving iunfoldr can be eliminated using iunfoldr_replace below.
The standard library contains a number of helper implementations that are useful to implement bit blasting, which is the technique used by bv_decide to encode propositions as Boolean satisfiability problems for external solvers.
BitVec.adc {w : Nat} (x y : BitVec w) :
Bool → Bool × BitVec wBitwise addition implemented via a ripple carry adder.
BitVec.carry {w : Nat} (i : Nat)
(x y : BitVec w) (c : Bool) : Bool
carry i x y c returns true if the i carry bit is true when computing x + y + c.
BitVec.mulRec {w : Nat} (x y : BitVec w)
(s : Nat) : BitVec wA recurrence that describes multiplication as repeated addition. Is useful for bitblasting multiplication.
BitVec.divRec {w : Nat} (m : Nat)
(args : BitVec.DivModArgs w)
(qr : BitVec.DivModState w) :
BitVec.DivModState wA recursive definition of division for bitblasting, in terms of a shift-subtraction circuit.
BitVec.divSubtractShift {w : Nat}
(args : BitVec.DivModArgs w)
(qr : BitVec.DivModState w) :
BitVec.DivModState w
One round of the division algorithm, that tries to perform a subtract shift.
Note that this should only be called when r.msb = false, so we will not overflow.
BitVec.shiftLeftRec {w₁ w₂ : Nat}
(x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
BitVec w₁
shiftLeftRec x y n shifts x to the left by the first n bits of y.
The theorem shiftLeft_eq_shiftLeftRec proves the equivalence of (x <<< y) and shiftLeftRec.
Together with equations shiftLeftRec_zero, shiftLeftRec_succ,
this allows us to unfold shiftLeft into a circuit for bitblasting.
BitVec.sshiftRightRec {w₁ w₂ : Nat}
(x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
BitVec w₁
sshiftRightRec x y n shifts x arithmetically/signed to the right by the first n bits of y.
The theorem sshiftRight_eq_sshiftRightRec proves the equivalence of (x.sshiftRight y) and sshiftRightRec.
Together with equations sshiftRightRec_zero, sshiftRightRec_succ,
this allows us to unfold sshiftRight into a circuit for bitblasting.
BitVec.ushiftRightRec {w₁ w₂ : Nat}
(x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
BitVec w₁
ushiftRightRec x y n shifts x logically to the right by the first n bits of y.
The theorem shiftRight_eq_ushiftRightRec proves the equivalence
of (x >>> y) and ushiftRightRec.
Together with equations ushiftRightRec_zero, ushiftRightRec_succ,
this allows us to unfold ushiftRight into a circuit for bitblasting.