Documentation

Complexity.Languages.Probabilistic.Oracle.Interaction

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

Main definitions #

Main results #

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

Instances For
    source
    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.

    Instances For
      source
      @[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.

      source
      @[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.

      source
      @[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.

      source
      @[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.

      source
      @[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.

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

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

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

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

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

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