feat(probabilistic): one semantics for OracleComp

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

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

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,13 +21,20 @@ 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.
 * `Cslib.ProbOracleComp.acceptProbWith`: the acceptance probability.
 
 ## 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 _ _ _

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