The machine verifier for quantified Boolean formulas

The verifier of the interactive proof for TQBF as a program with fair coins and word messages, realized by a strict oracle PPT machine (Cslib.Complexity.QBFProtocol.isOraclePPTOn_verifier). On a formula ψ it rejects when ψ has a free variable. Otherwise it computes the list xs of the variable components of all the tokens of ψ, with multiplicity and with 0 for the tokens without a variable (Cslib.Complexity.QBFProtocol.linVars), which contains every variable of ψ; the degree bound D = 2 * size ψ; and the greatest prime p at most 2 * B for B = 12 * size ψ ^ 2 * (size ψ + 1), found by trial division (Cslib.Complexity.QBFProtocol.modulus); by Bertrand's postulate B < p. It then runs a stack machine over the tokens of the arithmetization of ψ that linearizes the variables of xs after every quantifier (Cslib.Complexity.QBFProtocol.Machine.loop), one token per step (Cslib.Complexity.QBFProtocol.Machine.step), checking the claim that the arithmetization has value 1 at the origin over ZMod p:

• a state holds the remaining tokens, the stack of pending claims, each a point and a value, and whether every check so far passed;
• a variable or a constant checks the claim on top of the stack, and a negation replaces its value c by 1 - c;
• a binary connective or an operator sends the remaining tokens and the point of the top claim, reads D + 1 rows of width p bits of the reply, and proceeds as Cslib.Complexity.QBFProtocol.verifyAt; an operator draws its random point by Cslib.Complexity.QBFProtocol.sampleMod.

Points and values are rebuilt modulo p on the variables of xs whenever they are pushed, so that every step adds at most a polynomial amount of storage (Cslib.Complexity.QBFProtocol.Machine.length_encVState_le_of_mem_support_step).

Main definitions

• Cslib.Complexity.QBFProtocol.Machine.step, Cslib.Complexity.QBFProtocol.Machine.loop: the stack machine.
• Cslib.Complexity.QBFProtocol.loopInput: the parameters and tokens computed from a formula.
• Cslib.Complexity.QBFProtocol.verifier: the verifier.

Main results

• Cslib.Complexity.QBFProtocol.lt_modulus, Cslib.Complexity.QBFProtocol.prime_modulus: the modulus is a prime above the bound.
• Cslib.Complexity.QBFProtocol.isOraclePPTOn_verifier: the verifier is strict oracle PPT.

References

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

States

@[instance_reducible]

instance Cslib.Complexity.QBFProtocol.Machine.instFinEnumKind : FinEnum Logic.PL.ArithQBF.Kind

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Machine.encArithToken : Logic.PL.ArithQBF.Kind × ℕ ↪ List Bool

Tokens of arithmetic formulas, the kind framed before the variable in binary.

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Machine.Params : Type

The parameters of the machine: the variables xs linearized after every quantifier, the modulus less one, so that the modulus is positive, and the degree bound D of every round.

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Machine.LoopInput : Type

The input of the loop: the parameters and the tokens of the arithmetic formula.

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Machine.Claim : Type

A pending claim: a point and a value.

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Machine.encClaim : Claim ↪ List Bool

The encoding of a claim, its value in unary.

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Machine.VState : Type

A state of the machine: the remaining tokens, the stack of pending claims, and whether every check so far passed.

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Machine.encVState : VState ↪ List Bool

The encoding of the states.

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.Machine.StepData : Type

The data of a step: the input of the loop and the current state.

def Cslib.Complexity.QBFProtocol.Machine.StepData.xs (a : StepData) : List ℕ

The variables linearized after every quantifier.

def Cslib.Complexity.QBFProtocol.Machine.StepData.modulus (a : StepData) : ℕ

The modulus, which is positive.

instance Cslib.Complexity.QBFProtocol.Machine.StepData.instNeZeroNatModulus (a : StepData) : NeZero a.modulus

def Cslib.Complexity.QBFProtocol.Machine.StepData.degree (a : StepData) : ℕ

The degree bound of every round.

def Cslib.Complexity.QBFProtocol.Machine.StepData.head (a : StepData) : Logic.PL.ArithQBF.Kind × ℕ

The next token.

def Cslib.Complexity.QBFProtocol.Machine.StepData.top (a : StepData) : Claim

The claim on top of the stack.

def Cslib.Complexity.QBFProtocol.Machine.StepData.below (a : StepData) : List Claim

The claims below the top of the stack.

The step

def Cslib.Complexity.QBFProtocol.Machine.message (a : StepData) : List Bool

The message of a step: the remaining tokens and the point of the claim on top of the stack.

def Cslib.Complexity.QBFProtocol.Machine.reject (a : StepData) : VState

The state after a failed check: the token and the claim are dropped.

def Cslib.Complexity.QBFProtocol.Machine.replyOf (a : StepData) (word : List Bool) : List ℕ

The reply of a step, read as D + 1 residues.

def Cslib.Complexity.QBFProtocol.Machine.binNext (o : Logic.PL.ArithQBF.Connective) (a : StepData) (word : List Bool) : VState

The state after the reply word to a binary connective o: the claimed values of the two arguments are checked against the top claim, then pushed in its place.

def Cslib.Complexity.QBFProtocol.Machine.opCheck (o : Logic.PL.ArithQBF.Operator) (a : StepData) (word : List Bool) : Bool

Whether the reply word to an operator o passes the check against the top claim.

def Cslib.Complexity.QBFProtocol.Machine.opNext (a : StepData) (word : List Bool) (z : ℕ) : VState

The state after the reply word to an operator and the random point z: the claim that the body has the value of the reply at z, with the variable set to z.

noncomputable def Cslib.Complexity.QBFProtocol.Machine.ask (a : StepData) : Probability.WordOracleComp Unit (List Bool)

The reply to the message of a step, of which D + 1 rows are read.

noncomputable def Cslib.Complexity.QBFProtocol.Machine.opCont (o : Logic.PL.ArithQBF.Operator) (a : StepData) (word : List Bool) : Probability.WordOracleComp Unit VState

The continuation of a step on an operator after the reply word.

noncomputable def Cslib.Complexity.QBFProtocol.Machine.stepAt : Logic.PL.ArithQBF.Kind → StepData → Probability.WordOracleComp Unit VState

A step on a token of kind k.

noncomputable def Cslib.Complexity.QBFProtocol.Machine.step (I : LoopInput) (st : VState) : Probability.WordOracleComp Unit VState

One step of the machine: while every check passed and tokens remain, process the next token; otherwise stay put.

def Cslib.Complexity.QBFProtocol.Machine.init (I : LoopInput) : VState

The initial state: all the tokens, and the claim that the formula has value 1 at the origin.

noncomputable def Cslib.Complexity.QBFProtocol.Machine.loop (I : LoopInput) : Probability.WordOracleComp Unit VState

The machine runs one step per token.

The step in polynomial time

The storage of the machine

def Cslib.Complexity.QBFProtocol.Machine.claimBound (I : LoopInput) : ℕ

A bound on the encodings of the claims the machine pushes: points on the variables of xs with values below the modulus, and a value below the modulus.

theorem Cslib.Complexity.QBFProtocol.Machine.length_encVState_le_of_mem_support_step (I : LoopInput) (st : VState) {next : VState} (h : next ∈ OracleComp.support (step I st)) : (encVState next).length ≤ (encVState st).length + (8 * claimBound I + 8)

Every step adds a bounded amount of storage, polynomial in the input of the loop.

The machine in polynomial time

Parameters of a formula

def Cslib.Complexity.QBFProtocol.linVars (ψ : Logic.PL.QBF ℕ) : List ℕ

The variable components of the tokens of a formula, in prefix order, with multiplicity and with 0 for the tokens without a variable. Every variable of the formula occurs in it.

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

The degree bound of every round: twice the size of the formula.

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

The modulus must exceed 12 * size ^ 2 * (size + 1).

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

The modulus: the greatest prime at most twice the bound.

def Cslib.Complexity.QBFProtocol.loopInput (ψ : Logic.PL.QBF ℕ) : Machine.LoopInput

The parameters and tokens of the machine for a formula.

noncomputable def Cslib.Complexity.QBFProtocol.verifier (ψ : Logic.PL.QBF ℕ) : Probability.WordOracleComp Unit Bool

The verifier: reject a formula with a free variable, and otherwise run the machine on the arithmetization and accept when every check passed.

theorem Cslib.Complexity.QBFProtocol.prime_modulus (ψ : Logic.PL.QBF ℕ) : Nat.Prime (modulus ψ) ∧ primeBound ψ < modulus ψ

By Bertrand's postulate, the modulus is a prime above the bound.

theorem Cslib.Complexity.QBFProtocol.lt_modulus (ψ : Logic.PL.QBF ℕ) : primeBound ψ < modulus ψ

The verifier in polynomial time

theorem Cslib.Complexity.QBFProtocol.isOraclePPTOn_verifier : Probability.IsOraclePPTOn encQBF Turing.MultiTapeTM.encBool verifier

The verifier is strict oracle PPT: one fair-coin oracle machine with a polynomial clock realizes it against every stateful prover.