Output Distribution of Computations

This file defines HasEvalDist and related instances for OracleComp.

def OracleComp.supportWhen {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (o : QueryImpl spec Set) (mx : OracleComp spec α) : Set α

The possible outputs of mx when queries can output values in the specified sets. NOTE: currently proofs using this should reduce to simulateQ. A full API would be better

@[simp]

theorem OracleComp.supportWhen_pure {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (o : QueryImpl spec Set) (x : α) : supportWhen o (pure x) = {x}

@[simp]

theorem OracleComp.supportWhen_query_bind {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (o : QueryImpl spec Set) (q : spec.Domain) (oa : spec.Range q → OracleComp spec α) : supportWhen o (liftM (query q) >>= oa) = ⋃ x ∈ o q, supportWhen o (oa x)

@[simp]

theorem OracleComp.supportWhen_bind {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} (o : QueryImpl spec Set) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : supportWhen o (oa >>= ob) = ⋃ x ∈ supportWhen o oa, supportWhen o (ob x)

Reachable outputs of a bind are the reachable outputs of the continuation over reachable outputs of the first computation.

theorem OracleComp.mem_supportWhen_bind_iff {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} (o : QueryImpl spec Set) (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : y ∈ supportWhen o (oa >>= ob) ↔ ∃ x ∈ supportWhen o oa, y ∈ supportWhen o (ob x)

Membership form of [OracleComp.supportWhen_bind].

theorem OracleComp.supportWhen_mono {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} {o₁ o₂ : QueryImpl spec Set} (h : ∀ (q : spec.Domain), o₁ q ⊆ o₂ q) (oa : OracleComp spec α) : supportWhen o₁ oa ⊆ supportWhen o₂ oa

Enlarging the set of possible oracle outputs only enlarges the reachable output set.

@[implicit_reducible]

instance OracleComp.hasEvalSet {ι : Type u_1} {spec : OracleSpec ι} : HasEvalSet (OracleComp spec)

The support instance for OracleComp, defined as

theorem OracleComp.support_eq_simulateQ {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (mx : OracleComp spec α) : support mx = simulateQ (fun (x : spec.Domain) => Set.univ) mx

@[simp]

theorem OracleComp.support_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (q : OracleQuery spec α) : support (liftM q) = Set.range q.cont

theorem OracleComp.support_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : support (liftM (query t)) = Set.univ

theorem OracleComp.mem_support_liftM_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (q : OracleQuery spec α) (u : α) : u ∈ support (liftM q) ↔ ∃ (t : spec.Range q.input), q.cont t = u

theorem OracleComp.mem_support_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : u ∈ support (liftM (query t))

theorem OracleComp.support_liftM_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : support (liftM (query t)) = Set.univ

Alias of OracleComp.support_query.

theorem OracleComp.bind_congr_of_forall_mem_support {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} (mx : OracleComp spec α) {f g : α → OracleComp spec β} (h : ∀ x ∈ support mx, f x = g x) : mx >>= f = mx >>= g

Support-aware bind congruence: if two continuations agree on all elements in the support of mx, the resulting bind computations are equal.

@[implicit_reducible]

instance OracleComp.instHasEvalFinset {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] : HasEvalFinset (OracleComp spec)

Finite version of support for when oracles have a finite set of possible outputs. NOTE: we can't use simulateQ because Finset lacks a Monad instance.

@[simp]

theorem OracleComp.finSupport_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [DecidableEq α] (q : OracleQuery spec α) : finSupport (liftM q) = Finset.image q.cont Finset.univ

theorem OracleComp.finSupport_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.DecidableEq] (t : spec.Domain) : finSupport (liftM (query t)) = Finset.univ

theorem OracleComp.mem_finSupport_liftM_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [DecidableEq α] (q : OracleQuery spec α) (x : α) : x ∈ finSupport (liftM q) ↔ ∃ (t : spec.Range q.input), q.cont t = x

theorem OracleComp.mem_finSupport_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.DecidableEq] (t : spec.Domain) (u : spec.Range t) : u ∈ finSupport (liftM (query t))

noncomputable def OracleComp.evalDistWhen {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (d : QueryImpl spec SPMF) (mx : OracleComp spec α) : SPMF α

The output distribution of mx when queries follow the specified distribution. NOTE: currently proofs using this should reduce to simulateQ. A full API would be better

@[implicit_reducible]

noncomputable instance OracleComp.instHasEvalPMF {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] : HasEvalPMF (OracleComp spec)

Embed OracleComp into SPMF by mapping queries to uniform distributions over their range.

theorem OracleComp.evalDist_eq_simulateQ {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (mx : OracleComp spec α) : evalDist mx = liftM (simulateQ (fun (t : spec.Domain) => PMF.uniformOfFintype (spec.Range t)) mx)

@[simp]

theorem OracleComp.evalDist_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (q : OracleQuery spec α) : evalDist (liftM q) = liftM (PMF.map q.cont (PMF.uniformOfFintype (spec.Range q.input)))

@[simp]

theorem OracleComp.evalDist_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) : evalDist (liftM (query t)) = liftM (PMF.uniformOfFintype (spec.Range t))

@[simp]

theorem OracleComp.probOutput_liftM_eq_div {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (q : OracleQuery spec α) (x : α) : Pr[= x | liftM q] = (∑' (u : spec.Range q.input), Pr[= x | pure (q.cont u)]) / ↑(Fintype.card (spec.Range q.input))

@[simp]

theorem OracleComp.probOutput_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (u : spec.Range t) : Pr[= u | liftM (query t)] = (↑(Fintype.card (spec.Range t)))⁻¹

theorem OracleComp.probEvent_liftM_eq_div {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (q : OracleQuery spec α) (p : α → Prop) : probEvent (liftM q) p = (∑' (u : spec.Range q.input), probEvent (pure (q.cont u)) p) / ↑(Fintype.card (spec.Range q.input))

theorem OracleComp.probOutput_query_eq_div {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (u : spec.Range t) : Pr[= u | liftM (query t)] = 1 / ↑(Fintype.card (spec.Range t))

@[simp]

theorem OracleComp.probEvent_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (p : spec.Range t → Prop) [DecidablePred p] : probEvent (liftM (query t)) p = ↑{x : spec.Range t | p x}.card / ↑(Fintype.card (spec.Range t))

@[simp]

theorem OracleComp.mem_support_evalDist_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (x : α) : some x ∈ (OptionT.run (evalDist oa)).support ↔ x ∈ support oa

An output has non-zero probability in evalDist iff it is in computation support.

theorem OracleComp.mem_support_of_mem_support_evalDist {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (x : α) : some x ∈ (OptionT.run (evalDist oa)).support → x ∈ support oa

Alias of the forward direction of OracleComp.mem_support_evalDist_iff.

---

An output has non-zero probability in evalDist iff it is in computation support.

theorem OracleComp.mem_support_evalDist {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (x : α) : x ∈ support oa → some x ∈ (OptionT.run (evalDist oa)).support

Alias of the reverse direction of OracleComp.mem_support_evalDist_iff.

---

An output has non-zero probability in evalDist iff it is in computation support.

@[simp]

theorem OracleComp.mem_support_evalDist_iff' {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (x : α) [DecidableEq α] : some x ∈ (OptionT.run (evalDist oa)).support ↔ x ∈ finSupport oa

Finite-support variant of mem_support_evalDist_iff.

theorem OracleComp.mem_support_evalDist' {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (x : α) [DecidableEq α] : x ∈ finSupport oa → some x ∈ (OptionT.run (evalDist oa)).support

Alias of the reverse direction of OracleComp.mem_support_evalDist_iff'.

---

Finite-support variant of mem_support_evalDist_iff.

theorem OracleComp.mem_finSupport_of_mem_support_evalDist {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) (x : α) [DecidableEq α] : some x ∈ (OptionT.run (evalDist oa)).support → x ∈ finSupport oa

Alias of the forward direction of OracleComp.mem_support_evalDist_iff'.

---

Finite-support variant of mem_support_evalDist_iff.

@[simp]

theorem OracleComp.probFailure_eq_zero_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) : Pr[⊥ | oa] = 0 ↔ NeverFail oa

@[simp]

theorem OracleComp.probFailure_pos_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) : 0 < Pr[⊥ | oa] ↔ ¬NeverFail oa

theorem OracleComp.noFailure_of_probFailure_eq_zero {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] {oa : OracleComp spec α} (h : Pr[⊥ | oa] = 0) : NeverFail oa

theorem OracleComp.not_noFailure_of_probFailure_pos {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] {oa : OracleComp spec α} (h : 0 < Pr[⊥ | oa]) : ¬NeverFail oa

theorem OracleComp.evalDist_query_bind {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (ou : spec.Range t → OracleComp spec α) : evalDist (liftM (query t) >>= ou) = OptionT.lift (PMF.uniformOfFintype (spec.Range t)) >>= evalDist ∘ ou

theorem OracleComp.probOutput_congr {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.Fintype] [spec.Inhabited] {x y : α} {oa : OracleComp spec α} {oa' : OracleComp spec' α} [spec'.Fintype] [spec'.Inhabited] (h1 : x = y) (h2 : evalDist oa = evalDist oa') : Pr[= x | oa] = Pr[= y | oa']

theorem OracleComp.probEvent_congr' {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.Fintype] [spec.Inhabited] {p q : α → Prop} {oa : OracleComp spec α} {oa' : OracleComp spec' α} [spec'.Fintype] [spec'.Inhabited] (h1 : ∀ x ∈ support oa, p x ↔ q x) (h2 : evalDist oa = evalDist oa') : probEvent oa p = probEvent oa' q

theorem OracleComp.evalDist_ext_probEvent {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.Fintype] [spec.Inhabited] {oa : OracleComp spec α} {oa' : OracleComp spec' α} [spec'.Fintype] [spec'.Inhabited] (h : ∀ (x : α), Pr[= x | oa] = Pr[= x | oa']) : OptionT.run (evalDist oa) = OptionT.run (evalDist oa')

theorem OracleComp.probFailure_eq_sub_probEvent' {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec α) : Pr[⊥ | oa] = 1 - probEvent oa fun (x : α) => True

@[simp]

theorem OracleComp.probOutput_guard {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {p : Prop} [Decidable p] : Pr[= () | guard p] = if p then 1 else 0

@[simp]

theorem OracleComp.probFailure_guard {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {p : Prop} [Decidable p] : Pr[⊥ | guard p] = if p then 0 else 1

theorem OracleComp.probOutput_eq_sub_probFailure_of_unit {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {oa : OracleComp spec PUnit.{1}} : Pr[= () | oa] = 1 - Pr[⊥ | oa]

theorem OracleComp.probOutput_guard_eq_sub_probOutput_guard_not {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {oa : OracleComp spec α} [NeverFail oa] {p : α → Prop} [DecidablePred p] : Pr[= () | do let a ← liftM oa guard (p a)] = 1 - Pr[= () | do let a ← liftM oa guard ¬p a]

theorem OracleComp.evalDist_simulateQ_run'_eq_evalDist {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec))) (h : ∀ (t : spec.Domain) (s : σ), evalDist ((so t).run' s) = OptionT.lift (PMF.uniformOfFintype (spec.Range t))) (s : σ) (oa : OracleComp spec τ) : evalDist ((simulateQ so oa).run' s) = evalDist oa

If a StateT oracle implementation preserves distributions (each oracle query produces a uniform distribution after discarding state), then simulateQ followed by run' preserves evalDist. This is the key lemma for security proofs: it shows that stateful oracle implementations (e.g. counting/logging oracles) don't change outcome probabilities.

theorem OracleComp.evalDist_simulateQ_run'_of_run'_eq_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec))) (h : ∀ (t : spec.Domain) (s : σ), (so t).run' s = liftM (query t)) (s : σ) (oa : OracleComp spec τ) : evalDist ((simulateQ so oa).run' s) = evalDist oa

Stronger version with computational hypothesis: if the implementation passes through queries exactly, then simulateQ preserves evalDist.

theorem OracleComp.probOutput_simulateQ_run'_eq {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec))) (h : ∀ (t : spec.Domain) (s : σ), evalDist ((so t).run' s) = OptionT.lift (PMF.uniformOfFintype (spec.Range t))) (s : σ) (oa : OracleComp spec τ) (x : τ) : Pr[= x | (simulateQ so oa).run' s] = Pr[= x | oa]

Corollary for probOutput: stateful simulation preserves output probabilities.

theorem OracleComp.probEvent_simulateQ_run'_eq {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec))) (h : ∀ (t : spec.Domain) (s : σ), evalDist ((so t).run' s) = OptionT.lift (PMF.uniformOfFintype (spec.Range t))) (s : σ) (oa : OracleComp spec τ) (p : τ → Prop) : probEvent ((simulateQ so oa).run' s) p = probEvent oa p

Corollary for probEvent: stateful simulation preserves event probabilities.

theorem OracleComp.evalDist_simulateQ_run_eq_of_impl_evalDist_eq {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {ι' : Type} {spec' : OracleSpec ι'} {σ α : Type} (impl₁ impl₂ : QueryImpl spec' (StateT σ (OracleComp spec))) (h : ∀ (t : spec'.Domain) (s : σ), evalDist ((impl₁ t).run s) = evalDist ((impl₂ t).run s)) (comp : OracleComp spec' α) (s : σ) : evalDist ((simulateQ impl₁ comp).run s) = evalDist ((simulateQ impl₂ comp).run s)