mathlib documentation

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  :
→ Type

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 : } :
a = bbitvec abitvec b

Create a bitvector from another with a provably equal length.

Equations
def bitvec.append {m n : } :
bitvec mbitvec nbitvec (m + n)

bitvec specific version of vector.append

Equations

Shift operations

def bitvec.shl {n : } :
bitvec nbitvec n

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

Equations
def bitvec.fill_shr {n : } :
bitvec nboolbitvec n

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 : } :
bitvec nbitvec n

unsigned shift right

Equations
def bitvec.sshr {m : } :
bitvec mbitvec m

signed shift right

Equations

Bitwise operations

def bitvec.not {n : } :
bitvec nbitvec n

bitwise not

Equations
def bitvec.and {n : } :
bitvec nbitvec nbitvec n

bitwise and

Equations
def bitvec.or {n : } :
bitvec nbitvec nbitvec n

bitwise or

Equations
def bitvec.xor {n : } :
bitvec nbitvec nbitvec n

bitwise xor

Equations

Arithmetic operators

def bitvec.xor3  :
boolboolboolbool

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

Equations
def bitvec.carry  :
boolboolboolbool

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

Equations
def bitvec.neg {n : } :
bitvec nbitvec n

neg x is the two's complement of x.

Equations
def bitvec.adc {n : } :
bitvec nbitvec nboolbitvec (n + 1)

Add with carry (no overflow)

Equations
def bitvec.add {n : } :
bitvec nbitvec nbitvec n

The sum of two bitvectors

Equations
def bitvec.sbb {n : } :
bitvec nbitvec nboolbool × bitvec n

Subtract with borrow

Equations
def bitvec.sub {n : } :
bitvec nbitvec nbitvec n

The difference of two bitvectors

Equations
@[instance]
def bitvec.has_zero {n : } :

Equations
@[instance]
def bitvec.has_one {n : } :

Equations
@[instance]
def bitvec.has_add {n : } :

Equations
@[instance]
def bitvec.has_sub {n : } :

Equations
@[instance]
def bitvec.has_neg {n : } :

Equations
def bitvec.mul {n : } :
bitvec nbitvec nbitvec n

The product of two bitvectors

Equations
@[instance]
def bitvec.has_mul {n : } :

Equations

Comparison operators

def bitvec.uborrow {n : } :
bitvec nbitvec nbool

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

Equations
def bitvec.ult {n : } :
bitvec nbitvec n → Prop

unsigned less-than proposition

Equations
def bitvec.ugt {n : } :
bitvec nbitvec n → Prop

unsigned greater-than proposition

Equations
def bitvec.ule {n : } :
bitvec nbitvec n → Prop

unsigned less-than-or-equal-to proposition

Equations
def bitvec.uge {n : } :
bitvec nbitvec n → Prop

unsigned greater-than-or-equal-to proposition

Equations
def bitvec.sborrow {n : } :
bitvec nbitvec nbool

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

Equations
def bitvec.slt {n : } :
bitvec nbitvec n → Prop

signed less-than proposition

Equations
def bitvec.sgt {n : } :
bitvec nbitvec n → Prop

signed greater-than proposition

Equations
def bitvec.sle {n : } :
bitvec nbitvec n → Prop

signed less-than-or-equal-to proposition

Equations
def bitvec.sge {n : } :
bitvec nbitvec n → Prop

signed greater-than-or-equal-to proposition

Equations

Conversion to nat and int

def bitvec.of_nat (n : ) :
bitvec n

Create a bitvector from a nat

Equations
def bitvec.of_int (n : ) :

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

Equations
def bitvec.add_lsb  :
bool

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

Equations

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

Equations
def bitvec.to_nat {n : } :
bitvec n

Return the natural number encoded by the input bitvector

Equations
theorem bitvec.to_nat_of_nat {k n : } :
(bitvec.of_nat k n).to_nat = n % 2 ^ k

def bitvec.to_int {n : } :
bitvec n

Return the integer encoded by the input bitvector

Equations

Miscellaneous instances

@[instance]
def bitvec.has_repr (n : ) :

Equations
@[instance]
def bitvec.ult.decidable {n : } {x y : bitvec n} :

Equations
@[instance]
def bitvec.ugt.decidable {n : } {x y : bitvec n} :

Equations