@[inline]

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

Equations

• Hex.GraphIso.Nauty.mash l i = (l ^^^ 27421) + i &&& 32767

@[inline]

def Hex.GraphIso.Nauty.cleanup (l : Nat) : Nat

nauty's CLEANUP of an accumulated refinement code.

Equations

• Hex.GraphIso.Nauty.cleanup l = l % 32767

structure Hex.GraphIso.Nauty.Ctx (n : Nat) : Type

The graph on n vertices as adjacency rows.

• g : Array (VSet n)

  Row v is the neighbour set of vertex v.

@[instance_reducible]

instance Hex.GraphIso.Nauty.instInhabitedCtx {n : Nat} : Inhabited (Ctx n)

Equations

• Hex.GraphIso.Nauty.instInhabitedCtx = { default := { g := #[] } }

def Hex.GraphIso.Nauty.cellEnd (ptn : Array Nat) (level i : Nat) : Nat

The end position of the cell starting at i in the partition at level: the least j ≥ i with ptn[j] ≤ level.

Equations

• Hex.GraphIso.Nauty.cellEnd ptn level i = Hex.GraphIso.Nauty.cellEnd.go ptn level (ptn.size - i) i

def Hex.GraphIso.Nauty.cellEnd.go (ptn : Array Nat) (level : Nat) : Nat → Nat → Nat

Equations

• Hex.GraphIso.Nauty.cellEnd.go ptn level 0 a✝ = a✝
• Hex.GraphIso.Nauty.cellEnd.go ptn level fuel.succ a✝ = if ptn[a✝]! > level then Hex.GraphIso.Nauty.cellEnd.go ptn level fuel (a✝ + 1) else a✝

def Hex.GraphIso.Nauty.cells (ptn : Array Nat) (level n : Nat) : List (Nat × Nat)

The cells of the partition at level, as (start, end) position pairs in order.

Equations

• Hex.GraphIso.Nauty.cells ptn level n = Hex.GraphIso.Nauty.cells.go ptn level n n 0

def Hex.GraphIso.Nauty.cells.go (ptn : Array Nat) (level n : Nat) : Nat → Nat → List (Nat × Nat)

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.cells.go ptn level n 0 a✝ = []

structure Hex.GraphIso.Nauty.RefineSt (n : Nat) : Type

Working state of one refine call on n vertices. lab and ptn are the partition nest and active the positions of the cells still to be used as splitters, all three nauty's arrays of those names. numcells counts the cells. hint is the position pickSplit tries first on the next iteration. maxpos is the position of the largest fragment of the last nontrivial split, which is the one left out of the active set. longcode is the accumulated refinement code.

• lab : Array Nat
• ptn : Array Nat
• active : VSet n
• numcells : Nat
• hint : Nat
• maxpos : Nat
• longcode : Nat

def Hex.GraphIso.Nauty.pickSplit {n : Nat} (active : VSet n) (hint : Nat) : Option Nat

The next active splitting cell: nauty tries hint first, then the next active position after it, then wraps to the least active position.

Equations

• Hex.GraphIso.Nauty.pickSplit active hint = if active.mem hint = true then some hint else match active.nextElem (some hint) with | some v => some v | none => active.nextElem none

def Hex.GraphIso.Nauty.splitCellLoop {n : Nat} (gRow : VSet n) : Nat → Array Nat → Int → Int → Array Nat × Int × Int

The two-pointer partition of lab[c1..c2] by adjacency to the trivial splitter: adjacent vertices collect on the left in order, non-adjacent vertices on the right in reversed order, exactly as nauty's swap loop leaves them. Returns the final (lab, c1, c2).

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.splitCellLoop gRow 0 x✝² x✝¹ x✝ = (x✝², x✝¹, x✝)

def Hex.GraphIso.Nauty.trivialSplit {n : Nat} (level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineSt n) : RefineSt n

The position-level bookkeeping after a trivial split with final pointers c1, c2: record the new cell end, code, count, active entry, and hint. Touches no labelling data.

Equations

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

def Hex.GraphIso.Nauty.trivialCell {n : Nat} (level : Nat) (gRow : VSet n) (cell1 cell2 : Nat) (st : RefineSt n) : RefineSt n

One cell's processing in the trivial-splitter pass: two-pointer partition by adjacency, then the split bookkeeping.

Equations

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

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

One splitting pass of refine for the trivial splitter cell {lab[split1]}. The splitter row is captured before any cell is processed, as in nauty.

Equations

• Hex.GraphIso.Nauty.refineTrivial ctx level split1 st = Hex.GraphIso.Nauty.refineTrivial.go level ctx.g[st.lab[split1]!]! (Hex.GraphIso.Nauty.cells st.ptn level n) st

def Hex.GraphIso.Nauty.refineTrivial.go {n : Nat} (level : Nat) (gRow : VSet n) : List (Nat × Nat) → RefineSt n → RefineSt n

Equations

• Hex.GraphIso.Nauty.refineTrivial.go level gRow [] a✝ = a✝
• Hex.GraphIso.Nauty.refineTrivial.go level gRow ((cell1, cell2) :: rest) a✝ = Hex.GraphIso.Nauty.refineTrivial.go level gRow rest (Hex.GraphIso.Nauty.trivialCell level gRow cell1 cell2 a✝)

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

refineTrivial with the cell walk fused: boundaries come from a snapshot of the partition (ptn0), taken before the pass writes, so no (start, end) pair list is materialized. Runtime form of refineTrivial.

Equations

• Hex.GraphIso.Nauty.refineTrivialFast ctx level split1 st = Hex.GraphIso.Nauty.refineTrivialFast.go level ctx.g[st.lab[split1]!]! st.ptn n 0 st

def Hex.GraphIso.Nauty.refineTrivialFast.go {n : Nat} (level : Nat) (gRow : VSet n) (ptn0 : Array Nat) : Nat → Nat → RefineSt n → RefineSt n

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.refineTrivialFast.go level gRow ptn0 0 a✝¹ a✝ = a✝

theorem Hex.GraphIso.Nauty.refineTrivialFast_go_eq {n : Nat} (ctx : Ctx n) (level : Nat) (gRow : VSet n) (ptn0 : Array Nat) (fuel c1 : Nat) (st : RefineSt n) : refineTrivialFast.go level gRow ptn0 fuel c1 st = refineTrivial.go level gRow (cells.go ptn0 level n fuel c1) st

@[csimp]

theorem Hex.GraphIso.Nauty.refineTrivial_eq_fast : @refineTrivial = @refineTrivialFast

def Hex.GraphIso.Nauty.worksetOf (n : Nat) (lab : Array Nat) (lo hi : Nat) : VSet n

The splitter cell's vertex set: the members of lab[lo..hi].

Equations

• Hex.GraphIso.Nauty.worksetOf n lab lo hi = List.foldl (fun (w : Hex.GraphIso.Nauty.VSet n) (o : Nat) => w.insert lab[lo + o]!) Hex.GraphIso.Nauty.VSet.empty (List.range (hi + 1 - lo))

def Hex.GraphIso.Nauty.countsOf {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) : List Nat

The neighbour counts of a cell's members into the splitter set, in cell order.

Equations

• Hex.GraphIso.Nauty.countsOf ctx lab workset cell1 cell2 = List.map (fun (o : Nat) => workset.cardInter ctx.g[lab[cell1 + o]!]!) (List.range (cell2 + 1 - cell1))

def Hex.GraphIso.Nauty.multOf (counts : List Nat) (v : Nat) : Nat

The multiplicity of count value v in a count list.

Equations

• Hex.GraphIso.Nauty.multOf counts v = List.countP (fun (x : Nat) => x == v) counts

def Hex.GraphIso.Nauty.windowStep {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : RefineSt n

One nonempty count group's bookkeeping in the window scan: code contribution, maxpos of the largest group so far, the group boundary with its active-set entry, and the new cell end. Touches no labelling data.

Equations

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

def Hex.GraphIso.Nauty.windowScan {n : Nat} (level cell1 cell2 : Nat) (counts : List Nat) : List Nat → Nat → Int → RefineSt n → RefineSt n

The position scan over the count window [bmin, bmax]: register each nonempty group's boundary, code contribution, active-set entry, and the maxpos of the largest group.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.windowScan level cell1 cell2 counts [] x✝² x✝¹ x✝ = x✝

def Hex.GraphIso.Nauty.segmentOf (lab : Array Nat) (cell1 : Nat) (counts values : List Nat) : List Nat

The stable counting sort of a cell segment: members grouped by count value in ascending value order, keeping cell order within a group.

Equations

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

def Hex.GraphIso.Nauty.writeSegment (lab : Array Nat) (cell1 : Nat) : List Nat → Array Nat

Write a segment back at cell1.

Equations

• Hex.GraphIso.Nauty.writeSegment lab cell1 [] = lab
• Hex.GraphIso.Nauty.writeSegment lab cell1 (x_1 :: rest) = Hex.GraphIso.Nauty.writeSegment (lab.set! cell1 x_1) (cell1 + 1) rest

def Hex.GraphIso.Nauty.nontrivialFix {n : Nat} (cell1 : Nat) (st : RefineSt n) : RefineSt n

The active-set fix after a nontrivial split: if the original cell was not active, activate the whole boundary except the largest fragment. Touches no labelling data.

Equations

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

def Hex.GraphIso.Nauty.countValues (counts : List Nat) : List Nat

The value window scanned by the nontrivial splitter: bmin to bmax inclusive.

Equations

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

def Hex.GraphIso.Nauty.nontrivialCell {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (cell1 cell2 : Nat) (st : RefineSt n) : RefineSt n

One cell's processing in the nontrivial-splitter pass.

Equations

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

def Hex.GraphIso.Nauty.ntcPass {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 : Nat) : Nat → Nat → Array Nat → Array Nat → Nat → Nat → Array Nat × Array Nat × Nat × Nat

The counts pass: per-member neighbour counts into the splitter set, the members themselves, and the count extrema, in one walk.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.ntcPass ctx lab workset cell1 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = (x✝³, x✝², x✝¹, x✝)

def Hex.GraphIso.Nauty.ntcBucket (counts : Array Nat) (bmin : Nat) : Nat → Nat → Array Nat → Array Nat

Count multiplicities into a window-sized bucket array.

Equations

• Hex.GraphIso.Nauty.ntcBucket counts bmin 0 x✝¹ x✝ = x✝
• Hex.GraphIso.Nauty.ntcBucket counts bmin fuel.succ x✝¹ x✝ = Hex.GraphIso.Nauty.ntcBucket counts bmin fuel (x✝¹ + 1) (x✝.set! (counts[x✝¹]! - bmin) (x✝[counts[x✝¹]! - bmin]! + 1))

def Hex.GraphIso.Nauty.ntcScan {n : Nat} (level cell1 cell2 bmin : Nat) (bucket : Array Nat) : Nat → Nat → Nat → Int → RefineSt n → RefineSt n

The window scan driven by the bucket array: replays windowStep for each nonempty count group in ascending value order.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.ntcScan level cell1 cell2 bmin bucket 0 x✝³ x✝² x✝¹ x✝ = x✝

def Hex.GraphIso.Nauty.ntcStarts (bucket : Array Nat) : Nat → Nat → Array Nat → Array Nat

Exclusive prefix positions of the count groups, offset to the cell start.

Equations

• Hex.GraphIso.Nauty.ntcStarts bucket 0 x✝¹ x✝ = x✝
• Hex.GraphIso.Nauty.ntcStarts bucket fuel.succ x✝¹ x✝ = Hex.GraphIso.Nauty.ntcStarts bucket fuel (x✝¹ + bucket[x✝.size]!) (x✝.push x✝¹)

def Hex.GraphIso.Nauty.ntcPlace (counts members : Array Nat) (bmin : Nat) : Nat → Nat → Array Nat → Array Nat → Array Nat × Array Nat

The stable placement: one ascending walk over the members, each written at its group's next position.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.ntcPlace counts members bmin 0 x✝² x✝¹ x✝ = (x✝¹, x✝)

def Hex.GraphIso.Nauty.nontrivialCellFast {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (cell1 cell2 : Nat) (st : RefineSt n) : RefineSt n

nontrivialCell as the bucket-array counting sort.

Equations

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

theorem Hex.GraphIso.Nauty.windowStep_lab {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : (windowStep level cell1 cell2 v c1 c2 maxcell st).lab = st.lab

theorem Hex.GraphIso.Nauty.windowScan_lab {n : Nat} (level cell1 cell2 : Nat) (counts vs : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : (windowScan level cell1 cell2 counts vs c1 maxcell st).lab = st.lab

theorem Hex.GraphIso.Nauty.ntcScan_eq_windowScan {n : Nat} (level cell1 cell2 bmin : Nat) (bucket : Array Nat) (counts : List Nat) (fuel j c1 : Nat) (maxcell : Int) (st : RefineSt n) : (∀ (i : Nat), i < fuel → bucket[j + i]! = multOf counts (bmin + j + i)) → ntcScan level cell1 cell2 bmin bucket fuel j c1 maxcell st = windowScan level cell1 cell2 counts (List.map (fun (x : Nat) => bmin + j + x) (List.range fuel)) c1 maxcell st

The bucket-driven scan replays windowScan over an ascending value window whenever the bucket entries are the multiplicities.

theorem Hex.GraphIso.Nauty.writeSegment_outside (seg : List Nat) (lab : Array Nat) (lo q : Nat) : q < lo ∨ lo + seg.length ≤ q → (writeSegment lab lo seg)[q]! = lab[q]!

theorem Hex.GraphIso.Nauty.writeSegment_size (seg : List Nat) (lab : Array Nat) (lo : Nat) : (writeSegment lab lo seg).size = lab.size

theorem Hex.GraphIso.Nauty.ntcPass_spec {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 fuel o : Nat) (counts members : Array Nat) (bmin bmax : Nat) : ntcPass ctx lab workset cell1 fuel o counts members bmin bmax = (counts ++ (List.map (fun (i : Nat) => workset.cardInter ctx.g[lab[cell1 + o + i]!]!) (List.range fuel)).toArray, members ++ (List.map (fun (i : Nat) => lab[cell1 + o + i]!) (List.range fuel)).toArray, List.foldl (fun (b i : Nat) => b.min (workset.cardInter ctx.g[lab[cell1 + o + i]!]!)) bmin (List.range fuel), List.foldl (fun (b i : Nat) => b.max (workset.cardInter ctx.g[lab[cell1 + o + i]!]!)) bmax (List.range fuel))

ntcPass appends the per-member counts and members over its fuel window and folds the extrema, leaving the accumulator prefixes intact.

theorem Hex.GraphIso.Nauty.ntcBucket_spec (counts : Array Nat) (bmin fuel i : Nat) (bucket : Array Nat) : i + fuel ≤ counts.size → (∀ (q : Nat), i ≤ q → q < i + fuel → counts[q]! - bmin < bucket.size) → ∀ (v : Nat), v < bucket.size → (ntcBucket counts bmin fuel i bucket)[v]! = bucket[v]! + List.countP (fun (q : Nat) => counts[q]! - bmin == v) (List.range' i fuel)

ntcBucket accumulates, at slot v, the running bucket count plus the number of processed positions whose count value is bmin + v. Slots are only ever touched in range, so out-of-window reads are preserved.

theorem Hex.GraphIso.Nauty.ntcStarts_size (bucket : Array Nat) (fuel pos : Nat) (starts : Array Nat) : (ntcStarts bucket fuel pos starts).size = starts.size + fuel

ntcStarts appends one entry per fuel step.

theorem Hex.GraphIso.Nauty.ntcStarts_preserve (bucket : Array Nat) (fuel pos : Nat) (starts : Array Nat) (q : Nat) : q < starts.size → (ntcStarts bucket fuel pos starts)[q]! = starts[q]!

Slots below the current size are untouched by ntcStarts.

theorem Hex.GraphIso.Nauty.ntcStarts_value (bucket : Array Nat) (fuel pos : Nat) (starts : Array Nat) (t : Nat) : t < fuel → (ntcStarts bucket fuel pos starts)[starts.size + t]! = pos + (List.map (fun (j : Nat) => bucket[starts.size + j]!) (List.range t)).sum

ntcStarts fills each new slot with the running exclusive prefix sum of the bucket: slot starts.size + t holds pos plus the bucket mass over the intervening window.

theorem Hex.GraphIso.Nauty.countP_lt_succ (c : Nat → Nat) (v : Nat) (l : List Nat) : List.countP (fun (o : Nat) => decide (c o < v + 1)) l = List.countP (fun (o : Nat) => decide (c o < v)) l + List.countP (fun (o : Nat) => c o == v) l

The group base positions tile the cell: the count of members below value v + 1 is the count below v plus the multiplicity of v. This is what makes the group intervals [base v, base v + mult v) disjoint and contiguous, hence the placement injective and size-exact.

theorem Hex.GraphIso.Nauty.getElem!_append_left {α : Type} [Inhabited α] {as bs : List α} {i : Nat} (h : i < as.length) : (as ++ bs)[i]! = as[i]!

Reading an append below the left operand's length reads the left operand.

theorem Hex.GraphIso.Nauty.getElem!_append_right {α : Type} [Inhabited α] {as bs : List α} {i : Nat} (h : as.length ≤ i) (hi : i - as.length < bs.length) : (as ++ bs)[i]! = bs[i - as.length]!

Reading an append at or above the left operand's length reads the right operand.

theorem Hex.GraphIso.Nauty.ntcPass_concrete_counts {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) (h : cell1 ≤ cell2) : (ntcPass ctx lab workset cell1 (cell2 - cell1) 1 ((Array.mkEmpty (cell2 + 1 - cell1)).push (workset.cardInter ctx.g[lab[cell1]!]!)) ((Array.mkEmpty (cell2 + 1 - cell1)).push lab[cell1]!) (workset.cardInter ctx.g[lab[cell1]!]!) (workset.cardInter ctx.g[lab[cell1]!]!)).fst.toList = countsOf ctx lab workset cell1 cell2

The concrete counts pass reconstructs countsOf as its count array.

theorem Hex.GraphIso.Nauty.ntcPass_concrete_members {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) (h : cell1 ≤ cell2) : (ntcPass ctx lab workset cell1 (cell2 - cell1) 1 ((Array.mkEmpty (cell2 + 1 - cell1)).push (workset.cardInter ctx.g[lab[cell1]!]!)) ((Array.mkEmpty (cell2 + 1 - cell1)).push lab[cell1]!) (workset.cardInter ctx.g[lab[cell1]!]!) (workset.cardInter ctx.g[lab[cell1]!]!)).snd.fst.toList = List.map (fun (o : Nat) => lab[cell1 + o]!) (List.range (cell2 + 1 - cell1))

The concrete counts pass records the cell members in cell order.

theorem Hex.GraphIso.Nauty.ntcPlace_size (counts members : Array Nat) (bmin fuel o : Nat) (lab starts : Array Nat) : (ntcPlace counts members bmin fuel o lab starts).fst.size = lab.size

ntcPlace preserves the labelling size (it only overwrites in place).

theorem Hex.GraphIso.Nauty.ntcPlace_starts_size (counts members : Array Nat) (bmin fuel o : Nat) (lab starts : Array Nat) : (ntcPlace counts members bmin fuel o lab starts).snd.size = starts.size

ntcPlace preserves the cursor-array size.

theorem Hex.GraphIso.Nauty.ntcPass_concrete_bmin {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) (h : cell1 ≤ cell2) : (ntcPass ctx lab workset cell1 (cell2 - cell1) 1 ((Array.mkEmpty (cell2 + 1 - cell1)).push (workset.cardInter ctx.g[lab[cell1]!]!)) ((Array.mkEmpty (cell2 + 1 - cell1)).push lab[cell1]!) (workset.cardInter ctx.g[lab[cell1]!]!) (workset.cardInter ctx.g[lab[cell1]!]!)).snd.snd.fst = List.foldl Nat.min ((countsOf ctx lab workset cell1 cell2).headD 0) (countsOf ctx lab workset cell1 cell2)

The concrete counts pass folds the specification's count minimum.

theorem Hex.GraphIso.Nauty.ntcPass_concrete_bmax {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) (h : cell1 ≤ cell2) : (ntcPass ctx lab workset cell1 (cell2 - cell1) 1 ((Array.mkEmpty (cell2 + 1 - cell1)).push (workset.cardInter ctx.g[lab[cell1]!]!)) ((Array.mkEmpty (cell2 + 1 - cell1)).push lab[cell1]!) (workset.cardInter ctx.g[lab[cell1]!]!) (workset.cardInter ctx.g[lab[cell1]!]!)).snd.snd.snd = List.foldl Nat.max ((countsOf ctx lab workset cell1 cell2).headD 0) (countsOf ctx lab workset cell1 cell2)

The concrete counts pass folds the specification's count maximum.

@[csimp]

theorem Hex.GraphIso.Nauty.nontrivialCell_eq_fast : @nontrivialCell = @nontrivialCellFast

The bucket-array counting sort computes the specification's cell processing: one counts pass, the multiplicity bucket, the bucket-driven window scan, and the stable placement replay nontrivialCell exactly. The @[csimp] makes every compiled call site run the O(cell + window) fast path in place of the O(cell x window) multOf scan and segmentOf redistribution.

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

One splitting pass of refine for a nontrivial splitter cell lab[split1..split2].

nauty's bucket scratch is reproduced semantically: the multiplicity window over [bmin, bmax] and the stable counting redistribution give exactly the array contents nauty's incremental window zeroing and placement loop produce.

Equations

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

def Hex.GraphIso.Nauty.refineNontrivial.go {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) : List (Nat × Nat) → RefineSt n → RefineSt n

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.refineNontrivial.go ctx level workset [] a✝ = a✝

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

refineNontrivial with the cell walk fused over a partition snapshot, mirroring refineTrivialFast. Runtime form of refineNontrivial.

Equations

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

def Hex.GraphIso.Nauty.refineNontrivialFast.go {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (ptn0 : Array Nat) : Nat → Nat → RefineSt n → RefineSt n

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.refineNontrivialFast.go ctx level workset ptn0 0 a✝¹ a✝ = a✝

theorem Hex.GraphIso.Nauty.refineNontrivialFast_go_eq {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (ptn0 : Array Nat) (fuel c1 : Nat) (st : RefineSt n) : refineNontrivialFast.go ctx level workset ptn0 fuel c1 st = refineNontrivial.go ctx level workset (cells.go ptn0 level n fuel c1) st

@[csimp]

theorem Hex.GraphIso.Nauty.refineNontrivial_eq_fast : @refineNontrivial = @refineNontrivialFast

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

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

Equations

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

def Hex.GraphIso.Nauty.refineLoop {n : Nat} (ctx : Ctx n) (level : Nat) : Nat → RefineSt n → RefineSt n

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.refineLoop ctx level 0 x✝ = x✝

def Hex.GraphIso.Nauty.refine {n : Nat} (ctx : Ctx n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : 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.

Equations

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

def Hex.GraphIso.Nauty.cheapautom (ptn : Array Nat) (level n : Nat) : Bool

nauty's cheapautom: a cheap sufficient condition for the partition to have automorphisms rearranging only its nontrivial cells.

Equations

• Hex.GraphIso.Nauty.cheapautom ptn level n = match Hex.GraphIso.Nauty.cheapautom.go ptn level n 0 n 0 with | (k, nnt) => decide (k ≤ nnt + 1 ∨ k ≤ 4)

def Hex.GraphIso.Nauty.cheapautom.go (ptn : Array Nat) (level : Nat) : Nat → Nat → Nat → Nat → Nat × Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.cheapautom.go ptn level 0 a✝² a✝¹ a✝ = (a✝¹, a✝)

def Hex.GraphIso.Nauty.bestcellRow {n : Nat} (ctx : Ctx n) (lab startArr : Array Nat) (workset : VSet n) (v2 : Nat) : List Nat → Array Nat → Array Nat

One v2 round of bestcell's joined-cell count: bump the counts of v2 and each earlier nonsingleton cell nontrivially joined to it.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.bestcellRow ctx lab startArr workset v2 [] x✝ = x✝

def Hex.GraphIso.Nauty.bestcellRows {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level : Nat) (startArr : Array Nat) : List Nat → Array Nat → Array Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.bestcellRows ctx lab ptn level startArr [] x✝ = x✝

def Hex.GraphIso.Nauty.argmaxLoop (bucket : Array Nat) : List Nat → Nat → Nat → Nat

The position of the greatest count, first maximum winning.

Equations

• Hex.GraphIso.Nauty.argmaxLoop bucket [] x✝¹ x✝ = x✝¹
• Hex.GraphIso.Nauty.argmaxLoop bucket (i :: rest) x✝¹ x✝ = if bucket[i]! > x✝ then Hex.GraphIso.Nauty.argmaxLoop bucket rest i bucket[i]! else Hex.GraphIso.Nauty.argmaxLoop bucket rest x✝¹ x✝

def Hex.GraphIso.Nauty.bestcell {n : Nat} (ctx : 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.

Equations

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

def Hex.GraphIso.Nauty.targetcell {n : Nat} (ctx : 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.

Equations

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

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

nauty's maketargetcell: the chosen cell's position, contents, and size.

Equations

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

def Hex.GraphIso.Nauty.breakout (n : Nat) (lab ptn : Array Nat) (level tc tv : Nat) : Array Nat × Array Nat × VSet n

nauty's breakout: split {tv} off the front of the cell starting at tc, shifting the displaced vertices one place right, and make tc the only active position.

Equations

• Hex.GraphIso.Nauty.breakout n lab ptn level tc tv = (Hex.GraphIso.Nauty.breakout.go tv (lab.size + 1) lab tc tv, ptn.set! tc level, Hex.GraphIso.Nauty.VSet.empty.insert tc)

def Hex.GraphIso.Nauty.breakout.go (tv : Nat) : Nat → Array Nat → Nat → Nat → Array Nat

Equations

• Hex.GraphIso.Nauty.breakout.go tv 0 a✝² a✝¹ a✝ = a✝²
• Hex.GraphIso.Nauty.breakout.go tv fuel.succ a✝² a✝¹ a✝ = if (a✝²[a✝¹]! == tv) = true then a✝².set! a✝¹ a✝ else Hex.GraphIso.Nauty.breakout.go tv fuel (a✝².set! a✝¹ a✝) (a✝¹ + 1) a✝²[a✝¹]!

def Hex.GraphIso.Nauty.isautom {n : Nat} (ctx : Ctx n) (perm : Array Nat) : Bool

nauty's isautom for undirected graphs: perm maps edges to edges, checking each edge from its lesser endpoint.

Equations

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

def Hex.GraphIso.Nauty.invPerm (lab : Array Nat) : Array Nat

The inverse of a vertex list: inv[lab[i]] = i.

Equations

• Hex.GraphIso.Nauty.invPerm lab = Hex.GraphIso.Nauty.invPerm.go lab (List.range lab.size) (Array.replicate lab.size 0)

def Hex.GraphIso.Nauty.invPerm.go (lab : Array Nat) : List Nat → Array Nat → Array Nat

Equations

• Hex.GraphIso.Nauty.invPerm.go lab [] a✝ = a✝
• Hex.GraphIso.Nauty.invPerm.go lab (v1 :: rest) a✝ = Hex.GraphIso.Nauty.invPerm.go lab rest (a✝.set! lab[v1]! v1)

def Hex.GraphIso.Nauty.testcanlab {n : Nat} (ctx : Ctx n) (canong : Array (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.

Equations

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

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

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

Equations

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

def Hex.GraphIso.Nauty.fmperm (perm : Array Nat) (n : Nat) : VSet n × VSet n

nauty's fmperm: the fixed points of a permutation and the least point of each cycle.

Equations

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

def Hex.GraphIso.Nauty.fmptn (lab ptn : Array Nat) (level n : Nat) : VSet n × VSet n

nauty's fmptn: the vertices in singleton cells of the partition at level, and the least vertex of each cell.

Equations

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

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

Equations

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