Buffering an effectful machine's output

The output is redirected to a fresh last work tape, whose head remains at the write frontier. The real output stays empty. All choices and oracle interactions are preserved as a typed program, so this construction also retains state shared by coin and query interpreters.

The configuration map reuses upstream's outCfg. No budget or already computed output is supplied to the machine: an initially blank buffer is filled one source instruction at a time.

Main definitions

• Turing.MultiTapeMachine.outputToTape: buffer the source output without adding instructions.
• Turing.MultiTapeMachine.OutputToTape.config: retain source data and communication channels.

Main results

• Turing.MultiTapeMachine.runConfigFrom_outputToTape: preserve the whole clocked program.
• Turing.MultiTapeMachine.toTM_outputToTape: agree exactly with upstream's deterministic compiler.

References

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

def Turing.MultiTapeMachine.OutputToTape.action {k : ℕ} {Symbol State : Type} (a : Turing.Action k Symbol State) : Turing.Action (k + 1) Symbol State

Redirect an emitted symbol to the fresh work tape and advance its write frontier.

def Turing.MultiTapeMachine.OutputToTape.instruction {k : ℕ} {Symbol State Oracle : Type} : Action k Symbol State Oracle → Action (k + 1) Symbol State Oracle

Redirect ordinary output writes while retaining communication instructions.

def Turing.MultiTapeMachine.OutputToTape.config {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) : Config (k + 1) Symbol State Oracle input

Upstream's output-buffered configuration, with every communication channel retained.

@[simp]

theorem Turing.MultiTapeMachine.OutputToTape.config_state {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) : (config cfg).tapes.state = cfg.tapes.state

@[simp]

theorem Turing.MultiTapeMachine.OutputToTape.config_inputSymbol {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) : (config cfg).tapes.inputSymbol = cfg.tapes.inputSymbol

@[simp]

theorem Turing.MultiTapeMachine.OutputToTape.config_workTapeSymbols {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (i : Fin k) : (config cfg).tapes.workTapeSymbols i.castSucc = cfg.tapes.workTapeSymbols i

@[simp]

theorem Turing.MultiTapeMachine.OutputToTape.config_channels {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) : (config cfg).channels = cfg.channels

@[simp]

theorem Turing.MultiTapeMachine.OutputToTape.config_answerSymbols {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) : (config cfg).answerSymbols = cfg.answerSymbols

theorem Turing.MultiTapeMachine.OutputToTape.step_config {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (a : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) : (config cfg).step (action a) symbol move = config (cfg.step a symbol move)

A source output write appends exactly one cell at the buffer's write frontier.

theorem Turing.MultiTapeMachine.OutputToTape.receive_config {k : ℕ} {Symbol State Oracle : Type} {input : List Symbol} [DecidableEq Oracle] (cfg : Config k Symbol State Oracle input) (oracle : Oracle) (next : State) (answer : List Symbol) : (config cfg).receive oracle next answer = config (cfg.receive oracle next answer)

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

Buffer output on a fresh work tape, retaining the source's oracle interactions.

@[simp]

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

theorem Turing.MultiTapeMachine.outputToTape_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 + 1) → Option Symbol) (answer : Oracle → Option Symbol) : machine.outputToTape.tr state symbol work answer = OutputToTape.instruction <$> machine.tr state symbol (fun (i : Fin k) => work i.castSucc) answer

Unfold a single redirected transition without unfolding its machine in continuations.

theorem Turing.MultiTapeMachine.runConfigFrom_outputToTape {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)) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) : machine.outputToTape.runConfigFrom choose query fuel (OutputToTape.config cfg) = OutputToTape.config <$> machine.runConfigFrom choose query fuel cfg

Output buffering preserves the complete program, including the source's communication state.

theorem Turing.MultiTapeMachine.initialConfig_outputToTape {k : ℕ} {Symbol State Oracle : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k Symbol State Oracle Choose) (input : List Symbol) : machine.outputToTape.initialConfig input = OutputToTape.config (machine.initialConfig input)

Output buffering starts with a blank work tape, without a precomputed output word.

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

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