Polynomial external query budgets

An oracle PPT certificate implies polynomial bounds on the number and encoded length of external requests, as structural budgets of the program (ProbOracleComp.IsQueryBounded, ProbOracleComp.QueriesSatisfy). The derivation instruments the shared oracle state with a transcript and uses the certificate's equality of the full final-state distribution; the budgets then follow because they are exactly the bounds that every logged execution respects. It does not assume a separate query bound or restrict oracle reply sizes. Private randomness is independent and is not logged.

Main results

• Cslib.Probability.IsOraclePPTOn.query_bounds: one polynomial bounds calls and request lengths uniformly over all inputs and shared stateful oracles.

References

Adapted from Computability/Probabilistic/QueryBounds.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the current word-oracle realization contract.

theorem Cslib.Probability.IsOraclePPTOn.query_bounds {Operation α β : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → WordOracleComp Operation β} (h : IsOraclePPTOn input output program) : ∃ (c : ℕ) (d : ℕ), ∀ (a : α), ProbOracleComp.IsQueryBounded (program a) (c * ((input a).length + 1) ^ d) ∧ ProbOracleComp.QueriesSatisfy (fun (request : Operation × List Bool) => request.2.length ≤ c * ((input a).length + 1) ^ d) (program a)

Instrumenting the private state transfers the machine clock's query bounds to the program. The same machine polynomial bounds the number of external queries and the length of each request. The certificate is an equality of executions, so the bounds pass through every logged execution.