Interactive proofs and the class IP

An interactive proof system for a problem A is an efficient probabilistic verifier exchanging messages with an all-powerful prover. On members of A some prover convinces the verifier with high probability (completeness); on non-members no prover does, except with small probability (soundness) Goldwasser, Micali and Rackoff, Arora and Barak, Definition 8.6.

A verifier is a program α → WordOracleComp Unit Bool: it draws private fair coins with ProbOracleComp.sample and sends the prover a word with ProbOracleComp.query ((), message), receiving the reply word. Every call is one round, and later messages may depend on earlier replies and coins. Its efficiency is Cslib.Probability.IsOraclePPTOn: one finite fair-coin machine with one polynomial clock realizes the verifier against every stateful oracle. The clock charges writing messages and reading reply bits but not the prover's computation, so the verifier exchanges polynomially many messages of polynomial length (Cslib.Complexity.exists_queryBounds_of_mem_IP) and reads only a polynomial part of each reply.

A Cslib.Complexity.Prover is any stateful strategy answering messages: a type of private states, an initial state, and a probabilistic response function, with no efficiency requirement. It sees the messages but not the verifier's coins, so the proofs are private-coin. As in [GMR89] provers may be randomized; Arora and Barak use deterministic provers. The provers built here are deterministic, and soundness holds against the larger class.

IP uses the thresholds 2 / 3 and 1 / 3 of Arora and Barak. NP ⊆ IP with a single message: the prover sends a certificate and the verifier checks a prefix of the reply of the certificate length, with completeness 1 and soundness 0. BPP ⊆ IP without messages. Conversely, IP ⊆ PSPACE (CslibFrontier.Computability.Complexity.Classes.IP.PSPACE).

Main definitions

• Cslib.Complexity.Prover: an unbounded stateful prover, with Prover.run the joint law of a verifier's result and the prover's final state.
• Cslib.Complexity.acceptProb: the probability that a verifier accepts against a prover.
• Cslib.Complexity.IsInteractiveProof: completeness and soundness thresholds.
• Cslib.Complexity.IP.

Main results

• Cslib.Complexity.exists_queryBounds_of_mem_IP: polynomially many rounds of polynomial length.
• Cslib.Complexity.NP_subset_IP, Cslib.Complexity.BPP_subset_IP.

References

• S. Goldwasser, S. Micali, C. Rackoff, The knowledge complexity of interactive proof systems
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

structure Cslib.Complexity.Prover (Operation : Type) : Type 1

A prover for interactive proofs: a computationally unbounded strategy answering every message (op, word) of the verifier with a reply word, possibly at random, updating a private state.

• State : Type

  The private states of the prover.

• init : self.State

  The state at the start of the interaction.

• respond : Operation × List Bool → StateT self.State PMF (List Bool)

  The reply to one message, which may read and update the state.

noncomputable def Cslib.Complexity.Prover.run {Operation α : Type} (P : Prover Operation) (program : Probability.WordOracleComp Operation α) (s : P.State) : PMF (α × P.State)

The joint law of the result of program and of the prover's final state, when program interacts with P starting from the prover state s. Private coins are fresh fair samples.

theorem Cslib.Complexity.Prover.run_eq_runWith {Operation α : Type} (P : Prover Operation) (program : Probability.WordOracleComp Operation α) (s : P.State) : P.run program s = ProbOracleComp.runWith P.respond program s

Prover.run is the run against the prover as a stateful oracle with word queries and replies.

@[simp]

theorem Cslib.Complexity.Prover.run_pure {Operation α : Type} (P : Prover Operation) (a : α) (s : P.State) : P.run (pure a) s = PMF.pure (a, s)

theorem Cslib.Complexity.Prover.run_bind {Operation α β : Type} (P : Prover Operation) (program : Probability.WordOracleComp Operation α) (next : α → Probability.WordOracleComp Operation β) (s : P.State) : P.run (program >>= next) s = (P.run program s).bind fun (x : α × P.State) => P.run (next x.1) x.2

theorem Cslib.Complexity.Prover.run_map {Operation α β : Type} (P : Prover Operation) (f : α → β) (program : Probability.WordOracleComp Operation α) (s : P.State) : P.run (f <$> program) s = PMF.map (Prod.map f id) (P.run program s)

@[simp]

theorem Cslib.Complexity.Prover.run_sample {Operation α : Type} (P : Prover Operation) (program : ProbComp α) (s : P.State) : P.run (ProbOracleComp.sample program) s = PMF.map (fun (x : α) => (x, s)) program.eval

Private coins do not involve the prover, whose state is unchanged.

@[simp]

theorem Cslib.Complexity.Prover.run_query {Operation : Type} (P : Prover Operation) (q : Operation × List Bool) (s : P.State) : P.run (ProbOracleComp.query q) s = (P.respond q).run s

A message is answered by the prover's response function.

noncomputable def Cslib.Complexity.Prover.const {Operation : Type} (reply : List Bool) : Prover Operation

The deterministic prover answering every message with reply.

noncomputable def Cslib.Complexity.acceptProb {Operation : Type} (verifier : Probability.WordOracleComp Operation Bool) (P : Prover Operation) : ENNReal

The probability that verifier accepts when interacting with the prover P.

theorem Cslib.Complexity.acceptProb_eq_acceptProbWith {Operation : Type} (verifier : Probability.WordOracleComp Operation Bool) (P : Prover Operation) : acceptProb verifier P = ProbOracleComp.acceptProbWith P.respond verifier P.init

The acceptance probability is that of the verifier against the prover as a stateful oracle, from its initial state.

theorem Cslib.Complexity.acceptProb_eq_tsum {Operation : Type} (verifier : Probability.WordOracleComp Operation Bool) (P : Prover Operation) : acceptProb verifier P = ∑' (s : P.State), (P.run verifier P.init) (true, s)

The acceptance probability sums the masses of the accepting outcomes over final states.

theorem Cslib.Complexity.acceptProb_sample_bind {Operation β : Type} (program : ProbComp β) (next : β → Probability.WordOracleComp Operation Bool) (P : Prover Operation) : acceptProb (ProbOracleComp.sample program >>= next) P = ∑' (b : β), program.eval b * acceptProb (next b) P

Private coins drawn before any message average the acceptance probabilities of the continuations.

theorem Cslib.Complexity.acceptProb_eq_zero {Operation : Type} {verifier : Probability.WordOracleComp Operation Bool} (P : Prover Operation) (h : ∀ x ∈ (P.run verifier P.init).support, x.1 = false) : acceptProb verifier P = 0

A verifier none of whose possible results accepts has acceptance probability zero.

structure Cslib.Complexity.IsInteractiveProof {Operation α : Type} (verifier : α → Probability.WordOracleComp Operation Bool) (A : Set α) (completeness soundness : ENNReal) : Prop

verifier is an interactive proof for A with completeness completeness and soundness error soundness: on every member of A some prover is accepted with probability at least completeness, and on every non-member every prover is accepted with probability at most soundness.

• complete (a : α) : a ∈ A → ∃ (P : Prover Operation), completeness ≤ acceptProb (verifier a) P
• sound (a : α) : a ∉ A → ∀ (P : Prover Operation), acceptProb (verifier a) P ≤ soundness

theorem Cslib.Complexity.IsInteractiveProof.mono {Operation α : Type} {verifier : α → Probability.WordOracleComp Operation Bool} {A : Set α} {c c' s s' : ENNReal} (h : IsInteractiveProof verifier A c s) (hc : c' ≤ c) (hs : s ≤ s') : IsInteractiveProof verifier A c' s'

Weakening the thresholds preserves an interactive proof.

def Cslib.Complexity.IP {α : Type} (enc : α ↪ List Bool) : Set (Set α)

The problems with interactive proofs whose verifiers are strict oracle PPT, with completeness 2 / 3 and soundness error 1 / 3, with respect to the encoding enc of instances.

theorem Cslib.Complexity.mem_IP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ IP enc ↔ ∃ (verifier : α → Probability.WordOracleComp Unit Bool), Probability.IsOraclePPTOn enc Turing.MultiTapeTM.encBool verifier ∧ IsInteractiveProof verifier A (2 / 3) (1 / 3)

theorem Cslib.Complexity.mem_IP_of {α : Type} {enc : α ↪ List Bool} {A : Set α} {verifier : α → Probability.WordOracleComp Unit Bool} {c s : ENNReal} (hV : Probability.IsOraclePPTOn enc Turing.MultiTapeTM.encBool verifier) (h : IsInteractiveProof verifier A c s) (hc : 2 / 3 ≤ c) (hs : s ≤ 1 / 3) : A ∈ IP enc

An efficient interactive proof with at least the class thresholds puts a problem in IP.

theorem Cslib.Complexity.exists_queryBounds_of_mem_IP {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : A ∈ IP enc) : ∃ (verifier : α → Probability.WordOracleComp Unit Bool), Probability.IsOraclePPTOn enc Turing.MultiTapeTM.encBool verifier ∧ IsInteractiveProof verifier A (2 / 3) (1 / 3) ∧ ∃ (c : ℕ) (d : ℕ), ∀ (a : α), ProbOracleComp.IsQueryBounded (verifier a) (c * ((enc a).length + 1) ^ d) ∧ ProbOracleComp.QueriesSatisfy (fun (message : Unit × List Bool) => message.2.length ≤ c * ((enc a).length + 1) ^ d) (verifier a)

An IP verifier exchanges polynomially many messages of polynomial length: one polynomial in the instance length bounds the number of messages and the length of each, against every prover.

NP ⊆ IP

def Cslib.Complexity.npVerifier {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (V : α × List Bool → Bool) (a : α) : Probability.WordOracleComp Unit Bool

The one-message interactive proof of a problem with verifier V and certificate length p: ask the prover for a certificate, read the first p (enc a).length bits of its reply, and run V on them when there are that many.

theorem Cslib.Complexity.acceptProb_npVerifier_const {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {w : List Bool} (hw : w.length = Polynomial.eval (enc a).length p) : acceptProb (npVerifier enc p V a) (Prover.const w) = if V (a, w) = true then 1 else 0

Sending a certificate of the right length makes the verifier accept exactly when V accepts the certificate.

theorem Cslib.Complexity.NP_subset_IP {α : Type} (enc : α ↪ List Bool) : NP enc ⊆ IP enc

NP ⊆ IP, with one message, completeness 1 and soundness error 0.

BPP ⊆ IP

theorem Cslib.Complexity.BPP_subset_IP {α : Type} (enc : α ↪ List Bool) : BPP enc ⊆ IP enc

BPP ⊆ IP, without messages.