theorem
Hex.GraphIso.Nauty.Sparse.count_neighbors_map
{n : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v)
(s t : RefineSt n)
(ptn : Array Nat)
(level first len : Nat)
(hi : Index.Valid n s.lab ptn level s.cellstart s.cellend)
(hj : Index.Valid n t.lab ptn level t.cellstart t.cellend)
(hp : s.lab.toList.Perm (List.range n))
(hq : t.lab.toList.Perm (List.range n))
(hs : ptn.size = n)
(hend : ptn[n - 1]! ≤ level)
(hc : IsCell ptn level first len)
(hb : first + len ≤ n)
(hperm : cellsPerm ptn level t.lab (Array.map (renamingOf p).toFun s.lab))
(hm : Scratch.Marks n s.stamp s.marks)
(hh : s.hits.size = n)
(hn : Scratch.Marks n t.stamp t.marks)
(hk : t.hits.size = n)
:
have r :=
(have marks := s.marks;
have hits := s.hits;
have touched := #[];
do
let __s ←
forIn [first:first + len] (marks, hits, touched) fun (i : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have hits := __s.fst;
have touched := __s.snd;
have vertex := s.lab[i]!;
do
let __s ←
forIn [G.offsets[vertex]!:G.offsets[vertex + 1]!] (marks, hits, touched)
fun (e : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have hits := __s.fst;
have touched := __s.snd;
have j := (Graph.ofGraph G).neighbor e;
have k := s.cellstart[j]!;
if (k != n) = true then
have __do_jp := fun (__r : Unit) (marks hits touched : Array Nat) =>
have hits := hits.set! j (hits[j]! + 1);
pure (ForInStep.yield (marks, hits, touched));
if (marks[k]! != s.stamp + 1) = true then
have marks := marks.set! k (s.stamp + 1);
have touched := touched.push k;
do
let __s ←
forIn [k:s.cellend[k]! + 1] hits fun (l : Nat) (__s : Array Nat) =>
have hits := __s;
have hits := hits.set! s.lab[l]! 0;
pure (ForInStep.yield hits)
have hits : Array Nat := __s
__do_jp () marks hits touched
else __do_jp () marks hits touched
else pure (ForInStep.yield (marks, hits, touched))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have hits : Array Nat := __s.fst
have touched : Array Nat := __s.snd
pure (ForInStep.yield (marks, hits, touched))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have hits : Array Nat := __s.fst
have touched : Array Nat := __s.snd
pure (marks, sortCells touched, hits)).run;
have u :=
(have marks := t.marks;
have hits := t.hits;
have touched := #[];
do
let __s ←
forIn [first:first + len] (marks, hits, touched) fun (i : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have hits := __s.fst;
have touched := __s.snd;
have vertex := t.lab[i]!;
do
let __s ←
forIn [H.offsets[vertex]!:H.offsets[vertex + 1]!] (marks, hits, touched)
fun (e : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have hits := __s.fst;
have touched := __s.snd;
have j := (Graph.ofGraph H).neighbor e;
have k := t.cellstart[j]!;
if (k != n) = true then
have __do_jp := fun (__r : Unit) (marks hits touched : Array Nat) =>
have hits := hits.set! j (hits[j]! + 1);
pure (ForInStep.yield (marks, hits, touched));
if (marks[k]! != t.stamp + 1) = true then
have marks := marks.set! k (t.stamp + 1);
have touched := touched.push k;
do
let __s ←
forIn [k:t.cellend[k]! + 1] hits fun (l : Nat) (__s : Array Nat) =>
have hits := __s;
have hits := hits.set! t.lab[l]! 0;
pure (ForInStep.yield hits)
have hits : Array Nat := __s
__do_jp () marks hits touched
else __do_jp () marks hits touched
else pure (ForInStep.yield (marks, hits, touched))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have hits : Array Nat := __s.fst
have touched : Array Nat := __s.snd
pure (ForInStep.yield (marks, hits, touched))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have hits : Array Nat := __s.fst
have touched : Array Nat := __s.snd
pure (marks, sortCells touched, hits)).run;
r.snd.fst = u.snd.fst ∧ ∀ (v : Nat), v < n → s.cellstart[v]! ∈ r.snd.fst.toList → u.snd.snd[(renamingOf p).toFun v]! = r.snd.snd[v]!
The executed nontrivial native scans return the same sorted touched cells and transported hit values on those cells. Both their incoming scratch and their traversal orders may differ.