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

@[reducible, inline]

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

• x.adc' y c = let a := x.adc 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

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

Comparison operators

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

Unsigned greater than for bitvectors.

Equations

• x.ugt y = y.ult x

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

Signed greater than or equal to for bitvectors.

Equations

• x.uge y = y.ule x

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

Signed greater than for bitvectors.

Equations

• x.sgt y = y.slt x

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

Signed greater than or equal to for bitvectors.

Equations

• x.sge y = y.sle 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

• x.getLsb' i = x.getLsb ↑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

• x.getMsb' i = x.getMsb ↑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

• x.toLEList = List.ofFn x.getLsb'

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

• x.toBEList = List.ofFn x.getMsb'

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

Equations

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

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

Equations

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

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

Equations

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