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 Std.BitVec.one (w : ℕ) : Std.BitVec w

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

Equations

• Std.BitVec.one w = 1

Bitwise operations

Arithmetic operators

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

Add with carry (no overflow)

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

Equations

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

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

Subtract with borrow

Equations

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

Comparison operators

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

Unsigned greater than for bitvectors.

Equations

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

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

Signed greater than or equal to for bitvectors.

Equations

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

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

Signed greater than for bitvectors.

Equations

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

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

Signed greater than or equal to for bitvectors.

Equations

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

Conversion to nat and int

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def Std.BitVec.toLEList {w : ℕ} (x : Std.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

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

def Std.BitVec.toBEList {w : ℕ} (x : Std.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

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

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

Equations

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

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

Equations

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

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

Equations

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

instance Std.BitVec.instNatCastBitVec {w : ℕ} : NatCast (Std.BitVec w)

Equations

• Std.BitVec.instNatCastBitVec = { natCast := Std.BitVec.ofNat w }

instance Std.BitVec.instIntCastBitVec {w : ℕ} : IntCast (Std.BitVec w)

Equations

• Std.BitVec.instIntCastBitVec = { intCast := Std.BitVec.ofInt w }