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

bitvec n = vector bool n

@[protected, reducible]

def bitvec.zero (n : ℕ) :

Create a zero bitvector

Equations

bitvec.zero n = vector.repeat bool.ff n

@[protected, reducible]

def bitvec.one (n : ℕ) :

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

Equations

bitvec.one n.succ = (vector.repeat bool.ff n).append (bool.tt ::ᵥ vector.nil)
bitvec.one 0 = vector.nil

@[protected]

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

bitvec a → bitvec b

Create a bitvector from another with a provably equal length.

Equations

bitvec.cong h ⟨x, p⟩ = ⟨x, _⟩

def bitvec.append {m n : ℕ} :

bitvec m → bitvec n → bitvec (m + n)

bitvec specific version of vector.append

Equations

bitvec.append = vector.append

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

x.shl i = bitvec.cong _ ((vector.drop i x).append (vector.repeat bool.ff (linear_order.min n i)))

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

x.fill_shr i fill = bitvec.cong _ ((vector.repeat fill (linear_order.min n i)).append (vector.take (n - i) x))

def bitvec.ushr {n : ℕ} (x : bitvec n) (i : ℕ) :

unsigned shift right

Equations

x.ushr i = x.fill_shr i bool.ff

def bitvec.sshr {m : ℕ} :

bitvec m → ℕ → bitvec m

signed shift right

Equations

x.sshr i = vector.head x ::ᵥ bitvec.fill_shr (vector.tail x) i (vector.head x)
_x.sshr _x_1 = vector.nil

Bitwise operations #

def bitvec.not {n : ℕ} :

bitvec n → bitvec n

bitwise not

Equations

bitvec.not = vector.map bnot

def bitvec.and {n : ℕ} :

bitvec n → bitvec n → bitvec n

bitwise and

Equations

bitvec.and = vector.map₂ band

def bitvec.or {n : ℕ} :

bitvec n → bitvec n → bitvec n

bitwise or

Equations

bitvec.or = vector.map₂ bor

def bitvec.xor {n : ℕ} :

bitvec n → bitvec n → bitvec n

bitwise xor

Equations

bitvec.xor = vector.map₂ bxor

Arithmetic operators #

@[protected]

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

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

Equations

bitvec.xor3 x y c = bxor (bxor x y) c

@[protected]

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

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

Equations

bitvec.carry x y c = x && y || x && c || y && c

@[protected]

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

neg x is the two's complement of x.

Equations

x.neg = let f : bool → bool → bool × bool := λ (y c : bool), (y || c, bxor y c) in (vector.map_accumr f x bool.ff).snd

def bitvec.adc {n : ℕ} (x y : bitvec n) (c : bool) :

bitvec (n + 1)

Add with carry (no overflow)

Equations

x.adc y c = let f : bool → bool → bool → bool × bool := λ (x y c : bool), (bitvec.carry x y c, bitvec.xor3 x y c) in bitvec.adc._match_1 (vector.map_accumr₂ f x 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

x.add y = vector.tail (x.adc y bool.ff)

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

bool × bitvec n

Subtract with borrow

Equations

x.sbb y b = let f : bool → bool → bool → bool × bool := λ (x y c : bool), (bitvec.carry (!x) y c, bitvec.xor3 x y c) in vector.map_accumr₂ f x y b

@[protected]

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

The difference of two bitvectors

Equations

x.sub y = (x.sbb y bool.ff).snd

@[protected, instance]

def bitvec.has_zero {n : ℕ} :

has_zero (bitvec n)

Equations

bitvec.has_zero = {zero := bitvec.zero n}

@[protected, instance]

def bitvec.has_one {n : ℕ} :

has_one (bitvec n)

Equations

bitvec.has_one = {one := bitvec.one n}

@[protected, instance]

def bitvec.has_add {n : ℕ} :

has_add (bitvec n)

Equations

bitvec.has_add = {add := bitvec.add n}

@[protected, instance]

def bitvec.has_sub {n : ℕ} :

has_sub (bitvec n)

Equations

bitvec.has_sub = {sub := bitvec.sub n}

@[protected, instance]

def bitvec.has_neg {n : ℕ} :

has_neg (bitvec n)

Equations

bitvec.has_neg = {neg := bitvec.neg n}

@[protected]

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

The product of two bitvectors

Equations

x.mul y = let f : bitvec n → bool → bitvec n := λ (r : bitvec n) (b : bool), cond b (r + r + y) (r + r) in list.foldl f 0 (vector.to_list x)

@[protected, instance]

def bitvec.has_mul {n : ℕ} :

has_mul (bitvec n)

Equations

bitvec.has_mul = {mul := bitvec.mul n}

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

x.uborrow y = (x.sbb y bool.ff).fst

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

Prop

unsigned less-than proposition

Equations

x.ult y = ↥(x.uborrow y)

Instances for bitvec.ult

bitvec.ult.decidable

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

Prop

unsigned greater-than proposition

Equations

x.ugt y = y.ult x

Instances for bitvec.ugt

bitvec.ugt.decidable

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

Prop

unsigned less-than-or-equal-to proposition

Equations

x.ule y = ¬y.ult x

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

Prop

unsigned greater-than-or-equal-to proposition

Equations

x.uge y = y.ule x

def bitvec.sborrow {n : ℕ} :

bitvec n → bitvec n → bool

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

Equations

x.sborrow y = bitvec.sborrow._match_1 n x y (vector.head x, vector.head y)
_x.sborrow _x_1 = bool.ff
bitvec.sborrow._match_1 n x y (bool.tt, bool.tt) = bitvec.uborrow (vector.tail x) (vector.tail y)
bitvec.sborrow._match_1 n x y (bool.tt, bool.ff) = bool.tt
bitvec.sborrow._match_1 n x y (bool.ff, bool.tt) = bool.ff
bitvec.sborrow._match_1 n x y (bool.ff, bool.ff) = bitvec.uborrow (vector.tail x) (vector.tail y)

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

Prop

signed less-than proposition

Equations

x.slt y = ↥(x.sborrow y)

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

Prop

signed greater-than proposition

Equations

x.sgt y = y.slt x

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

Prop

signed less-than-or-equal-to proposition

Equations

x.sle y = ¬y.slt x

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

Prop

signed greater-than-or-equal-to proposition

Equations

x.sge y = y.sle x

Conversion to `nat` and `int` #

@[protected]

def bitvec.of_nat (n : ℕ) :

ℕ → bitvec n

Create a bitvector from a nat

Equations

bitvec.of_nat n.succ x = vector.append (bitvec.of_nat n (x / 2)) (decidable.to_bool (x % 2 = 1) ::ᵥ vector.nil)
bitvec.of_nat 0 x = vector.nil

@[protected]

def bitvec.of_int (n : ℕ) :

ℤ → bitvec n.succ

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

Equations

bitvec.of_int n -[1+ m] = bool.tt ::ᵥ (bitvec.of_nat n m).not
bitvec.of_int n (int.of_nat m) = bool.ff ::ᵥ bitvec.of_nat n m

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

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

Equations

bitvec.add_lsb r b = r + r + cond b 1 0

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

bitvec.bits_to_nat v = list.foldl bitvec.add_lsb 0 v

@[protected]

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

Return the natural number encoded by the input bitvector

Equations

v.to_nat = bitvec.bits_to_nat (vector.to_list v)

theorem bitvec.bits_to_nat_to_list {n : ℕ} (x : bitvec n) :

x.to_nat = bitvec.bits_to_nat (vector.to_list x)

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)

theorem bitvec.bits_to_nat_to_bool (n : ℕ) :

bitvec.to_nat (decidable.to_bool (n % 2 = 1) ::ᵥ vector.nil) = n % 2

theorem bitvec.of_nat_succ {k n : ℕ} :

bitvec.of_nat k.succ n = vector.append (bitvec.of_nat k (n / 2)) (decidable.to_bool (n % 2 = 1) ::ᵥ vector.nil)

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

v.to_int = cond (vector.head v) -[1+ (bitvec.not (vector.tail v)).to_nat] (int.of_nat (bitvec.to_nat (vector.tail v)))
_x.to_int = 0

Miscellaneous instances #

@[protected, instance]

def bitvec.has_repr (n : ℕ) :

has_repr (bitvec n)

Equations

bitvec.has_repr n = {repr := repr n}

@[protected, instance]

def bitvec.ult.decidable {n : ℕ} {x y : bitvec n} :

decidable (x.ult y)

Equations

bitvec.ult.decidable = bool.decidable_eq (x.uborrow y) bool.tt

@[protected, instance]

def bitvec.ugt.decidable {n : ℕ} {x y : bitvec n} :

decidable (x.ugt y)

Equations

bitvec.ugt.decidable = bool.decidable_eq (y.uborrow x) bool.tt