inductive Hex.GraphIso.Nauty.Engine.Exit : Type

Completion of a sweep, an unwind to a level with an optional short prune, or exhaustion of the recursion bound.

• done : Exit
• unwind (target : Nat) (short : Bool) : Exit
• fuel : Exit

def Hex.GraphIso.Nauty.Engine.instBEqExit.beq : Exit → Exit → Bool

Equations

• Hex.GraphIso.Nauty.Engine.instBEqExit.beq Hex.GraphIso.Nauty.Engine.Exit.done Hex.GraphIso.Nauty.Engine.Exit.done = true
• Hex.GraphIso.Nauty.Engine.instBEqExit.beq (Hex.GraphIso.Nauty.Engine.Exit.unwind a a_1) (Hex.GraphIso.Nauty.Engine.Exit.unwind b b_1) = (a == b && a_1 == b_1)
• Hex.GraphIso.Nauty.Engine.instBEqExit.beq Hex.GraphIso.Nauty.Engine.Exit.fuel Hex.GraphIso.Nauty.Engine.Exit.fuel = true
• Hex.GraphIso.Nauty.Engine.instBEqExit.beq x✝¹ x✝ = false

@[instance_reducible]

instance Hex.GraphIso.Nauty.Engine.instBEqExit : BEq Exit

Equations

• Hex.GraphIso.Nauty.Engine.instBEqExit = { beq := Hex.GraphIso.Nauty.Engine.instBEqExit.beq }

def Hex.GraphIso.Nauty.Engine.instReprExit.repr : Exit → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Nauty.Engine.instReprExit : Repr Exit

Equations

• Hex.GraphIso.Nauty.Engine.instReprExit = { reprPrec := Hex.GraphIso.Nauty.Engine.instReprExit.repr }

@[instance_reducible]

instance Hex.GraphIso.Nauty.Engine.instInhabitedExit : Inhabited Exit

Equations

• Hex.GraphIso.Nauty.Engine.instInhabitedExit = { default := Hex.GraphIso.Nauty.Engine.instInhabitedExit.default }

inductive Hex.GraphIso.Nauty.Engine.Leaf : Type

The five node classifications in nauty's processnode. A better leaf carries the number of adjacency rows shared with the incumbent.

• internal : Leaf
• autoFirst : Leaf
• autoCanon : Leaf
• better (sr : Nat) : Leaf
• bad : Leaf

@[instance_reducible]

instance Hex.GraphIso.Nauty.Engine.instBEqLeaf : BEq Leaf

Equations

• Hex.GraphIso.Nauty.Engine.instBEqLeaf = { beq := Hex.GraphIso.Nauty.Engine.instBEqLeaf.beq }

def Hex.GraphIso.Nauty.Engine.instBEqLeaf.beq : Leaf → Leaf → Bool

Equations

• Hex.GraphIso.Nauty.Engine.instBEqLeaf.beq Hex.GraphIso.Nauty.Engine.Leaf.internal Hex.GraphIso.Nauty.Engine.Leaf.internal = true
• Hex.GraphIso.Nauty.Engine.instBEqLeaf.beq Hex.GraphIso.Nauty.Engine.Leaf.autoFirst Hex.GraphIso.Nauty.Engine.Leaf.autoFirst = true
• Hex.GraphIso.Nauty.Engine.instBEqLeaf.beq Hex.GraphIso.Nauty.Engine.Leaf.autoCanon Hex.GraphIso.Nauty.Engine.Leaf.autoCanon = true
• Hex.GraphIso.Nauty.Engine.instBEqLeaf.beq (Hex.GraphIso.Nauty.Engine.Leaf.better a) (Hex.GraphIso.Nauty.Engine.Leaf.better b) = (a == b)
• Hex.GraphIso.Nauty.Engine.instBEqLeaf.beq Hex.GraphIso.Nauty.Engine.Leaf.bad Hex.GraphIso.Nauty.Engine.Leaf.bad = true
• Hex.GraphIso.Nauty.Engine.instBEqLeaf.beq x✝¹ x✝ = false

def Hex.GraphIso.Nauty.Engine.instReprLeaf.repr : Leaf → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Nauty.Engine.instReprLeaf : Repr Leaf

Equations

• Hex.GraphIso.Nauty.Engine.instReprLeaf = { reprPrec := Hex.GraphIso.Nauty.Engine.instReprLeaf.repr }

@[instance_reducible]

instance Hex.GraphIso.Nauty.Engine.instInhabitedLeaf : Inhabited Leaf

Equations

• Hex.GraphIso.Nauty.Engine.instInhabitedLeaf = { default := Hex.GraphIso.Nauty.Engine.instInhabitedLeaf.default }

structure Hex.GraphIso.Nauty.Engine.Search (n : Nat) : Type

The search globals, stored in one record so array updates need only consume one constructor. Level and target-cell data are call arguments.

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

• workperm : Array Nat

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

@[instance_reducible]

instance Hex.GraphIso.Nauty.Engine.instInhabitedSearch {a✝ : Nat} : Inhabited (Search a✝)

Equations

• Hex.GraphIso.Nauty.Engine.instInhabitedSearch = { default := Hex.GraphIso.Nauty.Engine.instInhabitedSearch.default }

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

Record an automorphism pair in the bounded workspace. This is Hex.GraphIso.Nauty.pushAuto on the flat engine state.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.Engine.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.Engine.recordFirst {n : Nat} (level refcode : Nat) (st : Search n) : Search 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.Engine.compareCodes {n : Nat} (level code : Nat) (st : Search n) : Search 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.Engine.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.Engine.firstterminal {n : Nat} (level : Nat) (st : Search n) : Search n

nauty's firstterminal: install the first leaf as both the first-path data and the initial best-so-far leaf. This retains the updates of Hex.GraphIso.Nauty.firstterminal.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.Engine.scatter {n : Nat} (refLab : Array Nat) (st : Search n) : Search 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.Engine.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.Engine.admit {n : Nat} (st : Search n) : Search 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.Engine.install {n : Nat} (level sr : Nat) (st : Search n) : Search 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.Engine.pruneReturn {n : Nat} (level : Nat) (st : Search n) : Exit × Search 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.Engine.leafExit {n : Nat} (leaf : Leaf) (level : Nat) (st : Search n) : Exit × Search 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.Engine.cheapCheck {n : Nat} (first : Bool) (level : Nat) (st : Search n) : Search 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.Engine.child {n : Nat} (first : Bool) (level tc tv : Nat) (st : Search n) : Search 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.Engine.afterChildFirst {n : Nat} (level tv1 : Nat) (st : Search n) : Search 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.Engine.afterSweep {n : Nat} (first : Bool) (level tcellsize index : Nat) (st : Search n) : Search 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.Engine.recoverPtn {n : Nat} (inf level : Nat) (st : Search n) : Search n

Reopen the partition below the receiving level, as in the rescan of Hex.GraphIso.Nauty.recover.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.Engine.recoverLevels {n : Nat} (level : Nat) (st : Search n) : Search n

Clamp the four level counters in the order of Hex.GraphIso.Nauty.recover. 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.

@[inline]

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

Intersect with the most recently written workspace pair, as in Hex.GraphIso.Nauty.shortprune.

Equations

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

@[irreducible]

def Hex.GraphIso.Nauty.Engine.node {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) : Exit × Search n

Refine a node, classify it, and sweep its surviving children. Only the leftmost child of a first-path node remains on the first path.

Equations

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

@[irreducible]

def Hex.GraphIso.Nauty.Engine.sweep {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (tv? : Option Nat) (tcell : VSet n) (index : Nat) (st : Search n) : Exit × Nat × Search n

Visit remaining target vertices in order, rereading the cell after each prune. The orbit index includes skipped vertices on the first path. Nodes return an unwind or fuel, so the done arm after a child is unreachable.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Engine.sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 none tcell index st = (Hex.GraphIso.Nauty.Engine.Exit.done, index, st)
• Hex.GraphIso.Nauty.Engine.sweep first ctx inf tcLevel fuel 0 level numcells tc tv1 (some val) tcell index st = (Hex.GraphIso.Nauty.Engine.Exit.fuel, index, st)

def Hex.GraphIso.Nauty.Engine.initial (n : Nat) (lab0 : Array Nat) (cellEnds : List Nat) : Search n

Allocate the search globals, including the reusable permutation.

Equations

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

def Hex.GraphIso.Nauty.Engine.runState (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : Exit × Search n

Run the search and retain the final state and exit for diagnostics. On a valid nonempty input, cell count is at least the level: refinement never decreases it and each child increases it. Thus node depth is at most n, so node fuel n + 2 suffices. A sweep visits at most n vertices in strictly increasing order, so sweep fuel n + 1 suffices.

Equations

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

def Hex.GraphIso.Nauty.Engine.finish {n : Nat} (ctx : Ctx n) (st : Search n) : TraceRun n

Read the canonical result and trace, updating the remaining rows.

Equations

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

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

Run the structured search with the certificate producer's result type.

Equations

• Hex.GraphIso.Nauty.Engine.runTraced n g lab0 cellEnds = Hex.GraphIso.Nauty.Engine.finish { g := g } (Hex.GraphIso.Nauty.Engine.runState n g lab0 cellEnds).snd

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

Run the structured search, discarding the trace.

Equations

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

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

Run the structured search on a coloured graph, retaining the trace.

Equations

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

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

Run the structured search on a coloured graph.

Equations

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