Basic operations on bitvectors

Std has defined bitvector of length w as Fin (2^w). Here we define a few more operations on these bitvectors

Main definitions

• Std.BitVec.sgt: Signed greater-than comparison of bitvectors
• Std.BitVec.sge: Signed greater-equals comparison of bitvectors
• Std.BitVec.ugt: Unsigned greater-than comparison of bitvectors
• Std.BitVec.uge: Unsigned greater-equals comparison of bitvectors

Constants

@[inline, reducible]

abbrev BitVec.one (w : ℕ) : BitVec w

The bitvector representing 1. That is, the bitvector with least-significant bit 1 and all other bits 0

Equations

• BitVec.one w = 1

Bitwise operations

Arithmetic operators

def BitVec.adc' {n : ℕ} (x : BitVec n) (y : BitVec n) (c : Bool) : BitVec (n + 1)

Add with carry (no overflow)

See also Std.BitVec.adc, which stores the carry bit separately.

Equations

• BitVec.adc' x y c = let a := BitVec.adc x y c; BitVec.cons a.1 a.2

def BitVec.sbb {n : ℕ} (x : BitVec n) (y : BitVec n) (b : Bool) : Bool × BitVec n

Subtract with borrow

Equations

• BitVec.sbb x y b = let y := y + { toFin := ↑(Bool.toNat b) }; (decide (x < y), x - y)

Comparison operators

def BitVec.ugt {w : ℕ} (x : BitVec w) (y : BitVec w) : Bool

Unsigned greater than for bitvectors.

Equations

• BitVec.ugt x y = BitVec.ult y x

def BitVec.uge {w : ℕ} (x : BitVec w) (y : BitVec w) : Bool

Signed greater than or equal to for bitvectors.

Equations

• BitVec.uge x y = BitVec.ule y x

def BitVec.sgt {w : ℕ} (x : BitVec w) (y : BitVec w) : Bool

Signed greater than for bitvectors.

Equations

• BitVec.sgt x y = BitVec.slt y x

def BitVec.sge {w : ℕ} (x : BitVec w) (y : BitVec w) : Bool

Signed greater than or equal to for bitvectors.

Equations

• BitVec.sge x y = BitVec.sle y x

Conversion to nat and int

def BitVec.addLsb (r : ℕ) (b : Bool) : ℕ

addLsb r b is r + r + 1 if b is true and r + r otherwise.

Equations

• BitVec.addLsb r b = Nat.bit b r

def BitVec.getLsb' {w : ℕ} (x : BitVec w) (i : Fin w) : Bool

Return the i-th least significant bit, where i is a statically known in-bounds index

Equations

• BitVec.getLsb' x i = BitVec.getLsb x ↑i

def BitVec.getMsb' {w : ℕ} (x : BitVec w) (i : Fin w) : Bool

Return the i-th most significant bit, where i is a statically known in-bounds index

Equations

• BitVec.getMsb' x i = BitVec.getMsb x ↑i

def BitVec.toLEList {w : ℕ} (x : BitVec w) : List Bool

Convert a bitvector to a little-endian list of Booleans. That is, the head of the list is the least significant bit

Equations

• BitVec.toLEList x = List.ofFn (BitVec.getLsb' x)

def BitVec.toBEList {w : ℕ} (x : BitVec w) : List Bool

Convert a bitvector to a big-endian list of Booleans. That is, the head of the list is the most significant bit

Equations

• BitVec.toBEList x = List.ofFn (BitVec.getMsb' x)

instance BitVec.instSMulNatBitVec {w : ℕ} : SMul ℕ (BitVec w)

Equations

• BitVec.instSMulNatBitVec = { smul := fun (x : ℕ) (y : BitVec w) => { toFin := x • y.toFin } }

instance BitVec.instSMulIntBitVec {w : ℕ} : SMul ℤ (BitVec w)

Equations

• BitVec.instSMulIntBitVec = { smul := fun (x : ℤ) (y : BitVec w) => { toFin := x • y.toFin } }

instance BitVec.instPowBitVecNat {w : ℕ} : Pow (BitVec w) ℕ

Equations

• BitVec.instPowBitVecNat = { pow := fun (x : BitVec w) (n : ℕ) => { toFin := x.toFin ^ n } }