Merge pull request #1693 from o1-labs/volhovm/add-pickles-drawio-diagram

Introduce Pickles drawio diagram

book/src/SUMMARY.md

@@ -62,9 +62,11 @@
 
 # Pickles & Inductive Proof Systems
 
-- [Overview](./fundamentals/zkbook_ips.md)
+- [Overview](./pickles/overview.md)
+- [Inductive Proof Systems](./pickles/zkbook_ips.md)
 - [Accumulation](./pickles/accumulation.md)
 - [Deferred Computation](./pickles/deferred.md)
+- [Technical Diagrams](./pickles/diagrams.md)
 
 
 # Technical Specifications

book/src/pickles/.gitignore

@@ -0,0 +1,2 @@
+.*.bkp
+.*.dtmp

book/src/pickles/accumulation.md

@@ -771,7 +771,9 @@ Let $\mathcal{C} \subseteq \FF$ be the challenge space (128-bit GLV decomposed c
 1. Checking $\relation_{\mathsf{IPA},1} \to \relation_{\mathsf{Acc}, \vec{G}}$
     1. Receive $c$ form the prover.
     1. Define $\hpoly$ from $\vec{\chalfold}$ (folding challenges, computed above).
-    1. Compute $\openy' \gets c \cdot (\hpoly(\chaleval) + \chalu \cdot \hpoly(\chaleval \omega))$, this works since:
+    1. Compute a combined evaluation of the IPA challenge polynomial on two points: $b = \hpoly(\chaleval) + \chalu \cdot \hpoly(\chaleval \omega)$
+       - Computationally, $b$ is obtained inside bulletproof folding procedure, by folding the vector $b_{\mathsf{init}}$ such that $b_{\mathsf{init},j} = \zeta^j + v \cdot \zeta^j w^j$ using the same standard bulletproof challenges that constitute $h(X)$. This $b_{\mathsf{init}}$ is a $v$-recombined evaluation point. The equality is by linearity of IPA recombination.
+    1. Compute $\openy' \gets c \cdot b = c \cdot (\hpoly(\chaleval) + \chalu \cdot \hpoly(\chaleval \omega))$, this works since:
        $$
        \openx^{(\rounds)} =
        \openx^{(\rounds)}_{\chaleval} + \chalu \cdot \openx^{(\rounds)}_{\chaleval\omega}

book/src/pickles/diagrams.md

@@ -0,0 +1,29 @@
+# Pickles Technical Diagrams
+
+This section contains a series of diagrams giving an overview of implementation of pickles, closely following the structures and abstractions in the code. However, they are very technical and are primarily intended for developer use. The primary source of all the images in this section is [`pickles_structure.drawio`](./pickles_structure.drawio) file, and if one edits it one must re-generate the `.svg` renders by doing "export -> selection".
+
+The legend of the diagrams is quite straightforward:
+- The black boxes are data structures that have names and labels following the implementation.
+  - `MFNStep`/`MFNWrap` is an abbreviation from `MessagesForNextStep` and `MessagesForNextWrap` that is used for brevity. Most other datatypes are exactly the same as in the codebase.
+- The blue boxes are computations. Sometimes, when the computation is trivial or only vaguely indicated, it is denoted as a text sign directly on an arrow.
+- Arrows are blue by default and denote moving a piece of data from one place to another with no (or very little) change. Light blue arrows are denoting witness query that is implemented through the `handler` mechanism. The "chicken foot" connector means that this arrow accesses just one field in an array: such an arrow could connect e.g. a input field of type `old_a: A` in a structure `Vec<(A,B)>` to an output `new_a: A`, which just means that we are inside a `for` loop and this computation is done for all the elemnts in the vector/array.
+- Colour of the field is sometimes introduced and denotes how many steps ago was this piece of data created. The absense of the colour means either that (1) the data structure contains different subfields of different origin, or that (2) it was not coloured but it could be. The colours are assigned according to the following convention:
+
+![](./pickles_structure_legend_1.svg)
+
+
+### Wrap Computatiton and Deferred Values
+
+The following is the diagram that explains the Wrap computation. The left half of it corresponds to the `wrap.ml` file and the general logic of proof creation, while the right part of it is `wrap_main.ml`/`wrap_verifier.ml` and explains in-circuit computation.
+
+[ ![](pickles_structure_wrap.svg) ](./pickles_structure_wrap.svg)
+
+This diagram explains the `deferred_values` computation which is in the heart of `wrap.ml` represented as a blue box in the middle of the left pane of the main Wrap diagram. Deferred values for Wrap are computed as follows:
+
+[ ![](pickles_structure_wrap_deferred_values.svg) ](./pickles_structure_wrap_deferred_values.svg)
+
+### Step Computation
+
+The following is the diagram that explains the Step computation, similarly to Wrap. The left half of it corresponds to the general logic in `step.ml`, and the right part of it is `step_main.ml` and explains in-circuit computation. We provide no `deferred_values` computation diagram for Step, but it is very conceptually similar to the one already presented for Wrap.
+
+[ ![](pickles_structure_step.svg) ](./pickles_structure_step.svg)

book/src/pickles/overview.md

@@ -1,14 +1,30 @@
-# Overview
-
-0. Run PlonK verifiers on proofs $\pi_1, \ldots, \pi_n$ outputs polynomial relations.
-1. Checking $\relation_{\mathsf{Acc}, \vec{G}}$ and polynomial relations to $\relation_{PCS,d}$:
-    1. Sample $\zeta \sample \mathcal{C}$ using the Poseidon sponge.
-    2. Compute $C \in \GG$ from $U^{(1)}, \ldots, U^{(n)}$ from
-2. Checking $\relation_{\mathsf{IPA}, \ell} \to \relation_{\mathsf{IPA},1}$
-3. Checking
-
-    - `RecursionChallenge.comm` $\in \GG$ fields from each "input proof"
-    - The polynomial commitments in the
-    - $u \in [0, 2^{128})$ challenge (provided in GLV form).
-3. Compute $y$ from:
-    - `RecursionChallenge.prev_challenges` $\in \FF^\ell$ fields from each "input proof"
+# Overview of Pickles
+
+Pickles is a recursion layer built on top of Kimchi. The complexity of pickles as a protocol lies in specifying how to verify previous kimchi inside of the current ones. Working over two curves requires us to have different circuits and a "mirrored" structure, some computations are deferred for efficiency, and one needs to carefully keep track of the accumulators. In this section we provide a general overview of pickles, while next sections in the same chapter dive into the actual implementation details.
+
+Pickles works over [Pasta](/specs/pasta.md), a cycle of curves consisting of Pallas and Vesta, and thus it defines two generic circuits, one for each curve. Each can be thought of as a parallel instantiation of a kimchi proof systems. These circuits are not symmetric and have somewhat different function:
+- **Step circuit**: this is the main circuit that contains application logic. Each step circuit verifies a statement and potentially several (at most 2) other wrap proofs.
+- **Wrap circuit**: this circuit merely verifies the step circuit, and does not have its own application logic. The intuition is that every time an application statement is proven it's done in Step, and then the resulting proof is immediately wrapped using Wrap.
+
+
+#### General Circuit Structure
+
+Both Step and Wrap circuits additionally do a lot of recursive verification of the previous steps. Without getting too technical, Step (without lost of generality) does the following:
+1. Execute the application logic statement (e.g. the mina transaction is valid)
+2. Verify that the previous Wrap proof is (first-)half-valid (perform only main checks that are efficient for the curve)
+3. Verify that the previous Step proof is (second-)half-valid (perform the secondary checks that were inefficient to perform when the previous Step was Wrapped)
+4. Verify that the previous Step correctly aggregated the previous accumulator, e.g. $\mathsf{acc}_2 = \mathsf{Aggregate}(\mathsf{acc}_1, \pi_{\mathsf{step},2})$.
+
+The diagram roughly illustrates the interplay of the two kimchi instances.
+
+![Overview](./pickles_structure_overview.svg)
+
+
+We note that the Step circuit may repeat items 2-3 to handle the following case: when Step 2 consumes several Wrap 1.X (e.g. Wrap 1.1, Wrap 1.2, etc), it must perform all these main Wrap 1.X checks, but also all the deferred Step 1.X checks where Wrap 1.X wraps exactly Step 1.X.
+
+
+#### On Accumulators
+
+The accumulator is an abstraction introduced for the purpose of this diagram. In practice, each kimchi proof consists of (1) commitments to polynomials, (2) evaluations of them, (3) and the opening proof. What we refer to as accumulator here is actually the commitment inside the opening proof. It is called `sg` in the implementation and is semantically a polynomial commitment to `h(X)` (`b_poly` in the code) --- the poly-sized polynomial that is built from IPA challenges. It's a very important polynomial -- it can be evaluated in log time, but the commitment verification takes poly time, so the fact that `sg` is a commitment to `h(X)` is never proven inside the circuit. For more details, see [Proof-Carrying Data from Accumulation Schemes](https://eprint.iacr.org/2020/499.pdf), Appendix A.2, where `sg` is called `U`.
+
+In pickles, what we do is that we "absorb" this commitment `sg` from the previous step while creating a new proof. That is, for example, Step 1 will produce this commitment that is denoted as `acc1` on the diagram, as part of its opening proof, and Step 2 will absorb this commitment. And this "absorbtion" is what Wrap 2 will prove (and, partially, Step 3 will also refer to the challenges used to build `acc1`, but this detail is completely avoided in this overview). In the end, `acc2` will be the result of Step 2, so in a way `acc2` "aggregates" `acc1` which somewhat justifies the language used.