# Documentation

Mathlib.Data.Bitvec.Core

# 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.

def Bitvec (n : ) :

Bitvec n is a Vector of Bool with length n.

Equations
def Bitvec.zero (n : ) :

Create a zero bitvector

Equations
def Bitvec.one (n : ) :

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

Equations
def Bitvec.cong {a : } {b : } (h : a = b) :

Create a bitvector from another with a provably equal length.

Equations
• = match x with | { val := x, property := p } => { val := x, property := (_ : = b) }
def Bitvec.append {m : } {n : } :
Bitvec (m + n)

Bitvec specific version of Vector.append

Equations
• Bitvec.append = Vector.append

### 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.

Equations
def Bitvec.fillShr {n : } (x : ) (i : ) (fill : Bool) :

fill_shr x i fill is the bitvector obtained by right-shifting x i times and then padding with fill : Bool. If x.length < i then this will return the constant fill bitvector.

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

unsigned shift right

Equations
def Bitvec.sshr {m : } :

signed shift right

Equations

### Bitwise operations #

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

bitwise not

Equations
def Bitvec.and {n : } :

bitwise and

Equations
• Bitvec.and =
def Bitvec.or {n : } :

bitwise or

Equations
• Bitvec.or =
def Bitvec.xor {n : } :

bitwise xor

Equations
• Bitvec.xor =

### Arithmetic operators #

def Bitvec.xor3 (x : Bool) (y : Bool) (c : Bool) :

xor3 x y c is ((x XOR y) XOR c).

Equations
def Bitvec.carry (x : Bool) (y : Bool) (c : Bool) :

carry x y c is x && y || x && c || y && c.

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

neg x is the two's complement of x.

Equations
• = let f := fun y c => (y || c, xor y c); ().snd
def Bitvec.adc {n : } (x : ) (y : ) (c : Bool) :
Bitvec (n + 1)

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

The sum of two bitvectors

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

Subtract with borrow

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

The difference of two bitvectors

Equations
• = ().snd
instance Bitvec.instZeroBitvec {n : } :
Zero ()
Equations
• Bitvec.instZeroBitvec = { zero := }
instance Bitvec.instOneBitvec {n : } :
One ()
Equations
• Bitvec.instOneBitvec = { one := }
instance Bitvec.instAddBitvec {n : } :
Equations
instance Bitvec.instSubBitvec {n : } :
Sub ()
Equations
• Bitvec.instSubBitvec = { sub := Bitvec.sub }
instance Bitvec.instNegBitvec {n : } :
Neg ()
Equations
• Bitvec.instNegBitvec = { neg := Bitvec.neg }
def Bitvec.mul {n : } (x : ) (y : ) :

The product of two bitvectors

Equations
• = let f := fun r b => bif b then r + r + y else r + r; List.foldl f 0 ()
instance Bitvec.instMulBitvec {n : } :
Mul ()
Equations
• Bitvec.instMulBitvec = { mul := Bitvec.mul }

### 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.

Equations
• = ().fst
def Bitvec.Ult {n : } (x : ) (y : ) :

unsigned less-than proposition

Equations
• = ()
def Bitvec.Ugt {n : } (x : ) (y : ) :

unsigned greater-than proposition

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

unsigned less-than-or-equal-to proposition

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

unsigned greater-than-or-equal-to proposition

Equations
def Bitvec.sborrow {n : } :
Bool

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

Equations
• One or more equations did not get rendered due to their size.
def Bitvec.Slt {n : } (x : ) (y : ) :

signed less-than proposition

Equations
• = ()
def Bitvec.Sgt {n : } (x : ) (y : ) :

signed greater-than proposition

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

signed less-than-or-equal-to proposition

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

signed greater-than-or-equal-to proposition

Equations

### Conversion to nat and int#

def Bitvec.ofNat (n : ) :

Create a bitvector from a nat

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

Create a bitvector in the two's complement representation from an int

Equations
• = match x, x with | n, => | n, =>
def Bitvec.addLsb (r : ) (b : Bool) :

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

Equations
• = r + r + bif b then 1 else 0
def Bitvec.bitsToNat (v : ) :

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

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

Return the natural number encoded by the input bitvector

Equations
theorem Bitvec.bitsToNat_toList {n : } (x : ) :
theorem Bitvec.toNat_append {m : } (xs : ) (b : Bool) :
Bitvec.toNat (Vector.append xs (b ::ᵥ Vector.nil)) = * 2 + Bitvec.toNat (b ::ᵥ Vector.nil)
theorem Bitvec.bits_toNat_decide (n : ) :
Bitvec.toNat (decide (n % 2 = 1) ::ᵥ Vector.nil) = n % 2
theorem Bitvec.ofNat_succ {k : } {n : } :
Bitvec.ofNat () n = Vector.append (Bitvec.ofNat k (n / 2)) (decide (n % 2 = 1) ::ᵥ Vector.nil)
theorem Bitvec.toNat_ofNat {k : } {n : } :
Bitvec.toNat () = n % 2 ^ k
def Bitvec.toInt {n : } :

Return the integer encoded by the input bitvector

Equations
• One or more equations did not get rendered due to their size.

### Miscellaneous instances #

instance Bitvec.instReprBitvec (n : ) :
Repr ()
Equations
• = { reprPrec := fun b x => }
instance instDecidableUlt {n : } {x : } {y : } :
Equations
instance instDecidableUgt {n : } {x : } {y : } :
Equations