Output Distribution of Computations

This file defines the MonadLiftT-based probability and support semantics for OracleComp.

@[reducible, inline]

abbrev OracleSpec.IsProbabilitySpec {ι : Type u_1} (spec : OracleSpec ι) : Type (max u_2 u_1)

A per-query distribution on an OracleSpec, definitionally the generic probability specification on its underlying polynomial functor.

@[reducible, inline]

abbrev OracleSpec.IsProbabilitySpec.toPMF {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] (t : spec.Domain) : PMF (spec.Range t)

The distribution of responses to query t.

class OracleSpec.IsUniformSpec {ι : Type u_1} (spec : OracleSpec ι) extends spec.toPFunctor.IsProbabilitySpec : Type (max u_1 u_2)

An OracleSpec whose responses are uniformly sampled from finite, inhabited ranges. Bundles finiteness and inhabitedness of every response type with IsProbabilitySpec spec and a Prop witness that the per-query distribution agrees with PMF.uniformOfFintype. Use this as the canonical input to lemmas that mention Fintype.card (spec.Range _) or PMF.uniformOfFintype in their statements.

• toPMF : Handler PMF spec.toPFunctor
• fintype (t : ι) : Fintype (spec.Range t)

  Every response set is finite.

• inhabited (t : ι) : Inhabited (spec.Range t)

  Every response set is inhabited.

• toPMF_eq_uniform (t : spec.toPFunctor.A) : PFunctor.IsProbabilitySpec.toPMF t = PMF.uniformOfFintype (spec.Range t)

  The per-query distribution is the uniform distribution on the response set.

@[reducible]

noncomputable def OracleSpec.IsUniformSpec.ofFintypeInhabited {ι : Type u} (spec : OracleSpec ι) [hF : (t : ι) → Fintype (spec.Range t)] [hI : (t : ι) → Inhabited (spec.Range t)] : spec.IsUniformSpec

Bridge from finite, inhabited response types to IsUniformSpec spec. Deliberately not an instance — IsUniformSpec must be opted into per spec so that uniform-sampling semantics never attach silently to a spec whose author didn't intend a probabilistic interpretation. Use this helper when declaring IsUniformSpec for a concrete spec.

@[instance_reducible]

noncomputable instance OracleSpec.instIsUniformSpecNatUnifSpec : unifSpec.IsUniformSpec

@[instance_reducible]

noncomputable instance OracleSpec.instIsUniformSpecUnitCoinSpec : coinSpec.IsUniformSpec

@[instance_reducible]

noncomputable instance OracleSpec.instIsUniformSpecAdd {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') [spec.IsUniformSpec] [spec'.IsUniformSpec] : (spec + spec').IsUniformSpec

Propagate IsUniformSpec through +: each summand's uniformity is preserved on its branch. IsProbabilitySpec (spec + spec') is derived via the extends chain.

@[reducible]

noncomputable def OracleSpec.IsUniformSpec.toPFunctor {ι : Type u_1} {spec : OracleSpec ι} [h : spec.IsUniformSpec] : spec.toPFunctor.IsUniformSpec

Package uniform oracle semantics as generic uniform semantics on the underlying polynomial functor. This is an explicit conversion rather than an instance so it cannot participate in overly broad toPFunctor unification.

Oracle-facing semantics

theorem OracleComp.evalSPMF_eq_simulateQ {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] (mx : OracleComp spec α) : 𝒮[mx] = liftM (simulateQ OracleSpec.IsProbabilitySpec.toPMF mx)

theorem OracleComp.evalSPMF_liftM_toPMF {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] (q : OracleQuery spec α) : 𝒮[liftM q] = liftM (PMF.map q.cont (OracleSpec.IsProbabilitySpec.toPMF q.input))

Abstract distribution of a single lifted query under IsProbabilitySpec: the per-query distribution toPMF is pushed forward through the query's continuation. Uniform-content sibling: evalSPMF_liftM.

theorem OracleComp.evalSPMF_query_toPMF {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] (t : spec.Domain) : 𝒮[liftM (OracleSpec.query t)] = liftM (OracleSpec.IsProbabilitySpec.toPMF t)

liftM (query t) : OracleComp spec _ evaluates to the per-query distribution IsProbabilitySpec.toPMF t, lifted to SPMF.

@[simp]

theorem OracleComp.evalSPMF_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (q : OracleQuery spec α) : 𝒮[liftM q] = liftM (PMF.map q.cont (PMF.uniformOfFintype (spec.Range q.input)))

@[simp]

theorem OracleComp.evalSPMF_query {ι : Type u_1} {spec : OracleSpec ι} [spec.IsUniformSpec] (t : spec.Domain) : 𝒮[liftM (OracleSpec.query t)] = liftM (PMF.uniformOfFintype (spec.Range t))

@[simp]

theorem OracleComp.probOutput_liftM_eq_div {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (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.IsUniformSpec] (t : spec.Domain) (u : spec.Range t) : Pr[= u | liftM (OracleSpec.query t)] = (↑(Fintype.card (spec.Range t)))⁻¹

theorem OracleComp.probEvent_liftM_eq_div {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (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.IsUniformSpec] (t : spec.Domain) (u : spec.Range t) : Pr[= u | liftM (OracleSpec.query t)] = 1 / ↑(Fintype.card (spec.Range t))

@[simp]

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

theorem OracleComp.probEvent_query_le_inv_of_unique {ι : Type u_1} {spec : OracleSpec ι} [spec.IsUniformSpec] (t : spec.Domain) (p : spec.Range t → Prop) (hunique : ∀ (x y : spec.Range t), p x → p y → x = y) : probEvent (liftM (OracleSpec.query t)) p ≤ (↑(Fintype.card (spec.Range t)))⁻¹

An event selecting at most one response to a uniform oracle query has probability at most the inverse response-space cardinality.

instance OracleComp.instEvalDistCompatible {ι : Type u_2} {spec : OracleSpec ι} [spec.IsUniformSpec] : EvalDistCompatible (OracleComp spec)

OracleComp spec admits the bridge between its direct support semantics and the SPMF.support of its evalSPMF.

theorem OracleComp.support_eq_evalSPMF_support {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) : support oa = 𝒮[oa].support

The reachable outputs of oa are exactly the outputs its distribution semantics gives nonzero probability. This is EvalDistCompatible.support_eq_SPMF_support specialized to the oracle façade, and it is the named bridge to reach for when a proof needs to move between the two semantics without unfolding either into its SetM / SPMF interpreter.

theorem OracleComp.mem_support_evalSPMF_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) : some x ∈ (OptionT.run 𝒮[oa]).support ↔ x ∈ support oa

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

theorem OracleComp.mem_support_evalSPMF {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) : x ∈ support oa → some x ∈ (OptionT.run 𝒮[oa]).support

Alias of the reverse direction of OracleComp.mem_support_evalSPMF_iff.

---

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

theorem OracleComp.mem_support_of_mem_support_evalSPMF {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) : some x ∈ (OptionT.run 𝒮[oa]).support → x ∈ support oa

Alias of the forward direction of OracleComp.mem_support_evalSPMF_iff.

---

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

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

Finite-support variant of mem_support_evalSPMF_iff.

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

Alias of the reverse direction of OracleComp.mem_support_evalSPMF_iff'.

---

Finite-support variant of mem_support_evalSPMF_iff.

theorem OracleComp.mem_finSupport_of_mem_support_evalSPMF {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (oa : OracleComp spec α) (x : α) [DecidableEq α] : some x ∈ (OptionT.run 𝒮[oa]).support → x ∈ finSupport oa

Alias of the forward direction of OracleComp.mem_support_evalSPMF_iff'.

---

Finite-support variant of mem_support_evalSPMF_iff.

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

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

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

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

theorem OracleComp.evalSPMF_query_bind {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsUniformSpec] (t : spec.Domain) (ou : spec.Range t → OracleComp spec α) : 𝒮[liftM (OracleSpec.query t) >>= ou] = do let u ← liftM (PMF.uniformOfFintype (spec.Range t)) 𝒮[ou u]

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

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

Two events have equal probabilities when their predicates agree on the support of the first computation and the two computations share an evaluation distribution.

theorem OracleComp.evalSPMF_ext_probEvent {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.IsUniformSpec] [spec'.IsProbabilitySpec] {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h : ∀ (x : α), Pr[= x | oa] = Pr[= x | oa']) : OptionT.run 𝒮[oa] = OptionT.run 𝒮[oa']

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

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

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

theorem OracleComp.support_guard {ι : Type u_2} {spec : OracleSpec ι} {p : Prop} [Decidable p] : support (guard p) = if p then {()} else ∅

theorem OracleComp.probOutput_punit_eq_sub_probFailure {m : Type → Type u_1} [Monad m] [MonadLiftT m SPMF] {oa : m PUnit.{1}} : Pr[= () | oa] = 1 - Pr[⊥ | oa]

For any PUnit-valued computation in an arbitrary monad with an SPMF denotation, the probability of returning () is the complementary mass of its failure probability.

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

The OracleComp instance of probOutput_punit_eq_sub_probFailure: for a PUnit-valued oracle computation, the probability of returning () is the complementary mass of its failure probability.

theorem OracleComp.probOutput_bind_guard_eq_probEvent {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {α : Type} (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] : Pr[= () | do let a ← liftM oa guard (p a)] = probEvent oa p

Guarding a computation oa by a decidable predicate p and asking for the probability of a successful () output recovers exactly the event probability Pr[p | oa]: the failure mass of the guard removes precisely the outputs falsifying p. Public guard-section API used by failure-based security experiments.

theorem OracleComp.probOutput_guard_eq_sub_probOutput_guard_not {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {α : 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]

Probabilities of orElse (<|>)

oa <|> oa' runs oa, falling back to oa' only when oa returns none. The base OracleComp never fails, so the two failure events are independent: oa <|> oa' fails exactly when both do, and an output comes either from oa or — on oa's failure mass — from oa'. (support_orElse is left as a future addition; it follows from probOutput_orElse via the support↔probability bridge.)

@[simp]

theorem OracleComp.probFailure_orElse {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {α : Type} (oa oa' : OptionT (OracleComp spec) α) : Pr[⊥ | oa <|> oa'] = Pr[⊥ | oa] * Pr[⊥ | oa']

@[simp]

theorem OracleComp.probOutput_orElse {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {α : Type} (oa oa' : OptionT (OracleComp spec) α) (x : α) : Pr[= x | oa <|> oa'] = Pr[= x | oa] + Pr[⊥ | oa] * Pr[= x | oa']

@[simp]

theorem OracleComp.probEvent_orElse {ι : Type u_1} {spec : OracleSpec ι} [spec.IsProbabilitySpec] {α : Type} (oa oa' : OptionT (OracleComp spec) α) (p : α → Prop) : probEvent (oa <|> oa') p = probEvent oa p + Pr[⊥ | oa] * probEvent oa' p

theorem OracleComp.evalSPMF_simulateQ_eq_evalSPMF {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type w} [spec.IsProbabilitySpec] [spec'.IsProbabilitySpec] (so : QueryImpl spec' (OracleComp spec)) (h : ∀ (t : spec'.Domain), 𝒮[so t] = 𝒮[liftM (OracleSpec.query t)]) (oa : OracleComp spec' α) : 𝒮[simulateQ so oa] = 𝒮[oa]

If an oracle implementation preserves the distribution of each source query, then simulateQ preserves the distribution of every source computation.

@[reducible]

noncomputable def OracleComp.evalSPMFWhen {ι : 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.

theorem OracleComp.mem_support_bind_peel {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} (mx : OracleComp spec α) (f : α → OracleComp spec β) {y : β} (hy : y ∈ support (mx >>= f)) : ∃ a ∈ support mx, y ∈ support (f a)

obtain-friendly bind support peeler at the bare OracleComp level. Unlike rw [mem_support_bind_iff], applying this lemma to a hypothesis uses definitional unification to match mx >>= f, so it engages through the Monad/MonadLift instance-tree mismatches that block the syntactic rw (the elaborated OracleComp.instMonad/Bind.bind spelling produced by unfolding nested protocol definitions differs syntactically from the canonical >>=).

theorem OracleComp.eq_of_mem_support_pure {ι : Type u_2} {spec : OracleSpec ι} {α : Type w} (a : α) {y : α} (hy : y ∈ support (pure a)) : y = a

obtain-friendly pure support resolver at the bare OracleComp level: y ∈ support (pure a) forces y = a, matched by definitional unification (so it engages on the PFunctor.FreeM.pure spelling that the syntactic support_pure rw rejects).

theorem OracleComp.mem_support_map_peel {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} (g : α → β) (mx : OracleComp spec α) {y : β} (hy : y ∈ support (g <$> mx)) : ∃ a ∈ support mx, y = g a

obtain-friendly <$> (map) support peeler at the bare OracleComp level: y ∈ support (g <$> mx) yields a preimage a ∈ support mx with y = g a, matched by definitional unification (so it engages on the elaborated Functor.map/OracleComp.instMonad spelling that the syntactic support_map rw rejects).

theorem OracleComp.probEvent_ofFreeM_map {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} [spec.IsProbabilitySpec] (mx : spec.toPFunctor.FreeM α) (f : α → β) (event : β → Prop) : probEvent (ofFreeM (PFunctor.FreeM.map f mx)) event = probEvent (ofFreeM mx) (event ∘ f)

Probability of an event after mapping a raw polynomial free program, viewed through the OracleComp semantic bridge.

theorem OracleComp.probEvent_ofFreeM_pure {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.IsProbabilitySpec] (x : α) (event : α → Prop) [DecidablePred event] : probEvent (ofFreeM (pure x)) event = if event x then 1 else 0

Probability of an event for a raw polynomial pure, viewed through OracleComp.

theorem OracleComp.probEvent_ofFreeM_bind_eq_tsum {ι : Type u_1} {spec : OracleSpec ι} {α β : Type w} [spec.IsProbabilitySpec] (mx : spec.toPFunctor.FreeM α) (next : α → spec.toPFunctor.FreeM β) (event : β → Prop) : probEvent (ofFreeM (mx.bind next)) event = ∑' (x : α), Pr[= x | ofFreeM mx] * probEvent (ofFreeM (next x)) event

Bind decomposition for a raw polynomial free program, viewed through OracleComp.

theorem OptionT.mem_support_run_bind {ι : Type} {spec : OracleSpec ι} {α β : Type} (mx : OptionT (OracleComp spec) α) (f : α → OptionT (OracleComp spec) β) {y : Option β} (hy : y ∈ support (mx >>= f).run) : none ∈ support mx.run ∧ y = none ∨ ∃ (a : α), some a ∈ support mx.run ∧ y ∈ support (f a).run

Support-level peeler for an OptionT-monadic bind, stated at the underlying OracleComp-level .run: every element y of the support of the run of mx >>= f factors through an intermediate some a in mx's run support and a y in the run support of f a, unless mx's run can produce none (in which case y may be that none). Companion to OptionT.mem_support_bind_mk for the case where the OptionT.run has already been stripped to the bare underlying computation.

Applies to a hypothesis y ∈ support oa whenever oa is definitionally (mx >>= f).run (the OptionT.run is identity), so callers need not respell the full bind term.

theorem OptionT.mem_support_run_lift_bind {ι : Type} {spec : OracleSpec ι} {α β : Type} (oa : OracleComp spec α) (f : α → OptionT (OracleComp spec) β) {y : Option β} (hy : y ∈ support (OptionT.lift oa >>= f).run) : ∃ a ∈ support oa, y ∈ support (f a).run

OptionT.lift-headed specialization of mem_support_run_bind: a lifted (hence never-failing) first computation oa peels cleanly, with the intermediate value living in support oa directly (no none branch).