Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Machine.Clock

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.AuxiliaryTape.config: retain source data beside the clock tape.

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) :

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

Instances For

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

Turing.Action (k + 1) Bool (Control State)

Leave all source tapes unchanged.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

@[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.

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

((AuxiliaryTape.config cfg tape position true).step (tick cfg.tapes.state) (fun (x : Oracle) => none) fun (x : Oracle) => 0) = AuxiliaryTape.config cfg tape (position + 1) false

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

((AuxiliaryTape.config cfg tape position false).step (idle (some (true , cfg.tapes.state))) (fun (x : Oracle) => none) fun (x : Oracle) => 0) = AuxiliaryTape.config cfg tape position true

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 (AuxiliaryTape.config cfg tape position true))).run s = PMF.pure (AuxiliaryTape.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 (AuxiliaryTape.config cfg tape position false))).run s = PMF.map (fun (x : Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (AuxiliaryTape.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) (AuxiliaryTape.config cfg tape position false))).run s = PMF.map (fun (x : Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (AuxiliaryTape.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 (AuxiliaryTape.config cfg tape position false))).run s = PMF.pure (AuxiliaryTape.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) (AuxiliaryTape.config cfg tape position false))).run s = PMF.map (fun (x : Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (AuxiliaryTape.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) (AuxiliaryTape.config cfg tape position false))).run s = PMF.map (fun (x : Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (AuxiliaryTape.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) (AuxiliaryTape.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) (AuxiliaryTape.config cfg tape position false))).run s).support) :

final.tapes.state = none

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