Possible results of randomized oracle programs

A result of a program with private coins is possible when some private samples and some replies to its external queries lead to it: it lies in OracleComp.support program, the results at the leaves of the program's tree of calls. That is the generic support of Complexity/Languages/Probabilistic/Semantics.lean, and the rules of OracleComp.supportWith apply to it. Private samples range over the support of the closed program (support_sample). Every stateful execution returns only possible results (mem_support_of_mem). When every reply type is nonempty, every possible result is returned by some stateful execution (mem_support_iff_exists): an oracle that answers its first call with a chosen reply realizes each path. Invariants of adaptive loops (OracleComp.iterate_invariant) quantify over possible results, so they remain valid for every shared oracle and every reply length.

Main results

• Cslib.ProbOracleComp.supportWith_query: an external query may return any possible reply.
• Cslib.ProbOracleComp.support_sample: private samples range over the closed program's support.
• Cslib.ProbOracleComp.mem_support_of_mem: stateful executions return possible results.
• Cslib.ProbOracleComp.mem_support_iff_exists: with nonempty reply types, the possible results are the results of stateful executions.

References

Generalizes the supported loop invariants of Computability/Probabilistic/Adaptive.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to programs with external calls, for the loop rules adapted from Christian Reitwiessner's Combinators/IterateWhile (crei:crei/tidy-universal @7f7c0696).

theorem Cslib.ProbOracleComp.eq_of_mem_support_pure {Query α : Type} {spec : Query → Type} {a result : α} (h : result ∈ OracleComp.support (pure a)) : result = a

A returned value is the only possible result.

theorem Cslib.ProbOracleComp.mem_support_map {Query α β : Type} {spec : Query → Type} {program : ProbOracleComp spec α} {f : α → β} {result : β} (h : result ∈ (f <$> program).support) : ∃ a ∈ OracleComp.support program, f a = result

A possible mapped result is the image of a possible result.

@[simp]

theorem Cslib.ProbOracleComp.supportWith_query {Query : Type} {spec : Query → Type} (possible : (q : ℕ ⊕ Query) → Set (probOracleSpec spec q)) (q : Query) : OracleComp.supportWith possible (query q) = possible (Sum.inr q)

An external query may return any of its possible replies.

@[simp]

theorem Cslib.ProbOracleComp.support_sample {Query α : Type} {spec : Query → Type} (program : ProbComp α) : OracleComp.support (sample program) = program.eval.support

Private samples range over the support of the closed program.

theorem Cslib.ProbOracleComp.mem_support_of_mem {Query α : Type} {spec : Query → Type} {program : ProbOracleComp spec α} {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) {s s' : State} {result : α} (h : (result, s') ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) program).run s).support) : result ∈ OracleComp.support program

A result supported by one stateful execution is possible.

theorem Cslib.ProbOracleComp.mem_support_iff_exists {Query α : Type} {spec : Query → Type} [hne : ∀ (q : Query), Nonempty (spec q)] {program : ProbOracleComp spec α} {result : α} : result ∈ OracleComp.support program ↔ ∃ (State : Type) (oracle : (q : Query) → StateT State PMF (spec q)) (s : State) (s' : State), (result, s') ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) program).run s).support

When every reply type is nonempty, the possible results of a program are exactly the results of its stateful executions.