theorem
Hex.GraphIso.Nauty.firstSweep_safe
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(level numcells tc tv index : Nat)
(cell : VSet n)
(st : Search n)
(horbit : st.orbits[tv]! = tv)
(hchild : RunInv G ctx (node true ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).snd)
(hready :
have out := (node true ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).snd;
have left :=
have __src := afterChildFirst level tv out;
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits,
fixedpts := out.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode,
canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab,
canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst,
eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon,
canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel,
cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes,
tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits,
numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel,
order := __src.order, genTrace := __src.genTrace, workperm := __src.workperm };
SweepPre G ctx tcLevel true level numcells tc tv none cell (recover (n + 2) level left))
:
A sweep's first child establishes the state used by every later off-path sibling.
theorem
Hex.GraphIso.Nauty.node_first
{n : Nat}
(ctx : Ctx n)
(inf tcLevel fuel level numcells : Nat)
(st : Search n)
:
node true ctx inf tcLevel (fuel + 1) level numcells st = (have r := Generic.prepareFirst ctx tcLevel level numcells st;
if (r.fst == n) = true then pure (Generic.Exit.unwind (level - 1) false, firstterminal level r.snd.snd.snd.snd)
else have s :=
sweep true ctx inf tcLevel fuel (n + 1) level r.fst r.snd.fst.toNat ((r.snd.snd.fst.nextElem none).getD 0)
(r.snd.snd.fst.nextElem none) r.snd.snd.fst 0 (cheapCheck true level r.snd.snd.snd.snd);
match s.fst with
| Generic.Exit.done =>
pure (Generic.Exit.unwind (level - 1) false, afterSweep true level r.snd.snd.snd.fst s.snd.fst s.snd.snd)
| x => pure (s.fst, s.snd.snd)).run
A first-path node consists of its prepared partition and the sweep of its chosen target.
theorem
Hex.GraphIso.Nauty.FirstPre.firstterminal
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{level numcells : Nat}
{st : Search n}
(h : FirstPre G ctx level numcells st)
(hn0 : 0 < n)
(tcLevel : Nat)
:
RunInv G ctx (Nauty.firstterminal level (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd)
Installing the first leaf establishes the persistent invariant.
theorem
Hex.GraphIso.Nauty.firstPath_safe
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
(hin : FirstPre G ctx level numcells st)
:
The first descent establishes the off-path invariant before any later sibling can be searched.
theorem
Hex.GraphIso.Nauty.initial_firstPre
{n k : Nat}
(G : Colored n k)
(hn0 : 0 < n)
:
FirstPre G { g := rowsOf G } 1 (initialPartition G).snd.length
(initial n (initialPartition G).fst (initialPartition G).snd)
The coloured initial state satisfies the first-descent entry conditions.
The complete search's generator trace is valid, including the empty graph.
theorem
Hex.GraphIso.Nauty.runColoredTraced_checked
{n k : Nat}
(G : Colored n k)
{γ : Array Nat}
(hγ : γ ∈ (runColoredTraced G).autos)
:
Every automorphism reported by the search passes the certificate check.