Executable constraint graphs

An edge list gives concrete indices to vertices and edges while keeping constraints as data. The interpretation uses an explicit Boolean evaluator; in particular, it does not decide an arbitrary proposition-valued relation. A separate WellFormed predicate says that endpoints are below the declared vertex count. None of the algorithms requires or computes that proof.

The natural-number interpretation is convenient for proving transformations correct. On well-formed inputs its vertices are the images of Fin vertices, with all other vertices isolated, and toFiniteGraph recovers the corresponding finite constraint graph.

Main definitions

• Cslib.PCP.Encoded.Edge, Cslib.PCP.Encoded.Graph: executable edge records and edge lists.
• Cslib.PCP.Encoded.Graph.toGraph, Cslib.PCP.Encoded.Graph.toFiniteGraph: interpretations.
• Cslib.PCP.Encoded.Graph.isWellFormed: an executable endpoint-bounds check.
• Cslib.PCP.Encoded.Graph.checkEdge: check a constraint against a list of vertex labels.

Main results

• Cslib.PCP.Encoded.Graph.checkEdge_eq_true_iff: exact agreement with graph satisfaction.
• Cslib.PCP.Encoded.Graph.satisfiable_toFiniteGraph_iff, Cslib.PCP.Encoded.Graph.unsatVal_toFiniteGraph: finite interpretations preserve the value.
• Cslib.PCP.Encoded.Graph.isPolyTime_checkEdge: a uniform machine-backed certificate, including edge lookup, label lookup and constraint evaluation.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1

structure Cslib.PCP.Encoded.Edge (Constraint : Type) : Type

An edge with numbered endpoints and an executable constraint descriptor.

• src : ℕ

  The first endpoint.

• dst : ℕ

  The second endpoint.

• constraint : Constraint

  The data interpreted by the constraint evaluator.

theorem Cslib.PCP.Encoded.Edge.ext_iff {Constraint : Type} {x y : Edge Constraint} : x = y ↔ x.src = y.src ∧ x.dst = y.dst ∧ x.constraint = y.constraint

theorem Cslib.PCP.Encoded.Edge.ext {Constraint : Type} {x y : Edge Constraint} (src : x.src = y.src) (dst : x.dst = y.dst) (constraint : x.constraint = y.constraint) : x = y

def Cslib.PCP.Encoded.instDecidableEqEdge.decEq {Constraint✝ : Type} [DecidableEq Constraint✝] (x✝ x✝¹ : Edge Constraint✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.PCP.Encoded.instDecidableEqEdge {Constraint✝ : Type} [DecidableEq Constraint✝] : DecidableEq (Edge Constraint✝)

@[instance_reducible]

instance Cslib.PCP.Encoded.instReprEdge {Constraint✝ : Type} [Repr Constraint✝] : Repr (Edge Constraint✝)

def Cslib.PCP.Encoded.instReprEdge.repr {Constraint✝ : Type} [Repr Constraint✝] : Edge Constraint✝ → ℕ → Std.Format

def Cslib.PCP.Encoded.Edge.encoding {C : Type} (enc : C ↪ List Bool) : Edge C ↪ List Bool

An edge is encoded by its unary endpoints and its constraint descriptor.

theorem Cslib.PCP.Encoded.Edge.isPolyTime_src {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {edge : Input → Edge C} (hedge : Turing.MultiTapeTM.ComputableTidilyInPolyTime edge input (encoding enc)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (edge x).src) input Turing.MultiTapeTM.encUnary

Reading an edge's first endpoint is polynomial-time.

theorem Cslib.PCP.Encoded.Edge.isPolyTime_dst {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {edge : Input → Edge C} (hedge : Turing.MultiTapeTM.ComputableTidilyInPolyTime edge input (encoding enc)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (edge x).dst) input Turing.MultiTapeTM.encUnary

Reading an edge's second endpoint is polynomial-time.

theorem Cslib.PCP.Encoded.Edge.isPolyTime_constraint {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {edge : Input → Edge C} (hedge : Turing.MultiTapeTM.ComputableTidilyInPolyTime edge input (encoding enc)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (edge x).constraint) input enc

Reading an edge's constraint descriptor is polynomial-time.

theorem Cslib.PCP.Encoded.Edge.isPolyTime_mk {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {src dst : Input → ℕ} {constraint : Input → C} (hsrc : Turing.MultiTapeTM.ComputableTidilyInPolyTime src input Turing.MultiTapeTM.encUnary) (hdst : Turing.MultiTapeTM.ComputableTidilyInPolyTime dst input Turing.MultiTapeTM.encUnary) (hconstraint : Turing.MultiTapeTM.ComputableTidilyInPolyTime constraint input enc) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => { src := src x, dst := dst x, constraint := constraint x }) input (encoding enc)

Assemble computed endpoints and a computed constraint into an edge.

structure Cslib.PCP.Encoded.Graph (Constraint : Type) : Type

A finite graph represented by its vertex count and ordered list of edges. The ordering distinguishes parallel edges.

• vertices : ℕ

  The number of vertices.

• edges : List (Edge Constraint)

  The ordered edges, including parallel edges and loops.

theorem Cslib.PCP.Encoded.Graph.ext {Constraint : Type} {x y : Graph Constraint} (vertices : x.vertices = y.vertices) (edges : x.edges = y.edges) : x = y

theorem Cslib.PCP.Encoded.Graph.ext_iff {Constraint : Type} {x y : Graph Constraint} : x = y ↔ x.vertices = y.vertices ∧ x.edges = y.edges

@[instance_reducible]

instance Cslib.PCP.Encoded.instDecidableEqGraph {Constraint✝ : Type} [DecidableEq Constraint✝] : DecidableEq (Graph Constraint✝)

def Cslib.PCP.Encoded.instDecidableEqGraph.decEq {Constraint✝ : Type} [DecidableEq Constraint✝] (x✝ x✝¹ : Graph Constraint✝) : Decidable (x✝ = x✝¹)

def Cslib.PCP.Encoded.instReprGraph.repr {Constraint✝ : Type} [Repr Constraint✝] : Graph Constraint✝ → ℕ → Std.Format

@[instance_reducible]

instance Cslib.PCP.Encoded.instReprGraph {Constraint✝ : Type} [Repr Constraint✝] : Repr (Graph Constraint✝)

def Cslib.PCP.Encoded.Graph.encoding {C : Type} (enc : C ↪ List Bool) : Graph C ↪ List Bool

The vertex count is unary and the edges use the standard framed list encoding.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_vertices {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {graph : Input → Graph C} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (graph x).vertices) input Turing.MultiTapeTM.encUnary

Reading the declared vertex count is polynomial-time.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_edges {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {graph : Input → Graph C} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (graph x).edges) input (Turing.MultiTapeTM.encList (Edge.encoding enc))

Reading the edge list is polynomial-time.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_mk {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {vertices : Input → ℕ} {edges : Input → List (Edge C)} (hvertices : Turing.MultiTapeTM.ComputableTidilyInPolyTime vertices input Turing.MultiTapeTM.encUnary) (hedges : Turing.MultiTapeTM.ComputableTidilyInPolyTime edges input (Turing.MultiTapeTM.encList (Edge.encoding enc))) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => { vertices := vertices x, edges := edges x }) input (encoding enc)

Assemble a computed vertex count and edge list into a graph.

def Cslib.PCP.Encoded.Graph.WellFormed {C : Type} (g : Graph C) : Prop

All listed endpoints are among the declared vertices.

def Cslib.PCP.Encoded.Graph.isWellFormed {C : Type} (g : Graph C) : Bool

Check the endpoint bounds by a scan through the edge records.

@[simp]

theorem Cslib.PCP.Encoded.Graph.isWellFormed_eq_true {C : Type} (g : Graph C) : g.isWellFormed = true ↔ g.WellFormed

The executable endpoint check is exact.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_isWellFormed {C : Type} (enc : C ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime isWellFormed (encoding enc) Turing.MultiTapeTM.encBool

Checking all endpoint bounds is uniformly polynomial-time.

def Cslib.PCP.Encoded.Graph.edgeAt {C : Type} (fallback : C) (g : Graph C) (i : ℕ) : Edge C

Read an edge by its natural-number index, returning a specified fallback if it is absent.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_edgeAt {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {graph : Input → Graph C} {index : Input → ℕ} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) (fallback : C) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => edgeAt fallback (graph x) (index x)) input (Edge.encoding enc)

A computed graph determines the edge encoding before the index is checked.

def Cslib.PCP.Encoded.Graph.checkEdge {C α : Type} (eval : C → α → α → Bool) (fallback : C) (label : α) (g : Graph C) (labels : List α) (i : ℕ) : Bool

Check a numbered edge against a list of labels. Both lookups are total, with explicit fallbacks; the correctness theorem applies to valid edge indices.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_checkEdge {C α Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {alphabet : α ↪ List Bool} {graph : Input → Graph C} {labels : Input → List α} {index : Input → ℕ} {eval : C → α → α → Bool} (fallback : C) (label : α) (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (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) (hlabels : Turing.MultiTapeTM.ComputableTidilyInPolyTime labels input (Turing.MultiTapeTM.encList alphabet)) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => checkEdge eval fallback label (graph x) (labels x) (index x)) input Turing.MultiTapeTM.encBool

Edge and label lookup, and the constraint evaluation, are all charged to the certificate.

def Cslib.PCP.Encoded.Graph.toGraph {C α : Type} (g : Graph C) (eval : C → α → α → Bool) : ConstraintGraph ℕ (Fin g.edges.length) α

Interpret the explicit edge list on natural-number vertices. Unlisted vertices are isolated.

theorem Cslib.PCP.Encoded.Graph.toGraph_eq_comap {C α : Type} {V : Type u_1} {ι : Type u_2} (g : Graph C) (eval : C → α → α → Bool) {edge : ι → Edge C} (enumeration : g.edges.Enumeration edge) (G : ConstraintGraph V ι α) (number : V → ℕ) (hsrc : ∀ (i : ι), (edge i).src = number (G.src i)) (hdst : ∀ (i : ι), (edge i).dst = number (G.dst i)) (hrel : ∀ (i : ι) (a b : α), eval (edge i).constraint a b = true ↔ G.rel i a b) : g.toGraph eval = (G.map number).comap ⇑enumeration.equiv

An occurrence enumeration and pointwise edge semantics identify the entire graph. No injectivity of the stored edge values is required, so loops and parallel edges are retained.

theorem Cslib.PCP.Encoded.Graph.checkEdge_eq_true_iff {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (label : α) (labels : List α) (i : Fin g.edges.length) : checkEdge eval fallback label g labels ↑i = true ↔ (g.toGraph eval).Satisfies (fun (v : ℕ) => labels.getD v label) i

On an existing edge, the executable check is exactly satisfaction by the list's labelling.

def Cslib.PCP.Encoded.Graph.toFiniteGraph {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (hg : g.WellFormed) : ConstraintGraph (Fin g.vertices) (Fin g.edges.length) α

Interpret a well-formed edge list using exactly its declared finite vertex set.

theorem Cslib.PCP.Encoded.Graph.toFiniteGraph_map {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (hg : g.WellFormed) : (g.toFiniteGraph eval hg).map Fin.val = g.toGraph eval

The natural-number interpretation only adds isolated vertices.

theorem Cslib.PCP.Encoded.Graph.satisfiable_toFiniteGraph_iff {C α : Type} [Nonempty α] (g : Graph C) (eval : C → α → α → Bool) (hg : g.WellFormed) : (g.toFiniteGraph eval hg).Satisfiable ↔ (g.toGraph eval).Satisfiable

The finite and natural-number interpretations have the same satisfiability.

theorem Cslib.PCP.Encoded.Graph.unsatVal_toFiniteGraph {C α : Type} [Nonempty α] (g : Graph C) (eval : C → α → α → Bool) (hg : g.WellFormed) : (g.toFiniteGraph eval hg).unsatVal = (g.toGraph eval).unsatVal

The finite and natural-number interpretations have the same unsatisfiability value.