Introduction
This is a way to prove something about two lists of data ("columns" in cryptographic terms), called $A$ and $S$. Imagine $A$ as a list of items you're claiming something about, and $S$ as a reference list you're checking against. The goal is to prove that every item in $A$ exists somewhere in $S$. In other words, $A$ is a subset of $S$. $S$ might have extra items not in $A$, and both lists can have repeats. Plus, $S$ can either be a fixed list agreed on beforehand, or a list that's part of the proof itself. You can compare this with the protocol description in the Halo2 book.
Key components
- Two columns: $A$ is the "claim" column, the list being tested. $S$ is the "reference" column. Both have a length of $2^k$. This power-of-two size aligns with roots of unity.
- The goal of the protocol:
- Every value in $A$ must appear at least once in $S$. For example, if $A = [1, 2]$, then $S = [3, 1, 2, 4]$ works.
- $S$ can have extra values that don't appear in $A$, as 3 and 4 do above.
- Fixed or variable $S$:
- Fixed: $S$ is a predefined list, like a table of valid denominations.
- Variable: $S$ is part of the trace, the computation's record. It isn't fixed in advance, but provided by the prover. This is more flexible, and the circuit must then constrain what $S$ may contain.
- Duplicates allowed: For instance, $A = [1, 1, 2]$ and $S = [1, 2, 2, 3]$ are valid.
- Padding to $2^k$: If $A$ or $S$ isn't already $2^k$ long, it must be extended.
- $A$: Fill it with some data from $S$. If $A = [1, 2]$ with $S = [1, 2, 3]$ and $k = 2$, it might become $[1, 2, 3, 3]$.
- $S$: Fill it with its last value, so $[1, 2, 3]$ becomes $[1, 2, 3, 3]$.
Is padding safe? Padding $A$ with values from $S$ doesn't weaken the proof. Padded cells hold values that are already in $S$, and they occupy only the rows the circuit doesn't otherwise use. The cells of $A$ that matter are fixed by the rest of the circuit, so the prover can't swap them out, and they must still pass the checks below.
What's Being Proved?
This is done in a cryptographic context, for a zero-knowledge proof system:
- The prover, who knows $A$ and $S$, convinces the verifier, who doesn't see the lists, that $A \subseteq S$.
- It's efficient, using polynomials and permutations.
The flexibility of $S$ is useful:
- Fixed $S$ is used to check against a standard table (e.g., "all my transaction amounts are valid denominations").
- Variable $S$ is used where the table is generated by the computation itself.
Protocol
The protocol works over $H = \{1, w, w^2, \ldots, w^{2^k - 1}\}$, a set of $2^k$ elements where $w$ is a root of unity in the finite field.
We will use this example throughout, with $k = 2$:
$$A = [1, 2, 2, 3] \qquad S = [3, 1, 2, 4]$$
Every value of $A$ is in $S$, and 4 is the extra value in $S$.
Step 1: Creating the Permutations $A'$ and $S'$
The prover rearranges $A$ and $S$ into new lists $A'$ and $S'$, with specific rules:
- $A'$: A permutation of $A$ where identical values are adjacent. Different values can be in any order.
- $S'$: A permutation of $S$ such that wherever a new value first appears in $A'$, $S'$ holds the same value at that position. The remaining positions of $S'$ are filled with whatever is left of $S$.
For our example:
$$A' = [1, 2, 2, 3] \qquad S' = [1, 2, 4, 3]$$
These satisfy the rule that, for each position $i$, either $A'_i = S'_i$ or $A'_i = A'_{i-1}$. So $A'$ either matches $S'$ or repeats its previous value, which means that every value in $A'$ traces back to an equal value in $S'$.
Position 2 is the interesting one: $A'_2 = 2$ isn't equal to $S'_2 = 4$, but it repeats $A'_1 = 2$, so it's fine. A value not in $S$ can't pass this. If $A'$ ended in 5, then at that position $A'_3 = 5$ would match neither $S'_3$ nor $A'_2$.
Step 2: Computing the $Z$ Polynomial
The verifier sends random challenges $\beta$ and $\gamma$. The prover computes a polynomial $Z$, a running product proving that $A'$ and $S'$ really are permutations of $A$ and $S$:
- Boundary conditions: $Z_0 = 1$ and $Z_{2^k} = 1$.
- Recurrence: For $i$ from 0 to $2^k - 1$:
$$Z_{i+1} = Z_i \cdot \frac{(A_i + \beta)(S_i + \gamma)}{(A'_i + \beta)(S'_i + \gamma)}$$
For our example, with $\beta = 2$ and $\gamma = 3$ (small numbers to keep it readable):
- $Z_0 = 1$
- $Z_1 = 1 \cdot \frac{(1+2)(3+3)}{(1+2)(1+3)} = \frac{3}{2}$
- $Z_2 = \frac{3}{2} \cdot \frac{(2+2)(1+3)}{(2+2)(2+3)} = \frac{6}{5}$
- $Z_3 = \frac{6}{5} \cdot \frac{(2+2)(2+3)}{(2+2)(4+3)} = \frac{6}{7}$
- $Z_4 = \frac{6}{7} \cdot \frac{(3+2)(4+3)}{(3+2)(3+3)} = 1$
The product returns to 1, because the numerators and denominators contain the same values in a different order. In a real run this happens in a finite field, with fractions meaning field inverses.
Step 3: Verifier Checks $A'$ and $S'$
The verifier checks two conditions over all points in $H$:
$$(A'(X) - S'(X)) \cdot (A'(X) - A'(w^{-1}X)) = 0$$
At every position, either $A'_i = S'_i$ or $A'_i = A'_{i-1}$.
$$L_0(X) \cdot (A'(X) - S'(X)) = 0$$
$L_0(X)$ is the Lagrange polynomial that's 1 at the first position $X = 1$, and 0 elsewhere. This forces $A'_0 = S'_0$. It is needed because, at the first position, the first check's "previous value" wraps around to the last one, which would otherwise let the first value of $A'$ escape the check.
Step 4: Verifier Checks $Z$
The verifier also checks $Z$ with two equations:
$$Z(wX) \cdot (A'(X) + \beta)(S'(X) + \gamma) - Z(X) \cdot (A(X) + \beta)(S(X) + \gamma) = 0$$
This is the polynomial version of the recurrence. It holds across all of $H$, including the wrap-around from the last position to the first, which is how it forces the product to come back to the start.
$$L_0(X) \cdot (1 - Z(X)) = 0$$
This fixes the starting value $Z_0 = 1$.
If all four equations hold, the verifier accepts. A real implementation in Halo2 also reserves a few rows for blinding, to keep the protocol zero knowledge, and leaves those rows out of the first and third checks.
Why Does This Prove $A \subseteq S$?
The two parts do different jobs:
- The $Z$ checks prove that $A'$ is a permutation of $A$, and $S'$ a permutation of $S$. So the prover can't invent new values for $S'$ or drop values of $A$.
- The $A'$ and $S'$ checks prove that each value of $A'$ appears in $S'$.
Together, each value of $A$ appears in $S$.
Can a Dishonest Prover Cheat?
Suppose $A = [1, 2, 4, 4]$ and $S = [3, 4, 4, 4]$, where 1 and 2 aren't in $S$. A cheating prover might set $A' = S' = [1, 2, 4, 4]$, which satisfies the checks of step 3. But this $S'$ isn't a permutation of $S$, and step 4 catches that. With $\beta = 2$ and $\gamma = 3$, the running product goes $1, \frac{3}{2}, \frac{21}{10}, \frac{21}{10}, \frac{21}{10}$, and never returns to 1.
Summary
The protocol pads $A$ and $S$, permutes them into $A'$ and $S'$, computes $Z$, and verifies polynomial equations to prove $A \subseteq S$.