Uniform strict PPT with external word oracles

IsOraclePPTOn uses one finite-control fair-coin machine and one polynomial clock for all inputs and all shared stateful oracle handlers. The certificate preserves the joint output and final oracle state. Finite operation names are separate from unbounded word requests and replies. The clock charges writing queries, reading replies and writing output, while the oracle's own computation is external. Clock exhaustion may cut off a still-live machine; the certificate does not assert that its control state has already halted.

Typed query encodings are not hidden inside this contract: any translation must separately account for its computation. In particular, an unbounded oracle reply cannot be returned for free. The machine clock bounds every supported output even when the handler returns a longer word.

Oracle.Normalization shows that every certificate also has a clean, intrinsically halting realization with the same joint law, and Oracle.Composition composes certificates.

Main definitions

• Cslib.Probability.WordOracleComp: private randomness and named word requests/replies.
• Cslib.Probability.IsOraclePPTOn: joint stateful realization by a strict polynomial clock.

Main results

• Cslib.Probability.IsOraclePPTOn.length_le: uniform bounds on supported encoded output lengths.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.isOraclePPTOn: deterministic functional programs reuse the existing tidy machine certificate.

References

Adapted from Computability/Probabilistic/Oracle.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the current encodings and ProbOracleComp.

@[reducible, inline]

abbrev Cslib.Probability.WordOracleComp (Operation α : Type) : Type

Private randomness and named external operations on word payloads.

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

One finite machine and polynomial clock preserve the full interaction with every shared stateful oracle. The oracle's computation is external; request construction and reply access are ordinary machine work.

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

A fixed finite-control machine and polynomial clock supply a certificate directly.

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

Finiteness of the operation names is part of the certificate.

theorem Cslib.Probability.IsOraclePPTOn.congr {Operation α β : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : β ↪ List Bool} {program program' : α → WordOracleComp Operation β} (h : IsOraclePPTOn input output program) (heq : ∀ (a : α) (State : Type) (oracle : Operation × List Bool → StateT State PMF (List Bool)) (s : State), (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (program a)).run s = (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (program' a)).run s) : IsOraclePPTOn input output program'

Equality of the complete stateful semantics preserves the same clock. Output marginals alone do not suffice, since later calls may observe the oracle's state.

theorem Cslib.Probability.IsOraclePPTOn.iff_encoded {Operation α β : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → WordOracleComp Operation β} : IsOraclePPTOn input output program ↔ IsOraclePPTOn input Turing.MultiTapeTM.encBits fun (a : α) => ⇑output <$> program a

A program returning its declared encoding has the same strict oracle PPT certificates.

theorem Cslib.Probability.IsOraclePPTOn.length_le {Operation α β : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → WordOracleComp Operation β} (h : IsOraclePPTOn input output program) : ∃ (c : ℕ) (d : ℕ), ∀ (a : α) (State : Type) (oracle : Operation × List Bool → StateT State PMF (List Bool)) (s s' : State) (result : β), (result, s') ∈ ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (program a)).run s).support → (output result).length ≤ c * ((input a).length + 1) ^ d

Every supported encoded output has polynomial length, independently of all oracle replies.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.isOraclePPTOn {Operation α β : Type} [DecidableEq Operation] [Finite Operation] {input : α ↪ List Bool} {output : β ↪ List Bool} {f : α → β} (h : ComputableTidilyInPolyTime f input output) : Cslib.Probability.IsOraclePPTOn input output fun (a : α) => pure (f a)

A tidy deterministic certificate also works in the presence of arbitrary external oracles.