IP ⊆ PSPACE — the strategy space is finite

⚠️ Unreviewed by Bolton

A prover strategy is a function on all transcripts, of which there are infinitely many, so the supremum over strategies that IP quantifies is a supremum over an infinite set. A machine cannot search that. The first thing to establish is therefore that the quantifier is really finite: a run of prot.rounds n rounds only ever consults the strategy on transcripts of length below 2 · rounds n, so two strategies agreeing there are indistinguishable.

That is what these lemmas say. Together with the message-length bound carried by ProverStrategy.Bounded, they cut the search down to a finite game tree of polynomial depth, which is the object a depth-first polynomial-space evaluation walks.

Main results

• Protocol.transcript_length — a run of n rounds produces 2 n messages
• Protocol.transcript_congr — strategy extensionality for the transcript
• Protocol.accepts_congr, Protocol.acceptEvent_congr — and for acceptance

theorem Complexity.Protocol.transcript_length (prot : Protocol) (S : ProverStrategy) (x r : List Bool) (n : ℕ) : List.length (prot.transcript S x r n) = 2 * n

A run of n rounds appends two messages per round.

theorem Complexity.Protocol.transcript_congr (prot : Protocol) {S S' : ProverStrategy} (x r : List Bool) (n : ℕ) : (∀ (τ : Transcript), List.length τ ≤ 2 * n → S τ = S' τ) → prot.transcript S x r n = prot.transcript S' x r n

Strategy extensionality. The run consults the strategy only on the transcripts it actually produces, all of which have length below 2 n; two strategies agreeing there yield the same transcript.

theorem Complexity.Protocol.accepts_congr (prot : Protocol) {S S' : ProverStrategy} (x r : List Bool) (h : ∀ (τ : Transcript), List.length τ ≤ 2 * prot.rounds x.length → S τ = S' τ) : prot.Accepts S x r ↔ prot.Accepts S' x r

Acceptance depends on the strategy only through its values on the transcripts the run produces.

theorem Complexity.Protocol.acceptEvent_congr (prot : Protocol) {S S' : ProverStrategy} (x : List Bool) (h : ∀ (τ : Transcript), List.length τ ≤ 2 * prot.rounds x.length → S τ = S' τ) : prot.acceptEvent S x = prot.acceptEvent S' x

The accepting coin set — and hence the acceptance probability — depends on the strategy only through those values.