Compiling polynomial clocks

A deterministic preparation program writes a unary budget on the last work tape. The common tape embedding and sequential compiler then run the common clock consumer. Preparation scratch tapes and source tapes are disjoint; all tapes start blank. Every preparation and controller instruction is charged to the compiled machine's polynomial bound.

Main definitions

• Turing.MultiTapePTM.PolynomialClock.compile: prepare a budget and consume it.

Main results

• Turing.MultiTapePTM.PolynomialClock.run_interpret_compile: retain the joint configuration and private interpreter state, apart from the source's discarded control state.
• Turing.MultiTapePTM.exists_polynomialClock: a finite-control machine implements the cutoff and halts within a uniform polynomial, against any query interpreter and stateless coin law.

References

Adapts the role of MultiTape/Oracle/PolynomialClock.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using functional budget generation and the shared machine compilers.

noncomputable def Turing.MultiTapePTM.PolynomialClock.compile {k r : ℕ} {State PrepareState Oracle : Type} (machine : MultiTapePTM k Bool State Oracle) (prepare : MultiTapeTM (r + 1) Bool PrepareState) : MultiTapePTM (k + r + 1) Bool (PrepareState ⊕ MultiTapeMachine.Clock.Control State) Oracle

Reserve disjoint source and preparation tapes, then run the budget controller.

theorem Turing.MultiTapePTM.PolynomialClock.embed_budget {k r : ℕ} {PrepareState : Type} (input word : List Bool) (state : Option PrepareState) : (MultiTapeTM.embed (Fin.natAddEmb k) (wordsCfg input state (Function.update (fun (x : Fin (r + 1)) => []) (Fin.last r) word) []) (fun (x : Fin (k + (r + 1))) (x_1 : ℤ) => none) fun (x : Fin (k + (r + 1))) => 0) = wordsCfg input state (Function.update (fun (x : Fin (k + r + 1)) => []) (Fin.last (k + r)) word) []

A prepared word stays on the last tape when disjoint source tapes are added in front.

def Turing.MultiTapePTM.PolynomialClock.ready {k r : ℕ} {PrepareState Oracle : Type} (input word : List Bool) : MultiTapeMachine.Config (k + r + 1) Bool PrepareState Oracle input

The preparation phase has halted, with only its last work tape nonempty.

theorem Turing.MultiTapePTM.PolynomialClock.start_ready {k r : ℕ} {State PrepareState Oracle : Type} (machine : MultiTapePTM k Bool State Oracle) (input word : List Bool) : MultiTapeMachine.Sequential.start (machine.extendTapes (Fin.castAddEmb r)).withClock (ready input word) = MultiTapeMachine.Clock.config (MultiTapeMachine.initialConfig (machine.extendTapes (Fin.castAddEmb r)) input) (tapeOfList word) 0 false

Handoff supplies precisely the initial source configuration and its prepared budget.

theorem Turing.MultiTapePTM.PolynomialClock.prepare_runFrom {k r : ℕ} {PrepareState : Type} (prepare : MultiTapeTM (r + 1) Bool PrepareState) (input word : List Bool) (time : ℕ) (hprepare : MultiTapeTM.runFrom (prepare.initCfg input) time = wordsCfg input none (Function.update (fun (x : Fin (r + 1)) => []) (Fin.last r) word) []) : MultiTapeTM.runFrom ((prepare.extendTapes (Fin.natAddEmb k)).initCfg input) time = wordsCfg input none (Function.update (fun (x : Fin (k + r + 1)) => []) (Fin.last (k + r)) word) []

The embedded deterministic preparation reaches the exact ready configuration.

def Turing.MultiTapePTM.PolynomialClock.finish {k r : ℕ} {State PrepareState Oracle : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Oracle input) (budget : ℕ) : MultiTapeMachine.Config (k + r + 1) Bool (PrepareState ⊕ MultiTapeMachine.Clock.Control State) Oracle input

The source data after exhaustion, embedded alongside the consumed budget and halted control.

theorem Turing.MultiTapePTM.PolynomialClock.run_interpret_compile {k r : ℕ} {State PrepareState Oracle Query OracleState : Type} {spec : Cslib.OracleSpec Query} [DecidableEq Oracle] (machine : MultiTapePTM k Bool State Oracle) (prepare : MultiTapeTM (r + 1) Bool PrepareState) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (coinLaw : PMF Bool) (hcoin : ∀ (s : OracleState), (Cslib.OracleComp.interpret oracle coin).run s = PMF.map (fun (bit : Bool) => (bit, s)) coinLaw) (input : List Bool) (budget time padding : ℕ) (s : OracleState) (hprepare : MultiTapeTM.runFrom (prepare.initCfg input) time = wordsCfg input none (Function.update (fun (x : Fin (r + 1)) => []) (Fin.last r) (List.replicate budget true)) []) : (Cslib.OracleComp.interpret oracle ((compile machine prepare).runConfigFrom coin query (time + (2 * budget + 1 + padding)) (MultiTapeMachine.initialConfig (compile machine prepare) input))).run s = PMF.map (fun (x : MultiTapeMachine.Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (finish final budget, s')) ((Cslib.OracleComp.interpret oracle (machine.runConfigFrom coin query budget (MultiTapeMachine.initialConfig machine input))).run s)

Preparing and consuming a budget preserves the entire source data and private interpreter state. Both preparation time and every controller instruction are included in the bound.

theorem Turing.MultiTapePTM.exists_polynomialClock {k : ℕ} {State Oracle : Type} [Finite State] [DecidableEq Oracle] (machine : MultiTapePTM k Bool State Oracle) (coefficient degree : ℕ) : ∃ (k' : ℕ) (State' : Type) (_ : Finite State') (target : MultiTapePTM k' Bool State' Oracle) (c : ℕ) (d : ℕ), ∀ (input : List Bool) (Query OracleState : Type) (spec : Cslib.OracleSpec Query) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Bool → Cslib.OracleComp spec (List Bool)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (coinLaw : PMF Bool), (∀ (s : OracleState), (Cslib.OracleComp.interpret oracle coin).run s = PMF.map (fun (bit : Bool) => (bit, s)) coinLaw) → ∀ (s : OracleState), (Cslib.OracleComp.interpret oracle (target.run coin query (c * (input.length + 1) ^ d) input)).run s = (Cslib.OracleComp.interpret oracle (machine.run coin query (coefficient * (input.length + 1) ^ degree) input)).run s ∧ ∀ result ∈ ((Cslib.OracleComp.interpret oracle (target.runConfigFrom coin query (c * (input.length + 1) ^ d) (MultiTapeMachine.initialConfig target input))).run s).support, result.1.tapes.state = none

A finite-control machine implements a polynomial cutoff uniformly and actually halts. Its polynomial charges budget generation, rewinding, and clock consumption. Oracle calls keep their abstract instruction cost; no efficiency of an arbitrary supplied query program is asserted.