Parts of the witness-enumerating machine

⚠️ Unreviewed by Bolton

The machine that will witness polyExistsClass PSPACE ⊆ PSPACE copies its input onto a work tape, then loops over witnesses, building pair x w and running the matrix machine on it. This file records the window contracts of the individual parts, obtained from their existing time contracts by TM.keepsWindowOn_of_haltsIn — no new tape analysis is needed for any of them.

Main results

• TM.copyInputToOutputTM_keepsWindowOn — the input-to-output copy stays inside a linear window
• TM.copyInputToWork_keepsWindow — and so does its retargeting onto a work tape
• TM.resetTapes_keepsWindowOn — the clear-scratch stage keeps a window
• TM.pairEmitPre, TM.pairInputWork_keepsWindowOn — and so does the pair emitter
• TM.binarySucc_keepsWindowOn — and the counter increment
• bump_eq_bumpLE — the witness-advancing machine computes the witness enumeration's step
• TM.binaryBump_keepsWindowOn — and it keeps a window

theorem Complexity.TM.copyInputToOutputTM_keepsWindowOn (n : ℕ) (x : List Bool) : copyInputToOutputTM.KeepsWindowOn (fun (c : Cfg n copyInputToOutputTM.Q) => c = copyInputToOutputTM.initCfg x) x.length (0 + (x.length + 2))

The input-to-output copy keeps a linear window. Started on its initial configuration it halts in |x| + 2 steps, and a head moves at most one cell per step, so nothing travels past cell |x| + 2.

theorem Complexity.TM.copyInputToWork_keepsWindow (n : ℕ) (x : List Bool) (D : Cfg (n + 1) copyInputToOutputTM.retargetOutput.Q) : copyInputToOutputTM.retargetOutput.reaches (copyInputToOutputTM.retargetCfg (copyInputToOutputTM.initCfg x)) D → D.WithinDecisionSpace x.length (0 + (x.length + 2) + 1)

Redirecting that copy onto a work tape keeps a window too. This is the stage that puts a copy of the real input where the pair emitter can delimit it.

theorem Complexity.TM.resetTapes_keepsWindowOn {n : ℕ} (targets : List (Fin n)) (hnodup : targets.Nodup) (r : Fin n) (hr : r ∉ targets) (H : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinpSI : inp₀.StartInvariant) (hinpP : Parked inp₀) (hout0 : out₀ = (Tape.init []).move Dir3.right) (hworkSI : ∀ (j : Fin n), j ≠ r → (work₀ j).StartInvariant) (htargetHead : ∀ j ∈ targets, (work₀ j).head ≤ H) (hworkR : work₀ r = regTape H) (hother : ∀ (j : Fin n), j ≠ r → j ∉ targets → Parked (work₀ j)) {inputLength h₀ : ℕ} (hheads : ∀ (i : Fin n), (work₀ i).head ≤ h₀) (hinputHead : inp₀.head ≤ inputLength + h₀ + 1) (houtputHead : out₀.head ≤ h₀ + 1) : ((skipTM.seqTM (bigSeqTM (List.map rewindWorkTM targets))).seqTM ((wipeStepTM targets).forRegTM r)).KeepsWindowOn (fun (c : Cfg n ((skipTM.seqTM (bigSeqTM (List.map rewindWorkTM targets))).seqTM ((wipeStepTM targets).forRegTM r)).Q) => c.state = ((skipTM.seqTM (bigSeqTM (List.map rewindWorkTM targets))).seqTM ((wipeStepTM targets).forRegTM r)).qstart ∧ c.input = inp₀ ∧ c.work = work₀ ∧ c.output = out₀) inputLength (h₀ + (targets.length * (H + 4) + H * 4 + 8))

The clear-scratch stage keeps a window. TM.resetTapesTM blanks its targets regardless of their contents, in time linear in the wipe height and the number of targets; converting its halting bound gives the window directly. This is the stage that makes a loop body robust enough for TM.seqTM_keepsWindow_of_post.

def Complexity.TM.pairEmitPre {n : ℕ} (firstIdx : Fin n) (first second : List Bool) (h₀ : ℕ) : TapePred n

The pair emitter's precondition, strengthened with the head bound its own contract omits.

Equations

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

theorem Complexity.TM.pairInputWork_keepsWindowOn {n : ℕ} (firstIdx : Fin n) (first second : List Bool) (inputLength h₀ : ℕ) : (pairInputWorkTM firstIdx).KeepsWindowOn (fun (c : Cfg n (pairInputWorkTM firstIdx).Q) => c.state = (pairInputWorkTM firstIdx).qstart ∧ pairEmitPre firstIdx first second h₀ c.input c.work c.output) inputLength (h₀ + pairInputWorkTime first second)

The pair emitter keeps a window. Its own precondition parks the input and output tapes at cell one but says nothing about how far the other work heads have travelled, so pairEmitPre adds that bound; everything else comes from the emitter's halting time.

theorem Complexity.TM.binarySucc_keepsWindowOn {n : ℕ} (idx : Fin n) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hvalue : (work₀ idx).HasBinaryNat value) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) {inputLength h₀ : ℕ} (hwork : ∀ (i : Fin n), (work₀ i).head ≤ h₀) (hinputHead : inp₀.head ≤ inputLength + h₀ + 1) (houtputHead : out₀.head ≤ h₀ + 1) : (binarySuccTM idx).KeepsWindowOn (fun (c : Cfg n (binarySuccTM idx).Q) => c.state = (binarySuccTM idx).qstart ∧ c.input = inp₀ ∧ c.work = work₀ ∧ c.output = out₀) inputLength (h₀ + binarySuccTime value)

The counter increment keeps a window. TM.binarySuccTM advances the little-endian counter that carries the witness; its framed contract already pins every tape, so the window follows from the head bounds and its running time.

theorem Complexity.TM.binaryBump_keepsWindowOn {n : ℕ} (idx : Fin n) (bits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hbits : (work₀ idx).HasBinaryString bits) (hcell0 : (work₀ idx).cells 0 = Γ.start) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) {inputLength h₀ : ℕ} (hwork : ∀ (i : Fin n), (work₀ i).head ≤ h₀) (hinputHead : inp₀.head ≤ inputLength + h₀ + 1) (houtputHead : out₀.head ≤ h₀ + 1) : (binaryBumpTM idx).KeepsWindowOn (fun (c : Cfg n (binaryBumpTM idx).Q) => c.state = (binaryBumpTM idx).qstart ∧ c.input = inp₀ ∧ c.work = work₀ ∧ c.output = out₀) inputLength (h₀ + binaryBumpTime bits)

The witness-advancing machine keeps a window. Like the counter increment beside it, its framed contract pins every tape, so the window follows from the head bounds and its running time.

theorem Complexity.bump_eq_bumpLE (w : List Bool) : BinaryBump.bump w = bumpLE w

The witness-advancing machine computes the enumeration's step. BinaryBump.bump is defined on the tape's bit string and bumpLE on the witness the counter denotes; they are the same function, which is what lets dropTop_succ serve as the loop invariant of a machine that carries its witness on a tape.