Semantics of oracle programs

A program program : OracleComp spec α is a tree of oracle calls. It has a meaning once its calls are answered, and this module gives that meaning once, for every interface spec, relative to the answers:

• OracleComp.evalWith h program is the output distribution when each call q is answered by an independent sample of h q : PMF (spec q). It is OracleComp.interpret into PMF.
• OracleComp.supportWith possible program is the set of results reached when each call q may be answered by any element of possible q. It is defined by recursion on the tree of calls, so it needs no distribution on the replies. With every reply possible it is OracleComp.support, the results at the leaves of the tree.
• OracleComp.runWith oracle program s is the joint law of the result and the final state when each call is answered by a stateful probabilistic oracle oracle : (q : ι) → StateT σ PMF (spec q) from the state s. It is OracleComp.interpret into StateT σ PMF.

The three agree: the support of evalWith h program is supportWith of the supports of h (support_evalWith), a result of a stateful run is reached along replies the oracle can give (mem_supportWith_of_mem_support_runWith), and a memoryless oracle run with state is evalWith with the state unchanged (runWith_lift). On the sum spec₁ ⊕ₒ spec₂, a handler is a sumHandler, and an embedded program sees only its own side (evalWith_sumHandler_liftLeft, supportWith_sumHandler_liftLeft, runWith_sumHandler_liftLeft).

The library's semantics are instances. ProbComp.eval is evalWith ProbComp.unifOracle (ProbComp.eval_eq_evalWith), and since every uniform reply has positive probability, the possible results of a closed program are its results for any replies (ProbComp.support_eval). A program with private coins and external calls, ProbOracleComp spec, is a program over unifSpec ⊕ₒ spec: its run against a stateful oracle is runWith of the sum of the lifted uniform handler and that oracle (ProbOracleComp.runWith), and its possible results are support.

Algorithms are programs

Probabilistic algorithms, such as key generation, signing, provers, verifiers, simulators, extractors and samplers, are ProbComp or OracleComp programs. PMF is reserved for their semantics, evalWith and its instances, and for genuinely semantic objects such as ideal distributions and the laws compared in a statistical argument. A program can be run against different oracles, budgeted (OracleComp.IsCostBounded), realized by a machine, and substituted into a reduction, while a bare PMF can do none of these. Exact theorems stay exact, as statements about evalWith.

Main definitions

• Cslib.OracleComp.evalWith: the output distribution for independent answers.
• Cslib.OracleComp.supportWith: the results for answers in given sets.
• Cslib.OracleComp.support: the results for any answers.
• Cslib.OracleComp.runWith: the joint law of the result and final state of a stateful oracle.

Main results

• Cslib.OracleComp.evalWith_bind, .mem_supportWith_bind_iff, .runWith_bind, .bind_congr_on_support, and the pure, map and query rules: the structural rules of each semantics.
• Cslib.OracleComp.isMonadHom_evalWith: evalWith h is a monad morphism.
• Cslib.OracleComp.evalWith_interpret, .supportWith_interpret: replacing calls by programs composes with the semantics.
• Cslib.OracleComp.support_evalWith: evaluation and support agree.
• Cslib.OracleComp.mem_supportWith_of_mem_support_runWith: stateful runs reach possible results.
• Cslib.OracleComp.runWith_lift: memoryless oracles leave the state unchanged.
• Cslib.OracleComp.support_liftLeft, .support_liftRight: embedding into a sum keeps the possible results.
• Cslib.ProbComp.eval_eq_evalWith, Cslib.ProbComp.support_eval, Cslib.ProbComp.support_nonempty, Cslib.ProbComp.mem_support_unifFin: closed probabilistic programs are the instance with uniform answers.
• Cslib.ProbComp.isMonadHom_eval, Cslib.ProbComp.eval_interpret: the instances of isMonadHom_evalWith and evalWith_interpret.

References

The design follows Devon Tuma, Quang Dao, and collaborators' VCVio, whose programs carry their distribution and possible outputs relative to an interpretation of the oracle calls.

Distributions for independent answers

noncomputable def Cslib.OracleComp.evalWith {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (program : OracleComp spec α) : PMF α

The output distribution of program when each call q is answered by an independent sample of h q.

@[simp]

theorem Cslib.OracleComp.evalWith_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (a : α) : evalWith h (pure a) = PMF.pure a

A returned value has a point distribution.

@[simp]

theorem Cslib.OracleComp.evalWith_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (h : (q : ι) → PMF (spec q)) (program : OracleComp spec α) (next : α → OracleComp spec β) : evalWith h (program >>= next) = (evalWith h program).bind fun (a : α) => evalWith h (next a)

Evaluating a sequence draws a result of the first program and evaluates the continuation at it.

@[simp]

theorem Cslib.OracleComp.evalWith_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (h : (q : ι) → PMF (spec q)) (f : α → β) (program : OracleComp spec α) : evalWith h (f <$> program) = PMF.map f (evalWith h program)

Postprocessing maps the distribution.

@[simp]

theorem Cslib.OracleComp.evalWith_query {ι : Type u} {spec : OracleSpec ι} (h : (q : ι) → PMF (spec q)) (q : ι) : evalWith h (query q) = h q

A single call has the distribution of its answer.

theorem Cslib.OracleComp.isMonadHom_evalWith {ι : Type u} {spec : OracleSpec ι} (h : (q : ι) → PMF (spec q)) : IsMonadHom (OracleComp spec) PMF fun {α : Type v} => evalWith h

Evaluation is a monad morphism into PMF.

theorem Cslib.OracleComp.evalWith_interpret {ι : Type u} {spec : OracleSpec ι} {α : Type v} {κ : Type u} {target : OracleSpec κ} (handler : (q : ι) → OracleComp target (spec q)) (h : (q : κ) → PMF (target q)) (program : OracleComp spec α) : evalWith h (interpret handler program) = evalWith (fun (q : ι) => evalWith h (handler q)) program

Evaluating a program whose calls were replaced by programs over another interface evaluates the original calls by the distributions of their replacements.

Possible results

def Cslib.OracleComp.supportWith {ι : Type u} {spec : OracleSpec ι} {α : Type v} (possible : (q : ι) → Set (spec q)) : OracleComp spec α → Set α

The results of program when each call q may be answered by any element of possible q: the results at the leaves of its tree of calls reached along such answers.

@[simp]

theorem Cslib.OracleComp.supportWith_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (possible : (q : ι) → Set (spec q)) (a : α) : supportWith possible (pure a) = {a}

A returned value is the only possible result.

@[simp]

theorem Cslib.OracleComp.mem_supportWith_bind_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {possible : (q : ι) → Set (spec q)} {program : OracleComp spec α} {next : α → OracleComp spec β} {b : β} : b ∈ supportWith possible (program >>= next) ↔ ∃ a ∈ supportWith possible program, b ∈ supportWith possible (next a)

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

theorem Cslib.OracleComp.supportWith_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (possible : (q : ι) → Set (spec q)) (program : OracleComp spec α) (next : α → OracleComp spec β) : supportWith possible (program >>= next) = ⋃ a ∈ supportWith possible program, supportWith possible (next a)

The possible results of a sequence, as a union over the possible first results.

@[simp]

theorem Cslib.OracleComp.mem_supportWith_map_iff {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {possible : (q : ι) → Set (spec q)} {f : α → β} {program : OracleComp spec α} {b : β} : b ∈ supportWith possible (f <$> program) ↔ ∃ a ∈ supportWith possible program, f a = b

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

theorem Cslib.OracleComp.supportWith_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (possible : (q : ι) → Set (spec q)) (f : α → β) (program : OracleComp spec α) : supportWith possible (f <$> program) = f '' supportWith possible program

The possible results of a mapped program are the image of its possible results.

@[simp]

theorem Cslib.OracleComp.supportWith_query {ι : Type u} {spec : OracleSpec ι} (possible : (q : ι) → Set (spec q)) (q : ι) : supportWith possible (query q) = possible q

A single call may return any of its possible answers.

theorem Cslib.OracleComp.supportWith_mono {ι : Type u} {spec : OracleSpec ι} {α : Type v} {possible possible' : (q : ι) → Set (spec q)} (hpossible : ∀ (q : ι), possible q ⊆ possible' q) (program : OracleComp spec α) : supportWith possible program ⊆ supportWith possible' program

Allowing more answers allows more results.

theorem Cslib.OracleComp.supportWith_interpret {ι : Type u} {spec : OracleSpec ι} {α : Type v} {κ : Type u} {target : OracleSpec κ} (handler : (q : ι) → OracleComp target (spec q)) (possible : (q : κ) → Set (target q)) (program : OracleComp spec α) : supportWith possible (interpret handler program) = supportWith (fun (q : ι) => supportWith possible (handler q)) program

Replacing calls by programs over another interface: the possible results are those of the original program, with each call answered by a possible result of its replacement.

theorem Cslib.OracleComp.eq_of_mem_supportWith_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {possible : (q : ι) → Set (spec q)} {a b : α} (h : b ∈ supportWith possible (pure a)) : b = a

A returned value is the only possible result.

@[reducible, inline]

abbrev Cslib.OracleComp.support {ι : Type u} {spec : OracleSpec ι} {α : Type v} (program : OracleComp spec α) : Set α

The results of program for any replies to its calls: the results at the leaves of its tree of calls. It is supportWith with every reply possible, and the rules of supportWith apply.

theorem Cslib.OracleComp.bind_congr_on_support {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {program : OracleComp spec α} {f g : α → OracleComp spec β} (h : ∀ a ∈ program.support, f a = g a) : program >>= f = program >>= g

Two continuations that agree on every possible output of program have identical >>= in OracleComp.

Evaluation and support

theorem Cslib.OracleComp.support_evalWith {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (program : OracleComp spec α) : (evalWith h program).support = supportWith (fun (q : ι) => (h q).support) program

The results with positive probability are the results reached along answers with positive probability.

Stateful oracles

noncomputable def Cslib.OracleComp.runWith {ι : Type u} {spec : OracleSpec ι} {α σ : Type v} (oracle : (q : ι) → StateT σ PMF (spec q)) (program : OracleComp spec α) (s : σ) : PMF (α × σ)

The joint law of the result of program and the final state of the stateful oracle answering its calls, starting from the state s.

@[simp]

theorem Cslib.OracleComp.runWith_pure {ι : Type u} {spec : OracleSpec ι} {α σ : Type v} (oracle : (q : ι) → StateT σ PMF (spec q)) (a : α) (s : σ) : runWith oracle (pure a) s = PMF.pure (a, s)

A returned value leaves the state unchanged.

@[simp]

theorem Cslib.OracleComp.runWith_bind {ι : Type u} {spec : OracleSpec ι} {α β σ : Type v} (oracle : (q : ι) → StateT σ PMF (spec q)) (program : OracleComp spec α) (next : α → OracleComp spec β) (s : σ) : runWith oracle (program >>= next) s = (runWith oracle program s).bind fun (x : α × σ) => runWith oracle (next x.1) x.2

Running a sequence runs the first program, then the continuation at its result from the state it reached.

@[simp]

theorem Cslib.OracleComp.runWith_map {ι : Type u} {spec : OracleSpec ι} {α β σ : Type v} (oracle : (q : ι) → StateT σ PMF (spec q)) (f : α → β) (program : OracleComp spec α) (s : σ) : runWith oracle (f <$> program) s = PMF.map (Prod.map f id) (runWith oracle program s)

Postprocessing maps the result and keeps the final state.

@[simp]

theorem Cslib.OracleComp.runWith_query {ι : Type u} {spec : OracleSpec ι} {σ : Type v} (oracle : (q : ι) → StateT σ PMF (spec q)) (q : ι) (s : σ) : runWith oracle (query q) s = oracle q s

A single call is answered by the oracle from the current state.

theorem Cslib.OracleComp.mem_supportWith_of_mem_support_runWith {ι : Type u} {spec : OracleSpec ι} {α σ : Type v} (oracle : (q : ι) → StateT σ PMF (spec q)) {possible : (q : ι) → Set (spec q)} (hpossible : ∀ (q : ι) (s : σ) (a : spec q) (s' : σ), (a, s') ∈ (oracle q s).support → a ∈ possible q) {program : OracleComp spec α} {s s' : σ} {a : α} (h : (a, s') ∈ (runWith oracle program s).support) : a ∈ supportWith possible program

Every result of a stateful run is reached along replies the oracle can give: if each reply of the oracle to q, from any state, lies in possible q, every result is in supportWith possible.

@[simp]

theorem Cslib.OracleComp.runWith_lift {ι : Type u} {spec : OracleSpec ι} {α σ : Type v} (h : (q : ι) → PMF (spec q)) (program : OracleComp spec α) (s : σ) : runWith (fun (q : ι) => StateT.lift (h q)) program s = PMF.map (fun (x : α) => (x, s)) (evalWith h program)

A memoryless oracle run with state leaves the state unchanged, and the result has the law of evalWith.

Sums of interfaces

@[simp]

theorem Cslib.OracleComp.evalWith_sumHandler_liftLeft {α : Type v} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (left : (q : ι₁) → PMF (spec₁ q)) (right : (q : ι₂) → PMF (spec₂ q)) (program : OracleComp spec₁ α) : evalWith (sumHandler left right) program.liftLeft = evalWith left program

An embedded left program is evaluated by the left handler alone.

@[simp]

theorem Cslib.OracleComp.evalWith_sumHandler_liftRight {α : Type v} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (left : (q : ι₁) → PMF (spec₁ q)) (right : (q : ι₂) → PMF (spec₂ q)) (program : OracleComp spec₂ α) : evalWith (sumHandler left right) program.liftRight = evalWith right program

An embedded right program is evaluated by the right handler alone.

theorem Cslib.OracleComp.evalWith_sumHandler {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {κ : Type u} {target : OracleSpec κ} (h : (q : κ) → PMF (target q)) (left : (q : ι₁) → OracleComp target (spec₁ q)) (right : (q : ι₂) → OracleComp target (spec₂ q)) : (fun (q : ι₁ ⊕ ι₂) => evalWith h (sumHandler left right q)) = sumHandler (fun (q : ι₁) => evalWith h (left q)) fun (q : ι₂) => evalWith h (right q)

Evaluation distributes over the two sides of a handler by programs.

theorem Cslib.OracleComp.support_sumHandler {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (left : (q : ι₁) → PMF (spec₁ q)) (right : (q : ι₂) → PMF (spec₂ q)) : (fun (q : ι₁ ⊕ ι₂) => (sumHandler left right q).support) = sumHandler (fun (q : ι₁) => (left q).support) fun (q : ι₂) => (right q).support

The supports of the answers of a sum handler are the sum of the supports.

@[simp]

theorem Cslib.OracleComp.supportWith_sumHandler_liftLeft {α : Type v} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (left : (q : ι₁) → Set (spec₁ q)) (right : (q : ι₂) → Set (spec₂ q)) (program : OracleComp spec₁ α) : supportWith (sumHandler left right) program.liftLeft = supportWith left program

An embedded left program has the possible results allowed by the left answers alone.

@[simp]

theorem Cslib.OracleComp.supportWith_sumHandler_liftRight {α : Type v} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (left : (q : ι₁) → Set (spec₁ q)) (right : (q : ι₂) → Set (spec₂ q)) (program : OracleComp spec₂ α) : supportWith (sumHandler left right) program.liftRight = supportWith right program

An embedded right program has the possible results allowed by the right answers alone.

@[simp]

theorem Cslib.OracleComp.support_liftLeft {α : Type v} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (program : OracleComp spec₁ α) : program.liftLeft.support = program.support

An embedded left program has the same possible results for any replies.

@[simp]

theorem Cslib.OracleComp.support_liftRight {α : Type v} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (program : OracleComp spec₂ α) : program.liftRight.support = program.support

An embedded right program has the same possible results for any replies.

@[simp]

theorem Cslib.OracleComp.runWith_sumHandler_liftLeft {α : Type v} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {σ : Type v} (left : (q : ι₁) → StateT σ PMF (spec₁ q)) (right : (q : ι₂) → StateT σ PMF (spec₂ q)) (program : OracleComp spec₁ α) (s : σ) : runWith (sumHandler left right) program.liftLeft s = runWith left program s

An embedded left program is run by the left oracle alone, which keeps the whole state.

@[simp]

theorem Cslib.OracleComp.runWith_sumHandler_liftRight {α : Type v} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {σ : Type v} (left : (q : ι₁) → StateT σ PMF (spec₁ q)) (right : (q : ι₂) → StateT σ PMF (spec₂ q)) (program : OracleComp spec₂ α) (s : σ) : runWith (sumHandler left right) program.liftRight s = runWith right program s

An embedded right program is run by the right oracle alone, which keeps the whole state.

theorem Cslib.ProbComp.eval_eq_evalWith {α : Type} (program : ProbComp α) : program.eval = OracleComp.evalWith unifOracle program

Evaluating a closed probabilistic program is evalWith of the uniform handler.

theorem Cslib.ProbComp.support_eval {α : Type} (program : ProbComp α) : program.eval.support = OracleComp.support program

The possible results of a closed probabilistic program are its results for any replies, since every uniform reply has positive probability.

theorem Cslib.ProbComp.support_nonempty {α : Type} (program : ProbComp α) : (OracleComp.support program).Nonempty

Every closed probabilistic program has at least one possible result.

@[simp]

theorem Cslib.ProbComp.mem_support_unifFin (n : ℕ) (k : Fin (n + 1)) : k ∈ OracleComp.support (unifFin n)

Every value in Fin (n + 1) is a possible output of unifFin n.

theorem Cslib.ProbComp.isMonadHom_eval : IsMonadHom ProbComp PMF @eval

Evaluating a closed probabilistic program is a monad morphism into PMF.

theorem Cslib.ProbComp.eval_interpret {α ι : Type} {spec : ι → Type} (handler : (q : ι) → ProbComp (spec q)) (program : OracleComp spec α) : (OracleComp.interpret handler program).eval = OracleComp.interpret (fun (q : ι) => (handler q).eval) program

Evaluating an interpreted oracle program is interpreting each call by its evaluated sampler.