mathlib docs: core.data.bitvec

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

source

def bitvec.add {n : ℕ} :

bitvec n → bitvec n → bitvec n

Equations

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

source

def bitvec.sbb {n : ℕ} :

bitvec n → bitvec n → bool → bool × bitvec n

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

source

def bitvec.sub {n : ℕ} :

bitvec n → bitvec n → bitvec n

Equations

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

source

@[instance]

def bitvec.has_zero {n : ℕ} :

has_zero (bitvec n)

Equations

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

source

@[instance]

def bitvec.has_one {n : ℕ} :

has_one (bitvec n)

Equations

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

source

@[instance]

def bitvec.has_add {n : ℕ} :

has_add (bitvec n)

Equations

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

source

@[instance]

def bitvec.has_sub {n : ℕ} :

has_sub (bitvec n)

Equations

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

source

@[instance]

def bitvec.has_neg {n : ℕ} :

has_neg (bitvec n)

Equations

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

source

def bitvec.mul {n : ℕ} :

bitvec n → bitvec n → bitvec n

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)

source

@[instance]

def bitvec.has_mul {n : ℕ} :

has_mul (bitvec n)

Equations

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

source

def bitvec.uborrow {n : ℕ} :

bitvec n → bitvec n → bool

Equations

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

source

def bitvec.ult {n : ℕ} :

bitvec n → bitvec n → Prop

Equations

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

source

def bitvec.ugt {n : ℕ} :

bitvec n → bitvec n → Prop

Equations

x.ugt y = y.ult x

source

def bitvec.ule {n : ℕ} :

bitvec n → bitvec n → Prop

Equations

x.ule y = ¬y.ult x

source

def bitvec.uge {n : ℕ} :

bitvec n → bitvec n → Prop

Equations

x.uge y = y.ule x

source

def bitvec.sborrow {n : ℕ} :

bitvec n → bitvec n → bool

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)

source

def bitvec.slt {n : ℕ} :

bitvec n → bitvec n → Prop

Equations

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

source

def bitvec.sgt {n : ℕ} :

bitvec n → bitvec n → Prop

Equations

x.sgt y = y.slt x

source

def bitvec.sle {n : ℕ} :

bitvec n → bitvec n → Prop

Equations

x.sle y = ¬y.slt x

source

def bitvec.sge {n : ℕ} :

bitvec n → bitvec n → Prop

Equations

x.sge y = y.sle x

source

def bitvec.of_nat (n : ℕ) :

ℕ → bitvec n

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

source

def bitvec.of_int (n : ℕ) :

ℤ → bitvec n.succ

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

source

def bitvec.add_lsb :

ℕ → bool → ℕ

Equations

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

source

def bitvec.bits_to_nat :

list bool → ℕ

Equations

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

source

def bitvec.to_nat {n : ℕ} :

bitvec n → ℕ

Equations

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

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 (decidable.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)) (decidable.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 → ℤ

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

source

@[instance]

def bitvec.has_repr (n : ℕ) :

has_repr (bitvec n)

Equations

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

source

@[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

source

@[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

mathlib documentation

core.data.bitvec

General documentation

Additional documentation

Library

mathlib documentation

core.​data.​bitvec

General documentation

Additional documentation

Library

core.data.bitvec