def Hex.GraphIso.Nauty.genCap : Nat

The generator-store cap. Beyond it, admission overwrites the last slot (bounded replacement) rather than stopping.

Equations

• Hex.GraphIso.Nauty.genCap = 500

structure Hex.GraphIso.Nauty.AutState : Type

Untrusted automorphism state threaded through the pruning producers.

• gens : Array (Array Nat × Array Nat)

  Verified generators paired with their inverses.

• gen : Nat

  Bumped on every successful admission (including cap-slot replacement), so per-node filter caches know when to refresh.

• orbits : Array Nat

  Union-find orbit array over vertices, for admission control.

• numorbits : Nat

  Number of orbit classes of orbits.

• firstLeaf : Option (Array Nat)

  The first leaf labelling seen by the current pass.

• prevLeaf : Option (Array Nat)

  The previous leaf labelling seen by the current pass.

• refLeaf : Option (Array Nat)

  A fixed reference leaf from an earlier pass (the achiever).

• budget : Option Nat

  Remaining node budget; none is unbounded.

• exhausted : Bool

  The budget ran out; the caller must discard the result.

def Hex.GraphIso.Nauty.AutState.init (nn : Nat) (budget : Option Nat := none) : AutState

Fresh state over nn vertices.

Equations

• Hex.GraphIso.Nauty.AutState.init nn budget = { orbits := Array.range nn, numorbits := nn, budget := budget }

def Hex.GraphIso.Nauty.AutState.charge (st : AutState) : AutState

Charge one node against the budget.

Equations

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

def Hex.GraphIso.Nauty.composeOnto (ref lab : Array Nat) : Array Nat

The permutation carrying labelling ref onto labelling lab: γ[ref[i]] = lab[i] (nauty's workperm composition).

Equations

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

def Hex.GraphIso.Nauty.composePerm (f π : Array Nat) (nn : Nat) : Array Nat

The composition f ∘ π as arrays over [0, nn).

Equations

• Hex.GraphIso.Nauty.composePerm f π nn = Array.map (fun (x : Nat) => f[π[x]!]!) (Array.range nn)

def Hex.GraphIso.Nauty.isIdentity (γ : Array Nat) (nn : Nat) : Bool

Equations

• Hex.GraphIso.Nauty.isIdentity γ nn = (List.range nn).all fun (v : Nat) => γ[v]! == v

def Hex.GraphIso.Nauty.AutState.admit {n : Nat} (ctx : Ctx n) (st : AutState) (γ : Array Nat) : AutState

Admit one candidate automorphism: reject the identity and duplicates, verify with the checker's own checkAutom, and store the inverse alongside. Admission past the cap overwrites the last slot, preferring generators that merge orbits.

Equations

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

def Hex.GraphIso.Nauty.AutState.harvest {n : Nat} (ctx : Ctx n) (st : AutState) (lab : Array Nat) : AutState

Harvest generators at a leaf: compose the leaf labelling against the pass's first leaf, the previous leaf, and the fixed reference leaf.

Equations

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

def Hex.GraphIso.Nauty.cellMasks (n : Nat) (rsLab rsPtn : Array Nat) (level : Nat) : List (VSet n)

The vertex bitset of every cell of the node's ordered partition.

Equations

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

def Hex.GraphIso.Nauty.respectsMasks {n : Nat} (masks : List (VSet n)) (γ : Array Nat) : Bool

Does γ map every cell bitset onto itself? Since the cells partition the vertices and γ is a bijection, per-cell image equality is exactly setwise cell preservation. Untrusted fast filter.

Equations

• Hex.GraphIso.Nauty.respectsMasks masks γ = masks.all fun (m : Hex.GraphIso.Nauty.VSet n) => Hex.GraphIso.Nauty.VSet.image (fun (w : Nat) => γ[w]!) m == m

def Hex.GraphIso.Nauty.childCellsOk {n : Nat} (ctx : Ctx n) (rsLab rsPtn : Array Nat) (level tc o o' : Nat) (γ : Array Nat) : Bool

The emission predicate for witness-composed automorphisms: the trusted automorphism check, the earlier-offset requirement, and the replay's cell-transport check. Rechecking the witness here makes certificate-store validity local to the producer: a malformed cached generator or composition can only turn this prune into an ordinary descent, rather than invalidate the whole candidate certificate.

Equations

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

def Hex.GraphIso.Nauty.witness? (n : Nat) (rsLab : Array Nat) (tc : Nat) (usable : Array (Array Nat × Array Nat)) (o : Nat) : Option (Nat × Array Nat)

Search for a witness pruning target-cell offset o onto an earlier offset: breadth-first search from v = rsLab[tc + o] over the filtered generators and their inverses, composing the witness along the path. The caller decides how to validate the returned witness: the key search may rely on the untrusted filters alone (a wrong skip is caught by the trusted replay), while certificate emission runs the literal checker predicate.

Equations

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

def Hex.GraphIso.Nauty.usableGens {n : Nat} (masks : List (VSet n)) (st : AutState) (cache : Option (Nat × Array (Array Nat × Array Nat))) : Nat × Array (Array Nat × Array Nat)

The per-node generator filter, cached against the admission generation: recompute only when generators were admitted since the cache was built (freezing at node entry would lose prunes from generators discovered under earlier children).

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.usableGens masks st none = (st.gen, Array.filter (fun (p : Array Nat × Array Nat) => Hex.GraphIso.Nauty.respectsMasks masks p.fst) st.gens)

def Hex.GraphIso.Nauty.certifyNodeAutom {n : Nat} (ctx : Ctx n) (tcLevel : Nat) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → List Nat → AutState → CertNode × AutState

Build the certificate tree for the final best key, emitting .autom records for target-cell offsets reachable from an earlier offset through verified automorphisms. Untrusted; checkKey revalidates everything.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.certifyNodeAutom ctx tcLevel 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = (Hex.GraphIso.Nauty.CertNode.codePrune, x✝)

def Hex.GraphIso.Nauty.produceCand {n k : Nat} (G : Colored n k) (budget : Option Nat) : Option (CertNode × Key n)

Trace-driven candidate production: the transcribed search runs once with tracing on, and the certificate pass translates its trace into a certificate against the traced key. The trace supplies the harvested generators, the achieving labelling, and the recorded code chain, which the checker accepts because the specification and the search share one code coordinate system. No second search runs. The node budget bounds the traced walk. This produces a candidate only. Nothing here is trusted.

Equations

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

def Hex.GraphIso.Nauty.certifyKey? {n k : Nat} (G : Colored n k) (budget : Option Nat := none) : Option (CertNode × Key n)

Produce a checked canonical-key certificate: the pruned branch-and-bound search finds the best key, the pruning certificate pass rebuilds the tree against it, and the trusted checkKey replay validates the pair. budget caps the traced walk's node count; with none the walk is unbounded. none is returned on budget exhaustion as well as on validation failure.

Equations

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

theorem Hex.GraphIso.Nauty.certifyKey?_sound {n k : Nat} {G : Colored n k} {budget : Option Nat} {cert : CertNode} {B : Key n} (h : certifyKey? G budget = some (cert, B)) : canonSpecKey G = B

Every key a successful certifyKey? returns is the spec key.