Words of the machine verifier for quantified Boolean formulas

The machine realizing the verifier of Cslib.Complexity.QBFProtocol.verifyAt over ZMod p represents ring elements by natural numbers below p, in unary, which is polynomial since p is chosen of polynomial size. This file gives the arithmetic it performs and its words:

• the operations of the arithmetization modulo p (Cslib.Complexity.QBFProtocol.subMod, Cslib.Complexity.QBFProtocol.connectiveMod, Cslib.Complexity.QBFProtocol.operatorMod) and Horner's rule modulo p (Cslib.Complexity.QBFProtocol.hornerMod), which compute in ZMod p;
• points as lists of pairs of a variable and its value (Cslib.Complexity.QBFProtocol.lookupPt, Cslib.Complexity.QBFProtocol.normPt, Cslib.Complexity.QBFProtocol.updatePt), which agree with the point of the protocol on the variables of a list xs (Cslib.Complexity.QBFProtocol.canonPt);
• the decoding of a reply word as D + 1 rows of width p bits, each read in binary modulo p (Cslib.Complexity.QBFProtocol.decodeReply), and the encoding of a reply by the honest prover (Cslib.Complexity.QBFProtocol.encodeReply), which it inverts;
• the samples, a uniform index in the dyadic range above p reduced modulo p (Cslib.Complexity.QBFProtocol.sampleMod), which give every residue probability at most 2 / p (Cslib.Complexity.QBFProtocol.eval_sampleMod_le) with a fixed number of fair coins.

All are polynomial-time in their unary or binary inputs.

Main definitions

• Cslib.Complexity.QBFProtocol.connectiveMod, Cslib.Complexity.QBFProtocol.operatorMod, Cslib.Complexity.QBFProtocol.hornerMod: arithmetic modulo p.
• Cslib.Complexity.QBFProtocol.canonPt, Cslib.Complexity.QBFProtocol.updatePt, Cslib.Complexity.QBFProtocol.encPt: points and their encoding.
• Cslib.Complexity.QBFProtocol.decodeReply, Cslib.Complexity.QBFProtocol.encodeReply: replies.
• Cslib.Complexity.QBFProtocol.sampleMod: samples.

Main results

• Cslib.Complexity.QBFProtocol.natCast_operatorMod, Cslib.Complexity.QBFProtocol.natCast_hornerMod: the arithmetic computes in ZMod p.
• Cslib.Complexity.QBFProtocol.updatePt_canonPt: updating a point.
• Cslib.Complexity.QBFProtocol.decodeReply_encodeReply: decoding inverts the honest encoding.
• Cslib.Complexity.QBFProtocol.eval_sampleMod_le: the samples are nearly uniform.

References

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

Arithmetic modulo p

def Cslib.Complexity.QBFProtocol.subMod (p a b : ℕ) : ℕ

The difference a - b modulo p.

def Cslib.Complexity.QBFProtocol.connectiveMod (p : ℕ) : Logic.PL.ArithQBF.Connective → ℕ → ℕ → ℕ

The value of a connective on residues modulo p.

def Cslib.Complexity.QBFProtocol.operatorMod (p : ℕ) : Logic.PL.ArithQBF.Operator → ℕ → ℕ → ℕ → ℕ

The value of an operator on residues modulo p.

def Cslib.Complexity.QBFProtocol.hornerMod (p z : ℕ) (l : List ℕ) : ℕ

The value at z of a coefficient list modulo p, by Horner's rule from the last coefficient. The modulus 0 is read as 1, so that the intermediate values stay small.

theorem Cslib.Complexity.QBFProtocol.natCast_subMod {p : ℕ} [NeZero p] (a b : ℕ) : ↑(subMod p a b) = ↑a - ↑b

theorem Cslib.Complexity.QBFProtocol.natCast_connectiveMod {p : ℕ} [NeZero p] (o : Logic.PL.ArithQBF.Connective) (a b : ℕ) : ↑(connectiveMod p o a b) = o.apply ↑a ↑b

theorem Cslib.Complexity.QBFProtocol.natCast_operatorMod {p : ℕ} [NeZero p] (o : Logic.PL.ArithQBF.Operator) (t a b : ℕ) : ↑(operatorMod p o t a b) = o.apply ↑t ↑a ↑b

For p ≠ 0, operatorMod computes the operators of the arithmetization in ZMod p.

theorem Cslib.Complexity.QBFProtocol.natCast_hornerMod {p : ℕ} [NeZero p] (z : ℕ) (l : List ℕ) : ↑(hornerMod p z l) = Polynomial.evalCoeffList (↑z) (List.map Nat.cast l)

For p ≠ 0, Horner's rule modulo p evaluates the coefficient list l at z in ZMod p.

theorem Cslib.Complexity.QBFProtocol.subMod_lt {p : ℕ} [NeZero p] (a b : ℕ) : subMod p a b < p

theorem Cslib.Complexity.QBFProtocol.connectiveMod_lt {p : ℕ} [NeZero p] (o : Logic.PL.ArithQBF.Connective) (a b : ℕ) : connectiveMod p o a b < p

theorem Cslib.Complexity.QBFProtocol.operatorMod_lt {p : ℕ} [NeZero p] (o : Logic.PL.ArithQBF.Operator) (t a b : ℕ) : operatorMod p o t a b < p

theorem Cslib.Complexity.QBFProtocol.hornerMod_lt {p : ℕ} [NeZero p] (z : ℕ) (l : List ℕ) : hornerMod p z l < p

theorem Cslib.Complexity.QBFProtocol.mod_eq_val_mod_iff {p : ℕ} [NeZero p] (a : ℕ) (c : ZMod p) : a % p = c.val % p ↔ ↑a = c

A residue below p compares with an element of ZMod p through its value.

Points

def Cslib.Complexity.QBFProtocol.lookupPt (pt : List (ℕ × ℕ)) (w : ℕ) : ℕ

The value of the variable w at a point given as a list of pairs of a variable and its value: the value of the first pair for w, or 0.

def Cslib.Complexity.QBFProtocol.canonPt {p : ℕ} (xs : List ℕ) (r : ℕ → ZMod p) : List (ℕ × ℕ)

The point r on the variables of xs, as a list of pairs of a variable and its value.

def Cslib.Complexity.QBFProtocol.normPt (p : ℕ) (xs : List ℕ) (pt : List (ℕ × ℕ)) : List (ℕ × ℕ)

A point rebuilt on the variables of xs, with values reduced modulo p.

def Cslib.Complexity.QBFProtocol.updatePt (p : ℕ) (xs : List ℕ) (pt : List (ℕ × ℕ)) (v z : ℕ) : List (ℕ × ℕ)

A point rebuilt on the variables of xs, with the variable v set to z.

theorem Cslib.Complexity.QBFProtocol.lookupPt_canonPt {p : ℕ} {xs : List ℕ} (r : ℕ → ZMod p) {w : ℕ} (hw : w ∈ xs) : lookupPt (canonPt xs r) w = (r w).val

theorem Cslib.Complexity.QBFProtocol.normPt_canonPt {p : ℕ} [NeZero p] (xs : List ℕ) (r : ℕ → ZMod p) : normPt p xs (canonPt xs r) = canonPt xs r

theorem Cslib.Complexity.QBFProtocol.updatePt_canonPt {p : ℕ} [NeZero p] (xs : List ℕ) (r : ℕ → ZMod p) (v z : ℕ) : updatePt p xs (canonPt xs r) v z = canonPt xs (Function.update r v ↑z)

For p ≠ 0, setting the variable v to z in the point r on the variables of xs gives the point Function.update r v z on the same variables.

Replies

def Cslib.Complexity.QBFProtocol.width (p : ℕ) : ℕ

The number of bits of a residue modulo p in a reply.

def Cslib.Complexity.QBFProtocol.replyLimit (p D : ℕ) : ℕ

The number of bits of a reply that the verifier reads: D + 1 rows.

def Cslib.Complexity.QBFProtocol.decodeReply (p D : ℕ) (word : List Bool) : List ℕ

A reply read as D + 1 rows of width p bits, missing bits being false, each row read in binary and reduced modulo p.

def Cslib.Complexity.QBFProtocol.encodeReply (p : ℕ) (l : List ℕ) : List Bool

The reply of the honest prover for a list of residues: their bits, row after row.

theorem Cslib.Complexity.QBFProtocol.length_decodeReply (p D : ℕ) (word : List Bool) : (decodeReply p D word).length = D + 1

theorem Cslib.Complexity.QBFProtocol.lt_of_mem_decodeReply {p : ℕ} [NeZero p] {D : ℕ} {word : List Bool} {a : ℕ} (ha : a ∈ decodeReply p D word) : a < p

theorem Cslib.Complexity.QBFProtocol.decodeReply_encodeReply {p D : ℕ} {l : List ℕ} (hl : ∀ a ∈ l, a < p) (hlen : l.length ≤ D + 1) : decodeReply p D (List.take (replyLimit p D) (encodeReply p l)) = List.map (fun (i : ℕ) => l.getD i 0) (List.range (D + 1))

Decoding inverts the honest encoding of at most D + 1 residues, padded with zeros.

Samples

noncomputable def Cslib.Complexity.QBFProtocol.sampleMod (p : ℕ) : ProbComp ℕ

A uniform index in the dyadic range above p, reduced modulo p.

theorem Cslib.Complexity.QBFProtocol.lt_of_mem_support_sampleMod {p : ℕ} [NeZero p] {n : ℕ} (hn : n ∈ (sampleMod p).eval.support) : n < p

theorem Cslib.Complexity.QBFProtocol.eval_sampleMod_le {p : ℕ} [NeZero p] (n : ℕ) : (sampleMod p).eval n ≤ 2 / ↑p

The samples are nearly uniform: every residue has probability at most 2 / p.

Polynomial time

@[reducible, inline]

abbrev Cslib.Complexity.QBFProtocol.encPt : List (ℕ × ℕ) ↪ List Bool

Points as lists of pairs (x, v) of a variable x in binary and its value v in unary, as lookupPt, normPt and updatePt read them: the pairs are framed and concatenated in order, each with its variable framed.

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_subMod {γ : Type} {encIn : γ ↪ List Bool} {p a b : γ → ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn Turing.MultiTapeTM.encUnary) (hb : Turing.MultiTapeTM.ComputableInPolyTime b encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => subMod (p x) (a x) (b x)) encIn Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_connectiveMod {γ : Type} {encIn : γ ↪ List Bool} (o : Logic.PL.ArithQBF.Connective) {p a b : γ → ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn Turing.MultiTapeTM.encUnary) (hb : Turing.MultiTapeTM.ComputableInPolyTime b encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => connectiveMod (p x) o (a x) (b x)) encIn Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_operatorMod {γ : Type} {encIn : γ ↪ List Bool} (o : Logic.PL.ArithQBF.Operator) {p t a b : γ → ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn Turing.MultiTapeTM.encUnary) (hb : Turing.MultiTapeTM.ComputableInPolyTime b encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => operatorMod (p x) o (t x) (a x) (b x)) encIn Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_hornerMod {γ : Type} {encIn : γ ↪ List Bool} {p z : γ → ℕ} {l : γ → List ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (hz : Turing.MultiTapeTM.ComputableInPolyTime z encIn Turing.MultiTapeTM.encUnary) (hl : Turing.MultiTapeTM.ComputableInPolyTime l encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => hornerMod (p x) (z x) (l x)) encIn Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_lookupPt {γ : Type} {encIn : γ ↪ List Bool} {pt : γ → List (ℕ × ℕ)} {w : γ → ℕ} (hpt : Turing.MultiTapeTM.ComputableInPolyTime pt encIn encPt) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => lookupPt (pt x) (w x)) encIn Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_normPt {γ : Type} {encIn : γ ↪ List Bool} {p : γ → ℕ} {xs : γ → List ℕ} {pt : γ → List (ℕ × ℕ)} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (hxs : Turing.MultiTapeTM.ComputableInPolyTime xs encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hpt : Turing.MultiTapeTM.ComputableInPolyTime pt encIn encPt) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => normPt (p x) (xs x) (pt x)) encIn encPt

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_updatePt {γ : Type} {encIn : γ ↪ List Bool} {p : γ → ℕ} {xs : γ → List ℕ} {pt : γ → List (ℕ × ℕ)} {v z : γ → ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (hxs : Turing.MultiTapeTM.ComputableInPolyTime xs encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hpt : Turing.MultiTapeTM.ComputableInPolyTime pt encIn encPt) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encNat) (hz : Turing.MultiTapeTM.ComputableInPolyTime z encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => updatePt (p x) (xs x) (pt x) (v x) (z x)) encIn encPt

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_width {γ : Type} {encIn : γ ↪ List Bool} {p : γ → ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => width (p x)) encIn Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_replyLimit {γ : Type} {encIn : γ ↪ List Bool} {p D : γ → ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (hD : Turing.MultiTapeTM.ComputableInPolyTime D encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => replyLimit (p x) (D x)) encIn Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.QBFProtocol.computableInPolyTime_decodeReply {γ : Type} {encIn : γ ↪ List Bool} {p D : γ → ℕ} {word : γ → List Bool} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (hD : Turing.MultiTapeTM.ComputableInPolyTime D encIn Turing.MultiTapeTM.encUnary) (hword : Turing.MultiTapeTM.ComputableInPolyTime word encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => decodeReply (p x) (D x) (word x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)

theorem Cslib.Complexity.QBFProtocol.isPPTOn_sampleMod {γ : Type} {encIn : γ ↪ List Bool} {p : γ → ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn encIn Turing.MultiTapeTM.encUnary fun (x : γ) => sampleMod (p x)

The samples are strict PPT in a unary modulus.