Honest binary choices for inductive counting

Ghost assertions describe honest scans and the as-yet unguessed suffix of a vertex identifier. They are used only to construct a successful binary-choice replay.

Main definitions

• Cslib.InductiveCounting.BinaryExtension: a vertex extends a partial binary guess.
• Cslib.InductiveCounting.Honest: the assertion maintained by honest choices.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.6

inductive Cslib.InductiveCounting.BinaryExtension : ℕ → ℕ → ℕ → Prop

v can be obtained from the partial guess g by appending bits binary choices.

• done (g : ℕ) : BinaryExtension 0 g g
• bit {n g v : ℕ} (b : Bool) (h : BinaryExtension n (2 * g + b.toNat) v) : BinaryExtension (n + 1) g v

theorem Cslib.InductiveCounting.BinaryExtension.le {n g v : ℕ} (h : BinaryExtension n g v) : g ≤ v

theorem Cslib.InductiveCounting.binaryExtension_exists {g v bits : ℕ} (hlo : g * 2 ^ bits ≤ v) (hhi : v < (g + 1) * 2 ^ bits) : BinaryExtension bits g v

theorem Cslib.InductiveCounting.binaryExtension_zero {g v : ℕ} (h : BinaryExtension 0 g v) : g = v

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

The selected count includes every reachable vertex of the processed prefix.

theorem Cslib.InductiveCounting.fullPrefix_start {N source : ℕ} {edge : ℕ → ℕ → Bool} (s : State) : FullPrefix N edge 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, hit := s.hit, finalScan := s.finalScan }

theorem Cslib.InductiveCounting.fullPrefix_skip {N source : ℕ} {edge : ℕ → ℕ → Bool} {s : State} (h : FullPrefix N edge source s) (hu : s.candidate ∉ roundSet N edge source s.round) : FullPrefix N edge 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.fullPrefix_observe {N source : ℕ} {edge : ℕ → ℕ → Bool} {s : State} (h : FullPrefix N edge source s) (hu : s.candidate ∈ roundSet N edge source s.round) : FullPrefix N edge source { phase := s.phase, round := s.round, count := s.count, target := s.target, nextCount := s.nextCount, candidate := s.candidate + 1, selected := s.selected + 1, remaining := s.remaining, current := s.current, guess := s.guess, bits := s.bits, hit := s.hit, finalScan := s.finalScan }

theorem Cslib.InductiveCounting.fullPrefix_end {N source : ℕ} {edge : ℕ → ℕ → Bool} {s : State} (h : FullPrefix N edge source s) (hc : RoundCorrect N edge source s) (hu : s.candidate = N) : s.selected = s.count

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

Additional ghost information used to construct honest choices. A walk retains a possible completion; a binary guess retains a vertex extending its guessed prefix.

theorem Cslib.InductiveCounting.honest_initial {N width source : ℕ} {edge : ℕ → ℕ → Bool} (hsource : source < N) : Honest N width edge source (initial N source)

def Cslib.InductiveCounting.ChoiceFits (N : ℕ) (s : State) (choice : Bool) : Prop

At a genuine binary-guess instruction, an honest choice produces a bounded prefix.

theorem Cslib.InductiveCounting.exists_honest_instruction {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (hsource : source < N) (hwidth : N ≤ 2 ^ width) (hsafe : Safe N source edge bad) (hi : Invariant N edge bad source s) (hh : Honest N width edge source s) : ∃ (choice : Bool), Honest N width edge source (instruction N width source s (answer edge bad s) choice) ∧ ChoiceFits N s choice

Every honest, semantically valid nonrejecting state has an honest next choice.

theorem Cslib.InductiveCounting.bounded_instruction {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} {choice : Bool} (hsource : source < N) (hi : Invariant N edge bad source s) (hb : Bounded N width s) (hc : ChoiceFits N s choice) : Bounded N width (instruction N width source s (answer edge bad s) choice)

Honest guesses pass the uniform register check; no state bound is assumed of an oracle.

theorem Cslib.InductiveCounting.exists_honest_step {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (hsource : source < N) (hwidth : N ≤ 2 ^ width) (hsafe : Safe N source edge bad) (hi : Invariant N edge bad source s) (hb : Bounded N width s) (hh : Honest N width edge source s) : ∃ (choice : Bool), Honest N width edge source (step N width source edge bad s choice)

Honest next instructions pass both executable checks.

theorem Cslib.InductiveCounting.bounded_initial {N width source : ℕ} : Bounded N width (initial N source)

theorem Cslib.InductiveCounting.accepts_complete {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (hsource : source < N) (hwidth : N ≤ 2 ^ width) (hsafe : Safe N source edge bad) : Accepts N width source edge bad

Honest choices yield an accepting replay whenever no bad vertex is reachable.

theorem Cslib.InductiveCounting.accepts_iff {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (hsource : source < N) (hwidth : N ≤ 2 ^ width) : Accepts N width source edge bad ↔ Safe N source edge bad

Correctness of the executable, binary-choice small-register controller.

theorem Cslib.InductiveCounting.accepts_iff_not_reachable {N width source target : ℕ} {edge : ℕ → ℕ → Bool} (hsource : source < N) (hwidth : N ≤ 2 ^ width) : (Accepts N width source edge fun (u : ℕ) => u == target) ↔ ¬Relation.ReflTransGen (Graph N edge) source target

In particular, the executable controller nondeterministically decides nonreachability.