An auxiliary tape for machine controllers

A controller can retain a source configuration, including its oracle channels, alongside a phase in finite control and an additional work tape. Clocks use a Boolean phase; saved-coin replay uses an optional bit. The source's tape actions and oracle replies keep their original effects.

Main definitions

• Turing.MultiTapeMachine.AuxiliaryTape.config: retain source data with a controller phase.
• Turing.MultiTapeMachine.AuxiliaryTape.move: change control and move the extra head.
• Turing.MultiTapeMachine.AuxiliaryTape.liftAction: retain the extra tape during a source action.
• Turing.MultiTapeMachine.AuxiliaryTape.stopped: halt while retaining source data and channels.

Main results

• Turing.MultiTapeMachine.AuxiliaryTape.step_liftAction: retain source tape and channel effects.
• Turing.MultiTapeMachine.AuxiliaryTape.step_move: move only the additional head.

References

Generalizes the shared controller operations from MultiTape.Machine.Clock, adapted there from MultiTape/Oracle/Clock.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Turing.MultiTapeMachine.AuxiliaryTape.config {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) : Config (k + 1) Bool (Phase × Option State) Oracle input

Retain source tapes and channels with a phase and one additional work tape.

def Turing.MultiTapeMachine.AuxiliaryTape.move {k : ℕ} {State Phase : Type} (next : Option (Phase × Option State)) (direction : SignType) : Turing.Action (k + 1) Bool (Phase × Option State)

Change control and move only the auxiliary head.

def Turing.MultiTapeMachine.AuxiliaryTape.liftAction {k : ℕ} {State Phase : Type} (phase : Phase) (action : Turing.Action k Bool State) : Turing.Action (k + 1) Bool (Phase × Option State)

Perform a source tape action and select the next phase, retaining the auxiliary tape.

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.config_state {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) : (config cfg tape position phase).tapes.state = some (phase, cfg.tapes.state)

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.config_inputSymbol {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) : (config cfg tape position phase).tapes.inputSymbol = cfg.tapes.inputSymbol

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.config_workTapeSymbols_castSucc {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) (i : Fin k) : (config cfg tape position phase).tapes.workTapeSymbols i.castSucc = cfg.tapes.workTapeSymbols i

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.config_workTapeSymbols_last {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) : (config cfg tape position phase).tapes.workTapeSymbols (Fin.last k) = tape position

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.config_answerSymbols {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) : (config cfg tape position phase).answerSymbols = cfg.answerSymbols

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.config_channels {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) : (config cfg tape position phase).channels = cfg.channels

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.config_output {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) : (config cfg tape position phase).tapes.output = cfg.tapes.output

theorem Turing.MultiTapeMachine.AuxiliaryTape.step_liftAction {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (before after : Phase) (action : Turing.Action k Bool State) (symbol : Oracle → Option Bool) (direction : Oracle → SignType) : (config cfg tape position before).step (liftAction after action) symbol direction = config (cfg.step action symbol direction) tape position after

Lifting a source action preserves its tape and communication effects.

theorem Turing.MultiTapeMachine.AuxiliaryTape.receive_config {k : ℕ} {State Oracle Phase : Type} {input : List Bool} [DecidableEq Oracle] (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (before after : Phase) (oracle : Oracle) (next : State) (answer : List Bool) : (config cfg tape position before).receive oracle (after, some next) answer = config (cfg.receive oracle next answer) tape position after

Receiving a reply changes exactly the source channel and control.

theorem Turing.MultiTapeMachine.AuxiliaryTape.step_move {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (before after : Phase) (direction : SignType) : ((config cfg tape position before).step (move (some (after, cfg.tapes.state)) direction) (fun (x : Oracle) => none) fun (x : Oracle) => 0) = config cfg tape (position + ↑direction) after

Moving the auxiliary head leaves source data and communication channels unchanged.

def Turing.MultiTapeMachine.AuxiliaryTape.stopped {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) : Config (k + 1) Bool (Phase × Option State) Oracle input

Halt the controller without changing its data or channels.

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.stopped_state {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) : (stopped cfg tape position).tapes.state = none

@[simp]

theorem Turing.MultiTapeMachine.AuxiliaryTape.stopped_output {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) : (stopped cfg tape position).tapes.output = cfg.tapes.output

theorem Turing.MultiTapeMachine.AuxiliaryTape.step_stop {k : ℕ} {State Oracle Phase : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (phase : Phase) : ((config cfg tape position phase).step (move none 0) (fun (x : Oracle) => none) fun (x : Oracle) => 0) = stopped cfg tape position

A stationary head update can stop the controller, preserving all data.