theorem Hex.GraphIso.Nauty.storePolicy {n : Nat} (ctx : Ctx n) (inf tcLevel : Nat) : Generic.StablePolicy ctx inf tcLevel (fun (st : Search n) => CanongInv ctx st.canong st.canonlab st.samerows) (fun (x : Nat) => True) fun (leaf : Generic.Leaf) (st : Search n) => ∀ (sr : Nat), leaf = Generic.Leaf.better sr → CanongInv ctx st.canong st.lab sr

Every off-path operation preserves the canonical row cache; a better verdict supplies the candidate prefix required by installation.

theorem Hex.GraphIso.Nauty.node_store {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells : Nat} {st : Search n} (h : CanongInv ctx st.canong st.canonlab st.samerows) : have out := (node false ctx inf tcLevel fuel level numcells st).snd; CanongInv ctx out.canong out.canonlab out.samerows

An off-path search call preserves the canonical row-store invariant.

theorem Hex.GraphIso.Nauty.sweep_store {n : Nat} {ctx : Ctx n} {first : Bool} {inf tcLevel fuel cfuel level numcells tc tv1 index : Nat} {cursor : Option Nat} {cell : VSet n} {st : Search n} (h : CanongInv ctx st.canong st.canonlab st.samerows) (hpast : Generic.Past first tv1 cursor) : have out := (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd; CanongInv ctx out.canong out.canonlab out.samerows

Later siblings preserve the canonical row-store invariant through every exit.

theorem Hex.GraphIso.Nauty.firstPath_canong {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) : leaf.canong = st.canong

Before its first leaf the search has not changed the canonical row array.

theorem Hex.GraphIso.Nauty.firstPath_store {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) (hsize : st.canong.size = n) : have out := (node true ctx inf tcLevel fuel level numcells st).snd; CanongInv ctx out.canong out.canonlab out.samerows

A successful first-path call initializes and preserves the canonical row cache.

theorem Hex.GraphIso.Nauty.runState_store {n k : Nat} (G : Colored n k) : have out := (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd; CanongInv { g := rowsOf G } out.canong out.canonlab out.samerows

The complete search run has a valid canonical row cache.