Preparing a polynomial clock with the tidy calculus

The budget is an ordinary functional program: compute a fixed polynomial in the input length and write that many true bits. Its efficiency follows from fun_prop; the existing output redirection and rewind compiler puts the result on a work tape. The resulting finite machine starts with blank tapes, halts, restores the input and all heads, leaves its scratch tapes blank, and emits nothing. Its polynomial bound charges both generation and rewinding.

Main definitions

• Turing.MultiTapeTM.PolynomialClock.budget: a unary monomial execution budget.

Main results

• Turing.MultiTapeTM.PolynomialClock.computableTidilyInPolyTime_budget: the functional generator has a uniform polynomial-time TM certificate.
• Turing.MultiTapeTM.PolynomialClock.exists_prepare: a finite machine prepares the budget on its last work tape, within one polynomial bound for every input.

References

This serves the role of MultiTape/Plumbing/PrepareClock.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing Christian Reitwiessner's tidy calculus and the existing output-to-word compiler instead of a separate polynomial generator.

def Turing.MultiTapeTM.PolynomialClock.budget (coefficient degree : ℕ) (input : List Bool) : List Bool

Unary execution budget, with coefficient and degree fixed independently of the input.

theorem Turing.MultiTapeTM.PolynomialClock.computableTidilyInPolyTime_budget (coefficient degree : ℕ) : ComputableTidilyInPolyTime (budget coefficient degree) encBits encBits

Generate the budget using the existing functional polynomial-time calculus.

theorem Turing.MultiTapeTM.PolynomialClock.exists_prepare (coefficient degree : ℕ) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeTM (k + 1) Bool State) (c : ℕ) (d : ℕ), ∀ (input : List Bool), runFrom (machine.initCfg input) (c * (input.length + 1) ^ d) = wordsCfg input none (Function.update (fun (x : Fin (k + 1)) => []) (Fin.last k) (budget coefficient degree input)) []

Prepare and rewind a budget from blank tapes, restoring every scratch tape and emitting nothing. The finite machine and its polynomial bound are uniform over all input words.