hex

33.3. Part two: the Lean implementation🔗

The Lean implementation follows part one section by section. A graph is stored as one vertex set per vertex, VSet: row u contains v exactly when u and v are adjacent. A vertex set is packed sixty-three vertices to a word, as nauty packs its setword arrays, so every set operation of the search costs one machine operation per word rather than one per vertex; the specification the theorems mention is the natural-number bitset VSet.toNat recovers from it. The row comparison of part one is implemented directly on these sets. It is not the numerical order on the bitsets: in the numerical order the largest vertex would be the most significant, while in the comparison of part one the smallest vertex is the most significant.

33.3.1. Refinement🔗

The accumulator update is mash; its definition contains the two octal constants of part one.

🔗def
Hex.GraphIso.Nauty.mash (l i : Nat) : Nat
Hex.GraphIso.Nauty.mash (l i : Nat) : Nat

nauty's refinement-code accumulator step: MASH(l, i) from naugraph.c. All inputs are nonnegative positions, sizes, or counts, so Nat arithmetic reproduces the C long arithmetic exactly.

One pass, from choosing the splitter through processing every cell, is refineStep. Complete refinement, which repeats passes and finishes the code, is refine.

🔗def
Hex.GraphIso.Nauty.refineStep {n : Nat} (ctx : Hex.GraphIso.Nauty.Ctx n)
  (level split1 : Nat) (st : Hex.GraphIso.Nauty.RefineSt n) :
  Hex.GraphIso.Nauty.RefineSt n
Hex.GraphIso.Nauty.refineStep {n : Nat}
  (ctx : Hex.GraphIso.Nauty.Ctx n)
  (level split1 : Nat)
  (st : Hex.GraphIso.Nauty.RefineSt n) :
  Hex.GraphIso.Nauty.RefineSt n

One iteration of refine's active-cell loop: remove the chosen splitter from the active set and perform its splitting pass.

🔗def
Hex.GraphIso.Nauty.refine {n : Nat} (ctx : Hex.GraphIso.Nauty.Ctx n)
  (level : Nat) (lab ptn : Array Nat)
  (active : Hex.GraphIso.Nauty.VSet n) (numcells : Nat) :
  Hex.GraphIso.Nauty.RefineSt n
Hex.GraphIso.Nauty.refine {n : Nat}
  (ctx : Hex.GraphIso.Nauty.Ctx n)
  (level : Nat) (lab ptn : Array Nat)
  (active : Hex.GraphIso.Nauty.VSet n)
  (numcells : Nat) :
  Hex.GraphIso.Nauty.RefineSt n

nauty's refine: make the partition at level equitable with respect to the active cells, producing the refinement code. With the pinned options (invarproc = NULL) this is also the whole of doref.

The worked example of part one, recomputed by the implementation:

open Hex Hex.GraphIso Hex.GraphIso.Nauty namespace NautyAlgorithmChapterExample private def pathSix : Colored 6 1 := { graph := Graph.ofEdges [(0, 1), (1, 2), (2, 3), (3, 4), (4, 5)] coloring := Coloring.trivial 6 } private def pathCtx : Ctx 6 := { g := rowsOf pathSix } private def initialState : RefineSt 6 := { lab := #[0, 1, 2, 3, 4, 5] ptn := initPtn 6 8 [5] active := initActive 6 [5] numcells := 1 hint := 0 maxpos := 0 longcode := 1 } private def blocks (st : RefineSt 6) : List (List Nat) := (cells st.ptn 1 6).map fun (lo, hi) => (List.range (hi + 1 - lo)).map fun i => st.lab[lo + i]! private def firstSplit : RefineSt 6 := refineStep pathCtx 1 0 initialState private def secondSplit : RefineSt 6 := refineStep pathCtx 1 firstSplit.hint firstSplit private def trace : List (List (List Nat)) := [blocks initialState, blocks firstSplit, blocks secondSplit] [[[0, 1, 2, 3, 4, 5]], [[0, 5], [1, 2, 3, 4]], [[0, 5], [2, 3], [1, 4]]]#eval trace #guard trace = [[[0, 1, 2, 3, 4, 5]], [[0, 5], [1, 2, 3, 4]], [[0, 5], [2, 3], [1, 4]]] #guard (refine pathCtx 1 #[0, 1, 2, 3, 4, 5] (initPtn 6 8 [5]) (initActive 6 [5]) 1).longcode = 27540 end NautyAlgorithmChapterExample 
[[[0, 1, 2, 3, 4, 5]], [[0, 5], [1, 2, 3, 4]], [[0, 5], [2, 3], [1, 4]]]

The first guard pins the three partitions displayed in part one, and the second pins the refinement code 27540 claimed there.

33.3.2. The target cell and the tree🔗

The production target-cell rule is bestcell, selected by targetcell according to the depth. The production rule tests linkage using one representative vertex per cell; the specification tests it using the counts of every vertex, which is the same test on equitable partitions and is independent of vertex order.

🔗def
Hex.GraphIso.Nauty.bestcell {n : Nat} (ctx : Hex.GraphIso.Nauty.Ctx n)
  (lab ptn : Array Nat) (level : Nat) : Nat
Hex.GraphIso.Nauty.bestcell {n : Nat}
  (ctx : Hex.GraphIso.Nauty.Ctx n)
  (lab ptn : Array Nat) (level : Nat) :
  Nat

nauty's bestcell: the first cell nontrivially joined to the greatest number of other nonsingleton cells, as a lab position. The result is n when every cell is a singleton.

🔗def
Hex.GraphIso.Nauty.targetcell {n : Nat} (ctx : Hex.GraphIso.Nauty.Ctx n)
  (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) : Nat
Hex.GraphIso.Nauty.targetcell {n : Nat}
  (ctx : Hex.GraphIso.Nauty.Ctx n)
  (lab ptn : Array Nat)
  (level tcLevel : Nat) (hint : Int) : Nat

nauty's targetcell for the pinned undirected configuration: keep the hinted position when it still starts a nonsingleton cell of the partition at level, otherwise take bestcell while level ≤ tcLevel and the first nonsingleton cell deeper than that.

The complete tree of part one is generated by specNode: refine, stop at a discrete partition, or create the children of the target cell and take the greatest of their keys.

🔗def
Hex.GraphIso.Nauty.specNode {n : Nat} (ctx : Hex.GraphIso.Nauty.Ctx n)
  (tcLevel : Nat) :
  Nat →
    Nat →
      Array Nat →
        Array Nat →
          Hex.GraphIso.Nauty.VSet n → Nat → Hex.GraphIso.Nauty.Key n
Hex.GraphIso.Nauty.specNode {n : Nat}
  (ctx : Hex.GraphIso.Nauty.Ctx n)
  (tcLevel : Nat) :
  Nat →
    Nat →
      Array Nat →
        Array Nat →
          Hex.GraphIso.Nauty.VSet n →
            Nat → Hex.GraphIso.Nauty.Key n

The key of the maximal leaf of the unpruned search tree below one node.

33.3.3. Keys and the declarative canonical form🔗

The two components of a leaf key are the fields of Key, compared by keyCmp. The appended marker is codeSentinel.

🔗structure
Hex.GraphIso.Nauty.Key (n : Nat) : Type
Hex.GraphIso.Nauty.Key (n : Nat) : Type

A leaf key of the unpruned search tree: the level codes ending with the sentinel, then the leaf's adjacency rows.

Constructor

Hex.GraphIso.Nauty.Key.mk

Fields

codes : List Nat

The refinement codes along the path, ending with the sentinel.

rows : List (Hex.GraphIso.Nauty.VSet n)

The leaf's g^lab rows in nauty's row order.

🔗def
Hex.GraphIso.Nauty.keyCmp {n : Nat} (k1 k2 : Hex.GraphIso.Nauty.Key n) :
  Ordering
Hex.GraphIso.Nauty.keyCmp {n : Nat}
  (k1 k2 : Hex.GraphIso.Nauty.Key n) :
  Ordering

The order on keys: level codes first, then rows in nauty's row order.

🔗def
Hex.GraphIso.Nauty.codeSentinel : Nat
Hex.GraphIso.Nauty.codeSentinel : Nat

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

The greatest key of the whole tree is canonSpecKey, and specCanon turns it into the canonical coloured graph, with the colour classes laid out contiguously in colour order.

🔗def
Hex.GraphIso.Nauty.canonSpecKey {n k : Nat}
  (G : Hex.GraphIso.Colored n k) : Hex.GraphIso.Nauty.Key n
Hex.GraphIso.Nauty.canonSpecKey
  {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.Nauty.Key n

The nauty-semantic canonical key of a coloured graph.

🔗def
Hex.GraphIso.Nauty.specCanon {n k : Nat}
  (G : Hex.GraphIso.Colored n k) : Hex.GraphIso.Colored n k
Hex.GraphIso.Nauty.specCanon {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.Colored n k

The nauty-semantic canonical form of a coloured graph: the coloured graph determined by the rows of canonSpecKey G, with the colour classes laid out contiguously in colour order. It is defined for every input, with no certificate needed.

For the six-vertex path, the whole computation gives:

{ codes := [27540, 68, 32767], rows := [16, 32, 24, 36, 5, 10] }#eval canonSpecKey NautyAlgorithmChapterExample.pathSix 
{ codes := [27540, 68, 32767], rows := [16, 32, 24, 36, 5, 10] }

The code list records the root refinement code 27540 from the worked example, the code 68 of the selected leaf's second refinement, and the marker. The rows are the relabelled adjacency bitsets: row 0 is 16, that is, bit 4, so new vertex 0 is adjacent exactly to new vertex 4.

33.3.4. The production search🔗

The pruned search compares leaves with testcanlab and installs a new best leaf with updatecan, which reuses the rows already known to be equal.

🔗def
Hex.GraphIso.Nauty.testcanlab {n : Nat} (ctx : Hex.GraphIso.Nauty.Ctx n)
  (canong : Array (Hex.GraphIso.Nauty.VSet n)) (lab : Array Nat) :
  Int × Nat
Hex.GraphIso.Nauty.testcanlab {n : Nat}
  (ctx : Hex.GraphIso.Nauty.Ctx n)
  (canong :
    Array (Hex.GraphIso.Nauty.VSet n))
  (lab : Array Nat) : Int × Nat

nauty's testcanlab: compare g^lab with canong row by row in nauty's setword order. Returns the comparison and the number of leading equal rows.

🔗def
Hex.GraphIso.Nauty.updatecan {n : Nat} (ctx : Hex.GraphIso.Nauty.Ctx n)
  (canong : Array (Hex.GraphIso.Nauty.VSet n)) (lab : Array Nat)
  (samerows : Nat) : Array (Hex.GraphIso.Nauty.VSet n)
Hex.GraphIso.Nauty.updatecan {n : Nat}
  (ctx : Hex.GraphIso.Nauty.Ctx n)
  (canong :
    Array (Hex.GraphIso.Nauty.VSet n))
  (lab : Array Nat) (samerows : Nat) :
  Array (Hex.GraphIso.Nauty.VSet n)

nauty's updatecan: overwrite rows samerows..n-1 of canong with the corresponding rows of g^lab.

The structured search is exposed as Hex.GraphIso.Nauty.searchResult?. The public entry point is Hex.GraphIso.canonicalize; the HexGraphIso chapter describes the public surface and the theorems it carries.

🔗def
Hex.GraphIso.Nauty.searchResult? {n k : Nat}
  (G : Hex.GraphIso.Colored n k) : Option (Hex.GraphIso.CanonResult n k)
Hex.GraphIso.Nauty.searchResult?
  {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  Option (Hex.GraphIso.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.

🔗def
Hex.GraphIso.canonicalize {n k : Nat} (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.CanonResult n k
Hex.GraphIso.canonicalize {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.CanonResult n k

Compute the canonical form of a coloured graph together with the label producing it: the checked-label transcription of the pinned nauty search. Total; worst-case cost is factorial. Its answer is the one the certificate replay validates (canonicalize_eq_certifyCanon), which is how every theorem below reaches it.

33.3.5. The automorphism output🔗

Each reported permutation is pushed onto the search state's generator trace at the moment the leaf classifies, so the trace is the discovery order of the traversal. Aut.trace reads it off, autom? rebuilds each entry as a permutation of the vertices and accepts it only when it passes the isomorphism check, and autos packages the checked list with the orbit array, the orbit count and the group order. The orbit array is built with the search's own orbjoin, so it is the array the program reports rather than a recomputation.

🔗def
Hex.GraphIso.Aut.trace {n k : Nat} (G : Hex.GraphIso.Colored n k) :
  List (Array Nat)
Hex.GraphIso.Aut.trace {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  List (Array Nat)

The raw generator arrays the pinned traversal records, in discovery order.

🔗def
Hex.GraphIso.autom? {n k : Nat} (G : Hex.GraphIso.Colored n k)
  (γ : Array Nat) : Option (Hex.Perm n)
Hex.GraphIso.autom? {n k : Nat}
  (G : Hex.GraphIso.Colored n k)
  (γ : Array Nat) : Option (Hex.Perm n)

Accept one raw generator array from the traversal: rebuild it as a permutation of Fin n and check that it is an automorphism. This is the only step that admits a generator, and the admission test is checkIso.

🔗def
Hex.GraphIso.Nauty.orbjoin (orbits map : Array Nat) (n : Nat) :
  Array Nat × Nat
Hex.GraphIso.Nauty.orbjoin
  (orbits map : Array Nat) (n : Nat) :
  Array Nat × Nat

nauty's orbjoin: join the orbit cells so that i and map[i] are equivalent, returning the new orbit array and count.

🔗def
Hex.GraphIso.autos {n k : Nat} (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.AutResult n
Hex.GraphIso.autos {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.AutResult n

Generators of the automorphism group of a coloured graph, with the vertex orbits, the orbit count and the orbit-stabilizer product for the group order. Every returned permutation is an automorphism (autos_isIso). Vertices sharing an orbit representative are in one orbit (autos_sameOrbit_of_eq). HexGraphIso.AutComplete supplies the biconditional autos_sameOrbit and proves in autos_complete that the list generates the full group. The Mathlib bridge proves exact cardinality theorems for the orbit count and order. Computing the order runs one traversal per base point, so a caller who wants only the generators or the orbits should take Aut.gens or Aut.orbits.

33.3.6. What the Lean proofs establish🔗

The three theorems below state that the declarative form is isomorphic to its input, is invariant under isomorphism, and decides isomorphism by equality.

🔗theorem
Hex.GraphIso.Nauty.specCanon_iso {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.Isomorphic G (Hex.GraphIso.Nauty.specCanon G)
Hex.GraphIso.Nauty.specCanon_iso
  {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  Hex.GraphIso.Isomorphic G
    (Hex.GraphIso.Nauty.specCanon G)

The total nauty-semantic canonical form is isomorphic to its input.

🔗theorem
Hex.GraphIso.Nauty.specCanon_invariant {n k : Nat}
  {G H : Hex.GraphIso.Colored n k}
  (hiso : Hex.GraphIso.Isomorphic G H) :
  Hex.GraphIso.Nauty.specCanon G = Hex.GraphIso.Nauty.specCanon H
Hex.GraphIso.Nauty.specCanon_invariant
  {n k : Nat}
  {G H : Hex.GraphIso.Colored n k}
  (hiso : Hex.GraphIso.Isomorphic G H) :
  Hex.GraphIso.Nauty.specCanon G =
    Hex.GraphIso.Nauty.specCanon H

specCanon is an isomorphism invariant: isomorphic coloured graphs have the same canonical form.

🔗theorem
Hex.GraphIso.Nauty.iso_iff_specCanon_eq {n k : Nat}
  {G H : Hex.GraphIso.Colored n k} :
  Hex.GraphIso.Isomorphic G H ↔
    Hex.GraphIso.Nauty.specCanon G = Hex.GraphIso.Nauty.specCanon H
Hex.GraphIso.Nauty.iso_iff_specCanon_eq
  {n k : Nat}
  {G H : Hex.GraphIso.Colored n k} :
  Hex.GraphIso.Isomorphic G H ↔
    Hex.GraphIso.Nauty.specCanon G =
      Hex.GraphIso.Nauty.specCanon H

Isomorphism is equivalent to equality of the nauty-semantic canonical forms.

The certificate checker connects the pruned search to the specification: checkKey_sound identifies an accepted key with canonSpecKey, and checkCanon_form identifies an accepted result with specCanon. certifyCanon?_isSome closes the loop: the checker accepts the pruned search's own answer on every input, so the public canonicalize inherits these theorems without replaying a certificate.

🔗theorem
Hex.GraphIso.Nauty.checkCanon_form {n k : Nat}
  {G : Hex.GraphIso.Colored n k} {cert : Hex.GraphIso.Nauty.CertNode}
  {B : Hex.GraphIso.Nauty.Key n} {lab : Array Nat}
  {res : Hex.GraphIso.CanonResult n k}
  (h : Hex.GraphIso.Nauty.checkCanon G cert B lab = some res) :
  res.form = Hex.GraphIso.Nauty.specCanon G
Hex.GraphIso.Nauty.checkCanon_form
  {n k : Nat}
  {G : Hex.GraphIso.Colored n k}
  {cert : Hex.GraphIso.Nauty.CertNode}
  {B : Hex.GraphIso.Nauty.Key n}
  {lab : Array Nat}
  {res : Hex.GraphIso.CanonResult n k}
  (h :
    Hex.GraphIso.Nauty.checkCanon G cert B
        lab =
      some res) :
  res.form =
    Hex.GraphIso.Nauty.specCanon G

A checked canonical form is specCanon of the input.

🔗theorem
Hex.GraphIso.Nauty.certifyCanon?_isSome {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  (Hex.GraphIso.Nauty.certifyCanon? G).isSome = true
Hex.GraphIso.Nauty.certifyCanon?_isSome
  {n k : Nat}
  (G : Hex.GraphIso.Colored n k) :
  (Hex.GraphIso.Nauty.certifyCanon?
        G).isSome =
    true

The certified canonicalization always succeeds.

The automorphism output carries the full generation contract. autos_isIso says every reported permutation is an automorphism, and autos_complete says every automorphism is generated by the returned list. autos_sameOrbit identifies equality of representatives with the full automorphism orbit relation in both directions. The Mathlib bridge proves exact cardinality theorems for the orbit count and group order. These proofs do not add work to the executable traversal, and conformance continues to compare the output against nauty.

🔗theorem
Hex.GraphIso.autos_complete {n k : Nat} (G : Hex.GraphIso.Colored n k)
  {p : Hex.Perm n} (hp : Hex.GraphIso.IsIso G G p) :
  Hex.GraphIso.Perm.Generated (Hex.GraphIso.autos G).gens p
Hex.GraphIso.autos_complete {n k : Nat}
  (G : Hex.GraphIso.Colored n k)
  {p : Hex.Perm n}
  (hp : Hex.GraphIso.IsIso G G p) :
  Hex.GraphIso.Perm.Generated
    (Hex.GraphIso.autos G).gens p

Completeness: every automorphism is a word in the returned generators.

🔗theorem
Hex.GraphIso.autos_isIso {n k : Nat} {G : Hex.GraphIso.Colored n k}
  {p : Hex.Perm n} (h : p ∈ (Hex.GraphIso.autos G).gens) :
  Hex.GraphIso.IsIso G G p
Hex.GraphIso.autos_isIso {n k : Nat}
  {G : Hex.GraphIso.Colored n k}
  {p : Hex.Perm n}
  (h : p ∈ (Hex.GraphIso.autos G).gens) :
  Hex.GraphIso.IsIso G G p

Membership: every returned generator is an automorphism.

🔗theorem
Hex.GraphIso.autos_sameOrbit {n k : Nat} (G : Hex.GraphIso.Colored n k)
  (u v : Fin n) :
  (Hex.GraphIso.autos G).orbits[↑u]! =
      (Hex.GraphIso.autos G).orbits[↑v]! ↔
    Hex.GraphIso.SameOrbit G u v
Hex.GraphIso.autos_sameOrbit {n k : Nat}
  (G : Hex.GraphIso.Colored n k)
  (u v : Fin n) :
  (Hex.GraphIso.autos G).orbits[↑u]! =
      (Hex.GraphIso.autos G).orbits[↑v]! ↔
    Hex.GraphIso.SameOrbit G u v

Two vertices have the same returned representative exactly when an automorphism carries one onto the other.

All of these theorems are about the Lean definitions. The evidence that those definitions agree with dense nauty 2.9.3, splitter order, codes, target cells, row order, and label tie-breaking included, is the conformance suite, which compares the two programs on every graph with up to six vertices and on the families described in the HexGraphIso conformance documentation.