The universal machine's loop body

One simulated step of the interpreted description: own halt check, peek (capture the at-origin flags of the three virtual tapes), seek to the entry region, first-match key scan, action copy to scratch, apply, or the no-match default; then cleanup. See docs/UTM-design.md (appendix) for the full state-machine design and the correspondence tricks (q'-length sync via the state tape, uniform mismatch path, sanitized default moves).

Tape layout: 0 vInput, 1 vWork, 2 vOut (virtual tapes, +1-shift representation, VTape.lean), 3 state, 4 desc, 5 scratch. The real input and output tapes are untouched (the loop verdict on the output tape is written by the halt-test machine, not the body).

This file defines the machine only; its HoareTime spec and the correspondence with TMDesc.toTM.step live in BodyInternal.lean (M3).

@[reducible, inline]

abbrev Complexity.TM.UTMBody.VFlags : Type

At-origin flags for the three virtual tapes (input, work, output): true = the simulated head is at position 0 (reading ▷), captured by the peek phase and threaded through the match/apply phases.

Equations

• Complexity.TM.UTMBody.VFlags = (Bool × Bool × Bool)

inductive Complexity.TM.UTMBody.BodyQ : Type

Control states of the body machine. See the design appendix.

• hc0 : BodyQ

  Halt check: skip desc field 1 (qstart).

• hc1 : BodyQ

  Halt check: lockstep-compare state tape vs desc field 2 (qhalt).

• haltRewS : BodyQ

  Machine already halted: rewind state, then desc, exit as no-op.

• haltRewD : BodyQ
• preRewS : BodyQ

  Not halted: rewind state, then desc, proceed to peek.

• preRewD : BodyQ
• peek1 : BodyQ

  Peek: virtual heads step left, read (▷ ⟺ at sim-origin), step back.

• peek2 : BodyQ
• seek1 (f : VFlags) : BodyQ

  Seek desc head past two □s to the entry region.

• seek2 (f : VFlags) : BodyQ
• cmpQ (f : VFlags) : BodyQ

  Key scan: state field (lockstep with state tape).

• cmpS (f : VFlags) (idx : Fin 6) : BodyQ

  Key scan: the six symbol cells (vs live virtual reads).

• skipSeg (f : VFlags) : BodyQ

  Mismatch: skip desc to the cell after the next □.

• segCheck (f : VFlags) : BodyQ

  After a □: another □ means no-match (default); else next segment.

• mmScr (f : VFlags) : BodyQ

  Mismatch cleanup: blank-rewind scratch.

• rewindSt (f : VFlags) : BodyQ

  Mismatch cleanup: rewind state head, then resume the key scan.

• copyQ' (f : VFlags) : BodyQ

  Copy the q' field to scratch, state head counting down (trick 1).

• copyAct (f : VFlags) (j : Fin 10) : BodyQ

  Copy the ten action cells to scratch.

• appRewScr (f : VFlags) : BodyQ

  Apply: rewind scratch.

• appQ' (f : VFlags) : BodyQ

  Apply: overwrite the state tape with the new state (trick 2).

• appAct (f : VFlags) (g : Fin 5) (pending : Option Bool) : BodyQ

  Apply: decode five 2-cell action groups and act (trick 6).

• dfScr : BodyQ

  Default path: blank-rewind scratch, blank state, copy qhalt field.

• dfStRew : BodyQ
• dfBlank : BodyQ
• dfStRew2 : BodyQ
• dfDescRew : BodyQ
• dfSkip : BodyQ
• dfCopy : BodyQ
• dfStRew3 : BodyQ
• dfDescRew2 : BodyQ
• clScr : BodyQ

  Cleanup after apply: blank-rewind scratch, rewind state and desc.

• clSt : BodyQ
• clDesc : BodyQ
• bodyDone : BodyQ

  Body halt state.

def Complexity.TM.UTMBody.instDecidableEqBodyQ.decEq (x✝ x✝¹ : BodyQ) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.TM.UTMBody.instDecidableEqBodyQ : DecidableEq BodyQ

Equations

• Complexity.TM.UTMBody.instDecidableEqBodyQ = Complexity.TM.UTMBody.instDecidableEqBodyQ.decEq

@[implicit_reducible]

instance Complexity.TM.UTMBody.instFintypeBodyQ : Fintype BodyQ

Equations

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

def Complexity.TM.UTMBody.vIn : Fin 6

Tape indices, for readability (0 vInput, 1 vWork, 2 vOut, 3 state, 4 desc, 5 scratch).

Equations

• Complexity.TM.UTMBody.vIn = 0

def Complexity.TM.UTMBody.vWk : Fin 6

Work-tape index of the simulated work tape.

Equations

• Complexity.TM.UTMBody.vWk = 1

def Complexity.TM.UTMBody.vOut : Fin 6

Work-tape index of the simulated output tape.

Equations

• Complexity.TM.UTMBody.vOut = 2

def Complexity.TM.UTMBody.stT : Fin 6

Work-tape index of the state tape.

Equations

• Complexity.TM.UTMBody.stT = 3

def Complexity.TM.UTMBody.dsT : Fin 6

Work-tape index of the description tape.

Equations

• Complexity.TM.UTMBody.dsT = 4

def Complexity.TM.UTMBody.scT : Fin 6

Work-tape index of the scratch tape.

Equations

• Complexity.TM.UTMBody.scT = 5

def Complexity.TM.UTMBody.simRead (flag : Bool) (live : Γ) : Γ

The simulated read of a virtual tape: ▷ at the origin, else the live cell under the (stationary) shadow head.

Equations

• Complexity.TM.UTMBody.simRead flag live = if flag = true then Complexity.Γ.start else live

def Complexity.TM.UTMBody.cellBit (g : Γ) : Bool

Bit value of a desc-tape cell (Γ.one ↦ true, all else false).

Equations

• Complexity.TM.UTMBody.cellBit g = decide (g = Complexity.Γ.one)

def Complexity.TM.UTMBody.bitCell (b : Bool) : Γ

A bit as the Γ symbol a desc-tape cell should hold.

Equations

• Complexity.TM.UTMBody.bitCell b = if b = true then Complexity.Γ.one else Complexity.Γ.zero

def Complexity.TM.UTMBody.grpΓw (b₀ b₁ : Bool) : Γw

Decode a 2-bit group as a write symbol (must match decΓw): 00→0, 01→1, 10→□, 11→□.

Equations

• Complexity.TM.UTMBody.grpΓw false false = Complexity.Γw.zero
• Complexity.TM.UTMBody.grpΓw false true = Complexity.Γw.one
• Complexity.TM.UTMBody.grpΓw b₀ b₁ = Complexity.Γw.blank

def Complexity.TM.UTMBody.grpDir (b₀ b₁ : Bool) : Dir3

Decode a 2-bit group as a direction (must match decDir): 00→left, 01→right, 10→stay, 11→stay.

Equations

• Complexity.TM.UTMBody.grpDir false false = Complexity.Dir3.left
• Complexity.TM.UTMBody.grpDir false true = Complexity.Dir3.right
• Complexity.TM.UTMBody.grpDir b₀ b₁ = Complexity.Dir3.stay

def Complexity.TM.UTMBody.keyCell (f : VFlags) (v0 v1 v2 : Γ) (idx : Fin 6) : Γ

The expected desc cell at key-symbol index idx (0,1 = input symbol's two encoding bits; 2,3 = work; 4,5 = output), given the flags and live virtual reads.

Equations

• Complexity.TM.UTMBody.keyCell f v0 v1 v2 0 = Complexity.TM.UTMBody.bitCell (Complexity.TM.UTMBody.simRead f.1 v0).encode[0]!
• Complexity.TM.UTMBody.keyCell f v0 v1 v2 1 = Complexity.TM.UTMBody.bitCell (Complexity.TM.UTMBody.simRead f.1 v0).encode[1]!
• Complexity.TM.UTMBody.keyCell f v0 v1 v2 2 = Complexity.TM.UTMBody.bitCell (Complexity.TM.UTMBody.simRead f.2.1 v1).encode[0]!
• Complexity.TM.UTMBody.keyCell f v0 v1 v2 3 = Complexity.TM.UTMBody.bitCell (Complexity.TM.UTMBody.simRead f.2.1 v1).encode[1]!
• Complexity.TM.UTMBody.keyCell f v0 v1 v2 4 = Complexity.TM.UTMBody.bitCell (Complexity.TM.UTMBody.simRead f.2.2 v2).encode[0]!
• Complexity.TM.UTMBody.keyCell f v0 v1 v2 5 = Complexity.TM.UTMBody.bitCell (Complexity.TM.UTMBody.simRead f.2.2 v2).encode[1]!

@[reducible, inline]

abbrev Complexity.TM.UTMBody.TapeActs : Type

A per-tape action: write this symbol and move this way (direction is sanitized against ▷ by the builder). none = idle.

Equations

• Complexity.TM.UTMBody.TapeActs = (Fin 6 → Option (Complexity.Γw × Complexity.Dir3))

def Complexity.TM.UTMBody.mkAct (q' : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (acts : TapeActs) : BodyQ × (Fin 6 → Γw) × Γw × Dir3 × (Fin 6 → Dir3) × Dir3

Build a full δ output from per-work-tape actions; the real input and output tapes always idle. Directions are sanitized (▷ ⇒ right), so δ_right_of_start holds by construction.

Equations

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

def Complexity.TM.UTMBody.idle (q' : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : BodyQ × (Fin 6 → Γw) × Γw × Dir3 × (Fin 6 → Dir3) × Dir3

All tapes idle.

Equations

• Complexity.TM.UTMBody.idle q' iH wH oH = Complexity.TM.UTMBody.mkAct q' iH wH oH fun (x : Fin 6) => none

def Complexity.TM.UTMBody.act1 (q' : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (t : Fin 6) (w : Γw) (d : Dir3) : BodyQ × (Fin 6 → Γw) × Γw × Dir3 × (Fin 6 → Dir3) × Dir3

One active tape.

Equations

• Complexity.TM.UTMBody.act1 q' iH wH oH t w d = Complexity.TM.UTMBody.mkAct q' iH wH oH fun (i : Fin 6) => if i = t then some (w, d) else none

def Complexity.TM.UTMBody.act2 (q' : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (t₁ : Fin 6) (w₁ : Γw) (d₁ : Dir3) (t₂ : Fin 6) (w₂ : Γw) (d₂ : Dir3) : BodyQ × (Fin 6 → Γw) × Γw × Dir3 × (Fin 6 → Dir3) × Dir3

Two active tapes.

Equations

• Complexity.TM.UTMBody.act2 q' iH wH oH t₁ w₁ d₁ t₂ w₂ d₂ = Complexity.TM.UTMBody.mkAct q' iH wH oH fun (i : Fin 6) => if i = t₁ then some (w₁, d₁) else if i = t₂ then some (w₂, d₂) else none

def Complexity.TM.UTMBody.act3 (q' : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (t₁ : Fin 6) (w₁ : Γw) (d₁ : Dir3) (t₂ : Fin 6) (w₂ : Γw) (d₂ : Dir3) (t₃ : Fin 6) (w₃ : Γw) (d₃ : Dir3) : BodyQ × (Fin 6 → Γw) × Γw × Dir3 × (Fin 6 → Dir3) × Dir3

Three active tapes.

Equations

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

def Complexity.TM.UTMBody.rewStep (cur next : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (t : Fin 6) : BodyQ × (Fin 6 → Γw) × Γw × Dir3 × (Fin 6 → Dir3) × Dir3

Rewind step for one tape: left until ▷, bounce right, and continue as next.

Equations

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

def Complexity.TM.UTMBody.blankRewStep (cur next : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (t : Fin 6) : BodyQ × (Fin 6 → Γw) × Γw × Dir3 × (Fin 6 → Dir3) × Dir3

Blank-rewind step for one tape: blank the cell, move left; at ▷ bounce right and continue as next.

Equations

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

def Complexity.TM.UTMBody.bodyδ (q : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : BodyQ × (Fin 6 → Γw) × Γw × Dir3 × (Fin 6 → Dir3) × Dir3

The body machine's transition function.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.TM.UTMBody.bodyδ Complexity.TM.UTMBody.BodyQ.bodyDone iH wH oH = Complexity.TM.UTMBody.idle Complexity.TM.UTMBody.BodyQ.bodyDone iH wH oH

theorem Complexity.TM.UTMBody.mkAct_right_of_start (q' : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (acts : TapeActs) : match mkAct q' iH wH oH acts with | (fst, fst_1, fst_2, inDir, workDirs, outDir) => (iH = Γ.start → inDir = Dir3.right) ∧ (∀ (i : Fin 6), wH i = Γ.start → workDirs i = Dir3.right) ∧ (oH = Γ.start → outDir = Dir3.right)

Every direction mkAct emits obeys the ▷ ⇒ right discipline.

theorem Complexity.TM.UTMBody.bodyδ_shape (q : BodyQ) (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : ∃ (q' : BodyQ) (acts : TapeActs), bodyδ q iH wH oH = mkAct q' iH wH oH acts

Every arm of bodyδ is a mkAct, so the direction discipline holds uniformly.

def Complexity.TM.UTMBody.bodyTM : TM 6

The body machine.

Equations

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