Reading an effectful machine's input from work tapes

Two fresh work tapes hold the virtual input and its left-boundary marker. The compiler reuses upstream's clamped-input simulation, retaining all typed choices and oracle interactions. The real input head stays at its original position, and the real input is never inspected.

The simulation starts from a prepared virtual input. Preparing these tapes is a separate computation whose cost must be included when composing machines.

Main definitions

• Turing.MultiTapeMachine.inputFromTape: read a virtual input without adding instructions.
• Turing.MultiTapeMachine.InputFromTape.config: embed the input and retain all oracle channels.

Main results

• Turing.MultiTapeMachine.runConfigFrom_inputFromTape: preserve the complete clocked program.
• Turing.MultiTapeMachine.toTM_inputFromTape: agree with upstream's deterministic compiler.

References

Adapted from MultiTape/Oracle/InputFromTape.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common machine and upstream input redirection by Christian Reitwiessner and Samuel Schlesinger.

def Turing.MultiTapeMachine.InputFromTape.action {k : ℕ} {Symbol State : Type} (a : Turing.Action k Symbol State) (symbol flag : Option Symbol) : Turing.Action (k + 2) Symbol State

Move the virtual input and boundary heads together, clamping at either end.

def Turing.MultiTapeMachine.InputFromTape.instruction {k : ℕ} {Symbol State Oracle : Type} (symbol flag : Option Symbol) : Action k Symbol State Oracle → Action (k + 2) Symbol State Oracle

Redirect input movement while retaining communication instructions.

def Turing.MultiTapeMachine.InputFromTape.config {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : Config (k + 2) Symbol State Oracle outerInput

Embed the source input on work tapes while retaining every communication channel.

@[simp]

theorem Turing.MultiTapeMachine.InputFromTape.config_state {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : (config mark cfg outerInput outerPosition).tapes.state = cfg.tapes.state

@[simp]

theorem Turing.MultiTapeMachine.InputFromTape.config_workTapeSymbols {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) (i : Fin k) : (config mark cfg outerInput outerPosition).tapes.workTapeSymbols (Fin.castAdd 2 i) = cfg.tapes.workTapeSymbols i

@[simp]

theorem Turing.MultiTapeMachine.InputFromTape.config_inputSymbol {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : (config mark cfg outerInput outerPosition).tapes.workTapeSymbols (Fin.natAdd k 0) = cfg.tapes.inputSymbol

@[simp]

theorem Turing.MultiTapeMachine.InputFromTape.config_flagSymbol {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : (config mark cfg outerInput outerPosition).tapes.workTapeSymbols (Fin.natAdd k 1) = if ↑cfg.tapes.inputPos = 0 then some mark else none

@[simp]

theorem Turing.MultiTapeMachine.InputFromTape.config_channels {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : (config mark cfg outerInput outerPosition).channels = cfg.channels

@[simp]

theorem Turing.MultiTapeMachine.InputFromTape.config_answerSymbols {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : (config mark cfg outerInput outerPosition).answerSymbols = cfg.answerSymbols

@[simp]

theorem Turing.MultiTapeMachine.InputFromTape.config_output {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : (config mark cfg outerInput outerPosition).tapes.output = cfg.tapes.output

theorem Turing.MultiTapeMachine.InputFromTape.step_config {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) (a : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) : (config mark cfg outerInput outerPosition).step (action a cfg.tapes.inputSymbol (if ↑cfg.tapes.inputPos = 0 then some mark else none)) symbol move = config mark (cfg.step a symbol move) outerInput outerPosition

Upstream's clamped move preserves the virtual input geometry after every instruction.

theorem Turing.MultiTapeMachine.InputFromTape.receive_config {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (mark : Symbol) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) [DecidableEq Oracle] (oracle : Oracle) (next : State) (answer : List Symbol) : (config mark cfg outerInput outerPosition).receive oracle next answer = config mark (cfg.receive oracle next answer) outerInput outerPosition

def Turing.MultiTapeMachine.inputFromTape {k : ℕ} {Symbol State Oracle : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k Symbol State Oracle Choose) : MultiTapeMachine (k + 2) Symbol State Oracle Choose

Read the input from two fresh work tapes: a word and its boundary marker.

@[simp]

theorem Turing.MultiTapeMachine.inputFromTape_initial {k : ℕ} {Symbol State Oracle : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k Symbol State Oracle Choose) : machine.inputFromTape.initial = machine.initial

theorem Turing.MultiTapeMachine.inputFromTape_tr {k : ℕ} {Symbol State Oracle : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k Symbol State Oracle Choose) (state : State) (symbol : Option Symbol) (work : Fin (k + 2) → Option Symbol) (answer : Oracle → Option Symbol) : machine.inputFromTape.tr state symbol work answer = InputFromTape.instruction (work (Fin.natAdd k 0)) (work (Fin.natAdd k 1)) <$> machine.tr state (work (Fin.natAdd k 0)) (fun (i : Fin k) => work (Fin.castAdd 2 i)) answer

Unfold a single virtual-input transition without unfolding its machine in continuations.

theorem Turing.MultiTapeMachine.runConfigFrom_inputFromTape {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (mark : Symbol) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : machine.inputFromTape.runConfigFrom choose query fuel (InputFromTape.config mark cfg outerInput outerPosition) = (fun (final : Config k Symbol State Oracle input) => InputFromTape.config mark final outerInput outerPosition) <$> machine.runConfigFrom choose query fuel cfg

Virtual input preserves the complete program, including communication and private state.

theorem Turing.MultiTapeMachine.runFrom_inputFromTape {k : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (mark : Symbol) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : machine.inputFromTape.runFrom choose query fuel (InputFromTape.config mark cfg outerInput outerPosition) = machine.runFrom choose query fuel cfg

The virtual-input compiler emits exactly the source output program.

theorem Turing.MultiTapeMachine.toTM_inputFromTape {k : ℕ} {Symbol State : Type} (machine : MultiTapeMachine k Symbol State Empty Id) : machine.inputFromTape.toTM = machine.toTM.inputFromTape

Effect-free deterministic input redirection is exactly upstream's compiler.