We define bitvectors. We choose the Fin
representation over others for its relative efficiency
(Lean has special support for Nat
), alignment with UIntXY
types which are also represented
with Fin
, 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.
- ofFin :: (
Interpret a bitvector as a number less than
2^w
. O(1), because we useFin
as the internal representation of a bitvector.- )
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
.
Instances For
Equations
- Std.instDecidableEqBitVec = Std.decEqBitVec✝
The BitVec
with value i mod 2^n
. Treated as an operation on bitvectors,
this is truncation of the high bits when downcasting and zero-extension when upcasting.
Equations
- i#n = { toFin := Fin.ofNat' i (_ : 0 < 2 ^ n) }
Instances For
Given a bitvector a
, return the underlying Nat
. This is O(1) because BitVec
is a
(zero-cost) wrapper around a Nat
.
Equations
- Std.BitVec.toNat a = a.toFin.val
Instances For
Return the i
-th least significant bit or false
if i ≥ w
.
Equations
- Std.BitVec.getLsb x i = (Std.BitVec.toNat x &&& 1 <<< i != 0)
Instances For
Return the i
-th most significant bit or false
if i ≥ w
.
Equations
- Std.BitVec.getMsb x i = (decide (i < w) && Std.BitVec.getLsb x (w - 1 - i))
Instances For
Return most-significant bit in bitvector.
Equations
- Std.BitVec.msb a = Std.BitVec.getMsb a 0
Instances For
The BitVec
with value (2^n + (i mod 2^n)) mod 2^n
.
Equations
- Std.BitVec.ofInt n i = match i with | Int.ofNat a => a#n | Int.negSucc a => (2 ^ n - 1 - a % 2 ^ n)#n
Instances For
Interpret the bitvector as an integer stored in two's complement form.
Equations
- Std.BitVec.toInt a = if Std.BitVec.msb a = true then Int.ofNat (Std.BitVec.toNat a) - Int.ofNat (2 ^ n) else Int.ofNat (Std.BitVec.toNat a)
Instances For
Return a bitvector 0
of size n
. This is the bitvector with all zero bits.
Equations
- Std.BitVec.zero n = 0#n
Instances For
Equations
- Std.BitVec.instInhabitedBitVec = { default := Std.BitVec.zero n }
Equations
- Std.BitVec.instOfNatBitVec = { ofNat := i#n }
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
Convert bitvector into a fixed-width hex number.
Equations
- Std.BitVec.toHex x = let s := List.asString (Nat.toDigits 16 (Std.BitVec.toNat x)); let t := List.asString (List.replicate ((n + 3) / 4 - String.length s) (Char.ofNat 48)); t ++ s
Instances For
Equations
- Std.BitVec.instReprBitVec = { reprPrec := fun a x => Std.Format.text "0x" ++ Std.Format.text (Std.BitVec.toHex a) ++ Std.Format.text "#" ++ repr n }
Theorem for normalizing the bit vector literal representation.
Addition for bit vectors. This can be interpreted as either signed or unsigned addition
modulo 2^n
.
SMT-Lib name: bvadd
.
Equations
- Std.BitVec.add x y = { toFin := x.toFin + y.toFin }
Instances For
Equations
- Std.BitVec.instAddBitVec = { add := Std.BitVec.add }
Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
modulo 2^n
.
Equations
- Std.BitVec.sub x y = { toFin := x.toFin - y.toFin }
Instances For
Equations
- Std.BitVec.instSubBitVec = { sub := Std.BitVec.sub }
Negation for bit vectors. This can be interpreted as either signed or unsigned negation
modulo 2^n
.
SMT-Lib name: bvneg
.
Equations
- Std.BitVec.neg x = Std.BitVec.sub 0 x
Instances For
Equations
- Std.BitVec.instNegBitVec = { neg := Std.BitVec.neg }
Return the absolute value of a signed bitvector.
Equations
- Std.BitVec.abs s = if Std.BitVec.msb s = true then Std.BitVec.neg s else s
Instances For
Multiplication for bit vectors. This can be interpreted as either signed or unsigned negation
modulo 2^n
.
SMT-Lib name: bvmul
.
Equations
- Std.BitVec.mul x y = { toFin := x.toFin * y.toFin }
Instances For
Equations
- Std.BitVec.instMulBitVec = { mul := Std.BitVec.mul }
Unsigned division for bit vectors using the Lean convention where division by zero returns zero.
Equations
- Std.BitVec.udiv x y = { toFin := x.toFin / y.toFin }
Instances For
Equations
- Std.BitVec.instDivBitVec = { div := Std.BitVec.udiv }
Unsigned modulo for bit vectors.
SMT-Lib name: bvurem
.
Equations
- Std.BitVec.umod x y = { toFin := x.toFin % y.toFin }
Instances For
Equations
- Std.BitVec.instModBitVec = { mod := Std.BitVec.umod }
Unsigned division for bit vectors using the
SMT-Lib convention
where division by zero returns the allOnes
bitvector.
SMT-Lib name: bvudiv
.
Equations
- Std.BitVec.smtUDiv x y = if y = 0 then -1 else Std.BitVec.udiv x 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
- One or more equations did not get rendered due to their size.
Instances For
Remainder for signed division rounding to zero.
SMT_Lib name: bvsrem
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Remainder for signed division rounded to negative infinity.
SMT_Lib name: bvsmod
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unsigned less-than for bit vectors.
SMT-Lib name: bvult
.
Equations
- Std.BitVec.ult x y = decide (x.toFin < y.toFin)
Instances For
Unsigned less-than-or-equal-to for bit vectors.
SMT-Lib name: bvule
.
Equations
- Std.BitVec.ule x y = decide (x.toFin ≤ y.toFin)
Instances For
Signed less-than for bit vectors.
BitVec.slt 6#4 7 = true
BitVec.slt 7#4 8 = false
SMT-Lib name: bvslt
.
Equations
- Std.BitVec.slt x y = decide (Std.BitVec.toInt x < Std.BitVec.toInt y)
Instances For
Signed less-than-or-equal-to for bit vectors.
SMT-Lib name: bvsle
.
Equations
- Std.BitVec.sle x y = decide (Std.BitVec.toInt x ≤ Std.BitVec.toInt y)
Instances For
Bitwise AND for bit vectors.
0b1010#4 &&& 0b0110#4 = 0b0010#4
SMT-Lib name: bvand
.
Equations
- Std.BitVec.and x y = { toFin := x.toFin &&& y.toFin }
Instances For
Equations
- Std.BitVec.instAndOpBitVec = { and := Std.BitVec.and }
Bitwise OR for bit vectors.
0b1010#4 ||| 0b0110#4 = 0b1110#4
SMT-Lib name: bvor
.
Equations
- Std.BitVec.or x y = { toFin := x.toFin ||| y.toFin }
Instances For
Equations
- Std.BitVec.instOrOpBitVec = { or := Std.BitVec.or }
Bitwise XOR for bit vectors.
0b1010#4 ^^^ 0b0110#4 = 0b1100#4
SMT-Lib name: bvxor
.
Equations
- Std.BitVec.xor x y = { toFin := x.toFin ^^^ y.toFin }
Instances For
Equations
- Std.BitVec.instXorBitVec = { xor := Std.BitVec.xor }
Bitwise NOT for bit vectors.
~~~(0b0101#4) == 0b1010
SMT-Lib name: bvnot
.
Equations
- Std.BitVec.not x = -(x + 1#n)
Instances For
Equations
- Std.BitVec.instComplementBitVec = { complement := Std.BitVec.not }
Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is
equivalent to a * 2^s
, modulo 2^n
.
SMT-Lib name: bvshl
except this operator uses a Nat
shift value.
Equations
- Std.BitVec.shiftLeft a s = (Std.BitVec.toNat a <<< s)#n
Instances For
Equations
- Std.BitVec.instHShiftLeftBitVecNat = { hShiftLeft := Std.BitVec.shiftLeft }
(Logical) right shift for bit vectors. The high bits are filled with zeros.
As a numeric operation, this is equivalent to a / 2^s
, rounding down.
SMT-Lib name: bvlshr
except this operator uses a Nat
shift value.
Equations
- Std.BitVec.ushiftRight a s = (Std.BitVec.toNat a >>> s)#n
Instances For
Equations
- Std.BitVec.instHShiftRightBitVecNat = { hShiftRight := Std.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 a.toInt >>> s
.
SMT-Lib name: bvashr
except this operator uses a Nat
shift value.
Equations
- Std.BitVec.sshiftRight a s = Std.BitVec.ofInt n (Std.BitVec.toInt a >>> s)
Instances For
Equations
- Std.BitVec.instHShiftLeftBitVec = { hShiftLeft := fun x y => x <<< Std.BitVec.toNat y }
Equations
- Std.BitVec.instHShiftRightBitVec = { hShiftRight := fun x y => x >>> Std.BitVec.toNat y }
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
- Std.BitVec.append msbs lsbs = (Std.BitVec.toNat msbs <<< m ||| Std.BitVec.toNat lsbs)#(n + m)
Instances For
Equations
- Std.BitVec.instHAppendBitVecHAddNatInstHAddInstAddNat = { hAppend := Std.BitVec.append }
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
- Std.BitVec.extractLsb' start len a = (Std.BitVec.toNat a >>> start)#len
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
- Std.BitVec.extractLsb hi lo a = Std.BitVec.extractLsb' lo (hi - lo + 1) a
Instances For
replicate i x
concatenates i
copies of x
into a new vector of length w*i
.
Equations
- Std.BitVec.replicate 0 x = 0
- Std.BitVec.replicate (Nat.succ n) x = let_fun hEq := (_ : w + w * n = w * (n + 1)); hEq ▸ (x ++ Std.BitVec.replicate n x)
Instances For
Fills a bitvector with w
copies of the bit b
.
Equations
- Std.BitVec.fill w b = bif b then -1 else 0
Instances For
Zero extend vector x
of length w
by adding zeros in the high bits until it has length v
.
If v < w
then it truncates the high bits instead.
SMT-Lib name: zero_extend
.
Equations
- Std.BitVec.zeroExtend v x = (Std.BitVec.toNat x)#v
Instances For
Truncate the high bits of bitvector x
of length w
, resulting in a vector of length v
.
If v > w
then it zero-extends the vector instead.
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
- Std.BitVec.signExtend i x = (_ : i + w = w + i) ▸ (Std.BitVec.fill i (Std.BitVec.msb x) ++ x)