From ff454cda0e11e569477f551ded1fbdc25a6eada3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 12:01:42 -0400 Subject: [PATCH] feat(probabilistic): one semantics for OracleComp Add Languages/Probabilistic/Semantics.lean with the generic semantics of oracle programs relative to their answers: - OracleComp.evalWith h: the output distribution for independent answers drawn from h, via interpret; - OracleComp.supportWith possible: the structural possible results for answers in given sets, with two-way pure/bind/map/query rules; - OracleComp.runWith oracle: the joint law of result and final state of a stateful StateT oracle. Prove that they agree (support_evalWith, mem_supportWith_of_mem_support_runWith, runWith_lift), compose with interpret and sumHandler, and agree with the existing specializations: ProbComp.eval_eq_evalWith, ProbComp.support_eval_eq_supportWith, ProbOracleComp.support_eq_supportWith, ProbOracleComp.runWith_eq_runWith_sumHandler, ProbOracleComp.runWith_lift and ProbOracleComp.acceptProbWith_lift. Record the principle that algorithms are programs and PMF is for semantics, in the module docstring and CONTRIBUTING. Part of #814. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- CONTRIBUTING.md | 11 + Complexity.lean | 1 + .../Probabilistic/Oracle/Interaction.lean | 39 ++ .../Probabilistic/Oracle/Support.lean | 15 + .../Languages/Probabilistic/Semantics.lean | 395 ++++++++++++++++++ ComplexityTests.lean | 1 + ComplexityTests/OracleSemantics.lean | 89 ++++ 7 files changed, 551 insertions(+) create mode 100644 Complexity/Languages/Probabilistic/Semantics.lean create mode 100644 ComplexityTests/OracleSemantics.lean diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 34e71e2f97..d0664e22ff 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -53,6 +53,17 @@ Mathlib's standard linter set already enforces the mechanical part; reviews enfo Improving an interface never weakens the mathematics: keep the models, encodings, independent resource bounds and nonvacuity of the results it touches. +### Algorithms are programs + +Probabilistic algorithms, such as key generation, signing, provers, verifiers, simulators, +extractors, samplers and reductions, are `ProbComp` or `OracleComp` programs. `PMF` is reserved +for their semantics, `OracleComp.evalWith` and its instances such as `ProbComp.eval`, and for +genuinely semantic objects: ideal distributions, the laws of games and the distributions compared +in a statistical argument. A program can be run against different oracles, budgeted, realized by a +machine and substituted into a reduction. A `PMF`-valued algorithm can do none of these, and +needs a separate hypothesis that some program realizes it. Exact theorems stay exact, as +statements about `evalWith`; see `Complexity/Languages/Probabilistic/Semantics.lean`. + ### Public surface under the module system Under an ordinary `import`, importers rebuild only when a module's exported `.olean` changes. That diff --git a/Complexity.lean b/Complexity.lean index cdcc00fa44..42468095ea 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1782,6 +1782,7 @@ public import Complexity.Languages.Probabilistic.RandomOracle public import Complexity.Languages.Probabilistic.RandomOracle.Probabilistic public import Complexity.Languages.Probabilistic.Repeat public import Complexity.Languages.Probabilistic.Selection +public import Complexity.Languages.Probabilistic.Semantics public import Complexity.Languages.Probabilistic.Simulation public import Complexity.Languages.Probabilistic.Sum public import Complexity.Languages.Probabilistic.Transcript diff --git a/Complexity/Languages/Probabilistic/Oracle/Interaction.lean b/Complexity/Languages/Probabilistic/Oracle/Interaction.lean index 22ad30e0b3..79299168f3 100644 --- a/Complexity/Languages/Probabilistic/Oracle/Interaction.lean +++ b/Complexity/Languages/Probabilistic/Oracle/Interaction.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Languages.Probabilistic.Oracle +public import Complexity.Languages.Probabilistic.Semantics /-! # Running a program against a stateful oracle @@ -20,6 +21,11 @@ and the final oracle state, with fresh fair samples for the private coins, and A prover of an interactive proof is such an oracle; `Cslib.Complexity.Prover.run` is the case of word queries and replies (`Cslib.Complexity.Prover.run_eq_runWith`). +`runWith` is the instance of the generic `OracleComp.runWith` whose handler is the sum of the +lifted uniform handler and `oracle` (`runWith_eq_runWith_sumHandler`). Against a memoryless oracle +it is `OracleComp.evalWith` of the sum of the uniform handler and the oracle, with the state +unchanged (`runWith_lift`). + ## Main definitions * `Cslib.ProbOracleComp.runWith`: the joint law of the result and the final oracle state. @@ -27,6 +33,8 @@ word queries and replies (`Cslib.Complexity.Prover.run_eq_runWith`). ## Main results +* `Cslib.ProbOracleComp.runWith_eq_runWith_sumHandler`, `Cslib.ProbOracleComp.runWith_lift`, + `Cslib.ProbOracleComp.acceptProbWith_lift`: the instances of the generic semantics. * `Cslib.ProbOracleComp.runWith_pure`, `Cslib.ProbOracleComp.runWith_bind`, `Cslib.ProbOracleComp.runWith_map`, `Cslib.ProbOracleComp.runWith_query`, `Cslib.ProbOracleComp.runWith_sample`: structural rules for `runWith`. @@ -56,6 +64,37 @@ noncomputable def runWith (program : ProbOracleComp spec α) (s : State) : PMF ( noncomputable def acceptProbWith (program : ProbOracleComp spec Bool) (s : State) : ℝ≥0∞ := (runWith oracle program s).map Prod.fst true +/-- The run is the generic stateful run whose handler answers private samples by fresh uniform +draws, keeping the state, and external calls by `oracle`. -/ +theorem runWith_eq_runWith_sumHandler (program : ProbOracleComp spec α) (s : State) : + runWith oracle program s = + OracleComp.runWith (OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) + oracle) program s := by + rw [runWith, handler_eq_sumHandler] + rfl + +/-- Against a memoryless oracle, the run is `OracleComp.evalWith` of the uniform handler on the +sampling side and the oracle on the other, with the state unchanged. -/ +theorem runWith_lift (h : (q : Query) → PMF (spec q)) (program : ProbOracleComp spec α) + (s : State) : + runWith (fun q => StateT.lift (h q)) program s = + (OracleComp.evalWith (OracleComp.sumHandler ProbComp.unifOracle h) program).map (·, s) := by + have hlift : OracleComp.sumHandler (fun n => StateT.lift (σ := State) (ProbComp.unifOracle n)) + (fun q => StateT.lift (h q)) = + fun q => StateT.lift (OracleComp.sumHandler ProbComp.unifOracle h q) := by + funext q + cases q <;> rfl + rw [runWith_eq_runWith_sumHandler, hlift, OracleComp.runWith_lift] + +/-- Against a memoryless oracle, the acceptance probability is the probability of `true` under +`OracleComp.evalWith` of the uniform handler and the oracle. -/ +theorem acceptProbWith_lift (h : (q : Query) → PMF (spec q)) (program : ProbOracleComp spec Bool) + (s : State) : + acceptProbWith (fun q => StateT.lift (h q)) program s = + OracleComp.evalWith (OracleComp.sumHandler ProbComp.unifOracle h) program true := by + rw [acceptProbWith, runWith_lift, PMF.map_comp, + show (Prod.fst ∘ fun a : Bool => (a, s)) = id from rfl, PMF.map_id] + /-- A pure program returns its value and leaves the oracle state unchanged. -/ @[simp] theorem runWith_pure (a : α) (s : State) : runWith oracle (pure a) s = PMF.pure (a, s) := OracleComp.run_interpret_pure _ _ _ diff --git a/Complexity/Languages/Probabilistic/Oracle/Support.lean b/Complexity/Languages/Probabilistic/Oracle/Support.lean index 3493cfc2e5..4c82199ce9 100644 --- a/Complexity/Languages/Probabilistic/Oracle/Support.lean +++ b/Complexity/Languages/Probabilistic/Oracle/Support.lean @@ -9,6 +9,7 @@ module public import Complexity.Languages.Probabilistic.Oracle public import Complexity.Languages.Probabilistic.Iteration +public import Complexity.Languages.Probabilistic.Semantics import Complexity.Languages.Probabilistic.Oracle.Simulation @@ -23,12 +24,17 @@ some stateful execution (`mem_support_iff_exists`): an oracle that answers its f 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. +`support` is the instance of the generic `OracleComp.supportWith` in which every reply is possible +(`support_eq_supportWith`). + ## Main definitions * `Cslib.ProbOracleComp.support`: the results at the leaves of the program's tree of calls. ## Main results +* `Cslib.ProbOracleComp.support_eq_supportWith`: `support` is `OracleComp.supportWith` of all + replies. * `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. @@ -59,6 +65,15 @@ def support : ProbOracleComp spec α → Set α | .pure a => {a} | .liftBind _ cont => ⋃ a, support (cont a) +/-- The possible results are the generic `OracleComp.supportWith` with every reply possible. -/ +theorem support_eq_supportWith (program : ProbOracleComp spec α) : + support program = OracleComp.supportWith (fun _ => Set.univ) program := by + induction program with + | pure a => rfl + | liftBind q cont ih => + change ⋃ a, support (cont a) = ⋃ a ∈ Set.univ, OracleComp.supportWith _ (cont a) + simp only [ih, Set.mem_univ, Set.iUnion_true] + /-- A returned value is the only possible result. -/ @[simp] theorem support_pure (a : α) : support (pure a : ProbOracleComp spec α) = {a} := rfl diff --git a/Complexity/Languages/Probabilistic/Semantics.lean b/Complexity/Languages/Probabilistic/Semantics.lean new file mode 100644 index 0000000000..7111aca99b --- /dev/null +++ b/Complexity/Languages/Probabilistic/Semantics.lean @@ -0,0 +1,395 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Languages.Probabilistic.Simulation +public import Complexity.Languages.Probabilistic.Sum + +/-! +# 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. +* `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_eq_supportWith`). 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, and its possible results are +`supportWith` of all replies (`ProbOracleComp.runWith_eq_runWith_sumHandler`, +`ProbOracleComp.support_eq_supportWith`). + +## 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.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`, 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.ProbComp.eval_eq_evalWith`, `Cslib.ProbComp.support_eval_eq_supportWith`: closed + probabilistic programs are the instance with uniform answers. + +## References + +The design follows Devon Tuma, Quang Dao, and collaborators' +[VCVio](https://github.com/Verified-zkEVM/VCVio), whose programs carry their distribution and +possible outputs relative to an interpretation of the oracle calls. +-/ + +@[expose] public section + +namespace Cslib + +open Probability + +namespace OracleComp + +universe u v + +variable {ι : Type u} {spec : OracleSpec.{u, v} ι} {α β : Type v} + +/-! ### Distributions for independent answers -/ + +/-- The output distribution of `program` when each call `q` is answered by an independent sample +of `h q`. -/ +noncomputable def evalWith (h : (q : ι) → PMF (spec q)) (program : OracleComp spec α) : PMF α := + interpret h program + +section EvalWith + +variable (h : (q : ι) → PMF (spec q)) + +/-- A returned value has a point distribution. -/ +@[simp] theorem evalWith_pure (a : α) : evalWith h (pure a : OracleComp spec α) = PMF.pure a := + rfl + +/-- Evaluating a sequence draws a result of the first program and evaluates the continuation at +it. -/ +@[simp] theorem evalWith_bind (program : OracleComp spec α) (next : α → OracleComp spec β) : + evalWith h (program >>= next) = (evalWith h program).bind fun a => evalWith h (next a) := + interpret_bind _ _ _ + +/-- Postprocessing maps the distribution. -/ +@[simp] theorem evalWith_map (f : α → β) (program : OracleComp spec α) : + evalWith h (f <$> program) = (evalWith h program).map f := + interpret_map _ _ _ + +/-- A single call has the distribution of its answer. -/ +@[simp] theorem evalWith_query (q : ι) : evalWith h (query (spec := spec) q) = h q := + interpret_query _ _ + +/-- Evaluation is a monad morphism into `PMF`. -/ +theorem isMonadHom_evalWith : IsMonadHom (OracleComp spec) PMF (evalWith h) := + PFunctor.FreeM.isMonadHom_liftM (P := ⟨ι, spec⟩) h + +end EvalWith + +/-- Evaluating a program whose calls were replaced by programs over another interface evaluates +the original calls by the distributions of their replacements. -/ +theorem evalWith_interpret {κ : Type u} {target : OracleSpec.{u, v} κ} + (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 := + interpret_interpret _ _ _ + +/-! ### Possible results -/ + +/-- 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. -/ +def supportWith (possible : (q : ι) → Set (spec q)) : OracleComp spec α → Set α + | .pure a => {a} + | .liftBind q cont => ⋃ a ∈ possible q, supportWith possible (cont a) + +section SupportWith + +variable (possible : (q : ι) → Set (spec q)) + +/-- A returned value is the only possible result. -/ +@[simp] theorem supportWith_pure (a : α) : + supportWith possible (pure a : OracleComp spec α) = {a} := + rfl + +variable {possible} in +/-- A possible result of a sequence is a possible result of a continuation at a possible first +result. -/ +@[simp] theorem mem_supportWith_bind_iff {program : OracleComp spec α} + {next : α → OracleComp spec β} {b : β} : + b ∈ supportWith possible (program >>= next) ↔ + ∃ a ∈ supportWith possible program, b ∈ supportWith possible (next a) := by + induction program with + | pure a => + constructor + · exact fun hb => ⟨a, rfl, hb⟩ + · rintro ⟨a', rfl, hb⟩ + exact hb + | liftBind q cont ih => + change b ∈ ⋃ x ∈ possible q, supportWith possible (cont x >>= next) ↔ + ∃ a ∈ ⋃ x ∈ possible q, supportWith possible (cont x), _ + simp only [Set.mem_iUnion, exists_prop, ih] + constructor + · rintro ⟨x, hx, a, ha, hb⟩ + exact ⟨a, ⟨x, hx, ha⟩, hb⟩ + · rintro ⟨a, ⟨x, hx, ha⟩, hb⟩ + exact ⟨x, hx, a, ha, hb⟩ + +/-- The possible results of a sequence, as a union over the possible first results. -/ +theorem supportWith_bind (program : OracleComp spec α) (next : α → OracleComp spec β) : + supportWith possible (program >>= next) = + ⋃ a ∈ supportWith possible program, supportWith possible (next a) := by + ext b + simp only [mem_supportWith_bind_iff, Set.mem_iUnion, exists_prop] + +variable {possible} in +/-- A possible mapped result is the image of a possible result. -/ +@[simp] theorem mem_supportWith_map_iff {f : α → β} {program : OracleComp spec α} {b : β} : + b ∈ supportWith possible (f <$> program) ↔ ∃ a ∈ supportWith possible program, f a = b := by + rw [← bind_pure_comp, mem_supportWith_bind_iff] + simp only [supportWith_pure, Set.mem_singleton_iff, eq_comm] + +/-- The possible results of a mapped program are the image of its possible results. -/ +theorem supportWith_map (f : α → β) (program : OracleComp spec α) : + supportWith possible (f <$> program) = f '' supportWith possible program := by + ext b + simp only [mem_supportWith_map_iff, Set.mem_image] + +/-- A single call may return any of its possible answers. -/ +@[simp] theorem supportWith_query (q : ι) : + supportWith possible (query (spec := spec) q) = possible q := + Set.biUnion_of_singleton (possible q) + +end SupportWith + +/-- Allowing more answers allows more results. -/ +theorem supportWith_mono {possible possible' : (q : ι) → Set (spec q)} + (hpossible : ∀ q, possible q ⊆ possible' q) (program : OracleComp spec α) : + supportWith possible program ⊆ supportWith possible' program := by + induction program using OracleComp.induction with + | pure a => exact subset_rfl + | query_bind q cont ih => + intro b hb + obtain ⟨a, ha, hb⟩ := mem_supportWith_bind_iff.mp hb + rw [supportWith_query] at ha + exact mem_supportWith_bind_iff.mpr + ⟨a, by rw [supportWith_query]; exact hpossible q ha, ih a hb⟩ + +/-- 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 supportWith_interpret {κ : Type u} {target : OracleSpec.{u, v} κ} + (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 := by + induction program using OracleComp.induction with + | pure a => rfl + | query_bind q cont ih => + ext b + simp only [interpret_bind, interpret_query, mem_supportWith_bind_iff, supportWith_query, ih] + +/-! ### Evaluation and support -/ + +/-- The results with positive probability are the results reached along answers with positive +probability. -/ +theorem support_evalWith (h : (q : ι) → PMF (spec q)) (program : OracleComp spec α) : + (evalWith h program).support = supportWith (fun q => (h q).support) program := by + induction program using OracleComp.induction with + | pure a => simp only [evalWith_pure, PMF.support_pure, supportWith_pure] + | query_bind q cont ih => + ext b + simp only [evalWith_bind, evalWith_query, PMF.mem_support_bind_iff, + mem_supportWith_bind_iff, supportWith_query, ih] + +/-! ### Stateful oracles -/ + +section RunWith + +variable {σ : Type v} (oracle : (q : ι) → StateT σ PMF (spec q)) + +/-- The joint law of the result of `program` and the final state of the stateful oracle answering +its calls, starting from the state `s`. -/ +noncomputable def runWith (program : OracleComp spec α) (s : σ) : PMF (α × σ) := + (interpret oracle program).run s + +/-- A returned value leaves the state unchanged. -/ +@[simp] theorem runWith_pure (a : α) (s : σ) : + runWith oracle (pure a : OracleComp spec α) s = PMF.pure (a, s) := + rfl + +/-- Running a sequence runs the first program, then the continuation at its result from the state +it reached. -/ +@[simp] theorem runWith_bind (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 := + run_interpret_bind _ _ _ _ + +/-- Postprocessing maps the result and keeps the final state. -/ +@[simp] theorem runWith_map (f : α → β) (program : OracleComp spec α) (s : σ) : + runWith oracle (f <$> program) s = (runWith oracle program s).map (Prod.map f id) := + run_interpret_map _ _ _ _ + +/-- A single call is answered by the oracle from the current state. -/ +@[simp] theorem runWith_query (q : ι) (s : σ) : + runWith oracle (query (spec := spec) q) s = oracle q s := + run_interpret_query _ _ _ + +/-- 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`. -/ +theorem mem_supportWith_of_mem_support_runWith {possible : (q : ι) → Set (spec q)} + (hpossible : ∀ q s a 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 := by + induction program using OracleComp.induction generalizing s s' with + | pure b => + rw [runWith_pure, PMF.mem_support_pure_iff, Prod.mk.injEq] at h + exact h.1 + | query_bind q cont ih => + rw [runWith_bind, runWith_query, PMF.mem_support_bind_iff] at h + obtain ⟨⟨b, middle⟩, hb, h⟩ := h + exact mem_supportWith_bind_iff.mpr + ⟨b, by rw [supportWith_query]; exact hpossible q s b middle hb, ih b h⟩ + +end RunWith + +/-- A memoryless oracle run with state leaves the state unchanged, and the result has the law of +`evalWith`. -/ +@[simp] theorem runWith_lift {σ : Type v} (h : (q : ι) → PMF (spec q)) + (program : OracleComp spec α) (s : σ) : + runWith (fun q => StateT.lift (h q)) program s = (evalWith h program).map (·, s) := + run_interpret_lift h program s + +/-! ### Sums of interfaces -/ + +section Sum + +variable {ι₁ ι₂ : Type u} {spec₁ : OracleSpec.{u, v} ι₁} {spec₂ : OracleSpec.{u, v} ι₂} + +/-- An embedded left program is evaluated by the left handler alone. -/ +@[simp] theorem evalWith_sumHandler_liftLeft (left : (q : ι₁) → PMF (spec₁ q)) + (right : (q : ι₂) → PMF (spec₂ q)) (program : OracleComp spec₁ α) : + evalWith (sumHandler left right) (liftLeft program) = evalWith left program := + interpret_sumHandler_liftLeft _ _ _ + +/-- An embedded right program is evaluated by the right handler alone. -/ +@[simp] theorem evalWith_sumHandler_liftRight (left : (q : ι₁) → PMF (spec₁ q)) + (right : (q : ι₂) → PMF (spec₂ q)) (program : OracleComp spec₂ α) : + evalWith (sumHandler left right) (liftRight program) = evalWith right program := + interpret_sumHandler_liftRight _ _ _ + +/-- Evaluation distributes over the two sides of a handler by programs. -/ +theorem evalWith_sumHandler {κ : Type u} {target : OracleSpec.{u, v} κ} + (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)) := + interpret_sumHandler h left right + +/-- The supports of the answers of a sum handler are the sum of the supports. -/ +theorem support_sumHandler (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) := by + funext q + cases q <;> rfl + +/-- An embedded left program has the possible results allowed by the left answers alone. -/ +@[simp] theorem supportWith_sumHandler_liftLeft (left : (q : ι₁) → Set (spec₁ q)) + (right : (q : ι₂) → Set (spec₂ q)) (program : OracleComp spec₁ α) : + supportWith (sumHandler left right) (liftLeft program) = supportWith left program := by + rw [liftLeft, supportWith_interpret] + congr 1 + funext q + exact supportWith_query _ _ + +/-- An embedded right program has the possible results allowed by the right answers alone. -/ +@[simp] theorem supportWith_sumHandler_liftRight (left : (q : ι₁) → Set (spec₁ q)) + (right : (q : ι₂) → Set (spec₂ q)) (program : OracleComp spec₂ α) : + supportWith (sumHandler left right) (liftRight program) = supportWith right program := by + rw [liftRight, supportWith_interpret] + congr 1 + funext q + exact supportWith_query _ _ + +/-- An embedded left program is run by the left oracle alone, which keeps the whole state. -/ +@[simp] theorem runWith_sumHandler_liftLeft {σ : Type v} + (left : (q : ι₁) → StateT σ PMF (spec₁ q)) (right : (q : ι₂) → StateT σ PMF (spec₂ q)) + (program : OracleComp spec₁ α) (s : σ) : + runWith (sumHandler left right) (liftLeft program) s = runWith left program s := + congrArg (StateT.run · s) (interpret_sumHandler_liftLeft left right program) + +/-- An embedded right program is run by the right oracle alone, which keeps the whole state. -/ +@[simp] theorem runWith_sumHandler_liftRight {σ : Type v} + (left : (q : ι₁) → StateT σ PMF (spec₁ q)) (right : (q : ι₂) → StateT σ PMF (spec₂ q)) + (program : OracleComp spec₂ α) (s : σ) : + runWith (sumHandler left right) (liftRight program) s = runWith right program s := + congrArg (StateT.run · s) (interpret_sumHandler_liftRight left right program) + +end Sum + +end OracleComp + +namespace ProbComp + +variable {α : Type} + +/-- Evaluating a closed probabilistic program is `evalWith` of the uniform handler. -/ +theorem eval_eq_evalWith (program : ProbComp α) : + eval program = OracleComp.evalWith unifOracle program := + rfl + +/-- The possible results of a closed probabilistic program are its results for any replies, since +every uniform reply has positive probability. -/ +theorem support_eval_eq_supportWith (program : ProbComp α) : + (eval program).support = OracleComp.supportWith (fun _ => Set.univ) program := by + rw [eval_eq_evalWith, OracleComp.support_evalWith] + congr 1 + funext n + exact Set.eq_univ_of_forall fun a => by simp [unifOracle, PMF.mem_support_iff] + +end ProbComp + +end Cslib diff --git a/ComplexityTests.lean b/ComplexityTests.lean index e38644354f..b72a7609b2 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -287,6 +287,7 @@ import ComplexityTests.OracleLowness import ComplexityTests.OraclePPT import ComplexityTests.OracleReplay import ComplexityTests.OracleRepresentation +import ComplexityTests.OracleSemantics import ComplexityTests.OracleSpecSum import ComplexityTests.OrderedAddition import ComplexityTests.OrderedBitSum diff --git a/ComplexityTests/OracleSemantics.lean b/ComplexityTests/OracleSemantics.lean new file mode 100644 index 0000000000..12567cee39 --- /dev/null +++ b/ComplexityTests/OracleSemantics.lean @@ -0,0 +1,89 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +import Complexity.Languages.Probabilistic.Oracle.Interaction +import Complexity.Languages.Probabilistic.Oracle.Support + +/-! # One semantics for oracle programs -/ + +namespace ComplexityTests.OracleSemantics + +open Cslib OracleComp + +/-- Two calls to a Boolean interface. -/ +private def twoCalls : OracleComp (fun _ : Unit => Bool) Bool := do + let a ← query () + let b ← query () + return a && !b + +-- A deterministic handler gives a point distribution. +example : evalWith (fun _ => PMF.pure true) twoCalls = PMF.pure false := by + simp [twoCalls] + +-- When every call must answer `true`, the only possible result is `false`. +example : supportWith (fun _ => {true}) twoCalls = {false} := by + ext b + simp [twoCalls, eq_comm] + +-- With fair answers, `true` has positive probability: evaluation and support agree. +example : true ∈ (evalWith (fun _ => Probability.PMF.uniformOfFintype Bool) twoCalls).support := by + rw [support_evalWith] + simp only [twoCalls, mem_supportWith_bind_iff, supportWith_query, supportWith_pure, + Set.mem_singleton_iff] + exact ⟨true, by simp [PMF.mem_support_iff], false, by simp [PMF.mem_support_iff], rfl⟩ + +-- A stateful oracle counting its calls. +private noncomputable def counter : (q : Unit) → StateT ℕ PMF Bool := + fun _ s => PMF.pure (true, s + 1) + +example : runWith counter twoCalls 0 = PMF.pure (false, 2) := by + simp [twoCalls, counter] + +-- Every result of the counting run is reached along a `true` reply. +example {result : Bool} {final : ℕ} (h : (result, final) ∈ (runWith counter twoCalls 0).support) : + result ∈ supportWith (fun _ => {true}) twoCalls := + mem_supportWith_of_mem_support_runWith counter + (fun _ _ _ _ h => by + simp only [counter, PMF.mem_support_pure_iff, Prod.mk.injEq] at h + exact h.1) h + +-- A memoryless oracle run with state keeps the state. +example (s : ℕ) : + runWith (fun _ => StateT.lift (PMF.pure true)) twoCalls s = + PMF.pure (false, s) := by + rw [runWith_lift] + simp [twoCalls] + +-- Closed probabilistic programs are the instance with uniform answers. +example (program : ProbComp Bool) : + ProbComp.eval program = evalWith ProbComp.unifOracle program := + ProbComp.eval_eq_evalWith program + +example : (ProbComp.eval (ProbComp.unifFin 1)).support = Set.univ := by + rw [ProbComp.support_eval_eq_supportWith, ProbComp.unifFin, supportWith_query] + +/-- A program with a private coin and one external call. -/ +private noncomputable def coinThenQuery : ProbOracleComp (fun _ : Unit => Bool) Bool := do + let coin ← ProbOracleComp.sample (ProbComp.uniform Bool) + let reply ← ProbOracleComp.query () + return coin && reply + +-- Its possible results are the generic ones for all replies. +example : ProbOracleComp.support coinThenQuery = supportWith (fun _ => Set.univ) coinThenQuery := + ProbOracleComp.support_eq_supportWith coinThenQuery + +-- Its run is the generic run of the sum handler. +example (oracle : (q : Unit) → StateT ℕ PMF Bool) (s : ℕ) : + ProbOracleComp.runWith oracle coinThenQuery s = + runWith (sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) oracle) coinThenQuery s := + ProbOracleComp.runWith_eq_runWith_sumHandler oracle coinThenQuery s + +-- Against a reply that is always `false`, it never accepts. +example (s : ℕ) : + ProbOracleComp.acceptProbWith (fun _ => StateT.lift (PMF.pure false)) coinThenQuery s = 0 := by + rw [ProbOracleComp.acceptProbWith_lift] + simp [coinThenQuery, ProbOracleComp.sample_eq_liftLeft, ProbOracleComp.query] + +end ComplexityTests.OracleSemantics