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: ProbOracleComp.support is the set of results at the leaves of the program's tree of calls. 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 quantify over possible results, so they remain valid for every shared oracle and every reply length.

Main definitions

• Cslib.ProbOracleComp.support: the results at the leaves of the program's tree of calls.

Main results

• Cslib.ProbOracleComp.mem_support_bind_iff: a possible result of a sequence is a possible result of a continuation at a possible intermediate result.
• Cslib.ProbOracleComp.support_sample: private samples range over the closed program's support.
• Cslib.ProbOracleComp.mem_support_iff_exists: with nonempty reply types, the possible results are the results of stateful executions.
• Cslib.ProbOracleComp.iterate_invariant: an invariant preserved by every possible step holds for every possible result of a bounded loop.

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).

def Cslib.ProbOracleComp.support {Query α : Type} {spec : Query → Type} : ProbOracleComp spec α → Set α

The results of program for some private samples and some replies to its external queries: the results at the leaves of its tree of calls.

@[simp]

theorem Cslib.ProbOracleComp.support_pure {Query α : Type} {spec : Query → Type} (a : α) : (pure a).support = {a}

A returned value is the only possible result.

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

A returned value is the only possible result.

@[simp]

theorem Cslib.ProbOracleComp.mem_support_bind_iff {Query α β : Type} {spec : Query → Type} {program : ProbOracleComp spec α} {next : α → ProbOracleComp spec β} {result : β} : result ∈ (program >>= next).support ↔ ∃ a ∈ program.support, result ∈ (next a).support

A possible result of a sequence is a possible result of a continuation at a possible intermediate result.

theorem Cslib.ProbOracleComp.mem_support_bind {Query α β : Type} {spec : Query → Type} {program : ProbOracleComp spec α} {next : α → ProbOracleComp spec β} {result : β} (h : result ∈ (program >>= next).support) : ∃ a ∈ program.support, result ∈ (next a).support

A possible result of a sequence comes from a possible first result.

@[simp]

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

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

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

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

@[simp]

theorem Cslib.ProbOracleComp.support_query {Query : Type} {spec : Query → Type} (q : Query) : (query q).support = Set.univ

An external query may return any reply.

@[simp]

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

Private samples range over the support of the closed program.

theorem Cslib.ProbOracleComp.support_sample_subset {Query α : Type} {spec : Query → Type} (program : ProbComp α) : (sample program).support ⊆ program.eval.support

Private samples can only return results in 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 ∈ program.support

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 ∈ program.support ↔ ∃ (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.

theorem Cslib.ProbOracleComp.iterate_invariant {Query : Type} {spec : Query → Type} {σ : Type} {step : σ → ProbOracleComp spec σ} {count : ℕ} {initial : σ} (invariant : ℕ → σ → Prop) (hbase : invariant 0 initial) (hpreserve : ∀ (i : ℕ) (state : σ), i < count → invariant i state → ∀ next ∈ (step state).support, invariant (i + 1) next) (state : σ) : state ∈ support (OracleComp.iterate count step initial) → invariant count state

An invariant indexed by the number of completed steps holds for every possible result of a bounded loop when every possible step preserves it.