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.
Theorem for normalizing the bitvector literal representation.
All empty bitvectors are equal
Returns a bitvector of size n
where all bits are 0
.
Equations
Instances For
Returns a bitvector of size n
where all bits are 1
.
Equations
Instances For
Returns the most significant bit in a bitvector.
Equations
Instances For
Interprets the bitvector as an integer stored in two's complement form.
Equations
Instances For
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
Instances For
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 iszero
(notofNat_zero
).The recommended spelling of
1#n
in identifiers isone
(notofNat_one
).
Equations
Instances For
Unexpander for bitvector literals.
Equations
Instances For
Notation for bitvector literals without truncation. i#'lt
is a shorthand for BitVec.ofNatLT i lt
.
Equations
Instances For
Unexpander for bitvector literals without truncation.
Equations
Instances For
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
Instances For
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
Instances For
Returns the absolute value of a signed bitvector.
Equations
Instances For
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
Instances For
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
Instances For
Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
Usually accessed via the /
operator.
Equations
Instances For
Unsigned modulo for bitvectors. Usually accessed via the %
operator.
SMT-LIB name: bvurem
.
Equations
Instances For
Unsigned division of bitvectors using the
SMT-LIB convention,
where division by zero returns BitVector.allOnes n
.
SMT-LIB name: bvudiv
.
Equations
Instances For
Signed T-division (using the truncating rounding convention) for bitvectors. This function obeys the Lean convention that division by zero returns zero.
Examples:
Equations
Instances For
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
Instances For
Remainder for signed division rounding to zero.
SMT-LIB name: bvsrem
.
Equations
Instances For
Remainder for signed division rounded to negative infinity.
SMT-LIB name: bvsmod
.
Equations
Instances For
Fills a bitvector with w
copies of the bit b
.
Equations
Instances For
Unsigned less-than for bitvectors.
SMT-LIB name: bvult
.
Equations
Instances For
Unsigned less-than-or-equal-to for bitvectors.
SMT-LIB name: bvule
.
Equations
Instances For
Signed less-than for bitvectors.
SMT-LIB name: bvslt
.
Examples:
BitVec.slt 6#4 7 = true
BitVec.slt 7#4 8 = false
Equations
Instances For
Signed less-than-or-equal-to for bitvectors.
SMT-LIB name: bvsle
.
Equations
Instances For
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
Instances For
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
Instances For
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 hasv
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
Instances For
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 hasv
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
Instances For
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 hasv
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
Instances For
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
Instances For
Bitwise and for bitvectors. Usually accessed via the &&&
operator.
SMT-LIB name: bvand
.
Example:
0b1010#4 &&& 0b0110#4 = 0b0010#4
Equations
Instances For
Bitwise xor for bitvectors. Usually accessed via the ^^^
operator.
SMT-LIB name: bvxor
.
Example:
0b1010#4 ^^^ 0b0110#4 = 0b1100#4
Equations
Instances For
Bitwise complement for bitvectors. Usually accessed via the ~~~
prefix operator.
SMT-LIB name: bvnot
.
Example:
~~~(0b0101#4) == 0b1010
Equations
Instances For
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
Instances For
Equations
Equations
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
Instances For
Auxiliary function for rotateLeft
, which does not take into account the case where
the rotation amount is greater than the bitvector width.
Equations
Instances For
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
Instances For
Auxiliary function for rotateRight
, which does not take into account the case where
the rotation amount is greater than the bitvector width.
Equations
Instances For
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
Instances For
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
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).
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
Instances For
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 i
th bit as 1
and all other bits as 0
.
Equations
Instances For
We add simp-lemmas that rewrite bitvector operations into the equivalent notation
Overflow #
Checks whether addition of x
and y
results in unsigned overflow.
SMT-LIB name: bvuaddo
.
Equations
Instances For
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
Instances For
Checks whether subtraction of x
and y
results in unsigned overflow.
SMT-Lib name: bvusubo
.
Equations
Instances For
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
Instances For
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
Instances For
Reverses the bits in a bitvector.
Equations
Instances For
umulOverflow x y
returns true
if multiplying x
and y
results in unsigned overflow.
SMT-Lib name: bvumulo
.
Equations
Instances For
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
.