Documentation

HexGraphIso.Nauty.Sparse.Scratch

source
structure Hex.GraphIso.Nauty.Sparse.Scratch.Bounded (n : Nat) (s : Scratch) :
Prop

Persistent storage bounds. Hit counts are unrestricted: the executable clears each touched cell before reading counts in a new refinement pass.

Instances For
    source
    structure Hex.GraphIso.Nauty.Sparse.Scratch.Valid (n : Nat) (lab ptn : Array Nat) (level : Nat) (s : Scratch) extends Hex.GraphIso.Nauty.Sparse.Scratch.Bounded n s :
    Prop

    Cache validity is tied to the current partition only while its flag is set.

    Instances For
      source
      theorem Hex.GraphIso.Nauty.Sparse.Scratch.fresh_valid (n : Nat) (lab ptn : Array Nat) (level : Nat) :
      Valid n lab ptn level (fresh n)
      source
      theorem Hex.GraphIso.Nauty.Sparse.Scratch.Bounded.invalidate {n : Nat} {s : Scratch} (h : Bounded n s) (lab ptn : Array Nat) (level : Nat) :
      Valid n lab ptn level { cellstart := s.cellstart, cellend := s.cellend, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp }

      Invalidating cached indices permits a different partition and labelling while retaining the allocated arrays and generation bounds.

      source
      theorem Hex.GraphIso.Nauty.Sparse.Scratch.Bounded.with_hits {n : Nat} {s : Scratch} (h : Bounded n s) (hits : Array Nat) (hs : hits.size = n) :
      Bounded n { cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp }
      source
      theorem Hex.GraphIso.Nauty.Sparse.Scratch.Valid.with_hits {n level : Nat} {lab ptn : Array Nat} {s : Scratch} (h : Valid n lab ptn level s) (hits : Array Nat) (hs : hits.size = n) :
      Valid n lab ptn level { cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp }

      Borrowing the count array leaves the partition and mark invariants intact.

      source
      theorem Hex.GraphIso.Nauty.Sparse.bestcellCached_scratch {n : Nat} (g : Graph n) (lab : Array Nat) (s : Scratch) :
      have out := (bestcellCached g lab s).snd; out = { cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := out.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp } ∧ out.hits.size = s.hits.size

      Target selection changes only hit counts and preserves their allocation.

      source
      theorem Hex.GraphIso.Nauty.Sparse.bestcellCached_valid {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level : Nat) (s : Scratch) (h : Scratch.Valid n lab ptn level s) :
      Scratch.Valid n lab ptn level (bestcellCached g lab s).snd
      source
      theorem Hex.GraphIso.Nauty.Sparse.bestcellCached_bounded {n : Nat} (g : Graph n) (lab : Array Nat) (s : Scratch) (h : Scratch.Bounded n s) :
      Scratch.Bounded n (bestcellCached g lab s).snd

      Allocation and generation preservation does not require valid indices.

      source
      theorem Hex.GraphIso.Nauty.Sparse.maketargetCached_valid {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (s : Scratch) (h : Scratch.Valid n lab ptn level s) :
      Scratch.Valid n lab ptn level (maketargetCached g lab ptn level tcLevel hint s).snd.snd.snd

      Both target dispatch paths retain scratch validity, including borrowed counts and the fallback used after invalidation.

      source
      theorem Hex.GraphIso.Nauty.Sparse.maketargetCached_bounded {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (s : Scratch) (h : Scratch.Bounded n s) :
      Scratch.Bounded n (maketargetCached g lab ptn level tcLevel hint s).snd.snd.snd