Preparing a buffered word for use as input

A completed output buffer has its head just past the word. prepareInput marks the cell left of the flag head and rewinds the word, using the existing markWork and rewindWork machines. Every other tape and head, the real input head, and the output are preserved.

Main definitions

• Turing.MultiTapeTM.prepareInput: prepare the last two work tapes as a virtual input.

Main results

• Turing.MultiTapeTM.runFrom_prepareInput: the handoff costs word.length + 4 transitions, including when the word is empty.

References

Adapted from MultiTape/Plumbing/PrepareInput.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing Christian Reitwiessner's tape routines.

noncomputable def Turing.MultiTapeTM.prepareInput {Symbol : Type u_1} (k : ℕ) (mark : Symbol) : MultiTapeTM (k + 2) Symbol (MarkWorkState ⊕ RewindWorkState)

Mark the left boundary and rewind the buffered word on the last two work tapes.

theorem Turing.MultiTapeTM.runFrom_prepareInput {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (mark : Symbol) (cfg : Cfg (k + 2) Symbol State input) (word : List Symbol) (hword : cfg.workTapes (Fin.natAdd k 0) = tapeOfList word) (hhead : cfg.workTapePos (Fin.natAdd k 0) = ↑word.length) (hflag : cfg.workTapePos (Fin.natAdd k 1) = 0) : runFrom (cfg.withState (some (prepareInput k mark).q₀)) (word.length + 4) = have __src := cfg.withState none; { state := __src.state, inputPos := __src.inputPos, workTapes := Function.update cfg.workTapes (Fin.natAdd k 1) (Function.update (cfg.workTapes (Fin.natAdd k 1)) (-1) (some mark)), workTapePos := Function.update cfg.workTapePos (Fin.natAdd k 0) 0, output := __src.output }

Preparation rewinds the buffered word and marks its left boundary, preserving all other data. The flag head must start at zero; the caller ensures its tape is otherwise blank.