Back to homepage

A PCP verifier for graph 3-coloring

This is an implementation of the PCP protocol for 3-coloring provided in A Simple Algebraic Proof of the PCP Theorem.

An untrusted prover claims that a graph is 3-colorable, and provides a claimed proof. The verifier wants to check that the proof is correct, but only wants to read a constant number of bits of the proof.

1. Configuration

The cheating strategy is used only when the graph is not 3-colorable. The verifier is random, so it is run 100 times, to see how often it catches a wrong proof.

2. Input graph

3. Prover

The proof consists of eight oracle tables. An oracle is simply a large table of bits that the verifier may query at a few chosen positions. Each of the four polynomials below has two oracles. The point oracle f holds the degree-3 Hadamard encoding of \(f(a)\) for every point \(a\). The lines oracle f_lines holds, for every line \(a + Xb\), the univariate polynomial \(f(a+Xb)\), first reduced in degree by \(\Psi\) and then Hadamard encoded.

OraclesPolynomial and purposeBits
chi, chi_lines \(\chi = \mathrm{LDE}(\mathrm{Color})\) in \(m\) variables: the prover's claimed coloring, extended to a low-degree polynomial.
chi_prime, chi_prime_lines \(\chi'(Y_1,Y_2) = \chi(Y_1) - \chi(Y_2)\) in \(2m\) variables: the difference between the colors at two vertices.
A0, A0_lines \(A_0 = \sum_i A^{(i)}(X)\,Y_i\) in \(2m\) variables: certifies that \(\chi^3 - 1\) vanishes on \(H^m\), i.e. every vertex has one of the three colors.
B0, B0_lines \(B_0 = \sum_i B^{(i)}(X)\,Y_i\) in \(4m\) variables: certifies that \(\mathrm{LDE}(E)\cdot(\chi'^3 - 1)\) vanishes on \(H^{2m}\), i.e. adjacent vertices have different colors.

No table is ever written out. The prover answers each query by evaluating its polynomials, exactly as the honest prover in simple_pcp does.

4. Verifier

Each round draws fresh randomness and runs all 77 tests of the verifier. The first round is shown step by step. The tests fall into four groups.

  1. Is every oracle a degree-3 Hadamard encoding?
    For each oracle, the verifier tests at a random position that the answers are affine and multiplicative in the question \(P\) (self-corrected with a random \(R\)). This checks that each table of bits really encodes a field element, rather than being an arbitrary table of bits. Tests LDT.*.affine*, LDT.*.mult*, ZERO.*.affine*.
  2. Do the oracles represent low-degree polynomials, and do they agree?
    The degree-\(c\) test checks that a lines-table entry is consistent with degree-reduced low-degree polynomials. The line-vs-point test checks that a random line through a random point agrees with the point table. CONS.chi_prime checks \(\chi'(a,b) = \chi(a) - \chi(b)\). Tests *.degree_c, *.line_vs_point, CONS.chi_prime.
  3. Does A0 prove that χ uses only the three allowed colors?
    At a random point \(a \in \mathbb{F}_q^m\), the verifier reads \(A_0\) at \((a, 0)\), where it must be 0, and at \((a, Z_H(a))\), where it must equal \(\chi(a)^3 - 1\). Both values come from the lines table, through line correction. Tests ZERO.A1.is_zero, ZERO.A2.equals_val.
  4. Does B0 prove that adjacent vertices have different colors?
    The same zero test for \(B_0\) at random \((a,b) \in \mathbb{F}_q^{2m}\): \(B_0(a,b,0) = 0\) and \(B_0(a,b,Z_H(a,b)) = \mathrm{LDE}(E)(a,b)\,(\chi'(a,b)^3 - 1)\). The verifier computes \(\mathrm{LDE}(E)(a,b)\) itself, from the graph. Tests ZERO.B1.is_zero, ZERO.B2.equals_prop.

The verifier has not run yet.

0/100

5. Result

Generate a graph and run the verifier.

Cheating prover strategies

If the graph is not 3-colorable, the cheating prover submits a false proof based on the strategy selected above. For a 3-colorable graph, the prover is always honest and the selected cheating strategy is ignored.

The cheating proofs are built the way the honest prover would build them. The only difference is that the honest prover requires the polynomial division by the vanishing polynomials \(Z_H(X_i)\) to leave remainder zero. A false coloring leaves a nonzero remainder, and the cheating prover silently drops it. In the first two strategies, every oracle is still a genuine encoding of a low-degree polynomial, so only the zero test can catch the lie. The last two strategies also fool the zero test. To do so, they have to break either the Hadamard encoding or the low-degree structure, and the remaining tests catch that.

Closest 3-coloring
Use only the three allowed colors and minimize the number of monochromatic edges. In the generated non-3-colorable examples, exactly one edge is bad. \(\chi\) and \(A_0\) are honest. The division for \(B_0\) leaves a remainder, so \(B_0\) cannot satisfy both zero-test identities. The verifier rejects through ZERO.B2.equals_prop, at a random point \((a,b)\) that is almost never the bad edge itself.
Closest 4-coloring
While the graph is not 3-colorable, a 4-coloring might exist. Properly color every edge using four colors. The fourth color is the field element 0, which is not a cube root of unity. \(B_0\) is honest, because the colors at the ends of each edge still differ. The division for \(A_0\) leaves a remainder, and ZERO.A2.equals_val rejects.
Fake Hadamard encoding
Start with the closest 3-coloring proof, and change the table chi_prime. At each point, an honest table answers the question \(P\) with \(P(\rho(x))\), where \(x = \chi'(a,b)\). This is a linear combination of the coefficients of \(P\), with weights \(\prod_{i\in S} x_i\), one for each monomial \(S\). The cheating table keeps the answers linear in \(P\), and keeps the weights of the constant and linear monomials. Questions of degree at most 1, which are all that the consistency tests ask, therefore get honest answers. The weights of the quadratic monomials are changed, by solving a small linear system over \(\mathbb{F}_2\), so that the zero test's question \(\Lambda_\gamma\) is always answered as if the coloring were proper. The zero test passes, but the table is no longer a Hadamard codeword. Only the multiplicativity tests LDT.chi_prime.point.mult* can notice.
Functions that are not polynomials
Start with the closest 3-coloring proof. The zero test reads the certificate \(B_0(X,Y)\) only on the slices \(Y = 0\) and \(Y = Z_H(X)\). The prover replaces \(B_0\) by the function that agrees with it everywhere except on the slice \(Y = Z_H(X)\), where it is set to \(\mathrm{LDE}(E)(X)(\chi'(X)^3 - 1)\), and does the same for \(A_0\). This function is not a polynomial of low degree. Each line of the lines table that starts on the slice is moved by a constant, so that it takes the new value at \(\lambda = 0\). The zero test passes, but the line no longer agrees with the point table at its other points, and ZERO.B2.line_vs_point rejects.

Why the field size matters

Completeness holds for every \(q\): an honest proof is always accepted. Soundness needs \(q\) to be large compared with the degree bound \(D\) of the polynomials (\(D = 20\) for 9 vertices). With \(q = 4\), a cheating prover is caught far less often. At 16 vertices, \(H\) is all of \(\mathbb{F}_4\), so \(Z_H\) is identically zero on \(\mathbb{F}_4\) and the zero test is almost blind. Try it: switch the field to \(q = 4\) and run the verifier on a non-3-colorable graph.

How does the encoding work?

Before encoding, the entries of the oracles are elements of \(\mathbb{F}_q\), where \(q=2^t\). One field element therefore takes \(t=\log_2 q\) bits to write down, which is already more than the verifier is allowed to read. An entry of a line-table oracle contains even more information: it describes a univariate polynomial of degree \(D\) over \(\mathbb{F}_q\).

The four algebraic objects \(\chi,\chi',A_0,B_0\) are encoded using the degree-3 Hadamard encoding. Fix an \(\mathbb{F}_2\)-linear identification \(\rho:\mathbb{F}_q\to\mathbb{F}_2^t\). For a field element \(a\in\mathbb{F}_q\), its encoding records \(P(\rho(a))\) for every polynomial \(P\in\mathcal{P}_3(t,\mathbb{F}_2)\). Thus every encoded position is a single bit, even though it represents information about an element of \(\mathbb{F}_q\).

This code has constant relative distance. Consequently, the verifier can distinguish two different field elements and test whether a submitted table has the required Hadamard form by reading only a constant number of bits.

For the line tables, the coefficient vector of each degree-\(D\) univariate polynomial is first transformed into a constant-degree multivariate polynomial using the map \(\Psi\). The values of that polynomial are then degree-3 Hadamard encoded in the same way. This lets the verifier combine low-degree tests and local correction with only a constant number of oracle queries, at the cost of a small increase in randomness.

On this page, a field element is written as the integer whose binary digits are its \(t\) bits \(\rho(x)\). For example, in \(\mathbb{F}_4\), 2 stands for \(\omega\) and 3 for \(\omega^2 = \omega + 1\).