def Hex.GraphIso.Nauty.lowBit (s : Nat) : Nat

The index of the least set bit, or 0 for the empty set (callers guard on nonemptiness). Structurally recursive on an always-sufficient fuel so the kernel can replay it.

Equations

• Hex.GraphIso.Nauty.lowBit s = Hex.GraphIso.Nauty.lowBit.go (s + 1) s

def Hex.GraphIso.Nauty.lowBit.go : Nat → Nat → Nat

Equations

• Hex.GraphIso.Nauty.lowBit.go 0 a✝ = 0
• Hex.GraphIso.Nauty.lowBit.go fuel.succ a✝ = if (a✝ == 0) = true then 0 else if (a✝ % 2 == 1) = true then 0 else 1 + Hex.GraphIso.Nauty.lowBit.go fuel (a✝ / 2)

theorem Hex.GraphIso.Nauty.lowBit_go_congr (f₁ : Nat) {f₂ s : Nat} : s < f₁ → s < f₂ → lowBit.go f₁ s = lowBit.go f₂ s

theorem Hex.GraphIso.Nauty.lowBit_eq (s : Nat) : lowBit s = if s = 0 then 0 else if s % 2 = 1 then 0 else 1 + lowBit (s / 2)

The unconditional unfolding of lowBit.

def Hex.GraphIso.Nauty.lbByte : Array Nat

lowBit of every nonzero byte, by the specification itself.

Equations

• Hex.GraphIso.Nauty.lbByte = (List.map Hex.GraphIso.Nauty.lowBit (List.range 256)).toArray

@[irreducible]

def Hex.GraphIso.Nauty.lowBitGo (s shift : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.lowBitGo s shift = if s = 0 then 0 else if s % 256 = 0 then Hex.GraphIso.Nauty.lowBitGo (s >>> 8) (shift + 8) else shift + Hex.GraphIso.Nauty.lbByte[s % 256]!

def Hex.GraphIso.Nauty.lowBitFast (s : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.lowBitFast s = Hex.GraphIso.Nauty.lowBitGo s 0

theorem Hex.GraphIso.Nauty.lbByte_get {b : Nat} (h : b < 256) : lbByte[b]! = lowBit b

@[simp]

theorem Hex.GraphIso.Nauty.lowBit_zero : lowBit 0 = 0

theorem Hex.GraphIso.Nauty.lowBit_mod_pow (k : Nat) {s : Nat} : s % 2 ^ k ≠ 0 → lowBit s = lowBit (s % 2 ^ k)

lowBit looks only at the low bits while they are not all zero.

theorem Hex.GraphIso.Nauty.lowBit_shift_pow (k : Nat) {s : Nat} : s ≠ 0 → s % 2 ^ k = 0 → lowBit s = k + lowBit (s / 2 ^ k)

lowBit steps over all-zero low bits.

theorem Hex.GraphIso.Nauty.lowBitGo_eq (s shift : Nat) : lowBitGo s shift = if s = 0 then 0 else shift + lowBit s

@[csimp]

theorem Hex.GraphIso.Nauty.lowBit_eq_lowBitFast : lowBit = lowBitFast

def Hex.GraphIso.Nauty.popCount (s : Nat) : Nat

The number of set bits. Structurally recursive on an always-sufficient fuel so the kernel can replay it.

Equations

• Hex.GraphIso.Nauty.popCount s = Hex.GraphIso.Nauty.popCount.go (s + 1) s

def Hex.GraphIso.Nauty.popCount.go : Nat → Nat → Nat

Equations

• Hex.GraphIso.Nauty.popCount.go 0 a✝ = 0
• Hex.GraphIso.Nauty.popCount.go fuel.succ a✝ = if (a✝ == 0) = true then 0 else a✝ % 2 + Hex.GraphIso.Nauty.popCount.go fuel (a✝ / 2)

theorem Hex.GraphIso.Nauty.popCount_go_congr (f₁ : Nat) {f₂ s : Nat} : s < f₁ → s < f₂ → popCount.go f₁ s = popCount.go f₂ s

theorem Hex.GraphIso.Nauty.popCount_eq (s : Nat) : popCount s = s % 2 + popCount (s / 2)

The unconditional unfolding of popCount: also valid at zero.

@[simp]

theorem Hex.GraphIso.Nauty.popCount_zero : popCount 0 = 0

def Hex.GraphIso.Nauty.pcByte : Array Nat

popCount of every byte, by the specification itself.

Equations

• Hex.GraphIso.Nauty.pcByte = (List.map Hex.GraphIso.Nauty.popCount (List.range 256)).toArray

@[irreducible]

def Hex.GraphIso.Nauty.popCountGo (s acc : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.popCountGo s acc = if s = 0 then acc else Hex.GraphIso.Nauty.popCountGo (s >>> 8) (acc + Hex.GraphIso.Nauty.pcByte[s % 256]!)

def Hex.GraphIso.Nauty.popCountFast (s : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.popCountFast s = Hex.GraphIso.Nauty.popCountGo s 0

theorem Hex.GraphIso.Nauty.pcByte_get {b : Nat} (h : b < 256) : pcByte[b]! = popCount b

theorem Hex.GraphIso.Nauty.popCount_split_pow (k s : Nat) : popCount s = popCount (s % 2 ^ k) + popCount (s / 2 ^ k)

popCount splits at any power-of-two boundary.

theorem Hex.GraphIso.Nauty.popCount_split (s : Nat) : popCount s = popCount (s % 256) + popCount (s >>> 8)

popCount splits at the byte boundary.

theorem Hex.GraphIso.Nauty.popCountGo_eq (s acc : Nat) : popCountGo s acc = acc + popCount s

@[csimp]

theorem Hex.GraphIso.Nauty.popCount_eq_popCountFast : popCount = popCountFast

@[irreducible]

def Hex.GraphIso.Nauty.toListByteGo (b base cnt k : Nat) (acc : List Nat) : List Nat

One byte of toList: prepend the set positions base + k, k < min 8 cnt, in ascending order (so the whole accumulator is descending and one final reverse restores order).

Equations

• Hex.GraphIso.Nauty.toListByteGo b base cnt k acc = if k ≥ 8 ∨ k ≥ cnt then acc else Hex.GraphIso.Nauty.toListByteGo b base cnt (k + 1) (if b.testBit k = true then (base + k) :: acc else acc)

def Hex.GraphIso.Nauty.toListByte (b base cnt : Nat) (acc : List Nat) : List Nat

Equations

• Hex.GraphIso.Nauty.toListByte b base cnt acc = Hex.GraphIso.Nauty.toListByteGo b base cnt 0 acc

@[irreducible]

def Hex.GraphIso.Nauty.toListGo (base cnt s : Nat) (acc : List Nat) : List Nat

The byte-chunked toList walk: one big-number shift per byte, with an early exit once the remainder is empty. It accumulates in reverse, and one final reverse restores ascending order.

Equations

• Hex.GraphIso.Nauty.toListGo base cnt s acc = if cnt = 0 ∨ s = 0 then acc else Hex.GraphIso.Nauty.toListGo (base + 8) (cnt - 8) (s >>> 8) (Hex.GraphIso.Nauty.toListByte (s % 256) base cnt acc)

theorem Hex.GraphIso.Nauty.toListByteGo_eq (b base cnt k : Nat) (acc : List Nat) : toListByteGo b base cnt k acc = (List.map (fun (x : Nat) => base + x) (List.filter b.testBit (List.range' k (min 8 cnt - k)))).reverse ++ acc

theorem Hex.GraphIso.Nauty.toListGo_eq (base cnt s : Nat) (acc : List Nat) : toListGo base cnt s acc = (List.map (fun (x : Nat) => base + x) (List.filter s.testBit (List.range cnt))).reverse ++ acc

def Hex.GraphIso.Nauty.bitCount (n s : Nat) : Nat

The number of set bits below n.

Equations

• Hex.GraphIso.Nauty.bitCount n s = List.countP s.testBit (List.range n)

theorem Hex.GraphIso.Nauty.popCount_eq_bitCount (n s : Nat) : s < 2 ^ n → popCount s = bitCount n s

popCount counts exactly the bits below any bound dominating the set.

theorem Hex.GraphIso.Nauty.testBit_one_shift (v w : Nat) : (1 <<< v).testBit w = (v == w)

The single-bit set.

theorem Hex.GraphIso.Nauty.testBit_lowBit (s : Nat) : s ≠ 0 → s.testBit (lowBit s) = true

The least set bit is a member.

theorem Hex.GraphIso.Nauty.lt_two_pow_of_bits {s n : Nat} (h : ∀ (i : Nat), n ≤ i → s.testBit i = false) : s < 2 ^ n

A set whose bits all lie below n is bounded by 2 ^ n.

theorem Hex.GraphIso.Nauty.or_shift_lt {x : Nat} (hx : x < 2 ^ 63) {j : Nat} (hj : j < 63) : x ||| 1 <<< j < 2 ^ 63

Entry bound after an insertion.

theorem Hex.GraphIso.Nauty.testBit_lt_lowBit (s i : Nat) : i < lowBit s → s.testBit i = false

theorem Hex.GraphIso.Nauty.lowBit_eq_of {s d : Nat} (hd : s.testBit d = true) (hlow : ∀ (i : Nat), i < d → s.testBit i = false) : lowBit s = d

theorem Hex.GraphIso.Nauty.xor_ne_zero_of_ne {a b : Nat} (hab : a ≠ b) : a ^^^ b ≠ 0

theorem Hex.GraphIso.Nauty.testBit_eq_of_lt_lowBit_xor {a b i : Nat} (hi : i < lowBit (a ^^^ b)) : a.testBit i = b.testBit i

theorem Hex.GraphIso.Nauty.testBit_ne_at_lowBit_xor {a b : Nat} (hab : a ≠ b) : a.testBit (lowBit (a ^^^ b)) ≠ b.testBit (lowBit (a ^^^ b))

def Hex.GraphIso.Nauty.NatSet.insert (n s v : Nat) : Nat

Insertion, a no-op outside the vertex range.

Equations

• Hex.GraphIso.Nauty.NatSet.insert n s v = if v < n then s ||| 1 <<< v else s

def Hex.GraphIso.Nauty.NatSet.erase (n s v : Nat) : Nat

Deletion, a no-op outside the vertex range.

Equations

• Hex.GraphIso.Nauty.NatSet.erase n s v = if v < n ∧ s.testBit v = true then s ^^^ 1 <<< v else s

def Hex.GraphIso.Nauty.NatSet.nextElem (s : Nat) (pos : Option Nat) : Option Nat

The least element strictly after the cursor (none starts from the least element): nauty's nextelement.

Equations

• Hex.GraphIso.Nauty.NatSet.nextElem s none = if s = 0 then none else some (Hex.GraphIso.Nauty.lowBit s)
• Hex.GraphIso.Nauty.NatSet.nextElem s (some p) = if s >>> (p + 1) <<< (p + 1) = 0 then none else some (Hex.GraphIso.Nauty.lowBit (s >>> (p + 1) <<< (p + 1)))

def Hex.GraphIso.Nauty.NatSet.rowCmp (a b : Nat) : Ordering

nauty's row order: the least differing vertex decides, and the row holding it is the greater.

Equations

• Hex.GraphIso.Nauty.NatSet.rowCmp a b = if a = b then Ordering.eq else if a.testBit (Hex.GraphIso.Nauty.lowBit (a ^^^ b)) = true then Ordering.gt else Ordering.lt

def Hex.GraphIso.Nauty.NatSet.image (n : Nat) (σ : Nat → Nat) (s : Nat) : Nat

The image of a bitset under a vertex map.

Equations

• Hex.GraphIso.Nauty.NatSet.image n σ s = List.foldl (fun (t v : Nat) => if s.testBit v = true then Hex.GraphIso.Nauty.NatSet.insert n t (σ v) else t) 0 (List.range n)

theorem Hex.GraphIso.Nauty.testBit_shiftUp (x a w : Nat) : (x >>> a <<< a).testBit w = (decide (a ≤ w) && x.testBit w)