Skip to content

Commit

Permalink
Repair book links with mdbook-linkcheck
Browse files Browse the repository at this point in the history
  • Loading branch information
volhovm committed Dec 11, 2023
1 parent e3a2871 commit 0fc9487
Show file tree
Hide file tree
Showing 14 changed files with 50 additions and 48 deletions.
2 changes: 1 addition & 1 deletion book/specifications/kimchi/template.md
Original file line number Diff line number Diff line change
Expand Up @@ -195,7 +195,7 @@ Similarly to the generic gate, each values taking part in a lookup can be scaled
The lookup functionality is an opt-in feature of kimchi that can be used by custom gates.
From the user's perspective, not using any gates that make use of lookups means that the feature will be disabled and there will be no overhead to the protocol.

Refer to the [lookup RFC](../rfcs/3-lookup.md) for an overview of the lookup feature.
Please refer to the [lookup RFC](../kimchi/lookup.md) for an overview of the lookup feature.

In this section, we describe the tables kimchi supports, as well as the different lookup selectors (and their associated queries)

Expand Down
8 changes: 4 additions & 4 deletions book/src/fundamentals/zkbook_ips.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Earlier we defined zero-knowledge proofs as being proofs of a computation of a f

We will now go beyond this, and try to define zero-knowledge proof systems for computations that proceed **inductively**. That is, in pieces, and potentially over different locations involving different parties in a distributed manner.

An example of an **inductive computation** would be the verification of the Mina blockchain. Each block producer, when they produce a new block,
An example of an **inductive computation** would be the verification of the Mina blockchain. Each block producer, when they produce a new block,

- verifies that previous state of the chain was arrived at correctly

Expand All @@ -31,7 +31,7 @@ Another way of looking at this is that they let you prove membership in sets of
$A_f := \{ a \colon A \mid \text{There exists } w \colon W \text{ such that} f(a, w) = \mathsf{true} \}$[^1]


These are called [NP sets](todo.link). In intuitive terms, an NP set is one in which membership can be efficiently checked given some "witness" or helper information (which is $w$).
These are called [NP sets](https://en.wikipedia.org/wiki/NP_(complexity)). In intuitive terms, an NP set is one in which membership can be efficiently checked given some "witness" or helper information (which is $w$).

Inductive proof systems let you prove membership in sets that are inductively defined. An inductively defined set is one where membership can be efficiently checked given some helper information, but the computation is explicitly segmented into pieces.

Expand All @@ -45,7 +45,7 @@ We will give a recursive definition of a few concepts. Making this mathematicall



The data of an **inductive rule for a type $A$** is
The data of an **inductive rule for a type $A$** is

- a sequence of inductive sets $A_0, \dots, A_{n-1}$ (note the recursive reference to )

Expand All @@ -59,7 +59,7 @@ The data of an **inductive set over a type $A$** is

The subset of $A$ corresponding to $R$ (which we will for now write $A_R$) is defined inductively as follows.

For $a \colon A$, $a \in A_R$ if and only if
For $a \colon A$, $a \in A_R$ if and only if

- there is some inductive rule $r$ in the sequence $R$ with function $f \colon A \times W_r \times A_{r,0} \times \dots A_{r, n_r-1} \to \mathsf{Bool}$ such that

Expand Down
2 changes: 1 addition & 1 deletion book/src/kimchi/final_check.md
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ $$
\end{align}
$$

here are the actual lagrange basis calculated with the [formula here](lagrange.md), oh and we actually use $L_0$ in the code, not $L_1$, so let's change that as well:
here are the actual lagrange basis calculated with the [formula here](../plonk/lagrange.md), oh and we actually use $L_0$ in the code, not $L_1$, so let's change that as well:

$$
\begin{align}
Expand Down
28 changes: 14 additions & 14 deletions book/src/kimchi/foreign_field_add.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ If $f < n$ then we can easily perform the above computation. But in this gate we
- our foreign field will have 256-bit length
- our native field has 255-bit length

In other words, using 3 limbs of 88 bits each allows us to represent any foreign field element in the range $[0,2^{264})$ for foreign field addition, but only up to $2^{259}$ for foreign field multiplication. Thus, with the current configuration of our limbs, our foreign field must be smaller than $2^{259}$ (because $2^{264} \cdot 2^{255} > {2^{259}}^2 + 2^{259}$, more on this in the [FFmul RFC](https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md).
In other words, using 3 limbs of 88 bits each allows us to represent any foreign field element in the range $[0,2^{264})$ for foreign field addition, but only up to $2^{259}$ for foreign field multiplication. Thus, with the current configuration of our limbs, our foreign field must be smaller than $2^{259}$ (because $2^{264} \cdot 2^{255} > {2^{259}}^2 + 2^{259}$, more on this in [Foreign Field Multiplication](../kimchi/foreign_field_mul.md) or the original [FFmul RFC](https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md).

### Splitting the addition

Expand Down Expand Up @@ -155,13 +155,13 @@ So far, one can recompute the result as follows:
```text
bits 0..............87|88...........175|176...........263
r = (-------r0-------|-------r1-------|-------r2-------)
=
=
a = (-------a0-------|-------a1-------|-------a2-------)
+
s = 1 | -1
·
b = (-------b0-------|-------b1-------|-------b2-------)
-
-
q = -1 |0 | 1
·
f = (-------f0-------|-------f1-------|-------f2-------)
Expand All @@ -174,13 +174,13 @@ Inspired by the halving approach in foreign field multiplication, an optimized v
```text
bits 0..............87|88...........175|176...........263
r = (-------r0------- -------r1-------|-------r2-------)
=
=
a = (-------a0------- -------a1-------|-------a2-------)
+
s = 1 | -1
·
b = (-------b0------- -------b1-------|-------b2-------)
-
-
q = -1 |0 | 1
·
f = (-------f0------- -------f1-------|-------f2-------)
Expand All @@ -193,18 +193,18 @@ f = (-------f0------- -------f1-------|-------f2-------)
$$
\begin{aligned}
r_{bot} &= (a_0 + 2^{88} \cdot a_1) + s \cdot (b_0 + 2^{88} \cdot b_1) - q \cdot (f_0 + 2^{88} \cdot f_1) - c \cdot 2^{176} \\
r_{top} &= a_2 + s \cdot b_2 - q \cdot f_2 + c
r_{top} &= a_2 + s \cdot b_2 - q \cdot f_2 + c
\end{aligned}
$$

with $r_{top} = r_2$ and $c = c_1$.
with $r_{top} = r_2$ and $c = c_1$.

## Gadget

The full foreign field addition/subtraction gadget will be composed of:
The full foreign field addition/subtraction gadget will be composed of:
- $1$ public input row containing the value $1$;
- $n$ rows with `ForeignFieldAdd` gate type:
- for the actual $n$ chained additions or subtractions;
- for the actual $n$ chained additions or subtractions;
- $1$ `ForeignFieldAdd` row for the bound addition;
- $1$ `Zero` row for the final bound addition.
- $1$ `RangeCheck` gadget for the first left input of the chain $a_1 := a$;
Expand All @@ -227,7 +227,7 @@ A total of 20 rows with 15 columns in Kimchi for 1 addition. All ranges below ar
| 9n+7..9n+10 | `multi-range-check` | $u$ |


This mechanism can chain foreign field additions together. Initially, there are $n$ foreign field addition gates, followed by a foreign field addition gate for the bound addition (whose current row corresponds to the next row of the last foreign field addition gate), and an auxiliary `Zero` row that holds the upper bound. At the end, an initial left input range check is performed, which is followed by a $n$ pairs of range check gates for the right input and intermediate result (which become the left input for the next iteration). After the chained inputs checks, a final range check on the bound takes place.
This mechanism can chain foreign field additions together. Initially, there are $n$ foreign field addition gates, followed by a foreign field addition gate for the bound addition (whose current row corresponds to the next row of the last foreign field addition gate), and an auxiliary `Zero` row that holds the upper bound. At the end, an initial left input range check is performed, which is followed by a $n$ pairs of range check gates for the right input and intermediate result (which become the left input for the next iteration). After the chained inputs checks, a final range check on the bound takes place.

For example, chaining the following set of 3 instructions would result in a full gadget with 37 rows:

Expand All @@ -250,7 +250,7 @@ $$add(add(add(a,b),c),d)$$
| 30..33 | `multi-range-check` | $a+b+c+d$ |
| 34..37 | `multi-range-check` | bound |

Nonetheless, such an exhaustive set of checks are not necessary for completeness nor soundness. In particular, only the very final range check for the bound is required. Thus, a shorter gadget that is equally valid and takes $(8*n+4)$ fewer rows could be possible if we can assume that the inputs of each addition are correct foreign field elements. It would follow the next layout (with inclusive ranges):
Nonetheless, such an exhaustive set of checks are not necessary for completeness nor soundness. In particular, only the very final range check for the bound is required. Thus, a shorter gadget that is equally valid and takes $(8*n+4)$ fewer rows could be possible if we can assume that the inputs of each addition are correct foreign field elements. It would follow the next layout (with inclusive ranges):

| Row(s) | Gate type(s) | Witness |
| -------- | ----------------------------------------------------- | ------- |
Expand All @@ -260,7 +260,7 @@ Nonetheless, such an exhaustive set of checks are not necessary for completeness
| n+2 | `Zero` | |
| n+3..n+6 | `multi-range-check` for `bound` | $u$ |

Otherwise, we would need range checks for each new input of the chain, but none for intermediate results; implying $4\cdot n$ fewer rows.
Otherwise, we would need range checks for each new input of the chain, but none for intermediate results; implying $4\cdot n$ fewer rows.

| Row(s) | Gate type(s) | Witness |
| --------------- | ----------------------------------------------------- | --------- |
Expand All @@ -273,7 +273,7 @@ Otherwise, we would need range checks for each new input of the chain, but none
| 5n+7..5n+10 | `multi-range-check` for bound | $u$ |


For more details see the Bound Addition section of the [Foreign Field Multiplication RFC](https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md).
For more details see the Bound Addition section in [Foreign Field Multiplication](../kimchi/foreign_field_mul.md) or the original [Foreign Field Multiplication RFC](https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md).

### Layout

Expand Down Expand Up @@ -326,4 +326,4 @@ TODO: decide if we really want to keep this check or leave it implicit as it is
When we use this gate as part of a larger chained gadget, we should optimize the number of range check rows
to avoid redundant checks. In particular, if the result of an addition becomes one input of another addition, there is no need to check twice that the limbs of that term have the right length.

The sign is now part of the coefficients of the gate. This will allow us to remove the sign check constraint and release one witness cell element. But more importantly, it brings soundness to the gate as it is now possible to wire the $1$ public input to the overflow witness of the final bound check of every addition chain.
The sign is now part of the coefficients of the gate. This will allow us to remove the sign check constraint and release one witness cell element. But more importantly, it brings soundness to the gate as it is now possible to wire the $1$ public input to the overflow witness of the final bound check of every addition chain.
2 changes: 1 addition & 1 deletion book/src/kimchi/foreign_field_mul.md
Original file line number Diff line number Diff line change
Expand Up @@ -610,7 +610,7 @@ $$

### Bound checks

To perform the above range checks we use the *upper bound check* method described in the [Foreign Field Addition RFC](](https://github.com/o1-labs/proof-systems/blob/master/book/src/rfcs/ffadd.md#upper-bound-check)).
To perform the above range checks we use the *upper bound check* method described in the upper bound check section in [Foreign Field Addition](../kimchi/foreign_field_add.md#upper-bound-check).

The upper bound check is as follows. We must constrain $0 \le q < f$ over the positive integers, so

Expand Down
18 changes: 9 additions & 9 deletions book/src/kimchi/maller_15.md
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
# Maller's optimization for kimchi
# Maller's optimization for Kimchi

This document proposes a protocol change for [kimchi](../../specs/kimchi/kimchi.md).
This document proposes a protocol change for [kimchi](../specs/kimchi.md).

## What is Maller's optimization?

See the [section on Maller's optimization](maller.md) for background.
See the [section on Maller's optimization](../plonk/maller.md) for background.

## Overview

Expand Down Expand Up @@ -35,7 +35,7 @@ Note right of Verifier: verifies the evaluation proof \n to check that L(zeta) =
```
-->

In the rest of this document, we review the details and considerations needed to implement this change in [kimchi](../../specs/kimchi/kimchi.md).
In the rest of this document, we review the details and considerations needed to implement this change in [kimchi](../specs/kimchi.md).

## How to deal with a chunked $t$?

Expand All @@ -50,7 +50,7 @@ L = L_0 + x^n L_1 + x^{2n} L_1 + \cdots
$$

where every $L_i$ is of degree $n-1$ at most.
Then we have that
Then we have that

$$
com(L) = com(L_0) + com(x^n \cdot L_1) + com(x^{2n} \cdot L_2) + \cdots
Expand Down Expand Up @@ -87,7 +87,7 @@ To compute it, there are two rules to follow:
* when **scaling** a commitment, its blinding factor gets scalled too:
$$n \cdot com(a) \implies n \cdot r_a$$

As such, if we know $r_f$ and $r_t$, we can compute:
As such, if we know $r_f$ and $r_t$, we can compute:

$$
r_{\tilde L} = r_{\tilde f} + (\zeta^n-1) \cdot r_{\tilde t}
Expand Down Expand Up @@ -130,7 +130,7 @@ $$
\end{align}
$$

Because we use the [inner product polynomial commitment](../../specs/polynomial_commitment.md), we also need:
Because we use the [inner product polynomial commitment](../plonk/polynomial_commitments.md), we also need:

$$
\tilde L(\zeta \omega) = \tilde f(\zeta \omega) - Z_H(\zeta) \cdot \tilde t(\zeta \omega)
Expand All @@ -156,8 +156,8 @@ Prover->Verifier: com(t) (several of them)
Note right of Verifier: generates random point zeta
Verifier->Prover: zeta
Prover->Verifier: L_bar(zeta * omega) = y
Prover->Verifier: proof that L_bar(zeta) = 0
Prover->Verifier: proof that L_bar(zeta * omega) = y
Prover->Verifier: proof that L_bar(zeta) = 0
Prover->Verifier: proof that L_bar(zeta * omega) = y
Note right of Verifier: produces com(L_bar)
Note right of Verifier: verifies the evaluation proof \n to check that L_bar(zeta) = 0
```
Expand Down
4 changes: 2 additions & 2 deletions book/src/pickles/accumulation.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
## Introduction

The trick below was originally described in [Halo](https://eprint.iacr.org/2020/499.pdf),
however we are going to base this post on the abstraction of "accumulation schemes" described by Bünz, Chiesa, Mishra and Spooner in [Proof-Carrying Data from Accumulation Schemes](/https://eprint.iacr.org/2020/499.pdf), in particular the scheme in Appendix A. 2.
however we are going to base this post on the abstraction of "accumulation schemes" described by Bünz, Chiesa, Mishra and Spooner in [Proof-Carrying Data from Accumulation Schemes](https://eprint.iacr.org/2020/499.pdf), in particular the scheme in Appendix A. 2.

Relevant resources include:

Expand Down Expand Up @@ -767,7 +767,7 @@ Note that the accumulator verifier must be proven (in addition to the Kimchi/Plo

Note that the "cycles of curves" (e.g. Pasta cycle) does not show up in this part of the code:
a <u>separate accumulator</u> is needed for each curve and the final verifier must check both accumulators to deem the combined recursive proof valid.
This takes the form of [`passthough` data](passthrough.html) in pickles.
This takes the form of `passthough` data in pickles.

Note however, that the accumulation verifier makes use of both $\GG$-operations and $\FF$-operations,
therefore it (like the Kimchi verifier) also requires [deferred computation](deferred.html).
13 changes: 7 additions & 6 deletions book/src/specs/kimchi.md
Original file line number Diff line number Diff line change
Expand Up @@ -329,7 +329,7 @@ Similarly to the generic gate, each values taking part in a lookup can be scaled
The lookup functionality is an opt-in feature of kimchi that can be used by custom gates.
From the user's perspective, not using any gates that make use of lookups means that the feature will be disabled and there will be no overhead to the protocol.

Refer to the [lookup RFC](../rfcs/3-lookup.md) for an overview of the lookup feature.
Please refer to the [lookup RFC](../kimchi/lookup.md) for an overview of the lookup feature.

In this section, we describe the tables kimchi supports, as well as the different lookup selectors (and their associated queries)

Expand Down Expand Up @@ -1103,7 +1103,7 @@ left_input +/- right_input = field_overflow * foreign_modulus + result

##### Documentation

For more details please see the [Foreign Field Addition RFC](../rfcs/foreign_field_add.md)
For more details please see the [Foreign Field Addition](../kimchi/foreign_field_add.md) chapter.

##### Mapping

Expand Down Expand Up @@ -1224,7 +1224,8 @@ left_input * right_input = quotient * foreign_field_modulus + remainder

##### Documentation

For more details please see the [Foreign Field Multiplication RFC](https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md)
For more details please see the [Foreign Field Multiplication](../kimchi/foreign_field_add.md)
chapter or the original [Foreign Field Multiplication RFC](https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md)

##### Notations

Expand Down Expand Up @@ -2225,9 +2226,9 @@ The prover then follows the following steps to create the proof:
1. Evaluate the same polynomials without chunking them
(so that each polynomial should correspond to a single value this time).
1. Compute the ft polynomial.
This is to implement [Maller's optimization](https://o1-labs.github.io/mina-book/crypto/plonk/maller_15.html).
This is to implement [Maller's optimization](https://o1-labs.github.io/mina-book/kimchi/maller_15.html).
1. construct the blinding part of the ft polynomial commitment
[see this section](https://o1-labs.github.io/mina-book/crypto/plonk/maller_15.html#evaluation-proof-and-blinding-factors)
[see this section](https://o1-labs.github.io/mina-book/kimchi/maller_15.html#evaluation-proof-and-blinding-factors)
1. Evaluate the ft polynomial at $\zeta\omega$ only.
1. Setup the Fr-Sponge
1. Squeeze the Fq-sponge and absorb the result with the Fr-Sponge.
Expand Down Expand Up @@ -2343,7 +2344,7 @@ Essentially, this steps verifies that $f(\zeta) = t(\zeta) * Z_H(\zeta)$.
unless a polynomial has its evaluation provided by the proof
in which case the evaluation should be used in place of the commitment.
1. Compute the (chuncked) commitment of $ft$
(see [Maller's optimization](../crypto/plonk/maller_15.html)).
(see [Maller's optimization](../kimchi/maller_15.md)).
1. List the polynomial commitments, and their associated evaluations,
that are associated to the aggregated evaluation proof in the proof:
* recursion
Expand Down
2 changes: 1 addition & 1 deletion book/src/specs/pickles.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Pickles is Mina’s inductive zk-SNARK composition system. It lets you construct

---

Pickles uses a pair of amicable curves called [Pasta](../pasta_curves.md) in order to deliver incremental verifiable computation efficiently.
Pickles uses a pair of amicable curves called [Pasta](./pasta.md) in order to deliver incremental verifiable computation efficiently.

These curves are referred to as "tick" and "tock" within the Mina source code.

Expand Down
6 changes: 3 additions & 3 deletions book/src/specs/poseidon.md
Original file line number Diff line number Diff line change
Expand Up @@ -149,15 +149,15 @@ and the following permutation configuration:

### Poseidon-Fp

You can find the MDS matrix and round constants we use in [/poseidon/src/pasta/fp_kimchi.rs](/poseidon/src/pasta/fp_kimchi.rs).
You can find the MDS matrix and round constants we use in [/poseidon/src/pasta/fp_kimchi.rs](https://github.com/o1-labs/proof-systems/tree/master/poseidon/src/pasta/fp_kimchi.rs).

### Poseidon-Fq

You can find the MDS matrix and round constants we use in [/poseidon/src/pasta/fp_kimchi.rs](/poseidon/src/pasta/fq_kimchi.rs).
You can find the MDS matrix and round constants we use in [/poseidon/src/pasta/fp_kimchi.rs](https://github.com/o1-labs/proof-systems/tree/master/poseidon/src/pasta/fq_kimchi.rs).

## Test vectors

We have test vectors contained in [/poseidon/src/tests/test_vectors/kimchi.json](/poseidon/src/tests/test_vectors/kimchi.json).
We have test vectors contained in [/poseidon/src/tests/test_vectors/kimchi.json](https://github.com/o1-labs/proof-systems/tree/master/poseidon/src/tests/test_vectors/kimchi.json).

## Pointers to the OCaml code

Expand Down
Loading

0 comments on commit 0fc9487

Please sign in to comment.