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.

structure Std.BitVec (w : Nat) : Type

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.

• 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.

• )

instance Std.instDecidableEqBitVec : {w : Nat} → DecidableEq (Std.BitVec w)

Equations

• Std.instDecidableEqBitVec = Std.decEqBitVec✝

@[inline]

def Std.BitVec.cast {n : Nat} {m : Nat} (eq : n = m) (i : Std.BitVec n) : Std.BitVec m

cast eq i embeds i into an equal BitVec type.

Equations

• Std.BitVec.cast eq i = { toFin := Fin.cast (_ : 2 ^ n = 2 ^ m) i.toFin }

@[match_pattern]

def Std.BitVec.ofNat (n : Nat) (i : Nat) : Std.BitVec n

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) }

def Std.BitVec.toNat {n : Nat} (a : Std.BitVec n) : Nat

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

theorem Std.BitVec.isLt {w : Nat} (x : Std.BitVec w) : Std.BitVec.toNat x < 2 ^ w

Return the bound in terms of toNat.

@[inline]

def Std.BitVec.getLsb {w : Nat} (x : Std.BitVec w) (i : Nat) : Bool

Return the i-th least significant bit or false if i ≥ w.

Equations

• Std.BitVec.getLsb x i = Nat.testBit (Std.BitVec.toNat x) i

@[inline]

def Std.BitVec.getMsb {w : Nat} (x : Std.BitVec w) (i : Nat) : Bool

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))

@[inline]

def Std.BitVec.msb {n : Nat} (a : Std.BitVec n) : Bool

Return most-significant bit in bitvector.

Equations

• Std.BitVec.msb a = Std.BitVec.getMsb a 0

def Std.BitVec.toInt {n : Nat} (a : Std.BitVec n) : Int

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)

def Std.BitVec.zero (n : Nat) : Std.BitVec n

Return a bitvector 0 of size n. This is the bitvector with all zero bits.

Equations

• Std.BitVec.zero n = { toFin := { val := 0, isLt := (_ : 0 < 2 ^ n) } }

instance Std.BitVec.instInhabitedBitVec {n : Nat} : Inhabited (Std.BitVec n)

Equations

• Std.BitVec.instInhabitedBitVec = { default := Std.BitVec.zero n }

instance Std.BitVec.instOfNatBitVec {n : Nat} {i : Nat} : OfNat (Std.BitVec n) i

Equations

• Std.BitVec.instOfNatBitVec = { ofNat := i#n }

def Std.BitVec.«term__#__» : Lean.TrailingParserDescr

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.

def Std.BitVec.unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander

Unexpander for bit vector literals.

Equations

• One or more equations did not get rendered due to their size.

def Std.BitVec.toHex {n : Nat} (x : Std.BitVec n) : String

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

instance Std.BitVec.instReprBitVec {n : Nat} : Repr (Std.BitVec n)

Equations

• One or more equations did not get rendered due to their size.

instance Std.BitVec.instToStringBitVec {n : Nat} : ToString (Std.BitVec n)

Equations

• Std.BitVec.instToStringBitVec = { toString := fun (a : Std.BitVec n) => toString (repr a) }

@[simp]

theorem Std.BitVec.ofNat_eq_ofNat {n : Nat} {i : Nat} : OfNat.ofNat i = i#n

Theorem for normalizing the bit vector literal representation.

def Std.BitVec.add {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

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 }

instance Std.BitVec.instAddBitVec {n : Nat} : Add (Std.BitVec n)

Equations

• Std.BitVec.instAddBitVec = { add := Std.BitVec.add }

def Std.BitVec.sub {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

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 }

instance Std.BitVec.instSubBitVec {n : Nat} : Sub (Std.BitVec n)

Equations

• Std.BitVec.instSubBitVec = { sub := Std.BitVec.sub }

def Std.BitVec.neg {n : Nat} (x : Std.BitVec n) : Std.BitVec n

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

instance Std.BitVec.instNegBitVec {n : Nat} : Neg (Std.BitVec n)

Equations

• Std.BitVec.instNegBitVec = { neg := Std.BitVec.neg }

def Std.BitVec.allOnes (n : Nat) : Std.BitVec n

Bit vector of size n where all bits are 1s

Equations

• Std.BitVec.allOnes n = -1

def Std.BitVec.abs {n : Nat} (s : Std.BitVec n) : Std.BitVec n

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

def Std.BitVec.mul {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

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 }

instance Std.BitVec.instMulBitVec {n : Nat} : Mul (Std.BitVec n)

Equations

• Std.BitVec.instMulBitVec = { mul := Std.BitVec.mul }

def Std.BitVec.udiv {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

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 }

instance Std.BitVec.instDivBitVec {n : Nat} : Div (Std.BitVec n)

Equations

• Std.BitVec.instDivBitVec = { div := Std.BitVec.udiv }

def Std.BitVec.umod {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

Unsigned modulo for bit vectors.

SMT-Lib name: bvurem.

Equations

• Std.BitVec.umod x y = { toFin := x.toFin % y.toFin }

instance Std.BitVec.instModBitVec {n : Nat} : Mod (Std.BitVec n)

Equations

• Std.BitVec.instModBitVec = { mod := Std.BitVec.umod }

def Std.BitVec.smtUDiv {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

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

def Std.BitVec.sdiv {n : Nat} (s : Std.BitVec n) (t : Std.BitVec n) : Std.BitVec n

Signed t-division for bit vectors using the Lean convention where division by zero returns zero.

sdiv 7#4 2 = 3#4
sdiv (-9#4) 2 = -4#4
sdiv 5#4 -2 = -2#4
sdiv (-7#4) (-2) = 3#4

Equations

• One or more equations did not get rendered due to their size.

def Std.BitVec.smtSDiv {n : Nat} (s : Std.BitVec n) (t : Std.BitVec n) : Std.BitVec n

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.

def Std.BitVec.srem {n : Nat} (s : Std.BitVec n) (t : Std.BitVec n) : Std.BitVec n

Remainder for signed division rounding to zero.

SMT_Lib name: bvsrem.

Equations

• One or more equations did not get rendered due to their size.

def Std.BitVec.smod {m : Nat} (s : Std.BitVec m) (t : Std.BitVec m) : Std.BitVec m

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.

def Std.BitVec.ult {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Bool

Unsigned less-than for bit vectors.

SMT-Lib name: bvult.

Equations

• Std.BitVec.ult x y = decide (x.toFin < y.toFin)

instance Std.BitVec.instLTBitVec {n : Nat} : LT (Std.BitVec n)

Equations

• Std.BitVec.instLTBitVec = { lt := fun (x y : Std.BitVec n) => x.toFin < y.toFin }

def Std.BitVec.ule {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Bool

Unsigned less-than-or-equal-to for bit vectors.

SMT-Lib name: bvule.

Equations

• Std.BitVec.ule x y = decide (x.toFin ≤ y.toFin)

instance Std.BitVec.instLEBitVec {n : Nat} : LE (Std.BitVec n)

Equations

• Std.BitVec.instLEBitVec = { le := fun (x y : Std.BitVec n) => x.toFin ≤ y.toFin }

def Std.BitVec.slt {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Bool

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)

def Std.BitVec.sle {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Bool

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)

def Std.BitVec.and {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

Bitwise AND for bit vectors.

0b1010#4 &&& 0b0110#4 = 0b0010#4

SMT-Lib name: bvand.

Equations

• Std.BitVec.and x y = { toFin := { val := Std.BitVec.toNat x &&& Std.BitVec.toNat y, isLt := (_ : Std.BitVec.toNat x &&& Std.BitVec.toNat y < 2 ^ n) } }

instance Std.BitVec.instAndOpBitVec {w : Nat} : AndOp (Std.BitVec w)

Equations

• Std.BitVec.instAndOpBitVec = { and := Std.BitVec.and }

def Std.BitVec.or {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

Bitwise OR for bit vectors.

0b1010#4 ||| 0b0110#4 = 0b1110#4

SMT-Lib name: bvor.

Equations

• Std.BitVec.or x y = { toFin := { val := Std.BitVec.toNat x ||| Std.BitVec.toNat y, isLt := (_ : Std.BitVec.toNat x ||| Std.BitVec.toNat y < 2 ^ n) } }

instance Std.BitVec.instOrOpBitVec {w : Nat} : OrOp (Std.BitVec w)

Equations

• Std.BitVec.instOrOpBitVec = { or := Std.BitVec.or }

def Std.BitVec.xor {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec n

Bitwise XOR for bit vectors.

0b1010#4 ^^^ 0b0110#4 = 0b1100#4

SMT-Lib name: bvxor.

Equations

• Std.BitVec.xor x y = { toFin := { val := Std.BitVec.toNat x ^^^ Std.BitVec.toNat y, isLt := (_ : Std.BitVec.toNat x ^^^ Std.BitVec.toNat y < 2 ^ n) } }

instance Std.BitVec.instXorBitVec {w : Nat} : Xor (Std.BitVec w)

Equations

• Std.BitVec.instXorBitVec = { xor := Std.BitVec.xor }

def Std.BitVec.not {n : Nat} (x : Std.BitVec n) : Std.BitVec n

Bitwise NOT for bit vectors.

~~~(0b0101#4) == 0b1010

SMT-Lib name: bvnot.

Equations

• Std.BitVec.not x = let ones := { toFin := { val := Nat.pred (1 <<< n), isLt := (_ : Nat.pred (1 <<< n) < 2 ^ n) } }; ones ^^^ x

instance Std.BitVec.instComplementBitVec {w : Nat} : Complement (Std.BitVec w)

Equations

• Std.BitVec.instComplementBitVec = { complement := Std.BitVec.not }

def Std.BitVec.ofInt (n : Nat) (i : Int) : Std.BitVec n

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 => ~~~a#n

def Std.BitVec.shiftLeft {n : Nat} (a : Std.BitVec n) (s : Nat) : Std.BitVec n

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

instance Std.BitVec.instHShiftLeftBitVecNat {w : Nat} : HShiftLeft (Std.BitVec w) Nat (Std.BitVec w)

Equations

• Std.BitVec.instHShiftLeftBitVecNat = { hShiftLeft := Std.BitVec.shiftLeft }

def Std.BitVec.ushiftRight {n : Nat} (a : Std.BitVec n) (s : Nat) : Std.BitVec n

(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

instance Std.BitVec.instHShiftRightBitVecNat {w : Nat} : HShiftRight (Std.BitVec w) Nat (Std.BitVec w)

Equations

• Std.BitVec.instHShiftRightBitVecNat = { hShiftRight := Std.BitVec.ushiftRight }

def Std.BitVec.sshiftRight {n : Nat} (a : Std.BitVec n) (s : Nat) : Std.BitVec n

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)

instance Std.BitVec.instHShiftLeftBitVec {m : Nat} {n : Nat} : HShiftLeft (Std.BitVec m) (Std.BitVec n) (Std.BitVec m)

Equations

• Std.BitVec.instHShiftLeftBitVec = { hShiftLeft := fun (x : Std.BitVec m) (y : Std.BitVec n) => x <<< Std.BitVec.toNat y }

instance Std.BitVec.instHShiftRightBitVec {m : Nat} {n : Nat} : HShiftRight (Std.BitVec m) (Std.BitVec n) (Std.BitVec m)

Equations

• Std.BitVec.instHShiftRightBitVec = { hShiftRight := fun (x : Std.BitVec m) (y : Std.BitVec n) => x >>> Std.BitVec.toNat y }

def Std.BitVec.rotateLeft {w : Nat} (x : Std.BitVec w) (n : Nat) : Std.BitVec w

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.

Equations

• Std.BitVec.rotateLeft x n = x <<< n ||| x >>> (w - n)

def Std.BitVec.rotateRight {w : Nat} (x : Std.BitVec w) (n : Nat) : Std.BitVec w

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.

Equations

• Std.BitVec.rotateRight x n = x >>> n ||| x <<< (w - n)

def Std.BitVec.zeroExtend' {n : Nat} {w : Nat} (le : n ≤ w) (x : Std.BitVec n) : Std.BitVec w

A version of zeroExtend that requires a proof, but is a noop.

Equations

• Std.BitVec.zeroExtend' le x = { toFin := { val := Std.BitVec.toNat x, isLt := (_ : Std.BitVec.toNat x < 2 ^ w) } }

def Std.BitVec.shiftLeftZeroExtend {w : Nat} (msbs : Std.BitVec w) (m : Nat) : Std.BitVec (w + m)

shiftLeftZeroExtend x n returns zeroExtend (w+n) x <<< n without needing to compute x % 2^(2+n).

Equations

• One or more equations did not get rendered due to their size.

def Std.BitVec.append {n : Nat} {m : Nat} (msbs : Std.BitVec n) (lsbs : Std.BitVec m) : Std.BitVec (n + m)

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.shiftLeftZeroExtend msbs m ||| Std.BitVec.zeroExtend' (_ : m ≤ n + m) lsbs

instance Std.BitVec.instHAppendBitVecHAddNatInstHAddInstAddNat {w : Nat} {v : Nat} : HAppend (Std.BitVec w) (Std.BitVec v) (Std.BitVec (w + v))

Equations

• Std.BitVec.instHAppendBitVecHAddNatInstHAddInstAddNat = { hAppend := Std.BitVec.append }

def Std.BitVec.extractLsb' {n : Nat} (start : Nat) (len : Nat) (a : Std.BitVec n) : Std.BitVec len

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

def Std.BitVec.extractLsb {n : Nat} (hi : Nat) (lo : Nat) (a : Std.BitVec n) : Std.BitVec (hi - lo + 1)

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

def Std.BitVec.replicate {w : Nat} (i : Nat) : Std.BitVec w → Std.BitVec (w * i)

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)

def Std.BitVec.fill (w : Nat) (b : Bool) : Std.BitVec w

Fills a bitvector with w copies of the bit b.

Equations

• Std.BitVec.fill w b = bif b then -1 else 0

def Std.BitVec.zeroExtend {w : Nat} (v : Nat) (x : Std.BitVec w) : Std.BitVec v

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 = if h : w ≤ v then Std.BitVec.zeroExtend' h x else (Std.BitVec.toNat x)#v

def Std.BitVec.truncate {w : Nat} (v : Nat) (x : Std.BitVec w) : Std.BitVec v

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

• @Std.BitVec.truncate = @Std.BitVec.zeroExtend

def Std.BitVec.signExtend {w : Nat} (v : Nat) (x : Std.BitVec w) : Std.BitVec v

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 v x = Std.BitVec.ofInt v (Std.BitVec.toInt x)

We add simp-lemmas that rewrite bitvector operations into the equivalent notation

@[simp]

theorem Std.BitVec.append_eq {w : Nat} {v : Nat} (x : Std.BitVec w) (y : Std.BitVec v) : Std.BitVec.append x y = x ++ y

@[simp]

theorem Std.BitVec.shiftLeft_eq {w : Nat} (x : Std.BitVec w) (n : Nat) : Std.BitVec.shiftLeft x n = x <<< n

@[simp]

theorem Std.BitVec.ushiftRight_eq {w : Nat} (x : Std.BitVec w) (n : Nat) : Std.BitVec.ushiftRight x n = x >>> n

@[simp]

theorem Std.BitVec.not_eq {w : Nat} (x : Std.BitVec w) : Std.BitVec.not x = ~~~x

@[simp]

theorem Std.BitVec.and_eq {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Std.BitVec.and x y = x &&& y

@[simp]

theorem Std.BitVec.or_eq {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Std.BitVec.or x y = x ||| y

@[simp]

theorem Std.BitVec.xor_eq {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Std.BitVec.xor x y = x ^^^ y

@[simp]

theorem Std.BitVec.neg_eq {w : Nat} (x : Std.BitVec w) : Std.BitVec.neg x = -x

@[simp]

theorem Std.BitVec.add_eq {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Std.BitVec.add x y = x + y

@[simp]

theorem Std.BitVec.sub_eq {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Std.BitVec.sub x y = x - y

@[simp]

theorem Std.BitVec.mul_eq {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Std.BitVec.mul x y = x * y

@[simp]

theorem Std.BitVec.zero_eq {n : Nat} : Std.BitVec.zero n = 0#n

@[simp]

theorem Std.BitVec.cast_ofNat {n : Nat} {m : Nat} (h : n = m) (x : Nat) : Std.BitVec.cast h x#n = x#m

@[simp]

theorem Std.BitVec.cast_cast {n : Nat} {m : Nat} {k : Nat} (h₁ : n = m) (h₂ : m = k) (x : Std.BitVec n) : Std.BitVec.cast h₂ (Std.BitVec.cast h₁ x) = Std.BitVec.cast (_ : n = k) x

@[simp]

theorem Std.BitVec.cast_eq {n : Nat} (h : n = n) (x : Std.BitVec n) : Std.BitVec.cast h x = x

def Std.BitVec.ofBool (b : Bool) : Std.BitVec 1

Turn a Bool into a bitvector of length 1

Equations

• Std.BitVec.ofBool b = bif b then 1 else 0

@[simp]

theorem Std.BitVec.ofBool_false : Std.BitVec.ofBool false = 0

@[simp]

theorem Std.BitVec.ofBool_true : Std.BitVec.ofBool true = 1

@[inline, reducible]

abbrev Std.BitVec.nil : Std.BitVec 0

The empty bitvector

Equations

• Std.BitVec.nil = 0

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).

def Std.BitVec.concat {n : Nat} (msbs : Std.BitVec n) (lsb : Bool) : Std.BitVec (n + 1)

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.

Equations

• Std.BitVec.concat msbs lsb = msbs ++ Std.BitVec.ofBool lsb

def Std.BitVec.cons {n : Nat} (msb : Bool) (lsbs : Std.BitVec n) : Std.BitVec (n + 1)

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

• Std.BitVec.cons msb lsbs = Std.BitVec.cast (_ : 1 + n = n + 1) (Std.BitVec.ofBool msb ++ lsbs)

instance Std.BitVec.instSubsingletonBitVecOfNatNatInstOfNatNat : Subsingleton (Std.BitVec 0)

All empty bitvectors are equal

Equations

• Std.BitVec.instSubsingletonBitVecOfNatNatInstOfNatNat = (_ : Subsingleton (Std.BitVec 0))

theorem Std.BitVec.eq_nil (x : Std.BitVec 0) : x = Std.BitVec.nil

Every bitvector of length 0 is equal to nil, i.e., there is only one empty bitvector

theorem Std.BitVec.append_ofBool {w : Nat} (msbs : Std.BitVec w) (lsb : Bool) : msbs ++ Std.BitVec.ofBool lsb = Std.BitVec.concat msbs lsb

theorem Std.BitVec.ofBool_append {w : Nat} (msb : Bool) (lsbs : Std.BitVec w) : Std.BitVec.ofBool msb ++ lsbs = Std.BitVec.cast (_ : w + 1 = 1 + w) (Std.BitVec.cons msb lsbs)