Semantic invariants of the inductive-counting controller

The sets in this file are ghost state used in the proofs. They are not part of the controller's registers. A scan selects distinct identifiers because its candidate register increases; equality of its selected count with the round count then forces exhaustiveness.

Main definitions

• Cslib.InductiveCounting.Graph: the graph restricted to the vertex interval.
• Cslib.InductiveCounting.roundSet, Cslib.InductiveCounting.prefixCount: the finite set represented by a round count and the next-round count below the current target.
• Cslib.InductiveCounting.Observed: the predicate observed for one included candidate.
• Cslib.InductiveCounting.RoundCorrect, Cslib.InductiveCounting.ScanContext, Cslib.InductiveCounting.ScanPrefix: ghost invariants for the round count and scan loop.
• Cslib.InductiveCounting.Safe: no bad vertex is reachable in the restricted input graph.
• Cslib.InductiveCounting.Invariant: the semantic assertion at each instruction.

References

• N. Immerman, Nondeterministic Space Is Closed under Complementation
• R. Szelepcsényi, The Method of Forcing for Nondeterministic Automata
• M. Sipser, Introduction to the Theory of Computation, Section 8.6

def Cslib.InductiveCounting.Graph (N : ℕ) (edge : ℕ → ℕ → Bool) (u v : ℕ) : Prop

The input graph restricted to identifiers less than N.

noncomputable def Cslib.InductiveCounting.roundSet (N : ℕ) (edge : ℕ → ℕ → Bool) (source k : ℕ) : Finset ℕ

The ghost set whose cardinality the controller carries.

theorem Cslib.InductiveCounting.reachable_lt {N source u : ℕ} {edge : ℕ → ℕ → Bool} (hsource : source < N) (h : Relation.ReflTransGen (Graph N edge) source u) : u < N

theorem Cslib.InductiveCounting.within_lt {N source k u : ℕ} {edge : ℕ → ℕ → Bool} (hsource : source < N) (h : Relation.RelatesWithinSteps (Graph N edge) source u k) : u < N

Every vertex reachable within k steps in the restricted graph lies below N.

theorem Cslib.InductiveCounting.mem_roundSet {N source k u : ℕ} {edge : ℕ → ℕ → Bool} (hsource : source < N) : u ∈ roundSet N edge source k ↔ Relation.RelatesWithinSteps (Graph N edge) source u k

Membership in roundSet characterizes reachability from source within k steps.

theorem Cslib.InductiveCounting.roundSet_zero {N source : ℕ} {edge : ℕ → ℕ → Bool} (hsource : source < N) : roundSet N edge source 0 = {source}

theorem Cslib.InductiveCounting.roundSet_card_le {N source k : ℕ} {edge : ℕ → ℕ → Bool} : (roundSet N edge source k).card ≤ N

Every round set contains at most N vertices.

theorem Cslib.InductiveCounting.mem_roundSet_succ {N source k v : ℕ} {edge : ℕ → ℕ → Bool} (hsource : source < N) (hv : v < N) : v ∈ roundSet N edge source (k + 1) ↔ ∃ u ∈ roundSet N edge source k, u = v ∨ edge u v = true

theorem Cslib.InductiveCounting.mem_roundSet_final {N source k u : ℕ} {edge : ℕ → ℕ → Bool} (hsource : source < N) (hk : k + 1 = N) : u ∈ roundSet N edge source k ↔ Relation.ReflTransGen (Graph N edge) source u

Round N - 1 is already the entire reachable set.

noncomputable def Cslib.InductiveCounting.prefixCount (N : ℕ) (edge : ℕ → ℕ → Bool) (source k v : ℕ) : ℕ

Count of members of the next round below the current target.

@[simp]

theorem Cslib.InductiveCounting.prefixCount_zero {N source k : ℕ} {edge : ℕ → ℕ → Bool} : prefixCount N edge source k 0 = 0

The prefix count below target 0 is zero.

def Cslib.InductiveCounting.Observed (edge : ℕ → ℕ → Bool) (bad : ℕ → Bool) (s : State) (u : ℕ) : Prop

The predicate observed for one included candidate.

def Cslib.InductiveCounting.RoundCorrect (N : ℕ) (edge : ℕ → ℕ → Bool) (source : ℕ) (s : State) : Prop

The count and round number are correct.

def Cslib.InductiveCounting.ScanContext (N : ℕ) (edge : ℕ → ℕ → Bool) (source : ℕ) (s : State) : Prop

The outer loops' ghost invariant during a scan.

def Cslib.InductiveCounting.ScanPrefix (N : ℕ) (edge : ℕ → ℕ → Bool) (bad : ℕ → Bool) (source : ℕ) (s : State) : Prop

The selected identifiers form a subset of the processed prefix. The ghost set S is not stored by the algorithm. Omissions are allowed here and detected by the final count check.

def Cslib.InductiveCounting.Safe (N source : ℕ) (edge : ℕ → ℕ → Bool) (bad : ℕ → Bool) : Prop

No bad vertex is reachable in the restricted input graph.

def Cslib.InductiveCounting.Invariant (N : ℕ) (edge : ℕ → ℕ → Bool) (bad : ℕ → Bool) (source : ℕ) (s : State) : Prop

Semantic assertion at every instruction of the explicit controller.

theorem Cslib.InductiveCounting.scan_exhaustive {N source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (hc : RoundCorrect N edge source s) (hp : ScanPrefix N edge bad source s) (he : s.selected = s.count) : s.hit = true ↔ ∃ u ∈ roundSet N edge source s.round, Observed edge bad s u

When the selected count matches the round count, s.hit reflects the entire round set.

theorem Cslib.InductiveCounting.invariant_initial {N source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (hsource : source < N) : Invariant N edge bad source (initial N source)

The initial state satisfies the semantic invariant whenever source < N.

theorem Cslib.InductiveCounting.invariant_advance {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (hsource : source < N) (h : Invariant N edge bad source s) (choice : Bool) : Invariant N edge bad source (advance N width source s (answer edge bad s) choice)

The checked controller preserves the semantic invariant on every branch.

theorem Cslib.InductiveCounting.invariant_replay {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (hsource : source < N) (h : Invariant N edge bad source s) (bs : List Bool) : Invariant N edge bad source (replay N width source edge bad s bs)

Every replay of the checked controller preserves the semantic invariant.

theorem Cslib.InductiveCounting.accepts_sound {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (hsource : source < N) (h : Accepts N width source edge bad) : Safe N source edge bad

An accepting choice replay certifies the absence of every reachable bad vertex.