An internal clock on a work tape

withClock reserves a last work tape for a unary budget. Each true cell permits one source instruction, implemented by two target instructions. The first other cell stops the controller. After the source halts, the controller consumes the remaining budget without changing source tapes or communication channels. Preparing this tape is a separate computation: a machine does not receive a polynomial-sized budget for free.

The choice interpreter must commute with mapping and interpret a constant choice as a pure result with unchanged private state. For probabilistic machines, stateless coin draws satisfy these conditions even when controller instructions discard their result. Query programs may modify shared private state.

Main definitions

• Turing.MultiTapeMachine.withClock: consume a budget stored on a fresh work tape.
• Turing.MultiTapeMachine.Clock.config: embed source data alongside the clock tape and head.

Main results

• Turing.MultiTapeMachine.run_interpret_runConfigFrom_withClock_add: a budget of t cells reproduces the externally clocked source in 2 * t + 1 instructions, with arbitrary padding.
• Turing.MultiTapeMachine.withClock_halted: every supported final configuration has halted.

References

Adapted from MultiTape/Oracle/Clock.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the common machine and typed program interface.

@[reducible, inline]

abbrev Turing.MultiTapeMachine.Clock.Control (State : Type) : Type

A phase bit and the source's optional control state.

def Turing.MultiTapeMachine.Clock.config {k : ℕ} {State Oracle : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (ticking : Bool) : Config (k + 1) Bool (Control State) Oracle input

Add a budget tape; a true phase bit means the next instruction advances its head.

def Turing.MultiTapeMachine.Clock.idle {k : ℕ} {State : Type} (next : Option (Control State)) : Turing.Action (k + 1) Bool (Control State)

Leave all source tapes unchanged.

def Turing.MultiTapeMachine.Clock.tick {k : ℕ} {State : Type} (next : Option State) : Turing.Action (k + 1) Bool (Control State)

Advance the budget head while leaving all source tapes unchanged.

def Turing.MultiTapeMachine.Clock.liftAction {k : ℕ} {State : Type} (action : Turing.Action k Bool State) : Turing.Action (k + 1) Bool (Control State)

Perform one source tape action, then enter the clock-advance phase.

def Turing.MultiTapeMachine.Clock.liftInstruction {k : ℕ} {State Oracle : Type} : Action k Bool State Oracle → Action (k + 1) Bool (Control State) Oracle

Lift either a tape instruction or an oracle submission to the clock controller.

def Turing.MultiTapeMachine.withClock {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} [Applicative Choose] (machine : MultiTapeMachine k Bool State Oracle Choose) : MultiTapeMachine (k + 1) Bool (Clock.Control State) Oracle Choose

Run under a unary budget on the last work tape; its construction is a separate computation.

@[simp]

theorem Turing.MultiTapeMachine.withClock_initial {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} [Applicative Choose] (machine : MultiTapeMachine k Bool State Oracle Choose) : machine.withClock.initial = (false, some machine.initial)

theorem Turing.MultiTapeMachine.withClock_tr {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} [Applicative Choose] (machine : MultiTapeMachine k Bool State Oracle Choose) (control : Clock.Control State) (symbol : Option Bool) (work : Fin (k + 1) → Option Bool) (answer : Oracle → Option Bool) : machine.withClock.tr control symbol work answer = if control.1 = true then pure (Action.step (Clock.tick control.2) (fun (x : Oracle) => none) fun (x : Oracle) => 0) else if work (Fin.last k) = some true then match control.2 with | none => pure (Action.step (Clock.idle (some (true, none))) (fun (x : Oracle) => none) fun (x : Oracle) => 0) | some state => Clock.liftInstruction <$> machine.tr state symbol (fun (i : Fin k) => work i.castSucc) answer else pure (Action.step (Clock.idle none) (fun (x : Oracle) => none) fun (x : Oracle) => 0)

Unfold one controller instruction without unfolding the machine in its continuation.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Turing.MultiTapeMachine.Clock.step_liftAction {k : ℕ} {State Oracle : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (action : Turing.Action k Bool State) (symbol : Oracle → Option Bool) (move : Oracle → SignType) : (config cfg tape position false).step (liftAction action) symbol move = config (cfg.step action symbol move) tape position true

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

theorem Turing.MultiTapeMachine.Clock.step_tick {k : ℕ} {State Oracle : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) : ((config cfg tape position true).step (tick cfg.tapes.state) (fun (x : Oracle) => none) fun (x : Oracle) => 0) = config cfg tape (position + 1) false

theorem Turing.MultiTapeMachine.Clock.step_idle {k : ℕ} {State Oracle : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (ticking : Bool) (next : Option (Control State)) : ((config cfg tape position ticking).step (idle next) (fun (x : Oracle) => none) fun (x : Oracle) => 0) = have __src := config cfg tape position ticking; { tapes := (config cfg tape position ticking).tapes.withState next, channels := __src.channels }

theorem Turing.MultiTapeMachine.Clock.step_pause {k : ℕ} {State Oracle : Type} {input : List Bool} (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) : ((config cfg tape position false).step (idle (some (true, cfg.tapes.state))) (fun (x : Oracle) => none) fun (x : Oracle) => 0) = config cfg tape position true

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

Stop the controller, retaining the source tapes, channels, and exhausted budget tape.

@[simp]

theorem Turing.MultiTapeMachine.Clock.stopped_state {k : ℕ} {State Oracle : 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.Clock.stopped_output {k : ℕ} {State Oracle : 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.Clock.run_interpret_tick {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} {input : List Bool} [Applicative Choose] [DecidableEq Oracle] {Query : Type u} {spec : Cslib.OracleSpec Query} {OracleState : Type} (machine : MultiTapeMachine k Bool State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hpure : ∀ {α : Type} (a : α) (s : OracleState), (Cslib.OracleComp.interpret oracle (choose (pure a))).run s = PMF.pure (a, s)) (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (s : OracleState) : (Cslib.OracleComp.interpret oracle (machine.withClock.runConfigFrom choose query 1 (config cfg tape position true))).run s = PMF.pure (config cfg tape (position + 1) false, s)

The clock-advance instruction leaves the source and private interpreter state unchanged.

theorem Turing.MultiTapeMachine.Clock.run_interpret_pair {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} {input : List Bool} [Applicative Choose] [DecidableEq Oracle] {Query : Type u} {spec : Cslib.OracleSpec Query} {OracleState : Type} (machine : MultiTapeMachine k Bool State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hpure : ∀ {α : Type} (a : α) (s : OracleState), (Cslib.OracleComp.interpret oracle (choose (pure a))).run s = PMF.pure (a, s)) (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (s : OracleState) (hcell : tape position = some true) : (Cslib.OracleComp.interpret oracle (machine.withClock.runConfigFrom choose query 2 (config cfg tape position false))).run s = PMF.map (fun (x : Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (config final tape (position + 1) false, s')) ((Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query 1 cfg)).run s)

One available budget cell permits one source instruction and one clock advance.

theorem Turing.MultiTapeMachine.Clock.run_interpret_prefix {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} {input : List Bool} [Applicative Choose] [DecidableEq Oracle] {Query : Type u} {spec : Cslib.OracleSpec Query} {OracleState : Type} (machine : MultiTapeMachine k Bool State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hpure : ∀ {α : Type} (a : α) (s : OracleState), (Cslib.OracleComp.interpret oracle (choose (pure a))).run s = PMF.pure (a, s)) (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (fuel : ℕ) (s : OracleState) (hbudget : ∀ i < fuel, tape (position + ↑i) = some true) : (Cslib.OracleComp.interpret oracle (machine.withClock.runConfigFrom choose query (2 * fuel) (config cfg tape position false))).run s = PMF.map (fun (x : Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (config final tape (position + ↑fuel) false, s')) ((Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query fuel cfg)).run s)

A bounded simulation advances the clock head once per source instruction.

theorem Turing.MultiTapeMachine.Clock.run_interpret_stop {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} {input : List Bool} [Applicative Choose] [DecidableEq Oracle] {Query : Type u} {spec : Cslib.OracleSpec Query} {OracleState : Type} (machine : MultiTapeMachine k Bool State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hpure : ∀ {α : Type} (a : α) (s : OracleState), (Cslib.OracleComp.interpret oracle (choose (pure a))).run s = PMF.pure (a, s)) (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (s : OracleState) (hstop : tape position ≠ some true) : (Cslib.OracleComp.interpret oracle (machine.withClock.runConfigFrom choose query 1 (config cfg tape position false))).run s = PMF.pure (stopped cfg tape position, s)

At the budget's end, halt without another source instruction or oracle call.

theorem Turing.MultiTapeMachine.run_interpret_runConfigFrom_withClock {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} {input : List Bool} [Applicative Choose] [DecidableEq Oracle] {Query : Type u} {spec : Cslib.OracleSpec Query} {OracleState : Type} (machine : MultiTapeMachine k Bool State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hpure : ∀ {α : Type} (a : α) (s : OracleState), (Cslib.OracleComp.interpret oracle (choose (pure a))).run s = PMF.pure (a, s)) (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (budget : ℕ) (s : OracleState) (hbudget : ∀ i < budget, tape (position + ↑i) = some true) (hstop : tape (position + ↑budget) ≠ some true) : (Cslib.OracleComp.interpret oracle (machine.withClock.runConfigFrom choose query (2 * budget + 1) (Clock.config cfg tape position false))).run s = PMF.map (fun (x : Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (Clock.stopped final tape (position + ↑budget), s')) ((Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query budget cfg)).run s)

A prepared unary budget implements the source's external cutoff with actual halting. All source tapes, channels, and private interpreter state are retained; the source control state is discarded when the controller halts. Constant choices must have no interpreted effect.

theorem Turing.MultiTapeMachine.run_interpret_runConfigFrom_withClock_add {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} {input : List Bool} [Applicative Choose] [DecidableEq Oracle] {Query : Type u} {spec : Cslib.OracleSpec Query} {OracleState : Type} (machine : MultiTapeMachine k Bool State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hpure : ∀ {α : Type} (a : α) (s : OracleState), (Cslib.OracleComp.interpret oracle (choose (pure a))).run s = PMF.pure (a, s)) (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (budget padding : ℕ) (s : OracleState) (hbudget : ∀ i < budget, tape (position + ↑i) = some true) (hstop : tape (position + ↑budget) ≠ some true) : (Cslib.OracleComp.interpret oracle (machine.withClock.runConfigFrom choose query (2 * budget + 1 + padding) (Clock.config cfg tape position false))).run s = PMF.map (fun (x : Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (Clock.stopped final tape (position + ↑budget), s')) ((Cslib.OracleComp.interpret oracle (machine.runConfigFrom choose query budget cfg)).run s)

Extra time after budget exhaustion cannot change the configuration or private state.

theorem Turing.MultiTapeMachine.run_interpret_runFrom_withClock {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} {input : List Bool} [Applicative Choose] [DecidableEq Oracle] {Query : Type u} {spec : Cslib.OracleSpec Query} {OracleState : Type} (machine : MultiTapeMachine k Bool State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hpure : ∀ {α : Type} (a : α) (s : OracleState), (Cslib.OracleComp.interpret oracle (choose (pure a))).run s = PMF.pure (a, s)) (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (budget padding : ℕ) (s : OracleState) (hbudget : ∀ i < budget, tape (position + ↑i) = some true) (hstop : tape (position + ↑budget) ≠ some true) : (Cslib.OracleComp.interpret oracle (machine.withClock.runFrom choose query (2 * budget + 1 + padding) (Clock.config cfg tape position false))).run s = (Cslib.OracleComp.interpret oracle (machine.runFrom choose query budget cfg)).run s

In particular, the output and final private state agree with the original clocked run.

theorem Turing.MultiTapeMachine.withClock_halted {k : ℕ} {State Oracle : Type} {Choose : Type → Type v} {input : List Bool} [Applicative Choose] [DecidableEq Oracle] {Query : Type u} {spec : Cslib.OracleSpec Query} {OracleState : Type} (machine : MultiTapeMachine k Bool State Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hpure : ∀ {α : Type} (a : α) (s : OracleState), (Cslib.OracleComp.interpret oracle (choose (pure a))).run s = PMF.pure (a, s)) (cfg : Config k Bool State Oracle input) (tape : ℤ → Option Bool) (position : ℤ) (budget padding : ℕ) (s : OracleState) (hbudget : ∀ i < budget, tape (position + ↑i) = some true) (hstop : tape (position + ↑budget) ≠ some true) (final : Config (k + 1) Bool (Clock.Control State) Oracle input) (s' : OracleState) (hfinal : (final, s') ∈ ((Cslib.OracleComp.interpret oracle (machine.withClock.runConfigFrom choose query (2 * budget + 1 + padding) (Clock.config cfg tape position false))).run s).support) : final.tapes.state = none

Every supported final configuration is halted when the prepared budget expires.