diff --git a/book/src/rfcs/3-lookup.md b/book/src/rfcs/3-lookup.md index 6f256e6a6f..fcc214599a 100644 --- a/book/src/rfcs/3-lookup.md +++ b/book/src/rfcs/3-lookup.md @@ -40,17 +40,17 @@ where $\text{diff}$ is a new set derived by applying a "randomized difference" b The equality between the multisets can be proved with the permutation argument of plonk, which would look like enforcing constraints on the following accumulator: -* init: $acc_0 = 1$ -* final: $acc_n = 1$ +* init: $\mathsf{acc}_0 = 1$ +* final: $\mathsf{acc}_n = 1$ * for every $0 < i \leq n$: $$ - acc_i = acc_{i-1} \cdot \frac{(\gamma + (1+\beta) f_{i-1})(\gamma + t_{i-1} + \beta t_i)}{(\gamma + s_{i-1} + \beta s_{i})} + \mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(\gamma + (1+\beta) f_{i-1})(\gamma + t_{i-1} + \beta t_i)}{(\gamma + s_{i-1} + \beta s_{i})} $$ - + Note that the plookup paper uses a slightly different equation to make the proof work. I believe the proof would work with the above equation, but for simplicity let's just use the equation published in plookup: $$ -acc_i = acc_{i-1} \cdot \frac{(1+\beta)(\gamma + f_{i-1})(\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})} +\mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(1+\beta)(\gamma + f_{i-1})(\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})} $$ > Note: in plookup $s$ is too large, and so needs to be split into multiple vectors to enforce the constraint at every $i \in [[0;n]]$. We ignore this for now. @@ -67,9 +67,9 @@ Kimchi uses a single **lookup table** at the moment of this writing; the XOR tab | 1 | 1 | 0 | | 0 | 0 | 0 | -Whereas kimchi uses the XOR table for values of 4 bits, which has $2^{8}$ entries. +Whereas kimchi uses the XOR table for values of $4$ bits, which has $2^{8}$ entries. -Note: the (0, 0, 0) **entry** is at the very end on purpose (as it will be used as dummy entry for rows of the witness that don't care about lookups). +Note: the $(0, 0, 0)$ **entry** is at the very end on purpose (as it will be used as dummy entry for rows of the witness that don't care about lookups). ### Querying the table @@ -80,16 +80,16 @@ The plookup paper handles a vector of lookups $f$ which we do not have. So the f Let's go over the first item in this section. -For example, the following **query** tells us that we want to check if $r_0 \oplus r_2 = 2r_1$ +For example, the following **query** tells us that we want to check if $r_0 \oplus r_2 = 2\cdot r_1$ -| l | r | o | -| :---: | :---: | :---: | -| 1, r0 | 1, r2 | 2, r1 | +| l | r | o | +| :---: | :---: | :---: | +| 1, $r_0$ | 1, $r_2$ | 2, $r_1$ | The grand product argument for the lookup consraint will look like this at this point: $$ -acc_i = acc_{i-1} \cdot \frac{\color{green}{(1+\beta)(\gamma + w_0(g^i) + j \cdot w_2(g^i) + j^2 \cdot 2 \cdot w_1(g^i))}(\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})} +\mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(1+\beta){\color{green}(\gamma + w_0(g^i) + j \cdot w_2(g^i) + j^2 \cdot 2 \cdot w_1(g^i))}(\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})} $$ Not all rows need to perform queries into a lookup table. We will use a query selector in the next section to make the constraints work with this in mind. @@ -109,40 +109,44 @@ Both the (XOR) lookup table and the query are built-ins in kimchi. The query sel The grand product argument for the lookup constraint looks like this now: $$ -acc_i = acc_{i-1} \cdot \frac{\color{green}{(1+\beta) \cdot query} \cdot (\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})} +\mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(1+\beta) \cdot {\color{green}\mathsf{query}} \cdot (\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})} $$ -where $\color{green}{query}$ is constructed so that a dummy query ($0 \oplus 0 = 0$) is used on rows that don't have a query. +where $\color{green}{\mathsf{query}}$ is constructed so that a dummy query ($0 \oplus 0 = 0$) is used on rows that don't have a query. $$ \begin{align} -query = &\ selector \cdot (\gamma + w_0(g^i) + j \cdot w_2(g^i) + j^2 \cdot 2 \cdot w_1(g^i)) + \\ -&\ (1- selector) \cdot (\gamma + 0 + j \cdot 0 + j^2 \cdot 0) +\mathsf{query} := &\ \mathsf{selector} \cdot (\gamma + w_0(g^i) + j \cdot w_2(g^i) + j^2 \cdot 2 \cdot w_1(g^i)) + \\ +&\ (1- \mathsf{selector}) \cdot (\gamma + 0 + j \cdot 0 + j^2 \cdot 0) \end{align} $$ ### Queries, not query -Since we allow multiple queries per row, we define multiple **queries**, where each query is associated with a **lookup selector**. +Since we allow multiple queries per row, we define multiple **queries**, where each query is associated with a **lookup selector**. At the moment of this writing, the `ChaCha` gates all perform $4$ queries in a row. Thus, $4$ is trivially the largest number of queries that happen in a row. -**Important**: to make constraints work, this means that each row must make 4 queries. (Potentially some or all of them are dummy queries.) +**Important**: to make constraints work, this means that each row must make $4$ queries. (Potentially some or all of them are dummy queries.) For example, the `ChaCha0`, `ChaCha1`, and `ChaCha2` gates will apply the following 4 XOR queries on the current and following rows: -| l | r | o | - | l | r | o | - | l | r | o | - | l | r | o | -| :---: | :---: | :----: | --- | :---: | :---: | :----: | --- | :---: | :---: | :----: | --- | :---: | :----: | :----: | -| 1, r3 | 1, r7 | 1, r11 | - | 1, r4 | 1, r8 | 1, r12 | - | 1, r5 | 1, r9 | 1, r13 | - | 1, r6 | 1, r10 | 1, r14 | +| l | r | o | - | l | r | o | - | l | r | o | - | l | r | o | +| :---: | :---: | :----: | --- | :---: | :---: | :----: | --- | :---: | :---: | :----: | --- | :---: | :----: | :----: | +| 1, $r_3$ | 1, $r_7$ | 1, $r_{11}$ | - | 1, $r_4$ | 1, $r_8$ | 1, $r_{12}$ | - | 1, $r_5$ | 1, $r_9$ | 1, $r_{13}$ | - | 1, $r_6$ | 1, $r_{10}$ | 1, $r_{14}$ | which you can understand as checking for the current and following row that -* $r_3 \oplus r7 = r_{11}$ -* $r_4 \oplus r8 = r_{12}$ -* $r_5 \oplus r9 = r_{13}$ -* $r_6 \oplus r10 = r_{14}$ +$$ +\begin{align} +r_3 \oplus r_7 &= r_{11}\\ +r_4 \oplus r_8 &= r_{12}\\ +r_5 \oplus r_9 &= r_{13}\\ +r_6 \oplus r_{10} &= r_{14} +\end{align} +$$ -The `ChaChaFinal` also performs $4$ (somewhat similar) queries in the XOR lookup table. In total this is 8 different queries that could be associated to 8 selector polynomials. +The `ChaChaFinal` also performs $4$ (somewhat similar) queries in the XOR lookup table. In total this is $8$ different queries that could be associated to $8$ selector polynomials. ### Grouping queries by queries pattern @@ -156,16 +160,16 @@ Using the previous section's method, we'd have to use $8$ different lookup selec The grand product argument for the lookup constraint looks like this now: $$ -acc_i = acc_{i-1} \cdot \frac{\color{green}{(1+\beta)^4 \cdot query} \cdot (\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})} +\mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{{\color{green}(1+\beta)^4 \cdot \mathsf{query}} \cdot (\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})} $$ -where $\color{green}{query}$ is constructed as: +where $\color{green}{\mathsf{query}}$ is constructed as: $$ \begin{align} -query = &\ selector_1 \cdot pattern_1 + \\ -&\ selector_2 \cdot pattern_2 + \\ -&\ (1 - selector_1 - selector_2) \cdot (\gamma + 0 + j \cdot 0 + j^2 \cdot 0)^4 +\mathsf{query} = &\ \mathsf{selector}_1 \cdot \mathsf{pattern}_1 + \\ +&\ \mathsf{selector}_2 \cdot \mathsf{pattern}_2 + \\ +&\ (1 - \mathsf{selector}_1 - \mathsf{selector}_2) \cdot (\gamma + 0 + j \cdot 0 + j^2 \cdot 0)^4 \end{align} $$ @@ -173,7 +177,7 @@ where, for example the first pattern for the `ChaCha0`, `ChaCha1`, and `ChaCha2` $$ \begin{align} -pattern_1 = &\ (\gamma + w_3(g^i) + j \cdot w_7(g^i) + j^2 \cdot w_{11}(g^i)) \cdot \\ +\mathsf{pattern}_1 = &\ (\gamma + w_3(g^i) + j \cdot w_7(g^i) + j^2 \cdot w_{11}(g^i)) \cdot \\ &\ (\gamma + w_4(g^i) + j \cdot w_8(g^i) + j^2 \cdot w_{12}(g^i)) \cdot \\ &\ (\gamma + w_5(g^i) + j \cdot w_9(g^i) + j^2 \cdot w_{13}(g^i)) \cdot \\ &\ (\gamma + w_6(g^i) + j \cdot w_{10}(g^i) + j^2 \cdot w_{14}(g^i)) \cdot \\ @@ -192,7 +196,7 @@ There are two things that we haven't touched on: * The vector $t$ representing the **combined lookup table** (after its columns have been combined with a joint combiner $j$). The **non-combined loookup table** is fixed at setup time and derived based on the lookup tables used in the circuit (for now only one, the XOR lookup table, can be used in the circuit). * The vector $s$ representing the sorted multiset of both the queries and the lookup table. This is created by the prover and sent as commitment to the verifier. -The first vector $t$ is quite straightforward to think about: +The first vector $t$ is quite straightforward to think about: * if it is smaller than the domain (of size $n$), then we can repeat the last entry enough times to make the table of size $n$. * if it is larger than the domain, then we can either increase the domain or split the vector in two (or more) vectors. This is most likely what we will have to do to support multiple lookup tables later. @@ -201,7 +205,7 @@ What about the second vector? ## The sorted vector $s$ -The second vector $s$ is of size +The second vector $s$ is of size $$n \cdot |\text{queries}| + |\text{lookup\_table}|$$ @@ -210,10 +214,10 @@ That is, it contains the $n$ elements of each **query vectors** (the actual valu Because the vector $s$ is larger than the domain size $n$, it is split into several vectors of size $n$. Specifically, in the plonkup paper, the two halves of $s$ (which are then interpolated as $h_1$ and $h_2$). $$ -acc_i = acc_{i-1} \cdot \frac{\color{green}{(1+\beta)^4 \cdot query} \cdot (\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})(\gamma(1+\beta)+s_{n+i-1} + \beta s_{n+i})} +\mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{{\color{green}(1+\beta)^4 \cdot \mathsf{query}} \cdot (\gamma(1 + \beta) + t_{i-1} + \beta t_i)}{(\gamma(1+\beta) + s_{i-1} + \beta s_{i})(\gamma(1+\beta)+s_{n+i-1} + \beta s_{n+i})} $$ -Since you must compute the difference of every contiguous pairs, the last element of the first half is the replicated as the first element of the second half ($s_{n-1} = s_{n}$), and a separate constraint enforces that continuity on the interpolated polynomials $h_1$ and $h_2$: +Since you must compute the difference of every contiguous pairs, the last element of the first half is the replicated as the first element of the second half ($s_{n-1} = s_{n}$), and a separate constraint enforces that continuity on the interpolated polynomials $h_1$ and $h_2$: $$L_{n-1}(h_1(x) - h_2(g \cdot x)) = 0$$ @@ -223,7 +227,7 @@ $$h_1(g^{n-1}) = h_2(1)$$ ## The sorted vector $s$ in kimchi -Since this vector is known only by the prover, and is evaluated as part of the protocol, zero-knowledge must be added to the polynomial. To do this in kimchi, we use the same technique as with the other prover polynomials: we randomize the last evaluations (or rows, on the domain) of the polynomial. +Since this vector is known only by the prover, and is evaluated as part of the protocol, zero-knowledge must be added to the polynomial. To do this in kimchi, we use the same technique as with the other prover polynomials: we randomize the last evaluations (or rows, on the domain) of the polynomial. This means two things for the lookup grand product argument: @@ -232,9 +236,9 @@ This means two things for the lookup grand product argument: The first problem can be solved in two ways: -* **Zig-zag technique**. By reorganizing $s$ to alternate its values between the columns. For example, $h_1 = (s_0, s_2, s_4, \cdots)$ and $h_2 = (s_1, s_3, s_5, \cdots)$ so that you can simply write the denominator of the grand product argument as +* **Zig-zag technique**. By reorganizing $s$ to alternate its values between the columns. For example, $h_1 = (s_0, s_2, s_4, \cdots)$ and $h_2 = (s_1, s_3, s_5, \cdots)$ so that you can simply write the denominator of the grand product argument as $$(\gamma(1+\beta) + h_1(x) + \beta h_2(x))(\gamma(1+\beta)+ h_2(x) + \beta h_1(x \cdot g))$$ - this is what the [plonkup](https://eprint.iacr.org/2022/086) paper does. + this is what the [plonkup](https://eprint.iacr.org/2022/086) paper does. * **Snake technique**. by reorganizing $s$ as a snake. This is what is done in kimchi currently. The snake technique rearranges $s$ into the following shape: @@ -244,6 +248,7 @@ The snake technique rearranges $s$ into the following shape: | | | | | | | | | | |_| |_| | + ``` so that the denominator becomes the following equation: @@ -273,7 +278,7 @@ We do the second one, but there is an edge-case: the combined $t$ entries can re For some $i, l$ such that $i \neq l$, we might have $$ -t_0[i] + j t_1[i] + j^2 t_2[i] = t_0[l] + j t_1[l] + j^2 t_2[l] +t_0[i] + j \cdot t_1[i] + j^2 \cdot t_2[i] = t_0[l] + j \cdot t_1[l] + j^2 \cdot t_2[l] $$ For example, if $f = \{1, 2, 2, 3\}$ and $t = \{2, 1, 2, 3\}$, then $\text{sorted}(f, t) = \{2, 2, 2, 1, 1, 2, 3, 3\}$ would be one way of sorting things out. But $\text{sorted}(f, t) = \{ 2, 2, 2, 2, 1, 1, 3, 3 \}$ would be incorrect.