def InteractiveProofs.Prover (Γ : Type) : Type

A prover P in an interactive proof system. Given the input w : List Γ and the transcript-so-far (a list of messages already exchanged), P returns the next message to send to the verifier. Provers are not restricted in computational power.

structure InteractiveProofs.Verifier (Q Γ : Type) : Type

A verifier V in an interactive proof system. It is parameterised by a state-type Q and the alphabet Γ. On input w with n random coins Fin n → Bool, it can sendMessage to the prover or decide (accept/reject) based on the transcript of the conversation.

• sendMessage (w : List Γ) (n : ℕ) : (Fin n → Bool) → (transcript : List (List Γ)) → List Γ
• decide (w : List Γ) (n : ℕ) : (Fin n → Bool) → (transcript : List (List Γ)) → Bool

def InteractiveProofs.runRounds {Q Γ : Type} (V : Verifier Q Γ) (P : Prover Γ) (w : List Γ) (n : ℕ) (coins : Fin n → Bool) : ℕ → List (List Γ)

Run k rounds of interaction between verifier V and prover P on input w using random coins coins : Fin n → Bool. Each round consists of a verifier message followed by a prover message. Returns the resulting transcript as a List (List Γ).

def InteractiveProofs.runProtocol {Q Γ : Type} (V : Verifier Q Γ) (P : Prover Γ) (w : List Γ) (n : ℕ) (coins : Fin n → Bool) (numRounds : ℕ) : Bool

The boolean outcome of running the full numRounds-round protocol V ↔ P on input w with random coins coins: returns true iff V accepts the resulting transcript.

def InteractiveProofs.Verifier.numAccepting {Q Γ : Type} (V : Verifier Q Γ) (P : Prover Γ) (w : List Γ) (n numRounds : ℕ) : ℕ

The number of random-coin assignments in Fin n → Bool that lead V to accept when interacting with P on input w for numRounds rounds.

def InteractiveProofs.Verifier.acceptProb {Q Γ : Type} (V : Verifier Q Γ) (P : Prover Γ) (w : List Γ) (n numRounds : ℕ) : ℚ

The acceptance probability Pr[(V ↔ P) accepts w] = |accepting coin sequences| / 2ⁿ over uniformly random coins in Fin n → Bool.

def InteractiveProofs.IPAcceptanceProbability {Q Γ : Type} (V : Verifier Q Γ) (P : Prover Γ) (w : List Γ) (n numRounds : ℕ) : ℚ

Notation-level alias for the textbook quantity Pr[(V ↔ P) accepts w], defined as V.acceptProb P w n numRounds.

def InteractiveProofs.IsInteractiveProofSystem {Q Γ : Type} (V : Verifier Q Γ) (P : Prover Γ) (A : Set (List Γ)) (t r : ℕ → ℕ) : Prop

(V, P) is an interactive proof system for the language A with random budget t and round budget r if:

• (completeness) for every w ∈ A, Pr[(V ↔ P) accepts w] ≥ 2/3;
• (soundness) for every w ∉ A and every dishonest prover P̃, Pr[(V ↔ P̃) accepts w] ≤ 1/3.

def InteractiveProofs.InIP {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) : Prop

The class IP (Sipser, Lecture 25): a language A is in IP if there exist a verifier V and an honest prover P such that (V, P) forms an interactive proof system for A with both the random-coin budget t and the number-of-rounds budget r polynomial in the input length.

def InteractiveProofs.VerifierPolyMessages {Q Γ : Type} (V : Verifier Q Γ) (t : ℕ → ℕ) (ℓ : ℕ) : Prop

Predicate saying that every message the verifier V sends has length bounded by |w|^ℓ + ℓ, i.e. its outgoing communication is polynomial in the input length. Used to formulate the strong notion InIP_strong which is the form needed for IP = PSPACE.

def InteractiveProofs.InIP_strong {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) : Prop

The strong form of IP membership, identical to InIP but additionally requiring that the verifier's outgoing messages have polynomial length (VerifierPolyMessages V t ℓ). This is the formulation used in the standard IP = PSPACE proof.

def InteractiveProofs.Verifier.PolyMessages {Q Γ : Type} (V : Verifier Q Γ) (t : ℕ → ℕ) (ℓ : ℕ) : Prop

Dot-notation alias for VerifierPolyMessages: every message sent by V has length at most |w|^ℓ + ℓ.

theorem IPEqPSPACE.IP_subset_PSPACE {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) (hA : InteractiveProofs.InIP A) : SpaceComplexity.InPSPACE A

IP ⊆ PSPACE (one direction of Shamir's theorem). A polynomial-space verifier can enumerate all polynomially many random-coin sequences and prover-message choices, computing the optimal acceptance probability and deciding membership in A deterministically in polynomial space.

theorem IPEqPSPACE.PSPACE_subset_IP {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) (hA : SpaceComplexity.InPSPACE A) : InteractiveProofs.InIP A

PSPACE ⊆ IP (Shamir's theorem; the harder direction). Every polynomial-space language has an interactive proof system, by reducing to TQBF (which is PSPACE-complete) and giving an IP protocol for TQBF via arithmetization and sum-check.

theorem IPEqPSPACE.IP_eq_PSPACE {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) : InteractiveProofs.InIP A ↔ SpaceComplexity.InPSPACE A

IP = PSPACE (Shamir's theorem, Sipser Lecture 26). For every language A, A ∈ IP iff A ∈ PSPACE. Combines IP_subset_PSPACE and PSPACE_subset_IP.

theorem ip_eq_pspace {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) : InteractiveProofs.InIP A ↔ SpaceComplexity.InPSPACE A

Top-level restatement of Shamir's theorem IP = PSPACE outside the IPEqPSPACE namespace, for convenient external use.