Every branch of a nondeterministic counter program

A nondeterministic counter program (Turing.CounterProgram.toNondeterministicQueryMachine) writes a fresh choice bit into register 0 after every step. Its correctness is proved branch by branch with the inductive predicate Turing.CounterProgram.AllBranches: every branch from a configuration reaches a configuration satisfying Q, or halts in one satisfying Post, and passes only through configurations whose registers are at most B. These predicates compose (Turing.CounterProgram.AllBranches.bind), and every branch of a program satisfying one from its initial configuration with Q empty halts within a common number of steps, keeps its registers bounded and halts only in configurations satisfying Post (Turing.CounterProgram.AllBranches.exists_haltsWithin, Turing.CounterProgram.AllBranches.replay).

Most of a program is deterministic: its instructions do not mention register 0 (Turing.CounterProgram.Instr.readsChoice). On such code every branch follows the deterministic run up to register 0, so the deterministic reachability of counter programs (Turing.CounterProgram.Reaches) gives both every branch (Turing.CounterProgram.allBranches_of_reaches) and one branch (Turing.CounterProgram.branches_of_reaches).

Main definitions

• Turing.CounterProgram.Expr.readsChoice, Turing.CounterProgram.Instr.readsChoice: whether an expression or an instruction mentions register 0.
• Turing.CounterProgram.AllBranches: every branch reaches a target or halts.

Main results

• Turing.CounterProgram.AllBranches.bind: sequential composition.
• Turing.CounterProgram.AllBranches.exists_haltsWithin, Turing.CounterProgram.AllBranches.replay: the consequences for every branch from the initial configuration.
• Turing.CounterProgram.allBranches_of_reaches, Turing.CounterProgram.branches_of_reaches: deterministic code that does not read register 0.
• Turing.CounterProgram.exists_decidesInLogSpace_of_allBranches: deciding in logarithmic space from every branch and one accepting branch.

Code that does not read the choice

def Turing.CounterProgram.Expr.readsChoice : Expr → Bool

Whether an expression mentions register 0, the choice.

theorem Turing.CounterProgram.Expr.eval_set_zero {e : Expr} (he : e.readsChoice = false) (regs : List ℕ) (x : ℕ) : eval (regs.set 0 x) e = eval regs e

An expression that does not mention register 0 ignores its value.

def Turing.CounterProgram.Instr.readsChoice : Instr → Bool

Whether an instruction reads or writes register 0, the choice.

theorem Turing.CounterProgram.step_withChoice {P : CounterProgram} {w : List Bool} {s : Config} (hs : (P.instr s.1).readsChoice = false) (c : Bool) : P.step w (withChoice s c) = withChoice (P.step w s) c

A step that does not read the choice commutes with it: overwriting register 0 before the step overwrites it after the step.

Every branch

inductive Turing.CounterProgram.AllBranches (P : CounterProgram) (w : List Bool) (B : ℕ) (Post Q : Config → Prop) : Config → Prop

P.AllBranches w B Post Q s: every branch from s reaches a configuration satisfying Q, or halts in a configuration satisfying Post, and the configurations before are running ones with registers at most B.

• exit {P : CounterProgram} {w : List Bool} {B : ℕ} {Post Q : Config → Prop} {s : Config} : Q s → P.AllBranches w B Post Q s

  A target is reached.

• halt {P : CounterProgram} {w : List Bool} {B : ℕ} {Post Q : Config → Prop} {s : Config} : P.halted s = true → Post s → (∀ r ∈ s.2, r ≤ B) → P.AllBranches w B Post Q s

  A halt satisfying Post.

• step {P : CounterProgram} {w : List Bool} {B : ℕ} {Post Q : Config → Prop} {s : Config} : P.halted s = false → (∀ r ∈ s.2, r ≤ B) → (∀ (choice : Bool), P.AllBranches w B Post Q (withChoice (P.step w s) choice)) → P.AllBranches w B Post Q s

  A step from a running configuration, with either choice.

theorem Turing.CounterProgram.AllBranches.bind {P : CounterProgram} {w : List Bool} {B : ℕ} {Post Q Q' : Config → Prop} {s : Config} (h : P.AllBranches w B Post Q s) (h' : ∀ (q : Config), Q q → P.AllBranches w B Post Q' q) : P.AllBranches w B Post Q' s

Sequential composition: continuing from every target.

theorem Turing.CounterProgram.AllBranches.mono {P : CounterProgram} {w : List Bool} {B : ℕ} {Post Q Q' : Config → Prop} {s : Config} (h : P.AllBranches w B Post Q s) (hQ : ∀ (q : Config), Q q → Q' q) : P.AllBranches w B Post Q' s

theorem Turing.CounterProgram.AllBranches.single {P : CounterProgram} {w : List Bool} {B : ℕ} {Post Q : Config → Prop} {s : Config} (hh : P.halted s = false) (hb : ∀ r ∈ s.2, r ≤ B) (h : ∀ (choice : Bool), Q (withChoice (P.step w s) choice)) : P.AllBranches w B Post Q s

One step from a running configuration, whatever the choice.

theorem Turing.CounterProgram.AllBranches.exists_haltsWithin {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {s : Config} (h : P.AllBranches w B Post (fun (x : Config) => False) s) : ∃ (t : ℕ), ∀ (choices : List Bool), t ≤ choices.length → P.halted (P.toNondeterministicQueryMachine.replay w choices s) = true

Every branch halts within a common number of steps, for a program with no target.

theorem Turing.CounterProgram.AllBranches.replay {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {s : Config} (h : P.AllBranches w B Post (fun (x : Config) => False) s) (choices : List Bool) : (∀ r ∈ (P.toNondeterministicQueryMachine.replay w choices s).2, r ≤ B) ∧ (P.halted (P.toNondeterministicQueryMachine.replay w choices s) = true → Post (P.toNondeterministicQueryMachine.replay w choices s))

Every branch keeps its registers bounded and halts only where Post holds, for a program with no target.

Deterministic code

theorem Turing.CounterProgram.allBranches_of_reaches {P : CounterProgram} {w : List Bool} {B : ℕ} (hB : 1 ≤ B) {Post Q R : Config → Prop} {s s' : Config} (h : P.Reaches w R s s') (hR : ∀ (x : Config), R x → (P.instr x.1).readsChoice = false ∧ (P.instr x.1).IsStep ∧ ∀ r ∈ x.2, r ≤ B) (hQ : ∀ (c : Bool), Q (withChoice s' c)) (c : Bool) : P.AllBranches w B Post Q (withChoice s c)

Every branch through deterministic code that does not read register 0 follows the deterministic run, whatever the choice before it.

theorem Turing.CounterProgram.branches_of_reaches {P : CounterProgram} {w : List Bool} {R : Config → Prop} {s s' : Config} (h : P.Reaches w R s s') (hR : ∀ (x : Config), R x → (P.instr x.1).readsChoice = false ∧ (P.instr x.1).IsStep) (c c' : Bool) (hc : s = s' → c = c') : Branches (withChoice s c) (withChoice s' c')

One branch through deterministic code that does not read register 0: the deterministic run from s to s', ending with any choice c' when s ≠ s' and with the initial choice c when s = s'.

Steps of code that does not read the choice

def Turing.CounterProgram.Oblivious (P : CounterProgram) (B : ℕ) (s : Config) : Prop

Running configurations, with registers at most B, at instructions that do not read the choice.

theorem Turing.CounterProgram.Reaches.oassign {P : CounterProgram} {w : List Bool} {B : ℕ} {regs : List ℕ} {s' : Config} {c i : ℕ} {e : Expr} {next : ℕ} (hc : P.instr c = Instr.assign i e next) (hi : i ≠ 0) (he : e.readsChoice = false) (hB : ∀ r ∈ regs, r ≤ B) (h : P.Reaches w (P.Oblivious B) (next, regs.set i (Expr.eval regs e)) s') : P.Reaches w (P.Oblivious B) (c, regs) s'

theorem Turing.CounterProgram.Reaches.olt {P : CounterProgram} {w : List Bool} {B : ℕ} {regs : List ℕ} {s' : Config} {c : ℕ} {x y : Expr} {yes no : ℕ} (hc : P.instr c = Instr.lt x y yes no) (hx : x.readsChoice = false) (hy : y.readsChoice = false) (hB : ∀ r ∈ regs, r ≤ B) (h : P.Reaches w (P.Oblivious B) (if Expr.eval regs x < Expr.eval regs y then yes else no, regs) s') : P.Reaches w (P.Oblivious B) (c, regs) s'

theorem Turing.CounterProgram.Reaches.oread {P : CounterProgram} {w : List Bool} {B : ℕ} {regs : List ℕ} {s' : Config} {c : ℕ} {e : Expr} {onTrue onFalse onEnd : ℕ} (hc : P.instr c = Instr.read e onTrue onFalse onEnd) (he : e.readsChoice = false) (hB : ∀ r ∈ regs, r ≤ B) (h : P.Reaches w (P.Oblivious B) (readLabel onTrue onFalse onEnd w[Expr.eval regs e]?, regs) s') : P.Reaches w (P.Oblivious B) (c, regs) s'

theorem Turing.CounterProgram.allBranches_of_oblivious {P : CounterProgram} {w : List Bool} {B : ℕ} (hB : 1 ≤ B) {Post Q : Config → Prop} {s s' : Config} (h : P.Reaches w (P.Oblivious B) s s') (hQ : ∀ (c : Bool), Q (withChoice s' c)) (c : Bool) : P.AllBranches w B Post Q (withChoice s c)

Every branch through oblivious deterministic code.

theorem Turing.CounterProgram.branches_of_oblivious {P : CounterProgram} {w : List Bool} {B : ℕ} {s s' : Config} (h : P.Reaches w (P.Oblivious B) s s') (c c' : Bool) (hc : s = s' → c = c') : Branches (withChoice s c) (withChoice s' c')

One branch through oblivious deterministic code.

Deciding in logarithmic space

theorem Turing.CounterProgram.exists_decidesInLogSpace_of_allBranches (P : CounterProgram) {α : Type} {enc : α ↪ List Bool} {A : Set α} (d : ℕ) (hall : ∀ (a : α), P.AllBranches (enc a) (((enc a).length + 1) ^ d) (fun (s : Config) => P.instr s.1 = Instr.accept → a ∈ A) (fun (x : Config) => False) P.init) (hacc : ∀ a ∈ A, ∃ (s : Config), Branches P.init s ∧ P.instr s.1 = Instr.accept) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (ntm : MultiTapeNTM k Bool State) (c : ℕ), ntm.DecidesInSpace enc A fun (a : α) => c * ((enc a).length.log2 + 1)

A nondeterministic counter program decides in logarithmic space a problem when, on every encoded instance, every branch from the initial configuration halts with registers at most (n + 1) ^ d and accepts only instances of the problem, and some branch reaches the accepting halt on every instance of the problem.