diff --git a/book/Makefile b/book/Makefile index 18f8a09762..9b25df8adb 100644 --- a/book/Makefile +++ b/book/Makefile @@ -9,20 +9,23 @@ MDBOOK_LINKCHECK_VERSION = 0.7.7 MDBOOK_MERMAID_VERSION = 0.12.6 MDBOOK_TOC_VERSION = 0.14.1 + +all: deps check build serve + # -# use `make deps` to install the dependencies required to serve or build the book +# Installs the dependencies required to serve or build the book # deps: cargo install "mdbook@$(MDBOOK_VERSION)" cargo install "mdbook-admonish@$(MDBOOK_ADMONISH_VERSION)" cargo install "mdbook-katex@$(MDBOOK_KATEX_VERSION)" - # cargo install "mdbook-linkcheck@$(MDBOOK_LINKCHECK_VERSION)" + cargo install --git https://github.com/o1-labs/mdbook-linkcheck --rev 8cccfc8fee397092ecdf1236a42871c5c980672e --locked mdbook-linkcheck cargo install "mdbook-mermaid@$(MDBOOK_MERMAID_VERSION)" cargo install "mdbook-toc@$(MDBOOK_TOC_VERSION)" # -# use `make check` to check if your installed dependencies match what we've listed above +# Checks if your installed dependencies match what we've listed above # define check_version @@ -33,25 +36,26 @@ check: $(call check_version,mdbook,$(MDBOOK_VERSION)) $(call check_version,mdbook-admonish,$(MDBOOK_ADMONISH_VERSION)) $(call check_version,mdbook-katex,$(MDBOOK_KATEX_VERSION)) + $(call check_version,mdbook-linkcheck,$(MDBOOK_LINKCHECK_VERSION)) $(call check_version,mdbook-mermaid,$(MDBOOK_MERMAID_VERSION)) $(call check_version,mdbook-toc,$(MDBOOK_TOC_VERSION)) # -# use `make` to serve the book locally +# Builds the book # -all: check - mdbook serve --open +build: check + mdbook build # -# use `make build` to build the book +# Serves the book locally # -build: check - mdbook build +serve: check + mdbook serve --open # -# use `make clean` to clean the generated artefacts +# Cleans the generated artefacts # clean: diff --git a/book/book.toml b/book/book.toml index cfc89991f6..6a4665cd4c 100644 --- a/book/book.toml +++ b/book/book.toml @@ -33,3 +33,12 @@ command = "mdbook-mermaid" [preprocessor.toc] command = "mdbook-toc" renderer = ["html"] + + +# See docs: +# - https://github.com/o1-labs/mdbook-linkcheck +# - (original repo) https://github.com/Michael-F-Bryan/mdbook-linkcheck +[output.linkcheck] +follow-web-links = false +traverse-parent-directories = false +latex-support = true diff --git a/book/src/fundamentals/zkbook_2pc/fkaes.md b/book/src/fundamentals/zkbook_2pc/fkaes.md index 65a8e10989..9c7003483a 100644 --- a/book/src/fundamentals/zkbook_2pc/fkaes.md +++ b/book/src/fundamentals/zkbook_2pc/fkaes.md @@ -3,9 +3,9 @@ Using fixed-key AES as a hash function in this context can be traced back to the Prior to [BHKR13](https://eprint.iacr.org/2013/426.pdf) CPU time was the main bottleneck for protocols based on circuit garbling; after the introduction of fixed-key cipher garbling, network throughput became the dominant factor. For this reason, fixed-key AES has been almost universally adopted in subsequent implementations of garbled circuits. -Several instantiations of hash function based on fix-key AES are proposed inspired by the work of Bellare et al. However, most of them have some security flaws as pointed out by [GKWY20](https://eprint.iacr.org/2019/074.pdf). [GKWY20] also proposes a provable secure instantiation satisfies the property called Tweakable Circular Correlation Robustness (TCCR). More discussions about the concrete security of fixed-key AES based hash are introduced in [GKWWY20](https://eprint.iacr.org/2019/1168.pdf). +Several instantiations of hash function based on fix-key AES are proposed inspired by the work of Bellare et al. However, most of them have some security flaws as pointed out by [GKWY20](https://eprint.iacr.org/2019/074.pdf). (GKWY20) also proposes a provable secure instantiation satisfies the property called Tweakable Circular Correlation Robustness (TCCR). More discussions about the concrete security of fixed-key AES based hash are introduced in [GKWWY20](https://eprint.iacr.org/2019/1168.pdf). The TCCR hash based on fixed-key AES is defined as follows. $$\sH(i,x) = \mathsf{TCCR\_Hash}(i,x) = \pi(\pi(x)\oplus i)\oplus\pi(x),$$ -where $x$ is a $128$-bit string, $i$ a public $128$-bit $\mathsf{tweak}$, and $\pi(x) = \aes(k,x)$ for any fixed-key $k$. \ No newline at end of file +where $x$ is a $128$-bit string, $i$ a public $128$-bit $\mathsf{tweak}$, and $\pi(x) = \aes(k,x)$ for any fixed-key $k$. diff --git a/book/src/introduction.md b/book/src/introduction.md index 1b34395553..cdcbc403e7 100644 --- a/book/src/introduction.md +++ b/book/src/introduction.md @@ -1,6 +1,6 @@ # Introduction -This page hosts documentations and specifications for some of the cryptographic algorithms of [Mina](https://minaprotocol.com/). [For the Rust documentation, see here](rustdoc). +This page hosts documentations and specifications for some of the cryptographic algorithms of [Mina](https://minaprotocol.com/). [For the Rust documentation, see here](https://o1-labs.github.io/proof-systems/rustdoc/). Note that this book is a work in progress, not necessarily reflecting the current state of Mina. diff --git a/book/src/kimchi/arguments.md b/book/src/kimchi/arguments.md index 1867905caa..9040bfb94f 100644 --- a/book/src/kimchi/arguments.md +++ b/book/src/kimchi/arguments.md @@ -5,6 +5,7 @@ In the previous section we saw how we can prove that certain equations hold for But first, let's recall the table that summarizes some important notation that will be used extensively: ![kimchi](../img/kimchi.png) + One of the first ideas that we must grasp is the notion of a **circuit**. A circuit can be thought of as a set of gates with wires connections between them. The simplest type of circuit that one could think of is a boolean circuit. Boolean circuits only have binary values: $1$ and $0$, `true` and `false`. From a very high level, boolean circuits are like an intricate network of pipes, and the values could be seen as _water_ or _no water_. Then, gates will be like stopcocks, making water flow or not between the pipes. [This video](https://twitter.com/i/status/1188749430020698112) is a cool representation of this idea. Then, each of these _behaviours_ will represent a gate (i.e. logic gates). One can have circuits that can perform more operations, for instance arithmetic circuits. Here, the type of gates available will be arithmetic operations (additions and multiplications) and wires could have numeric values and we could perform any arbitrary computation. But if we loop the loop a bit more, we could come up with a single `Generic` gate that could represent any arithmetic operation at once. This thoughtful type of gate is the one gate whose concatenation is used in Plonk to describe any relation. Apart from it's wires, these gates are tied to an array of **coefficients** that help describe the functionality. But the problem of this gate is that it takes a large set of them to represent any meaningful function. So instead, recent Plonk-like proof systems have appeared which use **custom gates** to represent repeatedly used functionalities more efficiently than as a series of generic gates connected to each other. Kimchi is one of these protocols. Currently, we give support to specific gates for the `Poseidon` hash function, the `CompleteAdd` operation for curve points, `VarBaseMul` for variable base multiplication, `EndoMulScalar` for endomorphism variable base scalar multiplication, `RangeCheck` for range checks and `ForeignFieldMul` and `ForeignFieldAdd` for foreign field arithmetic. Nonetheless, we have plans to further support many other gates soon, possibly even `Cairo` instructions. @@ -15,4 +16,3 @@ The **execution trace** refers to the state of all the wires throughout the circ Going back to the main motivation of the scheme, recall that we wanted to check that certain equations hold in a given set of numbers. Here's where this claim starts to make sense. The total number of rows in the execution trace will give us a **domain**. That is, we define a mapping between each of the row indices of the execution trace and the elements of a multiplicative group $\mathbb{G}$ with as many elements as rows in the table. Two things to note here. First, if no such group exists we can pad with zeroes. Second, any multiplicative group has a generator $g$ whose powers generate the whole group. Then we can assign to each row a power of $g$. Why do we want to do this? Because this will be the set over which we want to check our equations: we can transform a claim about the elements of a group to a claim like _"these properties hold for each of the rows of this table"_. Interesting, right? - diff --git a/book/src/pickles/accumulation.md b/book/src/pickles/accumulation.md index 9ad8ced432..f03c16bd5a 100644 --- a/book/src/pickles/accumulation.md +++ b/book/src/pickles/accumulation.md @@ -778,7 +778,7 @@ Let $\mathcal{C} \subseteq \FF$ be the challenge space (128-bit GLV decomposed c \openx^{(\rounds)} = \openx^{(\rounds)}_{\chaleval} + \chalu \cdot \openx^{(\rounds)}_{\chaleval\omega} $$ - See [Different functionalities](/plonk/inner_product_api.html) for more details or + See [Different functionalities](../plonk/inner_product_api.html) for more details or [the relevant code](https://github.com/o1-labs/proof-systems/blob/76c678d3db9878730f8a4eead65d1e038a509916/poly-commitment/src/commitment.rs#L785). 1. Compute $\accCom \gets \comm^{(k)} - [\openy'] \cdot \genOpen$ (i.e. st. $\comm^{(k)} = \accCom + [\openy'] \cdot \genOpen$) diff --git a/book/src/pickles/deferred.md b/book/src/pickles/deferred.md index 83489b3a85..0144abb54e 100644 --- a/book/src/pickles/deferred.md +++ b/book/src/pickles/deferred.md @@ -7,7 +7,7 @@ P_p = \langle \vec{e}, \vec{H} \rangle \in \mathbb{E}_p(\mathbb{F}_q) \\ P_q = \langle \vec{e}, \vec{G} \rangle \in \mathbb{E}_q(\mathbb{F}_p) $$ -Respectively. See [Pasta Curves](/specs/pasta.html) for more details. +Respectively. See [Pasta Curves](../specs/pasta.html) for more details. When referring to the $\mathbb{F}_q$-side we mean the proof system for circuit over the field $\mathbb{F}_q$. diff --git a/book/src/pickles/overview.md b/book/src/pickles/overview.md index 08f3b71401..7d2d8bdb7a 100644 --- a/book/src/pickles/overview.md +++ b/book/src/pickles/overview.md @@ -2,7 +2,7 @@ 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: +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. diff --git a/book/src/pickles/zkbook_ips.md b/book/src/pickles/zkbook_ips.md index 0716062284..f5ed648750 100644 --- a/book/src/pickles/zkbook_ips.md +++ b/book/src/pickles/zkbook_ips.md @@ -22,7 +22,7 @@ Ok, so what are inductive SNARKs? Well, first let's describe precisely the afore ## Inductive sets -zk-SNARKs [as defined earlier](./zkbook_plonk.md) allow you to prove for efficiently computable functions $f \colon A \times W \to \mathsf{Bool}$ statements of the form +zk-SNARKs [as defined earlier](../fundamentals/zkbook_plonk.md) allow you to prove for efficiently computable functions $f \colon A \times W \to \mathsf{Bool}$ statements of the form > I know $w \colon W$ such that $f(a, w) = \mathsf{true}$ diff --git a/book/src/plonk/domain.md b/book/src/plonk/domain.md index 186f03758e..4dd79da36a 100644 --- a/book/src/plonk/domain.md +++ b/book/src/plonk/domain.md @@ -7,7 +7,7 @@ We choose a domain $H$ such that it is a multiplicative subgroup of the scalar f Furthermore, as FFT (used for interpolation, [see the section on FFTs](https://o1-labs.github.io/proof-systems/fundamentals/zkbook_fft.html)) works best in domains of size $2^k$ for some $k$, we choose $H$ to be a subgroup of order $2^k$. -Since the [pasta curves](https://o1-labs.github.io/proof-systems/specs/pasta.html) both have scalar fields of prime orders $p$ and $q$, their multiplicative subgroup is of order $p-1$ and $q-1$ respectively (without the zero element). +Since the [pasta curves](https://o1-labs.github.io/proof-systems/specs/pasta.html) both have scalar fields of prime orders $p$ and $q$, their multiplicative subgroup is of order $p-1$ and $q-1$ respectively (without the zero element). [The pasta curves were generated](https://forum.zcashcommunity.com/t/noob-question-about-plonk-halo2/39098) specifically so that both $p-1$ and $q-1$ are multiples of $2^{32}$. We say that they have *2-adicity* of 32. @@ -29,7 +29,7 @@ impl FftParameters for FqParameters { The 2-adicity of 32 means that there's a multiplicative subgroup of size $2^{32}$ that exists in the field. The code above also defines a generator $g$ for it, such that $g^{2^{32}} = 1$ and $g^i \neq 1$ for $i \in [[1, 2^{32}-1]]$ (so it's a **primitive** $2^{32}$-th root of unity). -[Lagrange's theorem](https://en.wikipedia.org/wiki/Lagrange%27s_theorem_(group_theory\)) tells us that if we have a group of order $n$, then we'll have subgroups with orders dividing $n$. So in our case, we have subgroups with all the powers of 2, up to the 32-th power of 2. +[Lagrange's theorem](https://en.wikipedia.org/wiki/Lagrange%27s_theorem_(group_theory)) tells us that if we have a group of order $n$, then we'll have subgroups with orders dividing $n$. So in our case, we have subgroups with all the powers of 2, up to the 32-th power of 2. To find any of these groups, it is pretty straight forward as well. Notice that: @@ -52,11 +52,11 @@ this allows you to easily find subgroups of different sizes of powers of 2, whic ## Efficient computation of the vanishing polynomial -For each curve, we generate a domain $H$ as the set $H = {1, \omega, \omega^2, \cdots, \omega^{n-1}}$. -As we work in a multiplicative subgroup, the polynomial that vanishes in all of these points can be written and efficiently calculated as $Z_H(x) = x^{|H|} - 1$. +For each curve, we generate a domain $H$ as the set $H = {1, \omega, \omega^2, \cdots, \omega^{n-1}}$. +As we work in a multiplicative subgroup, the polynomial that vanishes in all of these points can be written and efficiently calculated as $Z_H(x) = x^{|H|} - 1$. This is because, by definition, $\omega^{|H|} = 1$. If $x \in H$, then $x = \omega^i$ for some $i$, and we have: $$x^{|H|} = (\omega^i)^{|H|} = (\omega^{|H|})^i = 1^i = 1$$ -This optimization is important, as without it calculating the vanishing polynomial would take a number of operations linear in $|H|$ (which is not doable in a verifier circuit, for recursion). +This optimization is important, as without it calculating the vanishing polynomial would take a number of operations linear in $|H|$ (which is not doable in a verifier circuit, for recursion). With the optimization, it takes us a logarithmic number of operation (using [exponentiation by squaring](https://en.wikipedia.org/wiki/Exponentiation_by_squaring)) to calculate the vanishing polynomial. diff --git a/book/src/plonk/zkpm.md b/book/src/plonk/zkpm.md index 84f46f3ec0..c27cec0950 100644 --- a/book/src/plonk/zkpm.md +++ b/book/src/plonk/zkpm.md @@ -54,15 +54,15 @@ $$ **Modified permutation checks.** To recall, the permutation check was originally as follows. For all $h \in H$, * $L_1(h)(Z(h) - 1) = 0$ -* $Z(h)[(a(h) + \beta h + \gamma)(b(h) + \beta k_1 h + \gamma)(c(h) + \beta k_2 h + \gamma)] \\ - = Z(\omega h)[(a(h) + \beta S_{\sigma1}(h) + \gamma)(b(h) + \beta S_{\sigma2}(h) + \gamma)(c(h) + \beta S_{\sigma3}(h) + \gamma)]$ +* $$Z(h)[(a(h) + \beta h + \gamma)(b(h) + \beta k_1 h + \gamma)(c(h) + \beta k_2 h + \gamma)] \\ + = Z(\omega h)[(a(h) + \beta S_{\sigma1}(h) + \gamma)(b(h) + \beta S_{\sigma2}(h) + \gamma)(c(h) + \beta S_{\sigma3}(h) + \gamma)]$$ The modified permuation checks that ensures that the check is performed only on all the values except the last $k$ elements in the witness polynomials are as follows. * For all $h \in H$, $L_1(h)(Z(h) - 1) = 0$ -* For all $h \in \blue{H\setminus \{h_{n-k}, \ldots, h_n\}}$, $\begin{aligned} & Z(h)[(a(h) + \beta h + \gamma)(b(h) + \beta k_1 h + \gamma)(c(h) + \beta k_2 h + \gamma)] \\ - &= Z(\omega h)[(a(h) + \beta S_{\sigma1}(h) + \gamma)(b(h) + \beta S_{\sigma2}(h) + \gamma)(c(h) + \beta S_{\sigma3}(h) + \gamma)] \end{aligned}$ +* For all $h \in \blue{H\setminus \{h_{n-k}, \ldots, h_n\}}$, $$\begin{aligned} & Z(h)[(a(h) + \beta h + \gamma)(b(h) + \beta k_1 h + \gamma)(c(h) + \beta k_2 h + \gamma)] \\ + &= Z(\omega h)[(a(h) + \beta S_{\sigma1}(h) + \gamma)(b(h) + \beta S_{\sigma2}(h) + \gamma)(c(h) + \beta S_{\sigma3}(h) + \gamma)] \end{aligned}$$ * For all $h \in H$, $L_{n-k}(h)(Z(h) - 1) = 0$ diff --git a/book/src/specs/kimchi.md b/book/src/specs/kimchi.md index b46ebd49c5..25a469bdea 100644 --- a/book/src/specs/kimchi.md +++ b/book/src/specs/kimchi.md @@ -913,10 +913,10 @@ v_1$ and $v_2$) of up to 88 bits each. Values can be copied as inputs to the multi range check gadget in two ways: -* [Standard mode] With 3 copies, by copying $v_0, v_1$ and $v_2$ to the first +* (Standard mode) With 3 copies, by copying $v_0, v_1$ and $v_2$ to the first cells of the first 3 rows of the gadget. In this mode the first gate coefficient is set to `0`. -* [Compact mode] With 2 copies, by copying $v_2$ to the first cell of the first +* (Compact mode) With 2 copies, by copying $v_2$ to the first cell of the first row and copying $v_{10} = v_0 + 2^{\ell} \cdot v_1$ to the 2nd cell of row 2. In this mode the first gate coefficient is set to `1`. diff --git a/book/src/specs/pickles.md b/book/src/specs/pickles.md index 4470cd7d67..dc55aab6b8 100644 --- a/book/src/specs/pickles.md +++ b/book/src/specs/pickles.md @@ -8,8 +8,8 @@ Pickles uses a pair of amicable curves called [Pasta](./pasta.md) in order to de These curves are referred to as "tick" and "tock" within the Mina source code. -* Tick - Vesta (a.k.a. Step), constraint domain size $2^{18}$ [block and transaction proofs] -* Tock - Pallas (a.k.a. Wrap), constraint domain size $2^{17}$ [signatures] +* Tick - Vesta (a.k.a. Step), constraint domain size $2^{18}$ (block and transaction proofs) +* Tock - Pallas (a.k.a. Wrap), constraint domain size $2^{17}$ (signatures) The Tock prover does less (only performs recursive verifications and no other logic), so it requires fewer constraints and has a smaller domain size. Internally Pickles refers to Tick and Tock as Step and Wrap, respectively. diff --git a/kimchi/src/circuits/polynomials/range_check/circuitgates.rs b/kimchi/src/circuits/polynomials/range_check/circuitgates.rs index 3fa6ea6202..4d6729f98b 100644 --- a/kimchi/src/circuits/polynomials/range_check/circuitgates.rs +++ b/kimchi/src/circuits/polynomials/range_check/circuitgates.rs @@ -4,10 +4,10 @@ //~ //~ Values can be copied as inputs to the multi range check gadget in two ways: //~ -//~ * [Standard mode] With 3 copies, by copying $v_0, v_1$ and $v_2$ to the first +//~ * (Standard mode) With 3 copies, by copying $v_0, v_1$ and $v_2$ to the first //~ cells of the first 3 rows of the gadget. In this mode the first gate //~ coefficient is set to `0`. -//~ * [Compact mode] With 2 copies, by copying $v_2$ to the first cell of the first +//~ * (Compact mode) With 2 copies, by copying $v_2$ to the first cell of the first //~ row and copying $v_{10} = v_0 + 2^{\ell} \cdot v_1$ to the 2nd cell of row 2. //~ In this mode the first gate coefficient is set to `1`. //~