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.

@[reducible]
def bitvec (n : ) :
Type

bitvec n is a vector of bool with length n.

Equations
@[protected, reducible]
def bitvec.zero (n : ) :

Create a zero bitvector

Equations
@[protected, reducible]
def bitvec.one (n : ) :

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

Equations
@[protected]
def bitvec.cong {a b : } (h : a = b) :
bitvec 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 : } (x : bitvec n) (i : ) :

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 : } (x : bitvec n) (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 : bitvec n) (i : ) :

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 #

@[protected]
def bitvec.xor3 (x y c : bool) :

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

Equations
@[protected]
def bitvec.carry (x y c : bool) :

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

Equations
@[protected]
def bitvec.neg {n : } (x : bitvec n) :

neg x is the two's complement of x.

Equations
def bitvec.adc {n : } (x y : bitvec n) (c : bool) :
bitvec (n + 1)

Add with carry (no overflow)

Equations
@[protected]
def bitvec.add {n : } (x y : bitvec n) :

The sum of two bitvectors

Equations
def bitvec.sbb {n : } (x y : bitvec n) (b : bool) :

Subtract with borrow

Equations
@[protected]
def bitvec.sub {n : } (x y : bitvec n) :

The difference of two bitvectors

Equations
@[protected, instance]
def bitvec.has_zero {n : } :
Equations
@[protected, instance]
def bitvec.has_one {n : } :
Equations
@[protected, instance]
def bitvec.has_add {n : } :
Equations
@[protected, instance]
def bitvec.has_sub {n : } :
Equations
@[protected, instance]
def bitvec.has_neg {n : } :
Equations
@[protected]
def bitvec.mul {n : } (x y : bitvec n) :

The product of two bitvectors

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

Comparison operators #

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

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

Equations
def bitvec.ult {n : } (x y : bitvec n) :
Prop

unsigned less-than proposition

Equations
Instances for bitvec.ult
def bitvec.ugt {n : } (x y : bitvec n) :
Prop

unsigned greater-than proposition

Equations
Instances for bitvec.ugt
def bitvec.ule {n : } (x y : bitvec n) :
Prop

unsigned less-than-or-equal-to proposition

Equations
def bitvec.uge {n : } (x y : bitvec 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 : } (x y : bitvec n) :
Prop

signed less-than proposition

Equations
def bitvec.sgt {n : } (x y : bitvec n) :
Prop

signed greater-than proposition

Equations
def bitvec.sle {n : } (x y : bitvec n) :
Prop

signed less-than-or-equal-to proposition

Equations
def bitvec.sge {n : } (x y : bitvec n) :
Prop

signed greater-than-or-equal-to proposition

Equations

Conversion to nat and int #

@[protected]
def bitvec.of_nat (n : ) :
bitvec n

Create a bitvector from a nat

Equations
@[protected]
def bitvec.of_int (n : ) :

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

Equations
def bitvec.add_lsb (r : ) (b : 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
@[protected]
def bitvec.to_nat {n : } (v : 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
@[protected]
def bitvec.to_int {n : } :
bitvec n

Return the integer encoded by the input bitvector

Equations

Miscellaneous instances #

@[protected, instance]
def bitvec.has_repr (n : ) :
Equations
@[protected, instance]
def bitvec.ult.decidable {n : } {x y : bitvec n} :
Equations
@[protected, instance]
def bitvec.ugt.decidable {n : } {x y : bitvec n} :
Equations