Documentation

Mathlib.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 (n : ℕ) :

Bitvec n is a Vector of Bool with length n.

Equations

Bitvec n = Vector Bool n

def Bitvec.zero (n : ℕ) :

Create a zero bitvector

Equations

Bitvec.zero n = Vector.replicate n false

def Bitvec.one (n : ℕ) :

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

Equations

Bitvec.one x = match x with | 0 => Vector.nil | Nat.succ n => Vector.append (Vector.replicate n false) (true ::ᵥ Vector.nil)

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 = match x with | { val := x, property := p } => { val := x, property := (_ : List.length x = b) }

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 false. If x.length < i then this will return the all-falses bitvector.

Equations

Bitvec.shl x i = Bitvec.cong (_ : n - i + min n i = n) (Vector.append (Vector.drop i x) (Vector.replicate (min n i) false))

def Bitvec.fillShr {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

Bitvec.fillShr x i fill = Bitvec.cong (_ : min n i + min (n - i) n = n) (Vector.append (Vector.replicate (min n i) fill) (Vector.take (n - i) x))

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

unsigned shift right

Equations

Bitvec.ushr x i = Bitvec.fillShr x i false

def Bitvec.sshr {m : ℕ} :

Bitvec m → ℕ → Bitvec m

signed shift right

Equations

Bitvec.sshr x x = match x, x, x with | 0, x, x_1 => Vector.nil | Nat.succ n, x, i => Vector.head x ::ᵥ Bitvec.fillShr (Vector.tail x) i (Vector.head x)

Bitwise operations #

def Bitvec.not {n : ℕ} (bv : Bitvec n) :

bitwise not

Equations

Bitvec.not bv = Vector.map not bv

def Bitvec.and {n : ℕ} :

Bitvec n → Bitvec n → Bitvec n

bitwise and

Equations

Bitvec.and = Vector.map₂ and

def Bitvec.or {n : ℕ} :

Bitvec n → Bitvec n → Bitvec n

bitwise or

Equations

Bitvec.or = Vector.map₂ or

def Bitvec.xor {n : ℕ} :

Bitvec n → Bitvec n → Bitvec n

bitwise xor

Equations

Bitvec.xor = Vector.map₂ xor

Arithmetic operators #

def Bitvec.xor3 (x : Bool) (y : Bool) (c : Bool) :

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

Equations

Bitvec.xor3 x y c = xor (xor x y) c

def Bitvec.carry (x : Bool) (y : Bool) (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)

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

neg x is the two's complement of x.

Equations

Bitvec.neg x = let f := fun y c => (y || c, xor y c); (Vector.mapAccumr f x false).snd

def Bitvec.adc {n : ℕ} (x : Bitvec n) (y : Bitvec n) (c : Bool) :

Bitvec (n + 1)

Add with carry (no overflow)

Equations

Bitvec.adc x y c = let f := fun x y c => (Bitvec.carry x y c, Bitvec.xor3 x y c); match Vector.mapAccumr₂ f x y c with | (c, z) => c ::ᵥ z

def Bitvec.add {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

The sum of two bitvectors

Equations

Bitvec.add x y = Vector.tail (Bitvec.adc x y false)

def Bitvec.sbb {n : ℕ} (x : Bitvec n) (y : Bitvec n) (b : Bool) :

Bool × Bitvec n

Subtract with borrow

Equations

Bitvec.sbb x y b = let f := fun x y c => (Bitvec.carry (!x) y c, Bitvec.xor3 x y c); Vector.mapAccumr₂ f x y b

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

The difference of two bitvectors

Equations

Bitvec.sub x y = (Bitvec.sbb x y false).snd

instance Bitvec.instZeroBitvec {n : ℕ} :

Zero (Bitvec n)

Equations

Bitvec.instZeroBitvec = { zero := Bitvec.zero n }

instance Bitvec.instOneBitvec {n : ℕ} :

Equations

Bitvec.instOneBitvec = { one := Bitvec.one n }

instance Bitvec.instAddBitvec {n : ℕ} :

Equations

Bitvec.instAddBitvec = { add := Bitvec.add }

instance Bitvec.instSubBitvec {n : ℕ} :

Equations

Bitvec.instSubBitvec = { sub := Bitvec.sub }

instance Bitvec.instNegBitvec {n : ℕ} :

Equations

Bitvec.instNegBitvec = { neg := Bitvec.neg }

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

The product of two bitvectors

Equations

Bitvec.mul x y = let f := fun r b => bif b then r + r + y else r + r; List.foldl f 0 (Vector.toList x)

instance Bitvec.instMulBitvec {n : ℕ} :

Equations

Bitvec.instMulBitvec = { mul := Bitvec.mul }

Comparison operators #

def Bitvec.uborrow {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

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

Equations

Bitvec.uborrow x y = (Bitvec.sbb x y false).fst

def Bitvec.Ult {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

unsigned less-than proposition

Equations

Bitvec.Ult x y = (Bitvec.uborrow x y = true)

def Bitvec.Ugt {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

unsigned greater-than proposition

Equations

Bitvec.Ugt x y = Bitvec.Ult y x

def Bitvec.Ule {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

unsigned less-than-or-equal-to proposition

Equations

Bitvec.Ule x y = ¬Bitvec.Ult y x

def Bitvec.Uge {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

unsigned greater-than-or-equal-to proposition

Equations

Bitvec.Uge x y = Bitvec.Ule y x

def Bitvec.sborrow {n : ℕ} :

Bitvec n → Bitvec n → Bool

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

Equations

One or more equations did not get rendered due to their size.

def Bitvec.Slt {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

signed less-than proposition

Equations

Bitvec.Slt x y = (Bitvec.sborrow x y = true)

def Bitvec.Sgt {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

signed greater-than proposition

Equations

Bitvec.Sgt x y = Bitvec.Slt y x

def Bitvec.Sle {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

signed less-than-or-equal-to proposition

Equations

Bitvec.Sle x y = ¬Bitvec.Slt y x

def Bitvec.Sge {n : ℕ} (x : Bitvec n) (y : Bitvec n) :

signed greater-than-or-equal-to proposition

Equations

Bitvec.Sge x y = Bitvec.Sle y x

Conversion to `nat` and `int` #

def Bitvec.ofNat (n : ℕ) :

ℕ → Bitvec n

Create a bitvector from a nat

Equations

Bitvec.ofNat 0 x = Vector.nil
Bitvec.ofNat (Nat.succ n) x = Vector.append (Bitvec.ofNat n (x / 2)) (decide (x % 2 = 1) ::ᵥ Vector.nil)

def Bitvec.ofInt (n : ℕ) :

ℤ → Bitvec (Nat.succ n)

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

Equations

Bitvec.ofInt x x = match x, x with | n, Int.ofNat m => false ::ᵥ Bitvec.ofNat n m | n, Int.negSucc m => true ::ᵥ Bitvec.not (Bitvec.ofNat n m)

def Bitvec.addLsb (r : ℕ) (b : Bool) :

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

Equations

Bitvec.addLsb r b = r + r + bif b then 1 else 0

def Bitvec.bitsToNat (v : List Bool) :

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

Equations

Bitvec.bitsToNat v = List.foldl Bitvec.addLsb 0 v

def Bitvec.toNat {n : ℕ} (v : Bitvec n) :

Return the natural number encoded by the input bitvector

Equations

Bitvec.toNat v = Bitvec.bitsToNat (Vector.toList v)

theorem Bitvec.bitsToNat_toList {n : ℕ} (x : Bitvec n) :

Bitvec.toNat x = Bitvec.bitsToNat (Vector.toList x)

theorem Bitvec.toNat_append {m : ℕ} (xs : Bitvec m) (b : Bool) :

Bitvec.toNat (Vector.append xs (b ::ᵥ Vector.nil)) = Bitvec.toNat xs * 2 + Bitvec.toNat (b ::ᵥ Vector.nil)

theorem Bitvec.bits_toNat_decide (n : ℕ) :

Bitvec.toNat (decide (n % 2 = 1) ::ᵥ Vector.nil) = n % 2

theorem Bitvec.ofNat_succ {k : ℕ} {n : ℕ} :

Bitvec.ofNat (Nat.succ k) n = Vector.append (Bitvec.ofNat k (n / 2)) (decide (n % 2 = 1) ::ᵥ Vector.nil)

theorem Bitvec.toNat_ofNat {k : ℕ} {n : ℕ} :

Bitvec.toNat (Bitvec.ofNat k n) = n % 2 ^ k

def Bitvec.toInt {n : ℕ} :

Bitvec n → ℤ

Return the integer encoded by the input bitvector

Equations

One or more equations did not get rendered due to their size.

Miscellaneous instances #

instance Bitvec.instReprBitvec (n : ℕ) :

Repr (Bitvec n)

Equations

Bitvec.instReprBitvec n = { reprPrec := fun b x => Std.Format.text (Bitvec.repr b) }

instance instDecidableUlt {n : ℕ} {x : Bitvec n} {y : Bitvec n} :

Decidable (Bitvec.Ult x y)

Equations

instDecidableUlt = decEq (Bitvec.uborrow x y) true

instance instDecidableUgt {n : ℕ} {x : Bitvec n} {y : Bitvec n} :

Decidable (Bitvec.Ugt x y)

Equations

instDecidableUgt = decEq (Bitvec.uborrow y x) true