A verifier for a constraint graph

The verifier of a constraint graph picks an edge at random, reads the symbols its two endpoints carry, and checks the constraint. The proof is the assignment, written as one fixed-width block per vertex, so the queries are the two blocks.

This module packages the algorithmic content a graph must supply — how many edges, the endpoints of an edge, and the constraint — and turns it into a PCPVerifier. Nothing here is about the graph's quality: completeness and soundness are hypotheses on the supplied data, discharged elsewhere by Dinur's amplification.

Main definitions

• Complexity.AlgCSP — a constraint graph presented algorithmically

Main results

• Complexity.AlgCSP.cntU_mem_FP, Complexity.AlgCSP.posU_mem_FP — the query list is polynomial-time describable
• Complexity.AlgCSP.verifier — the verifier itself
• Complexity.mem_PCP_of_algCSP — a constraint graph with a gap puts its language in PCP

structure Complexity.AlgCSP : Type

A constraint graph presented the way an algorithm sees it: a count of edges, the endpoints of each edge, and a decidable constraint. Indices are handled in unary, which is what a polynomial-time loop can carry.

• numEdges : List Bool → ℕ

  How many edges the graph on this input has.

• numEdges_mem : (fun (x : List Bool) => List.replicate (self.numEdges x) true) ∈ FP

  The edge count is polynomial-time computable in unary.

• width : ℕ

  The number of bits a symbol occupies.

• width_pos : 0 < self.width

  A symbol occupies at least one bit.

• vert : Bool → List Bool → ℕ → ℕ

  The endpoints of an edge: false for the first, true for the second.

• vert_mem (b : Bool) : (fun (w : List Bool) => List.replicate (self.vert b (pairFst w) (pairSnd w).length) true) ∈ FP

  The endpoints are polynomial-time computable in unary.

• ok : Language

  The constraint, on pair (pair x (unary e)) (the two symbol blocks).

• ok_mem : self.ok ∈ P

  The constraint is polynomial-time decidable.

def Complexity.AlgCSP.edgeIdx (z : List Bool) : ℕ

The edge a coin string names.

Equations

• Complexity.AlgCSP.edgeIdx z = Complexity.binValLE (Complexity.pairSnd z)

noncomputable def Complexity.AlgCSP.edgeU (p : Polynomial ℕ) (z : List Bool) : List Bool

That index in unary, as far as the clamp allows.

Equations

• Complexity.AlgCSP.edgeU p z = Complexity.unaryVal p z

theorem Complexity.AlgCSP.edgeU_mem_FP (p : Polynomial ℕ) : edgeU p ∈ FP

theorem Complexity.AlgCSP.edgeU_eq (p : Polynomial ℕ) {z : List Bool} (h : 2 ^ (pairSnd z).length ≤ Polynomial.eval z.length p) : edgeU p z = List.replicate (edgeIdx z) true

noncomputable def Complexity.AlgCSP.inRange (A : AlgCSP) (p : Polynomial ℕ) (z : List Bool) : List Bool

Is the named edge a real one?

Equations

• A.inRange p z = Complexity.Cobham.lenLeFlag (List.replicate (A.numEdges (Complexity.pairFst z)) true) (true :: Complexity.AlgCSP.edgeU p z)

theorem Complexity.AlgCSP.inRange_mem_FP (A : AlgCSP) (p : Polynomial ℕ) : A.inRange p ∈ FP

theorem Complexity.AlgCSP.inRange_eq_true_iff (A : AlgCSP) (p : Polynomial ℕ) {z : List Bool} (h : 2 ^ (pairSnd z).length ≤ Polynomial.eval z.length p) : A.inRange p z = [true] ↔ edgeIdx z < A.numEdges (pairFst z)

noncomputable def Complexity.AlgCSP.cntU (A : AlgCSP) (p : Polynomial ℕ) (z : List Bool) : List Bool

How many queries the verifier makes: both symbol blocks, or none when the coin string names no edge.

Equations

• A.cntU p z = Complexity.Cobham.selectHead (A.inRange p z) (List.replicate (2 * A.width) true) []

theorem Complexity.AlgCSP.cntU_mem_FP (A : AlgCSP) (p : Polynomial ℕ) : A.cntU p ∈ FP

Where the verifier looks

noncomputable def Complexity.AlgCSP.vertU (A : AlgCSP) (p : Polynomial ℕ) (b : Bool) (w : List Bool) : List Bool

The endpoint a query index refers to: the first for the low half of the queries, the second for the high half.

Equations

• A.vertU p b w = List.replicate (A.vert b (Complexity.pairFst (Complexity.pairFst w)) (Complexity.AlgCSP.edgeU p (Complexity.pairFst w)).length) true

theorem Complexity.AlgCSP.vertU_mem_FP (A : AlgCSP) (p : Polynomial ℕ) (b : Bool) : A.vertU p b ∈ FP

def Complexity.AlgCSP.lowFlag (A : AlgCSP) (w : List Bool) : List Bool

Is this query in the low half?

Equations

• A.lowFlag w = Complexity.Cobham.lenLeFlag (List.replicate A.width true) (true :: Complexity.pairSnd w)

theorem Complexity.AlgCSP.lowFlag_mem_FP (A : AlgCSP) : A.lowFlag ∈ FP

theorem Complexity.AlgCSP.lowFlag_eq_true_iff (A : AlgCSP) (w : List Bool) : A.lowFlag w = [true] ↔ (pairSnd w).length < A.width

def Complexity.AlgCSP.offU (A : AlgCSP) (w : List Bool) : List Bool

The offset inside the symbol block.

Equations

• A.offU w = Complexity.Cobham.selectHead (A.lowFlag w) (Complexity.pairSnd w) (List.drop A.width (Complexity.pairSnd w))

theorem Complexity.AlgCSP.offU_mem_FP (A : AlgCSP) : A.offU ∈ FP

noncomputable def Complexity.AlgCSP.posU (A : AlgCSP) (p : Polynomial ℕ) (w : List Bool) : List Bool

The position a query reads, in unary.

Equations

• A.posU p w = List.replicate ((Complexity.Cobham.selectHead (A.lowFlag w) (A.vertU p false w) (A.vertU p true w)).length * A.width) true ++ List.replicate (A.offU w).length true

theorem Complexity.AlgCSP.posU_mem_FP (A : AlgCSP) (p : Polynomial ℕ) : A.posU p ∈ FP

theorem Complexity.AlgCSP.cntU_eq_replicate (A : AlgCSP) (p : Polynomial ℕ) (z : List Bool) : A.cntU p z = List.replicate (A.cntU p z).length true

theorem Complexity.AlgCSP.posU_eq_replicate (A : AlgCSP) (p : Polynomial ℕ) (w : List Bool) : A.posU p w = List.replicate (A.posU p w).length true

The verifier

noncomputable def Complexity.AlgCSP.cnt (A : AlgCSP) (p : Polynomial ℕ) (z : List Bool) : ℕ

How many queries, as a number.

Equations

• A.cnt p z = (A.cntU p z).length

noncomputable def Complexity.AlgCSP.pos (A : AlgCSP) (p : Polynomial ℕ) (z : List Bool) (i : ℕ) : ℕ

The i-th query position, as a number.

Equations

• A.pos p z i = (A.posU p (Complexity.pair z (List.replicate i true))).length

noncomputable def Complexity.AlgCSP.okArg (p : Polynomial ℕ) (z : List Bool) : List Bool

The argument the constraint is asked about.

Equations

• Complexity.AlgCSP.okArg p z = Complexity.pair (Complexity.pair (Complexity.pairFst (Complexity.pairFst z)) (Complexity.AlgCSP.edgeU p (Complexity.pairFst z))) (Complexity.pairSnd z)

theorem Complexity.AlgCSP.okArg_mem_FP (p : Polynomial ℕ) : okArg p ∈ FP

noncomputable def Complexity.AlgCSP.verdictLang (A : AlgCSP) (p : Polynomial ℕ) : Language

The verdict: accept unless the coin string names a real edge whose constraint fails.

Equations

• A.verdictLang p = {z : List Bool | A.inRange p (Complexity.pairFst z) = [true] → Complexity.AlgCSP.okArg p z ∈ A.ok}

theorem Complexity.AlgCSP.verdictLang_mem_P (A : AlgCSP) (p : Polynomial ℕ) : A.verdictLang p ∈ P

theorem Complexity.AlgCSP.cnt_le (A : AlgCSP) (p : Polynomial ℕ) (z : List Bool) : A.cnt p z ≤ 2 * A.width

noncomputable def Complexity.AlgCSP.verifier (A : AlgCSP) (p : Polynomial ℕ) : PCPVerifier

The verifier of a constraint graph.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.AlgCSP.positions_verifier (A : AlgCSP) (p : Polynomial ℕ) (x ρ : List Bool) : (A.verifier p).positions x ρ = List.map (A.pos p (pair x ρ)) (List.range (A.cnt p (pair x ρ)))

theorem Complexity.AlgCSP.verifier_queryBounded (A : AlgCSP) (p : Polynomial ℕ) : (A.verifier p).QueryBounded fun (x : ℕ) => 2 * A.width

theorem Complexity.AlgCSP.mem_verdict_verifier (A : AlgCSP) (p : Polynomial ℕ) (z : List Bool) : z ∈ (A.verifier p).verdict ↔ A.inRange p (pairFst z) = [true] → okArg p z ∈ A.ok

What the verifier reads and decides

def Complexity.AlgCSP.posVal (A : AlgCSP) (x : List Bool) (e i : ℕ) : ℕ

The position query i reads, as a function of the edge alone.

Equations

• A.posVal x e i = A.vert (decide ¬i < A.width) x e * A.width + if i < A.width then i else i - A.width

theorem Complexity.AlgCSP.pos_eq (A : AlgCSP) (p : Polynomial ℕ) {x ρ : List Bool} (h : 2 ^ ρ.length ≤ Polynomial.eval (pair x ρ).length p) (i : ℕ) : A.pos p (pair x ρ) i = A.posVal x (binValLE ρ) i

def Complexity.AlgCSP.Sat (A : AlgCSP) (x π : List Bool) (e : ℕ) : Prop

Edge e is satisfied by the proof π.

Equations

• A.Sat x π e = (Complexity.pair (Complexity.pair x (List.replicate e true)) (Complexity.PCPVerifier.answers π (List.map (A.posVal x e) (List.range (2 * A.width)))) ∈ A.ok)

theorem Complexity.AlgCSP.cnt_eq_of_inRange (A : AlgCSP) (p : Polynomial ℕ) {z : List Bool} (h : A.inRange p z = [true]) : A.cnt p z = 2 * A.width

theorem Complexity.AlgCSP.accepts_verifier_iff (A : AlgCSP) (p : Polynomial ℕ) {x ρ : List Bool} (h : 2 ^ ρ.length ≤ Polynomial.eval (pair x ρ).length p) (π : List Bool) : (A.verifier p).Accepts x π ρ ↔ binValLE ρ < A.numEdges x → A.Sat x π (binValLE ρ)

What the verifier decides. It accepts unless the coin string names a real edge that the proof fails to satisfy.

How often the verifier accepts

theorem Complexity.AlgCSP.acceptEvent_eq (A : AlgCSP) (p : Polynomial ℕ) {x : List Bool} {T : ℕ} (h : 2 ^ T ≤ Polynomial.eval (2 * x.length + 2 + T) p) (π : List Bool) : (A.verifier p).acceptEvent T x π = {ρ : Fin T → Bool | PCPVerifier.coinIndex ρ < A.numEdges x → A.Sat x π (PCPVerifier.coinIndex ρ)}

theorem Complexity.AlgCSP.card_reject (A : AlgCSP) {x : List Bool} {T : ℕ} (hN : A.numEdges x ≤ 2 ^ T) (π : List Bool) : {ρ : Fin T → Bool | PCPVerifier.coinIndex ρ < A.numEdges x → A.Sat x π (PCPVerifier.coinIndex ρ)}ᶜ.card = {e ∈ Finset.range (A.numEdges x) | ¬A.Sat x π e}.card

theorem Complexity.AlgCSP.eventProb_eq_one (A : AlgCSP) (p : Polynomial ℕ) {x : List Bool} {T : ℕ} (h : 2 ^ T ≤ Polynomial.eval (2 * x.length + 2 + T) p) (hN : A.numEdges x ≤ 2 ^ T) {π : List Bool} (hsat : ∀ e < A.numEdges x, A.Sat x π e) : eventProb ((A.verifier p).acceptEvent T x π) = 1

Perfect completeness. A proof satisfying every edge is always accepted.

theorem Complexity.AlgCSP.eventProb_le (A : AlgCSP) (p : Polynomial ℕ) {x : List Bool} {T : ℕ} {gap : ℚ} (h : 2 ^ T ≤ Polynomial.eval (2 * x.length + 2 + T) p) (hN : A.numEdges x ≤ 2 ^ T) (hT : 2 ^ T ≤ 2 * A.numEdges x) {π : List Bool} (hs : ↑(Finset.filter (A.Sat x π) (Finset.range (A.numEdges x))).card ≤ (1 - gap) * ↑(A.numEdges x)) : eventProb ((A.verifier p).acceptEvent T x π) ≤ 1 - gap / 2

Soundness. If no proof satisfies more than a 1 - gap fraction of the edges, the verifier accepts with probability at most 1 - gap / 2.

theorem Complexity.mem_PCP_of_algCSP (A : AlgCSP) (p : Polynomial ℕ) (t : ℕ → ℕ) (ht : (fun (x : List Bool) => List.replicate (t x.length) true) ∈ FP) (hclamp : ∀ (n : ℕ), 2 ^ t n ≤ Polynomial.eval (2 * n + 2 + t n) p) (hN : ∀ (x : List Bool), A.numEdges x ≤ 2 ^ t x.length) (hT : ∀ (x : List Bool), 2 ^ t x.length ≤ 2 * A.numEdges x) {L : Language} {gap : ℚ} (hgap0 : 0 < gap) (hgap1 : gap ≤ 1) (hcomp : ∀ x ∈ L, ∃ (π : List Bool), ∀ e < A.numEdges x, A.Sat x π e) (hsound : ∀ x ∉ L, ∀ (π : List Bool), ↑(Finset.filter (A.Sat x π) (Finset.range (A.numEdges x))).card ≤ (1 - gap) * ↑(A.numEdges x)) : ∃ (j : ℕ), L ∈ PCP (fun (n : ℕ) => 2 ^ j * t n) fun (x : ℕ) => 2 ^ j * (2 * A.width)

A constraint graph with a gap puts its language in PCP. Completeness and soundness are hypotheses on the graph: a member has an assignment satisfying every edge, and a non-member has none satisfying more than a 1 - gap fraction.