The witness layout of a PCP verifier

A witness for a PCP verifier is a table of answers, one fixed-width block per coin string. This module fixes that layout and reads it back: the block for a coin string, cut down to the number of queries actually made, is exactly the answer list SubsetNP.tableOf names.

It also records that the query bound can be taken to be a constant. A bound q =O 1 need not be a computable function, but it is eventually bounded and takes finitely many values before that, so a single number bounds every query list — which is what an algorithm can actually use.

Main definitions

• Complexity.wBlock — the witness block for one coin string

Main results

• Complexity.exists_const_query_bound — a constant bounds every query list
• Complexity.tableOf_eq_wBlock — the block is the answer list
• Complexity.accLang_mem_P — checking every coin string is polynomial time

theorem Complexity.exists_const_query_bound {V : PCPVerifier} {q : ℕ → ℕ} (hV : V.QueryBounded q) (hq : BigO q fun (x : ℕ) => 1) : ∃ (K : ℕ), ∀ (x ρ : List Bool), (V.positions x ρ).length ≤ K

A constant bounds every query list. This is what makes the witness layout uniform: each block has the same fixed width.

def Complexity.wBlock (w : List Bool) (start len : ℕ) : List Bool

The witness block starting at start and holding len answers.

Equations

• Complexity.wBlock w start len = List.take len (List.drop start w)

theorem Complexity.wBlock_mem_FP {w s l : List Bool → List Bool} (hw : w ∈ FP) (hs : s ∈ FP) (hl : l ∈ FP) : (fun (z : List Bool) => wBlock (w z) (s z).length (l z).length) ∈ FP

theorem Complexity.length_wBlock {w : List Bool} {start len : ℕ} (h : start + len ≤ w.length) : (wBlock w start len).length = len

theorem Complexity.getElem_wBlock {w : List Bool} {start len : ℕ} (h : start + len ≤ w.length) {i : ℕ} (hi : i < len) : (wBlock w start len)[i] = w.getD (start + i) false

theorem Complexity.tableOf_eq_wBlock (V : PCPVerifier) (t Q : ℕ) (x w : List Bool) (ρ : Fin t → Bool) (h : PCPVerifier.coinIndex ρ * Q + (V.positions x (BitString.toList ρ)).length ≤ w.length) : V.tableOf t Q x w ρ = wBlock w (PCPVerifier.coinIndex ρ * Q) (V.positions x (BitString.toList ρ)).length

The block is the answer list. With the answers for coin index c laid out in the slots c * Q, …, the witness block is exactly the table SubsetNP.tableOf reads.

theorem Complexity.wBlock_one {w : List Bool} {k : ℕ} (h : k < w.length) : wBlock w k 1 = [w.getD k false]

A one-bit block is the bit it holds.

theorem Complexity.getElem?_tableOf (V : PCPVerifier) (t Q : ℕ) (x w : List Bool) (ρ : Fin t → Bool) {i : ℕ} (hi : i < (V.positions x (BitString.toList ρ)).length) : (V.tableOf t Q x w ρ)[i]? = some (w.getD (PCPVerifier.coinIndex ρ * Q + i) false)

Reading a slot of the table.

Acceptance on every coin string

The check is a loop over coin indices. Each iteration recovers the coin string from its index, reads the verifier's query list to learn how many answers this coin string uses, cuts that many out of the witness block, and asks the verdict.

def Complexity.accX (y : List Bool) : List Bool

The input of one iteration is pair (pair x w) (unary c).

Equations

• Complexity.accX y = Complexity.pairFst (Complexity.pairFst y)

def Complexity.accW (y : List Bool) : List Bool

The witness, out of the iteration's input.

Equations

• Complexity.accW y = Complexity.pairSnd (Complexity.pairFst y)

noncomputable def Complexity.accCoin (r : ℕ → ℕ) (y : List Bool) : List Bool

The coin string named by the iteration's index.

Equations

• Complexity.accCoin r y = Complexity.coinStr (r (Complexity.accX y).length) (Complexity.pairSnd y).length

noncomputable def Complexity.accView (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (y : List Bool) : List Bool

The verifier's view: input and coins paired with the answers read off the witness block.

Equations

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

theorem Complexity.accX_mem_FP : accX ∈ FP

theorem Complexity.accW_mem_FP : accW ∈ FP

theorem Complexity.accCoin_mem_FP (r : ℕ → ℕ) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : accCoin r ∈ FP

theorem Complexity.accView_mem_FP (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : accView f r Q ∈ FP

noncomputable def Complexity.accInner (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) : Language

One iteration's condition: the verifier accepts the view.

Equations

• Complexity.accInner V f r Q = Complexity.accView f r Q ⁻¹' V.verdict

theorem Complexity.accInner_mem_P (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : accInner V f r Q ∈ P

noncomputable def Complexity.accLang (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) : Language

Acceptance on every coin string, as a language of pair x w.

Equations

• Complexity.accLang V f r Q = {z : List Bool | ∀ c < 2 ^ r (Complexity.pairFst z).length, Complexity.pair z (List.replicate c true) ∈ Complexity.accInner V f r Q}

theorem Complexity.accLang_mem_P (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) (hrlog : BigO r fun (n : ℕ) => Nat.log 2 n) : accLang V f r Q ∈ P

theorem Complexity.accView_pair (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hfspec : ∀ (x rr : List Bool), f (pair x rr) = DataEncode.bitstringEncode (V.positions x rr)) {x w : List Bool} {c : ℕ} (hc : c < 2 ^ r x.length) (hw : w.length = 2 ^ r x.length * Q) (hQ : ∀ (rr : List Bool), (V.positions x rr).length ≤ Q) : accView f r Q (pair (pair x w) (List.replicate c true)) = pair (pair x (BitString.toList (PCPVerifier.coinOfIndex ⟨c, hc⟩))) (V.tableOf (r x.length) Q x w (PCPVerifier.coinOfIndex ⟨c, hc⟩))

What one iteration looks at, on a well-formed input.

theorem Complexity.mem_accLang_iff (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hfspec : ∀ (x rr : List Bool), f (pair x rr) = DataEncode.bitstringEncode (V.positions x rr)) {x w : List Bool} (hw : w.length = 2 ^ r x.length * Q) (hQ : ∀ (rr : List Bool), (V.positions x rr).length ≤ Q) : pair x w ∈ accLang V f r Q ↔ ∀ (ρ : Fin (r x.length) → Bool), pair (pair x (BitString.toList ρ)) (V.tableOf (r x.length) Q x w ρ) ∈ V.verdict

Acceptance on every coin string.