Running a program against a stateful oracle

A program with private samples and typed external calls (Cslib.ProbOracleComp) interacts with a stateful probabilistic oracle answering each call q with an element of spec q, possibly at random and updating a private state. Cslib.ProbOracleComp.runWith is the joint law of the result and the final oracle state, with fresh fair samples for the private coins, and Cslib.ProbOracleComp.acceptProbWith the probability that a Boolean program returns true. 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 OracleComp.sumHandler of fresh uniform draws for private samples, which keep the state, and oracle for external calls. Against a memoryless oracle it is OracleComp.evalWith of the sum of the uniform handler and the oracle, with the state unchanged (runWith_lift). Its structural rules are those of OracleComp.runWith; Languages.Probabilistic.Oracle.Simulation gives its simulation and state-representation rules.

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_lift, Cslib.ProbOracleComp.acceptProbWith_lift: against a memoryless oracle, the instances of OracleComp.evalWith.
• Cslib.ProbOracleComp.induction: structural induction over returned values, private uniform draws and external calls; Cslib.ProbOracleComp.sample_unifFin identifies a draw with its sampling request.
• Cslib.ProbOracleComp.runWith_pure, Cslib.ProbOracleComp.runWith_bind, Cslib.ProbOracleComp.runWith_map, Cslib.ProbOracleComp.runWith_query, Cslib.ProbOracleComp.runWith_sample: structural rules for runWith.
• Cslib.ProbOracleComp.eval_run_interpret_eq_runWith: evaluating a closed run is runWith against the evaluated handler.
• Cslib.ProbOracleComp.runWith_sample_bind: a private sample averages the continuation's run; Cslib.ProbOracleComp.runWith_sample_bind_congr exchanges samples with the same law, and Cslib.ProbOracleComp.runWith_sample_bind_comm moves a sample past any program.
• Cslib.ProbOracleComp.runWith_interpret, Cslib.ProbOracleComp.runWith_interpret_sumHandler: running an interpreted program runs the original program against the handler programs' runs.
• Cslib.ProbOracleComp.acceptProbWith_bind: sequencing for acceptance probability.
• Cslib.ProbOracleComp.acceptProbWith_query_bind, Cslib.ProbOracleComp.acceptProbWith_sample_bind: averages over replies and samples.
• Cslib.ProbOracleComp.acceptProbWith_bind_ite_le: a check run only after another one accepted accepts at most as often.

theorem Cslib.ProbOracleComp.sample_unifFin {Query : Type} {spec : Query → Type} (n : ℕ) : sample (ProbComp.unifFin n) = OracleComp.query (Sum.inl n)

A private uniform draw is the sampling request that it embeds.

theorem Cslib.ProbOracleComp.induction {Query : Type} {spec : Query → Type} {α : Type} {motive : ProbOracleComp spec α → Prop} (pure : ∀ (a : α), motive (pure a)) (sample_bind : ∀ (n : ℕ) (cont : Fin (n + 1) → ProbOracleComp spec α), (∀ (i : Fin (n + 1)), motive (cont i)) → motive (sample (ProbComp.unifFin n) >>= cont)) (query_bind : ∀ (q : Query) (cont : spec q → ProbOracleComp spec α), (∀ (a : spec q), motive (cont a)) → motive (query q >>= cont)) (program : ProbOracleComp spec α) : motive program

Structural induction on a program with private samples and external calls: a returned value, a private uniform draw followed by a continuation, or an external call followed by a continuation.

noncomputable def Cslib.ProbOracleComp.runWith {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbOracleComp spec α) (s : State) : PMF (α × State)

The joint law of the result of program and the final state of the oracle answering its external calls, starting from the state s. Private samples are fresh. This is the generic stateful run OracleComp.runWith of the sum handler.

noncomputable def Cslib.ProbOracleComp.acceptProbWith {Query : Type} {spec : Query → Type} {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbOracleComp spec Bool) (s : State) : ENNReal

The probability that program returns true against the oracle from the state s.

theorem Cslib.ProbOracleComp.runWith_lift {Query : Type} {spec : Query → Type} {State α : Type} (h : (q : Query) → PMF (spec q)) (program : ProbOracleComp spec α) (s : State) : runWith (fun (q : Query) => StateT.lift (h q)) program s = PMF.map (fun (x : α) => (x, s)) (OracleComp.evalWith (OracleComp.sumHandler ProbComp.unifOracle h) program)

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 Cslib.ProbOracleComp.acceptProbWith_lift {Query : Type} {spec : Query → Type} {State : Type} (h : (q : Query) → PMF (spec q)) (program : ProbOracleComp spec Bool) (s : State) : acceptProbWith (fun (q : Query) => StateT.lift (h q)) program s = (OracleComp.evalWith (OracleComp.sumHandler ProbComp.unifOracle h) program) true

Against a memoryless oracle, the acceptance probability is the probability of true under OracleComp.evalWith of the uniform handler and the oracle.

@[simp]

theorem Cslib.ProbOracleComp.runWith_pure {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (a : α) (s : State) : runWith oracle (pure a) s = PMF.pure (a, s)

A pure program returns its value and leaves the oracle state unchanged.

@[simp]

theorem Cslib.ProbOracleComp.runWith_bind {Query : Type} {spec : Query → Type} {State α β : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbOracleComp spec α) (next : α → ProbOracleComp spec β) (s : State) : runWith oracle (program >>= next) s = (runWith oracle program s).bind fun (x : α × State) => runWith oracle (next x.1) x.2

Running program >>= next runs program, then runs next at its result from the oracle state it reached.

@[simp]

theorem Cslib.ProbOracleComp.runWith_map {Query : Type} {spec : Query → Type} {State α β : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (f : α → β) (program : ProbOracleComp spec α) (s : State) : runWith oracle (f <$> program) s = PMF.map (Prod.map f id) (runWith oracle program s)

Mapping f over a program maps it over the result and keeps the final oracle state.

@[simp]

theorem Cslib.ProbOracleComp.runWith_query {Query : Type} {spec : Query → Type} {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (q : Query) (s : State) : runWith oracle (query q) s = oracle q s

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

@[simp]

theorem Cslib.ProbOracleComp.runWith_sample {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbComp α) (s : State) : runWith oracle (sample program) s = PMF.map (fun (x : α) => (x, s)) program.eval

A private sample has the law of the sampled program and leaves the oracle state unchanged.

theorem Cslib.ProbOracleComp.runWith_sample_bind {Query : Type} {spec : Query → Type} {State α β : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbComp α) (next : α → ProbOracleComp spec β) (s : State) : runWith oracle (sample program >>= next) s = program.eval.bind fun (a : α) => runWith oracle (next a) s

A private sample followed by a continuation averages the continuation's run over the sample, from the same oracle state.

theorem Cslib.ProbOracleComp.runWith_sample_bind_congr {Query : Type} {spec : Query → Type} {State α β : Type} (oracle : (q : Query) → StateT State PMF (spec q)) {program program' : ProbComp α} (h : program.eval = program'.eval) (next : α → ProbOracleComp spec β) (s : State) : runWith oracle (sample program >>= next) s = runWith oracle (sample program' >>= next) s

Private samples with the same law can be exchanged in front of any continuation.

theorem Cslib.ProbOracleComp.runWith_sample_bind_comm {Query : Type} {spec : Query → Type} {State α β : Type} (oracle : (q : Query) → StateT State PMF (spec q)) {γ : Type} (program : ProbComp α) (other : ProbOracleComp spec β) (next : α → β → ProbOracleComp spec γ) (s : State) : runWith oracle (do let a ← sample program let b ← other next a b) s = runWith oracle (do let b ← other let a ← sample program next a b) s

A private sample commutes with any program: since the draw neither reads nor changes the oracle state, drawing it before or after the program gives the same run.

theorem Cslib.ProbOracleComp.runWith_interpret {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State PMF (spec q)) {ι : Type} {spec' : OracleSpec ι} (handler : (q : ι) → ProbOracleComp spec (spec' q)) (program : OracleComp spec' α) (s : State) : runWith oracle (OracleComp.interpret handler program) s = OracleComp.runWith (fun (q : ι) => runWith oracle (handler q)) program s

Running a program whose calls a handler answers with ProbOracleComp spec programs is a stateful run of the original program, each call answered by running its handler program.

theorem Cslib.ProbOracleComp.runWith_interpret_sumHandler {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State PMF (spec q)) {Query' : Type} {spec' : Query' → Type} (handler : (q : Query') → ProbOracleComp spec (spec' q)) (program : ProbOracleComp spec' α) (s : State) : runWith oracle (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => sample (ProbComp.unifFin n)) handler) program) s = runWith (fun (q : Query') => runWith oracle (handler q)) program s

A program whose private draws are forwarded and whose external calls a handler answers with ProbOracleComp spec programs runs against the oracle that runs each handler program.

theorem Cslib.ProbOracleComp.eval_run_interpret_eq_runWith {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State ProbComp (spec q)) (program : ProbOracleComp spec α) (s : State) : ((OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) oracle) program).run s).eval = runWith (fun (q : Query) (state : State) => (oracle q state).eval) program s

Evaluating a closed run, in which a handler program answers the external calls, is runWith against the evaluated handler.

theorem Cslib.ProbOracleComp.acceptProbWith_pure {Query : Type} {spec : Query → Type} {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (b : Bool) (s : State) : acceptProbWith oracle (pure b) s = if b = true then 1 else 0

A pure program accepts with probability 1 if it returns true and 0 otherwise.

theorem Cslib.ProbOracleComp.acceptProbWith_le_one {Query : Type} {spec : Query → Type} {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbOracleComp spec Bool) (s : State) : acceptProbWith oracle program s ≤ 1

An acceptance probability is at most 1.

theorem Cslib.ProbOracleComp.acceptProbWith_bind {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbOracleComp spec α) (next : α → ProbOracleComp spec Bool) (s : State) : acceptProbWith oracle (program >>= next) s = ∑' (x : α × State), (runWith oracle program s) x * acceptProbWith oracle (next x.1) x.2

The acceptance probability of program >>= next averages the acceptance probability of next over the joint law of the result and oracle state of program.

theorem Cslib.ProbOracleComp.acceptProbWith_query_bind {Query : Type} {spec : Query → Type} {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (q : Query) (next : spec q → ProbOracleComp spec Bool) (s : State) : acceptProbWith oracle (query q >>= next) s = ∑' (x : spec q × State), (oracle q s) x * acceptProbWith oracle (next x.1) x.2

The acceptance probability after an external call q averages over the oracle's replies and next states.

theorem Cslib.ProbOracleComp.acceptProbWith_sample_bind {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbComp α) (next : α → ProbOracleComp spec Bool) (s : State) : acceptProbWith oracle (sample program >>= next) s = ∑' (a : α), program.eval a * acceptProbWith oracle (next a) s

The acceptance probability after a private sample averages over the law of the sample, with the oracle state unchanged.

theorem Cslib.ProbOracleComp.acceptProbWith_bind_ite_le {Query : Type} {spec : Query → Type} {State : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program next : ProbOracleComp spec Bool) (s : State) : acceptProbWith oracle (do let b ← program if b = true then next else pure false) s ≤ acceptProbWith oracle program s

Running a second check only after a first one accepted accepts at most as often as the first check.