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.

source
def bitvec (n : ℕ) :
Type

bitvec n is a vector of bool with length n.

Equations
source
def bitvec.zero (n : ℕ) :
bitvec n

Create a zero bitvector

Equations
source
def bitvec.one (n : ℕ) :
bitvec n

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

Equations
source
def bitvec.cong {a b : ℕ} (h : a = b) :
bitvec a → bitvec b

Create a bitvector from another with a provably equal length.

Equations
source
def bitvec.append {m n : ℕ} :
bitvec m → bitvec n → bitvec (m + n)

bitvec specific version of vector.append

Equations

Shift operations

source
def bitvec.shl {n : ℕ} (x : bitvec n) (i : ℕ) :
bitvec 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
source
def bitvec.fill_shr {n : ℕ} (x : bitvec n) (i : ℕ) (fill : bool) :
bitvec 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
source
def bitvec.ushr {n : ℕ} (x : bitvec n) (i : ℕ) :
bitvec n

unsigned shift right

Equations
source
def bitvec.sshr {m : ℕ} :
bitvec m → ℕ → bitvec m

signed shift right

Equations

Bitwise operations

source
def bitvec.not {n : ℕ} :
bitvec n → bitvec n

bitwise not

Equations
source
def bitvec.and {n : ℕ} :
bitvec n → bitvec n → bitvec n

bitwise and

Equations
source
def bitvec.or {n : ℕ} :
bitvec n → bitvec n → bitvec n

bitwise or

Equations
source
def bitvec.xor {n : ℕ} :
bitvec n → bitvec n → bitvec n

bitwise xor

Equations

Arithmetic operators

source
def bitvec.xor3 (x y c : bool) :
bool

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

Equations
source
def bitvec.carry (x y c : bool) :
bool

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

Equations
source
def bitvec.neg {n : ℕ} (x : bitvec n) :
bitvec n

neg x is the two's complement of x.

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

Add with carry (no overflow)

Equations
source
def bitvec.add {n : ℕ} (x y : bitvec n) :
bitvec n

The sum of two bitvectors

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

Subtract with borrow

Equations
source
def bitvec.sub {n : ℕ} (x y : bitvec n) :
bitvec n

The difference of two bitvectors

Equations
source
@[instance]
def bitvec.has_zero {n : ℕ} :
has_zero (bitvec n)

Equations
source
@[instance]
def bitvec.has_one {n : ℕ} :
has_one (bitvec n)

Equations
source
@[instance]
def bitvec.has_add {n : ℕ} :
has_add (bitvec n)

Equations
source
@[instance]
def bitvec.has_sub {n : ℕ} :
has_sub (bitvec n)

Equations
source
@[instance]
def bitvec.has_neg {n : ℕ} :
has_neg (bitvec n)

Equations
source
def bitvec.mul {n : ℕ} (x y : bitvec n) :
bitvec n

The product of two bitvectors

Equations
source
@[instance]
def bitvec.has_mul {n : ℕ} :
has_mul (bitvec n)

Equations

Comparison operators

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

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

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

unsigned less-than proposition

Equations
source
def bitvec.ugt {n : ℕ} (x y : bitvec n) :
Prop

unsigned greater-than proposition

Equations
source
def bitvec.ule {n : ℕ} (x y : bitvec n) :
Prop

unsigned less-than-or-equal-to proposition

Equations
source
def bitvec.uge {n : ℕ} (x y : bitvec n) :
Prop

unsigned greater-than-or-equal-to proposition

Equations
source
def bitvec.sborrow {n : ℕ} :
bitvec n → bitvec n → bool

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

Equations
source
def bitvec.slt {n : ℕ} (x y : bitvec n) :
Prop

signed less-than proposition

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

signed greater-than proposition

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

signed less-than-or-equal-to proposition

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

signed greater-than-or-equal-to proposition

Equations

Conversion to nat and int

source
def bitvec.of_nat (n : ℕ) :
ℕ → bitvec n

Create a bitvector from a nat

Equations
source
def bitvec.of_int (n : ℕ) :
ℤ → bitvec n.succ

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

Equations
source
def bitvec.add_lsb (r : ℕ) (b : bool) :
ℕ

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

Equations
source
def bitvec.bits_to_nat (v : list bool) :
ℕ

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

Equations
source
def bitvec.to_nat {n : ℕ} (v : bitvec n) :
ℕ

Return the natural number encoded by the input bitvector

Equations
source
theorem bitvec.bits_to_nat_to_list {n : ℕ} (x : bitvec n) :
x.to_nat = bitvec.bits_to_nat (vector.to_list x)

source
theorem bitvec.to_nat_append {m : ℕ} (xs : bitvec m) (b : bool) :
bitvec.to_nat (vector.append xs (b::ᵥvector.nil)) = (xs.to_nat) * 2 + bitvec.to_nat (b::ᵥvector.nil)

source
theorem bitvec.bits_to_nat_to_bool (n : ℕ) :
bitvec.to_nat (to_bool (n % 2 = 1)::ᵥvector.nil) = n % 2

source
theorem bitvec.of_nat_succ {k n : ℕ} :
bitvec.of_nat k.succ n = vector.append (bitvec.of_nat k (n / 2)) (to_bool (n % 2 = 1)::ᵥvector.nil)

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

source
def bitvec.to_int {n : ℕ} :
bitvec n → ℤ

Return the integer encoded by the input bitvector

Equations

Miscellaneous instances

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

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

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

Equations