Equivariance of the pieces of the canonical labelling #
This file works at the level of IsoGraph.Canon.Algorithm: raw Array Nats, and permutations of
{0, …, n-1} represented as Nat → Nat. The translation to Equiv.Perm (Fin n) happens in
IsoGraph/Canon/Spec.lean.
Fix a renaming σ of the vertices and write q ≈ p for "the ordered partitions q and p have
the same cell boundaries, and the i-th cell of q is the σ-image of the i-th cell of p
as a set" (PartEquiv). Only as a set: refinement's counting sort is stable, so the order
within a cell is inherited from the parent cell and therefore does depend on the vertex names.
What is invariant is the sequence of cells.
Each piece of the search respects ≈:
Graph.ofOracletransforms along a renaming, and the labelling really is a permutation of the vertices (canonicalLabellingOfOraclechecks that at run time);Part.WFandPartEquivare the vocabulary — "well-formed ordered partition" and "the same partition up to renaming" — that everything else is phrased in;cellCount_equiv: corresponding cells agree on every count;countFrom_cellCount: the counting phase ofrefineStepcomputes exactly such a count (countFrom_equivcombines the two);countFrom_mem_touched: the set of vertices that phase records is invariant too;collect_equiv: the two runs go on to split the very same list of cells, in the very same order;- the two readers of a partition,
shapeHashandtargetCell, see only cell boundaries, so they agree on partitions related by any renaming; - individualising corresponding vertices of related partitions gives related partitions, at the
same position (
individualize_partEquiv), and preserves well-formedness; - two runs that reach related discrete partitions read off the same certificate
(
certOf_of_partEquiv, viacertOf_relabel), withdiscrete_of_targetCell_nonesupplying the discreteness at the leaves.
Permutations of an initial segment #
σ permutes {0, …, n-1}: it maps the segment into itself and is injective there. Since
the segment is finite this is the same as being a bijection of it, but the two clauses are what
the proofs actually use.
σmaps the segment into itself.σis injective on the segment.
Instances For
The identity labelling is a permutation — the fallback branch of
canonicalLabellingOfOracle.
isPermArray is sound: what it accepts really is a permutation of {0, …, n-1}. (It is
also complete, but nothing below needs that — an unsound accept would be the problem.)
The labelling really is a labelling. Not because the search is known to produce one —
that is still open — but because canonicalLabellingOfOracle checks, and falls back to the
identity if the check fails.
Graph.ofOracle #
The algorithm never reads an oracle directly: it reads the adj matrix and the nbr lists that
Graph.ofOracle builds from it. So every statement about renaming vertices has to pass through
these three lemmas.
The number of neighbour lists is the number of vertices.
Readers of a partition that see only the cell boundaries #
Step 2 of the decomposition: shapeHash and targetCell walk the partition cell by cell using
cen alone, never touching lab. So they agree on any two partitions with the same boundaries
— in particular on partitions related by a renaming of the vertices, whatever that renaming does
inside the cells.
The walk only reports a cell start it has already checked is < n.
The target cell, when there is one, is a cell start inside the vertex set that is not a singleton. (Used to know that individualising is legitimate.)
Certificates #
Step 4 of the decomposition, certificate half. A certificate is the adjacency matrix read in the
order given by lab; so renaming the vertices along σ and reading in the order lab gives the
same bits as leaving the graph alone and reading in the order σ ∘ lab. This is the point at
which "the search found corresponding leaves" turns into "the two runs return the same array".
One packed row only reads columns j < n. The fuel invariant j + fuel = n is what makes
that available: it says the loop is at position j with fuel columns left, so fuel ≥ 1
forces j < n.
Certificates are equivariant. Reading the renamed graph along lab is reading the
original along σ ∘ lab.
Partitions related by a renaming #
The vocabulary the rest of the decomposition is phrased in. Fix a renaming σ and think of two
runs of the algorithm: one on f, one on the graph fun v w => f (σ v) (σ w) whose vertex v
"is" vertex σ v of the first. The two runs do not produce partitions that agree positionwise
under σ — they both start from Part.unit n, whose lab is Array.range n in either run, and
refinement's counting sort is stable, so the order within a cell is inherited from the parent
and depends on vertex names. What they do produce is partitions whose cells sit at the same
positions and correspond as sets, which is what PartEquiv says.
p is a well-formed ordered partition of {0, …, n-1}: lab and pos are mutually inverse
bijections of the segment, and cst/cen mark off a decomposition of it into intervals.
The last two clauses are what make cst/cen describe cells rather than arbitrary bounds: the
interval [cst[i], cen[i]) is the same for every i inside it, so cst[i] is a well-defined name
for the cell containing position i.
labcovers the segment.poscovers the segment.cstcovers the segment.cencovers the segment.Positions hold vertices of the segment.
Vertices sit at positions in the segment.
posis a left inverse oflab.labis a left inverse ofpos.A cell starts at or before each of its positions.
A cell ends after each of its positions.
Cells stay inside the segment.
Every position of a cell reports the same start.
Every position of a cell reports the same end.
Instances For
Cells are determined by their starts. Two positions report the same cell start exactly
when they lie in the same interval — so cst really is a set-theoretic partition of positions,
not just a monotone pair of arrays. This is the workhorse behind individualize_cell.
A partition the walk finds no target in is discrete. This is what discharges the
Discrete hypotheses of step 4 at the leaves of the search: the algorithm stops individualising
exactly when targetCell returns none, and that is the same condition.
p and q are the same ordered partition up to the renaming σ: the cells occupy the same
ranges of positions, and vertex v of q's graph lies in the cell where σ v lies in p.
The third clause is how "the cells correspond as sets" is said pointwise: a cell is named by its
start position, so it asserts that σ maps the cell of v in q onto the cell at the same
place in p.
Cells start at the same positions.
Cells end at the same positions.
σcarries the cell ofvinqto the cell at the same position inp.
Instances For
The search starts from a well-formed partition: one cell, [0, n), in vertex order.
Once the partitions are discrete, σ relates the labellings positionwise. This is where
"cells correspond as sets" turns into an equation between arrays: a singleton cell has only one
member, so there is nothing left for the stable sort to have permuted.
Step 4 of the decomposition. Two runs that reach related discrete partitions read off
the same certificate — the renamed graph along q.lab is the original along p.lab. This is
the point at which "the search found corresponding leaves" becomes "the two runs return the same
array".
Step 3 of the decomposition: individualisation #
individualize p v splits v off to the front of its cell. The two runs pick different
vertices to displace — p.lab[c] need not be σ (q.lab[c]), since the order inside a cell is
name-dependent — so the arrays are genuinely different. What survives is exactly what PartEquiv
records: the cell boundaries move the same way, and a vertex other than the individualised one
lands in the second fragment of the old cell precisely when it was in that cell to begin with.
The facts about p that every statement below is phrased in: v sits at position i, whose
cell is [c, ec), and u is the vertex displaced from the front of that cell.
vis a vertex of the segment.iis wherevsits.cis the start ofi's cell.ecis its end.uis the vertex at the front of it.
Instances For
The cell of each vertex after individualisation. v gets the singleton cell c;
everything else that was in v's cell moves to c + 1; everything else is untouched. Note that
this says nothing about where inside its cell a vertex sits — which is exactly why it is stable
under a renaming that reorders cells internally.
Individualisation preserves well-formedness. lab/pos stay inverse because the update
is a transposition, and cst/cen still describe intervals because [c, ec) was cut in two.
Step 3 of the decomposition. Individualising corresponding vertices of related partitions gives related partitions, and at the same position — so the two runs stay in step through the branch, and the recursive call sees the same splitter.
What refineStep counts #
refineStep is the one piece of the algorithm whose equivariance is not positionwise. Every
other loop walks positions, and corresponding positions hold corresponding data; but the counting
phase walks a cell in lab order, and corresponding cells are related only as sets. So the
quantity it computes has to be described set-theoretically before it can be shown invariant, and
that description is cellCount: the number of vertices of a given cell satisfying a predicate.
The arithmetic comes first (cellCount_equiv: the quantity is invariant), then the first of
refineStep's loops (countFrom_cellCount: the loop computes the quantity).
How many vertices of the cell starting at position s satisfy P. Every number
refineStep computes is of this form: the neighbour count of v is P w := adj w v, a bucket
size in the counting sort is P w := cnt w == t, and a cell size is P w := true.
Equations
Instances For
The arithmetic behind step 1. Corresponding cells have the same size, and more generally
agree on any count, because σ restricts to a bijection between them. Note this is a genuine
cardinality argument — there is no order-preserving correspondence to appeal to.
The counting loop #
countFrom is phase (1) of refineStep: it walks the splitter cell lab[s:e] and, for every
vertex w, accumulates in cnt[w] the number of cell members adjacent to w. Written as a
for loop this would be out of reach — see the note on cenHashFrom — so Algorithm.lean gives
it as a structural recursion on fuel, and the three lemmas below read the result off.
The bridge to cellCount is List.count: the inner loop bumps cnt[w] once per occurrence of
w in a neighbour list, and Graph.ofOracle's neighbour lists are filtered ranges, hence
duplicate-free, so each cell member contributes at most one.
The inner loop adds to cnt[w] the multiplicity of w in the part of the neighbour list it
scans. Entries of nbrs outside cnt write nothing, but they are not w either, so the
statement needs no hypothesis on them.
Unfolding lemma for the outer loop. The definition destructures the inner loop's result
rather than projecting it (that is what keeps cnt unshared, see Algorithm.lean), and
definitional eta for structures makes the two forms interchangeable.
What the counting phase computes. Run from cleared scratch over the cell starting at
position s, countFrom leaves cnt[w] holding the number of vertices of that cell adjacent to
w — that is, exactly cellCount n p s (· is adjacent to w).
With cellCount_equiv, which says that quantity is invariant, this says the loop computes an
invariant.
The counting phase of refineStep is equivariant. Putting the two halves together: in
two runs whose partitions correspond under σ, the count the f-run records at σ w is the one
the f ∘ σ-run records at w. Note the cells need only correspond as sets — the two runs walk
them in different orders, and the proof goes through cellCount precisely to avoid caring.
The invariant the counting phase maintains on its scratch space: touched lists exactly the
vertices whose count is nonzero, each once.
refineStep needs both halves. Completeness is what makes the collected cells the right ones —
a cell met by the splitter has a member with a nonzero count, so it is represented. Soundness
and no-repetition are what make the restore loop at the end of the step put the scratch back
exactly, in time proportional to what was dirtied rather than to n.
No vertex is recorded twice.
Only vertices are recorded.
Recorded is the same as counted.
Instances For
The inner loop maintains the scratch invariant: it pushes a vertex exactly when it is raising
that vertex's count off zero. The hypothesis on nbrs is needed — a neighbour outside cnt
would leave the count at the getElem! default of 0 and so be pushed on every visit.
The counting phase as refineStep actually calls it, from cleared scratch.
The vertices the counting phase records form an invariant set. touched is exactly the
set of vertices that the splitter cell reaches, and membership is stated in terms of cellCount,
which cellCount_equiv shows corresponding runs agree on.
The order of touched is not invariant — it is first-touch order, which depends on vertex
names. That is why refineStep maps it to cell starts and sorts before using it.
Collecting the cells met by the splitter #
Phase (2) of refineStep turns the touched vertices into the list of cells that have to be split.
Its output has to be canonical in a stronger sense than phase (1)'s: not just the same set of
cells in both runs, but the same array, since the step then processes them in order. That is
what the sort is for, and why sortNats goes through List.mergeSort rather than Array.qsort —
qsort has no specification in this toolchain, and an unspecified order is exactly what cannot be
tolerated here. sortNats_ext is the punchline of the sorting half ("duplicate-free arrays with
the same elements sort alike"), collect_equiv of the whole phase.
The scratch invariant of the collection phase: cells lists exactly the cell starts marked
in hit, each once. The analogue of Touched for phase (2).
No cell is collected twice — this is what
hitis for.Collected cells are in range.
hitmarks exactly the collected cells.
Instances For
What the collection phase collects: exactly the cell starts of the vertices it is given,
each once (the Nodup half is collectFrom_collected).
The collection phase as refineStep runs it: from an all-clear hit, it collects exactly the
cells that the touched vertices lie in.
Phase (2) of refineStep is equivariant. The two runs meet the same cells, in the same
order: the cells are the same positions because PartEquiv matches cell boundaries, and the
sort makes the order depend on nothing but the set.
The counting sort #
The heart of refineStep: each cell that the splitter met is sorted by neighbour count. The
sort is a counting sort in five passes — count the buckets (bucketFrom), turn the counts into
offsets (offsetFrom), scatter the vertices into a block (scatterFrom), write the block back
(writeFrom), install the new fragment boundaries (boundsFrom) — and each pass gets its own
getElem! characterisation here. The one substantial argument is scatterFrom_block: the
scatter writes each vertex to a distinct slot, which needs the buckets' offset ranges to be
disjoint (Sep) and is what makes the whole thing a permutation of the cell.
The bucket table and the list of occurring counts satisfy the same invariant as the count
array and its touched list: ks lists exactly the counts with a nonzero bucket, each once.
The offset the scatter writes the vertex at position i to, as seen from position k: the
bucket's current offset plus the number of items of the same count already scattered.
Equations
Instances For
The buckets do not overlap: distinct counts have disjoint offset ranges, each as wide as the number of items still to be scattered into it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Writing the sorted block back #
The fragment boundaries #
The total size of the fragments [a, b).
Equations
- IsoGraph.Canon.sizesSum sizes a b = ∑ j ∈ Finset.Ico a b, sizes[j]!
Instances For
The boundaries the split installs. Every position of fragment j' reports that
fragment's range.
Odds and ends: array extensionality, the leftover bucket counters, clearing scratch #
The fragment starts and the trace do not depend on the boundary arrays being written.
Where the fragment of neighbour count t starts: after every vertex of the cell with a
smaller count. The point of this description is that it never mentions the bucket list, so two
runs of refineStep on isomorphic inputs manifestly agree on it.
Equations
- IsoGraph.Canon.fragStart n p cnt c t = c + ∑ t' ∈ Finset.range t, IsoGraph.Canon.cellCount n p c fun (u : ℕ) => cnt[u]! == t'
Instances For
The prefix sums the algorithm computes are the fragment starts. The bucket list is sorted and holds exactly the counts that occur, so summing along it is summing over all smaller counts.
What splitting one cell does. Outside the cell [c, cen[c]) nothing moves; inside, each
vertex lands in the fragment of its neighbour count, and the fragments sit in increasing order of
count. Everything is phrased through fragStart/cellCount, which mention only the cell as a
set — that is what makes the description equivariant.
- wf : Part.WF n p'
The result is still a partition.
Positions outside the cell keep their vertex.
Positions outside the cell keep their cell start.
Positions outside the cell keep their cell end.
Vertices outside the cell keep their position.
- pos_mem (v : ℕ) : v < n → c ≤ p.pos[v]! → p.pos[v]! < p.cen[c]! → c ≤ p'.pos[v]! ∧ p'.pos[v]! < p.cen[c]!
Vertices of the cell stay in it.
- cell (v : ℕ) : v < n → c ≤ p.pos[v]! → p.pos[v]! < p.cen[c]! → p'.cst[p'.pos[v]!]! = fragStart n p cnt c cnt[v]!
A vertex of the cell lands in the fragment of its count.
- cen_cell (v : ℕ) : v < n → c ≤ p.pos[v]! → p.pos[v]! < p.cen[c]! → p'.cen[p'.pos[v]!]! = fragStart n p cnt c cnt[v]! + cellCount n p c fun (u : ℕ) => cnt[u]! == cnt[v]!
That fragment is as long as the number of cell vertices of that count.
Instances For
A cell whose vertices all have the same count does not split. Both easy branches of
splitCell are this: the cell is a singleton, or the counting pass found a single bucket.
The counting sort is a permutation of the cell #
Everything the scatter needs is packaged in Offsets: the counts occurring in the cell, in some
order and without duplicates (ks), their bucket sizes (sizes) and the offset each bucket was
given (bc1, the prefix sums). From that alone the scatter is a bijection from the cell onto
[0, ec - c).
What the count-and-offset passes leave behind.
The counts are listed once each.
sizes[j]is the size of bucketks[j].Bucket
ks[j]was given the offset just past all earlier buckets.Every count occurring in the cell is listed.
Instances For
Reading off one step of splitCell #
splitCell has three branches; these equations name the state each one produces, so that the
rest of the file never has to unfold splitCell again: unfolding it in place would leave the
trace hash of the branch in the goal, and deciding whether two such hashes agree is something the
kernel should never be asked to do.
A cell with a single bucket: again only the trace hash moves (and the bucket counter is put back).
The general branch, with each pass of the counting sort named.
The partition after a one-bucket cell "splits": unchanged.
The partition after a genuine split.
The general branch of splitCell: the counting sort really does sort the cell into
fragments by count, and installs the fragment boundaries.
The split is equivariant. Two corresponding cells are split into corresponding fragments: the fragment of a vertex is determined by its count, and corresponding vertices have corresponding counts, so the two runs lay their cells out identically.
Reading off the scratch fields of one splitCell step #
The same branch equations again, now for the fields the partition proofs ignore: the trace, the worklist, and the bucket scratch.
The bucket scratch array is restored. Whatever branch it takes, splitCell hands back a
bc of the same size and again all zero, so the next split can run on it.
What the bucketing and offset passes leave behind, in a form that mentions neither the size of the scratch array nor the order the counts were met in: the counts are listed once each, they are exactly the counts occurring in the cell, and the fragment sizes are their bucket sizes.
The scratch fields move in lockstep too. Corresponding cells hash to the same trace and queue the same fragments: the branch taken, the fragment sizes and the fragment starts are all determined by data the two runs share.
One refinement step #
Everything above is about a single cell. splitCellsFrom walks a list of cells, so the facts have
to be packaged into an invariant that survives the walk.
What a split step needs of its state: a well-formed partition, a cleared bucket array, and counts that index into it.
The partition is well-formed.
The bucket scratch has one slot per possible count.
The bucket scratch is cleared.
Every count indexes the bucket scratch.
Instances For
What two split states run in parallel share: corresponding partitions, and identical trace and worklist.
The partitions correspond under
σ.The traces agree.
The worklists agree.
Instances For
A split step preserves the relation: this is step 1 for a single cell.
Splitting a list of distinct cells preserves the invariant.
Step 1 for a refinement pass. Two runs that split the same list of cells with corresponding counts stay in correspondence.
Reading off one refinement step #
The scratch space is restored, and the partition stays well-formed #
Sorting the collected cells changes neither the invariant nor the marks.
Every vertex the counting phase touches is a vertex — packaged for a named result.
The cells the collection phase gathers are distinct cell starts.
The state the cell loop starts from satisfies its invariant.
What one refinement step leaves behind. The partition is still well-formed, the cells it split are cells of the old partition, and the scratch space is back to its cleared state — the last point is what lets the worklist loop keep reusing it.
One refinement step is equivariant #
Step 1. One refinement pass commutes with relabelling: run on corresponding partitions with corresponding adjacency oracles it produces corresponding partitions, the same worklist and the same trace.
Reading off the worklist loop #
The worklist loop is equivariant #
Step 1 for a whole refinement. Two runs of the worklist loop on corresponding partitions stay in correspondence and produce the same trace. The two runs pop the same positions in the same order, because the worklist is literally the same array in both.
The worklist loop keeps the partition well-formed.
Refinement from a partition, and from the unit partition #
Step 1. The initial equitable refinement is equivariant.
Certificate readback #
The search compares packed certificates; certOf_get below turns an equality of certificates
back into an equality of adjacency entries, which is what Spec.LabellingInvariant asks for.
The accumulator invariant of certRow: acc holds the bits of columns
64 * (j / 64) … j - 1, right-aligned, with column j - 1 at bit 0.
Equations
Instances For
The search only ever stores honest leaves #
Two facts about every leaf the search records: its labelling is a permutation of the vertices,
and its certificate is the certificate of that labelling. Together they say that the winner
returned by canonical passes the isPermArray check of canonicalLabellingOfOracle and that
Result.cert and Result.lab belong together, which is what turns an equality of certificates
into Spec.LabellingInvariant.
A stored leaf whose labelling is a vertex permutation and whose certificate matches it.
The labelling has one entry per vertex.
Its entries are vertices.
Distinct positions hold distinct vertices.
The stored certificate is the one the labelling determines.
Instances For
Every leaf a state remembers is honest.
Equations
- IsoGraph.Canon.StOk G st = ((∀ (l : IsoGraph.Canon.Leaf), st.best = some l → IsoGraph.Canon.LeafOk G l) ∧ ∀ (l : IsoGraph.Canon.Leaf), st.first = some l → IsoGraph.Canon.LeafOk G l)
Instances For
Branch equations for the search #
dfsNode and dfsChildren are written as one match/if cascade each, with lets naming the
intermediate states. Rewriting inside those lets is painful, so each branch gets an equation
here, stated with the intermediates named by orbRefresh and unwind. Proofs elsewhere only
ever use these, never the definitions.
Every leaf the search stores is honest. By functional induction over the two mutually
recursive halves of the search: the only place a leaf is created is leafUpdate, and there it is
built from the lab of the current partition, which the refinement keeps well-formed.
isPermArray is complete #
isPermArray_spec says an accept is honest. Here is the converse: an honest array is accepted.
That is what turns canonicalLabellingOfOracle's if into a no-op, so that the labelling really
is the search's output and not the identity fallback.
The search's output is an honest leaf #
The canonical labelling is a permutation and its certificate is the graph read at it.
With the check now known to pass, the labelling is the search's output.