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.

Honest choices reach the final count check even when a bad vertex is reachable (Cslib.InductiveCounting.exists_replay_done_final); a machine that inspects the count there learns whether some reachable vertex is bad.

Main definitions

• Cslib.InductiveCounting.BinaryExtension: a vertex extends a partial binary guess.
• Cslib.InductiveCounting.FullPrefix: the selected count equals the reachable prefix count.
• Cslib.InductiveCounting.Honest: the assertion maintained by honest choices.

Main results

• Cslib.InductiveCounting.accepts_iff: correctness of the executable, binary-choice small-register controller.
• Cslib.InductiveCounting.accepts_iff_not_reachable: the controller nondeterministically decides nonreachability.

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

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

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

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.bounded_initial {N width source : ℕ} : Bounded N width (initial N source)

The initial controller state satisfies the uniform register bound.

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.exists_replay_done_final {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (hsource : source < N) (hwidth : N ≤ 2 ^ width) : ∃ (bs : List Bool), (replay N width source edge bad (initial N source) bs).phase = Phase.done ∧ (replay N width source edge bad (initial N source) bs).finalScan = true ∧ (replay N width source edge bad (initial N source) bs).selected = (replay N width source edge bad (initial N source) bs).count

Honest choices reach the final count check, whether or not a bad vertex is reachable: some replay ends in the final scan's done instruction with every reachable vertex selected.

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.