# Bitwise operations using binary representation of integers #

## Definitions #

• bitwise operations for PosNum and Num,
• SNum, a type that represents integers as a bit string with a sign bit at the end,
• arithmetic operations for SNum.

Bitwise "or" for PosNum.

Equations
Instances For
instance PosNum.instOrOp :
Equations
@[simp]
theorem PosNum.lor_eq_or (p : PosNum) (q : PosNum) :
p.lor q = p ||| q

Bitwise "and" for PosNum.

Equations
Instances For
@[simp]
theorem PosNum.land_eq_and (p : PosNum) (q : PosNum) :
p.land q = p &&& q

Bitwise fun a b ↦ a && !b for PosNum. For example, ldiff 5 9 = 4:

 101
1001
----
100

Equations
Instances For

Bitwise "xor" for PosNum.

Equations
Instances For
@[simp]
theorem PosNum.lxor_eq_xor (p : PosNum) (q : PosNum) :
p.lxor q = p ^^^ q

a.testBit n is true 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 false.

Equations
Instances For
def PosNum.oneBits :
PosNum

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

Equations
• PosNum.one.oneBits x = [x]
• p.bit0.oneBits x = p.oneBits (x + 1)
• p.bit1.oneBits x = x :: p.oneBits (x + 1)
Instances For

Left-shift the binary representation of a PosNum.

Equations
• x.shiftl 0 = x
• x.shiftl n.succ = x.bit0.shiftl n
Instances For
@[simp]
theorem PosNum.shiftl_eq_shiftLeft (p : PosNum) (n : ) :
p.shiftl n = p <<< n
theorem PosNum.shiftl_succ_eq_bit0_shiftl (p : PosNum) (n : ) :
p <<< n.succ = (p <<< n).bit0

Right-shift the binary representation of a PosNum.

Equations
• x.shiftr 0 =
• PosNum.one.shiftr x = 0
• p.bit0.shiftr n.succ = p.shiftr n
• p.bit1.shiftr n.succ = p.shiftr n
Instances For
@[simp]
theorem PosNum.shiftr_eq_shiftRight (p : PosNum) (n : ) :
p.shiftr n = p >>> n
def Num.lor :

Bitwise "or" for Num.

Equations
Instances For
instance Num.instOrOp :
Equations
@[simp]
theorem Num.lor_eq_or (p : Num) (q : Num) :
p.lor q = p ||| q
def Num.land :

Bitwise "and" for Num.

Equations
Instances For
instance Num.instAndOp :
Equations
@[simp]
theorem Num.land_eq_and (p : Num) (q : Num) :
p.land q = p &&& q
def Num.ldiff :

Bitwise fun a b ↦ a && !b for Num. For example, ldiff 5 9 = 4:

 101
1001
----
100

Equations
• x✝.ldiff x = match x✝, x with | Num.zero, x => 0 | p, Num.zero => p | , => p.ldiff q
Instances For
def Num.lxor :

Bitwise "xor" for Num.

Equations
Instances For
instance Num.instXor :
Equations
@[simp]
theorem Num.lxor_eq_xor (p : Num) (q : Num) :
p.lxor q = p ^^^ q
def Num.shiftl :
NumNum

Left-shift the binary representation of a Num.

Equations
Instances For
Equations
@[simp]
theorem Num.shiftl_eq_shiftLeft (p : Num) (n : ) :
p.shiftl n = p <<< n
def Num.shiftr :
NumNum

Right-shift the binary representation of a Num.

Equations
• x✝.shiftr x = match x✝, x with | Num.zero, x => 0 | , n => p >>> n
Instances For
Equations
@[simp]
theorem Num.shiftr_eq_shiftRight (p : Num) (n : ) :
p.shiftr n = p >>> n
def Num.testBit :
Num

a.testBit n is true 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 false.

Equations
• x✝.testBit x = match x✝, x with | Num.zero, x => false | , n => p.testBit n
Instances For
def Num.oneBits :
Num

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

Equations
• x.oneBits = match x with | Num.zero => [] | => p.oneBits 0
Instances For
inductive NzsNum :

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

• msb:
• bit: Bool

Add a bit at the end of a NzsNum.

Instances For
Equations
inductive SNum :

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 true)))) -13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false))))

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 false -1 = ..1111111(base 2) = zero true

• zero:
• nz:
Instances For
Equations
Equations
instance instZeroSNum :
Equations
instance instOneNzsNum :
Equations
instance instOneSNum :
Equations
Equations
Equations

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

Add a bit at the end of a NzsNum.

Equations
Instances For

Sign of a NzsNum.

Equations
• ().sign = !b
• ().sign = p.sign
Instances For
@[match_pattern]

Bitwise not for NzsNum.

Equations
Instances For

Bitwise not for NzsNum.

Equations
Instances For

Add an inactive bit at the end of a NzsNum. This mimics PosNum.bit0.

Equations
Instances For

Add an active bit at the end of a NzsNum. This mimics PosNum.bit1.

Equations
Instances For

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

Equations
• x.head = match x with | => b | => b
Instances For

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

Equations
Instances For
def SNum.sign :

Sign of a SNum.

Equations
• x.sign = match x with | => z | => p.sign
Instances For
@[match_pattern]
def SNum.not :

Bitwise not for SNum.

Equations
Instances For

Bitwise not for SNum.

Equations
Instances For
@[match_pattern]
def SNum.bit :
Bool

Add a bit at the end of a SNum. This mimics NzsNum.bit.

Equations
Instances For

Add a bit at the end of a SNum. This mimics NzsNum.bit.

Equations
Instances For
def SNum.bit0 :

Add an inactive bit at the end of a SNum. This mimics ZNum.bit0.

Equations
Instances For
def SNum.bit1 :

Add an active bit at the end of a SNum. This mimics ZNum.bit1.

Equations
Instances For
theorem SNum.bit_zero (b : Bool) :
SNum.bit b () =
def NzsNum.drec' {C : SNumSort u_1} (z : (b : Bool) → C ()) (s : (b : Bool) → (p : SNum) → C pC (SNum.bit b p)) (p : NzsNum) :
C ()

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

Equations
Instances For

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

Equations
• x.head = match x with | => z | => p.head
Instances For
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
• x.tail = match x with | => | => p.tail
Instances For
def SNum.drec' {C : SNumSort u_1} (z : (b : Bool) → C ()) (s : (b : Bool) → (p : SNum) → C pC (SNum.bit b p)) (p : SNum) :
C p

A dependent induction principle for SNum which avoids relying on NzsNum.

Equations
Instances For
def SNum.rec' {α : Sort u_1} (z : Boolα) (s : BoolSNumαα) :
SNumα

An induction principle for SNum which avoids relying on NzsNum.

Equations
Instances For
def SNum.testBit :

SNum.testBit n a is true 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 false.

Equations
Instances For
def SNum.succ :

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

Equations
Instances For
def SNum.pred :

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

Equations
Instances For
def SNum.neg (n : SNum) :

The opposite of a SNum.

Equations
• n.neg = n.not.succ
Instances For
instance SNum.instNeg :
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
Instances For
def SNum.bits :
SNum(n : ) →

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

Equations
• x.bits 0 = Vector.nil
• x.bits n.succ = x.head ::ᵥ x.tail.bits n
Instances For
SNumSNum

SNum.cAdd n m a is n + m + a (where a should be read as either 0 or 1). a represents a carry bit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SNum.add (a : SNum) (b : SNum) :

Add two SNums.

Equations
Instances For
Equations
def SNum.sub (a : SNum) (b : SNum) :

Subtract two SNums.

Equations
• a.sub b = a + -b
Instances For
instance SNum.instSub :
Equations
def SNum.mul (a : SNum) :

Multiply two SNums.

Equations
• a.mul = SNum.rec' (fun (b : Bool) => bif b then -a else 0) fun (b : Bool) (x IH : SNum) => bif b then IH.bit0 + a else IH.bit0
Instances For
instance SNum.instMul :
Equations