The optimal prover against private coins

Fixing the private coins of a verifier leaves a deterministic program making word requests (Cslib.Complexity.WordQueryComp). A verifier whose coins range over a finite set R is thus a family F : R → WordQueryComp Unit Bool of such programs, one for every value of the coins, and a prover interacting with the verifier interacts with F r for a uniformly random r that it does not see. It sees only the messages, so after a history of messages and replies (Cslib.Complexity.Interaction.History) the coin values still in play are those of the programs that sent exactly the messages of the history; what remains of each of them is Cslib.Complexity.Interaction.after.

The value of a history (Cslib.Complexity.Interaction.value) counts the programs that accept on it, plus, for every next message, the best value over the replies. The best reply cannot depend on the coins: it is chosen once for all the programs sending that message. Sums and maxima range over the words of length at most L (Cslib.BitString.shortWords), which suffices for a bounded family (Cslib.Complexity.Interaction.IsBounded): every program makes at most D requests, every message has length at most L, and only the first L bits of a reply matter.

For a bounded family, the value of the empty history is the largest number of accepting programs in expectation over the provers: every prover, randomized and stateful, is accepted on average over r with probability at most the value divided by the number of coin values (Cslib.Complexity.Interaction.sum_acceptFrom_le_value), and the deterministic prover that answers every history with a best reply (Cslib.Complexity.Interaction.optimalProver) attains it (Cslib.Complexity.Interaction.sum_acceptFrom_optimalProver). This is the optimal prover of the proof of IP ⊆ PSPACE Arora and Barak, Chapter 8 Sipser, Section 10.4.

The outcome of a program on a history (Cslib.Complexity.Interaction.outcome) is also its run against the history as a replay (Cslib.Complexity.Interaction.outcome_eq_replay), which is how a deterministic machine evaluates it.

Main definitions

• Cslib.Complexity.Interaction.History, Cslib.Complexity.Interaction.after, Cslib.Complexity.Interaction.outcome: histories and what remains of a program after them.
• Cslib.Complexity.Interaction.acceptFrom: the probability that a prover accepts from a state.
• Cslib.Complexity.Interaction.value: the value of a history.
• Cslib.Complexity.Interaction.IsBounded: bounds on rounds, messages and the replies read.
• Cslib.Complexity.Interaction.optimalProver: the prover answering with best replies.
• Cslib.Complexity.Interaction.replay: a run against a history.

Main results

• Cslib.Complexity.Interaction.sum_acceptFrom_le_value: no prover beats the value.
• Cslib.Complexity.Interaction.sum_acceptFrom_optimalProver: the optimal prover attains it.
• Cslib.Complexity.Interaction.value_le_card: the value is at most the number of coin values.
• Cslib.Complexity.Interaction.outcome_eq_replay: outcomes are replays.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• M. Sipser, Introduction to the Theory of Computation

Histories

@[reducible, inline]

abbrev Cslib.Complexity.Interaction.History : Type

A history of an interaction: the messages of the verifier, each with the reply of the prover, in order.

def Cslib.Complexity.Interaction.after {α : Type} : WordQueryComp Unit α → History → Option (WordQueryComp Unit α)

What remains of the program p after the history h, if p sends exactly the messages of h when it receives its replies.

@[simp]

theorem Cslib.Complexity.Interaction.after_nil {α : Type} (p : WordQueryComp Unit α) : after p [] = some p

@[simp]

theorem Cslib.Complexity.Interaction.after_pure_cons {α : Type} (a : α) (x : List Bool × List Bool) (h : History) : after (pure a) (x :: h) = none

theorem Cslib.Complexity.Interaction.after_query_bind_cons {α : Type} (m : List Bool) (next : List Bool → WordQueryComp Unit α) (m' y : List Bool) (h : History) : after (OracleComp.query ((), m) >>= next) ((m', y) :: h) = if m' = m then after (next y) h else none

theorem Cslib.Complexity.Interaction.after_append {α : Type} (p : WordQueryComp Unit α) (h e : History) : after p (h ++ e) = (after p h).bind fun (x : WordQueryComp Unit α) => after x e

What remains after a concatenation is what remains of what remains.

inductive Cslib.Complexity.Interaction.Outcome : Type

The outcome of a program after a history: it has finished with a result, it sends a message, or it does not send the messages of the history.

• done (result : Bool) : Outcome

  The program has finished with this result.

• ask (message : List Bool) : Outcome

  The program sends this message.

• invalid : Outcome

  The program does not send the messages of the history.

def Cslib.Complexity.Interaction.instDecidableEqOutcome.decEq (x✝ x✝¹ : Outcome) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.Interaction.instDecidableEqOutcome : DecidableEq Outcome

def Cslib.Complexity.Interaction.outcome (p : WordQueryComp Unit Bool) (h : History) : Outcome

The outcome of p after the history h.

Acceptance against a prover

noncomputable def Cslib.Complexity.Interaction.acceptFrom {Operation : Type} (P : Prover Operation) (s : P.State) : Option (WordQueryComp Operation Bool) → ENNReal

The probability that the prover P, from its state s, makes what remains of a program accept; 0 when nothing remains.

@[simp]

theorem Cslib.Complexity.Interaction.acceptFrom_none {Operation : Type} (P : Prover Operation) (s : P.State) : acceptFrom P s none = 0

The value of a history

def Cslib.Complexity.Interaction.accepted {R : Type} [Fintype R] (F : R → WordQueryComp Unit Bool) (h : History) : ℕ

The number of coin values whose programs accept after the history h.

noncomputable def Cslib.Complexity.Interaction.value {R : Type} [Fintype R] (F : R → WordQueryComp Unit Bool) (L : ℕ) : ℕ → History → ℕ

The value of the history h with n rounds to go: the accepting programs, plus, for every next message of length at most L, the best value over the replies of length at most L.

structure Cslib.Complexity.Interaction.IsBounded {R : Type} (F : R → WordQueryComp Unit Bool) (D L : ℕ) : Prop

A family of programs makes at most D requests, sends messages of length at most L, and reads only the first L bits of each reply.

• rounds (r : R) (h : History) (m : List Bool) : outcome (F r) h = Outcome.ask m → List.length h < D

  Every program has finished after D messages.

• message (r : R) (h : History) (m : List Bool) : outcome (F r) h = Outcome.ask m → m.length ≤ L

  Every message has length at most L.

• reply (r : R) (h : List (List Bool × List Bool)) (m y : List Bool) (e : List (List Bool × List Bool)) : outcome (F r) (h ++ (m, y) :: e) = outcome (F r) (h ++ (m, List.take L y) :: e)

  Only the first L bits of a reply matter.

theorem Cslib.Complexity.Interaction.value_congr {R : Type} [Fintype R] {F : R → WordQueryComp Unit Bool} {L : ℕ} {h h' : History} (hh : ∀ (r : R) (e : History), outcome (F r) (h ++ e) = outcome (F r) (h' ++ e)) (n : ℕ) : value F L n h = value F L n h'

The value of a history depends only on the outcomes of its extensions.

theorem Cslib.Complexity.Interaction.value_le_card {R : Type} [Fintype R] {F : R → WordQueryComp Unit Bool} {L : ℕ} (n : ℕ) (h : History) : value F L n h ≤ {r : R | outcome (F r) h ≠ Outcome.invalid}.card

The value is at most the number of coin values whose programs follow the history.

No prover beats the value

theorem Cslib.Complexity.Interaction.sum_acceptFrom_le_value {R : Type} [Fintype R] {F : R → WordQueryComp Unit Bool} {L D : ℕ} (hF : IsBounded F D L) (P : Prover Unit) : ∑ r : R, acceptFrom P P.init (some (F r)) ≤ ↑(value F L D [])

No prover beats the value: for a bounded family, every prover makes the programs accept with probabilities summing to at most the value of the empty history.

The optimal prover

noncomputable def Cslib.Complexity.Interaction.bestReply {R : Type} [Fintype R] (F : R → WordQueryComp Unit Bool) (L n : ℕ) (h : History) (m : List Bool) : List Bool

A reply of length at most L that is best for the message m after the history h, with n rounds to go after it.

noncomputable def Cslib.Complexity.Interaction.optimalProver {R : Type} [Fintype R] (F : R → WordQueryComp Unit Bool) (L D : ℕ) : Prover Unit

The optimal prover: its state is the history so far, and it answers every message with a best reply for the rounds left of D.

theorem Cslib.Complexity.Interaction.sum_acceptFrom_optimalProver {R : Type} [Fintype R] {F : R → WordQueryComp Unit Bool} {L D : ℕ} (hF : IsBounded F D L) : ∑ r : R, acceptFrom (optimalProver F L D) (optimalProver F L D).init (some (F r)) = ↑(value F L D [])

The optimal prover attains the value: for a bounded family, it makes the programs accept with probabilities summing to the value of the empty history.

Replays

@[reducible, inline]

abbrev Cslib.Complexity.Interaction.ReplayM (α : Type) : Type

The replay monad: a history to answer from, and failure with the message sent when the history is exhausted, or with none when a message does not match the history.

def Cslib.Complexity.Interaction.replayAnswer (q : Unit × List Bool) : ReplayM (List Bool)

Answer a message from the history.

def Cslib.Complexity.Interaction.replay {α : Type} (p : WordQueryComp Unit α) : ReplayM α

Run a program against a history.

def Cslib.Complexity.Interaction.replayOutcome : Except (Option (List Bool)) (Bool × History) → Outcome

The outcome of a replay: the result when it consumed the whole history, the pending message when it ran out of history, and invalid otherwise.

theorem Cslib.Complexity.Interaction.outcome_eq_replay (p : WordQueryComp Unit Bool) (h : History) : outcome p h = replayOutcome (StateT.run (replay p) h)

Outcomes are replays.