theorem
Hex.GraphIso.Nauty.NodeInv.tree
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hg : ctx.g = rowsOf G)
(hn : 0 < n)
(hl : 1 ≤ level)
:
Generation.TreeOk ctx level (refine ctx level st.lab st.ptn st.active numcells)
Refining a valid node preserves the tree's cell-count depth bound.
theorem
Hex.GraphIso.Nauty.sweepStart_fields
{n : Nat}
(ctx : Ctx n)
(level numcells len : Nat)
(st : SearchSt n)
:
Generation.FirstFields st (sweepStart ctx level numcells len st)
Sweep preparation preserves the stored first reference and boundary.
theorem
Hex.GraphIso.Nauty.NodeInv.referenceSweep
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells : Nat}
{codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hn0 : 0 < n)
(hlevel : 2 ≤ level)
(hpath : level = codes.length + 1)
(hspec : level + 1 + specFuel = n + 1)
(hfuel : n + 2 < level + 1 + runFuel)
(hcheap : st.noncheaplevel ≤ level)
(hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells))
(hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail)
(hlive : Live ctx level st trail)
(hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hcoset : st.cosetindex < n)
(hdom : ∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n)
(heq : (otherLeafSt ctx level numcells st).eqlevFirst = level)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have full := codes ++ [rs.longcode];
∃ (tc : Nat), ∃ (len : Nat), have tcell := worksetOf n rs.lab tc (tc + len - 1);
have start := sweepStart ctx level numcells len st;
specMaketargetcell ctx rs.lab rs.ptn level tcLevel = (tc, tcell, len) ∧ OtherSweep G ctx inf tcLevel specFuel runFuel level rs.numcells tc len ((tcell.nextElem none).getD 0)
st.noncheaplevel full fs rs.lab rs.ptn start (n + 1) none tcell start best trail
A first-reference match at an internal node starts a verified sweep of the specification's target cell. Its visit evidence comes from the established totality proof, including the actual pruning decisions.
theorem
Hex.GraphIso.Nauty.other_internal_sweep
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells tc : Nat}
{st : SearchSt n}
{targets : List Nat}
{key : Key n}
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n)
(hok : IterOk ctx level (refine ctx level st.lab st.ptn st.active numcells))
(heq :
Equitable ctx level (refine ctx level st.lab st.ptn st.active numcells).lab
(refine ctx level st.lab st.ptn st.active numcells).ptn)
(hm : Generation.Matches ctx level st (tc :: targets) key)
(hleaf : Generation.HasLeaf ctx tcLevel level (refine ctx level st.lab st.ptn st.active numcells) (tc :: targets) key)
(hlevel : st.eqlevFirst = level - 1)
(hclear : st.needshortprune = false)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have mt := specMaketargetcell ctx rs.lab rs.ptn level tcLevel;
have result :=
otherChildLoop ctx inf tcLevel fuel (n + 1) level rs.numcells mt.fst ((mt.snd.fst.nextElem none).getD 0)
(mt.snd.fst.nextElem none) mt.snd.fst (sweepStart ctx level numcells mt.snd.snd st);
otherNode ctx inf tcLevel (fuel + 1) level numcells st = match result.fst with
| some r => (r, result.snd)
| none => (Int.ofNat level - 1, result.snd)
The matching-node equation uses the same prepared state as the verified loop invariant.