Query budgets of randomized programs

A program with private coins, ProbOracleComp spec α, makes two kinds of calls: private samples (Sum.inl) and external queries (Sum.inr). Its query budgets are the budgets OracleComp.IsCostBounded of a cost that is 0 on every sample:

• ProbOracleComp.IsQueryBounded program n: at most n external queries on every path, whatever the samples and the replies;
• ProbOracleComp.QueriesSatisfy p program: every external query satisfies p, for example a bound on its length.

All rules of OracleComp.IsCostBounded apply. A program over the external interface alone, with its calls made external queries, keeps its budget (isCostBounded_interpret_query).

Meaning. Against every stateful oracle, the external queries recorded on a supported run respect the budget (transcript_cost_le). Conversely, when every reply type is nonempty, a program whose recorded queries respect the budget against every stateful oracle satisfies it (isCostBounded_iff_transcript_cost_le): an oracle that answers its first call with a chosen reply realizes each path. This is how a certificate stated through executions, such as an oracle machine's, yields a structural budget. Without nonempty reply types the converse fails: if some reply type is empty, no oracle exists, and the condition on executions holds vacuously.

Main definitions

• Cslib.ProbOracleComp.IsQueryBounded: at most n external queries on every path.
• Cslib.ProbOracleComp.QueriesSatisfy: every external query on every path satisfies p.

Main results

• Cslib.ProbOracleComp.isCostBounded_sample: private samples cost nothing.
• Cslib.ProbOracleComp.isCostBounded_interpret_query: budgets of programs without private coins.
• Cslib.ProbOracleComp.isCostBounded_iff_transcript_cost_le: the structural budget is the budget of every logged execution.

@[reducible, inline]

abbrev Cslib.ProbOracleComp.IsQueryBounded {Query α : Type} {spec : Query → Type} (program : ProbOracleComp spec α) (n : ℕ) : Prop

The program makes at most n external queries on every path, whatever its private samples and the replies. Private samples are free.

@[reducible, inline]

abbrev Cslib.ProbOracleComp.QueriesSatisfy {Query α : Type} {spec : Query → Type} (p : Query → Prop) (program : ProbOracleComp spec α) : Prop

Every external query of the program, on every path, satisfies p. Private samples are unconstrained.

theorem Cslib.ProbOracleComp.isCostBounded_sample {Query α : Type} {spec : Query → Type} (cost : Query → ℕ) (program : ProbComp α) : OracleComp.IsCostBounded (Sum.elim (fun (x : ℕ) => 0) cost) (sample program) 0

A closed sampler makes no external query.

theorem Cslib.ProbOracleComp.isCostBounded_query {Query : Type} {spec : Query → Type} (cost : Query → ℕ) (q : Query) : OracleComp.IsCostBounded (Sum.elim (fun (x : ℕ) => 0) cost) (query q) (cost q)

A single external query costs its cost.

theorem Cslib.ProbOracleComp.isCostBounded_interpret_query {Query α : Type} {spec : Query → Type} {cost : Query → ℕ} {program : OracleComp spec α} {n : ℕ} (h : OracleComp.IsCostBounded cost program n) : OracleComp.IsCostBounded (Sum.elim (fun (x : ℕ) => 0) cost) (OracleComp.interpret (fun (q : Query) => query q) program) n

A program over the external interface alone keeps its budget when its calls become external queries of a program with private coins.

theorem Cslib.ProbOracleComp.IsQueryBounded.sample {Query α : Type} {spec : Query → Type} (program : ProbComp α) : (ProbOracleComp.sample program).IsQueryBounded 0

A closed sampler makes no external query.

theorem Cslib.ProbOracleComp.IsQueryBounded.query {Query : Type} {spec : Query → Type} (q : Query) : (ProbOracleComp.query q).IsQueryBounded 1

A single external query is one query.

theorem Cslib.OracleComp.IsQueryBounded.probOracleComp {Query α : Type} {spec : Query → Type} {program : OracleComp spec α} {n : ℕ} (h : program.IsQueryBounded n) : (interpret (fun (q : Query) => ProbOracleComp.query q) program).IsQueryBounded n

A program without private coins makes as many external queries as it makes calls.

theorem Cslib.ProbOracleComp.QueriesSatisfy.sample {Query α : Type} {spec : Query → Type} {p : Query → Prop} (program : ProbComp α) : QueriesSatisfy p (ProbOracleComp.sample program)

A closed sampler makes no external query.

theorem Cslib.ProbOracleComp.QueriesSatisfy.query {Query : Type} {spec : Query → Type} {p : Query → Prop} {q : Query} (hq : p q) : QueriesSatisfy p (ProbOracleComp.query q)

A single external query satisfies p when its request does.

theorem Cslib.ProbOracleComp.QueriesSatisfy.mono {Query α : Type} {spec : Query → Type} {p p' : Query → Prop} {program : ProbOracleComp spec α} (h : QueriesSatisfy p program) (hp : ∀ (q : Query), p q → p' q) : QueriesSatisfy p' program

A weaker predicate on external queries is still satisfied.

theorem Cslib.ProbOracleComp.QueriesSatisfy.of_forall {Query α : Type} {spec : Query → Type} {p : Query → Prop} (hp : ∀ (q : Query), p q) (program : ProbOracleComp spec α) : QueriesSatisfy p program

Every program satisfies a predicate that holds for every external query.

Logged executions

theorem Cslib.ProbOracleComp.transcript_cost_le {Query α : Type} {spec : Query → Type} {cost : Query → ℕ} {program : ProbOracleComp spec α} {n : ℕ} (h : OracleComp.IsCostBounded (Sum.elim (fun (x : ℕ) => 0) cost) program n) {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) {s s' : State} {result : α} {transcript : OracleComp.Transcript spec} (hmem : (result, s', transcript) ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (OracleComp.withTranscript oracle)) program).run (s, [])).support) : (List.map (fun (entry : (q : Query) × spec q) => cost entry.fst) transcript).sum ≤ n

Against every stateful oracle, the external queries recorded on a supported run cost at most the budget. Private samples are not recorded.

theorem Cslib.ProbOracleComp.isCostBounded_of_transcript_cost_le {Query α : Type} {spec : Query → Type} [hne : ∀ (q : Query), Nonempty (spec q)] {cost : Query → ℕ} {program : ProbOracleComp spec α} {n : ℕ} (h : ∀ (State : Type) (oracle : (q : Query) → StateT State PMF (spec q)) (s s' : State) (result : α) (transcript : OracleComp.Transcript spec), (result, s', transcript) ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (OracleComp.withTranscript oracle)) program).run (s, [])).support → (List.map (fun (entry : (q : Query) × spec q) => cost entry.fst) transcript).sum ≤ n) : OracleComp.IsCostBounded (Sum.elim (fun (x : ℕ) => 0) cost) program n

If, against every stateful oracle, the external queries recorded on every supported run cost at most n, and every reply type is nonempty, then the program's external queries cost at most n on every path.

theorem Cslib.ProbOracleComp.isCostBounded_iff_transcript_cost_le {Query α : Type} {spec : Query → Type} [∀ (q : Query), Nonempty (spec q)] {cost : Query → ℕ} {program : ProbOracleComp spec α} {n : ℕ} : OracleComp.IsCostBounded (Sum.elim (fun (x : ℕ) => 0) cost) program n ↔ ∀ (State : Type) (oracle : (q : Query) → StateT State PMF (spec q)) (s s' : State) (result : α) (transcript : OracleComp.Transcript spec), (result, s', transcript) ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (OracleComp.withTranscript oracle)) program).run (s, [])).support → (List.map (fun (entry : (q : Query) × spec q) => cost entry.fst) transcript).sum ≤ n

When every reply type is nonempty, a program's external queries cost at most n on every path exactly when, against every stateful oracle, those recorded on every supported run do.

theorem Cslib.ProbOracleComp.IsQueryBounded.length_transcript_le {Query α : Type} {spec : Query → Type} {program : ProbOracleComp spec α} {n : ℕ} (h : program.IsQueryBounded n) {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) {s s' : State} {result : α} {transcript : OracleComp.Transcript spec} (hmem : (result, s', transcript) ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (OracleComp.withTranscript oracle)) program).run (s, [])).support) : List.length transcript ≤ n

Against every stateful oracle, a supported run records at most n external queries.

theorem Cslib.ProbOracleComp.QueriesSatisfy.forall_mem_transcript {Query α : Type} {spec : Query → Type} {p : Query → Prop} {program : ProbOracleComp spec α} (h : QueriesSatisfy p program) {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) {s s' : State} {result : α} {transcript : OracleComp.Transcript spec} (hmem : (result, s', transcript) ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (OracleComp.withTranscript oracle)) program).run (s, [])).support) (entry : (q : Query) × spec q) : entry ∈ transcript → p entry.fst

Against every stateful oracle, every external query recorded on a supported run satisfies p.

theorem Cslib.ProbOracleComp.isQueryBounded_of_length_transcript_le {Query α : Type} {spec : Query → Type} [∀ (q : Query), Nonempty (spec q)] {program : ProbOracleComp spec α} {n : ℕ} (h : ∀ (State : Type) (oracle : (q : Query) → StateT State PMF (spec q)) (s s' : State) (result : α) (transcript : OracleComp.Transcript spec), (result, s', transcript) ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (OracleComp.withTranscript oracle)) program).run (s, [])).support → List.length transcript ≤ n) : program.IsQueryBounded n

When every reply type is nonempty and, against every stateful oracle, every supported run records at most n external queries, the program makes at most n external queries.

theorem Cslib.ProbOracleComp.queriesSatisfy_of_forall_mem_transcript {Query α : Type} {spec : Query → Type} [∀ (q : Query), Nonempty (spec q)] {p : Query → Prop} {program : ProbOracleComp spec α} (h : ∀ (State : Type) (oracle : (q : Query) → StateT State PMF (spec q)) (s s' : State) (result : α) (transcript : OracleComp.Transcript spec), (result, s', transcript) ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (OracleComp.withTranscript oracle)) program).run (s, [])).support → ∀ entry ∈ transcript, p entry.fst) : QueriesSatisfy p program

When every reply type is nonempty and, against every stateful oracle, every external query recorded on a supported run satisfies p, every external query of the program satisfies p.