Universal machine: the simulate/halt-test loop

The headline correctness theorem for the UTM's main loop loopTM bodyTM haltTestTM: if the interpreted machine (decodeDesc α).toTM halts on x in T steps at the configuration mcF, then from any tapes realizing the standing invariant SimInv at the interpreted machine's initial configuration (output tape cleared, head parked at cell 1), the loop halts within (T + 1) * utmStepTime α steps with SimInv re-established at mcF and the halt verdict Γ.one at output cell 1.

Proof structure

One loop iteration = one interpreted step:

• bodyIteration runs one body pass (SimInv at mc ↦ SimInv at (decodeDesc α).toTM.step mc, or an exact no-op when halted);
• the body→test / test→rewind combinator transitions apply transitionInput/transitionTape to every tape — literal identities here, since every SimInv tape is parked (head ≥ 1, read ≠ ▷);
• haltTestTM_hoareTime compares the state tape against the description's qhalt field, writing the verdict at output cell 1; simInv_verdict identifies the comparison with the interpreted halt test;
• the rewind/check bookkeeping (3 steps, output head 1 → 0 → 1) either halts the loop (verdict Γ.one) or returns to the loop start with the invariant re-established (loopTM_rewind_check below).

The outer induction (loop_sim_aux) is a strong induction on the remaining fuel T - t' rather than an instance of loopTM_hoareTime: the loop variant would have to be a function of the tapes, while here it is determined only through the existentially quantified prefix run of the interpreted machine. Determinism of reachesIn plus the halted-configurations-don't-step principle (TM.reachesIn_le_halt) identify the loop's exit configuration with mcF.

def Complexity.TM.UTMBody.utmStepTime (α : List Bool) : ℕ

Per-α time cost of one iteration of the UTM's simulate/halt-test loop: one body pass, the two combinator transitions, the halt test, and the loop's rewind/check bookkeeping.

Equations

• Complexity.TM.UTMBody.utmStepTime α = Complexity.TM.UTMBody.bodyIterTime α + 4 * (Complexity.groupPairs α).length + 20

theorem Complexity.TM.UTMBody.loop_iteration (α : List Bool) (hterm : TerminatedRegion α) (mc : Cfg 1 (decodeDesc α).toTM.Q) (inp : Tape) (work : Fin 6 → Tape) (out : Tape) (hinv : SimInv α mc inp work out) (hout0 : out.cells 0 = Γ.start) (houtns : ∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) (houth : out.head = 1) : ∃ (mc₂ : Cfg 1 (decodeDesc α).toTM.Q) (work' : Fin 6 → Tape) (out' : Tape), ∃ t ≤ utmStepTime α, 1 ≤ t ∧ ((decodeDesc α).toTM.step mc = some mc₂ ∨ (decodeDesc α).toTM.step mc = none ∧ mc₂ = mc) ∧ SimInv α mc₂ inp work' out' ∧ out'.cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → out'.cells j ≠ Γ.start) ∧ out'.head = 1 ∧ (mc₂.state = (decodeDesc α).toTM.qhalt ∧ out'.cells 1 = Γ.one ∧ (bodyTM.loopTM haltTestTM).reachesIn t { state := (bodyTM.loopTM haltTestTM).qstart, input := inp, work := work, output := out } { state := Sum.inr (Sum.inl LoopPhase.done), input := inp, work := work', output := out' } ∨ mc₂.state ≠ (decodeDesc α).toTM.qhalt ∧ (bodyTM.loopTM haltTestTM).reachesIn t { state := (bodyTM.loopTM haltTestTM).qstart, input := inp, work := work, output := out } { state := (bodyTM.loopTM haltTestTM).qstart, input := inp, work := work', output := out' })

One iteration of the UTM loop interprets one step of the simulated machine. From the loop's start state under SimInv at mc (output parked at cell 1), within utmStepTime α steps the loop either

• halts (the fresh verdict at output cell 1 is Γ.one) — exactly when the post-step configuration mc₂ is halted — or
• returns to the loop's start state with SimInv at mc₂ and the output tape again parked,

where mc₂ is (decodeDesc α).toTM.step mc when defined and mc itself otherwise. The input tape is untouched throughout, and every iteration takes at least one step.

theorem Complexity.TM.UTMBody.utm_loop_simulates (α x : List Bool) (hterm : TerminatedRegion α) (T : ℕ) (mcF : Cfg 1 (decodeDesc α).toTM.Q) (hrun : (decodeDesc α).toTM.reachesIn T ((decodeDesc α).toTM.initCfg x) mcF) (hhalt : (decodeDesc α).toTM.halted mcF) (inp : Tape) (work : Fin 6 → Tape) (out : Tape) (hinv : SimInv α ((decodeDesc α).toTM.initCfg x) inp work out) (hout0 : out.cells 0 = Γ.start) (houtns : ∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) (houth : out.head = 1) : ∃ (c' : Cfg 6 (bodyTM.loopTM haltTestTM).Q), ∃ t ≤ (T + 1) * utmStepTime α, (bodyTM.loopTM haltTestTM).reachesIn t { state := (bodyTM.loopTM haltTestTM).qstart, input := inp, work := work, output := out } c' ∧ (bodyTM.loopTM haltTestTM).halted c' ∧ SimInv α mcF c'.input c'.work c'.output ∧ c'.output.cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → c'.output.cells j ≠ Γ.start) ∧ c'.output.head = 1 ∧ c'.output.cells 1 = Γ.one

The UTM loop simulates the interpreted machine. Suppose (decodeDesc α).toTM halts on x in T steps at mcF. Then from any tapes realizing SimInv at the interpreted machine's initial configuration — with the output tape ▷-clean and parked at cell 1 — the loop loopTM bodyTM haltTestTM halts within (T + 1) * utmStepTime α steps, with SimInv re-established at mcF (so the virtual output tape shadows the simulated output) and the halt verdict Γ.one at output cell 1.

theorem Complexity.TM.UTMBody.utm_loop_hoareTime (α x : List Bool) (hterm : TerminatedRegion α) (T : ℕ) (mcF : Cfg 1 (decodeDesc α).toTM.Q) (hrun : (decodeDesc α).toTM.reachesIn T ((decodeDesc α).toTM.initCfg x) mcF) (hhalt : (decodeDesc α).toTM.halted mcF) : (bodyTM.loopTM haltTestTM).HoareTime (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => SimInv α ((decodeDesc α).toTM.initCfg x) inp work out ∧ out.cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) ∧ out.head = 1) (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => SimInv α mcF inp work out ∧ out.cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) ∧ out.head = 1 ∧ out.cells 1 = Γ.one) ((T + 1) * utmStepTime α)

Hoare-style packaging of utm_loop_simulates, ready for seqTM composition with the init and extract phases.

theorem Complexity.TM.UTMBody.utm_loop_extract_hoareTime (α x : List Bool) (hterm : TerminatedRegion α) (T : ℕ) (mcF : Cfg 1 (decodeDesc α).toTM.Q) (hrun : (decodeDesc α).toTM.reachesIn T ((decodeDesc α).toTM.initCfg x) mcF) (hhalt : (decodeDesc α).toTM.halted mcF) : ((bodyTM.loopTM haltTestTM).seqTM extractTM).HoareTime (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => SimInv α ((decodeDesc α).toTM.initCfg x) inp work out ∧ out.cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) ∧ out.head = 1) (fun (x : Tape) (x_1 : Fin 6 → Tape) (out : Tape) => ∃ m ≤ T, mcF.output.cells (m + 1) = Γ.blank ∧ (∀ j < m, mcF.output.cells (j + 1) ≠ Γ.blank) ∧ ∀ j ≤ m, out.cells (j + 1) = mcF.output.cells (j + 1)) ((T + 1) * utmStepTime α + 1 + (2 * T + 9))

Loop + extraction: after the simulate/halt-test loop, extractTM copies the virtual output tape onto the real output tape. The combined machine turns the loop's precondition into the final output guarantee: the real output tape agrees with the simulated machine's final output tape (cells 1, …, m + 1) through the latter's first blank.

theorem Complexity.TM.UTMBody.utm_init_trans (α x : List Bool) (inp : Tape) (work : Fin 6 → Tape) (out : Tape) (hpost : inp.cells = (Tape.init (List.map Γ.ofBool (pair α x))).cells ∧ ((work 0).cells = fun (k : ℕ) => if k = 0 then Γ.start else if k = 1 then Γ.blank else (List.map Γ.ofBool x)[k - 2]?.getD Γ.blank) ∧ (work 0).head = 1 ∧ (work 1).HoldsExact [] ∧ (work 1).head = 1 ∧ (work 2).HoldsExact [] ∧ (work 2).head = 1 ∧ (work 3).HoldsExact (takeField (groupPairs α)).1 ∧ (work 3).head = 1 ∧ (work 4).HoldsExact (groupPairs α) ∧ (work 4).head = 1 ∧ (work 5).HoldsExact [] ∧ (work 5).head = 1 ∧ out.cells = (Tape.init []).cells ∧ out.head = 1) : SimInv α ((decodeDesc α).toTM.initCfg x) (transitionInput inp) (fun (i : Fin 6) => transitionTape (work i)) (transitionTape out) ∧ (transitionTape out).cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → (transitionTape out).cells j ≠ Γ.start) ∧ (transitionTape out).head = 1

The init/loop seam. Every tape configuration satisfying the init phase's postcondition passes through the seqTM phase transition to the loop's standing invariant at the interpreted machine's initial configuration, with the output tape parked at cell 1.

theorem Complexity.TM.UTMBody.utmTM_hoareTime (α x : List Bool) (hterm : TerminatedRegion α) (T : ℕ) (mcF : Cfg 1 (decodeDesc α).toTM.Q) (hrun : (decodeDesc α).toTM.reachesIn T ((decodeDesc α).toTM.initCfg x) mcF) (hhalt : (decodeDesc α).toTM.halted mcF) : utmTM.HoareTime (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool (pair α x)) ∧ (∀ (i : Fin 6), work i = Tape.init []) ∧ out = Tape.init []) (fun (x : Tape) (x_1 : Fin 6 → Tape) (out : Tape) => ∃ m ≤ T, mcF.output.cells (m + 1) = Γ.blank ∧ (∀ j < m, mcF.output.cells (j + 1) ≠ Γ.blank) ∧ ∀ j ≤ m, out.cells (j + 1) = mcF.output.cells (j + 1)) (4 * (pair α x).length + 4 * (groupPairs α).length + 24 + 1 + ((T + 1) * utmStepTime α + 1 + (2 * T + 9)))

The universal machine's end-to-end specification. On the standard initial tapes for input pair α x, if the interpreted machine (decodeDesc α).toTM halts on x at mcF within T steps, then utmTM halts within 4·|pair α x| + 4·|groupPairs α| + 26 + (T + 1)·utmStepTime α + 2T + 9 steps with its real output tape agreeing with the simulated machine's final output tape through the latter's first blank — i.e. the UTM computes exactly the simulated machine's output.