A binary-choice inductive-counting controller

The controller scans vertex identifiers in increasing order. It guesses whether to include each identifier, certifies each included identifier by a padded walk, and checks the selected count against the previous round's count. Only a fixed number of natural-number registers and Boolean flags are stored. An edge or bad-vertex oracle is consulted only in an explicit query phase.

Main definitions

• Cslib.InductiveCounting.State: the finite phase and the registers.
• Cslib.InductiveCounting.query: the request made in a query phase.
• Cslib.InductiveCounting.advance: one binary-choice controller instruction.
• Cslib.InductiveCounting.replay: replay a finite sequence of choices.

References

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

inductive Cslib.InductiveCounting.Phase : Type

The finite control. Neither a walk nor a set of selected vertices is stored.

• round : Phase
• target : Phase
• candidate : Phase
• walk : Phase
• guess : Phase
• edge : Phase
• observe : Phase
• done : Phase
• accept : Phase
• reject : Phase

@[instance_reducible]

instance Cslib.InductiveCounting.instDecidableEqPhase : DecidableEq Phase

@[instance_reducible]

instance Cslib.InductiveCounting.instReprPhase : Repr Phase

def Cslib.InductiveCounting.instReprPhase.repr : Phase → ℕ → Std.Format

@[instance_reducible]

instance Cslib.InductiveCounting.instFintypePhase : Fintype Phase

inductive Cslib.InductiveCounting.Query : Type

A request for one bit of the graph or of the bad-vertex predicate.

• edge (src dst : ℕ) : Query
• bad (vertex : ℕ) : Query

def Cslib.InductiveCounting.instDecidableEqQuery.decEq (x✝ x✝¹ : Query) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.InductiveCounting.instDecidableEqQuery : DecidableEq Query

@[instance_reducible]

instance Cslib.InductiveCounting.instReprQuery : Repr Query

def Cslib.InductiveCounting.instReprQuery.repr : Query → ℕ → Std.Format

structure Cslib.InductiveCounting.State : Type

Ten registers and two flags suffice, independently of the number of vertices. remaining is the number of padded walk steps still to check; bits counts unguessed bits of guess.

• phase : Phase

  Current instruction.

• round : ℕ

  Current round.

• count : ℕ

  Certified size of the current round.

• target : ℕ

  Target currently being tested.

• nextCount : ℕ

  Accumulated size of the next round.

• candidate : ℕ

  Candidate currently being scanned.

• selected : ℕ

  Number of selected candidates.

• remaining : ℕ

  Number of walk steps left.

• current : ℕ

  Current walk vertex.

• guess : ℕ

  Partially guessed next vertex.

• bits : ℕ

  Number of vertex bits left.

• hit : Bool

  Has a selected candidate satisfied the scan's predicate?

• finalScan : Bool

  Is this the last scan, which tests the bad-vertex predicate?

def Cslib.InductiveCounting.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.InductiveCounting.instDecidableEqState : DecidableEq State

@[instance_reducible]

instance Cslib.InductiveCounting.instReprState : Repr State

def Cslib.InductiveCounting.instReprState.repr : State → ℕ → Std.Format

def Cslib.InductiveCounting.reject : State

Canonical rejecting state.

def Cslib.InductiveCounting.accept : State

Canonical accepting state.

def Cslib.InductiveCounting.halted (s : State) : Bool

A state has halted when it is accepting or rejecting.

def Cslib.InductiveCounting.query (s : State) : Option Query

Oracle calls occur only at these two instructions.

def Cslib.InductiveCounting.instruction (N width source : ℕ) (s : State) (answer choice : Bool) : State

The underlying instruction, before the uniform storage and termination checks. answer is consulted only at edge and observe; choice only at candidate and guess. Vertex identifiers are guessed from most significant to least significant bit.

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

A uniform bound on each register. It includes the whole range of a width-bit guess, vertex counts (which can equal N), and the width counter.

def Cslib.InductiveCounting.Bounded (N width : ℕ) (s : State) : Prop

The bounds checked at each transition, including transitions on dishonest guesses.

@[instance_reducible]

instance Cslib.InductiveCounting.instDecidableBounded {N width : ℕ} {s : State} : Decidable (Bounded N width s)

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

Worst-case cost of checking one candidate, with slack for the loop instructions.

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

Worst-case cost of one target scan, with slack for the loop instructions.

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

Worst-case cost of one whole round, with slack for the loop instructions.

def Cslib.InductiveCounting.rank (N width : ℕ) (s : State) : ℕ

A natural-number progress measure. In a legitimate state, each instruction decreases it. The runtime check also rejects malformed states rather than allowing them to cycle.

def Cslib.InductiveCounting.advance (N width source : ℕ) (s : State) (answer choice : Bool) : State

One instruction, checked for bounded storage and progress. These checks are executable and do not consult the edge relation or the bad-vertex predicate.

def Cslib.InductiveCounting.answer (edge : ℕ → ℕ → Bool) (bad : ℕ → Bool) (s : State) : Bool

Supply the answer to the unique pending oracle request.

def Cslib.InductiveCounting.step (N width source : ℕ) (edge : ℕ → ℕ → Bool) (bad : ℕ → Bool) (s : State) (choice : Bool) : State

A graph-backed step of the controller.

def Cslib.InductiveCounting.initial (N source : ℕ) : State

Initial state; an out-of-range source is rejected.

def Cslib.InductiveCounting.replay (N width source : ℕ) (edge : ℕ → ℕ → Bool) (bad : ℕ → Bool) (s : State) : List Bool → State

Replay finite binary choices. Bits at deterministic instructions are ignored.

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

A finite run from the canonical initial state.

@[simp]

theorem Cslib.InductiveCounting.bounded_reject {N width : ℕ} : Bounded N width reject

@[simp]

theorem Cslib.InductiveCounting.bounded_accept {N width : ℕ} : Bounded N width accept

theorem Cslib.InductiveCounting.bounded_advance {N width source : ℕ} {s : State} (ans choice : Bool) (h : Bounded N width s) : Bounded N width (advance N width source s ans choice)

All branches preserve the uniform register bound.

theorem Cslib.InductiveCounting.rank_advance_lt {N width source : ℕ} {s : State} (ans choice : Bool) (h : halted s = false) : rank N width (advance N width source s ans choice) < rank N width s

Each unhalted transition decreases the progress measure.

@[simp]

theorem Cslib.InductiveCounting.advance_halted {N width source : ℕ} {s : State} (ans choice : Bool) (h : halted s = true) : advance N width source s ans choice = s

theorem Cslib.InductiveCounting.bounded_replay {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (h : Bounded N width s) (bs : List Bool) : Bounded N width (replay N width source edge bad s bs)

Register bounds hold at every point of every replay.

theorem Cslib.InductiveCounting.replay_append {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (xs ys : List Bool) : replay N width source edge bad s (xs ++ ys) = replay N width source edge bad (replay N width source edge bad s xs) ys

Appending choice sequences composes their executions.

theorem Cslib.InductiveCounting.replay_halted {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (h : halted s = true) (bs : List Bool) : replay N width source edge bad s bs = s

Further choices do not change a halted state.

theorem Cslib.InductiveCounting.halted_replay_of_rank_le {N width source : ℕ} {edge : ℕ → ℕ → Bool} {bad : ℕ → Bool} {s : State} (bs : List Bool) (h : rank N width s ≤ bs.length) : halted (replay N width source edge bad s bs) = true

Every branch halts within the initial progress measure, including adversarial guesses.