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 draws private samples freshly and answers external calls by oracle; that 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). Its structural rules are those of OracleComp.runWith.

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.
• 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.

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.

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_eq_runWith_sumHandler {Query : Type} {spec : Query → Type} {State α : Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbOracleComp spec α) (s : State) : runWith oracle program s = OracleComp.runWith (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) program s

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 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.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.