Basic operations on bitvectors

This is a work-in-progress, and contains additions to other theories.

This file was moved to mathlib from core Lean in the switch to Lean 3.20.0c. It is not fully in compliance with mathlib style standards.

@[reducible]

def Bitvec (n : ℕ) : Type

Bitvec n is a Vector of Bool with length n.

@[reducible]

def Bitvec.zero (n : ℕ) : Bitvec n

Create a zero bitvector

@[reducible]

def Bitvec.one (n : ℕ) : Bitvec n

Create a bitvector of length n whose n-1st entry is 1 and other entries are 0.

def Bitvec.cong {a : ℕ} {b : ℕ} : a = b → Bitvec a → Bitvec b

Create a bitvector from another with a provably equal length.

def Bitvec.append {m : ℕ} {n : ℕ} : Bitvec m → Bitvec n → Bitvec (m + n)

Bitvec specific version of Vector.append

Shift operations

def Bitvec.shl {n : ℕ} (x : Bitvec n) (i : ℕ) : Bitvec n

shl x i is the bitvector obtained by left-shifting x i times and padding with false. If x.length < i then this will return the all-falses bitvector.

def Bitvec.ushr {n : ℕ} (x : Bitvec n) (i : ℕ) : Bitvec n

unsigned shift right

def Bitvec.sshr {m : ℕ} : Bitvec m → ℕ → Bitvec m

signed shift right

Bitwise operations

def Bitvec.not {n : ℕ} (bv : Bitvec n) : Bitvec n

bitwise not

def Bitvec.and {n : ℕ} : Bitvec n → Bitvec n → Bitvec n

bitwise and

def Bitvec.or {n : ℕ} : Bitvec n → Bitvec n → Bitvec n

bitwise or

def Bitvec.xor {n : ℕ} : Bitvec n → Bitvec n → Bitvec n

bitwise xor

instance Bitvec.instComplementBitvec {n : ℕ} : Complement (Bitvec n)

instance Bitvec.instAndOpBitvec {n : ℕ} : AndOp (Bitvec n)

instance Bitvec.instOrOpBitvec {n : ℕ} : OrOp (Bitvec n)

instance Bitvec.instXorBitvec {n : ℕ} : Xor (Bitvec n)

Arithmetic operators

def Bitvec.neg {n : ℕ} (x : Bitvec n) : Bitvec n

neg x is the two's complement of x.

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

Add with carry (no overflow)

def Bitvec.add {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Bitvec n

The sum of two bitvectors

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

Subtract with borrow

def Bitvec.sub {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Bitvec n

The difference of two bitvectors

instance Bitvec.instZeroBitvec {n : ℕ} : Zero (Bitvec n)

instance Bitvec.instOneBitvec {n : ℕ} : One (Bitvec n)

instance Bitvec.instAddBitvec {n : ℕ} : Add (Bitvec n)

instance Bitvec.instSubBitvec {n : ℕ} : Sub (Bitvec n)

instance Bitvec.instNegBitvec {n : ℕ} : Neg (Bitvec n)

def Bitvec.mul {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Bitvec n

The product of two bitvectors

instance Bitvec.instMulBitvec {n : ℕ} : Mul (Bitvec n)

Comparison operators

def Bitvec.uborrow {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Bool

uborrow x y returns true iff the "subtract with borrow" operation on x, y and false required a borrow.

def Bitvec.Ult {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Prop

unsigned less-than proposition

def Bitvec.Ugt {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Prop

unsigned greater-than proposition

def Bitvec.Ule {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Prop

unsigned less-than-or-equal-to proposition

def Bitvec.Uge {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Prop

unsigned greater-than-or-equal-to proposition

def Bitvec.sborrow {n : ℕ} : Bitvec n → Bitvec n → Bool

sborrow x y returns true iff x < y as two's complement integers

def Bitvec.Slt {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Prop

signed less-than proposition

def Bitvec.Sgt {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Prop

signed greater-than proposition

def Bitvec.Sle {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Prop

signed less-than-or-equal-to proposition

def Bitvec.Sge {n : ℕ} (x : Bitvec n) (y : Bitvec n) : Prop

signed greater-than-or-equal-to proposition

Conversion to nat and int

def Bitvec.ofNat (n : ℕ) : ℕ → Bitvec n

Create a bitvector from a nat

Equations

• Bitvec.ofNat 0 x = Vector.nil
• Bitvec.ofNat (Nat.succ n) x = Vector.append (Bitvec.ofNat n (x / 2)) (decide (x % 2 = 1) ::ᵥ Vector.nil)

def Bitvec.ofInt (n : ℕ) : ℤ → Bitvec n

Create a bitvector from an Int. The ring homomorphism from Int to bitvectors.

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

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

def Bitvec.bitsToNat (v : List Bool) : ℕ

Given a List of Bools, return the nat they represent as a list of binary digits.

def Bitvec.toNat {n : ℕ} (v : Bitvec n) : ℕ

Return the natural number encoded by the input bitvector

instance Bitvec.instPreorderBitvec (n : ℕ) : Preorder (Bitvec n)

def Bitvec.ofFin {n : ℕ} (i : Fin (2 ^ n)) : Bitvec n

convert fin to Bitvec

def Bitvec.toFin {n : ℕ} (i : Bitvec n) : Fin (2 ^ n)

convert Bitvec to fin

def Bitvec.toInt {n : ℕ} : Bitvec n → ℤ

Return the integer encoded by the input bitvector

Miscellaneous instances

instance Bitvec.instReprBitvec (n : ℕ) : Repr (Bitvec n)

instance instDecidableUlt {n : ℕ} {x : Bitvec n} {y : Bitvec n} : Decidable (Bitvec.Ult x y)

instance instDecidableUgt {n : ℕ} {x : Bitvec n} {y : Bitvec n} : Decidable (Bitvec.Ugt x y)

instance instHShiftLeftBitvecNat {n : ℕ} : HShiftLeft (Bitvec n) ℕ (Bitvec n)

instance instHShiftRightBitvecNat {n : ℕ} : HShiftRight (Bitvec n) ℕ (Bitvec n)

instance instShiftLeftBitvec {n : ℕ} : ShiftLeft (Bitvec n)

instance instShiftRightBitvec {n : ℕ} : ShiftRight (Bitvec n)