Canonical labelling of finite graphs (a compact "mini-nauty")

This file is deliberately programming Lean rather than proving Lean: it implements an individualisation–refinement (IR) canonical labelling algorithm in the style of McKay's nauty, with no Prop-level content at all. Correctness proofs live elsewhere; the only thing this file promises syntactically is termination.

The algorithm

Fix a graph G on the vertex set {0, …, n-1}.

• An ordered partition of the vertices is stored nauty-style: an array lab listing the vertices in partition order, its inverse pos, and for every position i the start cst[i] and end cen[i] of the cell containing position i. Cells are contiguous blocks of lab.

• Refinement (refine) computes the coarsest equitable ordered partition refining a given one, by the usual Hopcroft-style worklist: pop a cell S (the splitter), and split every other cell C according to |N(v) ∩ S|, ordering the fragments by increasing count. This is 1-dimensional Weisfeiler–Leman; on a random graph it already produces a discrete partition.

• A discrete ordered partition is a labelling, so it yields a certificate: the adjacency matrix read off in that order, stored one Nat bitmask per row. Certificates are totally ordered lexicographically.

• When refinement does not discretise, we individualise: pick the first non-singleton cell (an isomorphism-invariant choice), split off one of its vertices, re-refine, and recurse. This produces a search tree whose leaves are labellings.

• The canonical labelling is the leaf that is largest for the order (invariant path, certificate), lexicographically. The invariant path records, for each node on the root-to-leaf path, a hash of the trace of the refinement that produced it (which cells split, into what sizes, at which counts) together with the shape of the resulting partition. Everything hashed is a function of positions and multiplicities only — never of vertex names — so the invariant path is an isomorphism invariant.

Two prunings make this fast:

• Invariant pruning. At a node of depth d, compare its length-d invariant path with that of the best leaf so far. Smaller ⇒ every leaf below is smaller ⇒ prune. Larger ⇒ every leaf below beats the incumbent ⇒ discard the incumbent.

• Automorphism pruning. Two leaves with equal certificates differ by an automorphism γ, which we record. At a node with individualisation path p, any recorded γ fixing p pointwise maps the subtree below p ++ [v] isomorphically onto the one below p ++ [γ v], so only one vertex per orbit needs to be explored.

Note that hash collisions can only weaken pruning: an invariant path is used solely as the first component of a total order on leaves, and any isomorphism-invariant function works there.

Graphs

structure IsoGraph.Canon.Graph : Type

A finite graph on the vertex set {0, …, n-1}, stored both as a dense adjacency matrix (for O(1) adjacency queries) and as neighbour lists (for the refinement inner loop).

The constructor is private so callers cannot supply arrays with inconsistent dimensions or contents. Use Graph.ofOracle, which builds both representations from the same oracle.

• n : Nat

  Number of vertices.

• adj : Array (Array Bool)

  adj[v]![w]! is true iff v and w are adjacent.

• nbr : Array (Array Nat)

  nbr[v]! lists the neighbours of v in increasing order.

@[instance_reducible]

instance IsoGraph.Canon.instInhabitedGraph : Inhabited Graph

Equations

• IsoGraph.Canon.instInhabitedGraph = { default := IsoGraph.Canon.instInhabitedGraph.default }

def IsoGraph.Canon.Graph.ofOracle (n : Nat) (f : Nat → Nat → Bool) : Graph

Build a Graph from an adjacency oracle on {0, …, n-1}.

Written with Array.ofFn/Array.filter rather than as an imperative fill: the arrays are the same, but every entry is then definitionally the oracle, which is what makes the lemmas in IsoGraph/Canon/Equivariance.lean about this function short. vs is shared across the rows so the nbr pass allocates only the neighbour lists themselves.

Equations

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

def IsoGraph.Canon.Graph.edgeCount (G : Graph) : Nat

Number of edges (counting each unordered pair once); handy for sanity checks.

Equations

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

Hashing

A 64-bit FNV-style mixer. Only used to compress isomorphism-invariant integer sequences into a comparable summary; collisions cost pruning power, never correctness.

def IsoGraph.Canon.hashSeed : UInt64

The FNV-1a offset basis, used as the seed of every invariant hash.

Equations

• IsoGraph.Canon.hashSeed = 1469598103934665603

@[inline]

def IsoGraph.Canon.mix (h x : UInt64) : UInt64

Fold one number into a running hash.

Equations

• IsoGraph.Canon.mix h x = (h ^^^ x) * 1099511628211

@[inline]

def IsoGraph.Canon.mixN (h : UInt64) (x : Nat) : UInt64

Fold one Nat into a running hash.

Equations

• IsoGraph.Canon.mixN h x = IsoGraph.Canon.mix h (UInt64.ofNat x)

Ordered partitions

structure IsoGraph.Canon.Part : Type

An ordered partition of {0, …, n-1} into contiguous cells of lab.

• lab[i]! — the vertex at position i;
• pos[v]! — the position of vertex v (inverse of lab);
• cst[i]! — first position of the cell containing position i;
• cen[i]! — one past the last position of that cell.

A cell is therefore identified by its start position, and cell starts are exactly the i with cst[i]! = i.

• lab : Array Nat

  Position ↦ vertex.

• pos : Array Nat

  Vertex ↦ position.

• cst : Array Nat

  Position ↦ start of its cell.

• cen : Array Nat

  Position ↦ end (exclusive) of its cell.

@[instance_reducible]

instance IsoGraph.Canon.instInhabitedPart : Inhabited Part

Equations

• IsoGraph.Canon.instInhabitedPart = { default := IsoGraph.Canon.instInhabitedPart.default }

def IsoGraph.Canon.Part.unit (n : Nat) : Part

The one-cell (unit) partition of {0, …, n-1}.

Equations

• IsoGraph.Canon.Part.unit n = { lab := Array.range n, pos := Array.range n, cst := Array.replicate n 0, cen := Array.replicate n n }

Both readers of a partition below walk it cell by cell: from a cell start i, cen[i]! is the start of the next cell, so the walk i ↦ cen[i]! visits every cell once and reaches n. They are written as structural recursions on an explicit fuel rather than as for loops with a break, because that is the form induction works on — see IsoGraph/Canon/Equivariance.lean, where everything about them is proved. n is always enough fuel: there are at most n cells.

def IsoGraph.Canon.cenHashFrom (cen : Array Nat) (n : Nat) : Nat → Nat → UInt64 → UInt64

Fold the cell sizes from cell start i into the hash h.

Equations

• IsoGraph.Canon.cenHashFrom cen n 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.cenHashFrom cen n fuel.succ x✝¹ x✝ = if x✝¹ ≥ n then x✝ else IsoGraph.Canon.cenHashFrom cen n fuel cen[x✝¹]! (IsoGraph.Canon.mixN x✝ (cen[x✝¹]! - x✝¹))

def IsoGraph.Canon.cenTargetFrom (cen : Array Nat) (n : Nat) : Nat → Nat → Option Nat

Start of the first non-singleton cell at or after cell start i, if any.

Equations

• IsoGraph.Canon.cenTargetFrom cen n 0 x✝ = none
• IsoGraph.Canon.cenTargetFrom cen n fuel.succ x✝ = if x✝ ≥ n then none else if cen[x✝]! - x✝ > 1 then some x✝ else IsoGraph.Canon.cenTargetFrom cen n fuel cen[x✝]!

def IsoGraph.Canon.Part.shapeHash (p : Part) (n : Nat) : UInt64

Hash of the sequence of cell sizes. Isomorphism-invariant.

Equations

• p.shapeHash n = IsoGraph.Canon.cenHashFrom p.cen n n 0 IsoGraph.Canon.hashSeed

def IsoGraph.Canon.Part.targetCell (p : Part) (n : Nat) : Option Nat

Start position of the first non-singleton cell, if any. This is the target cell for individualisation; picking the first one is an isomorphism-invariant rule.

Equations

• p.targetCell n = IsoGraph.Canon.cenTargetFrom p.cen n n 0

Refinement

structure IsoGraph.Canon.Scratch : Type

Scratch space reused across refinement steps.

Allocating these three arrays afresh in every step would make a step cost Ω(n) even when the splitter is tiny, which on sparse graphs dominates everything else. Instead they are threaded through the worklist loop and each step restores them, so the invariant

• cnt is all 0,
• hit is all false,
• bc is all 0

holds on entry to and on exit from every step, and clearing costs only what was dirtied.

• cnt : Array Nat

  Vertex ↦ number of neighbours in the current splitter cell.

• hit : Array Bool

  Cell start ↦ has this cell already been collected?

• bc : Array Nat

  Neighbour count ↦ bucket size, then bucket offset, during the counting sort.

@[instance_reducible]

instance IsoGraph.Canon.instInhabitedScratch : Inhabited Scratch

Equations

• IsoGraph.Canon.instInhabitedScratch = { default := IsoGraph.Canon.instInhabitedScratch.default }

def IsoGraph.Canon.Scratch.empty (n : Nat) : Scratch

Cleared scratch space for a graph on n vertices. Counts never exceed n, so bc needs n + 1 entries.

Equations

• IsoGraph.Canon.Scratch.empty n = { cnt := Array.replicate n 0, hit := Array.replicate n false, bc := Array.replicate (n + 1) 0 }

def IsoGraph.Canon.bumpFrom (nbrs : Array Nat) : Nat → Nat → Array Nat → Array Nat → Array Nat × Array Nat

Bump cnt[v] for every v in nbrs[j:], pushing each newly-touched vertex onto touched.

Like cenHashFrom above this is a structural recursion on an explicit fuel (only ever nbrs.size - j) rather than a for loop, so that the equivariance proof can read off the resulting count at each index; the j < nbrs.size that a for loop hides is exactly what the proof needs.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.bumpFrom nbrs 0 x✝² x✝¹ x✝ = (x✝¹, x✝)

def IsoGraph.Canon.countFrom (G : Graph) (lab : Array Nat) (e : Nat) : Nat → Nat → Array Nat → Array Nat → Array Nat × Array Nat

Accumulate into cnt the number of neighbours each vertex has among lab[k:e], recording in touched the vertices whose count became nonzero. This is phase (1) of refineStep, and is the hot loop of the whole algorithm: it costs the splitter cell's degree sum.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.countFrom G lab e 0 x✝² x✝¹ x✝ = (x✝¹, x✝)

def IsoGraph.Canon.sortNats (a : Array Nat) : Array Nat

Sort an array of naturals increasingly.

Array.qsort would do the same job, but it has no verified specification in this toolchain, and the sorted order of the cells and of the counts is part of what makes the trace canonical. So this goes through List.mergeSort, which does. The round trip through List costs nothing measurable on the benchmarks: both call sites sort at most one entry per cell of the partition, against a refinement step that already costs the splitter's degree sum.

Equations

• IsoGraph.Canon.sortNats a = (a.toList.mergeSort fun (x y : Nat) => decide (x ≤ y)).toArray

def IsoGraph.Canon.collectFrom (pos cst touched : Array Nat) : Nat → Nat → Array Bool → Array Nat → Array Bool × Array Nat

Collect the distinct cell starts of the vertices in touched[j:], using hit to deduplicate. Phase (2) of refineStep, as a structural recursion on fuel; fuel is only ever touched.size - j.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.collectFrom pos cst touched 0 x✝² x✝¹ x✝ = (x✝¹, x✝)

def IsoGraph.Canon.bucketFrom (lab cnt : Array Nat) (ec : Nat) : Nat → Nat → Array Nat → Array Nat → Array Nat × Array Nat

Bucket the cell lab[k:ec] by neighbour count: bc[t] counts the members whose count is t, and ks lists the counts that occur, in first-occurrence order. Phase (3a) of refineStep, and another fuel recursion in place of a for loop; fuel is only ever ec - k.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.bucketFrom lab cnt ec 0 x✝² x✝¹ x✝ = (x✝¹, x✝)

def IsoGraph.Canon.offsetFrom (ks : Array Nat) : Nat → Nat → Array Nat → Array Nat → Nat → Array Nat × Array Nat

Turn the bucket sizes into the fragment sizes sizes[j] and the bucket offsets bc[ks[j]] (relative to the start of the cell). acc is the running offset. Phase (3b).

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.offsetFrom ks 0 x✝³ x✝² x✝¹ x✝ = (x✝², x✝¹)

def IsoGraph.Canon.scatterFrom (lab cnt : Array Nat) (ec : Nat) : Nat → Nat → Array Nat → Array Nat → Array Nat × Array Nat

Scatter the cell's vertices into block in count order, each bucket keeping the order it had in the cell. Phase (3c).

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.scatterFrom lab cnt ec 0 x✝² x✝¹ x✝ = (x✝¹, x✝)

def IsoGraph.Canon.clearBcFrom (ks : Array Nat) : Nat → Nat → Array Nat → Array Nat

Zero the buckets the cell used, leaving bc clear for the next cell. Phase (3d).

Equations

• IsoGraph.Canon.clearBcFrom ks 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.clearBcFrom ks fuel.succ x✝¹ x✝ = if x✝¹ ≥ ks.size then x✝ else IsoGraph.Canon.clearBcFrom ks fuel (x✝¹ + 1) (x✝.set! ks[x✝¹]! 0)

def IsoGraph.Canon.writeFrom (block : Array Nat) (c : Nat) : Nat → Nat → Array Nat → Array Nat → Array Nat × Array Nat

Copy the sorted block back into lab[c:], keeping pos its inverse. Phase (3e).

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.writeFrom block c 0 x✝² x✝¹ x✝ = (x✝¹, x✝)

def IsoGraph.Canon.fillBoundsFrom (st en : Nat) : Nat → Nat → Array Nat → Array Nat → Array Nat × Array Nat

Write the boundaries of the fragment [st, en) into cst/cen. Phase (4a).

Equations

• IsoGraph.Canon.fillBoundsFrom st en 0 x✝² x✝¹ x✝ = (x✝¹, x✝)
• IsoGraph.Canon.fillBoundsFrom st en fuel.succ x✝² x✝¹ x✝ = if x✝² ≥ en then (x✝¹, x✝) else IsoGraph.Canon.fillBoundsFrom st en fuel (x✝² + 1) (x✝¹.set! x✝² st) (x✝.set! x✝² en)

def IsoGraph.Canon.boundsFrom (ks sizes : Array Nat) : Nat → Nat → Array Nat → Array Nat → Array Nat → Nat → UInt64 → Array Nat × Array Nat × Array Nat × UInt64

Install the boundaries of every fragment of a split cell, collecting the fragment starts and hashing each fragment's size and count into the trace. Phase (4).

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.boundsFrom ks sizes 0 x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = (x✝⁴, x✝³, x✝², x✝)

def IsoGraph.Canon.markAllFrom (starts : Array Nat) : Nat → Nat → Array Bool → Array Bool

Queue every fragment of a split cell. Phase (5), the case where the parent was queued.

Equations

• IsoGraph.Canon.markAllFrom starts 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.markAllFrom starts fuel.succ x✝¹ x✝ = if x✝¹ ≥ starts.size then x✝ else IsoGraph.Canon.markAllFrom starts fuel (x✝¹ + 1) (x✝.set! starts[x✝¹]! true)

def IsoGraph.Canon.maxIdxFrom (sizes : Array Nat) : Nat → Nat → Nat → Nat

Index of a largest fragment, scanning left to right.

Equations

• IsoGraph.Canon.maxIdxFrom sizes 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.maxIdxFrom sizes fuel.succ x✝¹ x✝ = if x✝¹ ≥ sizes.size then x✝ else IsoGraph.Canon.maxIdxFrom sizes fuel (x✝¹ + 1) (if sizes[x✝¹]! > sizes[x✝]! then x✝¹ else x✝)

def IsoGraph.Canon.markExceptFrom (starts : Array Nat) (bi : Nat) : Nat → Nat → Array Bool → Array Bool

Queue every fragment but starts[bi]. Phase (5), Hopcroft's case: skipping one largest fragment is what keeps refinement near-linear.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.markExceptFrom starts bi 0 x✝¹ x✝ = x✝

def IsoGraph.Canon.clearCntFrom (touched : Array Nat) : Nat → Nat → Array Nat → Array Nat

Zero the counts of the touched vertices. Phase (6).

Equations

• IsoGraph.Canon.clearCntFrom touched 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.clearCntFrom touched fuel.succ x✝¹ x✝ = if x✝¹ ≥ touched.size then x✝ else IsoGraph.Canon.clearCntFrom touched fuel (x✝¹ + 1) (x✝.set! touched[x✝¹]! 0)

def IsoGraph.Canon.clearHitFrom (cells : Array Nat) : Nat → Nat → Array Bool → Array Bool

Unmark the cells that were collected. Phase (6).

Equations

• IsoGraph.Canon.clearHitFrom cells 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.clearHitFrom cells fuel.succ x✝¹ x✝ = if x✝¹ ≥ cells.size then x✝ else IsoGraph.Canon.clearHitFrom cells fuel (x✝¹ + 1) (x✝.set! cells[x✝¹]! false)

structure IsoGraph.Canon.SplitState : Type

The state refineStep's cell loop carries: the partition being rewritten, the worklist, the trace, and the bucket scratch. (cnt is read-only during the loop, so it stays outside.)

• lab : Array Nat

  Position to vertex.

• pos : Array Nat

  Vertex to position.

• cst : Array Nat

  Position to the start of its cell.

• cen : Array Nat

  Position to the end of its cell.

• inW : Array Bool

  Which cells are queued as splitters.

• tr : UInt64

  The trace hash so far.

• bc : Array Nat

  The bucket scratch, all-zero between cells.

def IsoGraph.Canon.splitCell (cnt : Array Nat) (c : Nat) (st : SplitState) : SplitState

Split the cell starting at position c by neighbour count, phases (3) to (5). Written as a chain of matches rather than a do block for the same reason as the loops above.

Equations

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

def IsoGraph.Canon.splitCellsFrom (cnt cells : Array Nat) : Nat → Nat → SplitState → SplitState

Split every cell in cells[j:], left to right.

Equations

• IsoGraph.Canon.splitCellsFrom cnt cells 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.splitCellsFrom cnt cells fuel.succ x✝¹ x✝ = if x✝¹ ≥ cells.size then x✝ else IsoGraph.Canon.splitCellsFrom cnt cells fuel (x✝¹ + 1) (IsoGraph.Canon.splitCell cnt cells[x✝¹]! x✝)

def IsoGraph.Canon.refineStep (G : Graph) (p : Part) (inW : Array Bool) (s : Nat) (tr : UInt64) (sc : Scratch) : Part × Array Bool × UInt64 × Scratch

Perform one refinement step: use the cell starting at position s as a splitter, splitting every cell that meets its neighbourhood.

Returns the new partition, the updated worklist (inW, indexed by cell start position), the updated trace hash, and the scratch space, restored to its cleared state. Cells created by a split are pushed onto the worklist following Hopcroft's rule: all fragments if the parent was queued, otherwise all but a largest fragment.

Equations

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

def IsoGraph.Canon.firstSet (a : Array Bool) : Option Nat

Index of the first true entry of a.

Equations

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

def IsoGraph.Canon.refineLoop (G : Graph) : Nat → Part → Array Bool → UInt64 → Scratch → Part × UInt64

The refinement worklist loop. fuel bounds the number of splitter pops.

The guard s < G.n && p.cst[s]! == s is never false in a real run — only cell starts are ever queued, and a cell start stays one when its cell is split — but checking it costs one array read per pop and saves Equivariance.refineLoop_equiv from having to carry the worklist invariant. Popping a position that is not a cell start simply drops it.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.refineLoop G 0 x✝³ x✝² x✝¹ x✝ = (x✝³, x✝¹)

def IsoGraph.Canon.refine (G : Graph) (p : Part) (inW : Array Bool) (tr : UInt64) : Part × UInt64

Refine p to the coarsest equitable partition refining it, using the cells whose start positions are flagged in inW as initial splitters. Returns the refined partition together with the trace hash of the refinement.

The fuel n² + n + 1 is a genuine bound: a cell start enters the worklist once initially and once per fragment of each split, there are at most n - 1 splits, and each split creates at most n fragments.

Equations

• IsoGraph.Canon.refine G p inW tr = IsoGraph.Canon.refineLoop G (G.n * G.n + G.n + 1) p inW tr (IsoGraph.Canon.Scratch.empty G.n)

def IsoGraph.Canon.initialRefine (G : Graph) : Part × UInt64

Refine from the unit partition: equivalently, the coarsest equitable partition of G.

Equations

• IsoGraph.Canon.initialRefine G = IsoGraph.Canon.refine G (IsoGraph.Canon.Part.unit G.n) (if (G.n == 0) = true then #[] else (Array.replicate G.n false).set! 0 true) IsoGraph.Canon.hashSeed

def IsoGraph.Canon.setCstFrom (c ec : Nat) : Nat → Nat → Array Nat → Array Nat

Write c + 1 into cst[j] for every j ∈ [j₀, ec), where j₀ is the second argument. A structural recursion rather than a for loop so that Equivariance.setCstFrom_getElemD can read off each entry; fuel is only ever ec - j₀, so the work is the same.

Equations

• IsoGraph.Canon.setCstFrom c ec 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.setCstFrom c ec fuel.succ x✝¹ x✝ = if x✝¹ ≥ ec then x✝ else IsoGraph.Canon.setCstFrom c ec fuel (x✝¹ + 1) (x✝.set! x✝¹ (c + 1))

def IsoGraph.Canon.individualize (p : Part) (v : Nat) : Part × Nat

Split the vertex v off from its cell, placing it first. Returns the new partition and the position of the new singleton cell {v} (which is the only splitter needed to re-refine, since the input partition is assumed equitable).

Equations

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

Certificates

def IsoGraph.Canon.rowWords (n : Nat) : Nat

Number of 64-bit words used for one row of a certificate.

Equations

• IsoGraph.Canon.rowWords n = (n + 63) / 64

def IsoGraph.Canon.certRow (n : Nat) (b : Nat → Bool) : Nat → Nat → UInt64 → Nat → Array UInt64 → Array UInt64

An n × n bit matrix packed into 64-bit words: row i occupies words [i * rowWords n, (i+1) * rowWords n), and column j of a row is bit 63 - j % 64 of word j / 64. Unused trailing bits are zero.

The matrix is given as a curried function so that a caller can do its per-row work — for certOf below, one array index — in the outer lambda, where this loop applies it once per row rather than once per bit.

Like the partition walks above, the two loops are structural recursions on fuel rather than for loops, so that induction applies to them: fuel counts the entries still to do and j (resp. i) the position reached, and j + fuel = n is the invariant that gives j < n inside the body — which is exactly what a proof about the loop needs and what a for loop hides.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.certRow n b 0 x✝³ x✝² x✝¹ x✝ = if (n % 64 != 0) = true then x✝.set! x✝¹ (x✝² <<< UInt64.ofNat (64 - n % 64)) else x✝

def IsoGraph.Canon.certRowsFrom (n : Nat) (bit : Nat → Nat → Bool) (w : Nat) : Nat → Nat → Array UInt64 → Array UInt64

Pack rows i, i+1, … of the matrix, fuel of them, into out.

Equations

• IsoGraph.Canon.certRowsFrom n bit w 0 x✝¹ x✝ = x✝
• IsoGraph.Canon.certRowsFrom n bit w fuel.succ x✝¹ x✝ = IsoGraph.Canon.certRowsFrom n bit w fuel (x✝¹ + 1) (IsoGraph.Canon.certRow n (bit x✝¹) n 0 0 (x✝¹ * w) x✝)

def IsoGraph.Canon.certBits (n : Nat) (bit : Nat → Nat → Bool) : Array UInt64

An n × n bit matrix packed into 64-bit words: row i occupies words [i * rowWords n, (i+1) * rowWords n), and column j of a row is bit 63 - j % 64 of word j / 64. Unused trailing bits are zero.

The matrix is given as a curried function so that a caller can do its per-row work — for certOf below, one array index — in the outer lambda, where this loop applies it once per row rather than once per bit.

Like the partition walks above, the two loops are structural recursions on fuel rather than for loops, so that induction applies to them: fuel counts the entries still to do and j (resp. i) the position reached, and j + fuel = n is the invariant that gives j < n inside the body — which is exactly what a proof about the loop needs and what a for loop hides.

Equations

• IsoGraph.Canon.certBits n bit = IsoGraph.Canon.certRowsFrom n bit (IsoGraph.Canon.rowWords n) n 0 (Array.replicate (n * IsoGraph.Canon.rowWords n) 0)

def IsoGraph.Canon.certOf (G : Graph) (lab : Array Nat) : Array UInt64

The adjacency matrix of G read off in the order lab, packed by certBits.

Packing bits most-significant-first means that comparing the word arrays lexicographically, as unsigned integers, compares the bit strings lexicographically. Two labellings give the same certificate exactly when they differ by an automorphism.

Equations

• IsoGraph.Canon.certOf G lab = IsoGraph.Canon.certBits G.n fun (i : Nat) => have row := G.adj[lab[i]!]!; fun (j : Nat) => row[lab[j]!]!

def IsoGraph.Canon.lexCmpFrom (a b : Array UInt64) : Nat → Nat → Ordering

Lexicographic comparison of a and b from index i on, with fuel bounding the number of positions still to look at. Written as a structural recursion rather than a for loop so that the order lemmas in IsoGraph.Canon.Search can be proved by induction on fuel.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.lexCmpFrom a b 0 x✝ = compare a.size b.size

def IsoGraph.Canon.lexCmpU64 (a b : Array UInt64) : Ordering

Lexicographic comparison of UInt64 arrays (shorter is smaller on a common prefix).

Equations

• IsoGraph.Canon.lexCmpU64 a b = IsoGraph.Canon.lexCmpFrom a b (min a.size b.size) 0

Automorphisms

def IsoGraph.Canon.autoOf (n : Nat) (σ τ : Array Nat) : Array Nat

Given two labellings σ τ : position → vertex with equal certificates, the permutation γ = τ ∘ σ⁻¹, which is an automorphism of the graph.

Written as a foldl over List.range n rather than as a for loop so that IsoGraph.Canon.Autos.autoOf_get can read off each entry; the work is the same.

Equations

• IsoGraph.Canon.autoOf n σ τ = List.foldl (fun (g : Array Nat) (i : Nat) => g.set! σ[i]! τ[i]!) (Array.replicate n 0) (List.range n)

def IsoGraph.Canon.moves (g : Array Nat) : Bool

Whether a permutation moves some point.

Equations

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

def IsoGraph.Canon.closureStep (gens : Array (Array Nat)) (mark : Array Bool) (stack : Array Nat) (v : Nat) : Array Bool × Array Nat

One step of orbit closure: mark the images of v under all generators. A foldl rather than a for loop so that IsoGraph.Canon.Orbits can induct on the generator list.

Equations

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

def IsoGraph.Canon.closureLoop (gens : Array (Array Nat)) : Nat → Array Bool → Array Nat → Array Bool

Close mark under the generators, using stack as the frontier. fuel bounds the number of pops, which is at most the number of marked points.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.closureLoop gens 0 x✝¹ x✝ = x✝¹

def IsoGraph.Canon.orbitClosure (n : Nat) (gens : Array (Array Nat)) (seed : Array Nat) : Array Bool

The union of the gens-orbits of the vertices in seed, as a membership array of size n.

Equations

• IsoGraph.Canon.orbitClosure n gens seed = IsoGraph.Canon.closureLoop gens (n + 1) (Array.foldl (fun (mark : Array Bool) (v : Nat) => mark.set! v true) (Array.replicate n false) seed) seed

The search

def IsoGraph.Canon.commonPrefixFrom (a b : Array Nat) (m : Nat) : Nat → Nat → Nat

Scan for the first disagreement at or after i, stopping at m. A structural recursion on fuel rather than a for loop with a break, for the same reason as the partition walks above: IsoGraph.Canon.Jump needs to induct on it.

Equations

• IsoGraph.Canon.commonPrefixFrom a b m 0 x✝ = x✝
• IsoGraph.Canon.commonPrefixFrom a b m fuel.succ x✝ = if x✝ ≥ m then m else if (a[x✝]! == b[x✝]!) = true then IsoGraph.Canon.commonPrefixFrom a b m fuel (x✝ + 1) else x✝

def IsoGraph.Canon.commonPrefix (a b : Array Nat) : Nat

Length of the longest common prefix of two paths.

Equations

• IsoGraph.Canon.commonPrefix a b = IsoGraph.Canon.commonPrefixFrom a b (min a.size b.size) (min a.size b.size) 0

structure IsoGraph.Canon.Leaf : Type

A leaf of the search tree: a discrete ordered partition together with the data used to compare it against other leaves.

• path : Array Nat

  The vertices individualised to reach this leaf.

• invPath : Array UInt64

  Node invariants along the root-to-leaf path.

• cert : Array UInt64

  The certificate of lab.

• lab : Array Nat

  The labelling itself: position ↦ vertex.

@[instance_reducible]

instance IsoGraph.Canon.instInhabitedLeaf : Inhabited Leaf

Equations

• IsoGraph.Canon.instInhabitedLeaf = { default := IsoGraph.Canon.instInhabitedLeaf.default }

structure IsoGraph.Canon.St : Type

Mutable state threaded through the depth-first search.

• best : Option Leaf

  The best leaf seen so far, for the order (invPath, cert).

• first : Option Leaf

  The very first leaf reached, kept only to detect automorphisms.

• autos : Array (Array Nat)

  Automorphisms discovered so far, as image arrays γ[v]!.

• nodes : Nat

  Number of search-tree nodes visited.

• abortTo : Option Nat

  When some k: abandon the search below depth k. See leafUpdate.

@[instance_reducible]

instance IsoGraph.Canon.instInhabitedSt : Inhabited St

Equations

• IsoGraph.Canon.instInhabitedSt = { default := IsoGraph.Canon.instInhabitedSt.default }

def IsoGraph.Canon.maxGens : Nat

Cap on the number of stored automorphism generators. Dropping generators only weakens orbit pruning, so this is a pure performance guard.

Equations

• IsoGraph.Canon.maxGens = 256

def IsoGraph.Canon.St.addAuto (st : St) (g : Array Nat) : St

Record a newly found automorphism, ignoring the identity and duplicates.

Equations

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

def IsoGraph.Canon.pruneNode (invPath : Array UInt64) (st : St) : Option St

Invariant pruning at a node. Returns none if the whole subtree is dominated by the current best leaf, and otherwise the state to continue with (with the incumbent discarded if the subtree is guaranteed to beat it).

Equations

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

def IsoGraph.Canon.leafUpdate (G : Graph) (path : Array Nat) (invPath : Array UInt64) (lab : Array Nat) (st : St) : St

Process a leaf: update the incumbent, harvest any automorphism, and decide how far to backjump.

If the new leaf ν has the same certificate as a previously completed leaf ζ, then γ = ζ ∘ ν⁻¹ is an automorphism. Writing k for the depth of the greatest common ancestor of the two leaves, γ fixes the first k individualised vertices and maps ν's branch at depth k onto ζ's. Since depth-first search had already finished ζ's branch before entering ν's, every leaf still unexplored below ν's branch is a γ-image of one already seen, and carries the same certificate. So the whole remainder of that branch can be abandoned: we request a backjump to depth k.

Equations

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

def IsoGraph.Canon.usableAutos (autos : Array (Array Nat)) (path : Array Nat) : Array (Array Nat)

The automorphisms found so far that fix every vertex of path. Only these may be used to prune the children of the node reached by path.

Equations

• IsoGraph.Canon.usableAutos autos path = if autos.isEmpty = true then autos else Array.filter (fun (g : Array Nat) => path.all fun (x : Nat) => g[x]! == x) autos

structure IsoGraph.Canon.Orbits : Type

Cached orbit information for the children of one search-tree node: the orbit of the already processed children, under those automorphisms that fix the node's individualisation path.

• nGens : Nat

  Size of St.autos when this was computed; used to detect staleness.

• gens : Array (Array Nat)

  The automorphisms fixing the node's path pointwise.

• mark : Array Bool

  Membership array for the orbit of the processed children.

@[instance_reducible]

instance IsoGraph.Canon.instInhabitedOrbits : Inhabited Orbits

Equations

• IsoGraph.Canon.instInhabitedOrbits = { default := IsoGraph.Canon.instInhabitedOrbits.default }

@[irreducible]

def IsoGraph.Canon.dfsNode (G : Graph) (fuel : Nat) (path : Array Nat) (invPath : Array UInt64) (p : Part) (st : St) : St

Visit one node of the search tree. p is the (already refined) ordered partition, path the vertices individualised to reach it, and invPath the node invariants along that path.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.dfsNode G 0 path invPath p st = st

@[irreducible]

def IsoGraph.Canon.dfsChildren (G : Graph) (fuel : Nat) (path : Array Nat) (invPath : Array UInt64) (p : Part) (verts : List Nat) (processed : Array Nat) (orb : Orbits) (st : St) : St

Visit the remaining children verts of a node, skipping those in the orbit of an already visited child, and honouring any backjump request coming back from below.

Equations

• One or more equations did not get rendered due to their size.
• IsoGraph.Canon.dfsChildren G fuel path invPath p [] processed orb st = st

Entry points

structure IsoGraph.Canon.Result : Type

The result of canonicalisation.

• lab : Array Nat

  The canonical labelling: lab[i]! is the vertex placed at canonical position i.

• cert : Array UInt64

  The canonical form: certOf G lab, one row bitmask per canonical position.

• autos : Array (Array Nat)

  Generators of (a subgroup of) the automorphism group found along the way.

• nodes : Nat

  Number of search-tree nodes visited, for diagnostics.

@[instance_reducible]

instance IsoGraph.Canon.instInhabitedResult : Inhabited Result

Equations

• IsoGraph.Canon.instInhabitedResult = { default := IsoGraph.Canon.instInhabitedResult.default }

def IsoGraph.Canon.canonical (G : Graph) : Result

Compute a canonical labelling of G.

Result.lab is a permutation of {0, …, n-1} such that Result.cert depends only on the isomorphism class of G.

Equations

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

def IsoGraph.Canon.canonicalForm (G : Graph) : Array UInt64

The canonical form of G: an isomorphism invariant that is complete (equal iff isomorphic, for graphs on the same number of vertices).

Equations

• IsoGraph.Canon.canonicalForm G = (IsoGraph.Canon.canonical G).cert

def IsoGraph.Canon.invLab (n : Nat) (a : Array Nat) : Array Nat

Positional inverse of a: if a is a permutation of {0, …, n-1} then this is the array with invLab n a at position a[i]! equal to i. Used only to check that, so nothing is claimed about it when a is not a permutation.

Equations

• IsoGraph.Canon.invLab n a = List.foldl (fun (b : Array Nat) (i : Nat) => if a[i]! < n then b.set! a[i]! i else b) (Array.replicate n 0) (List.range n)

def IsoGraph.Canon.isPermArray (n : Nat) (a : Array Nat) : Bool

Is a a permutation of {0, …, n-1}? O(n): build the positional inverse and check that it really inverts, which gives injectivity for free (if a[v]! = a[w]! then v = b[a[v]!]! = b[a[w]!]! = w).

Equations

• IsoGraph.Canon.isPermArray n a = (a.size == n && have b := IsoGraph.Canon.invLab n a; (List.range n).all fun (i : Nat) => decide (a[i]! < n) && b[a[i]!]! == i)

def IsoGraph.Canon.canonicalLabellingOfOracle (n : Nat) (f : Nat → Nat → Bool) : Array Nat

Canonical labelling from an adjacency oracle.

The search's output is checked to be a permutation of {0, …, n-1} before being returned, and the identity is substituted if it is not. The check costs O(n) against an Ω(n²) search, and makes the returned array a permutation whatever the search does (Spec.labellingIsPerm).

Equations

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

theorem IsoGraph.Canon.Graph.ext {G H : Graph} (hn : G.n = H.n) (hadj : G.adj = H.adj) (hnbr : G.nbr = H.nbr) : G = H

Two graphs are equal when their stored representations are equal.

theorem IsoGraph.Canon.Graph.ext_iff {G H : Graph} : G = H ↔ G.n = H.n ∧ G.adj = H.adj ∧ G.nbr = H.nbr