Multi-tape machines with optional oracle channels

A MultiTapeMachine separates the tape interface from the choice of a transition. Ordinary steps use Turing.Action on a Turing.Cfg; in addition, Oracle indexes communication operations. Each operation has a write-only query buffer and a read-only answer tape, and Empty gives a machine without communication.

The operation type names interfaces such as hashing, signing and decryption; it does not contain their request payloads. Payloads are words written to the selected query buffer, so a finite operation type still permits arbitrarily long requests. At the game level, OracleComp can use typed payloads and operation-dependent replies; a machine realization must encode these as words.

Different operations may share one hidden interpreter state. Separate communication channels do not assert independent oracles. In particular, a random-oracle handler must retain its sampled answers across every user of that oracle, including calls made inside another game operation.

Choose describes the result of a transition. A fair-coin table uses fun α => Bool → α, which keeps the action for each coin value, including when the two actions agree.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The effect-free deterministic and nondeterministic interfaces are related step-exactly to upstream machines in MultiTape.Machine.Equivalence.

Main definitions

• Turing.MultiTapeMachine: a transition table parameterized by its choice mechanism.
• Turing.MultiTapeMachine.Config: upstream tapes and control, plus oracle communication channels.
• Turing.MultiTapeMachine.Action.mapState, Turing.MultiTapeMachine.Config.mapState: relabel control states, preserving halting, tape data and communication channels.

No finiteness or complexity assumptions are imposed here. A complexity predicate must require fixed finite control, a finite alphabet and finitely many oracle channels. With these assumptions an ordinary step inspects and updates a fixed number of tape cells. Query submission is a separate step; writing the query and reading its reply require ordinary steps.

inductive Turing.MultiTapeMachine.Action (k : ℕ) (Symbol : Type u) (State : Type v) (Oracle : Type w) : Type (max (max u v) w)

The local tape action and communication updates, or a call to a named oracle.

• step {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} (action : Turing.Action k Symbol State) (querySymbol : Oracle → Option Symbol) (answerMove : Oracle → SignType) : Action k Symbol State Oracle

  Update ordinary tapes, write at most one symbol per query buffer, and move answer heads.

• query {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} (oracle : Oracle) (next : State) : Action k Symbol State Oracle

  Submit one buffer, install its reply, and resume in the specified state.

def Turing.MultiTapeMachine.Action.mapState {k : ℕ} {Symbol : Type u} {State : Type v} {State' : Type x} {Oracle : Type w} (e : State → State') : Action k Symbol State Oracle → Action k Symbol State' Oracle

Rename the successor state of an instruction.

structure Turing.MultiTapeMachine.Channel (Symbol : Type u) : Type u

The communication state for one oracle. It is separate from the oracle's private state.

• queryBuffer : List Symbol

  Symbols written since the last query.

• answer : List Symbol

  The last reply, read only through the answer head.

• answerPos : ℤ

  The first answer symbol has position zero.

theorem Turing.MultiTapeMachine.Channel.ext {Symbol : Type u} {x y : Channel Symbol} (queryBuffer : x.queryBuffer = y.queryBuffer) (answer : x.answer = y.answer) (answerPos : x.answerPos = y.answerPos) : x = y

theorem Turing.MultiTapeMachine.Channel.ext_iff {Symbol : Type u} {x y : Channel Symbol} : x = y ↔ x.queryBuffer = y.queryBuffer ∧ x.answer = y.answer ∧ x.answerPos = y.answerPos

structure Turing.MultiTapeMachine.Config (k : ℕ) (Symbol : Type u) (State : Type v) (Oracle : Type w) (input : List Symbol) : Type (max (max u v) w)

Ordinary machine tapes together with the communication state of each oracle channel.

• tapes : Cfg k Symbol State input

  The shared configuration of ordinary tapes and control.

• channels : Oracle → Channel Symbol

  Each oracle has its own query buffer and answer head.

theorem Turing.MultiTapeMachine.Config.ext {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} {input : List Symbol} {x y : Config k Symbol State Oracle input} (tapes : x.tapes = y.tapes) (channels : x.channels = y.channels) : x = y

theorem Turing.MultiTapeMachine.Config.ext_iff {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} {input : List Symbol} {x y : Config k Symbol State Oracle input} : x = y ↔ x.tapes = y.tapes ∧ x.channels = y.channels

def Turing.MultiTapeMachine.Config.mapState {k : ℕ} {Symbol : Type u} {State : Type v} {State' : Type x} {Oracle : Type w} {input : List Symbol} (e : State → State') (cfg : Config k Symbol State Oracle input) : Config k Symbol State' Oracle input

Rename the control state of a configuration, keeping its tapes and channels.

@[simp]

theorem Turing.MultiTapeMachine.Config.mapState_tapes_state {k : ℕ} {Symbol : Type u} {State : Type v} {State' : Type x} {Oracle : Type w} {input : List Symbol} (e : State → State') (cfg : Config k Symbol State Oracle input) : (mapState e cfg).tapes.state = Option.map e cfg.tapes.state

@[simp]

theorem Turing.MultiTapeMachine.Config.mapState_tapes_output {k : ℕ} {Symbol : Type u} {State : Type v} {State' : Type x} {Oracle : Type w} {input : List Symbol} (e : State → State') (cfg : Config k Symbol State Oracle input) : (mapState e cfg).tapes.output = cfg.tapes.output

def Turing.MultiTapeMachine.Channel.answerSymbol {Symbol : Type u} (channel : Channel Symbol) : Option Symbol

Read the cell under a channel's answer head; positions outside the reply are blank.

def Turing.MultiTapeMachine.Config.answerSymbols {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} {input : List Symbol} (cfg : Config k Symbol State Oracle input) : Oracle → Option Symbol

Read one answer cell per channel.

def Turing.MultiTapeMachine.Config.step {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (action : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) : Config k Symbol State Oracle input

Apply one ordinary tape action and the channel-local writes and head moves.

def Turing.MultiTapeMachine.Config.receive {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} {input : List Symbol} [DecidableEq Oracle] (cfg : Config k Symbol State Oracle input) (oracle : Oracle) (next : State) (answer : List Symbol) : Config k Symbol State Oracle input

Install a reply on the selected channel, clear its query buffer, and reset its answer head. All other communication channels and all ordinary tapes are preserved.

theorem Turing.MultiTapeMachine.Config.mapState_step {k : ℕ} {Symbol : Type u} {State : Type v} {State' : Type x} {Oracle : Type w} {input : List Symbol} (e : State → State') (cfg : Config k Symbol State Oracle input) (action : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) : (mapState e cfg).step { inputTape := action.inputTape, workTapes := action.workTapes, output := action.output, state := Option.map e action.state } symbol move = mapState e (cfg.step action symbol move)

theorem Turing.MultiTapeMachine.Config.mapState_receive {k : ℕ} {Symbol : Type u} {State : Type v} {State' : Type x} {Oracle : Type w} {input : List Symbol} [DecidableEq Oracle] (e : State → State') (cfg : Config k Symbol State Oracle input) (oracle : Oracle) (next : State) (answer : List Symbol) : (mapState e cfg).receive oracle (e next) answer = mapState e (cfg.receive oracle next answer)

structure Turing.MultiTapeMachine (k : ℕ) (Symbol : Type u) (State : Type v) (Oracle : Type w) (Choose : Type (max u v w) → Type x) : Type (max (max (max u v) w) x)

A multi-tape transition table with an explicit choice mechanism and optional oracle channels.

• initial : State

  Initial control state.

• tr : State → Option Symbol → (Fin k → Option Symbol) → (Oracle → Option Symbol) → Choose (Action k Symbol State Oracle)

  Inspect only the current state and the symbols under the input, work and answer heads.

theorem Turing.MultiTapeMachine.ext {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} {Choose : Type (max u v w) → Type x} {x y : MultiTapeMachine k Symbol State Oracle Choose} (initial : x.initial = y.initial) (tr : x.tr = y.tr) : x = y

theorem Turing.MultiTapeMachine.ext_iff {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} {Choose : Type (max u v w) → Type x} {x y : MultiTapeMachine k Symbol State Oracle Choose} : x = y ↔ x.initial = y.initial ∧ x.tr = y.tr

def Turing.MultiTapeMachine.initialConfig {k : ℕ} {Symbol : Type u} {State : Type v} {Oracle : Type w} {Choose : Type (max u v w) → Type x} (machine : MultiTapeMachine k Symbol State Oracle Choose) (input : List Symbol) : Config k Symbol State Oracle input

Start with the ordinary initial configuration and empty communication channels.