Shared tape layout for closed buffered composition

The source runs on its own work tapes and writes to a fresh output buffer. The consumer has separate initially blank work tapes and reads that buffer through the existing virtual-input compiler. A native deterministic handoff rewinds the buffer and marks its left boundary in exactly the word length plus four transitions. Source scratch and the real input head remain explicit in the configuration maps; no clearing or copying occurs outside machine instructions.

These maps and program laws are independent of the transition-choice mechanism. The complete compiler must still supply its choice-preserving deterministic lift and prove halting/count laws. The scope here is closed machines with no oracle channels.

Main definitions

• Turing.MultiTapeMachine.Composition.source: reserve consumer tapes and buffer source output.
• Turing.MultiTapeMachine.Composition.consumer: read the buffer on separate work tapes.
• Turing.MultiTapeMachine.Composition.consumerConfig: the exact joint tape layout.

Main results

• Turing.MultiTapeMachine.Composition.runConfigFrom_source: exact source program embedding.
• Turing.MultiTapeMachine.Composition.runConfigFrom_consumer: exact consumer program embedding.
• Turing.MultiTapeMachine.Composition.runFrom_prepare: the charged native buffer handoff.

References

Extracted from MultiTape.Probabilistic.Composition, adapted from MultiTape/Oracle/Composition.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The native deterministic tape plumbing is by Christian Reitwiessner and Samuel Schlesinger.

def Turing.MultiTapeMachine.Composition.reserve {k₀ : ℕ} {Symbol State₀ : Type} {input : List Symbol} (k₁ : ℕ) (cfg : Config k₀ Symbol State₀ Empty input) : Config (k₁ + k₀) Symbol State₀ Empty input

Reserve blank continuation tapes before the source's work tapes.

def Turing.MultiTapeMachine.Composition.buffer {k₀ : ℕ} {Symbol State₀ : Type} {input : List Symbol} (k₁ : ℕ) (cfg : Config k₀ Symbol State₀ Empty input) : Config (k₁ + k₀ + 2) Symbol State₀ Empty input

Buffer the source result and reserve a blank boundary-marker tape.

def Turing.MultiTapeMachine.Composition.source {k₀ : ℕ} {Symbol State₀ : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k₀ Symbol State₀ Empty Choose) (k₁ : ℕ) : MultiTapeMachine (k₁ + k₀ + 2) Symbol State₀ Empty Choose

Run the source on its own tapes, redirecting its output to the virtual input buffer.

def Turing.MultiTapeMachine.Composition.consumer {k₁ : ℕ} {Symbol State₁ : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k₁ Symbol State₁ Empty Choose) (k₀ : ℕ) : MultiTapeMachine (k₁ + k₀ + 2) Symbol State₁ Empty Choose

Run the continuation on separate work tapes, reading the virtual input.

def Turing.MultiTapeMachine.Composition.consumerConfig {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (mark : Symbol) (cfg₀ : Config k₀ Symbol State₀ Empty input) (cfg₁ : Config k₁ Symbol State₁ Empty cfg₀.tapes.output) : Config (k₁ + k₀ + 2) Symbol State₁ Empty input

Retain the first machine's scratch tapes while the continuation runs on its output.

def Turing.MultiTapeMachine.Composition.ready {k₀ : ℕ} {Symbol State₀ : Type} {input : List Symbol} (mark : Symbol) (k₁ : ℕ) (cfg : Config k₀ Symbol State₀ Empty input) : Config (k₁ + k₀ + 2) Symbol (MultiTapeTM.MarkWorkState ⊕ MultiTapeTM.RewindWorkState) Empty input

The prepared virtual input, with every source work tape retained.

theorem Turing.MultiTapeMachine.Composition.runConfigFrom_source {k₀ : ℕ} {Symbol State₀ : Type} {Choose : Type → Type v} {Query : Type u} {spec : Cslib.OracleSpec Query} [Functor Choose] (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (machine : MultiTapeMachine k₀ Symbol State₀ Empty Choose) (k₁ fuel : ℕ) (input : List Symbol) : (source machine k₁).runConfigFrom choose Empty.elim fuel ((source machine k₁).initialConfig input) = buffer k₁ <$> machine.runConfigFrom choose Empty.elim fuel (machine.initialConfig input)

Buffering the source preserves its complete configuration program from initialized tapes.

theorem Turing.MultiTapeMachine.Composition.runConfigFrom_consumer {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} {Choose : Type → Type v} {Query : Type u} {spec : Cslib.OracleSpec Query} [Functor Choose] (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (machine : MultiTapeMachine k₁ Symbol State₁ Empty Choose) (mark : Symbol) (cfg₀ : Config k₀ Symbol State₀ Empty input) (cfg₁ : Config k₁ Symbol State₁ Empty cfg₀.tapes.output) (fuel : ℕ) : (consumer machine k₀).runConfigFrom choose Empty.elim fuel (consumerConfig mark cfg₀ cfg₁) = consumerConfig mark cfg₀ <$> machine.runConfigFrom choose Empty.elim fuel cfg₁

The consumer preserves its complete program and every reserved source scratch tape.

theorem Turing.MultiTapeMachine.Composition.buffer_tapes {k₀ : ℕ} {Symbol State₀ : Type} {input : List Symbol} (k₁ : ℕ) (cfg : Config k₀ Symbol State₀ Empty input) : (buffer k₁ cfg).tapes = { state := cfg.tapes.state, inputPos := cfg.tapes.inputPos, workTapes := Fin.append (reserve k₁ cfg).tapes.workTapes ![tapeOfList cfg.tapes.output, fun (x : ℤ) => none], workTapePos := Fin.append (reserve k₁ cfg).tapes.workTapePos ![↑cfg.tapes.output.length, 0], output := [] }

The two new tapes are the completed output buffer and a blank boundary tape.

theorem Turing.MultiTapeMachine.Composition.runFrom_prepare {k₀ : ℕ} {Symbol State₀ : Type} {input : List Symbol} (mark : Symbol) (k₁ : ℕ) (cfg : Config k₀ Symbol State₀ Empty input) : MultiTapeTM.runFrom ((buffer k₁ cfg).tapes.withState (some (MultiTapeTM.prepareInput (k₁ + k₀) mark).q₀)) (cfg.tapes.output.length + 4) = (ready mark k₁ cfg).tapes

The handoff costs the buffered word length plus four, with no assumptions on source scratch.

theorem Turing.MultiTapeMachine.Composition.start_ready {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k₁ Symbol State₁ Empty Choose) (mark : Symbol) (cfg : Config k₀ Symbol State₀ Empty input) : Sequential.start (consumer machine k₀) (ready mark k₁ cfg) = consumerConfig mark cfg (machine.initialConfig cfg.tapes.output)

The prepared input starts the consumer with blank work tapes while retaining source scratch.

def Turing.MultiTapeMachine.Composition.finalConfig {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (mark : Symbol) (cfg₀ : Config k₀ Symbol State₀ Empty input) (cfg₁ : Config k₁ Symbol State₁ Empty cfg₀.tapes.output) : Config (k₁ + k₀ + 2) Symbol (State₀ ⊕ (MultiTapeTM.MarkWorkState ⊕ MultiTapeTM.RewindWorkState) ⊕ State₁) Empty input

The control-state embeddings of a completed buffered composition.

@[simp]

theorem Turing.MultiTapeMachine.Composition.finalConfig_output {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (mark : Symbol) (cfg₀ : Config k₀ Symbol State₀ Empty input) (cfg₁ : Config k₁ Symbol State₁ Empty cfg₀.tapes.output) : (finalConfig mark cfg₀ cfg₁).tapes.output = cfg₁.tapes.output