Internal clocks for probabilistic machines

The common clock controller preserves the source distribution when coin draws leave private interpreter state unchanged. The law may be biased; fair-coin semantics is a special case. This hypothesis is needed because clock bookkeeping consumes extra discarded coin draws. Query programs may still update arbitrary shared private state.

The budget tape must already be prepared. Its construction and runtime are a separate obligation.

Main definitions

• Turing.MultiTapePTM.withClock: the common clock consumer with Boolean-indexed transitions.

Main results

• Turing.MultiTapePTM.run_interpret_runConfigFrom_withClock_add: a prepared budget reproduces the clocked source's tapes and private state and halts, allowing extra time after exhaustion.

References

The common proof in MultiTape.Machine.Clock adapts the cslib crypto branch's MultiTape/Oracle/Clock.lean at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

@[reducible, inline]

abbrev Turing.MultiTapePTM.withClock {k : ℕ} {State Oracle : Type} (machine : MultiTapePTM k Bool State Oracle) : MultiTapePTM (k + 1) Bool (MultiTapeMachine.Clock.Control State) Oracle

The common unary-budget controller specialized to Boolean-indexed transitions.

theorem Turing.MultiTapePTM.run_interpret_runConfigFrom_withClock_add {k : ℕ} {State Oracle Query OracleState : Type} {spec : Cslib.OracleSpec Query} {input : List Bool} [DecidableEq Oracle] (machine : MultiTapePTM k Bool State Oracle) (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) (cfg : MultiTapeMachine.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 coin query (2 * budget + 1 + padding) (MultiTapeMachine.Clock.config cfg tape position false))).run s = PMF.map (fun (x : MultiTapeMachine.Config k Bool State Oracle input × OracleState) => match x with | (final, s') => (MultiTapeMachine.Clock.stopped final tape (position + ↑budget), s')) ((Cslib.OracleComp.interpret oracle (machine.runConfigFrom coin query budget cfg)).run s)

A prepared budget implements the externally clocked run and then halts. Coin draws must be stateless, whereas the query program may modify arbitrary shared private state.