The witness enumerator, assembled

⚠️ Unreviewed by Bolton

Five phases: park every head off the marker, copy the input, rewind what the copy left mid-scan, fill the registers, run the counting loop, and publish whether any witness was accepted.

Main results

• PolyExists.enumTM — the machine
• PolyExists.enumPark_hoareTime — its first phase, which parks the initial configuration

def Complexity.PolyExists.enumTM {k : ℕ} (M : TM k) (p q : Polynomial ℕ) : TM (enumTapes k)

The witness enumerator.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.PolyExists.enumPark_hoareTime (k : ℕ) (x : List Bool) : TM.skipTM.HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin (enumTapes k)) => Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = strTape x ∧ (work = fun (x : Fin (enumTapes k)) => TM.blankTape) ∧ out = TM.blankTape) 1

The parking phase. The initial configuration has every head on the left marker, and no stage of a composed machine can be entered that way; one step moves them all off.

def Complexity.PolyExists.afterCopyX (k : ℕ) (x : List Bool) : TM.TapePred (enumTapes k)

The state the copy phase leaves.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.PolyExists.afterCopyX_parked (k : ℕ) (x : List Bool) {inp : Tape} {work : Fin (enumTapes k) → Tape} {out : Tape} (h : afterCopyX k x inp work out) : TM.Parked inp ∧ (∀ (i : Fin (enumTapes k)), TM.Parked (work i)) ∧ TM.Parked out

theorem Complexity.PolyExists.afterCopyX_trans (k : ℕ) (x : List Bool) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : afterCopyX k x inp work out) : afterCopyX k x (TM.transitionInput inp) (fun (i : Fin (enumTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

Every tape the copy phase leaves is parked, so the boundary after it is the identity.

theorem Complexity.PolyExists.rewindX_hoareTime (k : ℕ) (x : List Bool) (B : ℕ) (hB : x.length + 1 ≤ B) : (TM.parkRewindTM [xIdx k]).HoareTime (afterCopyX k x) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = strTape x ∧ work = copiedBank k x ∧ out = TM.blankTape) (1 + 1 + (2 * (max (B + 2) (1 * (B + 3) + 1) + 1) + 1))

The rewinding phase. The copy left the input and its own target mid-scan; this puts both back at cell one, which pins the bank the prologue starts from.

def Complexity.PolyExists.enumTime (p q : Polynomial ℕ) (lx B N bBody bTest A : ℕ) : ℕ

The enumerator's running time: its six phases and the five boundaries between them.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.PolyExists.enumTM_hoareTime {k : ℕ} (M : TM k) {L' : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L' T) (hdecS : M.DecidesInSpace L' S) (p q : Polynomial ℕ) (x : List Bool) (N H B Hb bBody bTest : ℕ) (hNdef : N = 2 ^ (Polynomial.eval x.length p + 1) - 1) (hHdef : H = Polynomial.eval x.length q) (hN : 1 ≤ N) (hB1 : 1 ≤ B) (hBx : x.length + 1 ≤ B) (hHb1 : 1 ≤ Hb) (hpair : ∀ v < N, 1 + TM.pairInputWorkTime x (dropTop (v + 1)) ≤ B) (hspace : ∀ v < N, (pair x (dropTop (v + 1))).length + S (pair x (dropTop (v + 1))).length + 2 ≤ Hb) (hHbH : Hb + 1 ≤ H) (hlenH : ∀ v < N, (pair x (dropTop (v + 1))).length + 1 ≤ H) (hbodyB : ∀ v < N, bodyTime k x T H Hb B v (NTM.tally (enumP L' x) v) (NTM.tally (fun (u : ℕ) => !enumP L' x u) v) ≤ bBody) (heqB : ∀ v < N, 1 + 1 + TM.binaryEqTime (v + 1).bits N.bits ≤ B) (htestB : ∀ v < N, testTime B N v ≤ bTest) : (enumTM M p q).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin (enumTapes k)) => Tape.init []) ∧ out = Tape.init []) (fun (_inp : Tape) (_work : Fin (enumTapes k) → Tape) (out : Tape) => out = NTM.outSlot (TM.readBackWrite (Γ.ofBool (decide (0 < NTM.tally (enumP L' x) N))))) (enumTime p q x.length B N bBody bTest (NTM.tally (enumP L' x) N))

The enumerator, contracted. From its initial configuration the machine ends with 1 in the verdict slot exactly when some witness of the admitted lengths was accepted.