The interactive proof for quantified Boolean formulas

The protocol of Shamir with Shen's linearization Shamir, Shen, Arora and Barak, Section 8.3, built on the sum-check protocol of Lund, Fortnow, Karloff and Nisan [LFKN92], for an arithmetic formula e with operators ∃, ∀ and linearization (Cslib.Logic.PL.ArithQBF) over a commutative ring F. The verifier (Cslib.Complexity.QBFProtocol.verify) checks a claim e.eval r = c about the value of e at a point r, by recursion on e:

• at a variable or a constant it checks the claim directly, and a negation not e reduces the claim to e.eval r = 1 - c;
• at a binary connective it asks the prover for the values c₁ and c₂ of the two arguments, checks that they combine to c, and checks the claims c₁ and c₂ in turn;
• at an operator binding x it asks the prover for the polynomial s that the restriction of the body to x (Cslib.Logic.PL.ArithQBF.restrict) should be, as a list of coefficients of which it keeps the first degBound x + 1; it checks that the values s 0 and s 1 combine to c, draws z from the sampler, and checks the claim that the body has value s z at r with x set to z.

The verifier is a program with typed calls to the prover (Cslib.ProbOracleComp): each query sends the current subformula and point, each reply is a list of ring elements, and the field elements are drawn from an arbitrary closed probabilistic program sampler. A prover is any stateful probabilistic strategy respond answering the queries, with an arbitrary type of states, and Cslib.ProbOracleComp.acceptProbWith is the probability that the verifier accepts against it; Cslib.Complexity.acceptProb is the case of word queries and replies.

Completeness. The honest prover (Cslib.Complexity.QBFProtocol.honest) answers with the true values and restrictions, and is accepted with probability 1 on every true claim (Cslib.Complexity.QBFProtocol.acceptProb_honest_verify).

Soundness. If the sampler gives every element probability at most ε and F is an integral domain, every prover is accepted on a false claim with probability at most e.roundDegree * ε (Cslib.Complexity.QBFProtocol.acceptProb_verify_le): at an operator, a wrong polynomial agrees with the true restriction, both of degree at most degBound x, on at most degBound x points, and otherwise the claim passed on is false again. For the uniform distribution on a finite field this is e.roundDegree / |F|.

For a closed formula φ, the arithmetization φ.arithmetize xs has value 1 at the origin when φ is true and 0 when it is false (Cslib.Logic.PL.QBF.eval_arithmetize_zero), and its round degrees sum to at most (2 * |xs| + 1) * size φ ^ 2 when xs contains the variables of φ. The claim that it has value 1 at the origin is therefore accepted with probability 1 from a true formula, and with probability at most 3 * size φ ^ 3 / |F| from a false one (Cslib.Complexity.QBFProtocol.acceptProb_honest_of_mem_TQBF, Cslib.Complexity.QBFProtocol.acceptProb_le_of_notMem_TQBF). The efficient machine in the model of Cslib.Complexity.IP realizes a variant of this verifier, Cslib.Complexity.QBFProtocol.verifyAt: it reads D + 1 coefficients in every round, sends the remaining tokens of the formula with every query, and works over a prime field of polynomial size with elements drawn from fair coins, each with probability at most 2 / p (Cslib.Complexity.QBFProtocol.isOraclePPTOn_verifier, Cslib.Complexity.TQBF_mem_IP).

Main definitions

• Cslib.Complexity.QBFProtocol.verify: the verifier.
• Cslib.Complexity.QBFProtocol.honest: the honest prover.

Main results

• Cslib.Complexity.QBFProtocol.acceptProb_honest_verify: perfect completeness.
• Cslib.Complexity.QBFProtocol.acceptProbWith_bind_ite_le_add, Cslib.Complexity.QBFProtocol.acceptProbWith_sample_le: the soundness bounds for one round at a binary connective and at an operator, against an arbitrary oracle.
• Cslib.Complexity.QBFProtocol.acceptProb_verify_le, Cslib.Complexity.QBFProtocol.acceptProb_verify_uniform_le: soundness against every prover.
• Cslib.Complexity.QBFProtocol.acceptProb_honest_arithmetize, Cslib.Complexity.QBFProtocol.acceptProb_arithmetize_le: the protocol for closed quantified Boolean formulas.
• Cslib.Complexity.QBFProtocol.acceptProb_honest_of_mem_TQBF, Cslib.Complexity.QBFProtocol.acceptProb_le_of_notMem_TQBF: the protocol for TQBF over a finite field.

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

Queries

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Query (V F : Type) : Type

A query of the verifier: the subformula whose claim it is checking, and the current point.

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Spec (V F : Type) : Query V F → Type

Every reply of the prover is a list of ring elements.

The verifier

def Cslib.Complexity.QBFProtocol.verify {V F : Type} [DecidableEq V] [CommRing F] [DecidableEq F] (sampler : ProbComp F) : Logic.PL.ArithQBF V → (V → F) → F → ProbOracleComp (Spec V F) Bool

The verifier checking the claim that e has value c at r, drawing ring elements from sampler. At a binary connective the reply [c₁, c₂, …] gives the claimed values of the arguments, and at an operator binding x the first degBound x + 1 elements of the reply are the coefficients of the claimed restriction of the body to x; missing entries count as 0.

Completeness

noncomputable def Cslib.Complexity.QBFProtocol.honestReply {V F : Type} [DecidableEq V] [CommRing F] : Query V F → List F

The reply of the honest prover: the values of the two arguments of a binary connective, and the degBound x + 1 coefficients of the restriction of the body of an operator binding x.

noncomputable def Cslib.Complexity.QBFProtocol.honest {V F : Type} [DecidableEq V] [CommRing F] : Query V F → StateT Unit PMF (List F)

The honest prover, which keeps no state.

theorem Cslib.Complexity.QBFProtocol.acceptProb_honest_verify {V F : Type} [DecidableEq V] [CommRing F] [DecidableEq F] (sampler : ProbComp F) (e : Logic.PL.ArithQBF V) (r : V → F) : ProbOracleComp.acceptProbWith honest (verify sampler e r (Logic.PL.ArithQBF.eval r e)) () = 1

Perfect completeness: the honest prover is accepted on every true claim with probability 1.

Soundness

The two kinds of rounds are bounded once, for an arbitrary oracle, and both verifiers of this directory use these bounds: Cslib.Complexity.QBFProtocol.verify here and Cslib.Complexity.QBFProtocol.verifyAt in Classes.IP.TQBF.Tokens.

theorem Cslib.Complexity.QBFProtocol.acceptProbWith_query_ite_le {Q : Type} {spec : Q → Type} {S : Type} (oracle : (q : Q) → StateT S PMF (spec q)) (q : Q) (check : spec q → Prop) [DecidablePred check] {next : spec q → ProbOracleComp spec Bool} {B : ENNReal} (hnext : ∀ (l : spec q), check l → ∀ (s : S), ProbOracleComp.acceptProbWith oracle (next l) s ≤ B) (s : S) : ProbOracleComp.acceptProbWith oracle (do let l ← ProbOracleComp.query q if check l then next l else pure false) s ≤ B

A checked query: sending q and continuing with next l only when the reply l passes check accepts with probability at most B if, for every passing reply l, next l accepts with probability at most B from every oracle state.

theorem Cslib.Complexity.QBFProtocol.acceptProbWith_bind_ite_le_add {Q : Type} {spec : Q → Type} {S : Type} (oracle : (q : Q) → StateT S PMF (spec q)) {first second : ProbOracleComp spec Bool} {B₁ B₂ : ENNReal} (h : (∀ (s : S), ProbOracleComp.acceptProbWith oracle first s ≤ B₁) ∨ ∀ (s : S), ProbOracleComp.acceptProbWith oracle second s ≤ B₂) (s : S) : ProbOracleComp.acceptProbWith oracle (do let b ← first if b = true then second else pure false) s ≤ B₁ + B₂

The round at a binary connective: running second only after first accepted accepts with probability at most B₁ + B₂ if first accepts with probability at most B₁ or second accepts with probability at most B₂ from every state. At a false claim about a connective, one of the two claims passed on is false.

theorem Cslib.Complexity.QBFProtocol.acceptProbWith_sample_le {F : Type} [CommRing F] (sampler : ProbComp F) {Q : Type} {spec : Q → Type} {S : Type} (oracle : (q : Q) → StateT S PMF (spec q)) [IsDomain F] {ε : ENNReal} (hsampler : ∀ (z : F), sampler.eval z ≤ ε) {p g : Polynomial F} {d : ℕ} (hne : p ≠ g) (hp : p.natDegree ≤ d) (hg : g.natDegree ≤ d) {next : F → ProbOracleComp spec Bool} {B : ENNReal} {s : S} (hnext : ∀ (z : F), Polynomial.eval z p ≠ Polynomial.eval z g → ProbOracleComp.acceptProbWith oracle (next z) s ≤ B) : ProbOracleComp.acceptProbWith oracle (ProbOracleComp.sample sampler >>= next) s ≤ ↑d * ε + B

The round at an operator (the Schwartz–Zippel step of the sum-check protocol): let p be the claimed and g the true restriction of the body, two different polynomials of degree at most d. Drawing z from a sampler that gives every element probability at most ε and continuing with next z accepts with probability at most d * ε + B if next z accepts with probability at most B whenever p and g differ at z: they agree on at most d points.

theorem Cslib.Complexity.QBFProtocol.acceptProb_verify_le {V F : Type} [DecidableEq V] [CommRing F] [DecidableEq F] (sampler : ProbComp F) [IsDomain F] {ε : ENNReal} (hsampler : ∀ (z : F), sampler.eval z ≤ ε) {S : Type} (respond : Query V F → StateT S PMF (List F)) (e : Logic.PL.ArithQBF V) {r : V → F} {c : F} (hc : Logic.PL.ArithQBF.eval r e ≠ c) (s : S) : ProbOracleComp.acceptProbWith respond (verify sampler e r c) s ≤ ↑e.roundDegree * ε

Soundness: over an integral domain, if the sampler gives every element probability at most ε, every prover is accepted on a false claim with probability at most e.roundDegree * ε.

theorem Cslib.Complexity.QBFProtocol.acceptProb_verify_uniform_le {V F : Type} [DecidableEq V] [CommRing F] [DecidableEq F] [IsDomain F] [Fintype F] {S : Type} (respond : Query V F → StateT S PMF (List F)) (e : Logic.PL.ArithQBF V) {r : V → F} {c : F} (hc : Logic.PL.ArithQBF.eval r e ≠ c) (s : S) : ProbOracleComp.acceptProbWith respond (verify (ProbComp.uniform F) e r c) s ≤ ↑e.roundDegree / ↑(Fintype.card F)

Soundness for uniform samples: with ring elements drawn uniformly from a finite integral domain, every prover is accepted on a false claim with probability at most e.roundDegree / |F|.

Quantified Boolean formulas

theorem Cslib.Complexity.QBFProtocol.acceptProb_honest_arithmetize {V F : Type} [DecidableEq V] [CommRing F] [DecidableEq F] (sampler : ProbComp F) (xs : List V) {φ : Logic.PL.QBF V} (hφ : φ.Closed) (htrue : Logic.PL.QBF.eval (fun (x : V) => false) φ = true) : ProbOracleComp.acceptProbWith honest (verify sampler (Logic.PL.QBF.arithmetize xs φ) 0 1) () = 1

Completeness for quantified Boolean formulas: on a true closed formula, the honest prover is accepted with probability 1 on the claim that the arithmetization has value 1 at the origin.

theorem Cslib.Complexity.QBFProtocol.acceptProb_arithmetize_le {V F : Type} [DecidableEq V] [CommRing F] [DecidableEq F] (sampler : ProbComp F) [IsDomain F] {ε : ENNReal} (hsampler : ∀ (z : F), sampler.eval z ≤ ε) {xs : List V} {φ : Logic.PL.QBF V} (hφ : φ.Closed) (hxs : ∀ v ∈ φ.vars, v ∈ xs) (hfalse : Logic.PL.QBF.eval (fun (x : V) => false) φ = false) {S : Type} (respond : Query V F → StateT S PMF (List F)) (s : S) : ProbOracleComp.acceptProbWith respond (verify sampler (Logic.PL.QBF.arithmetize xs φ) 0 1) s ≤ ↑((2 * xs.length + 1) * φ.size ^ 2) * ε

Soundness for quantified Boolean formulas: on a false closed formula whose variables are all in xs, every prover is accepted on the claim that the arithmetization has value 1 at the origin with probability at most (2 * |xs| + 1) * size φ ^ 2 * ε, if the sampler gives every element probability at most ε.

theorem Cslib.Complexity.QBFProtocol.acceptProb_honest_of_mem_TQBF {F : Type} [CommRing F] [DecidableEq F] (sampler : ProbComp F) {φ : Logic.PL.QBF ℕ} (hφ : φ ∈ TQBF) : ProbOracleComp.acceptProbWith honest (verify sampler (Logic.PL.QBF.arithmetize φ.vars φ) 0 1) () = 1

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

theorem Cslib.Complexity.QBFProtocol.acceptProb_le_of_notMem_TQBF {F : Type} [CommRing F] [DecidableEq F] [IsDomain F] [Fintype F] {φ : Logic.PL.QBF ℕ} (hφ : φ.Closed) (hφ' : φ ∉ TQBF) {S : Type} (respond : Query ℕ F → StateT S PMF (List F)) (s : S) : ProbOracleComp.acceptProbWith respond (verify (ProbComp.uniform F) (Logic.PL.QBF.arithmetize φ.vars φ) 0 1) s ≤ ↑(3 * φ.size ^ 3) / ↑(Fintype.card F)

Soundness for TQBF: on a false closed formula φ, with field elements drawn uniformly from a finite field F, every prover is accepted with probability at most 3 * size φ ^ 3 / |F|.