Local tests and their constraint graphs

A local test reads a proof π : P → Γ, a word over the alphabet Γ indexed by positions, at a few positions chosen by a random string r : R, the positions query r i for i : Q, and decides from the symbols read whether to accept. Its acceptance probability acceptProb π is taken over a uniformly random string. This is the shape of the verifier of a probabilistically checkable proof making |Q| queries, and of the testers of the Hadamard code Arora and Barak, Chapter 11.

Such a test becomes a constraint graph Arora and Barak, Chapter 22 (LocalTest.toConstraintGraph): a vertex for every position, carrying a symbol, and a vertex for every random string, carrying the symbols the test is to read on it; for every random string r and query i, an edge from the vertex of r to the position query r i holds when the symbols claimed at r make the test accept and the i-th of them is the symbol at the position. On a random string where the test rejects the proof read off the positions, the claimed symbols either make the test reject or differ from the proof at some query, so one of the edges of the random string is violated. A labelling therefore violates a proportion of the edges at least the rejection probability of the test divided by |Q| (LocalTest.one_sub_acceptProb_le_card_mul_unsatFrac).

Local tests combine: LocalTest.map renames the positions, to run a test on part of a larger proof; LocalTest.and runs two tests on independent random strings and accepts when both do; LocalTest.mix runs a test of a family chosen uniformly at random.

Main definitions

• Cslib.PCP.LocalTest: a test reading a proof at positions chosen by a random string.
• Cslib.PCP.LocalTest.Passes, Cslib.PCP.LocalTest.acceptProb: acceptance on a random string, and its probability.
• Cslib.PCP.LocalTest.map, Cslib.PCP.LocalTest.and, Cslib.PCP.LocalTest.mix: renaming the positions, conjunction, and random choice in a family.
• Cslib.PCP.LocalTest.comapRand, Cslib.PCP.LocalTest.padQueries: adapting coin and query layouts.
• Cslib.PCP.LocalTest.toConstraintGraph: the constraint graph of a local test.
• Cslib.PCP.LocalTest.proofOf: the proof that a labelling of that graph carries at the positions.
• Cslib.PCP.LocalTest.labellingOf: the labelling of that graph by a proof.

Main results

• Cslib.PCP.LocalTest.acceptProb_eq_one_iff: a test accepts with probability one exactly when it passes on every random string.
• Cslib.PCP.LocalTest.acceptProb_and_le_left, Cslib.PCP.LocalTest.acceptProb_and_le_right, Cslib.PCP.LocalTest.acceptProb_mix: acceptance probabilities of combined tests.
• Cslib.PCP.LocalTest.card_filter_not_passes_le_card_unsatEdges, Cslib.PCP.LocalTest.one_sub_acceptProb_le_card_mul_unsatFrac: soundness of the constraint graph, every rejecting random string accounting for a violated edge.
• Cslib.PCP.LocalTest.satisfiable_toConstraintGraph: completeness of the constraint graph.
• Cslib.PCP.LocalTest.unsatFrac_labellingOf: its exact value on the labelling carried by a proof.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

structure Cslib.PCP.LocalTest (P : Type u_1) (R : Type u_2) (Q : Type u_3) (Γ : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A local test on proofs π : P → Γ, words over the alphabet Γ indexed by the positions P: on a random string r : R, it reads the proof at the positions query r i for i : Q, and accepts when Accepts r holds of the symbols read.

• query : R → Q → P

  The position read by the query i on the random string r.

• Accepts : R → (Q → Γ) → Prop

  Whether the test accepts on the random string r, given the symbols read by its queries.

def Cslib.PCP.LocalTest.Passes {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) (π : P → Γ) (r : R) : Prop

The test passes the proof π on the random string r when it accepts the symbols of π at the positions it queries.

Combining tests

def Cslib.PCP.LocalTest.map {P : Type u_1} {P' : Type u_2} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) (f : P → P') : LocalTest P' R Q Γ

The test T run through the renaming f : P → P' of its positions: it reads f (query r i). On a proof indexed by P' it is T run on the part of the proof that f selects.

def Cslib.PCP.LocalTest.comapRand {P : Type u_1} {R : Type u_3} {R' : Type u_4} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) (f : R' → R) : LocalTest P R' Q Γ

Run a test using the random string extracted by f. This does not assert that f preserves the uniform distribution.

def Cslib.PCP.LocalTest.reindexQueries {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Q' : Type u_6} {Γ : Type u_7} (T : LocalTest P R Q Γ) (read : Q' → Q) (use : Q → Q') : LocalTest P R Q' Γ

Replace the query layout by Q': read chooses the old query at each new position, and use selects the answers consumed by the original predicate. A left inverse makes this an exact padding or rearrangement, as expressed by passes_reindexQueries.

def Cslib.PCP.LocalTest.padQueries {P : Type u_1} {R : Type u_3} {Γ : Type u_7} {n m : ℕ} (T : LocalTest P R (Fin (n + 1)) Γ) (h : n + 1 ≤ m) : LocalTest P R (Fin m) Γ

Pad a nonempty query layout to length m, repeating the first query at unused positions. The acceptance predicate ignores those additional answers.

def Cslib.PCP.LocalTest.and {P : Type u_1} {R : Type u_3} {R' : Type u_4} {Q : Type u_5} {Q' : Type u_6} {Γ : Type u_7} (T : LocalTest P R Q Γ) (T' : LocalTest P R' Q' Γ) : LocalTest P (R × R') (Q ⊕ Q') Γ

The conjunction of two tests: on independent random strings r and r', run both tests, making the queries of both, and accept when both accept.

def Cslib.PCP.LocalTest.mix {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {E : Type u_8} (T : E → LocalTest P R Q Γ) : LocalTest P (E × R) Q Γ

The test that runs a uniformly random test of the family T: on the random string (e, r), it runs T e on r.

@[simp]

theorem Cslib.PCP.LocalTest.passes_map {P : Type u_1} {P' : Type u_2} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} {f : P → P'} {π : P' → Γ} {r : R} : (T.map f).Passes π r ↔ T.Passes (π ∘ f) r

@[simp]

theorem Cslib.PCP.LocalTest.passes_comapRand {P : Type u_1} {R : Type u_3} {R' : Type u_4} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} (f : R' → R) (π : P → Γ) (r : R') : (T.comapRand f).Passes π r ↔ T.Passes π (f r)

@[simp]

theorem Cslib.PCP.LocalTest.passes_reindexQueries {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Q' : Type u_6} {Γ : Type u_7} {T : LocalTest P R Q Γ} {read : Q' → Q} {use : Q → Q'} (h : Function.LeftInverse read use) (π : P → Γ) (r : R) : (T.reindexQueries read use).Passes π r ↔ T.Passes π r

@[simp]

theorem Cslib.PCP.LocalTest.passes_padQueries {P : Type u_1} {R : Type u_3} {Γ : Type u_7} {n m : ℕ} (T : LocalTest P R (Fin (n + 1)) Γ) (h : n + 1 ≤ m) (π : P → Γ) (r : R) : (T.padQueries h).Passes π r ↔ T.Passes π r

@[simp]

theorem Cslib.PCP.LocalTest.passes_and {P : Type u_1} {R : Type u_3} {R' : Type u_4} {Q : Type u_5} {Q' : Type u_6} {Γ : Type u_7} {T : LocalTest P R Q Γ} {T' : LocalTest P R' Q' Γ} {π : P → Γ} {r : R × R'} : (T.and T').Passes π r ↔ T.Passes π r.1 ∧ T'.Passes π r.2

@[simp]

theorem Cslib.PCP.LocalTest.passes_mix {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {E : Type u_8} {T : E → LocalTest P R Q Γ} {π : P → Γ} {r : E × R} : (mix T).Passes π r ↔ (T r.1).Passes π r.2

The acceptance probability

noncomputable def Cslib.PCP.LocalTest.acceptProb {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) [Fintype R] (π : P → Γ) : ℝ

The acceptance probability of the test on the proof π: the probability that it passes π on a uniformly random string.

theorem Cslib.PCP.LocalTest.acceptProb_eq_card_div {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) [Fintype R] (π : P → Γ) : T.acceptProb π = ↑{r : R | T.Passes π r}.card / ↑(Fintype.card R)

The acceptance probability is the proportion of the random strings on which the test passes.

theorem Cslib.PCP.LocalTest.one_sub_acceptProb {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) [Fintype R] [Nonempty R] (π : P → Γ) : 1 - T.acceptProb π = ↑{r : R | ¬T.Passes π r}.card / ↑(Fintype.card R)

The rejection probability is the proportion of the random strings on which the test does not pass.

theorem Cslib.PCP.LocalTest.acceptProb_nonneg {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) [Fintype R] (π : P → Γ) : 0 ≤ T.acceptProb π

theorem Cslib.PCP.LocalTest.acceptProb_le_one {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) [Fintype R] (π : P → Γ) : T.acceptProb π ≤ 1

theorem Cslib.PCP.LocalTest.acceptProb_eq_one_iff {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) [Fintype R] [Nonempty R] {π : P → Γ} : T.acceptProb π = 1 ↔ ∀ (r : R), T.Passes π r

A test accepts with probability one exactly when it passes on every random string.

@[simp]

theorem Cslib.PCP.LocalTest.acceptProb_map {P : Type u_1} {P' : Type u_2} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} [Fintype R] (f : P → P') (π : P' → Γ) : (T.map f).acceptProb π = T.acceptProb (π ∘ f)

theorem Cslib.PCP.LocalTest.acceptProb_and_le_left {P : Type u_1} {R : Type u_3} {R' : Type u_4} {Q : Type u_5} {Q' : Type u_6} {Γ : Type u_7} {T : LocalTest P R Q Γ} [Fintype R] [Fintype R'] [Nonempty R'] (T' : LocalTest P R' Q' Γ) (π : P → Γ) : (T.and T').acceptProb π ≤ T.acceptProb π

The conjunction of two tests accepts at most as often as the first one.

theorem Cslib.PCP.LocalTest.acceptProb_and_le_right {P : Type u_1} {R : Type u_3} {R' : Type u_4} {Q : Type u_5} {Q' : Type u_6} {Γ : Type u_7} {T : LocalTest P R Q Γ} [Fintype R] [Fintype R'] [Nonempty R] (T' : LocalTest P R' Q' Γ) (π : P → Γ) : (T.and T').acceptProb π ≤ T'.acceptProb π

The conjunction of two tests accepts at most as often as the second one.

theorem Cslib.PCP.LocalTest.acceptProb_mix {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {E : Type u_8} [Fintype R] [Fintype E] (T : E → LocalTest P R Q Γ) (π : P → Γ) : (mix T).acceptProb π = Finset.univ.expect fun (e : E) => (T e).acceptProb π

The acceptance probability of a random test of a family is the average of the acceptance probabilities of its members.

theorem Cslib.PCP.LocalTest.one_sub_acceptProb_le_card_mul_one_sub_acceptProb_mix {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Q' : Type u_6} {Γ : Type u_7} {E : Type u_8} [Fintype R] [Nonempty R] [Fintype E] [Nonempty E] (S : LocalTest P R Q' Γ) (T : E → LocalTest P R Q Γ) (π : P → Γ) (h : ∀ (r : R), (∀ (e : E), (T e).Passes π r) → S.Passes π r) : 1 - S.acceptProb π ≤ ↑(Fintype.card E) * (1 - (mix T).acceptProb π)

Selecting one of |E| checks loses at most a factor |E| in rejection compared with any test implied by passing all the checks on the same random string. The checks may share coins; independence is unnecessary.

The constraint graph of a local test

def Cslib.PCP.LocalTest.toConstraintGraph {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) : ConstraintGraph (P ⊕ R) (R × Q) (Γ × (Q → Γ))

The constraint graph of a local test Arora and Barak, Chapter 22. Its vertices are the positions, labelled by a symbol, and the random strings, labelled by the symbols the test is to read. For every random string r and query i, the edge (r, i) goes from the vertex of r to the position query r i, and holds when the symbols claimed at r make the test accept and the i-th of them is the symbol of the position. The alphabet Γ × (Q → Γ) serves both kinds of vertices: positions use the first component and random strings the second one.

def Cslib.PCP.LocalTest.proofOf {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (A : P ⊕ R → Γ × (Q → Γ)) (p : P) : Γ

The proof carried by a labelling of the constraint graph of a test: the symbols of the positions.

theorem Cslib.PCP.LocalTest.satisfies_toConstraintGraph {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} {A : P ⊕ R → Γ × (Q → Γ)} {x : R × Q} : T.toConstraintGraph.Satisfies A x ↔ T.Accepts x.1 (A (Sum.inr x.1)).2 ∧ (A (Sum.inr x.1)).2 x.2 = proofOf A (T.query x.1 x.2)

The edge (r, i) holds when the symbols claimed at r make the test accept and the i-th of them is the symbol of the position read.

theorem Cslib.PCP.LocalTest.exists_not_satisfies_of_not_passes {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} [Nonempty Q] {A : P ⊕ R → Γ × (Q → Γ)} {r : R} (h : ¬T.Passes (proofOf A) r) : ∃ (i : Q), ¬T.toConstraintGraph.Satisfies A (r, i)

A random string on which the test does not pass the proof carried by a labelling has a violated edge.

theorem Cslib.PCP.LocalTest.card_filter_not_passes_le_card_unsatEdges {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} [Fintype R] [Fintype Q] [Nonempty Q] (A : P ⊕ R → Γ × (Q → Γ)) : {r : R | ¬T.Passes (proofOf A) r}.card ≤ (T.toConstraintGraph.unsatEdges A).card

Soundness of the constraint graph of a test, counting version: the random strings on which the test does not pass the proof carried by a labelling are at most as many as the edges the labelling violates.

theorem Cslib.PCP.LocalTest.one_sub_acceptProb_le_card_mul_unsatFrac {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Q] (A : P ⊕ R → Γ × (Q → Γ)) : 1 - T.acceptProb (proofOf A) ≤ ↑(Fintype.card Q) * T.toConstraintGraph.unsatFrac A

Soundness of the constraint graph of a test: a labelling violates a proportion of the edges at least the rejection probability of the test on the proof it carries, divided by the number of queries.

def Cslib.PCP.LocalTest.labellingOf {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} (T : LocalTest P R Q Γ) (π : P → Γ) (γ : Γ) : P ⊕ R → Γ × (Q → Γ)

The labelling of the constraint graph of a test by a proof π: every position carries its symbol, and every random string the symbols of π that the test reads on it. The symbol γ fills the components that the constraints do not read.

@[simp]

theorem Cslib.PCP.LocalTest.proofOf_labellingOf {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} (π : P → Γ) (γ : Γ) : proofOf (T.labellingOf π γ) = π

The labelling of the constraint graph by a proof carries that proof.

theorem Cslib.PCP.LocalTest.satisfies_labellingOf {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} {π : P → Γ} {γ : Γ} {x : R × Q} (h : T.Passes π x.1) : T.toConstraintGraph.Satisfies (T.labellingOf π γ) x

The labelling by a proof satisfies the edges of the random strings on which the test passes that proof.

theorem Cslib.PCP.LocalTest.unsatFrac_labellingOf {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Q] (π : P → Γ) (γ : Γ) : T.toConstraintGraph.unsatFrac (T.labellingOf π γ) = 1 - T.acceptProb π

When the claimed answers are read from a proof, every edge at a random string is violated exactly when the test rejects. The violated fraction is therefore the rejection probability.

theorem Cslib.PCP.LocalTest.satisfiable_toConstraintGraph {P : Type u_1} {R : Type u_3} {Q : Type u_5} {Γ : Type u_7} {T : LocalTest P R Q Γ} [Nonempty Γ] {π : P → Γ} (h : ∀ (r : R), T.Passes π r) : T.toConstraintGraph.Satisfiable

Completeness of the constraint graph of a test: if the test passes the proof π on every random string, the labelling by π satisfies the constraint graph.