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: the finite set represented by a round count.
• Cslib.InductiveCounting.Invariant: the semantic assertion at each instruction.

References

• 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

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

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

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

theorem Cslib.InductiveCounting.prefixCount_full {N source k : ℕ} {edge : ℕ → ℕ → Bool} : prefixCount N edge source k N = (roundSet N edge source (k + 1)).card

theorem Cslib.InductiveCounting.prefixCount_succ {N source k : ℕ} {edge : ℕ → ℕ → Bool} (v : ℕ) : prefixCount N edge source k (v + 1) = prefixCount N edge source k v + if v ∈ roundSet N edge source (k + 1) then 1 else 0

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

theorem Cslib.InductiveCounting.scanPrefix_start {N source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (s : State) : ScanPrefix N edge bad source { phase := s.phase, round := s.round, count := s.count, target := s.target, nextCount := s.nextCount, remaining := s.remaining, current := s.current, guess := s.guess, bits := s.bits, finalScan := s.finalScan }

theorem Cslib.InductiveCounting.scanPrefix_skip {N source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (h : ScanPrefix N edge bad source s) : ScanPrefix N edge bad source { phase := s.phase, round := s.round, count := s.count, target := s.target, nextCount := s.nextCount, candidate := s.candidate + 1, selected := s.selected, remaining := s.remaining, current := s.current, guess := s.guess, bits := s.bits, hit := s.hit, finalScan := s.finalScan }

theorem Cslib.InductiveCounting.scanPrefix_observe {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} {choice : Bool} (h : ScanPrefix N edge bad source s) (hu : s.candidate ∈ roundSet N edge source s.round) (hp : s.phase = Phase.observe) : ScanPrefix N edge bad source (instruction N width source s (answer edge bad s) choice)

theorem Cslib.InductiveCounting.scan_hit_succ {N source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (hsource : source < N) (hc : RoundCorrect N edge source s) (hp : ScanPrefix N edge bad source s) (he : s.selected = s.count) (hf : s.finalScan = false) (hv : s.target < N) : s.hit = true ↔ s.target ∈ roundSet N edge source (s.round + 1)

theorem Cslib.InductiveCounting.scan_final_safe {N source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (hsource : source < N) (hc : RoundCorrect N edge source s) (hp : ScanPrefix N edge bad source s) (he : s.selected = s.count) (hf : s.finalScan = true) (hk : s.round + 1 = N) (hh : s.hit = false) : Safe N source edge bad

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

theorem Cslib.InductiveCounting.invariant_instruction {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 (instruction N width source s (answer edge bad s) choice)

Every underlying instruction preserves the semantic assertion. A rejected branch has no proof obligation; dishonest omissions can survive temporarily but cannot pass a count check.

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)

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.