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.
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 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`).
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 bitvector 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! 🐙
The bitvector of width w that has the largest value when interpreted as an integer.
Fills a bitvector with w copies of the bit b.
Returns a bitvector of size n where all bits are 0.
Returns a bitvector of size n where all bits are 1.
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.
Interprets the bitvector as an integer stored in two's complement form.
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).
The bitvector 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).
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.
Unsigned less-than-or-equal-to for bitvectors.
SMT-LIB name: bvule.
Signed less-than-or-equal-to for bitvectors.
SMT-LIB name: bvsle.
Unsigned less-than for bitvectors.
SMT-LIB name: bvult.
Signed less-than for bitvectors.
SMT-LIB name: bvslt.
Examples:
BitVec.slt 6#4 7 = true
BitVec.slt 7#4 8 = false
These operations treat bitvectors as sequences of bits, rather than as encodings of numbers.
Prepends a single bit to the front of a bitvector, using big-endian order (see append).
The new bit is the most significant bit.
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.
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.
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.
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.
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.
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.
Concatenates i copies of x into a new vector of length w * i.
Reverses the bits in a bitvector.
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
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
Returns the most significant bit in a bitvector.
Returns the ith most significant bit.
Returns the ith least significant bit.
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.
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.
These operators modify the individual bits of one or more bitvectors.
Bitwise and for bitvectors. Usually accessed via the &&& operator.
SMT-LIB name: bvand.
Example:
0b1010#4 &&& 0b0110#4 = 0b0010#4
Bitwise or for bitvectors. Usually accessed via the ||| operator.
SMT-LIB name: bvor.
Example:
0b1010#4 ||| 0b0110#4 = 0b1110#4
Bitwise complement for bitvectors. Usually accessed via the ~~~ prefix operator.
SMT-LIB name: bvnot.
Example:
~~~(0b0101#4) == 0b1010
Bitwise xor for bitvectors. Usually accessed via the ^^^ operator.
SMT-LIB name: bvxor.
Example:
0b1010#4 ^^^ 0b0110#4 = 0b1100#4
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.
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.
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.
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.
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.
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.
Subtracts one bitvector from another. This can be interpreted as either signed or unsigned subtraction
modulo 2^n. Usually accessed via the - operator.
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.
Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
Usually accessed via the / operator.
Unsigned division of bitvectors using the
SMT-LIB convention,
where division by zero returns BitVector.allOnes n.
SMT-LIB name: bvudiv.
Unsigned modulo for bitvectors. Usually accessed via the % operator.
SMT-LIB name: bvurem.
Checks whether addition of x and y results in unsigned overflow.
SMT-LIB name: bvuaddo.
Returns the absolute value of a signed bitvector.
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.
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.
Remainder for signed division rounded to negative infinity.
SMT-LIB name: bvsmod.
Remainder for signed division rounding to zero.
SMT-LIB name: bvsrem.
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.
Constructs a bitvector by iteratively computing a state for each bit using the function f,
starting with the initial state s. At each step, the prior state and the current bit index are
passed to f, and it produces a bit along with the next state value. These bits are assembled into
the final bitvector.
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).
The theorem iunfoldr_replace allows uses of BitVec.iunfoldr to be replaced with declarative
specifications that are easier to reason about.
Given a function state that provides the correct state for every potential iteration count and a
function that computes these states from the correct initial state, the result of applying
BitVec.iunfoldr f to the initial state is the state corresponding to the bitvector's width paired
with the bitvector that consists of each computed bit.
This theorem can be used to prove properties of functions that are defined using BitVec.iunfoldr.
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.
Bitwise addition implemented via a ripple carry adder.
Carry function for bitwise addition.
carry i x y c returns true if the i carry bit is true when computing x + y + c.
A recurrence that describes multiplication as repeated addition.
This function is useful for bit blasting multiplication.
A recursive definition of division for bit blasting, in terms of a shift-subtraction circuit.
BitVec.divSubtractShift {w : Nat} (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.DivModState wBitVec.divSubtractShift {w : Nat} (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.DivModState w
One round of the division algorithm. It tries to perform a subtract shift.
This should only be called when r.msb = false, so it will not overflow.
Shifts x to the left by the first n bits of y.
The theorem BitVec.shiftLeft_eq_shiftLeftRec proves the equivalence of (x <<< y) and
BitVec.shiftLeftRec x y.
Together with equations BitVec.shiftLeftRec_zero and BitVec.shiftLeftRec_succ, this allows
BitVec.shiftLeft to be unfolded into a circuit for bit blasting.
Shifts x arithmetically (signed) to the right by the first n bits of y.
The theorem BitVec.sshiftRight_eq_sshiftRightRec proves the equivalence of (x.sshiftRight y) and
BitVec.sshiftRightRec x y. Together with equations BitVec.sshiftRightRec_zero, and
BitVec.sshiftRightRec_succ, this allows BitVec.sshiftRight to be unfolded into a circuit for
bit blasting.
Shifts x logically to the right by the first n bits of y.
The theorem BitVec.shiftRight_eq_ushiftRightRec proves the equivalence
of (x >>> y) and BitVec.ushiftRightRec.
Together with equations BitVec.ushiftRightRec_zero and BitVec.ushiftRightRec_succ,
this allows BitVec.ushiftRight to be unfolded into a circuit for bit blasting.
