Uniform bounds for the inductive-counting controller

Every branch halts in O((N + 1)^4 * (width + 1)) instructions. Every register remains below N + 2^width + width + 2, independently of the graph and the choices. A binary encoding of the fixed register tuple therefore uses O(log N + width) bits when the width is chosen to encode vertex identifiers.

Main results

• Cslib.InductiveCounting.halted_replay_budget: a uniform all-branch time bound.
• Cslib.InductiveCounting.query_bounds: legitimate queries use valid vertex identifiers.

References

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

def Cslib.InductiveCounting.budget (N width : ℕ) : ℕ

A uniform polynomial instruction budget. The width counts binary choices per vertex.

theorem Cslib.InductiveCounting.rank_initial {N width source : ℕ} (hsource : source < N) : rank N width (initial N source) = N * roundCost N width + 1

theorem Cslib.InductiveCounting.rank_initial_le_budget {N width source : ℕ} : rank N width (initial N source) ≤ budget N width

theorem Cslib.InductiveCounting.halted_replay_budget {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (bs : List Bool) (hb : budget N width ≤ bs.length) : halted (replay N width source edge bad (initial N source) bs) = true

Every branch, including every dishonest branch, halts within the polynomial budget.

theorem Cslib.InductiveCounting.bounded_replay_initial {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (bs : List Bool) : Bounded N width (replay N width source edge bad (initial N source) bs)

All registers of all choice prefixes satisfy the uniform bound.

theorem Cslib.InductiveCounting.accepts_complete_bounded {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} (hsource : source < N) (hwidth : N ≤ 2 ^ width) (hsafe : Safe N source edge bad) : ∃ (bs : List Bool), bs.length ≤ budget N width ∧ (replay N width source edge bad (initial N source) bs).phase = Phase.accept

Honest acceptance needs no more choices than the all-branch instruction budget.

theorem Cslib.InductiveCounting.query_bounds {N source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} {q : Query} (hsource : source < N) (hi : Invariant N edge bad source s) (hq : query s = some q) : match q, hq with | Query.edge u v, hq => u < N ∧ v < N | Query.bad u, hq => u < N

Queries made along a semantically valid run use identifiers in the vertex interval.