structure Hex.GraphIso.Nauty.Generic.Contract (σ : Type) (n : Nat) : Type

Assertions at entry to and return from nodes and sweeps. The fuel arguments distinguish exhaustion from completed coverage.

• nodePre : Nat → Bool → Nat → Nat → σ → Prop

  Preconditions for a node call.

• nodePost : Nat → Bool → Nat → Nat → σ → Exit × σ → Prop

  Postconditions for a node call, including its exit.

• sweepPre : Nat → Nat → Bool → Nat → Nat → Nat → Nat → Option Nat → VSet n → Nat → σ → Prop

  Preconditions for a sweep call.

• sweepPost : Nat → Nat → Bool → Nat → Nat → Nat → Nat → Option Nat → VSet n → Nat → σ → Exit × Nat × σ → Prop

  Postconditions for a sweep call, including its exit and orbit index.

def Hex.GraphIso.Nauty.Generic.Contract.nodeValid {n : Nat} {σ : Type} (C : Contract σ n) (fuel : Nat) (f : NodeFn σ) : Prop

A continuation satisfies the node contract at its supplied fuel.

Equations

• C.nodeValid fuel f = ∀ (first : Bool) (level numcells : Nat) (st : σ), C.nodePre fuel first level numcells st → C.nodePost fuel first level numcells st (f first level numcells st)

def Hex.GraphIso.Nauty.Generic.Contract.sweepValid {n : Nat} {σ : Type} (C : Contract σ n) (fuel cfuel : Nat) (f : SweepFn σ n) : Prop

A continuation satisfies the sweep contract at its supplied fuels.

Equations

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

structure Hex.GraphIso.Nauty.Generic.SoundPolicy {n : Nat} {σ γ : Type} [Policy σ n] (ctx : γ) (inf tcLevel : Nat) (C : Contract σ n) : Prop

Local obligations sufficient for the contracts of every recursive call. The step obligations use only the contracts of their continuations.

• node_zero (first : Bool) (level numcells : Nat) (st : σ) : C.nodePre 0 first level numcells st → C.nodePost 0 first level numcells st (Exit.fuel, st)

  An exhausted node reports exhaustion without changing its state.

• node_step (fuel : Nat) (next : SweepFn σ n) : C.sweepValid fuel (n + 1) next → ∀ (first : Bool) (level numcells : Nat) (st : σ), C.nodePre (fuel + 1) first level numcells st → C.nodePost (fuel + 1) first level numcells st (nodeStep ctx tcLevel next first level numcells st)

  The local node operations preserve the contract when the sweep does.

• sweep_none (fuel cfuel : Nat) (first : Bool) (level numcells tc tv1 : Nat) (cell : VSet n) (index : Nat) (st : σ) : C.sweepPre fuel cfuel first level numcells tc tv1 none cell index st → C.sweepPost fuel cfuel first level numcells tc tv1 none cell index st (Exit.done, index, st)

  No remaining vertex means a complete sweep, even with zero fuel.

• sweep_zero (fuel : Nat) (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : σ) : C.sweepPre fuel 0 first level numcells tc tv1 (some tv) cell index st → C.sweepPost fuel 0 first level numcells tc tv1 (some tv) cell index st (Exit.fuel, index, st)

  A remaining vertex with zero fuel reports exhaustion.

• sweep_step (fuel cfuel : Nat) (descend : NodeFn σ) (next : SweepFn σ n) : C.nodeValid fuel descend → C.sweepValid fuel cfuel next → ∀ (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : σ), C.sweepPre fuel (cfuel + 1) first level numcells tc tv1 (some tv) cell index st → C.sweepPost fuel (cfuel + 1) first level numcells tc tv1 (some tv) cell index st (sweepStep inf descend next first level numcells tc tv1 tv cell index st)

  One vertex preserves the contract when its node and remaining sweep do.

theorem Hex.GraphIso.Nauty.Generic.node_sound {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {C : Contract σ n} (h : SoundPolicy ctx inf tcLevel C) (first : Bool) (fuel level numcells : Nat) (st : σ) (hin : C.nodePre fuel first level numcells st) : C.nodePost fuel first level numcells st (node first ctx inf tcLevel fuel level numcells st)

Local policy rules imply the postcondition of every node call.

theorem Hex.GraphIso.Nauty.Generic.sweep_sound {n : Nat} {σ γ : Type} [Policy σ n] {ctx : γ} {inf tcLevel : Nat} {C : Contract σ n} (h : SoundPolicy ctx inf tcLevel C) (first : Bool) (fuel cfuel level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : σ) (hin : C.sweepPre fuel cfuel first level numcells tc tv1 cursor cell index st) : C.sweepPost fuel cfuel first level numcells tc tv1 cursor cell index st (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st)

Local policy rules imply the postcondition of every sweep call.