def
Hex.GraphIso.Nauty.safetyContract
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel : Nat)
:
Generic.Contract (Search n) n
The off-path induction preserves all installed data, including the checked generator trace.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.safety_node
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{next : Generic.SweepFn (Search n) 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)
(hnext : (safetyContract G ctx tcLevel).sweepValid fuel (n + 1) next)
(level numcells : Nat)
(st : Search n)
(hin : NodePre G ctx tcLevel level numcells st)
:
RunInv G ctx (Generic.nodeStep ctx tcLevel next false level numcells st).snd
Refinement, comparison and classification meet the off-path node contract.
theorem
Hex.GraphIso.Nauty.safety_advance
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{next : Generic.SweepFn (Search n) n}
(hnext : (safetyContract G ctx tcLevel).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(out : Search n)
(exit : Exit)
(hstored : RunInv G ctx out)
(hready : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell (recover (n + 2) level out))
:
RunInv G ctx (Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit).snd.snd
Pruning removes target vertices; every resumed cursor receives the recovered history.
theorem
Hex.GraphIso.Nauty.safety_sweep
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{next : Generic.SweepFn (Search n) 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)
(hdescend : (safetyContract G ctx tcLevel).nodeValid fuel (Generic.nodeCall ctx (n + 2) tcLevel fuel))
(hnext : (safetyContract G ctx tcLevel).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(st : Search n)
(hin : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st)
:
RunInv G ctx
(Generic.sweepStep (n + 2) (Generic.nodeCall ctx (n + 2) tcLevel fuel) next first level numcells tc tv1 tv cell index
st).snd.snd
Each later sibling calls an off-path child and resumes with the parent's recovered history.
theorem
Hex.GraphIso.Nauty.safetyPolicy
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel : 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)
:
Generic.CallPolicy ctx (n + 2) tcLevel (safetyContract G ctx tcLevel)
The live histories discharge the generic induction rules for every off-path call.
theorem
Hex.GraphIso.Nauty.node_safe
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells : Nat}
{st : 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)
(hin : NodePre G ctx tcLevel level numcells st)
:
Every off-path call preserves the installed canonical data and checked generator trace.
theorem
Hex.GraphIso.Nauty.sweep_safe
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{first : Bool}
{tcLevel fuel cfuel level numcells tc tv1 index : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : 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)
(hin : SweepPre G ctx tcLevel first level numcells tc tv1 cursor cell st)
:
A sweep past the first child preserves the same invariant through all exits.