The counting loop's simulation stage

⚠️ Unreviewed by Bolton

The loop body runs one path of the source machine and reads off whether it accepts. Three wrappers turn that simulation into something a composed machine can use as a stage:

• TM.startedTM moves the start state past the compulsory ▷-step, because no stage of a composed machine can be entered with a head at cell zero;
• TM.placeWorkTM 0 m sets the simulation's tapes beside the loop's own registers, with an exact frame — the registers come back untouched;
• TM.retargetOutput sends the verdict to a work tape instead of the real output tape, which has to stay blank for the wipe that follows.

None of the three costs a step, and none of them disturbs the others' tapes, so a run of the simulation transports to a run of the stage of exactly the same length.

Main results

• NTM.simTM — the simulation as a stage of the counting machine
• NTM.simTM_reachesIn — a run of the simulation is a run of the stage
• NTM.simTM_verdict_tape — the verdict lands on the stage's last work tape
• NTM.simTM_run — the stage run to a halt, with the acceptance bit of path v
• NTM.simEntry, NTM.simEntry_dropChoice — the configuration the stage is entered at
• NTM.simTM_frame — the invariants and head bounds the stage leaves behind
• NTM.simCfg_work_middle, NTM.simCfg_work_extra, NTM.simCfg_counter_cells — where each of the stage's tapes comes from

def Complexity.NTM.simCore {k : ℕ} (tm : NTM k) : TM (k + 1)

The path simulator, entered after its sentinel step.

Equations

• tm.simCore = tm.delayNTM.choiceTM.startedTM

def Complexity.NTM.simTM {k : ℕ} (tm : NTM k) (m : ℕ) : TM (0 + (k + 1) + m + 1)

The simulation as a stage of the counting machine. Its tapes are the source machine's k work tapes and the choice tape — which is the loop's counter — followed by m registers of the loop's own and, last, the tape the verdict is written to.

Equations

• tm.simTM m = (Complexity.TM.placeWorkTM 0 m tm.simCore).retargetOutput

def Complexity.NTM.simCfg {k : ℕ} (tm : NTM k) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) (c : Cfg (k + 1) tm.simCore.Q) : Cfg (0 + (k + 1) + m + 1) (tm.simTM m).Q

The stage's entry configuration: the simulation's own configuration, placed beside the loop's registers, with the real output tape blank.

Equations

• tm.simCfg m extras c = (Complexity.TM.placeWorkTM 0 m tm.simCore).retargetCfg (tm.simCore.placeWorkCfg 0 m extras c)

theorem Complexity.NTM.simTM_reachesIn {k : ℕ} (tm : NTM k) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) (hinv : ∀ (i : Fin (0 + (k + 1) + m)), ¬TM.placeWorkInMiddle 0 (k + 1) i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (0 + (k + 1) + m)), ¬TM.placeWorkInMiddle 0 (k + 1) i → 1 ≤ (extras i).head) {t : ℕ} {c c' : Cfg (k + 1) tm.simCore.Q} (h : tm.simCore.reachesIn t c c') : (tm.simTM m).reachesIn t (tm.simCfg m extras c) (tm.simCfg m extras c')

A run of the simulation is a run of the stage, of exactly the same length. The loop's registers need only carry their left marker and be parked; they are returned untouched.

theorem Complexity.NTM.simTM_verdict_tape {k : ℕ} (tm : NTM k) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) (c : Cfg (k + 1) tm.simCore.Q) : (tm.simCfg m extras c).work (Fin.last (0 + (k + 1) + m)) = c.output

The verdict lands on the stage's last work tape — the one TM.retargetOutput redirects the simulation's output to.

theorem Complexity.NTM.simTM_output {k : ℕ} (tm : NTM k) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) (c : Cfg (k + 1) tm.simCore.Q) : (tm.simCfg m extras c).output = (Tape.init []).move Dir3.right

The stage leaves the real output tape blank and parked, which is what the wipe that follows the simulation requires.

theorem Complexity.NTM.simTM_qstart {k : ℕ} (tm : NTM k) (m : ℕ) : (tm.simTM m).qstart = tm.simCore.qstart

The stage's start state is the simulation's, so a run of the stage from simCfg is a run from the stage machine's own start state.

theorem Complexity.NTM.simTM_run {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T v : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) (hinv : ∀ (i : Fin (0 + (k + 1) + m)), ¬TM.placeWorkInMiddle 0 (k + 1) i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (0 + (k + 1) + m)), ¬TM.placeWorkInMiddle 0 (k + 1) i → 1 ≤ (extras i).head) (c : Cfg (k + 1) tm.simCore.Q) (hdrop : dropChoice c = tm.delayNTM.trace 1 (fun (x : Fin 1) => false) (tm.delayNTM.initCfg x)) (hv : (c.work (Fin.last k)).HasBinaryNat v) : ∃ (c' : Cfg (k + 1) tm.simCore.Q), ∃ t ≤ T, tm.simCore.reachesIn t c c' ∧ (tm.simTM m).reachesIn t (tm.simCfg m extras c) (tm.simCfg m extras c') ∧ (tm.simTM m).halted (tm.simCfg m extras c') ∧ decide (((tm.simCfg m extras c').work (Fin.last (0 + (k + 1) + m))).cells 1 = Γ.one) = tm.acceptsAt x T v

The simulation stage, run to a halt with its verdict. From an entry configuration whose counter carries v and whose simulated tapes are the delayed machine's post-sentinel ones, the stage halts within the horizon, leaves the loop's registers exactly as it found them, and writes the acceptance bit of path v onto its last work tape.

def Complexity.NTM.simEntry {k : ℕ} (tm : NTM k) (x : List Bool) (v : ℕ) : Cfg (k + 1) tm.simCore.Q

The simulation's entry configuration. The delayed machine's post-sentinel state: every head at cell one, the machine's own tapes blank, and the counter carrying v.

Equations

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

theorem Complexity.NTM.simEntry_counter {k : ℕ} (tm : NTM k) (x : List Bool) (v : ℕ) : (tm.simEntry x v).work (Fin.last k) = natTape v

theorem Complexity.NTM.simEntry_counter_hasBinaryNat {k : ℕ} (tm : NTM k) (x : List Bool) (v : ℕ) : ((tm.simEntry x v).work (Fin.last k)).HasBinaryNat v

theorem Complexity.NTM.simCore_qstart {k : ℕ} (tm : NTM k) : tm.simCore.qstart = Sum.inl ()

The resumed simulation's start state is the delayed machine's extra state: the sentinel step reads ▷ on the choice tape, and the delayed machine's first transition ignores its choice bit, so nothing branches there.

theorem Complexity.NTM.simEntry_dropChoice {k : ℕ} (tm : NTM k) (x : List Bool) (v : ℕ) : dropChoice (tm.simEntry x v) = tm.delayNTM.trace 1 (fun (x : Fin 1) => false) (tm.delayNTM.initCfg x)

The entry configuration is the delayed machine's post-sentinel one. This is the hypothesis NTM.choiceTM_delay_haltsIn asks for: the simulation is entered exactly where the compulsory ▷-step would have left the machine.

theorem Complexity.NTM.simTM_frame {k : ℕ} (tm : NTM k) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) {t : ℕ} {c c' : Cfg (k + 1) tm.simCore.Q} (hrun : (tm.simTM m).reachesIn t (tm.simCfg m extras c) (tm.simCfg m extras c')) (hInvI : (tm.simCfg m extras c).input.StartInvariant) (hInvW : ∀ (j : Fin (0 + (k + 1) + m + 1)), ((tm.simCfg m extras c).work j).StartInvariant) (hInvO : (tm.simCfg m extras c).output.StartInvariant) (hHeadI : (tm.simCfg m extras c).input.head ≤ 1) (hHeadW : ∀ (j : Fin (0 + (k + 1) + m + 1)), ((tm.simCfg m extras c).work j).head ≤ 1) : (tm.simCfg m extras c').input.StartInvariant ∧ (∀ (j : Fin (0 + (k + 1) + m + 1)), ((tm.simCfg m extras c').work j).StartInvariant) ∧ (tm.simCfg m extras c').input.cells = (tm.simCfg m extras c).input.cells ∧ (tm.simCfg m extras c').input.head ≤ 1 + t ∧ ∀ (j : Fin (0 + (k + 1) + m + 1)), ((tm.simCfg m extras c').work j).head ≤ 1 + t

What the stage leaves behind. Every tape still carries its marker only at cell zero; no head has travelled further than the run was long; the input tape's contents are untouched, since a machine never writes to it. These are the facts the cleanup stage needs, and they hold for any stage, so they are read off the generic run lemmas.

theorem Complexity.NTM.simCfg_work_middle {k : ℕ} (tm : NTM k) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) (c : Cfg (k + 1) tm.simCore.Q) (i : Fin (k + 1)) (j : Fin (0 + (k + 1) + m + 1)) (hj : ↑j = ↑i) : (tm.simCfg m extras c).work j = c.work i

The stage's tapes at the simulation's own indices are the simulation's.

theorem Complexity.NTM.simCfg_work_extra {k : ℕ} (tm : NTM k) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) (c : Cfg (k + 1) tm.simCore.Q) (j : Fin (0 + (k + 1) + m + 1)) (hmid : ¬↑j < 0 + (k + 1)) (hlt : ↑j < 0 + (k + 1) + m) : (tm.simCfg m extras c).work j = extras ⟨↑j, hlt⟩

The stage's tapes at the register indices are the registers, untouched.

theorem Complexity.NTM.simCfg_counter_cells {k : ℕ} (tm : NTM k) (m : ℕ) (extras : Fin (0 + (k + 1) + m) → Tape) {t : ℕ} {c c' : Cfg (k + 1) tm.simCore.Q} (hreach : tm.simCore.reachesIn t c c') (hinv : (c.work (Fin.last k)).StartInvariant) (hhead : 1 ≤ (c.work (Fin.last k)).head) (j : Fin (0 + (k + 1) + m + 1)) (hj : ↑j = k) : ((tm.simCfg m extras c').work j).cells = ((tm.simCfg m extras c).work j).cells

The simulation leaves the counter's digits alone. choiceTM writes every choice bit back unchanged and only advances the head, so after the cleanup rewinds it the counter reads as v again.