def Hex.GraphIso.Nauty.codeSentinel : Nat

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

Equations

• Hex.GraphIso.Nauty.codeSentinel = 32767

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Exit : Type

Search termination and nonlocal return control.

Equations

• Hex.GraphIso.Nauty.Exit = Hex.GraphIso.Nauty.Generic.Exit

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Leaf : Type

The five node classifications.

Equations

• Hex.GraphIso.Nauty.Leaf = Hex.GraphIso.Nauty.Generic.Leaf

structure Hex.GraphIso.Nauty.SearchState (n : Nat) (κ : Type) : 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, genTrace, and workperm.

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. The reusable workperm array holds the scatter permutation prepared at a leaf. Return levels and short-prune requests are carried by Exit.

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 : κ
• samerows : Nat
• compCanon : Int
• eqlevFirst : Nat
• eqlevCanon : Int
• gcaFirst : Nat
• gcaCanon : Nat
• canonlevel : Nat
• noncheaplevel : Nat
• allsamelevel : Nat
• cosetindex : Nat
• stabvertex : Nat
• numnodes : Nat
• tctotal : Nat
• canupdates : Nat
• numorbits : Nat
• numgenerators : Nat
• numbadleaves : Nat
• maxlevel : Nat
• order : Nat

  Exact stabilizer-index product, accumulated by policies that report it.

• 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.

• workperm : Array Nat

  Scratch permutation, allocated at initialization and filled by leaf comparisons.

@[instance_reducible]

instance Hex.GraphIso.Nauty.instInhabitedSearchState {a✝ : Nat} {a✝¹ : Type} [Inhabited a✝¹] : Inhabited (SearchState a✝ a✝¹)

Equations

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

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Search (n : Nat) : Type

Dense nauty's specialization of the shared search state.

Equations

• Hex.GraphIso.Nauty.Search n = Hex.GraphIso.Nauty.SearchState n (Array (Hex.GraphIso.Nauty.VSet n))

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

Record an automorphism pair in the bounded workspace.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.visit {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : Nat × Nat × Search n

Count and refine a node before comparing its refinement code.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.recordFirst {n : Nat} {κ : Type} (level refcode : Nat) (st : SearchState n κ) : SearchState n κ

Record the refinement code on the first path.

Equations

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

def Hex.GraphIso.Nauty.compareCodes {n : Nat} {κ : Type} (level code : Nat) (st : SearchState n κ) : SearchState 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.

@[inline]

def Hex.GraphIso.Nauty.chooseTarget {n : Nat} (first : Bool) (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : Int × VSet n × Nat × Search n

Choose a target cell exactly when children can be required. Only a canonically smaller off-path node uses the first path's target hint.

Equations

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

def Hex.GraphIso.Nauty.firstterminal {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : SearchState 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.

@[inline]

def Hex.GraphIso.Nauty.scatter {n : Nat} {κ : Type} (refLab : Array Nat) (st : SearchState n κ) : SearchState n κ

Scatter the current labelling through a reference labelling. Detach the scratch field while filling it so each element update consumes just the array, rather than reconstructing the search record.

Equations

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

def Hex.GraphIso.Nauty.classify {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : Leaf × Search n

Classify an off-path node, constructing its permutation in the scratch array and comparing canonical rows only after tied levels.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.admit {n : Nat} {κ : Type} (st : SearchState n κ) : SearchState n κ

Record a permutation and its workspace pair, then join its orbits. The caller decides whether it counts as a new generator.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.install {n : Nat} {κ : Type} (level sr : Nat) (st : SearchState n κ) : SearchState n κ

Install a better leaf, retaining its already compared row prefix.

Equations

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

def Hex.GraphIso.Nauty.pruneReturn {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : Exit × SearchState n κ

Return past a bad or newly installed leaf. The all-same level limits the return, and the noncheap level can extend it.

Equations

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

def Hex.GraphIso.Nauty.leafExit {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : Exit × SearchState n κ

Act on the five classifications. Code 2 without an orbit change still records its permutation and requests a short prune when needed.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.cheapCheck {n : Nat} {κ : Type} (first : Bool) (level : Nat) (st : SearchState n κ) : SearchState n κ

Update the deepest noncheap level before descending.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.child {n : Nat} {κ : Type} (first : Bool) (level tc tv : Nat) (st : SearchState n κ) : SearchState n κ

Individualize a child vertex, recording every first-path coset index.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.afterChildFirst {n : Nat} {κ : Type} (level tv1 : Nat) (st : SearchState n κ) : SearchState n κ

After the leftmost child, record its greatest common ancestor and the vertex fixed by the generators subsequently reported there.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.afterSweep {n : Nat} {κ : Type} (first : Bool) (level tcellsize index : Nat) (st : SearchState n κ) : SearchState n κ

Decrement the all-same level only after a complete first-path sweep.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.recoverPtn {n : Nat} {κ : Type} (inf level : Nat) (st : SearchState n κ) : SearchState n κ

Reopen the partition below the receiving level, as in nauty’s recover.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.recoverLevels {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : SearchState n κ

Clamp the four level counters in nauty’s order. Equality in the last clamp resets the comparison with the canonical code.

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.

@[inline]

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

Intersect with the most recently written workspace pair, as in nauty’s shortprune.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.recover {n : Nat} {κ : Type} (inf level : Nat) (st : SearchState n κ) : SearchState n κ

Restore the partition and comparison levels after a child returns.

Equations

• Hex.GraphIso.Nauty.recover inf level st = Hex.GraphIso.Nauty.recoverLevels level (Hex.GraphIso.Nauty.recoverPtn inf level st)

theorem Hex.GraphIso.Nauty.recover_eq {n : Nat} {κ : Type} (inf level : Nat) (st : SearchState n κ) : recoverLevels level (recoverPtn inf level st) = recover inf level st

Recovery consists of the partition rescan followed by the level clamps.

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 }

@[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.instReprRunResult.repr {n✝ : Nat} : RunResult n✝ → Nat → Std.Format

Equations

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

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.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.