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

Create a bitvector from another with a provably equal length.

Equations
def bitvec.append {m n : } :
bitvec (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 : } :

signed shift right

Equations

### Bitwise operations #

def bitvec.not {n : } :

bitwise not

Equations
def bitvec.and {n : } :

bitwise and

Equations
def bitvec.or {n : } :

bitwise or

Equations
def bitvec.xor {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)

Equations
• x.adc y c = let f : boolbool := λ (x y c : bool), y c, y c) in bitvec.adc._match_1 y c)
• bitvec.adc._match_1 (c, z) = c ::ᵥ z
@[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 : } :
bool

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

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.bits_to_nat_to_list {n : } (x : bitvec n) :
theorem bitvec.to_nat_append {m : } (xs : bitvec m) (b : bool) :
theorem bitvec.to_nat_of_nat {k n : } :
n).to_nat = n % 2 ^ k
@[protected]
def bitvec.to_int {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