The interactive proof for quantified Boolean formulas, on a stream of tokens

A machine running the verifier of Cslib.Complexity.QBFProtocol.verify reads the arithmetic formula as a list of tokens in prefix order (Cslib.Logic.PL.ArithQBF.tokens): the claims it has still to check form a stack, and the claim on top of the stack is about the subformula whose tokens start the remaining list. The arithmetization of a quantified Boolean formula φ has as tokens those of φ, with the linearizations of the variables of xs inserted before every quantifier (Cslib.Logic.PL.QBF.tokens_arithmetize).

This file gives the recursive form of that machine (Cslib.Complexity.QBFProtocol.verifyAt). It differs from Cslib.Complexity.QBFProtocol.verify in two ways: it reads the same number D + 1 of coefficients in every round, so that it need not compute the degree of each body, and its queries also carry the tokens that follow the current subformula, so that they determine the remaining list of tokens of the machine. Its soundness bound uses the uniform degree: if the syntactic largest round degree maxRoundDegree e is at most D, every prover is accepted on a false claim with probability at most ops e * D * ε instead of roundDegree e * ε (Cslib.Complexity.QBFProtocol.acceptProb_verifyAt_le), with ops e the number of operators. A stateless prover whose replies agree with the true values and restrictions on every query about a subformula all of whose variables lie in a list xs is accepted with certainty on every true claim about a formula whose variables lie in xs and whose largest round degree maxRoundDegree e is at most D (Cslib.Complexity.QBFProtocol.run_verifyAt_of_agreesAt).

Main definitions

• Cslib.Logic.PL.ArithQBF.Kind, Cslib.Logic.PL.ArithQBF.tokens: the tokens of an arithmetic formula.
• Cslib.Logic.PL.QBF.expandToken: the tokens of the arithmetization for a token of a formula.
• Cslib.Complexity.QBFProtocol.verifyAt: the verifier with uniform degree and contextual queries.
• Cslib.Complexity.QBFProtocol.honestReplyAt: the honest replies.

Main results

• Cslib.Logic.PL.ArithQBF.tokens_append_inj: tokens in prefix order determine the formula.
• Cslib.Logic.PL.QBF.tokens_arithmetize: the tokens of the arithmetization.
• Cslib.Complexity.QBFProtocol.acceptProb_verifyAt_le: soundness.
• Cslib.Complexity.QBFProtocol.run_verifyAt_of_agreesAt: perfect completeness.

References

• A. Shamir, IP = PSPACE
• A. Shen, IP = SPACE: simplified proof
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Tokens

inductive Cslib.Logic.PL.ArithQBF.Kind : Type

The kinds of nodes of an arithmetic formula.

• var : Kind

  A variable.

• top : Kind

  The constant 1.

• bot : Kind

  The constant 0.

• not : Kind

  Negation.

• and : Kind

  Conjunction.

• or : Kind

  Disjunction.

• ex : Kind

  Existential quantification.

• all : Kind

  Universal quantification.

• lin : Kind

  Linearization.

@[instance_reducible]

instance Cslib.Logic.PL.ArithQBF.instDecidableEqKind : DecidableEq Kind

@[instance_reducible]

instance Cslib.Logic.PL.instFintypeKind : Fintype ArithQBF.Kind

def Cslib.Logic.PL.ArithQBF.tokens : ArithQBF ℕ → List (Kind × ℕ)

The tokens of an arithmetic formula in prefix order: the kind of each node, with its variable for variables and operators, and 0 for the other nodes.

def Cslib.Logic.PL.ArithQBF.readToken : Kind × ℕ → Option (PrefixParser.Step (ArithQBF ℕ))

Interpret an arithmetic-formula token as its constructor, rejecting nonzero payloads on constants and connectives.

theorem Cslib.Logic.PL.ArithQBF.parseFuel_tokens (e : ArithQBF ℕ) (rest : List (Kind × ℕ)) (fuel : ℕ) (hf : e.tokens.length ≤ fuel) : PrefixParser.parseFuel readToken fuel (e.tokens ++ rest) = some (e, rest)

Parsing an arithmetic formula's tokens recovers it and leaves the suffix untouched.

theorem Cslib.Logic.PL.ArithQBF.tokens_append_inj {e e' : ArithQBF ℕ} {r r' : List (Kind × ℕ)} (h : e.tokens ++ r = e'.tokens ++ r') : e = e' ∧ r = r'

Tokens in prefix order determine the formula, and what follows them.

def Cslib.Logic.PL.QBF.Kind.arith : Kind → ArithQBF.Kind

The kind of the node of the arithmetization for a node of a quantified Boolean formula.

def Cslib.Logic.PL.QBF.Kind.isQuantifier : Kind → Bool

Whether a kind of nodes is a quantifier.

def Cslib.Logic.PL.QBF.expandToken (xs : List ℕ) (t : Kind × ℕ) : List (ArithQBF.Kind × ℕ)

The tokens of the arithmetization for a token of a formula: a quantifier is preceded by the linearizations of the variables of xs.

theorem Cslib.Logic.PL.QBF.tokens_arithmetize (xs : List ℕ) (φ : QBF ℕ) : (arithmetize xs φ).tokens = List.flatMap (expandToken xs) φ.tokens

The tokens of the arithmetization are those of the formula, with the linearizations of the variables of xs inserted before every quantifier.

The verifier on a stream of tokens

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.QueryAt (F : Type) : Type

A query of the verifier on a stream of tokens: the current subformula, the tokens that follow it, and the current point.

def Cslib.Complexity.QBFProtocol.verifyAt {F : Type} [CommRing F] [DecidableEq F] (sampler : ProbComp F) (D : ℕ) : Logic.PL.ArithQBF ℕ → List (Logic.PL.ArithQBF.Kind × ℕ) → (ℕ → F) → F → ProbOracleComp (fun (x : QueryAt F) => List F) Bool

The verifier on a stream of tokens, checking the claim that e, followed by the tokens rest, has value c at r. It is Cslib.Complexity.QBFProtocol.verify with D + 1 coefficients read in every round and with the tokens rest sent along with every query.

Soundness

theorem Cslib.Complexity.QBFProtocol.acceptProb_verifyAt_le {F : Type} [CommRing F] [DecidableEq F] (sampler : ProbComp F) (D : ℕ) [IsDomain F] {ε : ENNReal} (hsampler : ∀ (z : F), sampler.eval z ≤ ε) {S : Type} (respond : QueryAt F → StateT S PMF (List F)) (e : Logic.PL.ArithQBF ℕ) (hD : e.maxRoundDegree ≤ D) {rest : List (Logic.PL.ArithQBF.Kind × ℕ)} {r : ℕ → F} {c : F} (hc : Logic.PL.ArithQBF.eval r e ≠ c) (s : S) : ProbOracleComp.acceptProbWith respond (verifyAt sampler D e rest r c) s ≤ ↑(e.ops * D) * ε

Soundness of the verifier on a stream of tokens: if the sampler gives every element probability at most ε and the body of every operator of e has degree at most D in its variable, every prover is accepted on a false claim with probability at most ops e * D * ε.

Completeness

noncomputable def Cslib.Complexity.QBFProtocol.honestReplyAt {F : Type} [CommRing F] (D : ℕ) (e : Logic.PL.ArithQBF ℕ) (r : ℕ → F) : List F

The honest reply to a query about e at r: the values of the two arguments of a binary connective, and the D + 1 first coefficients of the restriction of the body of an operator.

def Cslib.Complexity.QBFProtocol.AgreesAt {F : Type} [CommRing F] (D : ℕ) (l : List F) (e : Logic.PL.ArithQBF ℕ) (r : ℕ → F) : Prop

A reply agrees with the honest reply to a query about e at r on what the verifier reads: the first two entries for a binary connective, the first D + 1 for an operator.

theorem Cslib.Complexity.QBFProtocol.agreesAt_honestReplyAt {F : Type} [CommRing F] (D : ℕ) (e : Logic.PL.ArithQBF ℕ) (r : ℕ → F) : AgreesAt D (honestReplyAt D e r) e r

theorem Cslib.Complexity.QBFProtocol.run_verifyAt_of_agreesAt {F : Type} [CommRing F] [DecidableEq F] (sampler : ProbComp F) (D : ℕ) (f : QueryAt F → List F) (xs : List ℕ) (hf : ∀ (e' : Logic.PL.ArithQBF ℕ) (rest' : List (Logic.PL.ArithQBF.Kind × ℕ)) (r' : ℕ → F), (∀ w ∈ e'.vars, w ∈ xs) → AgreesAt D (f (e', rest', r')) e' r') (e : Logic.PL.ArithQBF ℕ) (he : ∀ w ∈ e.vars, w ∈ xs) (hD : e.maxRoundDegree ≤ D) (rest : List (Logic.PL.ArithQBF.Kind × ℕ)) (r : ℕ → F) (s : Unit) : ProbOracleComp.runWith (fun (q : QueryAt F) (s : Unit) => PMF.pure (f q, s)) (verifyAt sampler D e rest r (Logic.PL.ArithQBF.eval r e)) s = PMF.pure (true, s)

Perfect completeness of the verifier on a stream of tokens. A stateless prover whose reply to every query about a subformula all of whose variables lie in xs agrees with the honest reply makes the verifier accept with certainty every true claim about a formula whose variables lie in xs and whose operators have bodies of degree at most D in their variable.