def Hex.GraphIso.Nauty.Generic.boundedContract {σ : Type} (n bound : Nat) (P : σ → Prop) : Contract σ n

An invariant retained by calls below a fixed ancestor.

Equations

• One or more equations did not get rendered due to their size.

structure Hex.GraphIso.Nauty.Generic.BoundedPolicy {n : Nat} {σ γ : Type} [Policy σ n] (ctx : γ) (inf tcLevel bound : Nat) (P : σ → Prop) : Prop

Local preservation below an ancestor; comparison happens strictly below it, while recovery may return to the ancestor itself.

• visit (level numcells : Nat) (st : σ) : P st → P (Policy.visit ctx level numcells st).snd.snd
• compare (level code : Nat) (st : σ) : bound < level → P st → P (Policy.compareCodes level code st)
• target (level numcells : Nat) (st : σ) : bound < level → P st → P (Policy.chooseTarget false ctx tcLevel level numcells st).snd.snd.snd
• classify (level numcells : Nat) (st : σ) : P st → P (Policy.classify ctx level numcells st).snd
• leaf (leaf : Leaf) (level : Nat) (st : σ) : bound < level → P st → P (Policy.leafExit leaf level st).snd
• cheap (first : Bool) (level : Nat) (st : σ) : bound ≤ level → P st → P (Policy.cheapCheck first level st)
• child (first : Bool) (level tc tv : Nat) (st : σ) : P st → P (Policy.child first level tc tv st)
• leave (tv : Nat) (st : σ) : P st → P (Policy.leaveChild tv st)
• recover (level : Nat) (st : σ) : bound ≤ level → P st → P (Policy.recover inf level st)
• afterSweep (first : Bool) (level size index : Nat) (st : σ) : bound ≤ level → P st → P (Policy.afterSweep first level size index st)

theorem Hex.GraphIso.Nauty.Generic.BoundedPolicy.node_step {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel bound : Nat} {P : σ → Prop} (h : BoundedPolicy ctx inf tcLevel bound P) {fuel : Nat} {next : SweepFn σ n} (hnext : (boundedContract n bound P).sweepValid fuel (n + 1) next) (level numcells : Nat) (st : σ) (hlevel : bound < level) (hin : P st) : P (nodeStep ctx tcLevel next false level numcells st).snd

An off-path node preserves the state invariant.

theorem Hex.GraphIso.Nauty.Generic.BoundedPolicy.sweep_step {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel bound : Nat} {P : σ → Prop} (h : BoundedPolicy ctx inf tcLevel bound P) {fuel cfuel : Nat} {descend : NodeFn σ} {next : SweepFn σ n} (hdescend : (boundedContract n bound P).nodeValid fuel descend) (hnext : (boundedContract n bound P).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : σ) (hpast : Past first tv1 (some tv)) (hlevel : bound ≤ level) (hin : P st) : P (sweepStep inf descend next first level numcells tc tv1 tv cell index st).snd.snd

Once past the first child, all later recursive calls are off-path.

theorem Hex.GraphIso.Nauty.Generic.BoundedPolicy.sound {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel bound : Nat} {P : σ → Prop} (h : BoundedPolicy ctx inf tcLevel bound P) : SoundPolicy ctx inf tcLevel (boundedContract n bound P)

Local preservation gives the generic invariant contract.

theorem Hex.GraphIso.Nauty.Generic.node_bounded {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel bound : Nat} {P : σ → Prop} (h : BoundedPolicy ctx inf tcLevel bound P) (fuel level numcells : Nat) (st : σ) (hlevel : bound < level) (hin : P st) : P (node false ctx inf tcLevel fuel level numcells st).snd

An off-path node preserves an invariant stable under its local operations.

theorem Hex.GraphIso.Nauty.Generic.sweep_bounded {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel bound : Nat} {P : σ → Prop} (h : BoundedPolicy ctx inf tcLevel bound P) (first : Bool) (fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : σ) (hpast : Past first tv1 cursor) (hlevel : bound ≤ level) (hin : P st) : P (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

A later sibling sweep preserves the same invariant.