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.

ink

def PosNum.lor : PosNum → PosNum → PosNum

Bitwise "or" for PosNum.

Equations

• PosNum.lor PosNum.one (PosNum.bit0 q) = PosNum.bit1 q
• PosNum.lor PosNum.one x = x
• PosNum.lor (PosNum.bit0 p) PosNum.one = PosNum.bit1 p
• PosNum.lor x PosNum.one = x
• PosNum.lor (PosNum.bit0 p) (PosNum.bit0 q) = PosNum.bit0 (PosNum.lor p q)
• PosNum.lor (PosNum.bit0 p) (PosNum.bit1 q) = PosNum.bit1 (PosNum.lor p q)
• PosNum.lor (PosNum.bit1 p) (PosNum.bit0 q) = PosNum.bit1 (PosNum.lor p q)
• PosNum.lor (PosNum.bit1 p) (PosNum.bit1 q) = PosNum.bit1 (PosNum.lor p q)

ink

def PosNum.land : PosNum → PosNum → Num

Bitwise "and" for PosNum.

Equations

• PosNum.land PosNum.one (PosNum.bit0 q) = 0
• PosNum.land PosNum.one x = 1
• PosNum.land (PosNum.bit0 p) PosNum.one = 0
• PosNum.land x PosNum.one = 1
• PosNum.land (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.land p q)
• PosNum.land (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit0 (PosNum.land p q)
• PosNum.land (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit0 (PosNum.land p q)
• PosNum.land (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit1 (PosNum.land p q)

ink

def PosNum.ldiff : PosNum → PosNum → Num

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

 101
1001
----
 100

Equations

• PosNum.ldiff PosNum.one (PosNum.bit0 a) = 1
• PosNum.ldiff PosNum.one x = 0
• PosNum.ldiff (PosNum.bit0 p) PosNum.one = Num.pos (PosNum.bit0 p)
• PosNum.ldiff (PosNum.bit1 p) PosNum.one = Num.pos (PosNum.bit0 p)
• PosNum.ldiff (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.ldiff p q)
• PosNum.ldiff (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit0 (PosNum.ldiff p q)
• PosNum.ldiff (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit1 (PosNum.ldiff p q)
• PosNum.ldiff (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit0 (PosNum.ldiff p q)

ink

def PosNum.lxor : PosNum → PosNum → Num

Bitwise "xor" for PosNum.

Equations

• PosNum.lxor PosNum.one PosNum.one = 0
• PosNum.lxor PosNum.one (PosNum.bit0 q) = Num.pos (PosNum.bit1 q)
• PosNum.lxor PosNum.one (PosNum.bit1 q) = Num.pos (PosNum.bit0 q)
• PosNum.lxor (PosNum.bit0 p) PosNum.one = Num.pos (PosNum.bit1 p)
• PosNum.lxor (PosNum.bit1 p) PosNum.one = Num.pos (PosNum.bit0 p)
• PosNum.lxor (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.lxor p q)
• PosNum.lxor (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit1 (PosNum.lxor p q)
• PosNum.lxor (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit1 (PosNum.lxor p q)
• PosNum.lxor (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit0 (PosNum.lxor p q)

ink

def PosNum.testBit : PosNum → ℕ → Bool

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

• PosNum.testBit PosNum.one 0 = true
• PosNum.testBit PosNum.one x = false
• PosNum.testBit (PosNum.bit0 a) 0 = false
• PosNum.testBit (PosNum.bit0 p) (Nat.succ n) = PosNum.testBit p n
• PosNum.testBit (PosNum.bit1 a) 0 = true
• PosNum.testBit (PosNum.bit1 p) (Nat.succ n) = PosNum.testBit p n

ink

def PosNum.oneBits : PosNum → ℕ → List ℕ

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

Equations

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

ink

def PosNum.shiftl : PosNum → ℕ → PosNum

Left-shift the binary representation of a PosNum.

Equations

• PosNum.shiftl x 0 = x
• PosNum.shiftl x (Nat.succ n) = PosNum.shiftl (PosNum.bit0 x) n

ink

theorem PosNum.shiftl_succ_eq_bit0_shiftl (p : PosNum) (n : ℕ) : PosNum.shiftl p (Nat.succ n) = PosNum.bit0 (PosNum.shiftl p n)

ink

def PosNum.shiftr : PosNum → ℕ → Num

Right-shift the binary representation of a PosNum.

Equations

• PosNum.shiftr x 0 = Num.pos x
• PosNum.shiftr PosNum.one x = 0
• PosNum.shiftr (PosNum.bit0 p) (Nat.succ n) = PosNum.shiftr p n
• PosNum.shiftr (PosNum.bit1 p) (Nat.succ n) = PosNum.shiftr p n

ink

def Num.lor : Num → Num → Num

Bitwise "or" for Num.

Equations

• Num.lor x x = match x, x with | Num.zero, q => q | p, Num.zero => p | Num.pos p, Num.pos q => Num.pos (PosNum.lor p q)

ink

def Num.land : Num → Num → Num

Bitwise "and" for Num.

Equations

• Num.land x x = match x, x with | Num.zero, x => 0 | x, Num.zero => 0 | Num.pos p, Num.pos q => PosNum.land p q

ink

def Num.ldiff : Num → Num → Num

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

 101
1001
----
 100

Equations

• Num.ldiff x x = match x, x with | Num.zero, x => 0 | p, Num.zero => p | Num.pos p, Num.pos q => PosNum.ldiff p q

ink

def Num.lxor : Num → Num → Num

Bitwise "xor" for Num.

Equations

• Num.lxor x x = match x, x with | Num.zero, q => q | p, Num.zero => p | Num.pos p, Num.pos q => PosNum.lxor p q

ink

def Num.shiftl : Num → ℕ → Num

Left-shift the binary representation of a Num.

Equations

• Num.shiftl x x = match x, x with | Num.zero, x => 0 | Num.pos p, n => Num.pos (PosNum.shiftl p n)

ink

def Num.shiftr : Num → ℕ → Num

Right-shift the binary representation of a Num.

Equations

• Num.shiftr x x = match x, x with | Num.zero, x => 0 | Num.pos p, n => PosNum.shiftr p n

ink

def Num.testBit : Num → ℕ → Bool

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

• Num.testBit x x = match x, x with | Num.zero, x => false | Num.pos p, n => PosNum.testBit p n

ink

def Num.oneBits : Num → List ℕ

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

Equations

• Num.oneBits x = match x with | Num.zero => [] | Num.pos p => PosNum.oneBits p 0

ink

inductive NzsNum : Type

• msb: Bool → NzsNum

• Add a bit at the end of a NzsNum.

  bit: Bool → NzsNum → NzsNum

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

ink

instance instDecidableEqNzsNum : DecidableEq NzsNum

Equations

• instDecidableEqNzsNum = decEqNzsNum✝

ink

inductive SNum : Type

• zero: Bool → SNum
• nz: NzsNum → 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

ink

instance instDecidableEqSNum : DecidableEq SNum

Equations

• instDecidableEqSNum = decEqSNum✝

ink

instance instCoeNzsNumSNum : Coe NzsNum SNum

Equations

• instCoeNzsNumSNum = { coe := SNum.nz }

ink

instance instZeroSNum : Zero SNum

Equations

• instZeroSNum = { zero := SNum.zero false }

ink

instance instOneNzsNum : One NzsNum

Equations

• instOneNzsNum = { one := NzsNum.msb true }

ink

instance instOneSNum : One SNum

Equations

• instOneSNum = { one := SNum.nz 1 }

ink

instance instInhabitedNzsNum : Inhabited NzsNum

Equations

• instInhabitedNzsNum = { default := 1 }

ink

instance instInhabitedSNum : Inhabited SNum

Equations

• instInhabitedSNum = { default := 0 }

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.

ink

def NzsNum.«term_::_» : Lean.TrailingParserDescr

Add a bit at the end of a NzsNum.

Equations

• NzsNum.«term_::_» = Lean.ParserDescr.trailingNode `NzsNum.term_::_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "::") (Lean.ParserDescr.cat `term 0))

ink

def NzsNum.sign : NzsNum → Bool

Sign of a NzsNum.

Equations

• NzsNum.sign (NzsNum.msb b) = !b
• NzsNum.sign (NzsNum.bit a p) = NzsNum.sign p

ink

@[match_pattern]

def NzsNum.not : NzsNum → NzsNum

Bitwise not for NzsNum.

Equations

• NzsNum.not (NzsNum.msb b) = NzsNum.msb (decide ¬b = true)
• NzsNum.not (NzsNum.bit a p) = NzsNum.bit (decide ¬a = true) (NzsNum.not p)

ink

def NzsNum.«term~_» : Lean.ParserDescr

Bitwise not for NzsNum.

Equations

• NzsNum.«term~_» = Lean.ParserDescr.node `NzsNum.term~_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 100))

ink

def NzsNum.bit0 : NzsNum → NzsNum

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

Equations

• NzsNum.bit0 = NzsNum.bit false

ink

def NzsNum.bit1 : NzsNum → NzsNum

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

Equations

• NzsNum.bit1 = NzsNum.bit true

ink

def NzsNum.head : NzsNum → Bool

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

Equations

• NzsNum.head x = match x with | NzsNum.msb b => b | NzsNum.bit b a => b

ink

def NzsNum.tail : NzsNum → SNum

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

Equations

• NzsNum.tail x = match x with | NzsNum.msb b => SNum.zero (decide ¬b = true) | NzsNum.bit a p => SNum.nz p

ink

def SNum.sign : SNum → Bool

Sign of a SNum.

Equations

• SNum.sign x = match x with | SNum.zero z => z | SNum.nz p => NzsNum.sign p

ink

@[match_pattern]

def SNum.not : SNum → SNum

Bitwise not for SNum.

Equations

• SNum.not x = match x with | SNum.zero z => SNum.zero (decide ¬z = true) | SNum.nz p => SNum.nz (NzsNum.not p)

ink

def SNum.«term~_» : Lean.ParserDescr

Bitwise not for SNum.

Equations

• SNum.«term~_» = Lean.ParserDescr.node `SNum.term~_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 100))

ink

@[match_pattern]

def SNum.bit : Bool → SNum → SNum

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

Equations

• SNum.bit x x = match x, x with | b, SNum.zero z => if b = z then SNum.zero b else SNum.nz (NzsNum.msb b) | b, SNum.nz p => SNum.nz (NzsNum.bit b p)

ink

def SNum.«term_::_» : Lean.TrailingParserDescr

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

Equations

• SNum.«term_::_» = Lean.ParserDescr.trailingNode `SNum.term_::_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "::") (Lean.ParserDescr.cat `term 0))

ink

def SNum.bit0 : SNum → SNum

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

Equations

• SNum.bit0 = SNum.bit false

ink

def SNum.bit1 : SNum → SNum

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

Equations

• SNum.bit1 = SNum.bit true

ink

theorem SNum.bit_zero (b : Bool) : SNum.bit b (SNum.zero b) = SNum.zero b

ink

theorem SNum.bit_one (b : Bool) : SNum.bit b (SNum.zero (decide ¬b = true)) = SNum.nz (NzsNum.msb b)

ink

def NzsNum.drec' {C : SNum → Sort u_1} (z : (b : Bool) → C (SNum.zero b)) (s : (b : Bool) → (p : SNum) → C p → C (SNum.bit b p)) (p : NzsNum) : C (SNum.nz p)

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

Equations

• NzsNum.drec' z s (NzsNum.msb b) = Eq.mpr (_ : C (SNum.nz (NzsNum.msb b)) = C (SNum.bit b (SNum.zero (decide ¬b = true)))) (s b (SNum.zero (decide ¬b = true)) (z (decide ¬b = true)))
• NzsNum.drec' z s (NzsNum.bit a p) = s a (SNum.nz p) (NzsNum.drec' z s p)

ink

def SNum.head : SNum → Bool

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

Equations

• SNum.head x = match x with | SNum.zero z => z | SNum.nz p => NzsNum.head p

ink

def SNum.tail : SNum → SNum

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

• SNum.tail x = match x with | SNum.zero z => SNum.zero z | SNum.nz p => NzsNum.tail p

ink

def SNum.drec' {C : SNum → Sort u_1} (z : (b : Bool) → C (SNum.zero b)) (s : (b : Bool) → (p : SNum) → C p → C (SNum.bit b p)) (p : SNum) : C p

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

Equations

• SNum.drec' z s x = match x with | SNum.zero b => z b | SNum.nz p => NzsNum.drec' z s p

ink

def SNum.rec' {α : Sort u_1} (z : Bool → α) (s : Bool → SNum → α → α) : SNum → α

An induction principle for SNum which avoids relying on NzsNum.

Equations

• SNum.rec' z s = SNum.drec' z s

ink

def SNum.testBit : ℕ → SNum → Bool

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

• SNum.testBit 0 x = SNum.head x
• SNum.testBit (Nat.succ n) x = SNum.testBit n (SNum.tail x)

ink

def SNum.succ : SNum → SNum

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

Equations

• SNum.succ = SNum.rec' (fun b => bif b then 0 else 1) fun b p succp => bif b then SNum.bit false succp else SNum.bit true p

ink

def SNum.pred : SNum → SNum

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

Equations

• SNum.pred = SNum.rec' (fun b => bif b then SNum.not 1 else SNum.not 0) fun b p predp => bif b then SNum.bit false p else SNum.bit true predp

ink

def SNum.neg (n : SNum) : SNum

The opposite of a SNum.

Equations

• SNum.neg n = SNum.succ (SNum.not n)

ink

instance SNum.instNegSNum : Neg SNum

Equations

• SNum.instNegSNum = { neg := SNum.neg }

ink

def SNum.czAdd : Bool → Bool → SNum → SNum

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

• SNum.czAdd x x x = match x, x, x with | false, false, p => p | false, true, p => SNum.pred p | true, false, p => SNum.succ p | true, true, p => p

ink

def SNum.bits : SNum → (n : ℕ) → Vector Bool n

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

Equations

• SNum.bits x 0 = Vector.nil
• SNum.bits x (Nat.succ n) = SNum.head x ::ᵥ SNum.bits (SNum.tail x) n

ink

def SNum.cAdd : SNum → SNum → Bool → SNum

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.

ink

def SNum.add (a : SNum) (b : SNum) : SNum

Add two SNums.

Equations

• SNum.add a b = SNum.cAdd a b false

ink

instance SNum.instAddSNum : Add SNum

Equations

• SNum.instAddSNum = { add := SNum.add }

ink

def SNum.sub (a : SNum) (b : SNum) : SNum

Subtract two SNums.

Equations

• SNum.sub a b = a + -b

ink

instance SNum.instSubSNum : Sub SNum

Equations

• SNum.instSubSNum = { sub := SNum.sub }

ink

def SNum.mul (a : SNum) : SNum → SNum

Multiply two SNums.

Equations

• SNum.mul a = SNum.rec' (fun b => bif b then -a else 0) fun b x IH => bif b then SNum.bit0 IH + a else SNum.bit0 IH

ink

instance SNum.instMulSNum : Mul SNum

Equations

• SNum.instMulSNum = { mul := SNum.mul }