IP ⊆ PSPACE

Every problem with an interactive proof is decided within polynomial space (Cslib.Complexity.IP_subset_PSPACE) Arora and Barak, Chapter 8 Sipser, Section 10.4.

The model is that of Cslib.Complexity.IP. The verifier is strict oracle PPT: one finite fair-coin oracle machine M and one clock t = c * (n + 1) ^ d, for instances encoded with n bits, realize it against every stateful prover. So the coins are private and there are at most t of them, one per instruction; the verifier sends at most t messages, each shorter than t, and reads at most the first t bits of every reply. Provers are arbitrary: randomized, stateful and computationally unbounded; they see the messages but not the coins. The thresholds are 2 / 3 and 1 / 3.

The proof computes the acceptance probability of the optimal prover exactly, as a count of coin values:

• Fixing the t coins of the run leaves programs making word requests (Cslib.Complexity.Interaction.coinFamily), and acceptance averages over the coins (Cslib.Complexity.Interaction.acceptProb_eq_sum). The programs form a bounded family (Cslib.Complexity.Interaction.isBounded_coinFamily), so the value W of the empty history (Cslib.Complexity.Interaction.value) bounds every prover by W / 2 ^ t, and the optimal prover attains it. With completeness 2 / 3 and soundness 1 / 3, an instance is a member exactly when 2 ^ t < 2 * W (Cslib.Complexity.mem_iff_two_pow_lt_value).
• W is the value of a game tree whose messages and replies are coded by the words of length t + 1 containing a true, enumerated by a binary counter (Cslib.Complexity.Interaction.image_decodeWord_iterate_firstCode, Cslib.Complexity.Interaction.gameTree_value_eq). Its leaf values count the accepting coin values, within polynomial space (Cslib.Complexity.Interaction.computableInPolySpace_countAccepts).
• The explicit-stack evaluator of the game tree (Cslib.Complexity.Interaction.evaluate) runs for 2 ^ ((t + 1) * (2 * t + 1)) steps, with at most t frames of O(t) bits each (Cslib.Complexity.Interaction.length_encEvalState_iterate_le), so it computes W within polynomial space (Cslib.Complexity.Interaction.evaluate_eq, Cslib.Complexity.Interaction.computableInPolySpace_evaluate), in exponential time.

The converse inclusion PSPACE ⊆ IP (Cslib.Complexity.PSPACE_subset_IP), and with it IP = PSPACE (Cslib.Complexity.IP_eq_PSPACE), is proved downstream in CslibFrontier.Computability.Complexity.Classes.IP.Shamir.

Main definitions

• Cslib.Complexity.Interaction.decodeWord, Cslib.Complexity.Interaction.firstCode, Cslib.Complexity.Interaction.lastCode: the codes of the short words.
• Cslib.Complexity.Interaction.leafValue: the leaf values, the accepting programs.
• Cslib.Complexity.Interaction.evalStep, Cslib.Complexity.Interaction.evaluate: the evaluation.

Main results

• Cslib.Complexity.Interaction.image_decodeWord_iterate_firstCode: the codes enumerate the short words.
• Cslib.Complexity.Interaction.gameTree_value_eq: the value is the value of the game tree.
• Cslib.Complexity.Interaction.evaluate_eq: the evaluation computes the value.
• Cslib.Complexity.Interaction.computableInPolySpace_evaluate: within polynomial space.
• Cslib.Complexity.mem_iff_two_pow_lt_value: the value decides the problem.
• Cslib.Complexity.IP_subset_PSPACE: IP ⊆ PSPACE.

References

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

Enumerating the short words

def Cslib.Complexity.Interaction.decodeWord (u : List Bool) : List Bool

The word coded by u: what follows its first true.

def Cslib.Complexity.Interaction.encodeWord (L : ℕ) (w : List Bool) : List Bool

The code of a word w of length at most L among the words of length L + 1: L - |w| zeros, a one, then w.

theorem Cslib.Complexity.Interaction.decodeWord_encodeWord (L : ℕ) (w : List Bool) : decodeWord (encodeWord L w) = w

Decoding inverts coding.

theorem Cslib.Complexity.Interaction.length_encodeWord {L : ℕ} {w : List Bool} (hw : w.length ≤ L) : (encodeWord L w).length = L + 1

The code of a word of length at most L has length L + 1.

theorem Cslib.Complexity.Interaction.length_decodeWord_le {L : ℕ} {u : List Bool} (hu : u.length = L + 1) : (decodeWord u).length ≤ L

Any word decoded from a code of length L + 1 has length at most L.

def Cslib.Complexity.Interaction.firstCode (L : ℕ) : List Bool

The first code, 1 in binary.

def Cslib.Complexity.Interaction.lastCode (L : ℕ) (u : List Bool) : Bool

Whether a code is the last one, all ones.

def Cslib.Complexity.Interaction.codeCount (L : ℕ) : ℕ

The number of codes, and of the words of length at most L.

theorem Cslib.Complexity.Interaction.image_decodeWord_iterate_firstCode {L : ℕ} : Finset.image (fun (i : ℕ) => decodeWord (BitString.increment^[i] (firstCode L))) (Finset.range (codeCount L)) = BitString.shortWords L

The codes enumerate the short words: decoding the first codeCount L codes gives every word of length at most L exactly once.

The value as a game tree

def Cslib.Complexity.Interaction.decodeHistory (hs : List (List Bool × List Bool)) : History

The history coded by a game-tree history of codes, the most recent first.

@[simp]

theorem Cslib.Complexity.Interaction.decodeHistory_nil : decodeHistory [] = []

@[simp]

theorem Cslib.Complexity.Interaction.decodeHistory_cons (p : List Bool × List Bool) (hs : List (List Bool × List Bool)) : decodeHistory (p :: hs) = decodeHistory hs ++ [(decodeWord p.1, decodeWord p.2)]

def Cslib.Complexity.Interaction.leafValue {R : Type} [Fintype R] (F : R → WordQueryComp Unit Bool) (hs : List (List Bool × List Bool)) : ℕ

The leaf value of a game-tree history: the number of accepting programs.

theorem Cslib.Complexity.Interaction.gameTree_value_eq {L : ℕ} {R : Type} [Fintype R] (F : R → WordQueryComp Unit Bool) {cap : ℕ} (hcap : Fintype.card R ≤ cap) (n : ℕ) (hs : List (List Bool × List Bool)) : GameTree.value (codeCount L) cap (firstCode L) BitString.increment (leafValue F) n hs = value F L n (decodeHistory hs)

The value is the value of the game tree of the codes of the short words, with sums capped at a bound on the number of coin values.

Polynomial-time parts

theorem Cslib.Complexity.Interaction.computableInPolyTime_decodeWord : Turing.MultiTapeTM.ComputableInPolyTime decodeWord Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

Decoding a word is polynomial-time.

The evaluation

@[reducible, inline]

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

The states of the evaluation: the instance, the stack and the value being returned.

def Cslib.Complexity.Interaction.evalStep {α : Type} (enc : α ↪ List Bool) {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) (fuel : α → ℕ) (s : EvalState α) : EvalState α

One step of the evaluation of the game tree of the verifier M on a, with fuel a coins, rounds and message lengths.

def Cslib.Complexity.Interaction.evalTime {α : Type} (fuel : α → ℕ) (a : α) : ℕ

The number of steps of the evaluation, a bound on GameTree.time.

def Cslib.Complexity.Interaction.evaluate {α : Type} (enc : α ↪ List Bool) {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) (fuel : α → ℕ) (a : α) : ℕ

The value computed by the evaluation.

theorem Cslib.Complexity.Interaction.evaluate_eq {α : Type} (enc : α ↪ List Bool) {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) (fuel : α → ℕ) (a : α) : evaluate enc M fuel a = value (coinFamily M (fuel a) (enc a)) (fuel a) (fuel a) []

The evaluation computes the value of the verifier on a.

def Cslib.Complexity.Interaction.pushStep (L : ℕ) (st : List (GameTree.Frame (List Bool))) (v : ℕ) : List (GameTree.Frame (List Bool)) × Option ℕ

Pushing a frame, or returning the leaf value at the maximal depth.

theorem Cslib.Complexity.Interaction.step_none_eq (L cap : ℕ) (leaf : List (List Bool × List Bool) → ℕ) (st : List (GameTree.Frame (List Bool))) : GameTree.step L cap (firstCode L) BitString.increment (lastCode L) leaf (st, none) = pushStep L st (min cap (leaf (GameTree.history st)))

A node without a returned value, by pushStep.

The evaluation in polynomial space

@[reducible, inline]

abbrev Cslib.Complexity.Interaction.encFrame : GameTree.Frame (List Bool) ↪ List Bool

Frames, encoded by their fields.

@[reducible, inline]

abbrev Cslib.Complexity.Interaction.encEvalState {α : Type} (enc : α ↪ List Bool) : EvalState α ↪ List Bool

States of the evaluation, encoded by their fields.

theorem Cslib.Complexity.Interaction.length_encEvalState_iterate_le {α : Type} {enc : α ↪ List Bool} {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) {fuel : α → ℕ} (a : α) (j : ℕ) : ((encEvalState enc) ((evalStep enc M fuel)^[j] (a, [], none))).length ≤ 2 * (enc a).length + 2 * fuel a * (14 * fuel a + 21) + fuel a + 4

The states of the evaluation are of polynomial size.

theorem Cslib.Complexity.Interaction.computableInPolySpace_evaluate {α : Type} {enc : α ↪ List Bool} {k : ℕ} {Control : Type} (M : Turing.MultiTapePTM k Bool Control Unit) {fuel : α → ℕ} [Finite Control] [Inhabited α] (hfuel : Turing.MultiTapeTM.ComputableInPolyTime fuel enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolySpace (evaluate enc M fuel) enc Turing.MultiTapeTM.encNat

The evaluation within polynomial space.

theorem Cslib.Complexity.mem_iff_two_pow_lt_value {α : Type} {enc : α ↪ List Bool} {k : ℕ} {Control : Type} {V : α → Probability.WordOracleComp Unit Bool} {A : Set α} {M : Turing.MultiTapePTM k Bool Control Unit} {fuel : α → ℕ} (hV : ∀ (a : α) (S : Type) (oracle : Unit × List Bool → StateT S PMF (List Bool)) (s : S), ProbOracleComp.runWith oracle (⇑Turing.MultiTapeTM.encBool <$> V a) s = ProbOracleComp.runWith oracle (M.runOracle (fuel a) (enc a)) s) (hA : IsInteractiveProof V A (2 / 3) (1 / 3)) (a : α) : a ∈ A ↔ 2 ^ fuel a < 2 * Interaction.value (Interaction.coinFamily M (fuel a) (enc a)) (fuel a) (fuel a) []

The value decides an interactive proof. If the verifier V is realized, against every stateful prover, by the run of the oracle machine M under the clock fuel a, then a member of the problem is exactly an instance on which the value of the programs of fuel a coins exceeds half the number of coin values: completeness 2 / 3 and the optimal prover give more than half, soundness 1 / 3 and the bound on all provers give less.

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

IP ⊆ PSPACE Arora and Barak, Chapter 8 Sipser, Section 10.4: a problem with an interactive proof, whose verifier is strict oracle PPT with private coins, against all randomized stateful provers, is decided within polynomial space. The decider evaluates the game tree of the optimal prover over the messages and replies no longer than the clock of the verifier, counting the accepting coin values at its leaves (Cslib.Complexity.Interaction.evaluate), and compares the count with half the number of coin values (Cslib.Complexity.mem_iff_two_pow_lt_value).