TQBF has an interactive proof

The machine verifier of Cslib.Complexity.QBFProtocol.verifier against a word prover behaves exactly as the token-stream verifier Cslib.Complexity.QBFProtocol.verifyAt over ZMod p against the typed prover that decodes the replies of the word prover to the messages encoding its queries (Cslib.Complexity.QBFProtocol.runWith_verdict): the machine keeps every point and value as the values below p of the points and values of the protocol, and every check of the machine modulo p is the check of the protocol in ZMod p. Hence, on a closed formula, the verifier accepts with the probability that the protocol accepts the claim that the arithmetization has value 1 at the origin (Cslib.Complexity.QBFProtocol.acceptProb_verifier_eq).

Soundness. The samples give every residue probability at most 2 / p, every round has degree at most D = 2 * size ψ, and the arithmetization has at most (size ψ + 1) * size ψ operators, so on a false closed formula every prover is accepted with probability at most (size ψ + 1) * size ψ * D * 2 / p ≤ 1 / 3, as p > 12 * size ψ ^ 2 * (size ψ + 1); a formula with a free variable is rejected (Cslib.Complexity.QBFProtocol.acceptProb_verifier_le).

Completeness. The honest prover (Cslib.Complexity.QBFProtocol.honestProver) decodes the subformula and the point from each message and encodes the honest reply, and is accepted with probability 1 on every true closed formula (Cslib.Complexity.QBFProtocol.acceptProb_verifier_honestProver).

Together with Cslib.Complexity.QBFProtocol.isOraclePPTOn_verifier, TQBF ∈ IP (Cslib.Complexity.TQBF_mem_IP), with perfect completeness.

Main definitions

• Cslib.Complexity.QBFProtocol.verdict: the verdict of the machine after a number of steps.
• Cslib.Complexity.QBFProtocol.typedRespond: the typed prover of a word prover.
• Cslib.Complexity.QBFProtocol.honestProver: the honest prover.

Main results

• Cslib.Complexity.QBFProtocol.runWith_verdict: the machine simulates the protocol.
• Cslib.Complexity.QBFProtocol.acceptProb_verifier_le: soundness error 1 / 3.
• Cslib.Complexity.QBFProtocol.acceptProb_verifier_honestProver: perfect completeness.
• Cslib.Complexity.QBFProtocol.isInteractiveProof_verifier: the interactive proof.
• Cslib.Complexity.TQBF_mem_IP: TQBF ∈ IP.

References

• C. Lund, L. Fortnow, H. Karloff, N. Nisan, Algebraic methods for interactive proof systems
• A. Shamir, IP = PSPACE
• A. Shen, IP = SPACE: simplified proof
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 8.3

Verdicts of the machine

noncomputable def Cslib.Complexity.QBFProtocol.verdict (I : Machine.LoopInput) (st : Machine.VState) (n : ℕ) : Probability.WordOracleComp Unit Bool

The verdict of the machine after n steps from the state st.

The typed prover of a word prover

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.modOf (I : Machine.LoopInput) : ℕ

The modulus of the machine on the input I.

noncomputable def Cslib.Complexity.QBFProtocol.samplerOf (I : Machine.LoopInput) : ProbComp (ZMod (modOf I))

The samples of the protocol: those of the machine, in ZMod p.

noncomputable def Cslib.Complexity.QBFProtocol.queryMessage (I : Machine.LoopInput) (q : QueryAt (ZMod (modOf I))) : List Bool

The message of the machine for a query of the protocol.

def Cslib.Complexity.QBFProtocol.decodeTyped (I : Machine.LoopInput) (word : List Bool) : List (ZMod (modOf I))

The reply of the machine to a word, in ZMod p.

noncomputable def Cslib.Complexity.QBFProtocol.typedRespond {S : Type} (I : Machine.LoopInput) (respond : Unit × List Bool → StateT S PMF (List Bool)) : QueryAt (ZMod (modOf I)) → StateT S PMF (List (ZMod (modOf I)))

The typed prover of a word prover: the decoded reply of the word prover to the message of the machine for the query.

The machine simulates the protocol

theorem Cslib.Complexity.QBFProtocol.runWith_verdict {S : Type} (respond : Unit × List Bool → StateT S PMF (List Bool)) (I : Machine.LoopInput) (e : Logic.PL.ArithQBF ℕ) (he : ∀ w ∈ e.vars, w ∈ I.1.1) (rest : List (Logic.PL.ArithQBF.Kind × ℕ)) (r : ℕ → ZMod (modOf I)) (c : ZMod (modOf I)) (St : List Machine.Claim) (m : ℕ) (s : S) : ProbOracleComp.runWith respond (verdict I (e.tokens ++ rest, (canonPt I.1.1 r, c.val) :: St, true) (e.tokens.length + m)) s = (ProbOracleComp.runWith (typedRespond I respond) (verifyAt (samplerOf I) I.1.2.2 e rest r c) s).bind fun (x : Bool × S) => if x.1 = true then ProbOracleComp.runWith respond (verdict I (rest, St, true) m) x.2 else PMF.pure (false, x.2)

The machine simulates the protocol. From a state whose remaining tokens are those of e followed by rest, and whose top claim holds the values below p of a point r on the variables of xs and of a claimed value c, the machine checks e as the token-stream verifier checks the claim that e has value c at r, against the typed prover of the word prover, and then goes on with rest and the claims below.

The verifier on a formula

def Cslib.Complexity.QBFProtocol.arithOf (ψ : Logic.PL.QBF ℕ) : Logic.PL.ArithQBF ℕ

The arithmetic formula checked by the machine on ψ.

theorem Cslib.Complexity.QBFProtocol.instFactPrimeModOfLoopInput (ψ : Logic.PL.QBF ℕ) : Fact (Nat.Prime (modOf (loopInput ψ)))

theorem Cslib.Complexity.QBFProtocol.acceptProb_verifier_eq (ψ : Logic.PL.QBF ℕ) (hψ : ψ.Closed) (P : Prover Unit) : acceptProb (verifier ψ) P = ProbOracleComp.acceptProbWith (typedRespond (loopInput ψ) P.respond) (verifyAt (samplerOf (loopInput ψ)) (loopInput ψ).1.2.2 (arithOf ψ) [] 0 1) P.init

The verifier against a word prover is the protocol against its typed prover: on a closed formula, the machine accepts with the probability that the token-stream verifier accepts the claim that the arithmetization has value 1 at the origin.

theorem Cslib.Complexity.QBFProtocol.acceptProb_verifier_le (ψ : Logic.PL.QBF ℕ) (hψ : ψ ∉ TQBF) (P : Prover Unit) : acceptProb (verifier ψ) P ≤ 1 / 3

Soundness of the verifier: on a formula outside TQBF, every prover is accepted with probability at most 1 / 3.

The honest prover

theorem Cslib.Complexity.QBFProtocol.honestReplyAt_congr {F : Type} [CommRing F] (D : ℕ) {e : Logic.PL.ArithQBF ℕ} {r r' : ℕ → F} (h : ∀ w ∈ e.vars, r w = r' w) : honestReplyAt D e r = honestReplyAt D e r'

noncomputable def Cslib.Complexity.QBFProtocol.honestWord (ψ : Logic.PL.QBF ℕ) (message : List Bool) : List Bool

The reply of the honest prover to a message of the machine on ψ: the encoding of the honest reply to the query of the protocol that the message encodes.

noncomputable def Cslib.Complexity.QBFProtocol.honestProver (ψ : Logic.PL.QBF ℕ) : Prover Unit

The honest prover on ψ, which keeps no state.

theorem Cslib.Complexity.QBFProtocol.acceptProb_verifier_honestProver (ψ : Logic.PL.QBF ℕ) (hψ : ψ ∈ TQBF) : acceptProb (verifier ψ) (honestProver ψ) = 1

Completeness of the verifier: on a true closed formula, the honest prover is accepted with probability 1.

theorem Cslib.Complexity.QBFProtocol.isInteractiveProof_verifier : IsInteractiveProof verifier TQBF 1 (1 / 3)

The interactive proof for TQBF, with perfect completeness and soundness error 1 / 3.

theorem Cslib.Complexity.TQBF_mem_IP : TQBF ∈ IP encQBF

TQBF has an interactive proof Shamir, Shen.