Clean realizations of arbitrary oracle PPT certificates

A strict IsOraclePPTOn witness may be cut off by its clock while still live, leave partial requests in its query buffers, read stale answer tapes and leave arbitrary storage behind. It is nevertheless equivalent to a clean phase. During fuel instructions from blank storage, a machine reads at most fuel symbols of any reply. The native run is therefore exactly the finite interpreter loop in which every external call returns its fuel-symbol prefix. Each interpreter step is certified by the clean calculus: a fair bit, a fixed table lookup, and at most one bounded-prefix query. The loop makes the same adaptive external calls in the same order, with identical requests, and preserves the complete joint law of the output and external oracle state.

Main results

• Cslib.Probability.IsTidyOraclePPTOn.finiteStep: one truncated interpreter step is clean.
• Cslib.Probability.IsTidyOraclePPTOn.runOracle: every clocked oracle machine run is clean.
• Cslib.Probability.IsOraclePPTOn.isTidyOraclePPTOn, Cslib.Probability.isOraclePPTOn_iff_isTidyOraclePPTOn: every strict oracle PPT certificate has a clean realization with the same joint output and external-state law.

References

Adapts the closed interpreter Computability/Probabilistic/Realization/OracleSimulation.lean of the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to open oracles, using the reply truncation lemma Turing.MultiTapePTM.finiteRunFrom_take_runOracle.

theorem Cslib.Probability.IsTidyOraclePPTOn.finiteStep {k : ℕ} {Control Operation : Type} [DecidableEq Operation] [Fintype Operation] [Finite Control] (machine : Turing.MultiTapePTM k Bool Control Operation) : IsTidyOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encFiniteConfig) Turing.MultiTapeTM.encFiniteConfig fun (pair : ℕ × Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation) => Turing.MultiTapeMachine.finiteStep machine (fun (choices : ReaderT Bool Id (Turing.MultiTapeMachine.Action k Bool Control Operation)) => choices <$> ProbOracleComp.sample (ProbComp.uniform Bool)) (fun (op : Operation) (word : List Bool) => List.take pair.1 <$> ProbOracleComp.query (op, word)) pair.2

One native instruction on finite storage, with each external reply truncated to the first limit symbols, is a clean phase. A query copies only the charged reply prefix.

theorem Cslib.Probability.IsTidyOraclePPTOn.runOracle {k : ℕ} {Control Operation : Type} [DecidableEq Operation] [Finite Operation] [Finite Control] (machine : Turing.MultiTapePTM k Bool Control Operation) (c d : ℕ) : IsTidyOraclePPTOn Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits fun (word : List Bool) => machine.runOracle (c * (word.length + 1) ^ d) word

Every clocked run of a finite-control oracle machine is a clean phase. The interpreter loop retains finite storage, runs exactly as many steps as the clock, and copies each reply only up to the clock, which bounds every reply position the original run can read.

theorem Cslib.Probability.IsOraclePPTOn.isTidyOraclePPTOn {Operation : Type} [DecidableEq Operation] {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → WordOracleComp Operation β} (h : IsOraclePPTOn input output program) : IsTidyOraclePPTOn input output program

Every strict oracle PPT certificate has a clean realization. The realization makes the same adaptive external calls with the same requests in the same order, and has the same joint law of output and external oracle state, for every stateful handler and arbitrarily long replies.

theorem Cslib.Probability.isOraclePPTOn_iff_isTidyOraclePPTOn {Operation : Type} [DecidableEq Operation] {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → WordOracleComp Operation β} : IsOraclePPTOn input output program ↔ IsTidyOraclePPTOn input output program

Strict oracle PPT certificates are exactly the clean polynomial-time realizations.