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-LIBv2.
Equations
- BitVec.natCastInst = { natCast := BitVec.ofNat w }
Theorem for normalizing the bit vector literal representation.
All empty bitvectors are equal
Equations
Every bitvector of length 0 is equal to nil
, i.e., there is only one empty bitvector
Return a bitvector 0
of size n
. This is the bitvector with all zero bits.
Equations
- BitVec.zero n = 0#'⋯
Instances For
Equations
- BitVec.instInhabited = { default := BitVec.zero n }
Equations
- BitVec.instIntCast = { intCast := BitVec.ofInt w }
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
Convert bitvector into a fixed-width hex number.
Equations
- x.toHex = (List.replicate ((n + 3) / 4 - (Nat.toDigits 16 x.toNat).asString.length) '0').asString ++ (Nat.toDigits 16 x.toNat).asString
Instances For
Equations
- BitVec.instRepr = { reprPrec := fun (a : BitVec n) (x : Nat) => Std.Format.text "0x" ++ Std.Format.text a.toHex ++ Std.Format.text "#" ++ repr n }
Negation for bit vectors. This can be interpreted as either signed or unsigned negation
modulo 2^n
.
SMT-Lib name: bvneg
.
Equations
- x.neg = BitVec.ofNat n (2 ^ n - x.toNat)
Instances For
Multiplication for bit vectors. This can be interpreted as either signed or unsigned
multiplication modulo 2^n
.
SMT-Lib name: bvmul
.
Equations
- x.mul y = BitVec.ofNat n (x.toNat * y.toNat)
Instances For
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 BitVec.allOnes n else x.udiv y
Instances For
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
Instances For
Remainder for signed division rounding to zero.
SMT_Lib name: bvsrem
.
Equations
Instances For
Fills a bitvector with w
copies of the bit b
.
Equations
- BitVec.fill w b = bif b then -1 else 0
Instances For
Signed less-than for bit vectors.
BitVec.slt 6#4 7 = true
BitVec.slt 7#4 8 = false
SMT-Lib name: bvslt
.
Instances For
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
- BitVec.extractLsb' start len x = BitVec.ofNat len (x.toNat >>> start)
Instances For
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
- BitVec.extractLsb hi lo x = BitVec.extractLsb' lo (hi - lo + 1) x
Instances For
A version of setWidth
that requires a proof, but is a noop.
Equations
- BitVec.setWidth' le x = x.toNat#'⋯
Instances For
A version of setWidth
that requires a proof, but is a noop.
Equations
Instances For
shiftLeftZeroExtend x n
returns zeroExtend (w+n) x <<< n
without
needing to compute x % 2^(2+n)
.
Instances For
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
, ifv > w
, or - truncating the high bits, if
v < w
.
SMT-Lib name: zero_extend
.
Equations
- BitVec.setWidth v x = if h : w ≤ v then BitVec.setWidth' h x else BitVec.ofNat v x.toNat
Instances For
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
, ifv > w
, or - truncating the high bits, if
v < w
.
SMT-Lib name: zero_extend
.
Equations
Instances For
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
, ifv > w
, or - truncating the high bits, if
v < w
.
SMT-Lib name: zero_extend
.
Equations
Instances For
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
- BitVec.signExtend v x = BitVec.ofInt v x.toInt
Instances For
Bitwise NOT for bit vectors.
~~~(0b0101#4) == 0b1010
SMT-Lib name: bvnot
.
Equations
- x.not = BitVec.allOnes n ^^^ x
Instances For
Equations
- BitVec.instComplement = { complement := BitVec.not }
Left shift for bit vectors. 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.
Equations
- x.shiftLeft s = BitVec.ofNat n (x.toNat <<< s)
Instances For
Equations
- BitVec.instHShiftLeftNat = { hShiftLeft := BitVec.shiftLeft }
(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.
Instances For
Equations
- BitVec.instHShiftRightNat = { hShiftRight := BitVec.ushiftRight }
Arithmetic right shift for bit vectors. The high bits are filled with the
most-significant bit.
As a numeric operation, this is equivalent to x.toInt >>> s
.
SMT-Lib name: bvashr
except this operator uses a Nat
shift value.
Equations
- x.sshiftRight s = BitVec.ofInt n (x.toInt >>> s)
Instances For
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.
Instances For
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.
Instances For
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
- msbs.append lsbs = msbs.shiftLeftZeroExtend m ||| BitVec.setWidth' ⋯ lsbs
Instances For
replicate i x
concatenates i
copies of x
into a new vector of length w*i
.
Equations
- BitVec.replicate 0 x = 0#0
- BitVec.replicate n.succ x = BitVec.cast ⋯ (x ++ BitVec.replicate n x)
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).
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.
Equations
- x.shiftConcat b = BitVec.truncate n (x.concat b)
Instances For
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
- BitVec.cons msb lsbs = BitVec.cast ⋯ (BitVec.ofBool msb ++ lsbs)
Instances For
twoPow w i
is the bitvector 2^i
if i < w
, and 0
otherwise.
That is, 2 to the power i
.
For the bitwise point of view, it has the i
th bit as 1
and all other bits as 0
.
Equations
- BitVec.twoPow w i = 1#w <<< i
Instances For
We add simp-lemmas that rewrite bitvector operations into the equivalent notation
Converts a list of Bool
s to a big-endian BitVec
.
Equations
- BitVec.ofBoolListBE [] = 0#0
- BitVec.ofBoolListBE (b :: bs) = BitVec.cons b (BitVec.ofBoolListBE bs)
Instances For
Converts a list of Bool
s to a little-endian BitVec
.
Equations
- BitVec.ofBoolListLE [] = 0#0
- BitVec.ofBoolListLE (b :: bs) = (BitVec.ofBoolListLE bs).concat b