def Hex.GraphIso.Nauty.Generic.Past (first : Bool) (tv1 : Nat) (cursor : Option Nat) : Prop

A sweep is strictly past its first child, or is entirely off the first path.

Equations

• Hex.GraphIso.Nauty.Generic.Past first tv1 cursor = (first = true → ∀ (v : Nat), cursor = some v → tv1 < v)

theorem Hex.GraphIso.Nauty.Generic.Past.next {n : Nat} {first : Bool} {tv1 tv : Nat} {cell : VSet n} (h : first = true → tv1 < tv) : Past first tv1 (cell.nextElem (some tv))

Every later bitset cursor remains past the first child.

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

An invariant preserved by off-path calls and later siblings.

Equations

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

structure Hex.GraphIso.Nauty.Generic.StablePolicy {n : Nat} {σ γ : Type} [Policy σ n] (ctx : γ) (inf tcLevel : Nat) (P : σ → Prop) (validCode : Nat → Prop := fun (x : Nat) => True) (validLeaf : Leaf → σ → Prop := fun (x : Leaf) (x_1 : σ) => True) : Prop

Local operations outside the first descent preserve a state invariant.

• code (level numcells : Nat) (st : σ) : validCode (Policy.visit ctx level numcells st).snd.fst
• visit (level numcells : Nat) (st : σ) : P st → P (Policy.visit ctx level numcells st).snd.snd
• compare (level code : Nat) (st : σ) : validCode code → P st → P (Policy.compareCodes level code st)
• target (level numcells : Nat) (st : σ) : 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 ∧ validLeaf (Policy.classify ctx level numcells st).fst (Policy.classify ctx level numcells st).snd
• leaf (leaf : Leaf) (level : Nat) (st : σ) : validLeaf leaf st → P st → P (Policy.leafExit leaf level st).snd
• cheap (first : Bool) (level : Nat) (st : σ) : 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 : σ) : P st → P (Policy.recover inf level st)
• afterSweep (level size index : Nat) (st : σ) : P st → P (Policy.afterSweep false level size index st)

theorem Hex.GraphIso.Nauty.Generic.StablePolicy.node_step {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} {validCode : Nat → Prop} {validLeaf : Leaf → σ → Prop} (h : StablePolicy ctx inf tcLevel P validCode validLeaf) {fuel : Nat} {next : SweepFn σ n} (hnext : (stableContract n P).sweepValid fuel (n + 1) next) (level numcells : Nat) (st : σ) (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.StablePolicy.sweep_step {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} {validCode : Nat → Prop} {validLeaf : Leaf → σ → Prop} (h : StablePolicy ctx inf tcLevel P validCode validLeaf) {fuel cfuel : Nat} {descend : NodeFn σ} {next : SweepFn σ n} (hdescend : (stableContract n P).nodeValid fuel descend) (hnext : (stableContract n P).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : σ) (hpast : Past first tv1 (some tv)) (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.StablePolicy.sound {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} {validCode : Nat → Prop} {validLeaf : Leaf → σ → Prop} (h : StablePolicy ctx inf tcLevel P validCode validLeaf) : SoundPolicy ctx inf tcLevel (stableContract n P)

Local preservation gives the generic invariant contract.

theorem Hex.GraphIso.Nauty.Generic.node_stable {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} {validCode : Nat → Prop} {validLeaf : Leaf → σ → Prop} (h : StablePolicy ctx inf tcLevel P validCode validLeaf) (fuel level numcells : Nat) (st : σ) (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_stable {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {P : σ → Prop} {validCode : Nat → Prop} {validLeaf : Leaf → σ → Prop} (h : StablePolicy ctx inf tcLevel P validCode validLeaf) (first : Bool) (fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : σ) (hpast : Past first tv1 cursor) (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.