mathlib docs: data.num.bitwise

Alternative representation of integers using a sign bit at the end. The convention on sign here is to have the argument to msb denote the sign of the MSB itself, with all higher bits set to the negation of this sign. The result is interpreted in two's complement.

13  = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb tt))))
-13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb ff))))

As with num, a special case must be added for zero, which has no msb, but by two's complement symmetry there is a second special case for -1. Here the bool field indicates the sign of the number.

0  = ..0000000(base 2) = zero ff
-1 = ..1111111(base 2) = zero tt

source

@[instance]

def snum.has_coe :

has_coe nzsnum snum

Equations

snum.has_coe = {coe := snum.nz}

source

@[instance]

def snum.has_zero :

has_zero snum

Equations

snum.has_zero = {zero := snum.zero ff}

source

@[instance]

def nzsnum.has_one :

has_one nzsnum

Equations

nzsnum.has_one = {one := nzsnum.msb tt}

source

@[instance]

def snum.has_one :

has_one snum

Equations

snum.has_one = {one := snum.nz 1}

source

@[instance]

def nzsnum.inhabited :

inhabited nzsnum

Equations

nzsnum.inhabited = {default := 1}

source

@[instance]

def snum.inhabited :

inhabited snum

Equations

snum.inhabited = {default := 0}

source

def nzsnum.sign (a : nzsnum) :

bool

Equations

(b :: p).sign = p.sign
(nzsnum.msb b).sign = !b

source

def nzsnum.not (a : nzsnum) :

nzsnum

Equations

(~b :: p) = !b :: ~p
(~nzsnum.msb b) = nzsnum.msb (!b)

source

def nzsnum.bit0 (a : nzsnum) :

nzsnum

Equations

nzsnum.bit0 = nzsnum.bit ff

source

def nzsnum.bit1 (a : nzsnum) :

nzsnum

Equations

nzsnum.bit1 = nzsnum.bit tt

source

def nzsnum.head (a : nzsnum) :

bool

Equations

(b :: p).head = b
(nzsnum.msb b).head = b

source

def nzsnum.tail (a : nzsnum) :

snum

Equations

(b :: p).tail = ↑p
(nzsnum.msb b).tail = snum.zero (!b)

source

def snum.sign (a : snum) :

bool

Equations

(snum.nz p).sign = p.sign
(snum.zero z).sign = z

source

def snum.not (a : snum) :

snum

Equations

(~snum.nz p) = ↑~p
(~snum.zero z) = snum.zero (!z)

source

def snum.bit (a : bool) (a_1 : snum) :

snum

Equations

b :: snum.nz p = ↑(b :: p)
b :: snum.zero z = ite (b = z) (snum.zero b) ↑(nzsnum.msb b)

source

def snum.bit0 (a : snum) :

snum

Equations

snum.bit0 = snum.bit ff

source

def snum.bit1 (a : snum) :

snum

Equations

snum.bit1 = snum.bit tt

source

theorem snum.bit_zero (b : bool) :

b :: snum.zero b = snum.zero b

source

theorem snum.bit_one (b : bool) :

b :: snum.zero (!b) = ↑(nzsnum.msb b)

source

def nzsnum.drec' {C : snum → Sort u_1} (z : Π (b : bool), C (snum.zero b)) (s : Π (b : bool) (p : snum), C p → C (b :: p)) (p : nzsnum) :

C ↑p

Equations

nzsnum.drec' z s (b :: p) = s b ↑p (nzsnum.drec' z s p)
nzsnum.drec' z s (nzsnum.msb b) = _.mpr (s b (snum.zero (!b)) (z (!b)))

source

def snum.head (a : snum) :

bool

Equations

(snum.nz p).head = p.head
(snum.zero z).head = z

source

def snum.tail (a : snum) :

snum

Equations

(snum.nz p).tail = p.tail
(snum.zero z).tail = snum.zero z

source

def snum.drec' {C : snum → Sort u_1} (z : Π (b : bool), C (snum.zero b)) (s : Π (b : bool) (p : snum), C p → C (b :: p)) (p : snum) :

C p

Equations

snum.drec' z s (snum.nz p) = nzsnum.drec' z s p
snum.drec' z s (snum.zero b) = z b

source

def snum.rec' {α : Sort u_1} (z : bool → α) (s : bool → snum → α → α) (a : snum) :

α

Equations

snum.rec' z s = snum.drec' z s

source

def snum.test_bit (a : ℕ) (a_1 : snum) :

bool

Equations

snum.test_bit (n + 1) p = snum.test_bit n p.tail
snum.test_bit 0 p = p.head

source

def snum.succ (a : snum) :

snum

Equations

snum.succ = snum.rec' (λ (b : bool), cond b 0 1) (λ (b : bool) (p succp : snum), cond b (ff :: succp) (tt :: p))

source

def snum.pred (a : snum) :

snum

Equations

snum.pred = snum.rec' (λ (b : bool), cond b (~1) (~0)) (λ (b : bool) (p predp : snum), cond b (ff :: p) (tt :: predp))

source

def snum.neg (n : snum) :

snum

Equations

n.neg = (~n).succ

source

@[instance]

def snum.has_neg :

has_neg snum

Equations

snum.has_neg = {neg := snum.neg}

source

def snum.czadd (a a_1 : bool) (a_2 : snum) :

snum

Equations

source

def snum.bits (a : snum) (n : ℕ) :

vector bool n

Equations

p.bits (n + 1) = p.head :: p.tail.bits n
p.bits 0 = vector.nil

source

def snum.cadd (a a_1 : snum) (a_2 : bool) :

snum

Equations

snum.cadd = snum.rec' (λ (a : bool) (p : snum) (c : bool), snum.czadd c a p) (λ (a : bool) (p : snum) (IH : snum → bool → snum), snum.rec' (λ (b c : bool), snum.czadd c b (a :: p)) (λ (b : bool) (q : snum) (_x : bool → snum) (c : bool), bitvec.xor3 a b c :: IH q (bitvec.carry a b c)))

source

def snum.add (a b : snum) :

snum

Equations

a.add b = a.cadd b ff

source

@[instance]

def snum.has_add :

has_add snum

Equations

snum.has_add = {add := snum.add}

source

def snum.sub (a b : snum) :

snum

Equations

a.sub b = a + -b

source

@[instance]

def snum.has_sub :

has_sub snum

Equations

snum.has_sub = {sub := snum.sub}

source

def snum.mul (a a_1 : snum) :

snum

Equations

a.mul = snum.rec' (λ (b : bool), cond b (-a) 0) (λ (b : bool) (q IH : snum), cond b (IH.bit0 + a) IH.bit0)

source

@[instance]

def snum.has_mul :

has_mul snum

Equations

snum.has_mul = {mul := snum.mul}