# Documentation

Mathlib.Data.Bitvec.Defs

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

Bitvec n is a Vector of Bool with length n.

Instances For
@[reducible]
def Bitvec.zero (n : ) :

Create a zero bitvector

Instances For
@[reducible]
def Bitvec.one (n : ) :

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

Instances For
def Bitvec.cong {a : } {b : } :
a = b

Create a bitvector from another with a provably equal length.

Instances For
def Bitvec.append {m : } {n : } :
Bitvec (m + n)

Bitvec specific version of Vector.append

Instances For

### Shift operations #

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

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.

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

unsigned shift right

Instances For
def Bitvec.sshr {m : } :

signed shift right

Instances For

### Bitwise operations #

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

bitwise not

Instances For
def Bitvec.and {n : } :

bitwise and

Instances For
def Bitvec.or {n : } :

bitwise or

Instances For
def Bitvec.xor {n : } :

bitwise xor

Instances For

### Arithmetic operators #

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

neg x is the two's complement of x.

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

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

The sum of two bitvectors

Instances For
def Bitvec.sbb {n : } (x : ) (y : ) (b : Bool) :

Subtract with borrow

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

The difference of two bitvectors

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

The product of two bitvectors

Instances For

### Comparison operators #

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

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

Instances For
def Bitvec.Ult {n : } (x : ) (y : ) :

unsigned less-than proposition

Instances For
def Bitvec.Ugt {n : } (x : ) (y : ) :

unsigned greater-than proposition

Instances For
def Bitvec.Ule {n : } (x : ) (y : ) :

unsigned less-than-or-equal-to proposition

Instances For
def Bitvec.Uge {n : } (x : ) (y : ) :

unsigned greater-than-or-equal-to proposition

Instances For
def Bitvec.sborrow {n : } :
Bool

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

Instances For
def Bitvec.Slt {n : } (x : ) (y : ) :

signed less-than proposition

Instances For
def Bitvec.Sgt {n : } (x : ) (y : ) :

signed greater-than proposition

Instances For
def Bitvec.Sle {n : } (x : ) (y : ) :

signed less-than-or-equal-to proposition

Instances For
def Bitvec.Sge {n : } (x : ) (y : ) :

signed greater-than-or-equal-to proposition

Instances For

### Conversion to nat and int#

def Bitvec.ofNat (n : ) :

Create a bitvector from a nat

Equations
Instances For
def Bitvec.ofInt (n : ) :

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

Instances For
def Bitvec.addLsb (r : ) (b : Bool) :

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

Instances For
def Bitvec.bitsToNat (v : ) :

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

Instances For
def Bitvec.toNat {n : } (v : ) :

Return the natural number encoded by the input bitvector

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

convert fin to Bitvec

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

convert Bitvec to fin

Instances For
def Bitvec.toInt {n : } :

Return the integer encoded by the input bitvector

Instances For

### Miscellaneous instances #

instance instDecidableUlt {n : } {x : } {y : } :
instance instDecidableUgt {n : } {x : } {y : } :