Proofs as assignments

The proof a PCP verifier reads is an assignment written out: one fixed-width block per vertex. This module sets up that correspondence — how to cut a proof into blocks, how to write an assignment as a proof, and that the two are inverse.

Main definitions

• Complexity.blockOf — the block a proof carries at a vertex
• Complexity.proofOf — the proof an assignment writes

Main results

• Complexity.blockOf_proofOf — reading back what was written
• Complexity.answers_posVal — the verifier reads exactly the two endpoint blocks
• Complexity.AlgCSP.Models — an algorithmic graph agrees with a real one
• Complexity.AlgCSP.Models.sat_of_satisfiable — completeness transfers

def Complexity.blockOf (w : ℕ) (π : List Bool) (v : ℕ) : List Bool

The block a proof carries at a vertex, when symbols occupy w bits.

Equations

• Complexity.blockOf w π v = List.take w (List.drop (v * w) π)

def Complexity.proofOf (n : ℕ) (f : ℕ → List Bool) : List Bool

The proof an assignment writes: the blocks of the first n vertices, one after another.

Equations

• Complexity.proofOf n f = List.flatMap f (List.range n)

theorem Complexity.length_proofOf {w : ℕ} {f : ℕ → List Bool} (hf : ∀ (i : ℕ), (f i).length = w) (n : ℕ) : (proofOf n f).length = n * w

theorem Complexity.blockOf_proofOf {w : ℕ} {f : ℕ → List Bool} (hf : ∀ (i : ℕ), (f i).length = w) (n v : ℕ) : v < n → blockOf w (proofOf n f) v = f v

Reading back what was written.

theorem Complexity.length_blockOf {w : ℕ} {π : List Bool} {v : ℕ} (h : (v + 1) * w ≤ π.length) : (blockOf w π v).length = w

theorem Complexity.getElem_blockOf {w : ℕ} {π : List Bool} {v j : ℕ} (h : (v + 1) * w ≤ π.length) (hj : j < w) : (blockOf w π v)[j] = π.getD (v * w + j) false

theorem Complexity.answers_posVal (A : AlgCSP) (x π : List Bool) (e : ℕ) (h0 : (A.vert false x e + 1) * A.width ≤ π.length) (h1 : (A.vert true x e + 1) * A.width ≤ π.length) : PCPVerifier.answers π (List.map (A.posVal x e) (List.range (2 * A.width))) = blockOf A.width π (A.vert false x e) ++ blockOf A.width π (A.vert true x e)

The verifier reads exactly the two endpoint blocks.

Padding a proof

theorem Complexity.answers_append_false (π : List Bool) (k : ℕ) (ps : List ℕ) : PCPVerifier.answers π ps = PCPVerifier.answers (π ++ List.replicate k false) ps

Agreement with a real constraint graph

structure Complexity.AlgCSP.Models (A : AlgCSP) {α : Type} (G : List Bool → ConstraintGraph α) (enc : α → List Bool) (dec : List Bool → α) : Prop

An algorithmic graph agrees with a real one: same edges, same endpoints, and the constraint means the same thing once symbols are decoded.

• numEdges_eq (x : List Bool) : A.numEdges x = (G x).numEdges

  The edge counts agree.

• tail_eq (x : List Bool) (e : ℕ) (he : e < (G x).numEdges) : A.vert false x e = ↑((G x).tail ⟨e, he⟩)

  The first endpoint agrees.

• head_eq (x : List Bool) (e : ℕ) (he : e < (G x).numEdges) : A.vert true x e = ↑((G x).head ⟨e, he⟩)

  The second endpoint agrees.

• length_enc (s : α) : (enc s).length = A.width

  Symbols occupy exactly the block width.

• dec_enc (s : α) : dec (enc s) = s

  Decoding inverts encoding.

• ok_iff (x : List Bool) (e : ℕ) (he : e < (G x).numEdges) (u v : List Bool) : u.length = A.width → v.length = A.width → (pair (pair x (List.replicate e true)) (u ++ v) ∈ A.ok ↔ (G x).rel ⟨e, he⟩ (dec u) (dec v) = true)

  The constraint agrees on blocks.

def Complexity.AlgCSP.assignProof {α : Type} [Inhabited α] (enc : α → List Bool) (n : ℕ) (a : Fin n → α) : List Bool

The proof an assignment writes.

Equations

• Complexity.AlgCSP.assignProof enc n a = Complexity.proofOf n fun (v : ℕ) => if h : v < n then enc (a ⟨v, h⟩) else enc default

theorem Complexity.AlgCSP.length_assignProof {A : AlgCSP} {α : Type} [Inhabited α] {G : List Bool → ConstraintGraph α} {enc : α → List Bool} {dec : List Bool → α} (hM : A.Models G enc dec) (n : ℕ) (a : Fin n → α) : (assignProof enc n a).length = n * A.width

theorem Complexity.AlgCSP.blockOf_assignProof {A : AlgCSP} {α : Type} [Inhabited α] {G : List Bool → ConstraintGraph α} {enc : α → List Bool} {dec : List Bool → α} (hM : A.Models G enc dec) {n : ℕ} (a : Fin n → α) {v : ℕ} (hv : v < n) : blockOf A.width (assignProof enc n a) v = enc (a ⟨v, hv⟩)

theorem Complexity.AlgCSP.Models.sat_of_satisfiable {A : AlgCSP} {α : Type} [Inhabited α] {G : List Bool → ConstraintGraph α} {enc : α → List Bool} {dec : List Bool → α} (hM : A.Models G enc dec) (x : List Bool) (h : (G x).Satisfiable) : ∃ (π : List Bool), ∀ e < A.numEdges x, A.Sat x π e

Completeness transfers. A satisfying assignment writes a proof the verifier accepts on every edge.

theorem Complexity.AlgCSP.card_filter_range_eq {n : ℕ} (P : ℕ → Prop) [DecidablePred P] : (Finset.filter P (Finset.range n)).card = {i : Fin n | P ↑i}.card

theorem Complexity.AlgCSP.Models.card_sat_le {A : AlgCSP} {α : Type} {G : List Bool → ConstraintGraph α} {enc : α → List Bool} {dec : List Bool → α} [Fintype α] [Nonempty α] (hM : A.Models G enc dec) (x : List Bool) {gap : ℚ} (hgap : gap ≤ (G x).unsatVal) (π : List Bool) : ↑(Finset.filter (A.Sat x π) (Finset.range (A.numEdges x))).card ≤ (1 - gap) * ↑(A.numEdges x)

Soundness transfers. No proof satisfies more than a 1 - gap fraction of the edges.