@[simp]

theorem Hex.GraphIso.Nauty.land_eq (a b : Nat) : a.land b = a &&& b

@[simp]

theorem Hex.GraphIso.Nauty.lor_eq (a b : Nat) : a.lor b = a ||| b

@[simp]

theorem Hex.GraphIso.Nauty.xor_eq (a b : Nat) : a.xor b = a ^^^ b

@[simp]

theorem Hex.GraphIso.Nauty.shiftRight_eq (a b : Nat) : a.shiftRight b = a >>> b

@[simp]

theorem Hex.GraphIso.Nauty.shiftLeft_eq (a b : Nat) : a.shiftLeft b = a <<< b

@[simp]

theorem Hex.GraphIso.Nauty.mul_eq (a b : Nat) : a.mul b = a * b

@[simp]

theorem Hex.GraphIso.Nauty.add_eq (a b : Nat) : a.add b = a + b

@[simp]

theorem Hex.GraphIso.Nauty.sub_eq (a b : Nat) : a.sub b = a - b

@[simp]

theorem Hex.GraphIso.Nauty.div_eq (a b : Nat) : a.div b = a / b

@[simp]

theorem Hex.GraphIso.Nauty.mod_eq (a b : Nat) : a.mod b = a % b

theorem Hex.GraphIso.Nauty.cond_beq {α : Type} (a b : Nat) (x y : α) : (bif a.beq b then x else y) = if a = b then x else y

theorem Hex.GraphIso.Nauty.cond_blt {α : Type} (a b : Nat) (x y : α) : (bif a.blt b then x else y) = if a < b then x else y

theorem Hex.GraphIso.Nauty.cond_ble {α : Type} (a b : Nat) (x y : α) : (bif a.ble b then x else y) = if a ≤ b then x else y

theorem Hex.GraphIso.Nauty.beq_eq_beq (a b : Nat) : a.beq b = (a == b)

theorem Hex.GraphIso.Nauty.blt_eq_decide (a b : Nat) : a.blt b = decide (a < b)

theorem Hex.GraphIso.Nauty.ble_eq_decide (a b : Nat) : a.ble b = decide (a ≤ b)

theorem Hex.GraphIso.Nauty.beq_eq_decide (a b : Nat) : a.beq b = decide (a = b)

theorem Hex.GraphIso.Nauty.cond_beq_true {α : Type} (a : Bool) (x y : α) : (bif a then x else y) = if a = true then x else y

def Hex.GraphIso.Nauty.iterUpImpl {α : Type} (k : Nat) (f : Nat → α → α) (a : α) : α

The compiled form of iterUp.

Equations

• Hex.GraphIso.Nauty.iterUpImpl k f a = Hex.GraphIso.Nauty.iterUpImpl.go✝ f k 0 a

@[implemented_by Hex.GraphIso.Nauty.iterUpImpl]

def Hex.GraphIso.Nauty.iterUp {α : Type} (k : Nat) (f : Nat → α → α) (a : α) : α

iterUp k f a = f (k - 1) (… (f 0 a)), one Nat.rec step per iteration.

Equations

• Hex.GraphIso.Nauty.iterUp k f a = Nat.rec (motive := fun (x : Nat) => α → α) (fun (a : α) => a) (fun (i : Nat) (ih : α → α) (a : α) => ih (f ((k.sub 1).sub i) a)) k a

theorem Hex.GraphIso.Nauty.iterUp_go {α : Type} (k : Nat) (f : Nat → α → α) (j : Nat) (a : α) : j ≤ k → Nat.rec (motive := fun (x : Nat) => α → α) (fun (a : α) => a) (fun (i : Nat) (ih : α → α) (a : α) => ih (f ((k.sub 1).sub i) a)) j a = List.foldl (fun (a : α) (i : Nat) => f i a) a (List.range' (k - j) j)

theorem Hex.GraphIso.Nauty.iterUp_eq_foldl {α : Type} (k : Nat) (f : Nat → α → α) (a : α) : iterUp k f a = List.foldl (fun (a : α) (i : Nat) => f i a) a (List.range k)

def Hex.GraphIso.Nauty.fuelRecImpl {β : Type} : Nat → β → (β → β) → β

The compiled form of fuelRec.

Equations

• Hex.GraphIso.Nauty.fuelRecImpl 0 x✝¹ x✝ = x✝¹
• Hex.GraphIso.Nauty.fuelRecImpl k.succ x✝¹ x✝ = x✝ (Hex.GraphIso.Nauty.fuelRecImpl k x✝¹ x✝)

@[implemented_by Hex.GraphIso.Nauty.fuelRecImpl]

def Hex.GraphIso.Nauty.fuelRec {β : Type} (k : Nat) (base : β) (step : β → β) : β

fuelRec k base step = step (… (step base)), k times: the fuel-bounded recursion of a loop with an early exit as one Nat.rec step per unfolding (β is the loop's function type).

Equations

• Hex.GraphIso.Nauty.fuelRec k base step = Nat.rec base (fun (x : Nat) (ih : β) => step ih) k

theorem Hex.GraphIso.Nauty.fuelRec_zero {β : Type} (base : β) (step : β → β) : fuelRec 0 base step = base

theorem Hex.GraphIso.Nauty.fuelRec_succ {β : Type} (k : Nat) (base : β) (step : β → β) : fuelRec (k + 1) base step = step (fuelRec k base step)

def Hex.GraphIso.Nauty.mapRange {α : Type} (k : Nat) (f : Nat → α) : List α

(List.range k).map f, built by the loop driver.

Equations

• Hex.GraphIso.Nauty.mapRange k f = (Hex.GraphIso.Nauty.iterUp k (fun (o : Nat) (acc : List α) => f o :: acc) []).reverse

theorem Hex.GraphIso.Nauty.mapRange_eq {α : Type} (k : Nat) (f : Nat → α) : mapRange k f = List.map f (List.range k)

def Hex.GraphIso.Nauty.allRange (k : Nat) (p : Nat → Bool) : Bool

(List.range k).all p, by the loop driver.

Equations

• Hex.GraphIso.Nauty.allRange k p = Hex.GraphIso.Nauty.iterUp k (fun (v : Nat) (b : Bool) => b && p v) true

theorem Hex.GraphIso.Nauty.allRange_eq (k : Nat) (p : Nat → Bool) : allRange k p = (List.range k).all p

def Hex.GraphIso.Nauty.elemK (s v : Nat) : Bool

Membership with the accelerated steps only.

Equations

• Hex.GraphIso.Nauty.elemK s v = ((s.shiftRight v).land 1).beq 1

theorem Hex.GraphIso.Nauty.elemK_eq (s v : Nat) : elemK s v = s.testBit v

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

NatSet.insert, raw: a no-op outside the vertex range.

Equations

• Hex.GraphIso.Nauty.insertK n s v = bif v.blt n then s.lor (Nat.shiftLeft 1 v) else s

theorem Hex.GraphIso.Nauty.insertK_eq (n s v : Nat) : insertK n s v = NatSet.insert n s v

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

NatSet.erase, raw: a no-op outside the vertex range.

Equations

• Hex.GraphIso.Nauty.eraseK n s v = bif v.blt n then bif Hex.GraphIso.Nauty.elemK s v then s.xor (Nat.shiftLeft 1 v) else s else s

theorem Hex.GraphIso.Nauty.eraseK_eq (n s v : Nat) : eraseK n s v = NatSet.erase n s v

def Hex.GraphIso.Nauty.mashK (l i : Nat) : Nat

mash, raw.

Equations

• Hex.GraphIso.Nauty.mashK l i = ((l.xor 27421).add i).land 32767

theorem Hex.GraphIso.Nauty.mashK_eq (l i : Nat) : mashK l i = mash l i

def Hex.GraphIso.Nauty.cleanupK (l : Nat) : Nat

cleanup, raw.

Equations

• Hex.GraphIso.Nauty.cleanupK l = l.mod 32767

theorem Hex.GraphIso.Nauty.cleanupK_eq (l : Nat) : cleanupK l = cleanup l

def Hex.GraphIso.Nauty.popCountTable : Nat

popCount of every byte, four bits per entry.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.lowBitTable : Nat

lowBit of every nonzero byte (and 0 for the zero byte), four bits per entry.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.byteEntry (table b : Nat) : Nat

The table entry of byte b.

Equations

• Hex.GraphIso.Nauty.byteEntry table b = (table.shiftRight (Nat.mul 4 b)).land 15

theorem Hex.GraphIso.Nauty.popCountTable_spec (b : Nat) : b < 256 → byteEntry popCountTable b = popCount b

theorem Hex.GraphIso.Nauty.lowBitTable_spec (b : Nat) : b < 256 → byteEntry lowBitTable b = lowBit b

def Hex.GraphIso.Nauty.popCountKGo (fuel : Nat) : Nat → Nat → Nat

The byte loop of popCountK.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.popCountKGo_succ (fuel s acc : Nat) : popCountKGo (fuel + 1) s acc = bif s.beq 0 then acc else popCountKGo fuel (s.shiftRight 8) (acc.add (byteEntry popCountTable (s.land 255)))

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

popCount by bytes, raw.

Equations

• Hex.GraphIso.Nauty.popCountK s = Hex.GraphIso.Nauty.popCountKGo (s + 1) s 0

theorem Hex.GraphIso.Nauty.popCountK_go_eq (fuel s acc : Nat) : s < fuel → popCountKGo fuel s acc = acc + popCount s

theorem Hex.GraphIso.Nauty.popCountK_eq (s : Nat) : popCountK s = popCount s

def Hex.GraphIso.Nauty.lowBitKGo (fuel : Nat) : Nat → Nat → Nat

The byte loop of lowBitK.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.lowBitKGo_succ (fuel s shift : Nat) : lowBitKGo (fuel + 1) s shift = bif s.beq 0 then 0 else bif (s.land 255).beq 0 then lowBitKGo fuel (s.shiftRight 8) (shift.add 8) else shift.add (byteEntry lowBitTable (s.land 255))

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

lowBit by bytes, raw.

Equations

• Hex.GraphIso.Nauty.lowBitK s = Hex.GraphIso.Nauty.lowBitKGo (s + 1) s 0

theorem Hex.GraphIso.Nauty.lowBitK_go_eq (fuel s shift : Nat) : s < fuel → lowBitKGo fuel s shift = if s = 0 then 0 else shift + lowBit s

theorem Hex.GraphIso.Nauty.lowBitK_eq (s : Nat) : lowBitK s = lowBit s

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

nextElem, raw.

Equations

• Hex.GraphIso.Nauty.nextElemK s none = bif s.beq 0 then none else some (Hex.GraphIso.Nauty.lowBitK s)
• Hex.GraphIso.Nauty.nextElemK s (some p) = bif ((s.shiftRight (p.add 1)).shiftLeft (p.add 1)).beq 0 then none else some (Hex.GraphIso.Nauty.lowBitK ((s.shiftRight (p.add 1)).shiftLeft (p.add 1)))

theorem Hex.GraphIso.Nauty.nextElemK_eq (s : Nat) (pos : Option Nat) : nextElemK s pos = NatSet.nextElem s pos

def Hex.GraphIso.Nauty.pack (w : Nat) : List Nat → Nat

The packed number of a list, low field first.

Equations

• Hex.GraphIso.Nauty.pack w [] = 0
• Hex.GraphIso.Nauty.pack w (x_1 :: l) = x_1.add ((Hex.GraphIso.Nauty.pack w l).shiftLeft w)

def Hex.GraphIso.Nauty.pget (w m a i : Nat) : Nat

The kernel-facing read of field i; m = 2 ^ w - 1 is the field mask, passed rather than recomputed. Fields beyond the list read as 0, matching atD.

Equations

• Hex.GraphIso.Nauty.pget w m a i = (a.shiftRight (w.mul i)).land m

def Hex.GraphIso.Nauty.pset (w m len a i v : Nat) : Nat

The kernel-facing write of field i below len; a write at or beyond len is the identity, matching List.set.

Equations

• Hex.GraphIso.Nauty.pset w m len a i v = bif i.blt len then (a.sub ((Hex.GraphIso.Nauty.pget w m a i).shiftLeft (w.mul i))).add (v.shiftLeft (w.mul i)) else a

def Hex.GraphIso.Nauty.Small (w : Nat) (l : List Nat) : Prop

Every entry below 2 ^ w.

Equations

• Hex.GraphIso.Nauty.Small w l = ∀ (x : Nat), x ∈ l → x < 2 ^ w

theorem Hex.GraphIso.Nauty.pack_cons (w x : Nat) (l : List Nat) : pack w (x :: l) = x + 2 ^ w * pack w l

theorem Hex.GraphIso.Nauty.pack_lt (w : Nat) (l : List Nat) : Small w l → pack w l < 2 ^ (w * l.length)

theorem Hex.GraphIso.Nauty.pack_append (w : Nat) (l : List Nat) (v : Nat) : pack w (l ++ [v]) = pack w l + 2 ^ (w * l.length) * v

theorem Hex.GraphIso.Nauty.pack_replicate (w n : Nat) : pack w (List.replicate n 0) = 0

theorem Hex.GraphIso.Nauty.pget_eq (w a i : Nat) : pget w (2 ^ w - 1) a i = a / 2 ^ (w * i) % 2 ^ w

The arithmetic form of a field read.

theorem Hex.GraphIso.Nauty.pget_lt (w a i : Nat) : pget w (2 ^ w - 1) a i < 2 ^ w

theorem Hex.GraphIso.Nauty.pget_pack (w : Nat) (l : List Nat) (i : Nat) : Small w l → pget w (2 ^ w - 1) (pack w l) i = atD l i 0

theorem Hex.GraphIso.Nauty.pset_pack (w : Nat) (l : List Nat) (i v : Nat) : Small w l → v < 2 ^ w → pset w (2 ^ w - 1) l.length (pack w l) i v = pack w (l.set i v)

theorem Hex.GraphIso.Nauty.pack_injective (w : Nat) (l₁ l₂ : List Nat) : Small w l₁ → Small w l₂ → l₁.length = l₂.length → pack w l₁ = pack w l₂ → l₁ = l₂

theorem Hex.GraphIso.Nauty.Small.set {w : Nat} {l : List Nat} (h : Small w l) {v : Nat} (hv : v < 2 ^ w) (i : Nat) : Small w (l.set i v)

theorem Hex.GraphIso.Nauty.Small.append {w : Nat} {l : List Nat} (h : Small w l) {v : Nat} (hv : v < 2 ^ w) : Small w (l ++ [v])

theorem Hex.GraphIso.Nauty.Small.replicate (w n : Nat) : Small w (List.replicate n 0)

theorem Hex.GraphIso.Nauty.Small.nil (w : Nat) : Small w []

theorem Hex.GraphIso.Nauty.Small.atD {w : Nat} {l : List Nat} : Small w l → ∀ (i : Nat), GraphIso.atD l i 0 < 2 ^ w

structure Hex.GraphIso.Nauty.Rep (w n a : Nat) (l : List Nat) : Prop

The correspondence between a packed number and a list of n entries below 2 ^ w.

• len : l.length = n
• small : Small w l
• eq : a = pack w l

theorem Hex.GraphIso.Nauty.Rep.get {w n a : Nat} {l : List Nat} (h : Rep w n a l) (i : Nat) : pget w (2 ^ w - 1) a i = atD l i 0

theorem Hex.GraphIso.Nauty.Rep.get_lt {w n a : Nat} {l : List Nat} : Rep w n a l → ∀ (i : Nat), pget w (2 ^ w - 1) a i < 2 ^ w

theorem Hex.GraphIso.Nauty.Rep.set {w n a : Nat} {l : List Nat} (h : Rep w n a l) (i : Nat) {v : Nat} (hv : v < 2 ^ w) : Rep w n (pset w (2 ^ w - 1) n a i v) (l.set i v)

theorem Hex.GraphIso.Nauty.Rep.push {w n a : Nat} {l : List Nat} (h : Rep w n a l) {v : Nat} (hv : v < 2 ^ w) : Rep w (n + 1) (a.add (v.shiftLeft (w.mul n))) (l ++ [v])

theorem Hex.GraphIso.Nauty.Rep.nil (w : Nat) : Rep w 0 0 []

theorem Hex.GraphIso.Nauty.Rep.replicate (w n : Nat) : Rep w n 0 (List.replicate n 0)

theorem Hex.GraphIso.Nauty.Rep.ofList {w : Nat} {l : List Nat} (h : Small w l) : Rep w l.length (pack w l) l

def Hex.GraphIso.flatRows (nn : Nat) (flat : List Bool) : Array Nat

Adjacency rows rebuilt from the flat literal as single-Nat bitsets: the flat list is cut into rows once, and each row folds over its own short segment instead of probing the flat list. This is the row form the kernel replay computes with.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.rowsOfFlat (nn : Nat) (flat : List Bool) : Array (Nauty.VSet nn)

The same rows as packed vertex sets: the form the specification side consumes.

Equations

• Hex.GraphIso.rowsOfFlat nn flat = (List.map (fun (seg : List Bool) => Hex.GraphIso.Nauty.VSet.ofFn fun (j : Nat) => Hex.GraphIso.atD seg j false) (Hex.GraphIso.chunkRows nn nn flat)).toArray

theorem Hex.GraphIso.rowsOfFlat_eq_rowsOf {n k : Nat} (G : Colored n k) : rowsOfFlat n G.graph.adjMatrix.data.toList = Nauty.rowsOf G

theorem Hex.GraphIso.toNat_rowsOfFlat (nn : Nat) (flat : List Bool) : List.map Nauty.VSet.toNat (rowsOfFlat nn flat).toList = (flatRows nn flat).toList

The kernel's Nat rows are the packed rows read as bitsets.

theorem Hex.GraphIso.size_flatRows (nn : Nat) (flat : List Bool) : (flatRows nn flat).size = nn

theorem Hex.GraphIso.flatRows_small (nn : Nat) (flat : List Bool) (r : Nat) : r ∈ (flatRows nn flat).toList → r < 2 ^ nn

def Hex.GraphIso.rowOfSegK : List Bool → Nat → Nat

The bit set of a row segment whose head sits at position j.

Equations

• Hex.GraphIso.rowOfSegK [] x✝ = 0
• Hex.GraphIso.rowOfSegK (b :: rest) x✝ = bif b then (Hex.GraphIso.rowOfSegK rest (x✝.add 1)).lor (Nat.shiftLeft 1 x✝) else Hex.GraphIso.rowOfSegK rest (x✝.add 1)

theorem Hex.GraphIso.atD_of_length_le {α : Type} (l : List α) (i : Nat) (d : α) : l.length ≤ i → atD l i d = d

theorem Hex.GraphIso.testBit_rowOfSegK (seg : List Bool) (j i : Nat) : (rowOfSegK seg j).testBit i = (decide (j ≤ i) && atD seg (i - j) false)

theorem Hex.GraphIso.testBit_rowFold (nn : Nat) (seg : List Bool) (len a acc i : Nat) : a + len ≤ nn → (List.foldl (fun (row j : Nat) => if atD seg j false = true then Nauty.NatSet.insert nn row j else row) acc (List.range' a len)).testBit i = (acc.testBit i || decide (a ≤ i ∧ i < a + len) && atD seg i false)

theorem Hex.GraphIso.rowOfSegK_eq (nn : Nat) (seg : List Bool) (hlen : seg.length ≤ nn) : rowOfSegK seg 0 = List.foldl (fun (row j : Nat) => if atD seg j false = true then Nauty.NatSet.insert nn row j else row) 0 (List.range nn)

theorem Hex.GraphIso.chunkRows_length_le (m r : Nat) (l seg : List Bool) : seg ∈ chunkRows r m l → seg.length ≤ m

def Hex.GraphIso.Kernel.packRows (nn : Nat) (flat : List Bool) : Nat

The rows packed with width n, read off the flat literal one segment at a time.

Equations

• Hex.GraphIso.Kernel.packRows nn flat = Hex.GraphIso.Nauty.pack nn (List.map (fun (seg : List Bool) => Hex.GraphIso.rowOfSegK seg 0) (Hex.GraphIso.chunkRows nn nn flat))

theorem Hex.GraphIso.Kernel.packRows_eq (nn : Nat) (flat : List Bool) : packRows nn flat = Nauty.pack nn (flatRows nn flat).toList