IP ⊆ PSPACE, assembled

⚠️ Unreviewed by Bolton

Everything is in place: Complexity.IPM.ipStep is the walk of the game tree written inside the polynomial-time algebra, Complexity.Protocol.walk_decides says its orbit ends with the membership bit, Complexity.IPM.runBound_le bounds how long that takes, and Complexity.IPM.encSst_length_le bounds how much room it needs. This file hands them to Complexity.SpaceIter.mem_PSPACE_of_iterate.

Main definitions

• Complexity.ipG — the function the space-bounded iteration runs

Main results

• Complexity.ipG_iterate — the packed orbit is the abstract one
• Complexity.IP_subset_PSPACE_internal — the containment

The iterated function

noncomputable def Complexity.ipG (prot : Protocol) (vd : List Bool → List Bool) (rp cp mp : Polynomial ℕ) (z : List Bool) : List Bool

The function the space-bounded iteration runs: the running state is the first component and the input the second, so the very first call — on pair [] x — builds the initial state.

Equations

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

theorem Complexity.ipG_nil (prot : Protocol) (vd : List Bool → List Bool) (rp cp mp : Polynomial ℕ) (x : List Bool) : ipG prot vd rp cp mp (pair [] x) = pair (IPM.ipInit (polyRuler cp x) (polyRuler rp x)) x

theorem Complexity.ipG_step (prot : Protocol) (vd : List Bool → List Bool) (rp cp mp : Polynomial ℕ) (st x : List Bool) (h : st ≠ []) : ipG prot vd rp cp mp (pair st x) = pair (IPM.ipStep (polyRuler mp x) (polyRuler cp x) (okFn prot.vmsg vd (polyRuler rp x) x) st) x

The orbit

theorem Complexity.cr_length (prot : Protocol) (cp : Polynomial ℕ) (hcp : ∀ (n : ℕ), prot.coins n = Polynomial.eval n cp) (x : List Bool) : (polyRuler cp x).length = (prot.walkParams x).t

theorem Complexity.mr_length (prot : Protocol) (mp : Polynomial ℕ) (hmp : ∀ (n : ℕ), prot.msgLen n = Polynomial.eval n mp) (x : List Bool) : (polyRuler mp x).length = (prot.walkParams x).m

theorem Complexity.ipG_iterate (prot : Protocol) (vd : List Bool → List Bool) (rp cp mp : Polynomial ℕ) (hcp : ∀ (n : ℕ), prot.coins n = Polynomial.eval n cp) (hmp : ∀ (n : ℕ), prot.msgLen n = Polynomial.eval n mp) (hvd : ∀ (z : List Bool), vd z = [decide (z ∈ prot.verdict)]) (x : List Bool) (j : ℕ) : (ipG prot vd rp cp mp)^[j + 1] (pair [] x) = pair (IPM.encSst ((IPM.step (prot.walkParams x))^[j] { done := false, ansBit := false, ret := none, stk := [IPM.freshFrm (prot.walkParams x) [] (polyRuler rp x)] })) x

The packed orbit is the abstract one.

The run at a fixed input

noncomputable def Complexity.IPRunSpec (prot : Protocol) (L : Language) (rp : Polynomial ℕ) (x : List Bool) (T : ℕ) : Prop

What a run of T steps at x achieves.

Equations

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

theorem Complexity.ipRun_exists (prot : Protocol) {L : Language} (rp : Polynomial ℕ) (hrp : ∀ (n : ℕ), prot.rounds n = Polynomial.eval n rp) (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 : List Bool) : ∃ (T : ℕ), IPRunSpec prot L rp x T

noncomputable def Complexity.ipT (prot : Protocol) (L : Language) (rp : Polynomial ℕ) (hex : ∀ (x : List Bool), ∃ (T : ℕ), IPRunSpec prot L rp x T) (x : List Bool) : ℕ

The number of steps the walk takes at x.

Equations

• Complexity.ipT prot L rp hex x = Classical.choose ⋯

theorem Complexity.ipT_spec (prot : Protocol) (L : Language) (rp : Polynomial ℕ) (hex : ∀ (x : List Bool), ∃ (T : ℕ), IPRunSpec prot L rp x T) (x : List Bool) : IPRunSpec prot L rp x (ipT prot L rp hex x)

The containment

theorem Complexity.ip_mem_PSPACE (prot : Protocol) {L : Language} (rp cp mp r w : Polynomial ℕ) (hrp : ∀ (n : ℕ), prot.rounds n = Polynomial.eval n rp) (hcp : ∀ (n : ℕ), prot.coins n = Polynomial.eval n cp) (hmp : ∀ (n : ℕ), prot.msgLen n = Polynomial.eval n mp) (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) (hr : ∀ (n : ℕ), 2 * (2 * (Polynomial.eval n cp + 1) + (Polynomial.eval n rp + 1) * (2 * (2 * (Polynomial.eval n rp + 1) + 2 * Polynomial.eval n mp + 2 * (Polynomial.eval n mp + Polynomial.eval n cp) + 4 * (Polynomial.eval n cp + 1) + (Polynomial.eval n rp + 1) * (8 * (Polynomial.eval n mp + Polynomial.eval n cp) + 4) + 10) + 2) + 10) + 2 + n ≤ Polynomial.eval n r) (hw : ∀ (n : ℕ), Polynomial.eval n cp + 2 + (2 * Polynomial.eval n mp + 3) * Polynomial.eval n rp ≤ Polynomial.eval n w) : L ∈ PSPACE

IP ⊆ PSPACE, for one protocol.

noncomputable def Complexity.ipStatePoly (rp cp mp : Polynomial ℕ) : Polynomial ℕ

The polynomial bounding the length of the state the walk carries.

Equations

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

noncomputable def Complexity.ipCountPoly (rp cp mp : Polynomial ℕ) : Polynomial ℕ

The polynomial bounding the logarithm of the number of steps it takes.

Equations

• Complexity.ipCountPoly rp cp mp = cp + 2 + (2 * mp + 3) * rp

theorem Complexity.ipStatePoly_eval (rp cp mp : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (ipStatePoly rp cp mp) = 2 * (2 * (Polynomial.eval n cp + 1) + (Polynomial.eval n rp + 1) * (2 * (2 * (Polynomial.eval n rp + 1) + 2 * Polynomial.eval n mp + 2 * (Polynomial.eval n mp + Polynomial.eval n cp) + 4 * (Polynomial.eval n cp + 1) + (Polynomial.eval n rp + 1) * (8 * (Polynomial.eval n mp + Polynomial.eval n cp) + 4) + 10) + 2) + 10) + 2 + n

theorem Complexity.ipCountPoly_eval (rp cp mp : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (ipCountPoly rp cp mp) = Polynomial.eval n cp + 2 + (2 * Polynomial.eval n mp + 3) * Polynomial.eval n rp

theorem Complexity.IP_subset_PSPACE_internal : IP ⊆ PSPACE

IP ⊆ PSPACE. The optimal prover's acceptance count is the value of a polynomially deep game tree, and a stack machine walks that tree in polynomial space.