The game tree of an interactive protocol

⚠️ Unreviewed by Bolton

The value of a protocol on an input is the acceptance probability against an optimal prover — a maximum over strategies, which are functions on transcripts. This file replaces that maximum by a finite recursion over the transcript tree, which is the object a polynomial-space machine walks.

The tree is indexed by the transcript so far. At a node the coins still in play are those consistent with the recorded verifier messages (Complexity.Protocol.consFinset); a round splits them by the verifier's next message and the prover picks, for each such message, the reply maximizing the count below. Everything is counted rather than averaged: Complexity.Protocol.gval is the number of coin strings that end up accepting, so the value is that count over 2 ^ coins.

Main definitions

• Complexity.Protocol.runFrom — the interaction continued from a partial transcript
• Complexity.Protocol.consFinset — the coins consistent with a transcript
• Complexity.Protocol.sval — the accepting count of a fixed strategy, as a tree recursion
• Complexity.Protocol.gval — the same with the prover playing optimally

Main results

• Complexity.Protocol.transcript_eq_runFrom — the two ways of running agree
• Complexity.Protocol.consFinset_append — a round filters the coins by the verifier's message
• Complexity.Protocol.view_eq — the verifier's view, with the transcript encoding unfolded
• Complexity.Protocol.gval_succ_strsLe — the sum ranges over every short string
• Complexity.Protocol.consistent_iff_replay — consistency is a replay of the verifier
• Complexity.Protocol.gvalR_zero, Complexity.Protocol.gvalR_succ — the recursion a stack machine walks

theorem Complexity.Protocol.view_eq (x r : List Bool) (τ : Transcript) : view x r τ = pair (pair x r) (false :: (encBody τ ++ [true]))

The verifier's view, unfolded. The transcript reaches the verifier through the concatenation Complexity.encBody, so extending the transcript only ever appends to it.

Running from a partial transcript

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

The interaction continued for n more rounds from the transcript τ.

Equations

• prot.runFrom x S r 0 x✝ = x✝
• prot.runFrom x S r n.succ x✝ = prot.runFrom x S r n (x✝ ++ [prot.vmsg (Complexity.Protocol.view x r x✝), S (x✝ ++ [prot.vmsg (Complexity.Protocol.view x r x✝)])])

@[simp]

theorem Complexity.Protocol.runFrom_zero (prot : Protocol) (x : List Bool) (S : ProverStrategy) (r : List Bool) (τ : Transcript) : prot.runFrom x S r 0 τ = τ

theorem Complexity.Protocol.runFrom_succ (prot : Protocol) (x : List Bool) (S : ProverStrategy) (r : List Bool) (n : ℕ) (τ : Transcript) : prot.runFrom x S r (n + 1) τ = prot.runFrom x S r n (τ ++ [prot.vmsg (view x r τ), S (τ ++ [prot.vmsg (view x r τ)])])

theorem Complexity.Protocol.runFrom_succ' (prot : Protocol) (x : List Bool) (S : ProverStrategy) (r : List Bool) (n : ℕ) (τ : Transcript) : prot.runFrom x S r (n + 1) τ = prot.runFrom x S r n τ ++ [prot.vmsg (view x r (prot.runFrom x S r n τ)), S (prot.runFrom x S r n τ ++ [prot.vmsg (view x r (prot.runFrom x S r n τ))])]

The continuation appends its last round at the end, exactly as Complexity.Protocol.transcript does.

theorem Complexity.Protocol.transcript_eq_runFrom (prot : Protocol) (x : List Bool) (S : ProverStrategy) (r : List Bool) (n : ℕ) : prot.transcript S x r n = prot.runFrom x S r n []

The two ways of running agree.

The coins still in play

def Complexity.Protocol.Consistent (prot : Protocol) (x r : List Bool) (τ : Transcript) : Prop

A coin string is consistent with a transcript when every verifier message recorded in it is the one the verifier would have sent.

Equations

• prot.Consistent x r τ = ∀ (j : ℕ), 2 * j < List.length τ → τ[2 * j]! = prot.vmsg (Complexity.Protocol.view x r (List.take (2 * j) τ))

theorem Complexity.Protocol.consistent_nil (prot : Protocol) (x r : List Bool) : prot.Consistent x r []

theorem Complexity.Protocol.consistent_append (prot : Protocol) (x r : List Bool) (τ : Transcript) (i : ℕ) (hτ : List.length τ = 2 * i) (v a : List Bool) : prot.Consistent x r (τ ++ [v, a]) ↔ prot.Consistent x r τ ∧ v = prot.vmsg (view x r τ)

Extending a transcript by one round adds exactly one condition: the verifier's message.

noncomputable def Complexity.Protocol.consFinset (prot : Protocol) (x : List Bool) (t : ℕ) (τ : Transcript) : Finset (Fin t → Bool)

The coins consistent with a transcript.

Equations

• prot.consFinset x t τ = {r : Fin t → Bool | prot.Consistent x (Complexity.BitString.toList r) τ}

theorem Complexity.Protocol.consFinset_nil (prot : Protocol) (x : List Bool) (t : ℕ) : prot.consFinset x t [] = Finset.univ

theorem Complexity.Protocol.consFinset_append (prot : Protocol) (x : List Bool) (t : ℕ) (τ : Transcript) (i : ℕ) (hτ : List.length τ = 2 * i) (v a : List Bool) : prot.consFinset x t (τ ++ [v, a]) = {r ∈ prot.consFinset x t τ | prot.vmsg (view x r.toList τ) = v}

A round filters the coins by the verifier's message. The reply the prover chooses plays no part: the coins in play below a node depend only on the verifier messages above it.

The tree recursion

noncomputable def Complexity.Protocol.vset (prot : Protocol) (x : List Bool) (t : ℕ) (τ : Transcript) : Finset (List Bool)

The verifier messages still possible at a node.

Equations

• prot.vset x t τ = Finset.image (fun (r : Complexity.BitString t) => prot.vmsg (Complexity.Protocol.view x r.toList τ)) (prot.consFinset x t τ)

noncomputable def Complexity.Protocol.sval (prot : Protocol) (x : List Bool) (t : ℕ) (S : ProverStrategy) : ℕ → Transcript → ℕ

The coins consistent with τ that accept when the prover plays S for the remaining n rounds, as a recursion down the tree.

Equations

• prot.sval x t S 0 x✝ = {r ∈ prot.consFinset x t x✝ | Complexity.Protocol.view x r.toList x✝ ∈ prot.verdict}.card
• prot.sval x t S n.succ x✝ = ∑ v ∈ prot.vset x t x✝, prot.sval x t S n (x✝ ++ [v, S (x✝ ++ [v])])

noncomputable def Complexity.Protocol.gval (prot : Protocol) (x : List Bool) (t m : ℕ) : ℕ → Transcript → ℕ

The same count with the prover playing optimally: at each node it picks, for every possible verifier message, the reply maximizing the count below.

Equations

• prot.gval x t m 0 x✝ = {r ∈ prot.consFinset x t x✝ | Complexity.Protocol.view x r.toList x✝ ∈ prot.verdict}.card
• prot.gval x t m n.succ x✝ = ∑ v ∈ prot.vset x t x✝, (Complexity.strsLe m).sup fun (a : List Bool) => prot.gval x t m n (x✝ ++ [v, a])

theorem Complexity.Protocol.sval_succ (prot : Protocol) (x : List Bool) (t : ℕ) (S : ProverStrategy) (n : ℕ) (τ : Transcript) : prot.sval x t S (n + 1) τ = ∑ v ∈ prot.vset x t τ, prot.sval x t S n (τ ++ [v, S (τ ++ [v])])

theorem Complexity.Protocol.gval_succ (prot : Protocol) (x : List Bool) (t m n : ℕ) (τ : Transcript) : prot.gval x t m (n + 1) τ = ∑ v ∈ prot.vset x t τ, (strsLe m).sup fun (a : List Bool) => prot.gval x t m n (τ ++ [v, a])

theorem Complexity.Protocol.sval_eq_card (prot : Protocol) (x : List Bool) (t : ℕ) (S : ProverStrategy) (n i : ℕ) (τ : Transcript) : List.length τ = 2 * i → prot.sval x t S n τ = {r ∈ prot.consFinset x t τ | view x r.toList (prot.runFrom x S r.toList n τ) ∈ prot.verdict}.card

What the recursion counts.

theorem Complexity.Protocol.sval_root (prot : Protocol) (x : List Bool) (t : ℕ) (S : ProverStrategy) : prot.sval x t S (prot.rounds x.length) [] = {r : Fin t → Bool | prot.Accepts S x (BitString.toList r)}.card

The count at the root is the acceptance probability's numerator.

The optimum is attained

theorem Complexity.Protocol.sval_le_gval (prot : Protocol) (x : List Bool) (t m : ℕ) {S : ProverStrategy} (hS : S.Bounded m) (n : ℕ) (τ : Transcript) : prot.sval x t S n τ ≤ prot.gval x t m n τ

A bounded strategy cannot beat the optimum.

noncomputable def Complexity.Protocol.optReply (prot : Protocol) (x : List Bool) (t m R : ℕ) (σ : Transcript) : List Bool

A reply attaining the maximum at a node whose depth says R rounds are planned.

Equations

• prot.optReply x t m R σ = Classical.choose ⋯

theorem Complexity.Protocol.optReply_mem (prot : Protocol) (x : List Bool) (t m R : ℕ) (σ : Transcript) : prot.optReply x t m R σ ∈ strsLe m

theorem Complexity.Protocol.optReply_sup (prot : Protocol) (x : List Bool) (t m R : ℕ) (σ : Transcript) : ((strsLe m).sup fun (a : List Bool) => prot.gval x t m (R - List.length σ / 2 - 1) (σ ++ [a])) = prot.gval x t m (R - List.length σ / 2 - 1) (σ ++ [prot.optReply x t m R σ])

noncomputable def Complexity.Protocol.optStrategy (prot : Protocol) (x : List Bool) (t m R : ℕ) : ProverStrategy

The strategy that always plays a maximizing reply.

Equations

• prot.optStrategy x t m R = prot.optReply x t m R

theorem Complexity.Protocol.optStrategy_bounded (prot : Protocol) (x : List Bool) (t m R : ℕ) : (prot.optStrategy x t m R).Bounded m

theorem Complexity.Protocol.sval_optStrategy (prot : Protocol) (x : List Bool) (t m R n i : ℕ) (τ : Transcript) : n + i = R → List.length τ = 2 * i → prot.sval x t (prot.optStrategy x t m R) n τ = prot.gval x t m n τ

The optimum is attained.

The value decides the language

theorem Complexity.Protocol.acceptEvent_eq_filter (prot : Protocol) (x : List Bool) (S : ProverStrategy) : prot.acceptEvent S x = {r : Fin (prot.coins x.length) → Bool | prot.Accepts S x (BitString.toList r)}

theorem Complexity.Protocol.card_acceptEvent_le_gval (prot : Protocol) (x : List Bool) (S : ProverStrategy) (hS : S.Bounded (prot.msgLen x.length)) : (prot.acceptEvent S x).card ≤ prot.gval x (prot.coins x.length) (prot.msgLen x.length) (prot.rounds x.length) []

The optimum is the largest accepting count a bounded strategy achieves.

theorem Complexity.Protocol.gval_eq_card_acceptEvent (prot : Protocol) (x : List Bool) : prot.gval x (prot.coins x.length) (prot.msgLen x.length) (prot.rounds x.length) [] = (prot.acceptEvent (prot.optStrategy x (prot.coins x.length) (prot.msgLen x.length) (prot.rounds x.length)) x).card

And it is achieved: the maximizing strategy is bounded and attains it.

theorem Complexity.Protocol.mem_iff_gval (prot : Protocol) (x : List Bool) {L : Language} (hcomp : ∀ y ∈ L, ∃ (S : ProverStrategy), S.Bounded (prot.msgLen y.length) ∧ 2 / 3 ≤ eventProb (prot.acceptEvent S y)) (hsound : ∀ y ∉ L, ∀ (S : ProverStrategy), S.Bounded (prot.msgLen y.length) → eventProb (prot.acceptEvent S y) ≤ 1 / 3) : x ∈ L ↔ 2 ^ prot.coins x.length < 2 * prot.gval x (prot.coins x.length) (prot.msgLen x.length) (prot.rounds x.length) []

The tree value decides the language. Completeness puts the optimum above two thirds of the coin space and soundness below one third, so a comparison against a half separates them.

Every message in the tree is short

theorem Complexity.Protocol.vset_length (prot : Protocol) (x : List Bool) (t : ℕ) (τ : Transcript) {v : List Bool} (hv : v ∈ prot.vset x t τ) : v.length ≤ prot.msgLen x.length

A verifier message the tree branches on respects the length bound.

theorem Complexity.Protocol.runFrom_length (prot : Protocol) (x : List Bool) (S : ProverStrategy) (hS : S.Bounded (prot.msgLen x.length)) (r : List Bool) (n : ℕ) (τ : Transcript) : (∀ u ∈ τ, u.length ≤ prot.msgLen x.length) → ∀ u ∈ prot.runFrom x S r n τ, u.length ≤ prot.msgLen x.length

Hence every message on a path down the tree does.

theorem Complexity.Protocol.runFrom_card (prot : Protocol) (x : List Bool) (S : ProverStrategy) (r : List Bool) (n : ℕ) (τ : Transcript) : List.length (prot.runFrom x S r n τ) = List.length τ + 2 * n

And the transcript never holds more than two messages per round.

The tree in the form a machine walks it

theorem Complexity.Protocol.gval_eq_zero (prot : Protocol) (x : List Bool) (t m n : ℕ) (σ : Transcript) (h : prot.consFinset x t σ = ∅) : prot.gval x t m n σ = 0

A node no coin string reaches contributes nothing.

theorem Complexity.Protocol.gval_succ_strsLe (prot : Protocol) (x : List Bool) (t n i : ℕ) (τ : Transcript) (hτ : List.length τ = 2 * i) : prot.gval x t (prot.msgLen x.length) (n + 1) τ = ∑ v ∈ strsLe (prot.msgLen x.length), (strsLe (prot.msgLen x.length)).sup fun (a : List Bool) => prot.gval x t (prot.msgLen x.length) n (τ ++ [v, a])

The sum may range over every short string. A verifier message no coin string would send splits off an empty set of coins, so its whole subtree is zero; and Protocol.vmsg_len keeps the messages that are sent inside Complexity.strsLe. The recursion is then a walk over a fixed finite index set, which is what a machine can enumerate.

theorem Complexity.Protocol.gval_zero_strsOfLen (prot : Protocol) (x : List Bool) (t m : ℕ) (τ : Transcript) : prot.gval x t m 0 τ = {s ∈ strsOfLen t | prot.Consistent x s τ ∧ view x s τ ∈ prot.verdict}.card

The leaf count, over bitstrings. The coin space is exactly the strings of the coin length, so the count a machine has to make at a leaf is a scan over Complexity.strsOfLen.

Replaying the verifier

def Complexity.Protocol.replay (prot : Protocol) (x s : List Bool) : List (List Bool × List Bool) → List Bool → Bool

Walk the rounds, checking that every message the verifier is recorded as having sent is the one it would have sent. The body of the transcript's encoding is carried along, so nothing is re-encoded.

Equations

• One or more equations did not get rendered due to their size.
• prot.replay x s [] x✝ = true

@[simp]

theorem Complexity.Protocol.replay_nil (prot : Protocol) (x s body : List Bool) : prot.replay x s [] body = true

theorem Complexity.Protocol.replay_cons (prot : Protocol) (x s : List Bool) (p : List Bool × List Bool) (ps : List (List Bool × List Bool)) (body : List Bool) : prot.replay x s (p :: ps) body = (decide (p.1 = prot.vmsg (pair (pair x s) (false :: (body ++ [true])))) && prot.replay x s ps (body ++ encMsg p.1 ++ encMsg p.2))

theorem Complexity.Protocol.consistent_append_iff_replay (prot : Protocol) (x s : List Bool) (ps : List (List Bool × List Bool)) (τ : Transcript) (i : ℕ) : List.length τ = 2 * i → (prot.Consistent x s (τ ++ flatRounds ps) ↔ prot.Consistent x s τ ∧ prot.replay x s ps (encBody τ) = true)

Consistency is a replay. Walking the rounds and re-deriving the verifier's messages decides whether a coin string could have produced the transcript.

theorem Complexity.Protocol.consistent_iff_replay (prot : Protocol) (x s : List Bool) (ps : List (List Bool × List Bool)) : prot.Consistent x s (flatRounds ps) ↔ prot.replay x s ps [] = true

Consistency at the root.

The tree indexed by rounds

noncomputable def Complexity.Protocol.gvalR (prot : Protocol) (x : List Bool) (t n : ℕ) (ps : List (List Bool × List Bool)) : ℕ

The tree value, indexed by the rounds already played. This is the recursion a stack machine walks: one frame per round, a sum over the verifier's possible messages and a maximum over the prover's replies, bottoming out in a count over the coin strings.

Equations

• prot.gvalR x t n ps = prot.gval x t (prot.msgLen x.length) n (Complexity.flatRounds ps)

theorem Complexity.Protocol.gvalR_zero (prot : Protocol) (x : List Bool) (t : ℕ) (ps : List (List Bool × List Bool)) : prot.gvalR x t 0 ps = {s ∈ strsOfLen t | prot.replay x s ps [] = true ∧ pair (pair x s) (false :: (encBodyR ps ++ [true])) ∈ prot.verdict}.card

theorem Complexity.Protocol.gvalR_succ (prot : Protocol) (x : List Bool) (t n : ℕ) (ps : List (List Bool × List Bool)) : prot.gvalR x t (n + 1) ps = ∑ v ∈ strsLe (prot.msgLen x.length), (strsLe (prot.msgLen x.length)).sup fun (a : List Bool) => prot.gvalR x t n (ps ++ [(v, a)])

theorem Complexity.Protocol.gvalR_root (prot : Protocol) (x : List Bool) (t n : ℕ) : prot.gvalR x t n [] = prot.gval x t (prot.msgLen x.length) n []

The recursion against the counters

theorem Complexity.Protocol.gvalR_succ_enum (prot : Protocol) (x : List Bool) (t n : ℕ) (ps : List (List Bool × List Bool)) : prot.gvalR x t (n + 1) ps = ∑ i ∈ Finset.range (2 ^ (prot.msgLen x.length + 1) - 1), (Finset.range (2 ^ (prot.msgLen x.length + 1) - 1)).sup fun (j : ℕ) => prot.gvalR x t n (ps ++ [(nextStr^[i] [], nextStr^[j] [])])

The branching, as two counter loops. Complexity.nextStr visits every message the verifier or the prover may send exactly once, so the sum and the maximum are ordinary loops.

theorem Complexity.Protocol.gvalR_zero_enum (prot : Protocol) (x : List Bool) (t : ℕ) (ps : List (List Bool × List Bool)) : prot.gvalR x t 0 ps = {i ∈ Finset.range (2 ^ t) | prot.replay x (bumpBits^[i] (List.replicate t false)) ps [] = true ∧ pair (pair x (bumpBits^[i] (List.replicate t false))) (false :: (encBodyR ps ++ [true])) ∈ prot.verdict}.card

The leaf, as a counter loop.

The value never exceeds the coin space

theorem Complexity.Protocol.gval_le_card (prot : Protocol) (x : List Bool) (t n i : ℕ) (τ : Transcript) : List.length τ = 2 * i → prot.gval x t (prot.msgLen x.length) n τ ≤ (prot.consFinset x t τ).card

The tree value never exceeds the number of coins still in play. The verifier's next message partitions those coins, so summing over the messages cannot double-count.

theorem Complexity.Protocol.gval_le_two_pow (prot : Protocol) (x : List Bool) (t n i : ℕ) (τ : Transcript) (hτ : List.length τ = 2 * i) : prot.gval x t (prot.msgLen x.length) n τ ≤ 2 ^ t

theorem Complexity.Protocol.gvalR_le_two_pow (prot : Protocol) (x : List Bool) (t n : ℕ) (ps : List (List Bool × List Bool)) : prot.gvalR x t n ps ≤ 2 ^ t

The containment, reduced to evaluating the tree

theorem Complexity.IP_subset_PSPACE_of_gval (h : ∀ (prot : Protocol) (rp cp mp : Polynomial ℕ), (∀ (n : ℕ), prot.rounds n = Polynomial.eval n rp) → (∀ (n : ℕ), prot.coins n = Polynomial.eval n cp) → (∀ (n : ℕ), prot.msgLen n = Polynomial.eval n mp) → {x : List Bool | 2 ^ prot.coins x.length < 2 * prot.gval x (prot.coins x.length) (prot.msgLen x.length) (prot.rounds x.length) []} ∈ PSPACE) : IP ⊆ PSPACE

IP ⊆ PSPACE, reduced to one computation. Membership in a language of IP is a comparison of the game-tree value against half the coin space, so a polynomial-space evaluation of that value settles the containment.