Skip to content

Commit

Permalink
Merge pull request #2194 from o1-labs/volhovm/1359-add-mdbook-linkche…
Browse files Browse the repository at this point in the history
…ck-fork

Add mdbook-linkcheck support via o1labs fork [5min]
  • Loading branch information
dannywillems authored May 8, 2024
2 parents 5a740e3 + 1dd7ed8 commit d640969
Show file tree
Hide file tree
Showing 14 changed files with 46 additions and 33 deletions.
24 changes: 14 additions & 10 deletions book/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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:
Expand Down
9 changes: 9 additions & 0 deletions book/book.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions book/src/fundamentals/zkbook_2pc/fkaes.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$.
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$.
2 changes: 1 addition & 1 deletion book/src/introduction.md
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
2 changes: 1 addition & 1 deletion book/src/kimchi/arguments.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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?

2 changes: 1 addition & 1 deletion book/src/pickles/accumulation.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$)

Expand Down
2 changes: 1 addition & 1 deletion book/src/pickles/deferred.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$.

Expand Down
2 changes: 1 addition & 1 deletion book/src/pickles/overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
2 changes: 1 addition & 1 deletion book/src/pickles/zkbook_ips.md
Original file line number Diff line number Diff line change
Expand Up @@ -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}$
Expand Down
10 changes: 5 additions & 5 deletions book/src/plonk/domain.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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:

Expand All @@ -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.
8 changes: 4 additions & 4 deletions book/src/plonk/zkpm.md
Original file line number Diff line number Diff line change
Expand Up @@ -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$

Expand Down
4 changes: 2 additions & 2 deletions book/src/specs/kimchi.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`.

Expand Down
4 changes: 2 additions & 2 deletions book/src/specs/pickles.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 2 additions & 2 deletions kimchi/src/circuits/polynomials/range_check/circuitgates.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
//~
Expand Down

0 comments on commit d640969

Please sign in to comment.