data.num.bitwise

# Bitwise operations using binary representation of integers

## Definitions

• bitwise operations for pos_num and num,
• snum, a type that represents integers as a bit string with a sign bit at the end,
• arithmetic operations for snum.
def pos_num.lor  :

Bitwise "or" for pos_num.

Equations
def pos_num.land  :

Bitwise "and" for pos_num.

Equations
def pos_num.ldiff  :

Bitwise λ a b, a && !b for pos_num. For example, ldiff 5 9 = 4:

101


1001

100

Equations
def pos_num.lxor  :

Bitwise "xor" for pos_num.

Equations

a.test_bit n is tt iff the n-th bit (starting from the LSB) in the binary representation of a is active. If the size of a is less than n, this evaluates to ff.

Equations
def pos_num.one_bits  :
pos_num

n.one_bits 0 is the list of indices of active bits in the binary representation of n.

Equations
def pos_num.shiftl  :
pos_num

Left-shift the binary representation of a pos_num.

Equations
def pos_num.shiftr  :
pos_numnum

Right-shift the binary representation of a pos_num.

Equations
def num.lor  :
num

Bitwise "or" for num.

Equations
def num.land  :
num

Bitwise "and" for num.

Equations
def num.ldiff  :
num

Bitwise λ a b, a && !b for num. For example, ldiff 5 9 = 4:

101


1001

100

Equations
def num.lxor  :
num

Bitwise "xor" for num.

Equations
def num.shiftl  :
numnum

Left-shift the binary representation of a num.

Equations
def num.shiftr  :
numnum

Right-shift the binary representation of a pos_num.

Equations
def num.test_bit  :
num

a.test_bit n is tt iff the n-th bit (starting from the LSB) in the binary representation of a is active. If the size of a is less than n, this evaluates to ff.

Equations
def num.one_bits  :
num

n.one_bits is the list of indices of active bits in the binary representation of n.

Equations
@[instance]
meta def nzsnum.has_reflect  :

@[instance]

inductive nzsnum  :
Type
• msb :
• bit : bool

This is a nonzero (and "non minus one") version of snum. See the documentation of snum for more details.

@[instance]

@[instance]
meta def snum.has_reflect  :

inductive snum  :
Type
• zero :
• nz :

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

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations

The snum representation uses a bit string, essentially a list of 0 (ff) and 1 (tt) bits, and the negation of the MSB is sign-extended to all higher bits.

def nzsnum.sign  :

Sign of a nzsnum.

Equations
def nzsnum.not  :

Bitwise not for nzsnum.

Equations
def nzsnum.bit0  :

Add an inactive bit at the end of a nzsnum. This mimics pos_num.bit0.

Equations
def nzsnum.bit1  :

Add an active bit at the end of a nzsnum. This mimics pos_num.bit1.

Equations

The head of a nzsnum is the boolean value of its LSB.

Equations
def nzsnum.tail  :

The tail of a nzsnum is the snum obtained by removing the LSB. Edge cases: tail 1 = 0 and tail (-2) = -1.

Equations
def snum.sign  :

Sign of a snum.

Equations
def snum.not  :

Bitwise not for snum.

Equations
def snum.bit  :
bool

Add a bit at the end of a snum. This mimics nzsnum.bit.

Equations
def snum.bit0  :

Add an inactive bit at the end of a snum. This mimics znum.bit0.

Equations
def snum.bit1  :

Add an active bit at the end of a snum. This mimics znum.bit1.

Equations
theorem snum.bit_zero (b : bool) :
b :: =

theorem snum.bit_one (b : bool) :

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

A dependent induction principle for nzsnum, with base cases 0 : snum and (-1) : snum.

Equations

The head of a snum is the boolean value of its LSB.

Equations
def snum.tail  :

The tail of a snum is obtained by removing the LSB. Edge cases: tail 1 = 0, tail (-2) = -1, tail 0 = 0 and tail (-1) = -1.

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

A dependent induction principle for snum which avoids relying on nzsnum.

Equations
def snum.rec' {α : Sort u_1} :
(bool → α)(boolsnumα → α)snum → α

An induction principle for snum which avoids relying on nzsnum.

Equations
• s = s
def snum.test_bit  :

snum.test_bit n a is tt iff the n-th bit (starting from the LSB) of a is active. If the size of a is less than n, this evaluates to ff.

Equations
def snum.succ  :

The successor of a snum (i.e. the operation adding one).

Equations
def snum.pred  :

The predecessor of a snum (i.e. the operation of removing one).

Equations
def snum.neg  :

The opposite of a snum.

Equations
@[instance]

Equations
boolbool

snum.czadd a b n is n + a - b (where a and b should be read as either 0 or 1). This is useful to implement the carry system in cadd.

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

a.bits n is the vector of the n first bits of a (starting from the LSB).

Equations
snumsnum

Equations
snum

Add two snums.

Equations
@[instance]

Equations
def snum.sub  :
snum

Substract two snums.

Equations
@[instance]

Equations
def snum.mul  :
snum

Multiply two snums.

Equations
@[instance]

Equations