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.
Constructor
BitVec.ofFin
20.5. Bitvectors
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.
20.5.1. Logical Model
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.
20.5.2. Runtime Representation
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.
20.5.3. Syntax
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.
Numeric Literals for Bitvectors
syntaxFixed-Width Bitvector Literals
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.
Fixed-Width Bitvector Literals
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 85#
A numeric literal is required to the left of the #:
(3 + 2)8
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
syntaxBounded Bitvector Literals
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.
Bounded Bitvector Literals
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)
20.5.4. Automation
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.
Popcount
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! 🐙
20.5.5. API Reference
20.5.5.1. Bounds
def
The bitvector of width w that has the largest value when interpreted as an integer.
def
The bitvector of width w that has the smallest value when interpreted as an integer.
20.5.5.2. Construction
def
Fills a bitvector with w copies of the bit b.
def
Returns a bitvector of size n where all bits are 0.
def
Returns a bitvector of size n where all bits are 1.
def
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.
20.5.5.3. Conversion
def
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.
def
Interprets the bitvector as an integer stored in two's complement form.
def
def
def
def
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).
def
The bitvector with value i mod 2^n.
Conventions for notations in identifiers:
-
The recommended spelling of
0#nin identifiers iszero(notofNat_zero). -
The recommended spelling of
1#nin identifiers isone(notofNat_one).
def
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.
20.5.5.4. Comparisons
def
Unsigned less-than-or-equal-to for bitvectors.
SMT-LIB name: bvule.
def
Signed less-than-or-equal-to for bitvectors.
SMT-LIB name: bvsle.
def
Unsigned less-than for bitvectors.
SMT-LIB name: bvult.
def
Signed less-than for bitvectors.
SMT-LIB name: bvslt.
Examples:
-
BitVec.slt 6#4 7 = true -
BitVec.slt 7#4 8 = false
20.5.5.5. Hashing
20.5.5.6. Sequence Operations
These operations treat bitvectors as sequences of bits, rather than as encodings of numbers.
def
Prepends a single bit to the front of a bitvector, using big-endian order (see append).
The new bit is the most significant bit.
def
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.
def
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.
def
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 hasvbits. -
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.
def
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 hasvbits. -
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.
def
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.
def
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.
def
Concatenates i copies of x into a new vector of length w * i.
def
Reverses the bits in a bitvector.
def
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
def
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
20.5.5.6.1. Bit Extraction
def
Returns the most significant bit in a bitvector.
def
Returns the ith most significant bit.
def
Returns the ith least significant bit.
def
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.
def
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.
20.5.5.7. Bitwise Operators
These operators modify the individual bits of one or more bitvectors.
def
Bitwise and for bitvectors. Usually accessed via the &&& operator.
SMT-LIB name: bvand.
Example:
-
0b1010#4 &&& 0b0110#4 = 0b0010#4
def
Bitwise or for bitvectors. Usually accessed via the ||| operator.
SMT-LIB name: bvor.
Example:
-
0b1010#4 ||| 0b0110#4 = 0b1110#4
def
Bitwise complement for bitvectors. Usually accessed via the ~~~ prefix operator.
SMT-LIB name: bvnot.
Example:
-
~~~(0b0101#4) == 0b1010
def
Bitwise xor for bitvectors. Usually accessed via the ^^^ operator.
SMT-LIB name: bvxor.
Example:
-
0b1010#4 ^^^ 0b0110#4 = 0b1100#4
def
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 hasvbits. -
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.
def
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.
def
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.
def
def
def
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.
20.5.5.8. Arithmetic
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.
def
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.
def
Subtracts one bitvector from another. This can be interpreted as either signed or unsigned subtraction
modulo 2^n. Usually accessed via the - operator.
def
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.
20.5.5.8.1. Unsigned Operations
def
Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
Usually accessed via the / operator.
def
Unsigned division of bitvectors using the
SMT-LIB convention,
where division by zero returns BitVector.allOnes n.
SMT-LIB name: bvudiv.
def
Unsigned modulo for bitvectors. Usually accessed via the % operator.
SMT-LIB name: bvurem.
def
Checks whether addition of x and y results in unsigned overflow.
SMT-LIB name: bvuaddo.
def
Checks whether subtraction of x and y results in unsigned overflow.
SMT-Lib name: bvusubo.
20.5.5.8.2. Signed Operations
def
Returns the absolute value of a signed bitvector.
def
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.
def
def
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.
def
Remainder for signed division rounded to negative infinity.
SMT-LIB name: bvsmod.
def
Remainder for signed division rounding to zero.
SMT-LIB name: bvsrem.
def
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.
def
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.
20.5.5.9. Iteration
def
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.
theorem
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.
20.5.5.10. Proof Automation
20.5.5.10.1. Bit Blasting
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.
def
Bitwise addition implemented via a ripple carry adder.
def
Carry function for bitwise addition.
def
carry i x y c returns true if the i carry bit is true when computing x + y + c.
def
A recurrence that describes multiplication as repeated addition.
This function is useful for bit blasting multiplication.
def
BitVec.divRec {w : Nat} (m : Nat) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.DivModState wBitVec.divRec {w : Nat} (m : Nat) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.DivModState w
A recursive definition of division for bit blasting, in terms of a shift-subtraction circuit.
def
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.
def
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.
def
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.
def
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.