Interactive proof classes: MA, AM, and IP

⚠️ Unreviewed by Bolton

A verifier here is a language in P — equivalently a polynomial-time predicate — applied to the encoded tuple of everything it sees, and its private coins are a uniformly random point of Fin t → Bool measured by eventProb. This keeps the definitions machine-free and auditable, in the style of Complexitylib.Classes.NP.Witness's use of pairLang.

The three classes differ in who speaks when:

• MA — Merlin sends a proof w, then Arthur flips coins and checks pair (pair x w) r. The proof cannot depend on the coins.
• AM — Arthur flips public coins r first, then Merlin answers w, and the check is on pair (pair x r) w. Merlin's answer may depend on the coins, so the existential sits inside the probability.
• IP — a Protocol runs a bounded number of rounds: the verifier's next message is a polynomial-time function of the input, its private coins and the transcript so far, and the prover replies by a ProverStrategy, which sees the transcript but never the coins. Completeness asks for one strategy that convinces the verifier; soundness quantifies over every strategy.

Main definitions

• Transcript, ProverStrategy, Protocol, Protocol.transcript, Protocol.Accepts, Protocol.acceptEvent
• MA, AM, IP

Main results

• P_subset_MA, P_subset_AM — the definitions contain P, by ignoring the proof and the coins

Conventions

Completeness 2/3 and soundness 1/3 are hard-wired, as in Complexitylib.Classes.Randomized. Message lengths are bounded by Protocol.msgLen — the prover's by ProverStrategy.Bounded, which soundness in IP quantifies over, and the verifier's by Protocol.vmsg_len. An unbounded message would blow up the transcript the polynomial-time verifier has to read, and after polynomially many rounds the verifier would no longer be polynomial in the input at all. The prover is adaptive — it is a function of the transcript, not a single witness string.

TODO

• Embed MA into IP as a one-round protocol with an empty verifier message.
• Amplification: sequential repetition and the resulting threshold robustness.
• NP ⊆ MA through the witness characterization interface, and IP ⊆ PSPACE.

Merlin–Arthur

noncomputable def Complexity.merlinEvent (V : Language) (t : ℕ) (x w : List Bool) : Finset (Fin t → Bool)

The coin strings on which the verifier V accepts input x with proof w.

Equations

• Complexity.merlinEvent V t x w = {r : Fin t → Bool | Complexity.pair (Complexity.pair x w) (Complexity.BitString.toList r) ∈ V}

def Complexity.MA : Set Language

MA (Merlin–Arthur): Merlin sends a polynomially bounded proof, and Arthur checks it with a polynomial-time predicate and polynomially many private coins, accepting a member with probability at least 2/3 and a non-member with probability at most 1/3 whatever the proof.

Equations

• One or more equations did not get rendered due to their size.

Arthur–Merlin

noncomputable def Complexity.arthurEvent (V : Language) (q t : ℕ) (x : List Bool) : Finset (Fin t → Bool)

The public coin strings that Merlin can answer: those admitting a polynomially bounded reply the verifier accepts.

Equations

• Complexity.arthurEvent V q t x = {r : Fin t → Bool | ∃ (w : List Bool), w.length ≤ q ∧ Complexity.pair (Complexity.pair x (Complexity.BitString.toList r)) w ∈ V}

def Complexity.AM : Set Language

AM (Arthur–Merlin): Arthur flips public coins first and Merlin answers them, so the existential over Merlin's reply sits inside the probability.

Equations

• One or more equations did not get rendered due to their size.

Interactive protocols

@[reducible, inline]

abbrev Complexity.Transcript : Type

The messages exchanged so far, in order: the verifier speaks on even positions and the prover on odd ones.

Equations

• Complexity.Transcript = List (List Bool)

def Complexity.ProverStrategy : Type

A prover strategy: the next message as a function of the visible transcript. The prover is adaptive and never sees the verifier's coins.

Equations

• Complexity.ProverStrategy = (Complexity.Transcript → List Bool)

def Complexity.ProverStrategy.Bounded (S : ProverStrategy) (m : ℕ) : Prop

A strategy respects a message-length bound.

Equations

• S.Bounded m = ∀ (τ : Complexity.Transcript), (S τ).length ≤ m

def Complexity.protocolView (x r : List Bool) (τ : Transcript) : List Bool

The encoded view handed to the verifier: the input, its coins, and the transcript so far.

Equations

• Complexity.protocolView x r τ = Complexity.pair (Complexity.pair x r) (Complexity.DataEncode.bitstringEncode τ)

structure Complexity.Protocol : Type

An interactive protocol: a round count, a private-coin count, a message-length bound, the verifier's next message as a polynomial-time function of the encoded input, coins and transcript, and its final verdict as a polynomial-time predicate of the same.

msgLen bounds both sides' messages: the prover's through ProverStrategy.Bounded, the verifier's through vmsg_len. Bounding the verifier is not a convenience — without it the transcript grows by a polynomial each round, so after polynomially many rounds the view, and with it the verifier's own running time, is no longer polynomial in the input.

• rounds : ℕ → ℕ

  Number of rounds, as a function of the input length.

• coins : ℕ → ℕ

  Number of private coins, as a function of the input length.

• msgLen : ℕ → ℕ

  Bound on the length of either side's messages.

• vmsg : List Bool → List Bool

  The verifier's next message, computed from pair (pair x r) ⌜τ⌝.

• vmsg_mem : self.vmsg ∈ FP

  That computation is polynomial-time.

• vmsg_len (x r : List Bool) (τ : Transcript) : (self.vmsg (protocolView x r τ)).length ≤ self.msgLen x.length

  The verifier's messages respect the length bound, so the transcript stays polynomially long however many rounds are played.

• verdict : Language

  The verifier's final verdict, on pair (pair x r) ⌜τ⌝.

• verdict_mem : self.verdict ∈ P

  That verdict is polynomial-time decidable.

@[reducible, inline]

abbrev Complexity.Protocol.view (x r : List Bool) (τ : Transcript) : List Bool

The encoded view handed to the verifier: the input, its coins, and the transcript so far.

Equations

• Complexity.Protocol.view x r τ = Complexity.protocolView x r τ

def Complexity.Protocol.transcript (prot : Protocol) (S : ProverStrategy) (x r : List Bool) : ℕ → Transcript

The transcript after n rounds of prot on input x with coins r against the strategy S: each round appends the verifier's message and then the prover's reply.

Equations

• One or more equations did not get rendered due to their size.
• prot.transcript S x r 0 = []

def Complexity.Protocol.Accepts (prot : Protocol) (S : ProverStrategy) (x r : List Bool) : Prop

The verifier accepts the completed interaction.

Equations

• prot.Accepts S x r = (Complexity.Protocol.view x r (prot.transcript S x r (prot.rounds x.length)) ∈ prot.verdict)

noncomputable def Complexity.Protocol.acceptEvent (prot : Protocol) (S : ProverStrategy) (x : List Bool) : Finset (Fin (prot.coins x.length) → Bool)

The coin strings on which the verifier accepts against S.

Equations

• prot.acceptEvent S x = {r : Fin (prot.coins x.length) → Bool | prot.Accepts S x (Complexity.BitString.toList r)}

def Complexity.IP : Set Language

IP: languages with an interactive proof system whose round count, coin count and message lengths are given by polynomials. Completeness asks for one strategy convincing the verifier with probability at least 2/3; soundness bounds every length-respecting strategy by 1/3.

The three counts are polynomials rather than merely polynomially bounded because a verifier has to know them: it must stop after the right number of rounds and read the right number of coins. An arbitrary polynomially bounded ℕ → ℕ need not be computable at all, and a protocol carrying one would let the class contain undecidable languages.

Equations

• One or more equations did not get rendered due to their size.

Elementary containments

theorem Complexity.P_subset_MA : P ⊆ MA

P ⊆ MA. Merlin sends nothing and Arthur ignores his coins.

theorem Complexity.P_subset_AM : P ⊆ AM

P ⊆ AM. Arthur's coins are irrelevant and Merlin's answer is empty.