Checking an encoded constraint graph with local proof queries

One random word selects an edge by capped binary decoding. A valid index reads fixed-width blocks for the two endpoints and checks their decoded labels. Padding indices make dummy queries at zero and accept independently of their answers. Fixed answer-block lengths support independent repetition. The cap charges arbitrary malformed random words without constructing exponentially large unary indices. The alphabet decoder and block width are fixed before the runtime graph.

Main definitions

• Cslib.PCP.Encoded.Edge.proofQueries: the bit positions of the two endpoint blocks.
• Cslib.PCP.Encoded.Graph.edgeVerifier: the nonadaptive graph verifier.

Main results

• Cslib.PCP.Encoded.Graph.polyTime_edgeVerifier: complete cost certificates for the coin count, binary query indices, and verdict on arbitrary inputs.
• Cslib.PCP.Encoded.Graph.edgeVerifier_accepts: the exact constraint checked for every proof.
• Cslib.PCP.Encoded.Graph.accepts_proofOfLabels: a satisfying labelling gives a finite proof.

References

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

def Cslib.PCP.Encoded.Edge.proofQueries {C : Type} (width : ℕ) (edge : Edge C) : List ℕ

Read the two endpoint blocks, retaining both copies when the edge is a loop.

def Cslib.PCP.Encoded.Edge.proofVerdict {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (edge : Edge C) (answers : List Bool) : Bool

Interpret the two blocks of answers, with missing bits defaulting to false.

@[simp]

theorem Cslib.PCP.Encoded.Edge.length_proofQueries {C : Type} (width : ℕ) (edge : Edge C) : (proofQueries width edge).length = 2 * width

A constraint check always requests two blocks of the declared width.

theorem Cslib.PCP.Encoded.Edge.proofVerdict_answers {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (edge : Edge C) (proof : List Bool) : proofVerdict width decode eval edge (Complexity.PCPVerifier.answers proof (proofQueries width edge)) = eval edge.constraint (decode fun (i : Fin width) => proof.getD (width * edge.src + ↑i) false) (decode fun (i : Fin width) => proof.getD (width * edge.dst + ↑i) false)

Reading the query list returns exactly the two endpoint bit blocks, including repeated bits.

theorem Cslib.PCP.Encoded.Edge.isPolyTime_proofQueries {C : Type} (width : ℕ) (enc : C ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (proofQueries width) (encoding enc) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Query construction is efficient, with positions returned in binary.

theorem Cslib.PCP.Encoded.Edge.isPolyTime_proofVerdict {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) {enc : C ↪ List Bool} {alphabet : α ↪ List Bool} {eval : C → α → α → Bool} (heval : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : C × α × α) => eval p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair alphabet alphabet)) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : Edge C × List Bool) => proofVerdict width decode eval p.1 p.2) (Turing.MultiTapeTM.encPair (encoding enc) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

A fixed finite decoder and a joint evaluator give an efficient verdict on arbitrary answers.

def Cslib.PCP.Encoded.Graph.sampleEdge {C : Type} (g : Graph C) (random : List Bool) : Option (Edge C)

Select an edge using bounded binary decoding; indices in the padding range give none.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_sampleEdge {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {graph : Input → Graph C} {random : Input → List Bool} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (hrandom : Turing.MultiTapeTM.ComputableTidilyInPolyTime random input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (graph x).sampleEdge (random x)) input (Turing.MultiTapeTM.encOption (Edge.encoding enc))

Edge selection charges the graph, the entire random word, and the bounded decoded index.

def Cslib.PCP.Encoded.Graph.edgeVerifier {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) : Complexity.PCPVerifier (Graph C)

A local verifier with accepting padding; all numeric indices are computed under the edge cap.

@[simp]

theorem Cslib.PCP.Encoded.Graph.coins_edgeVerifier {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) : (edgeVerifier width decode eval).coins g = Nat.clog 2 g.edges.length

A local check uses the ceiling of the binary logarithm of the edge count.

def Cslib.PCP.Encoded.Graph.proofLabels {α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (proof : List Bool) : ℕ → α

Every proof word, including short words, determines one consistent label at each vertex.

def Cslib.PCP.Encoded.Graph.proofOfLabels {α : Type} (width vertices : ℕ) (encode : α → Fin width → Bool) (labels : ℕ → α) : List Bool

Pack labels at all declared vertices into consecutive fixed-width proof blocks.

theorem Cslib.PCP.Encoded.Graph.proofLabels_proofOfLabels {α : Type} (width vertices : ℕ) (encode : α → Fin width → Bool) (decode : (Fin width → Bool) → α) (hdecode : Function.LeftInverse decode encode) (labels : ℕ → α) {vertex : ℕ} (hvertex : vertex < vertices) : proofLabels width decode (proofOfLabels width vertices encode labels) vertex = labels vertex

Every declared vertex recovers its original label from the packed proof.

theorem Cslib.PCP.Encoded.Graph.edgeVerifier_accepts {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) (proof random : List Bool) : (edgeVerifier width decode eval).Accepts g proof random = (g.sampleEdge random).elim true fun (edge : Edge C) => eval edge.constraint (proofLabels width decode proof edge.src) (proofLabels width decode proof edge.dst)

The verdict checks the labels determined by the proof at the selected edge.

@[simp]

theorem Cslib.PCP.Encoded.Graph.length_queries_edgeVerifier {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) (g : Graph C) (random : List Bool) : ((edgeVerifier width decode eval).queries (g, random)).length = 2 * width

A single check always uses two blocks, retaining ignored dummy queries on padding indices.

theorem Cslib.PCP.Encoded.Graph.query_edgeVerifier_lt {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) (eval : C → α → α → Bool) {g : Graph C} (hg : g.WellFormed) (random : List Bool) {index : ℕ} (hindex : index ∈ (edgeVerifier width decode eval).queries (g, random)) : index < width * g.vertices + 1

Queries use a declared vertex block or the dummy position zero.

theorem Cslib.PCP.Encoded.Graph.accepts_proofOfLabels {C α : Type} (width : ℕ) (encode : α → Fin width → Bool) (decode : (Fin width → Bool) → α) (hdecode : Function.LeftInverse decode encode) (eval : C → α → α → Bool) {g : Graph C} (hg : g.WellFormed) (labels : ℕ → α) (hsat : ∀ (edge : Fin g.edges.length), (g.toGraph eval).Satisfies labels edge) (random : List Bool) : (edgeVerifier width decode eval).Accepts g (proofOfLabels width g.vertices encode labels) random = true

A satisfying labelling gives a finite proof accepted on every random word.

theorem Cslib.PCP.Encoded.Graph.polyTime_edgeVerifier {C α : Type} (width : ℕ) (decode : (Fin width → Bool) → α) {enc : C ↪ List Bool} {alphabet : α ↪ List Bool} {eval : C → α → α → Bool} (heval : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : C × α × α) => eval p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair alphabet alphabet)) Turing.MultiTapeTM.encBool) : Complexity.PCPVerifier.PolyTime (encoding enc) (edgeVerifier width decode eval)

All verifier functions are polynomial-time, including on random strings of the wrong length.