def Hex.GraphIso.Nauty.codeSentinel : Nat

The sentinel code above every real refinement code: nauty's 077777.

Equations

• Hex.GraphIso.Nauty.codeSentinel = 32767

structure Hex.GraphIso.Nauty.SearchSt (n : Nat) : Type

Search state: what nauty keeps in file-scope variables for the duration of one nauty() call on n vertices. Every field is named for the nauty global or statsblk member it mirrors, except wsCap and genTrace.

lab and ptn are the partition nest: position i ends a cell at level l exactly when ptn[i] ≤ l. active holds the positions of the cells still to be used as splitters by refine. fixedpts holds the vertices individualized on the path from the root to this node.

firstlab and canonlab are the labellings of the first leaf and of the best-so-far leaf. firstcode and canoncode hold the refinement code of their ancestor at each level, terminated by codeSentinel. firsttc holds the target-cell position chosen at each level of the first path, or -1 where there is none. canong holds the adjacency rows of the best-so-far leaf, correct in its first samerows rows, and canonlevel is that leaf's level.

eqlevFirst (eqlev_first) and eqlevCanon (eqlev_canon) are the deepest levels to which this node's codes agree with the first leaf's and with the best-so-far leaf's. compCanon (comp_canon) is -1, 0 or 1 as this node's code at level eqlevCanon + 1 is less than, equal to, or greater than the best-so-far leaf's. gcaFirst (gca_first) and gcaCanon (gca_canon) are the levels of the greatest common ancestors of this node with those two leaves, and cosetindex and stabvertex are the vertices individualized there.

orbits sends each vertex to the least vertex of its orbit under the automorphisms found so far. noncheaplevel is one past the level of the deepest ancestor for which cheapautom is false. allsamelevel is the level of the least ancestor of the first leaf all of whose descendant leaves are known to be equivalent. needshortprune records that the parent's target cell is to be pruned by shortprune on return.

numnodes, numorbits, numgenerators, numbadleaves, maxlevel, tctotal and canupdates are the members of nauty's statsblk: the nodes visited, the orbits, the generators reported, the leaves that were neither an automorphism nor an improvement, the greatest depth reached, the total size of the target cells chosen, and the number of times the best-so-far leaf was replaced.

• lab : Array Nat
• ptn : Array Nat
• active : VSet n
• orbits : Array Nat
• fixedpts : VSet n
• autos : Array (VSet n × VSet n)

  nauty's automorphism workspace: stored (fix, mcr) pairs of discovered automorphisms, read by shortprune and longprune. Once wsCap pairs are present the last slot is overwritten instead of a new one being added. wsCap is 500, the number of pairs that fit in the 2 * 500 * m setwords densenauty supplies.

• wsCap : Nat
• firstcode : Array Nat
• canoncode : Array Nat
• firsttc : Array Int
• firstlab : Array Nat
• canonlab : Array Nat
• canong : Array (VSet n)
• samerows : Nat
• compCanon : Int
• eqlevFirst : Nat
• eqlevCanon : Int
• gcaFirst : Nat
• gcaCanon : Nat
• canonlevel : Nat
• noncheaplevel : Nat
• allsamelevel : Nat
• cosetindex : Nat
• stabvertex : Nat
• needshortprune : Bool
• numnodes : Nat
• tctotal : Nat
• canupdates : Nat
• numorbits : Nat
• numgenerators : Nat
• numbadleaves : Nat
• maxlevel : Nat
• genTrace : Array (Array Nat)

  No nauty counterpart: every accepted automorphism kept in full, in discovery order, for the certificate producer, alongside the bounded (fix, mcr) pairs of autos. run discards it.

@[instance_reducible]

instance Hex.GraphIso.Nauty.instInhabitedSearchSt {a✝ : Nat} : Inhabited (SearchSt a✝)

Equations

• Hex.GraphIso.Nauty.instInhabitedSearchSt = { default := Hex.GraphIso.Nauty.instInhabitedSearchSt.default }

def Hex.GraphIso.Nauty.pushAuto {n : Nat} (st : SearchSt n) (pair : VSet n × VSet n) : SearchSt n

Record an automorphism pair in the bounded workspace.

Equations

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

def Hex.GraphIso.Nauty.recover (n inf level : Nat) (st : SearchSt n) : SearchSt n

nauty's recover: reopen the partition below level and pull the level bookkeeping back.

Equations

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

def Hex.GraphIso.Nauty.firstterminal {n : Nat} (level : Nat) (st : SearchSt n) : SearchSt n

nauty's firstterminal: install the first leaf as both the first-path data and the initial best-so-far leaf.

Equations

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

def Hex.GraphIso.Nauty.processnode {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : Int × SearchSt n

nauty's processnode: classify a non-first-path node and act on it. Returns the level to return to.

Equations

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

def Hex.GraphIso.Nauty.longprune {n : Nat} (tcell fixedpts : VSet n) (autos : Array (VSet n × VSet n)) : VSet n

nauty's longprune: intersect the target cell with the minimum-cell representatives of every stored automorphism fixing all currently fixed points.

Equations

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

def Hex.GraphIso.Nauty.shortprune {n : Nat} (tcell : VSet n) (st : SearchSt n) : VSet n

nauty's shortprune: intersect the target cell with the mcr set of the most recently stored automorphism. The store is never empty when this is called. An empty store leaves the cell unchanged.

Equations

• Hex.GraphIso.Nauty.shortprune tcell st = match st.autos.back? with | some (fst, mcr) => tcell.inter mcr | none => tcell

@[irreducible]

def Hex.GraphIso.Nauty.firstPathNode {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) : Int × SearchSt n

nauty's firstpathnode: produce a node on the leftmost path. Returns the level to return to.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.firstPathNode ctx inf tcLevel 0 level numcells st = (0, st)

@[irreducible]

def Hex.GraphIso.Nauty.firstChildLoop {n : Nat} (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (tv? : Option Nat) (tcell0 : VSet n) (index0 : Nat) (st0 : SearchSt n) : Option Int × Nat × SearchSt n

The child loop of firstpathnode: individualize each surviving target-cell vertex in ascending order, tracking the orbit index count. Returns some rtn for an early unwind.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.firstChildLoop ctx inf tcLevel fuel 0 level numcells tc tv1 tv? tcell0 index0 st0 = (none, index0, st0)
• Hex.GraphIso.Nauty.firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 none tcell0 index0 st0 = (none, index0, st0)

def Hex.GraphIso.Nauty.otherNodePrep {n : Nat} (level code : Nat) (st : SearchSt n) : SearchSt n

The comparison bookkeeping of nauty's othernode between the refinement and the target-cell choice: the first-path level-code comparison and the best-so-far level-code comparison.

Equations

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

@[irreducible]

def Hex.GraphIso.Nauty.otherNode {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) : Int × SearchSt n

nauty's othernode: produce a node off the leftmost path. Returns the level to return to.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.otherNode ctx inf tcLevel 0 level numcells st = (0, st)

@[irreducible]

def Hex.GraphIso.Nauty.otherChildLoop {n : Nat} (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (tv? : Option Nat) (tcell0 : VSet n) (st0 : SearchSt n) : Option Int × SearchSt n

The child loop of othernode: individualize each surviving target-cell vertex in ascending order, applying shortprune after any child that asks for it and longprune after the first. Returns some rtn for an early unwind.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.otherChildLoop ctx inf tcLevel fuel 0 level numcells tc tv1 tv? tcell0 st0 = (none, st0)
• Hex.GraphIso.Nauty.otherChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 none tcell0 st0 = (none, st0)

structure Hex.GraphIso.Nauty.RunResult (n : Nat) : Type

The result of a canonical search on n vertices: the canonical labelling canonlab and the adjacency rows canong under it, together with the statistics nauty reports in its statsblk. Those are the nodes visited (numnodes), the orbits and generators of the automorphism group (numorbits, numgenerators), the leaves that were neither an automorphism nor an improvement (numbadleaves), the greatest depth reached (maxlevel), the total size of the target cells chosen (tctotal), and the number of times the best-so-far leaf was replaced (canupdates).

• canonlab : Array Nat
• canong : Array (VSet n)
• numnodes : Nat
• numorbits : Nat
• numgenerators : Nat
• numbadleaves : Nat
• maxlevel : Nat
• tctotal : Nat
• canupdates : Nat

@[instance_reducible]

instance Hex.GraphIso.Nauty.instInhabitedRunResult {a✝ : Nat} : Inhabited (RunResult a✝)

Equations

• Hex.GraphIso.Nauty.instInhabitedRunResult = { default := Hex.GraphIso.Nauty.instInhabitedRunResult.default }

def Hex.GraphIso.Nauty.instReprRunResult.repr {n✝ : Nat} : RunResult n✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Nauty.instReprRunResult {n✝ : Nat} : Repr (RunResult n✝)

Equations

• Hex.GraphIso.Nauty.instReprRunResult = { reprPrec := Hex.GraphIso.Nauty.instReprRunResult.repr }

def Hex.GraphIso.Nauty.initPtn (n inf : Nat) (cellEnds : List Nat) : Array Nat

The initial ptn array: inf everywhere except 0 at each cell end.

Equations

• Hex.GraphIso.Nauty.initPtn n inf cellEnds = List.foldl (fun (ptn : Array Nat) (e : Nat) => ptn.set! e 0) (Array.replicate n inf) cellEnds

def Hex.GraphIso.Nauty.initActive (n : Nat) (cellEnds : List Nat) : VSet n

The initial active set: one bit per cell start.

Equations

• Hex.GraphIso.Nauty.initActive n cellEnds = (List.foldl (fun (p : Hex.GraphIso.Nauty.VSet n × Nat) (e : Nat) => (p.fst.insert p.snd, e + 1)) (Hex.GraphIso.Nauty.VSet.empty, 0) cellEnds).fst

structure Hex.GraphIso.Nauty.TraceRun (n : Nat) : Type

A traced run: the search result, every accepted automorphism in discovery order, and the best path's refinement codes. This is the trace the certificate producer reads. The search's canoncode array and the certificate checker use the same code coordinates (each child call is seeded with the parent's recomputed cell count), so the codes are read off the final state directly.

• result : RunResult n
• autos : Array (Array Nat)
• bestCodes : List Nat

  The best leaf's refinement codes at levels 1 .. canonlevel, without the sentinel.

def Hex.GraphIso.Nauty.runTraced (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : TraceRun n

Run the pinned dense-nauty canonical search on n vertices with adjacency rows g and the initial ordered partition (lab0, cellEnds), returning the trace alongside the result. cellEnds lists, in order, the last position of each colour cell.

Equations

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

def Hex.GraphIso.Nauty.run (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : RunResult n

The canonical search result: the traced run with its trace discarded.

Equations

• Hex.GraphIso.Nauty.run n g lab0 cellEnds = (Hex.GraphIso.Nauty.runTraced n g lab0 cellEnds).result

def Hex.GraphIso.Nauty.rowOf {n k : Nat} (G : Colored n k) (i : Nat) : VSet n

The adjacency row of one vertex of a coloured graph.

Equations

• Hex.GraphIso.Nauty.rowOf G i = Hex.GraphIso.Nauty.VSet.ofFn fun (j : Nat) => if h : i < n ∧ j < n then G.graph.adj ⟨i, ⋯⟩ ⟨j, ⋯⟩ else false

theorem Hex.GraphIso.Nauty.mem_rowOf {n k : Nat} (G : Colored n k) (i j : Nat) : (rowOf G i).mem j = if h : i < n ∧ j < n then G.graph.adj ⟨i, ⋯⟩ ⟨j, ⋯⟩ else false

def Hex.GraphIso.Nauty.rowsOf {n k : Nat} (G : Colored n k) : Array (VSet n)

The adjacency rows of a coloured graph.

Equations

• Hex.GraphIso.Nauty.rowsOf G = (List.map (Hex.GraphIso.Nauty.rowOf G) (List.range n)).toArray

def Hex.GraphIso.Nauty.colorClass {n k : Nat} (G : Colored n k) (c : Nat) : List Nat

The vertices of one colour, in increasing order.

Equations

• Hex.GraphIso.Nauty.colorClass G c = List.filter (fun (v : Nat) => if h : v < n ∧ c < k then G.coloring.cells[⟨v, ⋯⟩] == ⟨c, ⋯⟩ else false) (List.range n)

def Hex.GraphIso.Nauty.initialPartition {n k : Nat} (G : Colored n k) : Array Nat × List Nat

The initial lab (vertices by increasing colour, then vertex) and the cell end positions of a coloured graph.

Equations

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

def Hex.GraphIso.Nauty.runColoredTraced {n k : Nat} (G : Colored n k) : TraceRun n

Run the nauty-compatible search on a coloured graph, returning the trace for the certificate producer.

Equations

• Hex.GraphIso.Nauty.runColoredTraced G = match Hex.GraphIso.Nauty.initialPartition G with | (lab0, cellEnds) => Hex.GraphIso.Nauty.runTraced n (Hex.GraphIso.Nauty.rowsOf G) lab0 cellEnds

def Hex.GraphIso.Nauty.runColored {n k : Nat} (G : Colored n k) : RunResult n

Run the nauty-compatible search on a coloured graph.

Equations

• Hex.GraphIso.Nauty.runColored G = (Hex.GraphIso.Nauty.runColoredTraced G).result

def Hex.GraphIso.Nauty.searchResult? {n k : Nat} (G : Colored n k) : Option (CanonResult n k)

The nauty-compatible canonical result: the checked label from canonlab and the relabelled coloured graph. none only if the raw search output fails the label check, which conformance shows does not occur.

Equations

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