diff --git a/.github/workflows/benches.yml b/.github/workflows/benches.yml index e8ac86e6b9..7fd1fe8e2e 100644 --- a/.github/workflows/benches.yml +++ b/.github/workflows/benches.yml @@ -17,7 +17,7 @@ jobs: if: github.event.label.name == 'benchmark' steps: - name: Checkout PR - uses: actions/checkout@v2 + uses: actions/checkout@v4.1.1 # as action-rs does not seem to be maintained anymore, building from # scratch the environment using rustup diff --git a/.github/workflows/coverage.yml.disabled b/.github/workflows/coverage.yml.disabled index f9f00e3503..837124ea24 100644 --- a/.github/workflows/coverage.yml.disabled +++ b/.github/workflows/coverage.yml.disabled @@ -17,7 +17,7 @@ jobs: timeout-minutes: 60 runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2.3.4 + - uses: actions/checkout@v4.1.1 with: persist-credentials: false diff --git a/.github/workflows/gh-page.yml b/.github/workflows/gh-page.yml index edbccf8ca3..7077069ded 100644 --- a/.github/workflows/gh-page.yml +++ b/.github/workflows/gh-page.yml @@ -16,7 +16,7 @@ jobs: steps: - name: Checkout Repository - uses: actions/checkout@v2 + uses: actions/checkout@v4.1.1 # as action-rs does not seem to be maintained anymore, building from # scratch the environment using rustup diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 13ec23a3ac..82f1ecd840 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -28,7 +28,7 @@ jobs: name: Run some basic checks and tests steps: - name: Checkout PR - uses: actions/checkout@v3 + uses: actions/checkout@v4.1.1 # as action-rs does not seem to be maintained anymore, building from # scratch the environment using rustup @@ -62,7 +62,7 @@ jobs: - name: Install cargo-spec for specifications run: | eval $(opam env) - cargo install cargo-spec + cargo install --locked cargo-spec - name: Build the kimchi specification run: | diff --git a/.gitignore b/.gitignore index 3a29d80589..fb03a39692 100644 --- a/.gitignore +++ b/.gitignore @@ -25,4 +25,6 @@ _build *.html # If symlink created for kimchi-visu -tools/srs \ No newline at end of file +tools/srs + +.ignore diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 3d3c479436..ed881acc75 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -48,3 +48,24 @@ cargo fmt ``` These are enforced by GitHub PR checks, so be sure to have any errors produced by the above tools fixed before pushing the code to your pull request branch. Refer to `.github/workflows` for all PR checks. + +## Branching policy + +Generally, proof-systems intends to be synchronized with the mina repository (see their [README-branching.md](https://github.com/MinaProtocol/mina/blob/develop/README-branching.md)), and so its branching policy is quite similar. However several important (some, temporary) distinctions exist: + +- `compatible`: + - Compatible with `rampup` in `mina`. + - Mina's `compatible`, similarly to mina's `master`, does not have `proof-systems`. +- `berkley`: future hardfork release, will be going out to berkeley. + - This is where hotfixes go. +- `develop`: matches mina's `develop`, soft fork-compatibility. + - Also used by `mina/o1js-main` and `o1js/main`. +- `master`: future feature work development, containing breaking changes. Anything that does not need to be released alongside mina. + - Note that `mina`'s `master` does not depend on `proof-systems` at all. +- `izmir`: next hardfork release after berkeley. +- In the future: + - `master`/`develop` will reverse roles and become something like gitflow. + - After Berkeley release `compatible` will become properly synced with `mina/compatible`. +- Direction of merge: + - Back-merging: `compatible` into `berkeley` into `develop` into `master`. + - Front-merging (introducing new features): other direction, but where you start depends on where the feature belongs. diff --git a/Cargo.toml b/Cargo.toml index c50da37068..3d0d91c9cb 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,6 +14,7 @@ members = [ "utils", "internal-tracing", ] +resolver = "2" [profile.release] lto = true diff --git a/book/Cargo.toml b/book/Cargo.toml index 8bf747f208..2a0d222bc7 100644 --- a/book/Cargo.toml +++ b/book/Cargo.toml @@ -10,4 +10,6 @@ edition = "2021" license = "Apache-2.0" [build-dependencies] -cargo-spec = { version = "0.5.0" } \ No newline at end of file +cargo-spec = { version = "0.5.0" } +time = { version = "~0.3.23" } # This crate is a known bad-actor for breaking rust version support. +plist = { version = "~1.5.0" } # This crate improperly constrains its bad-actor dependency (`time`). diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 8b6e482e3e..f30839da67 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -9,15 +9,15 @@ - [Rings](./fundamentals/zkbook_rings.md) - [Fields](./fundamentals/zkbook.md) - [Polynomials](./fundamentals/zkbook_polynomials.md) - - [Multiplying polynomials](./fundamentals/zkbook_multiplying_polynomials.md) - - [Fast Fourier transform](./fundamentals/zkbook_fft.md) + - [Multiplying Polynomials](./fundamentals/zkbook_multiplying_polynomials.md) + - [Fast Fourier Transform](./fundamentals/zkbook_fft.md) -# Cryptographic tools +# Cryptographic Tools - [Commitments](./fundamentals/zkbook_commitment.md) -- [Polynomial commitments](./plonk/polynomial_commitments.md) - - [Inner product argument](./plonk/inner_product.md) - - [Different functionnalities](./plonk/inner_product_api.md) +- [Polynomial Commitments](./plonk/polynomial_commitments.md) + - [Inner Product Argument](./plonk/inner_product.md) + - [Different Functionnalities](./plonk/inner_product_api.md) - [Two Party Computation](./fundamentals/zkbook_2pc/overview.md) - [Garbled Circuits](./fundamentals/zkbook_2pc/gc.md) - [Basics](./fundamentals/zkbook_2pc/basics.md) @@ -27,71 +27,50 @@ - [Half Gate](./fundamentals/zkbook_2pc/halfgate.md) - [Full Description](./fundamentals/zkbook_2pc/fulldesc.md) - [Fixed-Key-AES Hashes](./fundamentals/zkbook_2pc/fkaes.md) - - [Oblivious Transfer](./fundamentals/zkbook_2pc/ot.md) - [Base OT](./fundamentals/zkbook_2pc/baseot.md) - [OT Extension](./fundamentals/zkbook_2pc/ote.md) - - [Full Protocol](./fundamentals/zkbook_2pc/2pc.md) - -# Proof systems - -- [Overview](./fundamentals/proof_systems.md) -- [zk-SNARKs](./fundamentals/zkbook_plonk.md) -- [Custom constraints](./fundamentals/custom_constraints.md) +- [Proof Systems](./fundamentals/proof_systems.md) + - [zk-SNARKs](./fundamentals/zkbook_plonk.md) # Background on PLONK - [Overview](./plonk/overview.md) -- [Glossary](./plonk/glossary.md) + - [Glossary](./plonk/glossary.md) - [Domain](./plonk/domain.md) -- [Lagrange basis in multiplicative subgroups](./plonk/lagrange.md) -- [Non-interaction with fiat-shamir](./plonk/fiat_shamir.md) +- [Lagrange Basis in Multiplicative Subgroups](./plonk/lagrange.md) +- [Non-Interactivity via Fiat-Shamir](./plonk/fiat_shamir.md) - [Plookup](./plonk/plookup.md) -- [Maller's optimization](./plonk/maller.md) +- [Maller's Optimization](./plonk/maller.md) +- [Zero-Column Approach to Zero-Knowledge](./plonk/zkpm.md) # Kimchi - [Overview](./kimchi/overview.md) - - [Arguments](./kimchi/arguments.md) - - [Custom gates](./kimchi/gates.md) - - [Permutation](./kimchi/permut.md) - - [Lookup](./kimchi/lookup.md) - -# Snarky +- [Arguments](./kimchi/arguments.md) +- [Final Check](./kimchi/final_check.md) +- [Maller's Optimization for Kimchi](./kimchi/maller_15.md) +- [Lookup Tables](./kimchi/lookup.md) + - [Extended Lookup Tables](./kimchi/extended-lookup-tables.md) +- [Custom Constraints](./kimchi/custom_constraints.md) +- [Custom Gates](./kimchi/gates.md) + - [Foreign Field Addition](./kimchi/foreign_field_add.md) + - [Foreign Field Multiplication](./kimchi/foreign_field_mul.md) + - [Keccak](./kimchi/keccak.md) -- [Overview](./snarky/overview.md) -- [API](./snarky/api.md) -- [snarky wrapper](./snarky/snarky-wrapper.md) -- [Kimchi backend](./snarky/kimchi-backend.md) -- [Vars](./snarky/vars.md) -- [Booleans](./snarky/booleans.md) -- [Circuit generation](./snarky/circuit-generation.md) -- [Witness generation](./snarky/witness-generation.md) # Pickles & Inductive Proof Systems - [Overview](./fundamentals/zkbook_ips.md) - [Accumulation](./pickles/accumulation.md) - [Deferred Computation](./pickles/deferred.md) -- [Passthough & Me-Only](./pickles/passthrough.md) - -# RFCs -- [RFC 0: Alternative zero-knowledge](./plonk/zkpm.md) -- [RFC 1: Final check](./plonk/final_check.md) -- [RFC 2: Maller's optimization for kimchi](./plonk/maller_15.md) -- [RFC 3: Plookup integration in kimchi](./rfcs/3-lookup.md) -- [RFC 4: Extended lookup tables](./rfcs/extended-lookup-tables.md) -- [RFC 5: Foreign Field Addition](./rfcs/foreign_field_add.md) -- [RFC 6: Foreign Field Multiplication](./rfcs/foreign_field_mul.md) -- [RFC 7: Keccak](./rfcs/keccak.md) - -# Specifications +# Technical Specifications - [Poseidon hash](./specs/poseidon.md) -- [Polynomial commitment](./specs/poly-commitment.md) -- [Pasta curves](./specs/pasta.md) +- [Polynomial Commitment](./specs/poly-commitment.md) +- [Pasta Curves](./specs/pasta.md) - [Kimchi](./specs/kimchi.md) - [Universal Reference String (URS)](./specs/urs.md) - [Pickles](./specs/pickles.md) diff --git a/book/src/fundamentals/custom_constraints.md b/book/src/fundamentals/custom_constraints.md index e2c7256d68..8773465d1c 100644 --- a/book/src/fundamentals/custom_constraints.md +++ b/book/src/fundamentals/custom_constraints.md @@ -1,58 +1 @@ -This section explains how to design and add a custom constraint to our `proof-systems` library. - -PLONK is an AIOP. That is, it is a protocol in which the prover sends polynomials as messages and the verifier sends random challenges, and then evaluates the prover's polynomials and performs some final checks on the outputs. - -PLONK is very flexible. It can be customized with constraints specific to computations of interest. For example, in Mina, we use a PLONK configuration called kimchi that has custom constraints for poseidon hashing, doing elliptic curve operations, and more. - -A "PLONK configuration" specifies -- The set of types of constraints that you would like to be able to enforce. We will describe below how these types of constraints are specified. -- A number of "eq-able" columns `W` -- A number of "advice" columns `A` - -Under such configuration, a circuit is specified by -- A number of rows `n` -- A vector `cs` of constraint-types of length `n`. I.e., a vector that specifies, for each row, which types of constraints should be enforced on that row. -- A vector `eqs : Vec<(Position, Position)>` of equalities to enforce, where `struct Position { row: usize, column: usize }`. E.g., if the pair `(Position { row: 0, col: 8 }, Position { row: 10, col: 2 })` is in `eqs`, then the circuit is saying the entries in those two positions should be equal, or in other words that they refer to the same value. This is where the distinction between "eq-able" and "advice" columns comes in. The `column` field of a position in the `eqs` array can only refer to one of the first `W` columns. Equalities cannot be enforced on entries in the `A` columns after that. - -Then, given such a circuit, PLONK lets you produce proofs for the statement - -> I know `W + A` "column vectors" of field elements `vs: [Vec; W + A]` such that for each row index `i < n`, the constraint of type `cs[i]` holds on the values `[vs[0][i], ..., vs[W+A - 1][i], vs[0][i+1], ..., vs[W+A - 1][i+1]` and all the equalities in `eqs` hold. I.e., for `(p1, p2)` in `eqs` we have `vs[p1.col][p1.row] == vs[p2.col][p2.row]`. So, a constraint can check the values in two adjacent rows. - -## Specifying a constraint - -Mathematically speaking, a constraint is a multivariate polynomial over the variables $c_{\mathsf{Curr},i}, \dots, v_{\mathsf{Curr}, W+A-1}, v_{\mathsf{Next}, 0}, \dots, v_{\mathsf{Next}, W+A-1}$. In other words, there is one variable corresponding to the value of each column in the "current row" and one variable correspond to the value of each column in the "next row". - -In Rust, $v_{r, i}$ is written `E::cell(Column::Witness(i), r)`. So, for example, the variable $v_{\mathsf{Next}, 3}$ is written -`E::cell(Column::Witness(3), CurrOrNext::Next)`. - - - - let w = |i| v(Column::Witness(i)); -Let's - -## Defining a PLONK configuration - -The art in proof systems comes from knowing how to design a PLONK configuration to ensure maximal efficiency for the sorts of computations you are trying to prove. That is, how to choose the numbers of columns `W` and `A`, and how to define the set of constraint types. - -Let's describe the trade-offs involved here. - -The majority of the proving time for the PLONK prover is in -- committing to the `W + A` column polynomials, which have length equal to the number of rows `n` -- committing to the "permutation accumulator polynomial, which has length `n`. -- committing to the quotient polynomial, which reduces to computing `max(k, W)` MSMs of size `n`, where `k` is the max degree of a constraint. -- performing the commitment opening proof, which is mostly dependent on the number of rows `n`. - -So all in all, the proving time is approximately equal to the time to perform `W + A + 1 + max(k - 1, W)` MSMs of size `n`, plus the cost of an opening proof for polynomials of degree `n - 1`. - -and maybe -- computing the combined constraint polynomial, which has degree `k * n` where `k` is the maximum degree of a constraint - -- Increasing `W` and `A` increase proof size, and they potentially impact the prover-time as the prover must compute polynomial commitments to each column, and computing a polynomial commitment corresponds to doing one MSM (multi-scalar multiplication, also called a multi-exponentiation.) - - However, often increasing the number of columns allows you to decrease the number of rows required for a given computation. For example, if you can perform one Poseidon hash in 36 rows with 5 total columns, then you can also perform it in 12 (= 36 / 3) rows with 15 (= 5 * 3) total columns. - - **Decreasing the number of rows (even while keeping the total number of table entries the same) is desirable because it reduces the cost of the polynomial commitment opening proof, which is dominated by a factor linear in the number of rows, and barely depends on the number of columns.** - - Increasing the number of columns also increases verifier time, as the verifier must perform one scalar-multiplication and one hash per column. Proof length is also affected by a larger number of columns, as more polynomials need to be committed and sent along to the verifier. - -There is typically some interplay between these +# Custom constraints diff --git a/book/src/fundamentals/proof_systems.md b/book/src/fundamentals/proof_systems.md index 84b5f8fe97..d281048974 100644 --- a/book/src/fundamentals/proof_systems.md +++ b/book/src/fundamentals/proof_systems.md @@ -1,31 +1,29 @@ -# Overview +# Proof Systems Design Overview Many modern proof systems (and I think all that are in use) are constructed according to the following recipe. 1. You start out with a class of computations. 2. You devise a way to *arithmetize* those computations. That is, to express your computation as a statement about polynomials. - + More specifically, you describe what is often called an "algebraic interactive oracle proof" (AIOP) that encodes your computation. An AIOP is a protocol describing an interaction between a prover and a verifier, in which the prover sends the verifier some "polynomial oracles" (basically a black box function that given a point evaluates a polynomial at that point), the verifier sends the prover random challenges, and at the end, the verifier queries the prover's polynomials at points of its choosing and makes a decision as to whether it has been satisfied by the proof. 3. An AIOP is an imagined interaction between parties. It is an abstract description of the protocol that will be "compiled" into a SNARK. There are several "non-realistic" aspects about it. One is that the prover sends the verifier black-box polynomials that the verifier can evaluate. These polynomials have degree comparable to the size of the computation being verified. If we implemented these "polynomial oracles" by having the prover really send the $O(n)$ size polynomials (say by sending all their coefficients), then we would not have a zk-SNARK at all, since the verifier would have to read this linearly sized polynomial so we would lose succinctness, and the polynomials would not be black-box functions, so we may lose zero-knowledge. - + Instead, when we concretely instantiate the AIOP, we have the prover send constant-sized, hiding *polynomial commitments*. Then, in the phase of the AIOP where the verifier queries the polynomials, the prover sends an *opening proof* for the polynomial commitments which the verifier can check, thus simulating the activity of evaluating the prover's polynomials on your own. - + So this is the next step of making a SNARK: instantiating the AIOP with a polynomial commitment scheme of one's choosing. There are several choices here and these affect the properties of the SNARK you are constructing, as the SNARK will inherit efficiency and setup properties of the polynomial commitment scheme used. -4. An AIOP describes an interactive protocol between the verifier and the prover. In reality, typically, we also want our proofs to be non-interactive. - +4. An AIOP describes an interactive protocol between the verifier and the prover. In reality, typically, we also want our proofs to be non-interactive. + This is accomplished by what is called the [Fiat--Shamir transformation](). The basic idea is this: all that the verifier is doing is sampling random values to send to the prover. Instead, to generate a "random" value, the prover simulates the verifier by hashing its messages. The resulting hash is used as the "random" challenge. - + At this point we have a fully non-interactive proof. Let's review our steps. - + 1. Start with a computation. - + 2. Translate the computation into a statement about polynomials and design a corresponding AIOP. - - 3. Compile the AIOP into an interactive protocol by having the prover send hiding polynomial commitments instead of polynomial oracles. - - 4. Get rid of the verifier-interaction by replacing it with a hash function. I.e., apply the Fiat--Shamir transform. + 3. Compile the AIOP into an interactive protocol by having the prover send hiding polynomial commitments instead of polynomial oracles. + 4. Get rid of the verifier-interaction by replacing it with a hash function. I.e., apply the Fiat--Shamir transform. diff --git a/book/src/kimchi/custom_constraints.md b/book/src/kimchi/custom_constraints.md new file mode 100644 index 0000000000..e2c7256d68 --- /dev/null +++ b/book/src/kimchi/custom_constraints.md @@ -0,0 +1,58 @@ +This section explains how to design and add a custom constraint to our `proof-systems` library. + +PLONK is an AIOP. That is, it is a protocol in which the prover sends polynomials as messages and the verifier sends random challenges, and then evaluates the prover's polynomials and performs some final checks on the outputs. + +PLONK is very flexible. It can be customized with constraints specific to computations of interest. For example, in Mina, we use a PLONK configuration called kimchi that has custom constraints for poseidon hashing, doing elliptic curve operations, and more. + +A "PLONK configuration" specifies +- The set of types of constraints that you would like to be able to enforce. We will describe below how these types of constraints are specified. +- A number of "eq-able" columns `W` +- A number of "advice" columns `A` + +Under such configuration, a circuit is specified by +- A number of rows `n` +- A vector `cs` of constraint-types of length `n`. I.e., a vector that specifies, for each row, which types of constraints should be enforced on that row. +- A vector `eqs : Vec<(Position, Position)>` of equalities to enforce, where `struct Position { row: usize, column: usize }`. E.g., if the pair `(Position { row: 0, col: 8 }, Position { row: 10, col: 2 })` is in `eqs`, then the circuit is saying the entries in those two positions should be equal, or in other words that they refer to the same value. This is where the distinction between "eq-able" and "advice" columns comes in. The `column` field of a position in the `eqs` array can only refer to one of the first `W` columns. Equalities cannot be enforced on entries in the `A` columns after that. + +Then, given such a circuit, PLONK lets you produce proofs for the statement + +> I know `W + A` "column vectors" of field elements `vs: [Vec; W + A]` such that for each row index `i < n`, the constraint of type `cs[i]` holds on the values `[vs[0][i], ..., vs[W+A - 1][i], vs[0][i+1], ..., vs[W+A - 1][i+1]` and all the equalities in `eqs` hold. I.e., for `(p1, p2)` in `eqs` we have `vs[p1.col][p1.row] == vs[p2.col][p2.row]`. So, a constraint can check the values in two adjacent rows. + +## Specifying a constraint + +Mathematically speaking, a constraint is a multivariate polynomial over the variables $c_{\mathsf{Curr},i}, \dots, v_{\mathsf{Curr}, W+A-1}, v_{\mathsf{Next}, 0}, \dots, v_{\mathsf{Next}, W+A-1}$. In other words, there is one variable corresponding to the value of each column in the "current row" and one variable correspond to the value of each column in the "next row". + +In Rust, $v_{r, i}$ is written `E::cell(Column::Witness(i), r)`. So, for example, the variable $v_{\mathsf{Next}, 3}$ is written +`E::cell(Column::Witness(3), CurrOrNext::Next)`. + + + + let w = |i| v(Column::Witness(i)); +Let's + +## Defining a PLONK configuration + +The art in proof systems comes from knowing how to design a PLONK configuration to ensure maximal efficiency for the sorts of computations you are trying to prove. That is, how to choose the numbers of columns `W` and `A`, and how to define the set of constraint types. + +Let's describe the trade-offs involved here. + +The majority of the proving time for the PLONK prover is in +- committing to the `W + A` column polynomials, which have length equal to the number of rows `n` +- committing to the "permutation accumulator polynomial, which has length `n`. +- committing to the quotient polynomial, which reduces to computing `max(k, W)` MSMs of size `n`, where `k` is the max degree of a constraint. +- performing the commitment opening proof, which is mostly dependent on the number of rows `n`. + +So all in all, the proving time is approximately equal to the time to perform `W + A + 1 + max(k - 1, W)` MSMs of size `n`, plus the cost of an opening proof for polynomials of degree `n - 1`. + +and maybe +- computing the combined constraint polynomial, which has degree `k * n` where `k` is the maximum degree of a constraint + +- Increasing `W` and `A` increase proof size, and they potentially impact the prover-time as the prover must compute polynomial commitments to each column, and computing a polynomial commitment corresponds to doing one MSM (multi-scalar multiplication, also called a multi-exponentiation.) + + However, often increasing the number of columns allows you to decrease the number of rows required for a given computation. For example, if you can perform one Poseidon hash in 36 rows with 5 total columns, then you can also perform it in 12 (= 36 / 3) rows with 15 (= 5 * 3) total columns. + + **Decreasing the number of rows (even while keeping the total number of table entries the same) is desirable because it reduces the cost of the polynomial commitment opening proof, which is dominated by a factor linear in the number of rows, and barely depends on the number of columns.** + + Increasing the number of columns also increases verifier time, as the verifier must perform one scalar-multiplication and one hash per column. Proof length is also affected by a larger number of columns, as more polynomials need to be committed and sent along to the verifier. + +There is typically some interplay between these diff --git a/book/src/rfcs/extended-lookup-tables.md b/book/src/kimchi/extended-lookup-tables.md similarity index 99% rename from book/src/rfcs/extended-lookup-tables.md rename to book/src/kimchi/extended-lookup-tables.md index ed8d29bf7c..a2205ddebd 100644 --- a/book/src/rfcs/extended-lookup-tables.md +++ b/book/src/kimchi/extended-lookup-tables.md @@ -1,6 +1,6 @@ -# RFC: Extended lookup tables +# Extended lookup tables -This RFC proposes an extension to our use of lookup tables using the PLOOKUP +This (old) RFC proposes an extension to our use of lookup tables using the PLOOKUP multiset inclusion argument, so that values within lookup tables can be chosen after the constraint system for a circuit has been fixed. diff --git a/book/src/plonk/final_check.md b/book/src/kimchi/final_check.md similarity index 100% rename from book/src/plonk/final_check.md rename to book/src/kimchi/final_check.md diff --git a/book/src/rfcs/foreign_field_add.md b/book/src/kimchi/foreign_field_add.md similarity index 100% rename from book/src/rfcs/foreign_field_add.md rename to book/src/kimchi/foreign_field_add.md diff --git a/book/src/rfcs/foreign_field_mul.md b/book/src/kimchi/foreign_field_mul.md similarity index 100% rename from book/src/rfcs/foreign_field_mul.md rename to book/src/kimchi/foreign_field_mul.md diff --git a/book/src/kimchi/keccak.md b/book/src/kimchi/keccak.md new file mode 100644 index 0000000000..9c00ad6d7c --- /dev/null +++ b/book/src/kimchi/keccak.md @@ -0,0 +1,168 @@ +# Keccak Gate + +The Keccak gadget is comprised of 3 circuit gates (`Xor16`, `Rot64`, and `Zero`) + +Keccak works with 64-bit words. The state is represented using $5\times 5$ matrix +of 64 bit words. Each compression step of Keccak consists of 24 rounds. Let us +denote the state matrix with $A$ (indexing elements as $A[x,y]$), from which we derive +further states as follows in each round. Each round then consists of the following 5 steps: + +$$ +\begin{align} +C[x] &= A[x,0] \oplus A[x,1] \oplus A[x,2] \oplus A[x,3] \oplus A[x,4] \\ +D[x] &= C[x-1] \oplus ROT(C[x+1],1) \\ +E[x,y] &= A[x,y] \oplus D[x] \\ +B[y,2x+3y] &= ROT(E[x,y],\rho[x,y]) \\ +F[x,y] &= B[x,y] \oplus ((NOT\ B[x+1,y]) AND\ B[x+2,y]) \\ +Fp[0,0] &= F[0,0] \oplus RC +\end{align} +$$ + +for $0\leq x, y \leq 4$ and $\rho[x,y]$ is the rotation offset defined for Keccak. +The values are in the table below extracted from the Keccak reference + + +| | x = 3 | x = 4 | x = 0 | x = 1 | x = 2 | +| ----- | ----- | ----- | ----- | ----- | ----- | +| y = 2 | 155 | 231 | 3 | 10 | 171 | +| y = 1 | 55 | 276 | 36 | 300 | 6 | +| y = 0 | 28 | 91 | 0 | 1 | 190 | +| y = 4 | 120 | 78 | 210 | 66 | 253 | +| y = 3 | 21 | 136 | 105 | 45 | 15 | + +## Design Approach: + +The atomic operations are XOR, ROT, NOT, AND. In the sections below, we will describe +the gates for these operations. Below are some common approaches followed in their design. + +To fit within 15 wires, we first decompose each word into its lower and upper 32-bit +components. A gate for an atomic operation works with those 32-bit components at a time. + +Before we describe the specific gate design approaches, below are some constraints in the +Kimchi framework that dictated those approaches. +* only 4 lookups per row +* only first 7 columns are available to the permutation polynomial + +## Rot64 + +It is clear from the definition of the rotation gate that its constraints are complete +(meaning that honest instances always satisfy the constraints). It is left to be proven +that the proposal is sound. In this section, we will give a proof that as soon as we +perform the range checks on the excess and shifted parts of the input, only one possible +assignment satisfies the constraints. This means that there is no dishonest instance that +can make the constraints pass. We will also give an example where one could find wrong +rotation witnesses that would satisfy the constraints if we did not check the range. + +### Necessity of range checks + +First of all, we will illustrate the necessity of range-checks with a simple example. +For the sake of readability, we will use some toy field lengths. In particular, let us +assume that our words have 4 bits, meaning all of the elements between `0x0` and `0xF`. +Next, we will be using the native field $\mathbb{F}_{32}$. + +As we will later see, this choice of field lengths is not enough to perform any 4-bit +rotation, since the operations in the constraints would overflow the native field. +Nonetheless, it will be sufficient for our example where we will only rotate by 1 bit. + +Assume we want to rotate the word `0b1101` (meaning 13) by 1 bit to the left. This gives +us the rotated word `0b1011` (meaning 11). The excess part of the word is `0b1`, whereas +the shifted part corresponds to `0b1010`. We recall the constraints for the rotation gate: + +$$ +\begin{align*} +word \cdot 2^{rot} &= excess \cdot 2^{len} + shifted \\ +rotated &= excess + shifted +\end{align*} +$$ + +Applied to our example, this results in the following equations: + +$$ +\begin{align*} +13 \cdot 2 &= excess \cdot 16 + shifted \\ +11 &= excess + shifted +\end{align*} +$$ + +We can easily check that the proposed values of the shifted `0b1010=10` and the excess +`0b1=1` values satisfy the above constraint because $26 = 1 \cdot 16 + 10$ and $11 = 1 + 10$. +Now, the question is: _can we find another value for excess and shifted, such that their addition results in an incorrect rotated word?_ + +The answer to this question is yes, due to __diophantine equations__. We basically want to find $x,y$ such that $26 = x \cdot 16 + y (\text{ mod } 32)$. The solution to this equation is: + +$$ +\begin{align*} +\forall k \in [0 \ldots 31]: x &= k \ \land \\ +y &= 26 - 16 \cdot k +\end{align*} +$$ + +We chose these word and field lengths to better understand the behaviour of the solution. Here, we can see two "classes" of evaluations. + +- If we choose an even $k$, then $y$ will have the following shape: + - $$26 - 16 \cdot (2 \cdot n) \iff 26 - 32n \equiv_{32} 26 $$ + - Meaning, if $x = 2n$ then $y = 26$. + +- If on the other hand, we chose an odd $k$, then $y$ will have the following shape instead: + - $$26 - 16 \cdot (2 \cdot n + 1) \iff 26 - 32n - 16 \equiv_{32} 26 - 16 = 10$$ + - Meaning, if $x = 2n+1$ then $y = 10$. + +Thus, possible solutions to the diophantine equation are: + +$$ +\begin{align*} +x &= 0, 1, 2, 3, 4, 5 \ldots \\ +y &= 26, 10, 26, 10, 26, 10 \ldots +\end{align*} +$$ + +Note that our valid witness is part of that set of solutions, meaning $x=1$ and $y=10$. Of course, we can also find another dishonest instantiation such as $x=0$ and $y=26$. Perhaps one could think that we do not need to worry about this case, because the resulting rotation word would be $0+26=26$, and if we later use that result as an input to a subsequent gate such as XOR, the value $26$ would not fit and at some point the constraint system would complain. Nonetheless, we still have other solutions to worry about, such as $(x=3, y=10)$ or $(x=5, y=10)$, since they would result in a rotated word that would fit in the word length of 4 bits, yet would be incorrect (not equal to $11$). + +All of the above incorrect solutions differ in one thing: they have different bit lengths. This means that we need to range check the values for the excess and shifted witnesses to make sure they have the correct length. + +### Sufficiency of range checks + +In the following, we will give a proof that performing range checks for these values is not only necessary but also sufficient to prove that the rotation gate is sound. In other words, we will prove there are no two possible solutions of the decomposition constraint that have the correct bit lengths. Now, for the sake of robustness, we will consider 64-bit words and fields with at least twice the bit length of the words (as is our case). + +We will proceed by __contradiction__. Suppose there are two different solutions to the following diophantic equation: + +$$ +\begin{align*} +\forall k \in \mathbb{F}_n: x &= k \ \land \\ +y &= w \cdot 2^r - 2^{64} \cdot k +\end{align*} +$$ + +where $k$ is a parameter to instantiate the solutions, $w$ is the word to be rotated, $r$ is the rotation amount, and $n$ is the field length. + +Then, that means that there are two different solutions, $(0\leq x=a<2^r, 0\leq y=b<2^{64})$ and $(0\leq x=a'<2^r, 0\leq y=b'<2^{64})$ with at least $a \neq a'$ or $b \neq b'$. We will show that this is impossible. + +If both are solutions to the same equation, then: +$$ +\begin{align*} +w \cdot 2^r &= a \cdot 2^{64} + b \\ +w \cdot 2^r &= a'\cdot 2^{64} + b' +\end{align*} +$$ +means that $a \cdot 2^{64} + b = a'\cdot 2^{64} + b'$. Moving terms to the left side, we have an equivalent equality: $2^{64}(a-a') + (b-b')=0 \mod{n}$. There are three cases to consider: + +- $a = a'$ and $b \neq b'$: then $(b - b') \equiv_n 0$ and this can only happen if $b' = b + kn$. But since $n > 2^{64}$, then $b'$ cannot be smaller than $2^{64}$ as it was assumed. CONTRADICTION. + +- $b = b'$ and $a \neq a'$: then $2^{64}(a - a') \equiv_n 0$ and this can only happen if $a' = a + kn$. But since $n > 2^r$, then $a'$ cannot be smaller than $2^r$ as it was assumed. CONTRADICTION. + +- $a\neq a'$ and $b \neq b'$: then we have something like $2^{64} \alpha + \beta \equiv_n 0$. + - This means $\beta \equiv_n -2^{64} \alpha = k \cdot n - 2^{64} \alpha$ for any $k$. + - According to the assumption, both $0\leq a<2^r$ and $0\leq a'<2^r$. This means, the difference $\alpha:=(a - a')$ lies anywhere in between the following interval: + $$1 - 2^r \leq \alpha \leq 2^r - 1$$ + - We plug in this interval to the above equation to obtain the following interval for $\beta$: + $$k\cdot n - 2^{64}(1-2^r)\leq \beta \leq k\cdot n - 2^{64}(2^r - 1) $$ + - We look at this interval from both sides of the inequality: $\beta \geq kn - 2^{64} + 2^{64+r}$ and $\beta \leq kn + 2^{64} - 2^{64+r}$ and we wonder if $kn - 2^{64} + 2^{64+r} \leq kn + 2^{64} - 2^{64+r}$ is at all possible. We rewrite as follows: + $$ + \begin{align*} + 2^{64+r} - 2^{64} &\leq 2^{64} - 2^{64+r}\\ + 2\cdot2^{64+r} &\leq 2\cdot2^{64} \\ + 2^{64+r} &\leq 2^{64} + \end{align*} + $$ + - But this can only happen if $r\leq 0$, which is impossible since we assume $0 < r < 64$. CONTRADICTION. +- EOP. diff --git a/book/src/kimchi/lookup.md b/book/src/kimchi/lookup.md index 9989ac5557..a261672716 100644 --- a/book/src/kimchi/lookup.md +++ b/book/src/kimchi/lookup.md @@ -1,3 +1,318 @@ -## Lookup +# Plookup in Kimchi -TO-DO \ No newline at end of file +In 2020, [plookup](https://eprint.iacr.org/2020/315.pdf) showed how to create lookup proofs. Proofs that some witness values are part of a [lookup table](https://en.wikipedia.org/wiki/Lookup_table). Two years later, an independent team published [plonkup](https://eprint.iacr.org/2022/086) showing how to integrate Plookup into Plonk. + +This document specifies how we integrate plookup in kimchi. It assumes that the reader understands the basics behind plookup. + +## Overview + +We integrate plookup in kimchi with the following differences: + +* we snake-ify the sorted table instead of wrapping it around (see later) +* we allow fixed-ahead-of-time linear combinations of columns of the queries we make +* we only use a single table (XOR) at the moment of this writing +* we allow several lookups (or queries) to be performed within the same row +* zero-knowledgeness is added in a specific way (see later) + +The following document explains the protocol in more detail + +### Recap on the grand product argument of plookup + +As per the Plookup paper, the prover will have to compute three vectors: + +* $f$, the (secret) **query vector**, containing the witness values that the prover wants to prove are part of the lookup table. +* $t$, the (public) **lookup table**. +* $s$, the (secret) concatenation of $f$ and $t$, sorted by $t$ (where elements are listed in the order they are listed in $t$). + +Essentially, plookup proves that all the elements in $f$ are indeed in the lookup table $t$ if and only if the following multisets are equal: + +* $\{(1+\beta)f, \text{diff}(t)\}$ +* $\text{diff}(\text{sorted}(f, t))$ + +where $\text{diff}$ is a new set derived by applying a "randomized difference" between every successive pairs of a vector. For example: + +* $f = \{5, 4, 1, 5\}$ +* $t = \{1, 4, 5\}$ +* $\{\color{blue}{(1+\beta)f}, \color{green}{\text{diff}(t)}\} = \{\color{blue}{(1+\beta)5, (1+\beta)4, (1+\beta)1, (1+\beta)5}, \color{green}{1+\beta 4, 4+\beta 5}\}$ +* $\text{diff}(\text{sorted}(f, t)) = \{1+\beta 1, 1+\beta 4, 4+\beta 4, 4+\beta 5, 5+\beta 5, 5+\beta 5\}$ + +> Note: This assumes that the lookup table is a single column. You will see in the next section how to address lookup tables with more than one column. + +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: $\mathsf{acc}_0 = 1$ +* final: $\mathsf{acc}_n = 1$ +* for every $0 < i \leq n$: + $$ + \mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(\gamma + (1+\beta) f_{i-1}) \cdot (\gamma + t_{i-1} + \beta t_i)}{(\gamma + s_{i-1} + \beta s_{i})(\gamma + s_{n+i-1} + \beta s_{n+i})} + $$ + +Note that the plookup paper uses a slightly different equation to make the proof work. It is possible that the proof would work with the above equation, but for simplicity let's just use the equation published in plookup: + +$$ +\mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(1+\beta) \cdot (\gamma + f_{i-1}) \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})} +$$ + +> Note: in plookup $s$ is longer than $n$ ($|s| = |f| + |t|$), and thus it needs to be split into multiple vectors to enforce the constraint at every $i \in [[0;n]]$. This leads to the two terms in the denominator as shown above, so that the degree of $\gamma (1 + \beta)$ is equal in the nominator and denominator. + +### Lookup tables + +Kimchi uses a single **lookup table** at the moment of this writing; the XOR table. The XOR table for values of 1 bit is the following: + + +| l | r | o | +| --- | --- | --- | +| 1 | 0 | 1 | +| 0 | 1 | 1 | +| 1 | 1 | 0 | +| 0 | 0 | 0 | + +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). + +### Querying the table + +The plookup paper handles a vector of lookups $f$ which we do not have. So the first step is to create such a table from the witness columns (or registers). To do this, we define the following objects: + +* a **query** tells us what registers, in what order, and scaled by how much, are part of a query +* a **query selector** tells us which rows are using the query. It is pretty much the same as a [gate selector](). + +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 = 2\cdot r_1$ + +| 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: + +$$ +\mathsf{acc}_i = \mathsf{acc}_{i-1} \cdot \frac{(1+\beta) \cdot {\color{green}(\gamma + w_0(g^i) + j \cdot w_2(g^i) + j^2 \cdot 2 \cdot w_1(g^i))} \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})} +$$ + +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. + +### Query selector + +The associated **query selector** tells us on which rows the query into the XOR lookup table occurs. + +| row | query selector | +| :---: | :------------: | +| 0 | 1 | +| 1 | 0 | + + +Both the (XOR) lookup table and the query are built-ins in kimchi. The query selector is derived from the circuit at setup time. Currently only the ChaCha gates make use of the lookups. + +With the selectors, the grand product argument for the lookup constraint has the following form: + +$$ +\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}{\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} +\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} +$$ + +### Supporting multiple queries + +Since we would like to allow multiple table lookups 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. + +For example, the `ChaCha0`, `ChaCha1`, and `ChaCha2` gates will jointly 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, $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 + +$$ +\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. + +### Grouping queries by queries pattern + +Associating each query with a selector polynomial is not necessarily efficient. To summarize: + +* the `ChaCha0`, `ChaCha1`, and `ChaCha2` gates that in total make $4$ queries into the XOR table +* the `ChaChaFinal` gate makes another $4$ different queries into the XOR table + +Using the previous section's method, we'd have to use $8$ different lookup selector polynomials for each of the different $8$ queries. Since there's only $2$ use-cases, we can simply group them by **queries patterns** to reduce the number of lookup selector polynomials to $2$. + +The grand product argument for the lookup constraint looks like this now: + +$$ +\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})\times \ldots} +$$ + +where $\color{green}{\mathsf{query}}$ is constructed as: + +$$ +\begin{align} +\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} +$$ + +where, for example the first pattern for the `ChaCha0`, `ChaCha1`, and `ChaCha2` gates looks like this: + +$$ +\begin{align} +\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 \\ +\end{align} +$$ + +Note that there's now $4$ dummy queries, and they only appear when none of the lookup selectors are active. +If a pattern uses less than $4$ queries, it has to be padded with dummy queries as well. + +Finally, note that the denominator of the grand product argument is incomplete in the formula above. +Since the nominator has degree $5$ in $\gamma (1 + \beta)$, the denominator must match too. +This is achieved by having a longer $s$, and referring to it $5$ times. +The denominator thus becomes $\prod_{k=1}^{5} (\gamma (1+\beta) + s_{kn+i-1} + \beta s_{kn+i})$. + +## Back to the grand product argument + +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: + +* 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. + +What about the second vector $s$? + +## The sorted vector $s$ + +We said earlier that in original plonk the size of $s$ is equal to $|s| = |f|+|t|$, where $f$ encodes queries, and $t$ encodes the lookup table. +With our multi-query approach, the second vector $s$ is of the size + +$$n \cdot |\#\text{queries}| + |\text{lookup\_table}|$$ + +That is, it contains the $n$ elements of each **query vectors** (the actual values being looked up, after being combined with the joint combinator, that's $4$ per row), as well as the elements of our lookup table (after being combined as well). + +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$. +The denominator in plonk in the vector form is +$$ +\big(\gamma(1+\beta) + s_{i-1} + \beta s_{i}\big)\big(\gamma(1+\beta)+s_{n+i-1} + \beta s_{n+i}\big) +$$ +which, when interpolated into $h_1$ and $h_2$, becomes +$$ +\big(\gamma(1+\beta) + h_1(x) + \beta h_1(g \cdot x)\big)\big(\gamma(1+\beta) + h_2(x) + \beta h_2(g \cdot x)\big) +$$ + +Since one has to 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}$). +Hence, a separate constraint must be added to enforce that continuity on the interpolated polynomials $h_1$ and $h_2$: + +$$L_{n-1}(X)\cdot\big(h_1(X) - h_2(g \cdot X)\big) \equiv 0$$ + +which is equivalent to checking that $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 corresponding polynomial (in case of plookup approach, to $h_1(X),h_2(X)$). 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: + +1. We cannot use the wrap around trick to make sure that the list is split in two correctly (enforced by $L_{n-1}(h_1(x) - h_2(g \cdot x)) = 0$ which is equivalent to $h_1(g^{n-1}) = h_2(1)$ in the plookup paper) +2. We have even less space to store an entire query vector. Which is actually super correct, as the witness also has some zero-knowledge rows at the end that should not be part of the queries anyway. + +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 + $$(\gamma(1+\beta) + h_1(x) + \beta h_2(x))(\gamma(1+\beta)+ h_2(x) + \beta h_1(x \cdot g))$$ + Whis approach is taken by the [plonkup](https://eprint.iacr.org/2022/086) paper. +* **Snake technique**. By reorganizing $s$ as a snake. This is what is currently implemented in kimchi. + +The snake technique rearranges $s$ into the following shape: + +``` + __ _ + s_0 | s_{2n-1} | | | | + ... | ... | | | | + s_{n-1} | s_n | | | | + ‾‾‾‾‾‾‾‾‾‾‾ ‾‾ ‾ + h1 h2 h3 ... +``` + +Assuming that for now we have only one bend and two polynomials $h_1(X),h_2(X)$, the denominator has the following form: + +$$\big(\gamma(1+\beta) + h_1(x) + \beta h_1(x \cdot g)\big)\big(\gamma(1+\beta)+ h_2(x \cdot g) + \beta h_2(x)\big)$$ + +and the snake doing a U-turn is constrained via $s_{n-1} = s_n$, enforced by the following equation: + +$$L_{n-1} \cdot (h_1(x) - h_2(x)) = 0$$ + +In practice, $s$ will have more sections than just two. +Assume that we have $k$ sections in total, then the denominator generalizes to + +$$ +\prod_{i=1}^k \gamma(1+\beta) + h_i(x \cdot g^{\delta_{0,\ i \text{ mod } 2}}) + \beta h_i(x \cdot g^{\delta_{1,\ i \text{ mod } 2}}) +$$ + +where $\delta_{i,j}$ is Kronecker delta, equal to $1$ when $i$ is even (for the first term) or odd (for the second one), and equal to $0$ otherwise. + +Similarly, the U-turn constraints now become + +$$ +\begin{align*} +L_{n-1}(X) \cdot (h_2(X) - h_1(X)) &\equiv 0\\ +\color{green}L_{0}(X) \cdot (h_3(X) - h_2(X)) &\color{green}\equiv 0\\ +\color{green}L_{n-1}(X) \cdot (h_4(X) - h_3(X)) &\color{green}\equiv 0\\ +\ldots +\end{align*} +$$ + +In our concrete case with $4$ simultaneous lookups the vector $s$ has to be split into $k= 5$ sections --- each denominator term in the accumulator accounts for $4$ queries ($f$) and $1$ table consistency check ($t$). + +## Unsorted $t$ in $s$ + +Note that at setup time, $t$ cannot be sorted lexicographically as it is not combined yet. Since $s$ must be sorted by $t$ (in other words sorting of $s$ must follow the elements of $t$), there are two solutions: + +1. Both the prover and the verifier can sort the combined $t$ lexicographically, so that $s$ can be sorted lexicographically too using typical sorting algorithms +2. The prover can directly sort $s$ by $t$, so that the verifier doesn't have to do any pre-sorting and can just rely on the commitment of the columns of $t$ (which the prover can evaluate in the protocol). + +We take the second approach. +However, this must be done carefully since the combined $t$ entries can repeat. For some $i, l$ such that $i \neq l$, we might have + +$$ +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 a way of correctly sorting the combined vector $s$. At the same time $\text{sorted}(f, t) = \{ 2, 2, 2, 2, 1, 1, 3, 3 \}$ is incorrect since it does not have a second block of $2$s, and thus such an $s$ is not sorted by $t$. + + +## Recap + +So to recap, to create the sorted polynomials $h_i$, the prover: + +1. creates a large query vector which contains the concatenation of the $4$ per-row (combined with the joint combinator) queries (that might contain dummy queries) for all rows +2. creates the (combined with the joint combinator) table vector +3. sorts all of that into a big vector $s$ +4. divides that vector $s$ into as many $h_i$ vectors as a necessary following the snake method +5. interpolate these $h_i$ vectors into $h_i$ polynomials +6. commit to them, and evaluate them as part of the protocol. diff --git a/book/src/plonk/maller_15.md b/book/src/kimchi/maller_15.md similarity index 100% rename from book/src/plonk/maller_15.md rename to book/src/kimchi/maller_15.md diff --git a/book/src/kimchi/overview.md b/book/src/kimchi/overview.md index b8ad73a78e..6ecf0f95e4 100644 --- a/book/src/kimchi/overview.md +++ b/book/src/kimchi/overview.md @@ -1,11 +1,11 @@ # Overview -Here we explain how the Kimchi protocol design is translated into the `proof-systems` repository, from a high level perspective, touching briefly on all the involved aspects of cryptography. The concepts that we will be introducing can be studied more thoroughly by accessing the specific sections in the book. +Here we explain how the Kimchi protocol design is translated into the `proof-systems` repository, from a high level perspective, touching briefly on all the involved aspects of cryptography. The concepts that we will be introducing can be studied more thoroughly by accessing the specific sections in the book. -In brief, the Kimchi protocol requires three different types of arguments `Argument`: -- **Custom gates:** they correspond to each of the specific functions performed by the circuit, which are represented by gate constraints. +In brief, the Kimchi protocol requires three different types of arguments `Argument`: +- **Custom gates:** they correspond to each of the specific functions performed by the circuit, which are represented by gate constraints. - **Permutation:** the equality between different cells is constrained by copy constraints, which are represented by a permutation argument. It represents the wiring between gates, the connections from/to inputs and outputs. -- **Lookup tables:** for efficiency reasons, some public information can be stored by both parties (prover and verifier) instead of wired in the circuit. Examples of these are boolean functions. +- **Lookup tables:** for efficiency reasons, some public information can be stored by both parties (prover and verifier) instead of wired in the circuit. Examples of these are boolean functions. All of these arguments are translated into equations that must hold for a correct witness for the full relation. Equivalently, this is to say that a number of expressions need to evaluate to zero on a certain set of numbers. So there are two problems to tackle here: @@ -24,31 +24,31 @@ $$q(X) := \frac{p(X)}{v_S(X)}$$ And still, where's the hype? If you can provide such a quotient polynomial, one could easily check that if $q(a) = p(a) / v_S(a)$ for a random number $a\in\mathbb{F}$ \ $S$ (recall you will check in a point out of the set, otherwise you would get a $0/0$), then with very high probability that would mean that actually $p(X) = q(X) \cdot v_S(X)$, meaning that $p(X)$ vanishes on the whole set $S$, with **just one point**! -Let's take a deeper look into the _"magic"_ going on here. First, what do we mean by _high probability_? Is this even good enough? And the answer to this question is: as good as you want it to be. +Let's take a deeper look into the _"magic"_ going on here. First, what do we mean by _high probability_? Is this even good enough? And the answer to this question is: as good as you want it to be. **First** we analyse the math in this check. If the polynomial form of $p(X) = q(X) \cdot v_S(X)$ actually holds, then of course for any possible $a\in\mathbb{F}$ \ $S$ the check $p(a) =_? q(a) \cdot v_S(a)$ will hold. But is there any unlucky instantiation of the point $a$ such that $p(a) = q(a) \cdot v_S(a)$ but $p(X) \neq q(X) \cdot v_S(X)$? And the answer is, yes, there are, BUT not many. But how many? How unlikely this is? You already know the answer to this: **Schwartz-Zippel**. Recalling this lemma: -> Given two different polynomials $f(X)$ and $g(X)$ of degree $d$, they can at most intersect (i.e. _coincide_) in $d$ points. Or what's equivalent, let $h(X) := f(X) - g(X)$, the polynomial $h(X)$ can only evaluate to $0$ in at most $d$ points (its roots). +> Given two different polynomials $f(X)$ and $g(X)$ of degree $d$, they can at most intersect (i.e. _coincide_) in $d$ points. Or what's equivalent, let $h(X) := f(X) - g(X)$, the polynomial $h(X)$ can only evaluate to $0$ in at most $d$ points (its roots). Thus, if we interchange $p(X) \rightarrow f(X)$ and $q(X)\cdot v_S(X) \rightarrow g(X)$, both of degree $d$, there are at most $\frac{d}{|\mathbb{F}- S|}$ unlucky points of $a$ that could trick you into thinking that $p(X)$ was a multiple of the vanishing polynomial (and thus being equal to zero on all of $S$). So, how can you make this error probability negligible? By having a field size that is big enough (the formal definition says that the inverse of its size should decrease faster than any polynomial expression). Since we are working with fields of size $2^{255}$, we are safe on this side! **Second**, is this really faster than checking that $p(x)=0$ for all $x\in S$ ? At the end of the day, it seems like we need to evaluate $v_S(a)$, and since this is a degree $|S|$ polynomial it looks like we are still performing about the same order of computations. But here comes math again. _In practice_, we want to define this set $S$ to have a _nice structure_ that allows us to perform some computations more efficiently than with arbitrary sets of numbers. Indeed, this set will normally be a **multiplicative group** (normally represented as $\mathbb{G}$ or $\mathbb{H}$), because in such groups the vanishing polynomial $v_\mathbb{G}(X):=\prod_{\omega\in\mathbb{G}}(X-\omega)$ has an efficient representation $v_\mathbb{G}(X)=X^{|\mathbb{G}|}-1$, which is much faster to evaluate than the above product. -**Third**, we may want to understand what happens with the evaluation of $p(a)$ instead. Since this is a degree $d ≥ |\mathbb{G}|$, it may look like this will as well take a lot of effort. But here's where cryptography comes into play, since the verifier will _never_ get to evaluate the actual polynomial by themselves. Various reasons why. One, if the verifier had access to the full polynomial $p(X)$, then the prover should have sent it along with the proof, which would require $d+1$ coefficients to be represented (and this is no longer succinct for a SNARK). Two, this polynomial could carry some secret information, and if the verifier could recompute evaluations of it, they could learn some private data by evaluating on specific points. So instead, these evaluations will be a "mental game" thanks to **polynomial commitments** and **proofs of evaluation** sent by the prover (for whom a computation in the order of $d$ is not only acceptable, but necessary). The actual proof length will depend heavily on the type of polynomial commitments we are using. For example, in Kate-like commitments, committing to a polynomial takes a constant number of group elements (normally one), whereas in Bootleproof it is logarithmic. But in any case this will be shorter than sending $O(d)$ elements. +**Third**, we may want to understand what happens with the evaluation of $p(a)$ instead. Since this is a degree $d ≥ |\mathbb{G}|$, it may look like this will as well take a lot of effort. But here's where cryptography comes into play, since the verifier will _never_ get to evaluate the actual polynomial by themselves. Various reasons why. One, if the verifier had access to the full polynomial $p(X)$, then the prover should have sent it along with the proof, which would require $d+1$ coefficients to be represented (and this is no longer succinct for a SNARK). Two, this polynomial could carry some secret information, and if the verifier could recompute evaluations of it, they could learn some private data by evaluating on specific points. So instead, these evaluations will be a "mental game" thanks to **polynomial commitments** and **proofs of evaluation** sent by the prover (for whom a computation in the order of $d$ is not only acceptable, but necessary). The actual proof length will depend heavily on the type of polynomial commitments we are using. For example, in Kate-like commitments, committing to a polynomial takes a constant number of group elements (normally one), whereas in Bootleproof it is logarithmic. But in any case this will be shorter than sending $O(d)$ elements. ### Aggregation -So far we have seen how to check that a polynomial equals zero on all of $\mathbb{G}$, with just a single point. This is somehow an aggregation _per se_. But we are left to analyse how we can prove such a thing, for many polynomials. Altogether, if they hold, this will mean that the polynomials encode a correct witness and the relation would be satisfied. These checks can be performed one by one (checking that each of the quotients are indeed correct), or using an efficient aggregation mechanism and checking only **one longer equation at once**. +So far we have seen how to check that a polynomial equals zero on all of $\mathbb{G}$, with just a single point. This is somehow an aggregation _per se_. But we are left to analyse how we can prove such a thing, for many polynomials. Altogether, if they hold, this will mean that the polynomials encode a correct witness and the relation would be satisfied. These checks can be performed one by one (checking that each of the quotients are indeed correct), or using an efficient aggregation mechanism and checking only **one longer equation at once**. So what is the simplest way one could think of to perform this one-time check? Perhaps one could come up with the idea of adding up all of the equations $p_0(X),...,p_n(X)$ into a longer one $\sum_{i=0}^{n} p_i(X)$. But by doing this, we may be cancelling out terms and we could get an incorrect statemement. So instead, we can multiply each term in the sum by a random number. The reason why this trick works is the independence between random numbers. That is, if two different polynomials $f(X)$ and $g(X)$ are both equal to zero on a given $X=x$, then with very high probability the same $x$ will be a root of the random combination $\alpha\cdot f(x) + \beta\cdot g(x) = 0$. If applied to the whole statement, we could transform the $n$ equations into a single equation, -$$\bigwedge_{i_n} p_i(X) =_? 0 \iff_{w.h.p.} \sum_{i=0}^{n} \rho_i \cdot p_i(X) =_? 0 $$ +$$\bigwedge_{i_n} p_i(X) \stackrel{?}{=} 0 \text{\quad iff w.h.p. \quad} \sum_{i=0}^{n} \rho_i \cdot p_i(X) \stackrel{?}{=} 0$$ -This sounds great so far. But we are forgetting about an important part of proof systems which is proof length. For the above claim to be sound, the random values used for aggregation should be verifier-chosen, or at least prover-independent. So if the verifier had to communicate with the prover to inform about the random values being used, we would get an overhead of $n$ field elements. +This sounds great so far. But we are forgetting about an important part of proof systems which is proof length. For the above claim to be sound, the random values used for aggregation should be verifier-chosen, or at least prover-independent. So if the verifier had to communicate with the prover to inform about the random values being used, we would get an overhead of $n$ field elements. Instead, we take advantage of another technique that is called **powers-of-alpha**. Here, we make the assumption that powers of a random value $\alpha^i$ are indistinguishable from actual random values $\rho_i$. Then, we can twist the above claim to use only one random element $\alpha$ to be agreed with the prover as: -$$\bigwedge_{i_n} p_i(X) =_? 0 \iff_{w.h.p.} \sum_{i=0}^{n} \alpha^i \cdot p_i(X) =_? 0 $$ +$$\bigwedge_{i_n} p_i(X) \stackrel{?}{=} 0 \text{\quad iff w.h.p. \quad} \sum_{i=0}^{n} \alpha^i \cdot p_i(X) \stackrel{?}{=} 0$$ diff --git a/book/src/kimchi/permut.md b/book/src/kimchi/permut.md index 3d62293eae..cc82360ef6 100644 --- a/book/src/kimchi/permut.md +++ b/book/src/kimchi/permut.md @@ -1,4 +1 @@ -## Permutation - -TO-DO - +# Permutation diff --git a/book/src/kimchi/zkpm.md b/book/src/kimchi/zkpm.md new file mode 100644 index 0000000000..947a334538 --- /dev/null +++ b/book/src/kimchi/zkpm.md @@ -0,0 +1 @@ +# Zero-Column Approach to Zero-Knowledge diff --git a/book/src/pickles/passthrough.md b/book/src/pickles/passthrough.md deleted file mode 100644 index cc182c4e51..0000000000 --- a/book/src/pickles/passthrough.md +++ /dev/null @@ -1 +0,0 @@ -# Passthrough and Me-Only diff --git a/book/src/plonk/fiat_shamir.md b/book/src/plonk/fiat_shamir.md index fd486f6aba..f1e2b264ef 100644 --- a/book/src/plonk/fiat_shamir.md +++ b/book/src/plonk/fiat_shamir.md @@ -1,4 +1,4 @@ -# non-interaction with fiat-shamir +# Non-Interactivity via Fiat-Shamir So far we've talked about an interactive protocol between a prover and a verifier. The zero-knowledge proof was also in the honest verifier zero-knowedlge (HVZK) model, which is problematic. @@ -15,7 +15,7 @@ This is important as our technique to transform an interactive protocol to a non The whole idea is to replace the verifier by a random oracle, which in practice is a hash function. Note that by doing this, we remove potential leaks that can happen when the verifier acts dishonestly. -Initially the Fiat-Shamir transformation was only applied to sigma protocols, named after the greek letter $\Sigma$ due to its shape resembling the direction of messages (prover sends a commit to a verifier, verifier sends a challenge to a prover, prover sends the final proof to a verifier). +Initially the Fiat-Shamir transformation was only applied to sigma protocols, named after the greek letter $\Sigma$ due to its shape resembling the direction of messages (prover sends a commit to a verifier, verifier sends a challenge to a prover, prover sends the final proof to a verifier). A $Z$ would have made more sense but here we are. ## Generalization of Fiat-Shamir @@ -27,6 +27,6 @@ This is simple: every verifier move can be replaced by a hash of the transcript While we use a hash function for that, a different construction called the [duplex construction](https://keccak.team/sponge_duplex.html) is particularly useful in such situations as they allow to continuously absorb the transcript and produce challenges, while automatically authenticating the fact that they produced a challenge. -[Merlin](https://merlin.cool/) is a standardization of such a construction using the [Strobe protocol framework](https://strobe.sourceforge.io/) (a framework to make use of a duplex construction). -Note that the more recent [Xoodyak](https://keccak.team/xoodyak.html) (part of NIST's lightweight competition) could have been used for this as well. +[Merlin](https://merlin.cool/) is a standardization of such a construction using the [Strobe protocol framework](https://strobe.sourceforge.io/) (a framework to make use of a duplex construction). +Note that the more recent [Xoodyak](https://keccak.team/xoodyak.html) (part of NIST's lightweight competition) could have been used for this as well. Note also that Mina uses none of these standards, instead it simply uses Poseidon (see section on poseidon). diff --git a/book/src/plonk/glossary.md b/book/src/plonk/glossary.md index 4880894fb4..6769ac5f83 100644 --- a/book/src/plonk/glossary.md +++ b/book/src/plonk/glossary.md @@ -1,9 +1,9 @@ # Glossary -* size = number of rows -* columns = number of variables per rows -* cell = a pair (row, column) -* witness = the values assigned in all the cells -* gate = polynomials that act on the variables in a row -* selector vector = a vector of values 1 or 0 (not true for constant vector I think) that toggles gates and variables in a row -* gadget = a series of contiguous rows with some specific gates set (via selector vectors) +* Size: number of rows +* Columns: number of variables per rows +* Cell: a pair (row, column) +* Witness: the values assigned in all the cells +* Gate: polynomials that act on the variables in a row +* Selector vector: a vector of values 1 or 0 (not true for constant vector I think) that toggles gates and variables in a row +* Gadget: a series of contiguous rows with some specific gates set (via selector vectors) diff --git a/book/src/plonk/zkpm.md b/book/src/plonk/zkpm.md index a4a1ba291c..84f46f3ec0 100644 --- a/book/src/plonk/zkpm.md +++ b/book/src/plonk/zkpm.md @@ -19,7 +19,9 @@ Let $f(X)$ be an interpolation polynomial of degree $n-1$ such that $f(h_i) = v_ **Proof sketch.** Recall that the interpolation polynomial is -$f(X) = \sum_{j = 1}^n \prod_{k \neq j} \frac{(X-h_k)}{(h_j-h_k)} v_j$ +$$ +f(X) = \sum_{j = 1}^n \prod_{k \neq j} \frac{(X-h_k)}{(h_j-h_k)} v_j +$$ With $V_{w+1}, \ldots, V_{w+k}$ as random variables, we have, $f(X) = a_{w+1} V_{w+1} + a_{w+2} V_{w+2} + \ldots + a_{w+k} V_{w+k} + a$ @@ -32,16 +34,22 @@ The idea here is to set the last $k$ evaluations to be uniformly random elements **Modified permutation polynomial.** Specifically, set $z(X)$ as follows. -$z(X) = L_1(X) + \sum_{i = 1}^{\blue{n-k-2}} \left(L_{i+1} \prod_{j=1}^i \mathsf{frac}_{i,j} \right) + \blue{t_1 L_{n-k}(X) + \ldots + t_k L_{n}(X) }$ +$$ +z(X) = L_1(X) + \sum_{i = 1}^{\blue{n-k-2}} \left(L_{i+1} \prod_{j=1}^i \mathsf{frac}_{i,j} \right) + \blue{t_1 L_{n-k}(X) + \ldots + t_k L_{n}(X) } +$$ From Lemma 1, the above $z(X)$ has the desired zero knowledge property when $k$ evaluations are revealed. However, we need to modify the other parts of the protocol so that the last $k$ elements are not subject to the permutation evaluation, since they will no longer satisfy the permutation check. Specifically, we will need to modify the permutation polynomial to disregard those random elements, as follows. -$ \begin{aligned} & t(X) = \\ - & (a(X)b(X)q_M(X) + a(X)q_L(X) + b(X)q_R(X) + c(X)q_O(X) + PI(X) + q_C(X)) \frac{1}{z_H(X)} \\ - &+ ((a(X) + \beta X + \gamma)(b(X) + \beta k_1 X + \gamma)(c(X) + \beta k_2X + \gamma)z(X) \blue{(X-h_{n-k}) \ldots (X-h_{n-1})(X-h_n)} ) \frac{\alpha}{z_{H}(X)} \\ - & - ((a(X) + \beta S_{\sigma1}(X) + \gamma)(b(X) + \beta S_{\sigma2}(X) + \gamma)(c(X) + \beta S_{\sigma3}(X) + \gamma)z(X\omega) \blue{(X-h_{n-k}) \ldots (X-h_{n-1})(X-h_n)}) \frac{\alpha}{z_{H}(X)} \\ - & + (z(X)-1)L_1(X) \frac{\alpha^2}{z_H(X)} \\ - & + \blue{(z(X)-1)L_{n-k}(X) \frac{\alpha^3}{z_H(X)} } \end{aligned} $ +$$ +\begin{aligned} & t(X) = \\ + & \Big(a(X)b(X)q_M(X) + a(X)q_L(X) + b(X)q_R(X) + c(X)q_O(X) + PI(X) + q_C(X)\Big) \frac{1}{z_H(X)} \\ + &+ \Big((a(X) + \beta X + \gamma)(b(X) + \beta k_1 X + \gamma)(c(X) + \beta k_2X + \gamma)z(X)\\ + &\qquad\qquad\qquad\times{\blue{(X-h_{n-k}) \ldots (X-h_{n-1})(X-h_n)}} \Big) \frac{\alpha}{z_{H}(X)} \\ + & - \Big((a(X) + \beta S_{\sigma1}(X) + \gamma)(b(X) + \beta S_{\sigma2}(X) + \gamma)(c(X) + \beta S_{\sigma3}(X) + \gamma)z(X\omega)\\ + &\qquad\qquad\qquad\times{\blue{(X-h_{n-k}) \ldots (X-h_{n-1})(X-h_n)}}\Big) \frac{\alpha}{z_{H}(X)} \\ + & + \Big(z(X)-1\Big)\cdot L_1(X) \frac{\alpha^2}{z_H(X)} \\ + & + \blue{\Big(z(X)-1\Big)\cdot L_{n-k}(X) \frac{\alpha^3}{z_H(X)} } \end{aligned} +$$ **Modified permutation checks.** To recall, the permutation check was originally as follows. For all $h \in H$, @@ -50,7 +58,6 @@ $ \begin{aligned} & t(X) = \\ = 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$ diff --git a/book/src/rfcs/3-lookup.md b/book/src/rfcs/3-lookup.md deleted file mode 100644 index 6f256e6a6f..0000000000 --- a/book/src/rfcs/3-lookup.md +++ /dev/null @@ -1,291 +0,0 @@ -# RFC: Plookup in kimchi - -In 2020, [plookup](https://eprint.iacr.org/2020/315.pdf) showed how to create lookup proofs. Proofs that some witness values are part of a [lookup table](https://en.wikipedia.org/wiki/Lookup_table). Two years later, an independent team published [plonkup](https://eprint.iacr.org/2022/086) showing how to integrate Plookup into Plonk. - -This document specifies how we integrate plookup in kimchi. It assumes that the reader understands the basics behind plookup. - -## Overview - -We integrate plookup in kimchi with the following differences: - -* we snake-ify the sorted table instead of wrapping it around (see later) -* we allow fixed-ahead-of-time linear combinations of columns of the queries we make -* we only use a single table (XOR) at the moment of this writing -* we allow several lookups (or queries) to be performed within the same row -* zero-knowledgeness is added in a specific way (see later) - -The following document explains the protocol in more detail - -### Recap on the grand product argument of plookup - -As per the Plookup paper, the prover will have to compute three vectors: - -* $f$, the (secret) **query vector**, containing the witness values that the prover wants to prove are part of the lookup table. -* $t$, the (public) **lookup table**. -* $s$, the (secret) concatenation of $f$ and $t$, sorted by $t$ (where elements are listed in the order they are listed in $t$). - -Essentially, plookup proves that all the elements in $f$ are indeed in the lookup table $t$ if and only if the following multisets are equal: - -* $\{(1+\beta)f, \text{diff}(t)\}$ -* $\text{diff}(\text{sorted}(f, t))$ - -where $\text{diff}$ is a new set derived by applying a "randomized difference" between every successive pairs of a vector. For example: - -* $f = \{5, 4, 1, 5\}$ -* $t = \{1, 4, 5\}$ -* $\{\color{blue}{(1+\beta)f}, \color{green}{\text{diff}(t)}\} = \{\color{blue}{(1+\beta)5, (1+\beta)4, (1+\beta)1, (1+\beta)5}, \color{green}{1+\beta 4, 4+\beta 5}\}$ -* $\text{diff}(\text{sorted}(f, t)) = \{1+\beta 1, 1+\beta 4, 4+\beta 4, 4+\beta 5, 5+\beta 5, 5+\beta 5\}$ - -> Note: This assumes that the lookup table is a single column. You will see in the next section how to address lookup tables with more than one column. - -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$ -* 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})} - $$ - -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})} -$$ - -> 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. - -### Lookup tables - -Kimchi uses a single **lookup table** at the moment of this writing; the XOR table. The XOR table for values of 1 bit is the following: - - -| l | r | o | -| --- | --- | --- | -| 1 | 0 | 1 | -| 0 | 1 | 1 | -| 1 | 1 | 0 | -| 0 | 0 | 0 | - -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). - -### Querying the table - -The plookup paper handles a vector of lookups $f$ which we do not have. So the first step is to create such a table from the witness columns (or registers). To do this, we define the following objects: - -* a **query** tells us what registers, in what order, and scaled by how much, are part of a query -* a **query selector** tells us which rows are using the query. It is pretty much the same as a [gate selector](). - -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$ - -| l | r | o | -| :---: | :---: | :---: | -| 1, r0 | 1, r2 | 2, r1 | - -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})} -$$ - -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. - -### Query selector - -The associated **query selector** tells us on which rows the query into the XOR lookup table occurs. - -| row | query selector | -| :---: | :------------: | -| 0 | 1 | -| 1 | 0 | - - -Both the (XOR) lookup table and the query are built-ins in kimchi. The query selector is derived from the circuit at setup time. Currently only the ChaCha gates make use of the lookups. - -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})} -$$ - -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. - -$$ -\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) -\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**. - -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.) - -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 | - -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}$ - -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 - -Associating each query with a selector polynomial is not necessarily efficient. To summarize: - -* the `ChaCha0`, `ChaCha1`, and `ChaCha2` gates that make $4$ queries into the XOR table -* the `ChaChaFinal` gate makes $4$ different queries into the XOR table - -Using the previous section's method, we'd have to use $8$ different lookup selector polynomials for each of the different $8$ queries. Since there's only $2$ use-cases, we can simply group them by **queries patterns** to reduce the number of lookup selector polynomials to $2$. - -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})} -$$ - -where $\color{green}{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 -\end{align} -$$ - -where, for example the first pattern for the `ChaCha0`, `ChaCha1`, and `ChaCha2` gates looks like this: - -$$ -\begin{align} -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 \\ -\end{align} -$$ - -Note: - -* there's now 4 dummy queries, and they only appear when none of the lookup selectors are active -* if a pattern uses less than 4 queries, they'd have to pad their queries with dummy queries as well - -## Back to the grand product argument - -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: - -* 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. - -What about the second vector? - -## The sorted vector $s$ - -The second vector $s$ is of size - -$$n \cdot |\text{queries}| + |\text{lookup\_table}|$$ - -That is, it contains the $n$ elements of each **query vectors** (the actual values being looked up, after being combined with the joint combinator, that's $4$ per row), as well as the elements of our lookup table (after being combined as well). - -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})} -$$ - -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$$ - -which is equivalent with checking that - -$$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. - -This means two things for the lookup grand product argument: - -1. we cannot use the wrap around trick to make sure that the list is split in two correctly (enforced by $L_{n-1}(h_1(x) - h_2(g \cdot x)) = 0$ which is equivalent to $h_1(g^{n-1}) = h_2(1)$ in the plookup paper) -2. we have even less space to store an entire query vector. Which is actually super correct, as the witness also has some zero-knowledge rows at the end that should not be part of the queries anyway. - -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 - $$(\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. -* **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: - -``` - _ _ - | | | | | - | | | | | - |_| |_| | -``` - -so that the denominator becomes the following equation: - -$$(\gamma(1+\beta) + h_1(x) + \beta h_1(x \cdot g))(\gamma(1+\beta)+ h_2(x \cdot g) + \beta h_2(x))$$ - -and the snake doing a U-turn is constrained via something like - -$$L_{n-1} \cdot (h_1(x) - h_2(x)) = 0$$ - -If there's an $h_3$ (because the table is very large, for example), then you'd have something like: - -$$(\gamma(1+\beta) + h_1(x) + \beta h_1(x \cdot g))(\gamma(1+\beta)+ h_2(x \cdot g) + \beta h_2(x))\color{green}{(\gamma(1+\beta)+ h_3(x) + \beta h_3(x \cdot g))}$$ - -with the added U-turn constraint: - -$$L_{0} \cdot (h_2(x) - h_3(x)) = 0$$ - -## Unsorted $t$ in $s$ - -Note that at setup time, $t$ cannot be sorted as it is not combined yet. Since $s$ needs to be sorted by $t$ (in other words, not sorted, but sorted following the elements of $t$), there are two solutions: - -1. both the prover and the verifier can sort the combined $t$, so that $s$ can be sorted via the typical sorting algorithms -2. the prover can sort $s$ by $t$, so that the verifier doesn't have to do any sorting and can just rely on the commitment of the columns of $t$ (which the prover can evaluate in the protocol). - -We do the second one, but there is an edge-case: the combined $t$ entries can repeat. -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] -$$ - -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. - - -## Recap - -So to recap, to create the sorted polynomials $h_i$, the prover: - -1. creates a large query vector which contains the concatenation of the $4$ per-row (combined with the joint combinator) queries (that might contain dummy queries) for all rows -2. creates the (combined with the joint combinator) table vector -3. sorts all of that into a big vector $s$ -4. divides that vector $s$ into as many $h_i$ vectors as a necessary following the snake method -5. interpolate these $h_i$ vectors into $h_i$ polynomials -6. commit to them, and evaluate them as part of the protocol. diff --git a/book/src/rfcs/keccak.md b/book/src/rfcs/keccak.md index 457c247b97..03174df193 100644 --- a/book/src/rfcs/keccak.md +++ b/book/src/rfcs/keccak.md @@ -1,166 +1 @@ -# RFC: Keccak - -The Keccak gadget is comprised of 3 circuit gates (`Xor16`, `Rot64`, and `Zero`) - -Keccak works with 64-bit words. The state is represented using $5\times 5$ matrix -of 64 bit words. Each compression step of Keccak consists of 24 rounds. Let us -denote the state matrix with $A$ (indexing elements as $A[x,y]$), from which we derive -further states as follows in each round. Each round then consists of the following 5 steps: - -$$ -\begin{align} -C[x] &= A[x,0] \oplus A[x,1] \oplus A[x,2] \oplus A[x,3] \oplus A[x,4] \\ -D[x] &= C[x-1] \oplus ROT(C[x+1],1) \\ -E[x,y] &= A[x,y] \oplus D[x] \\ -B[y,2x+3y] &= ROT(E[x,y],\rho[x,y]) \\ -F[x,y] &= B[x,y] \oplus ((NOT\ B[x+1,y]) AND\ B[x+2,y]) \\ -Fp[0,0] &= F[0,0] \oplus RC -\end{align} -$$ - -for $0\leq x, y \leq 4$ and $\rho[x,y]$ is the rotation offset defined for Keccak. -The values are in the table below extracted from the Keccak reference - - -| | x = 3 | x = 4 | x = 0 | x = 1 | x = 2 | -| ----- | ----- | ----- | ----- | ----- | ----- | -| y = 2 | 155 | 231 | 3 | 10 | 171 | -| y = 1 | 55 | 276 | 36 | 300 | 6 | -| y = 0 | 28 | 91 | 0 | 1 | 190 | -| y = 4 | 120 | 78 | 210 | 66 | 253 | -| y = 3 | 21 | 136 | 105 | 45 | 15 | - -## Design Approach: - -The atomic operations are XOR, ROT, NOT, AND. In the sections below, we will describe -the gates for these operations. Below are some common approaches followed in their design. - -To fit within 15 wires, we first decompose each word into its lower and upper 32-bit -components. A gate for an atomic operation works with those 32-bit components at a time. - -Before we describe the specific gate design approaches, below are some constraints in the -Kimchi framework that dictated those approaches. -* only 4 lookups per row -* only first 7 columns are available to the permutation polynomial - -## Rot64 - -It is clear from the definition of the rotation gate that its constraints are complete -(meaning that honest instances always satisfy the constraints). It is left to be proven -that the proposal is sound. In this section, we will give a proof that as soon as we -perform the range checks on the excess and shifted parts of the input, only one possible -assignment satisfies the constraints. This means that there is no dishonest instance that -can make the constraints pass. We will also give an example where one could find wrong -rotation witnesses that would satisfy the constraints if we did not check the range. - -### Necessity of range checks - -First of all, we will illustrate the necessity of range-checks with a simple example. -For the sake of readability, we will use some toy field lengths. In particular, let us -assume that our words have 4 bits, meaning all of the elements between `0x0` and `0xF`. -Next, we will be using the native field $\mathbb{F}_{32}$. - -As we will later see, this choice of field lengths is not enough to perform any 4-bit -rotation, since the operations in the constraints would overflow the native field. -Nonetheless, it will be sufficient for our example where we will only rotate by 1 bit. - -Assume we want to rotate the word `0b1101` (meaning 13) by 1 bit to the left. This gives -us the rotated word `0b1011` (meaning 11). The excess part of the word is `0b1`, whereas -the shifted part corresponds to `0b1010`. We recall the constraints for the rotation gate: - -$$ -\begin{align*} -word \cdot 2^{rot} &= excess \cdot 2^{len} + shifted \\ -rotated &= excess + shifted -\end{align*} -$$ - -Applied to our example, this results in the following equations: - -$$ -\begin{align*} -13 \cdot 2 &= excess \cdot 16 + shifted \\ -11 &= excess + shifted -\end{align*} -$$ - -We can easily check that the proposed values of the shifted `0b1010=10` and the excess -`0b1=1` values satisfy the above constraint because $26 = 1 \cdot 16 + 10$ and $11 = 1 + 10$. -Now, the question is: _can we find another value for excess and shifted, such that their addition results in an incorrect rotated word?_ - -The answer to this question is yes, due to __diophantine equations__. We basically want to find $x,y$ such that $26 = x \cdot 16 + y (\text{ mod } 32)$. The solution to this equation is: - -$$ -\begin{align*} -\forall k \in [0..31]: & \\ -x &= k \\ -y &= 26 - 16 \cdot k -\end{align*} -$$ - -We chose these word and field lengths to better understand the behaviour of the solution. Here, we can see two "classes" of evaluations. - -- If we choose an even $k$, then $y$ will have the following shape: - - $$26 - 16 \cdot (2 \cdot n) \iff 26 - 32n \equiv_{32} 26 $$ - - Meaning, if $x = 2n$ then $y = 26$. - -- If on the other hand, we chose an odd $k$, then $y$ will have the following shape instead: - - $$26 - 16 \cdot (2 \cdot n + 1) \iff 26 - 32n - 16 \equiv_{32} 26 - 16 = 10$$ - - Meaning, if $x = 2n+1$ then $y = 10$. - -Thus, possible solutions to the diophantine equation are: - -$$ -\begin{align*} -x &= 0, 1, 2, 3, 4, 5... \\ -y &= 26, 10, 26, 10, 26, 10... -\end{align*} -$$ - -Note that our valid witness is part of that set of solutions, meaning $x=1$ and $y=10$. Of course, we can also find another dishonest instantiation such as $x=0$ and $y=26$. Perhaps one could think that we do not need to worry about this case, because the resulting rotation word would be $0+26=26$, and if we later use that result as an input to a subsequent gate such as XOR, the value $26$ would not fit and at some point the constraint system would complain. Nonetheless, we still have other solutions to worry about, such as $(x=3, y=10)$ or $(x=5, y=10)$, since they would result in a rotated word that would fit in the word length of 4 bits, yet would be incorrect (not equal to $11$). - -All of the above incorrect solutions differ in one thing: they have different bit lengths. This means that we need to range check the values for the excess and shifted witnesses to make sure they have the correct length. - -### Sufficiency of range checks - -In the following, we will give a proof that performing range checks for these values is not only necessary but also sufficient to prove that the rotation gate is sound. In other words, we will prove there are no two possible solutions of the decomposition constraint that have the correct bit lengths. Now, for the sake of robustness, we will consider 64-bit words and fields with at least twice the bit length of the words (as is our case). - -We will proceed by __contradiction__. Suppose there are two different solutions to the following diophantic equation: - -$$ -\begin{align*} -\forall k \in \mathbb{F}_n: & \\ -x &= k \\ -y &= w \cdot 2^r - 2^{64} \cdot k -\end{align*} -$$ - -where $k$ is a parameter to instantiate the solutions, $w$ is the word to be rotated, $r$ is the rotation amount, and $n$ is the field length. - -Then, that means that there are two different solutions, $(0\leq x=a<2^r, 0\leq y=b<2^{64})$ and $(0\leq x=a'<2^r, 0\leq y=b'<2^{64})$ with at least $a \neq a'$ or $b \neq b'$. We will show that this is impossible. - -If both are solutions to the same equation, then: -$$ -\begin{align*} -w \cdot 2^r &= a \cdot 2^{64} + b \\ -w \cdot 2^r &= a'\cdot 2^{64} + b' -\end{align*} -$$ -means that $a \cdot 2^{64} + b = a'\cdot 2^{64} + b'$. Moving terms to the left side, we have an equivalent equality: $2^{64}(a-a') + (b-b')=0 \mod{n}$. There are three cases to consider: - -- $a = a'$ and $b \neq b'$: then $(b - b') \equiv_n 0$ and this can only happen if $b' = b + kn$. But since $n > 2^{64}$, then $b'$ cannot be smaller than $2^{64}$ as it was assumed. CONTRADICTION. - -- $b = b'$ and $a \neq a'$: then $2^{64}(a - a') \equiv_n 0$ and this can only happen if $a' = a + kn$. But since $n > 2^r$, then $a'$ cannot be smaller than $2^r$ as it was assumed. CONTRADICTION. - -- $a\neq a'$ and $b \neq b'$: then we have something like $2^{64} \alpha + \beta \equiv_n 0$. - - This means $\beta \equiv_n -2^{64} \alpha = k \cdot n - 2^{64} \alpha$ for any $k$. - - According to the assumption, both $0\leq a<2^r$ and $0\leq a'<2^r$. This means, the difference $\alpha:=(a - a')$ lies anywhere in between the following interval: - - $$1 - 2^r \leq \alpha \leq 2^r - 1$$ - - We plug in this interval to the above equation to obtain the following interval for $\beta$: - - $$k\cdot n - 2^{64}(1-2^r)\leq \beta \leq k\cdot n - 2^{64}(2^r - 1) $$ - - We look at this interval from both sides of the inequality: $\beta \geq kn - 2^{64} + 2^{64+r}$ and $\beta \leq kn + 2^{64} - 2^{64+r}$ and we wonder if $kn - 2^{64} + 2^{64+r} \leq kn + 2^{64} - 2^{64+r}$ is at all possible. We rewrite as follows: - - $$2^{64+r} - 2^{64} \leq 2^{64} - 2^{64+r}$$ - - $$2\cdot2^{64+r} \leq 2\cdot2^{64} $$ - - $$2^{64+r} \leq 2^{64} $$ - - But this can only happen if $r\leq 0$, which is impossible since we assume $0 < r < 64$.CONTRADICTION. -- EOP. +# RFC 7: Keccak diff --git a/book/src/snarky/api.md b/book/src/snarky/api.md deleted file mode 100644 index e8b981a474..0000000000 --- a/book/src/snarky/api.md +++ /dev/null @@ -1,2 +0,0 @@ -# API of Snarky - diff --git a/book/src/snarky/booleans.md b/book/src/snarky/booleans.md deleted file mode 100644 index 7b503f0580..0000000000 --- a/book/src/snarky/booleans.md +++ /dev/null @@ -1,73 +0,0 @@ -# Booleans - -Booleans are a good example of a [snarky variable](./vars.md#snarky-vars). - -```rust -pub struct Boolean(CVar); - -impl SnarkyType for Boolean -where - F: PrimeField, -{ - type Auxiliary = (); - - type OutOfCircuit = bool; - - const SIZE_IN_FIELD_ELEMENTS: usize = 1; - - fn to_cvars(&self) -> (Vec>, Self::Auxiliary) { - (vec![self.0.clone()], ()) - } - - fn from_cvars_unsafe(cvars: Vec>, _aux: Self::Auxiliary) -> Self { - assert_eq!(cvars.len(), Self::SIZE_IN_FIELD_ELEMENTS); - Self(cvars[0].clone()) - } - - fn check(&self, cs: &mut RunState) { - // TODO: annotation? - cs.assert_(Some("boolean check"), vec![BasicSnarkyConstraint::Boolean(self.0.clone())]); - } - - fn deserialize(&self) -> (Self::OutOfCircuit, Self::Auxiliary) { - todo!() - } - - fn serialize(out_of_circuit: Self::OutOfCircuit, aux: Self::Auxiliary) -> Self { - todo!() - } - - fn constraint_system_auxiliary() -> Self::Auxiliary { - todo!() - } - - fn value_to_field_elements(x: &Self::OutOfCircuit) -> (Vec, Self::Auxiliary) { - todo!() - } - - fn value_of_field_elements(x: (Vec, Self::Auxiliary)) -> Self::OutOfCircuit { - todo!() - } -} -``` - -## Check - -The `check()` function is simply constraining the `CVar` $x$ to be either $0$ or $1$ using the following constraint: - -$$x ( x - 1) = 0$$ - -It is trivial to use the [double generic gate](../specs/kimchi.md#double-generic-gate) for this. - -## And - -$$x \land y = x \times y$$ - -## Not - -$$\sim x = 1 - x$$ - -## Or - -* $\sim x \land \sim y = b$ -* $x \lor y = \sim b$ diff --git a/book/src/snarky/circuit-generation.md b/book/src/snarky/circuit-generation.md deleted file mode 100644 index e81793aa03..0000000000 --- a/book/src/snarky/circuit-generation.md +++ /dev/null @@ -1,29 +0,0 @@ -# Circuit generation - -In circuit generation mode, the `has_witness` field of `RunState` is set to the default `CircuitGeneration`, and the program of the user is ran to completion. - -During the execution, the different snarky functions called on `RunState` will create [internal variables](./vars.md) as well as constraints. - -## Creation of variables - -[Variables](./vars.md) can be created via the `compute()` function, which takes two arguments: - -* A `TypeCreation` toggle, which is either set to `Checked` or `Unsafe`. We will describe this below. -* A closure representing the actual computation behind the variable. This computation will only take place when real values are computed, and can be non-deterministic (e.g. random, or external values provided by the user). Note that the closure takes one argument: a `WitnessGeneration`, a structure that allows you to read the runtime values of any variables that were previously created in your program. - -The `compute()` function also needs a type hint to understand what type of [snarky type](./vars.md#snarky-vars) it is creating. - -It then performs the following steps: - -* creates enough [`CVar`](./vars#circuit-vars) to hold the value to be created -* retrieves the auxiliary data needed to create the snarky type (TODO: explain auxiliary data) and create the [`snarky variable`](./vars.md#snarky-vars) out of the `CVar`s and the auxiliary data -* if the `TypeCreation` is set to `Checked`, call the `check()` function on the snarky type (which will constrain the value created), if it is set to `Unsafe` do nothing (in which case we're trusting that the value cannot be malformed, this is mostly used internally and it is highly-likely that users directly making use of `Unsafe` are writing bugs) - -```admonish -At this point we only created variables to hold future values, and made sure that they are constrained. -The actual values will fill the room created by the `CVar` only during the [witness generation](./witness-generation.md). -``` - -## Constraints - -All other functions exposed by the API are basically here to operate on variables and create constraints in doing so. diff --git a/book/src/snarky/kimchi-backend.md b/book/src/snarky/kimchi-backend.md deleted file mode 100644 index 2d2ebf789a..0000000000 --- a/book/src/snarky/kimchi-backend.md +++ /dev/null @@ -1,234 +0,0 @@ -# Kimchi Backend - -![](https://i.imgur.com/KmKU5Pl.jpg) - -Underneath the snarky wrapper (in `snarky/checked_runner.rs`) lies what we used to call the `plonk_constraint_system` or `kimchi_backend` in `snarky/constraint_systen.rs`. - -```admonish -It is good to note that we're planning on removing this abstract separation between the snarky wrapper and the constraint system. -``` - -The logic in the kimchi backend serves two purposes: - -* **Circuit generation**. It is the logic that adds gates to our list of gates (representing the circuit). For most of these gates, the variables used are passed to the backend by the snarky wrapper, but some of them are created by the backend itself (see more in the [variables section](#variables)). -* **Witness generation**. It is the logic that creates the witness - -One can also perform two additional operations once the constraint system has been compiled: - -* Generate the prover and verifier index for the system. -* Get a hash of the constraint system (this includes the circuit, the number of public input) (TODO: verify that this is true) (TODO: what else should be in that hash? a version of snarky and a version of kimchi?). - -## A circuit - -A circuit is either being built, or has been contructed during a circuit generation phase: - -```rust -enum Circuit -where - F: PrimeField, -{ - /** A circuit still being written. */ - Unfinalized(Vec>), - /** Once finalized, a circuit is represented as a digest - and a list of gates that corresponds to the circuit. - */ - Compiled([u8; 32], Vec>), -} -``` - -## State - -The state of the kimchi backend looks like this: - -```rust -where - Field: PrimeField, -{ - /// A counter used to track variables - /// (similar to the one in the snarky wrapper) - next_internal_var: usize, - - /// Instruction on how to compute each internal variable - /// (as a linear combination of other variables). - /// Used during witness generation. - internal_vars: HashMap, Option)>, - - /// The symbolic execution trace table. - /// Each cell is a variable that takes a value during witness generation. - /// (if not set, it will take the value 0). - rows: Vec>>, - - /// The circuit once compiled - gates: Circuit, - - /// The row to use the next time we add a constraint. - // TODO: I think we can delete this - next_row: usize, - - /// The size of the public input - /// (which fills the first rows of our constraint system. - public_input_size: Option, - - // omitted values... -} -``` - -## Variables - -In the backend, there's two types of variables: - -```rust -enum V { - /// An external variable - /// (generated by snarky, via [exists]). - External(usize), - - /// An internal variable is generated to hold an intermediate value, - /// (e.g. in reducing linear combinations to single PLONK positions). - Internal(InternalVar), -} -``` - -Internal variables are basically a `usize` pointing to a hashmap in the state. - -That hashmap tells you how to compute the internal variable during witness generation: it is always a linear combination of other variables (and a constant). - -## Circuit generation - -During circuit generation, the snarky wrapper will make calls to the `add_constraint()` or `add_basic_snarky_constraint` function of the kimchi backend, specifying what gate to use and what variables to use in that gate. - -At this point, the snarky wrapper might have some variables that are not yet tracked as such (with a counter). -Rather, they are constants, or they are a combination of other variables. -You can see that as a small AST representing how to compute a variable. -(See the [variables section](./vars.md#circuit-vars) for more details). - -For this reason, they can hide a number of operations that haven't been constrained yet. -It is the role of the `add_constrain` logic to enforce that at this point constants, as well as linear combinations or scalings of variables, are encoded in the circuit. -This is done by adding enough generic gates (using the `reduce_lincom()` or `reduce_to_var()` functions). - -```admonish -This is a remnant of an optimization targetting R1CS (in which additions are for free). -An issue with this approach is the following: imagine that two circuit variables are created from the same circuit variable, imagine also that the original circuit variable contained a long AST, then both variables might end up creating the same constraints to convert that AST. -Currently, snarkyjs and pickles expose a `seal()` function that allows you to reduce this issue, at the cost of some manual work and mental tracking on the developer. -We should probably get rid of this, while making sure that we can continue to optimize generic gates -(in some cases you can merge two generic gates in one (TODO: give an example of where that can happen)). -Another solution is to keep track of what was reduced, and reuse previous reductions (similar to how we handle constants). -``` - -It is during this "reducing" step that internal variables (known only to the kimchi backend) are created. - -```admonish -The process is quite safe, as the kimchi backend cannot use the snarky wrapper variables directly (which are of type `CVar`). -Since the expected format (see the [variables section](#variables) is a number (of type `usize`), the only way to convert a non-tracked variable (constant, or scale, or linear combination) is to reduce it (and in the process constraining its value). -``` - -Depending on the gate being used, several constraints might be added via the `add_row()` function which does three things: - -1. figure out if there's any wiring to be done -2. add a gate to our list of gates (representing the circuit) -3. add the variables to our _symbolic_ execution trace table (symbolic in the sense that nothing has values yet) - -This process happens as the circuit is "parsed" and the constraint functions of the kimchi backend are called. - -This does not lead to a finalized circuit, see the next section to see how that is done. - -(TODO: ideally this should happen in the same step) - -## Finalization of the circuit. - -So far we've only talked about adding specific constraints to the circuit, but not about how public input are handled. - -The `finalization()` function of the kimchi backend does the following: - -* add as many generic rows as there are public inputs. -* construct the permutation -* computes a cache of the circuit (TODO: this is so unecessary) -* and other things that are not that important - -## Witness generation - -Witness generation happens by taking the finalized state (in the `compute_witness()` function) with a callback that can be used to retrieve the values of external variables (public input and public output). - -The algorithm follows these steps using the symbolic execution table we built during circuit generation: - -1. it initializes the execution trace table with zeros -2. go through the rows related to the public input and set the most-left column values to the ones obtained by the callback. -3. go through the other rows and compute the value of the variables left in the table - -Variables in step 3. should either: - -* be absent (`None`) and evaluated to the default value 0 -* point to an external variable, in which case the closure passed can be used to retrieve the value -* be an internal variable, in which case the value is computed by evaluating the AST that was used to create it. - -## Permutation - -The permutation is used to wire cells of the execution trace table (specifically, cells belonging to the first 7 columns). -It is also known as "copy constraints". - -```admonish -In snarky, the permutation is represented differently from kimchi, and thus needs to be converted to the kimchi's format before a proof can be created. -TODO: merge the representations -``` - -We use the permutation in ingenious ways to optimize circuits. -For example, we use it to encode each constants once, and wire it to places where it is used. -Another example, is that we use it to assert equality between two cells. - -## Implementation details - -There's two aspect of the implementation of the permutation, the first one is a hashmap of equivalence classes, which is used to track all the positions of a variable, the second one is making use of a [union find]() data structure to link variables that are equivalent (we'll talk about that after). - -The two data structures are in the kimchi backend's state: - -```rust -pub struct SnarkyConstraintSystem -where - Field: PrimeField, -{ - equivalence_classes: HashMap>>, - union_finds: disjoint_set::DisjointSet, - // omitted fields... -} -``` - -### equivalence classes - -As said previously, during circuit generation a symbolic execution trace table is created. It should look a bit like this (if there were only 3 columns and 4 rows): - -| | 0 | 1 | 2 | -| :-: | :-: | :-: | :-:| -| 0 | v1 | v1 | | -| 1 | | v2 | | -| 2 | | v2 | | -| 3 | | | v1 | - -From that, it should be clear that all the cells containing the variable `v1` should be connected, -and all the cells containing the variable `v2` should be as well. - -The format that the permutation expects is a [cycle](https://en.wikipedia.org/wiki/Cyclic_permutation): a list of cells where each cell is linked to the next, the last one wrapping around and linking to the first one. - -For example, a cycle for the `v1` variable could be: - -``` -(0, 0) -> (0, 1) -(0, 1) -> (3, 2) -(3, 2) -> (0, 0) -``` - -During circuit generation, a hashmap (called `equivalence_classes`) is used to track all the positions (row and column) of each variable. - -During finalization, all the different cycles are created by looking at all the variables existing in the hashmap. - -### Union finds - -Sometimes, we know that two variables will have equivalent values due to an `assert_equal()` being called to link them. -Since we link two variables together, they need to be part of the same cycle, and as such we need to be able to detect that to construct correct cycles. - -To do this, we use a [union find]() data structure, which allows us to easily find the unions of equivalent variables. - -When an `assert_equal()` is called, we link the two variables together using the `union_finds` data structure. - -During finalization, when we create the cycles, we use the `union_finds` data structure to find the equivalent variables. -We then create a new equivalence classes hashmap to merge the keys (variables) that are in the same set. -This is done before using the equivalence classes hashmap to construct the cycles. diff --git a/book/src/snarky/overview.md b/book/src/snarky/overview.md deleted file mode 100644 index b67c1fa30b..0000000000 --- a/book/src/snarky/overview.md +++ /dev/null @@ -1,32 +0,0 @@ -# Snarky - -Snarky is a frontend to the [kimchi proof system](../kimchi/overview.md). - -It allows users to write circuits that can be proven using kimchi. - -This part of the Mina book documents both how to use snarky, and how its internals work. - -```admonish -Snarky was originally an OCaml library. It also is known as a typescript library: SnarkyJS. -This documentation talks about the Rust implementation, which one can refer to as snarky-rs (but we will just say snarky from now on). -``` - -## High-level design - -Snarky is divided into two parts: - -* **Circuit-generation**: which is also called the setup or compilation phase. It is when snarky turn code written using its library, to a circuit that kimchi can understand. This can later be used by kimchi to produce prover and verifier keys. -* **Witness-generation**: which is also called the proving, or runtime phase. It is when snarky executes the written program and records its state at various point in time to create an execution trace of the program (which we call witness here). This can later be used by kimchi, with a proving key, to produce a zero-knowledge proof. - -A snarky program is constructed using functions exposed by the library. -The API of snarky that one can use to design circuits can be split in three categories: - -* creation of snarky variables (via `compute()`) -* creation of constraints (via `assert` type-functions) -* manipulation of snarky variables (which can sometimes create constraints) - -Snarky itself is divided into three parts: - -* [The high-level API](./api.md) that you can find in `api.rs` and `traits.rs` -* [The snarky wrapper](./snarky-wrapper.md), which contains the logic for creating user variables and composed types (see the section on [Snarky vars](./vars.md#snarky-vars)). -* [The kimchi backend](./kimchi-backend.md), which contains the logic for constructing the circuit as well as the witness. diff --git a/book/src/snarky/snarky-wrapper.md b/book/src/snarky/snarky-wrapper.md deleted file mode 100644 index 725f7c35ec..0000000000 --- a/book/src/snarky/snarky-wrapper.md +++ /dev/null @@ -1,70 +0,0 @@ -# Snarky wrapper - -Snarky, as of today, is constructed as two parts: - -* a snarky wrapper, which is explained in this document -* a backend underneath that wrapper, explained in the [kimchi backend section](./kimchi-backend.md) - -```admonish -This separation exists for legacy reasons, and ideally we should merge the two into a single library. -``` - -The snarky wrapper mostly exists in `checked_runner.rs`, and has the following state: - -```rust -where - F: PrimeField, -{ - /// The constraint system used to build the circuit. - /// If not set, the constraint system is not built. - system: Option>, - - /// The public input of the circuit used in witness generation. - // TODO: can we merge public_input and private_input? - public_input: Vec, - - // TODO: we could also just store `usize` here - pub(crate) public_output: Vec>, - - /// The private input of the circuit used in witness generation. Still not sure what that is, or why we care about this. - private_input: Vec, - - /// If set, the witness generation will check if the constraints are satisfied. - /// This is useful to simulate running the circuit and return an error if an assertion fails. - eval_constraints: bool, - - /// The number of public inputs. - num_public_inputs: usize, - - /// A counter used to track variables (this includes public inputs) as they're being created. - next_var: usize, - - /// Indication that we're running the witness generation (as opposed to the circuit creation). - mode: Mode, -} -``` - -The wrapper is designed to be used in different ways, depending on the fields set. - -```admonish -Ideally, we would like to only run this once and obtain a result that's an immutable compiled artifact. -Currently, `public_input`, `private_input`, `eval_constriants`, `next_var`, and `mode` all need to be mutable. -In the future these should be passed as arguments to functions, and should not exist in the state. -``` - -## Public output - -The support for public output is implemented as kind of a hack. - -When the developer writes a circuit, they have to specify the type of the public output. - -This allows the API to save enough room at the end of the public input, and store the variables used in the public output in the state. - -When the API calls the circuit written by the developer, it expects the public output (as a snarky type) to be returned by the function. -The compilation or proving API that ends up calling that function, can thus obtain the variables of the public output. -With that in hand, the API can continue to write the circuit to enforce an equality constraint between these variables being returned and the public output variable that it had previously stored in the state. - -Essentially, the kimchi backend will turn this into as many wiring as there are `CVar` in the public output. - -During witness generation, we need a way to modify the witness once we know the values of the public output. -As the public output `CVar`s were generated from the snarky wrapper (and not from the kimchi backend), the snarky wrapper should know their values after running the given circuit. diff --git a/book/src/snarky/vars.md b/book/src/snarky/vars.md deleted file mode 100644 index 7a1e3a3be7..0000000000 --- a/book/src/snarky/vars.md +++ /dev/null @@ -1,135 +0,0 @@ -# Vars - -In this section we will introduce two types of variables: - -* Circuit vars, or `CVar`s, which are low-level variables representing field elements. -* Snarky vars, which are high-level variables that user can use to create more meaningful programs. - -## Circuit vars - -In snarky, we first define circuit variables (TODO: rename Field variable?) which represent field elements in a circuit. -These circuit variables, or cvars, can be represented differently in the system: - -```rust -pub enum CVar -where - F: PrimeField, -{ - /// A constant. - Constant(F), - - /// A variable that can be refered to via a `usize`. - Var(usize), - - /// The addition of two other [CVar]s. - Add(Box>, Box>), - - /// Scaling of a [CVar]. - Scale(F, Box>), -} -``` - -One can see a CVar as an AST, where two atoms exist: a `Var(usize)` which represents a private input, an a `Constant(F)` which represents a constant. -Anything else represents combinations of these two atoms. - -### Constants - -Note that a circuit variable does not represent a value that has been constrained in the circuit (yet). -This is why we need to know if a cvar is a constant, so that we can avoid constraining it too early. -For example, the following code does not encode 2 or 1 in the circuit, but will encode 3: - -```rust -let x: CVar = state.exists(|_| 2) + state.exists(|_| 3); -state.assert_eq(x, y); // 3 and y will be encoded in the circuit -``` - -whereas the following code will encode all variables: - -```rust -let x = y + y; -let one: CVar = state.exists(|_| 1); -assert_eq(x, one); -``` - -### Non-constants - -Right after being created, a `CVar` is not constrained yet, and needs to be constrained by the application. -That is unless the application wants the `CVar` to be a constant that will not need to be constrained (see previous example) or because the application wants the `CVar` to be a random value (unlikely) (TODO: we should add a "rand" function for that). - -In any case, a circuit variable which is not a constant has a value that is not known yet at circuit-generation time. -In some situations, we might not want to constrain the - - -### When do variables get constrained? - -In general, a circuit variable only gets constrained by an assertion call like `assert` or `assert_equals`. - -When variables are added together, or scaled, they do not directly get constrained. -This is due to optimizations targetting R1CS (which we don't support anymore) that were implemented in the original snarky library, and that we have kept in snarky-rs. - -Imagine the following example: - -```rust -let y = x1 + x2 + x3 +.... ; -let z = y + 3; -assert_eq(y, 6); -assert_eq(z, 7); -``` - -The first two lines will not create constraints, but simply create minimal ASTs that track all of the additions. - -Both assert calls will then reduce the variables to a single circuit variable, creating the same constraints twice. - -For this reason, there's a function `seal()` defined in pickles and snarkyjs. (TODO: more about `seal()`, and why is it not in snarky?) (TODO: remove the R1CS optimization) - -## Snarky vars - -Handling `CVar`s can be cumbersome, as they can only represent a single field element. -We might want to represent values that are either in a smaller range (e.g. [booleans](./booleans.md)) or that are made out of several `CVar`s. - -For this, snarky's API exposes the following trait, which allows users to define their own types: - -```rust -pub trait SnarkyType: Sized -where - F: PrimeField, -{ - /// ? - type Auxiliary; - - /// The equivalent type outside of the circuit. - type OutOfCircuit; - - const SIZE_IN_FIELD_ELEMENTS: usize; - - fn to_cvars(&self) -> (Vec>, Self::Auxiliary); - - fn from_cvars_unsafe(cvars: Vec>, aux: Self::Auxiliary) -> Self; - - fn check(&self, cs: &mut RunState); - - fn deserialize(&self) -> (Self::OutOfCircuit, Self::Auxiliary); - - fn serialize(out_of_circuit: Self::OutOfCircuit, aux: Self::Auxiliary) -> Self; - - fn constraint_system_auxiliary() -> Self::Auxiliary; - - fn value_to_field_elements(x: &Self::OutOfCircuit) -> (Vec, Self::Auxiliary); - - fn value_of_field_elements(x: (Vec, Self::Auxiliary)) -> Self::OutOfCircuit; -} -``` - -Such types are always handled as `OutOfCircuit` types (e.g. `bool`) by the users, and as a type implementing `SnarkyType` by snarky (e.g. [`Boolean`](./booleans.md)). -Thus, the user can pass them to snarky in two ways: - -**As public inputs**. In this case they will be serialized into field elements for snarky before [witness-generation](./witness-generation.md) (via the `value_to_field_elements()` function) - -**As private inputs**. In this case, they must be created using the `compute()` function with a closure returning an `OutOfCircuit` value by the user. -The call to `compute()` will need to have some type hint, for snarky to understand what `SnarkyType` it is creating. -This is because the relationship is currently only one-way: a `SnarkyType` knows what out-of-circuit type it relates to, but not the other way is not true. -(TODO: should we implement that though?) - -A `SnarkyType` always implements a `check()` function, which is called by snarky when `compute()` is called to create such a type. -The `check()` function is responsible for creating the constraints that sanitize the newly-created `SnarkyType` (and its underlying `CVar`s). -For example, creating a boolean would make sure that the underlying `CVar` is either 0 or 1. diff --git a/book/src/snarky/witness-generation.md b/book/src/snarky/witness-generation.md deleted file mode 100644 index 41fbc3b5f1..0000000000 --- a/book/src/snarky/witness-generation.md +++ /dev/null @@ -1,21 +0,0 @@ -# Witness generation - -In snarky, currently, the same code is run through again to generate the witness. - -That is, the `RunState` contains a few changes: - -* **`public_input: Vec`**: now contains concrete values (instead of being empty). -* **`has_witness`**: is set to `WitnessGeneration`. - -Additionaly, if we want to verify that the arguments are actually correct (and that the program implemented does not fail) we can also set `eval_constraints` to `true` (defaults to `false`) to verify that the program has a correct state at all point in time. - -If we do not do this, the user will only detect failure during proof generation (specifically when the [composition polynomial](../specs/kimchi.md#proof-creation) is divided by the [vanishing polynomial](../specs/kimchi.md#proof-creation)). - -```admonish -This is implemented by simply checking that each [generic gate](../specs/kimchi.md#double-generic-gate) encountered is correct, in relation to the witness values observed in that row. -In other words $c_0 l + c_1 r + c_2 o + c_3 l r + c_4 = 0$ (extrapolated to the [double generic gate](../specs/kimchi.md#double-generic-gate)). -Note that other custom gates are not checked, as they are wrapped by [gadgets](../specs/kimchi.md#gates) which fill in witness values instead of the user. -Thus there is no room for user error (i.e. the user entering a wrong private input). -``` - -Due to the `has_witness` variable set to `WitnessGeneration`, functions will behave differently and compute actual values instead of generating constraints. diff --git a/book/src/specs/kimchi.md b/book/src/specs/kimchi.md index 13a51330d9..91852cdbb0 100644 --- a/book/src/specs/kimchi.md +++ b/book/src/specs/kimchi.md @@ -1641,8 +1641,8 @@ If lookup is used, the following values are added to the common index: To create the index, follow these steps: 1. If no lookup is used in the circuit, do not create a lookup index -2. Get the lookup selectors and lookup tables (TODO: how?) -3. Concatenate runtime lookup tables with the ones used by gates +2. Get the lookup selectors and lookup tables that are specified implicitly +3. Concatenate explicit runtime lookup tables with the ones (implicitly) used by gates. 4. Get the highest number of columns `max_table_width` that a lookup table can have. 5. Create the concatenated table of all the fixed lookup tables. @@ -2202,7 +2202,7 @@ The prover then follows the following steps to create the proof: * $s_i$ * $w_i$ * $z$ - * lookup (TODO) + * lookup (TODO, see [this issue](https://github.com/MinaProtocol/mina/issues/13886)) * generic selector * poseidon selector @@ -2284,11 +2284,11 @@ We run the following algorithm: * Derive the scalar joint combiner challenge $j$ from $j'$ using the endomorphism. (TODO: specify endomorphism) * absorb the commitments to the sorted polynomials. -1. Sample $\beta$ with the Fq-Sponge. -1. Sample $\gamma$ with the Fq-Sponge. +1. Sample the first permutation challenge $\beta$ with the Fq-Sponge. +1. Sample the second permutation challenge $\gamma$ with the Fq-Sponge. 1. If using lookup, absorb the commitment to the aggregation lookup polynomial. 1. Absorb the commitment to the permutation trace with the Fq-Sponge. -1. Sample $\alpha'$ with the Fq-Sponge. +1. Sample the quotient challenge $\alpha'$ with the Fq-Sponge. 1. Derive $\alpha$ from $\alpha'$ using the endomorphism (TODO: details). 1. Enforce that the length of the $t$ commitment is of size 7. 1. Absorb the commitment to the quotient polynomial $t$ into the argument. diff --git a/kimchi/Cargo.toml b/kimchi/Cargo.toml index d9415dce18..67fc1e3c00 100644 --- a/kimchi/Cargo.toml +++ b/kimchi/Cargo.toml @@ -25,7 +25,7 @@ num-derive = "0.3" num-integer = "0.1.45" num-traits = "0.2" itertools = "0.10.3" -rand = "0.8.0" +rand = { version = "0.8.0", features = ["std_rng"] } rand_core = "0.6.3" rayon = "1.5.0" rmp-serde = "1.1.1" @@ -50,7 +50,7 @@ mina-poseidon = { path = "../poseidon", version = "0.1.0" } ocaml = { version = "0.22.2", optional = true } ocaml-gen = { version = "0.1.5", optional = true } -wasm-bindgen = { version = "0.2.81", optional = true } +wasm-bindgen = { version = "=0.2.87", optional = true } internal-tracing = { path = "../internal-tracing", version = "0.1.0" } diff --git a/kimchi/src/alphas.rs b/kimchi/src/alphas.rs index 2dbef2aaf3..0eaa047114 100644 --- a/kimchi/src/alphas.rs +++ b/kimchi/src/alphas.rs @@ -323,11 +323,8 @@ mod tests { fn get_alphas_for_spec() { let gates = vec![CircuitGate::::zero(Wire::for_row(0)); 2]; let index = new_index_for_test::(gates, 0); - let (_linearization, powers_of_alpha) = expr_linearization::( - Some(&index.cs.feature_flags), - true, - index.cs.zk_rows as usize, - ); + let (_linearization, powers_of_alpha) = + expr_linearization::(Some(&index.cs.feature_flags), true); // make sure this is present in the specification let manifest_dir = std::env::var("CARGO_MANIFEST_DIR").unwrap(); let spec_path = Path::new(&manifest_dir) diff --git a/kimchi/src/circuits/constraints.rs b/kimchi/src/circuits/constraints.rs index 473b84ce6d..6cef21f258 100644 --- a/kimchi/src/circuits/constraints.rs +++ b/kimchi/src/circuits/constraints.rs @@ -15,7 +15,7 @@ use crate::{ wires::*, }, curve::KimchiCurve, - error::SetupError, + error::{DomainCreationError, SetupError}, prover_index::ProverIndex, }; use ark_ff::{PrimeField, SquareRootField, Zero}; @@ -36,6 +36,11 @@ use std::sync::Arc; // /// Flags for optional features in the constraint system +#[cfg_attr( + feature = "ocaml_types", + derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct) +)] +#[cfg_attr(feature = "wasm_types", wasm_bindgen::prelude::wasm_bindgen)] #[derive(Copy, Clone, Serialize, Deserialize, Debug)] pub struct FeatureFlags { /// RangeCheck0 gate @@ -618,6 +623,47 @@ pub fn zk_rows_strict_lower_bound(num_chunks: usize) -> usize { (2 * (PERMUTS + 1) * num_chunks - 2) / PERMUTS } +impl FeatureFlags { + pub fn from_gates_and_lookup_features( + gates: &[CircuitGate], + lookup_features: LookupFeatures, + ) -> FeatureFlags { + let mut feature_flags = FeatureFlags { + range_check0: false, + range_check1: false, + lookup_features, + foreign_field_add: false, + foreign_field_mul: false, + xor: false, + rot: false, + }; + + for gate in gates { + match gate.typ { + GateType::RangeCheck0 => feature_flags.range_check0 = true, + GateType::RangeCheck1 => feature_flags.range_check1 = true, + GateType::ForeignFieldAdd => feature_flags.foreign_field_add = true, + GateType::ForeignFieldMul => feature_flags.foreign_field_mul = true, + GateType::Xor16 => feature_flags.xor = true, + GateType::Rot64 => feature_flags.rot = true, + _ => (), + } + } + + feature_flags + } + + pub fn from_gates( + gates: &[CircuitGate], + uses_runtime_tables: bool, + ) -> FeatureFlags { + FeatureFlags::from_gates_and_lookup_features( + gates, + LookupFeatures::from_gates(gates, uses_runtime_tables), + ) + } +} + impl Builder { /// Set up the number of public inputs. /// If not invoked, it equals `0` by default. @@ -637,7 +683,9 @@ impl Builder { /// If not invoked, it is `vec![]` by default. /// /// **Warning:** you have to make sure that the IDs of the lookup tables, - /// are unique and not colliding with IDs of built-in lookup tables + /// are unique and not colliding with IDs of built-in lookup tables, otherwise + /// the error will be raised. + /// /// (see [crate::circuits::lookup::tables]). pub fn lookup(mut self, lookup_tables: Vec>) -> Self { self.lookup_tables = lookup_tables; @@ -647,8 +695,9 @@ impl Builder { /// Set up the runtime tables. /// If not invoked, it is `None` by default. /// - /// **Warning:** you have to make sure that the IDs of the runtime lookup tables, - /// are unique and not colliding with IDs of built-in lookup tables + /// **Warning:** you have to make sure that the IDs of the runtime + /// lookup tables, are unique, i.e. not colliding internaly (with other runtime tables), + /// otherwise error will be raised. /// (see [crate::circuits::lookup::tables]). pub fn runtime(mut self, runtime_tables: Option>>) -> Self { self.runtime_tables = runtime_tables; @@ -686,30 +735,35 @@ impl Builder { // for some reason we need more than 1 gate for the circuit to work, see TODO below assert!(gates.len() > 1); - let lookup_features = LookupFeatures::from_gates(&gates, runtime_tables.is_some()); + let feature_flags = FeatureFlags::from_gates(&gates, runtime_tables.is_some()); let lookup_domain_size = { // First we sum over the lookup table size + let mut has_table_with_id_0 = false; let mut lookup_domain_size: usize = lookup_tables .iter() - .map( - |LookupTable { data, id: _ }| { - if data.is_empty() { - 0 - } else { - data[0].len() - } - }, - ) + .map(|LookupTable { id, data }| { + // See below for the reason + if *id == 0_i32 { + has_table_with_id_0 = true + } + if data.is_empty() { + 0 + } else { + data[0].len() + } + }) .sum(); // After that on the runtime tables if let Some(runtime_tables) = runtime_tables.as_ref() { + // FIXME: Check that a runtime table with ID 0 is enforced to + // contain a zero entry row. for runtime_table in runtime_tables.iter() { lookup_domain_size += runtime_table.len(); } } // And we add the built-in tables, depending on the features. - let LookupFeatures { patterns, .. } = &lookup_features; + let LookupFeatures { patterns, .. } = &feature_flags.lookup_features; let mut gate_lookup_tables = GateLookupTables { xor: false, range_check: false, @@ -722,7 +776,14 @@ impl Builder { for gate_table in gate_lookup_tables.into_iter() { lookup_domain_size += gate_table.table_size(); } - lookup_domain_size + + // A dummy zero entry will be added if there is no table with ID + // zero. Therefore we must count this in the size. + if has_table_with_id_0 { + lookup_domain_size + } else { + lookup_domain_size + 1 + } }; //~ 1. Compute the number of zero-knowledge rows (`zk_rows`) that will be required to @@ -749,6 +810,9 @@ impl Builder { //~ ``` //~ let (zk_rows, domain_size_lower_bound) = { + // We add 1 to the lookup domain size because there is one element + // used to close the permutation argument (the polynomial Z is of + // degree n + 1 where n is the order of the subgroup H). let circuit_lower_bound = std::cmp::max(gates.len(), lookup_domain_size + 1); let get_domain_size_lower_bound = |zk_rows: u64| circuit_lower_bound + zk_rows as usize; @@ -763,9 +827,13 @@ impl Builder { while { let domain_size = D::::compute_size_of_domain(domain_size_lower_bound) .ok_or(SetupError::DomainCreation( - "could not compute size of domain", + DomainCreationError::DomainSizeFailed(domain_size_lower_bound), ))?; - let num_chunks = domain_size / max_poly_size; + let num_chunks = if domain_size < max_poly_size { + 1 + } else { + domain_size / max_poly_size + }; zk_rows = (zk_rows_strict_lower_bound(num_chunks) + 1) as u64; domain_size_lower_bound = get_domain_size_lower_bound(zk_rows); domain_size < domain_size_lower_bound @@ -777,7 +845,8 @@ impl Builder { //~ 1. Create a domain for the circuit. That is, //~ compute the smallest subgroup of the field that //~ has order greater or equal to `n + zk_rows` elements. - let domain = EvaluationDomains::::create(domain_size_lower_bound)?; + let domain = EvaluationDomains::::create(domain_size_lower_bound) + .map_err(SetupError::DomainCreation)?; assert!(domain.d1.size > zk_rows); @@ -793,28 +862,6 @@ impl Builder { .collect(); gates.append(&mut padding); - let mut feature_flags = FeatureFlags { - range_check0: false, - range_check1: false, - lookup_features, - foreign_field_add: false, - foreign_field_mul: false, - xor: false, - rot: false, - }; - - for gate in &gates { - match gate.typ { - GateType::RangeCheck0 => feature_flags.range_check0 = true, - GateType::RangeCheck1 => feature_flags.range_check1 = true, - GateType::ForeignFieldAdd => feature_flags.foreign_field_add = true, - GateType::ForeignFieldMul => feature_flags.foreign_field_mul = true, - GateType::Xor16 => feature_flags.xor = true, - GateType::Rot64 => feature_flags.rot = true, - _ => (), - } - } - //~ 1. sample the `PERMUTS` shifts. let shifts = Shifts::new(&domain.d1); @@ -828,7 +875,7 @@ impl Builder { &domain, zk_rows as usize, ) - .map_err(|e| SetupError::ConstraintSystem(e.to_string()))?; + .map_err(SetupError::LookupCreation)?; let sid = shifts.map[0].clone(); diff --git a/kimchi/src/circuits/domains.rs b/kimchi/src/circuits/domains.rs index 7f32dd6e12..89251bea5f 100644 --- a/kimchi/src/circuits/domains.rs +++ b/kimchi/src/circuits/domains.rs @@ -3,7 +3,7 @@ use ark_poly::{EvaluationDomain, Radix2EvaluationDomain as Domain}; use serde::{Deserialize, Serialize}; use serde_with::serde_as; -use crate::error::SetupError; +use crate::error::DomainCreationError; #[serde_as] #[derive(Debug, Clone, Copy, Serialize, Deserialize)] @@ -22,26 +22,29 @@ impl EvaluationDomains { /// Creates 4 evaluation domains `d1` (of size `n`), `d2` (of size `2n`), `d4` (of size `4n`), /// and `d8` (of size `8n`). If generator of `d8` is `g`, the generator /// of `d4` is `g^2`, the generator of `d2` is `g^4`, and the generator of `d1` is `g^8`. - pub fn create(n: usize) -> Result { - let n = Domain::::compute_size_of_domain(n).ok_or(SetupError::DomainCreation( - "could not compute size of domain", - ))?; + pub fn create(n: usize) -> Result { + let n = Domain::::compute_size_of_domain(n) + .ok_or(DomainCreationError::DomainSizeFailed(n))?; - let d1 = Domain::::new(n).ok_or(SetupError::DomainCreation( - "construction of domain d1 did not work as intended", + let d1 = Domain::::new(n).ok_or(DomainCreationError::DomainConstructionFailed( + "d1".to_string(), + n, ))?; // we also create domains of larger sizes // to efficiently operate on polynomials in evaluation form. // (in evaluation form, the domain needs to grow as the degree of a polynomial grows) - let d2 = Domain::::new(2 * n).ok_or(SetupError::DomainCreation( - "construction of domain d2 did not work as intended", + let d2 = Domain::::new(2 * n).ok_or(DomainCreationError::DomainConstructionFailed( + "d2".to_string(), + 2 * n, ))?; - let d4 = Domain::::new(4 * n).ok_or(SetupError::DomainCreation( - "construction of domain d4 did not work as intended", + let d4 = Domain::::new(4 * n).ok_or(DomainCreationError::DomainConstructionFailed( + "d4".to_string(), + 4 * n, ))?; - let d8 = Domain::::new(8 * n).ok_or(SetupError::DomainCreation( - "construction of domain d8 did not work as intended", + let d8 = Domain::::new(8 * n).ok_or(DomainCreationError::DomainConstructionFailed( + "d8".to_string(), + 8 * n, ))?; // ensure the relationship between the three domains in case the library's behavior changes diff --git a/kimchi/src/circuits/expr.rs b/kimchi/src/circuits/expr.rs index a3bd390fcf..f331d96b1b 100644 --- a/kimchi/src/circuits/expr.rs +++ b/kimchi/src/circuits/expr.rs @@ -21,11 +21,11 @@ use o1_utils::{foreign_field::ForeignFieldHelpers, FieldHelpers}; use rayon::prelude::*; use serde::{Deserialize, Serialize}; use std::ops::{Add, AddAssign, Mul, Neg, Sub}; +use std::{cmp::Ordering, fmt, iter::FromIterator}; use std::{ collections::{HashMap, HashSet}, ops::MulAssign, }; -use std::{fmt, iter::FromIterator}; use thiserror::Error; use CurrOrNext::{Curr, Next}; @@ -459,6 +459,12 @@ impl FeatureFlag { } } +#[derive(Copy, Clone, Debug, PartialEq, Eq, Serialize, Deserialize)] +pub struct RowOffset { + pub zk_rows: bool, + pub offset: i32, +} + /// An multi-variate polynomial over the base ring `C` with /// variables /// @@ -479,7 +485,7 @@ pub enum Expr { VanishesOnZeroKnowledgeAndPreviousRows, /// UnnormalizedLagrangeBasis(i) is /// (x^n - 1) / (x - omega^i) - UnnormalizedLagrangeBasis(i32), + UnnormalizedLagrangeBasis(RowOffset), Pow(Box>, u64), Cache(CacheId, Box>), /// If the feature flag is enabled, return the first expression; otherwise, return the second. @@ -649,7 +655,7 @@ pub enum PolishToken { Mul, Sub, VanishesOnZeroKnowledgeAndPreviousRows, - UnnormalizedLagrangeBasis(i32), + UnnormalizedLagrangeBasis(RowOffset), Store, Load(usize), /// Skip the given number of tokens if the feature is enabled. @@ -764,7 +770,12 @@ impl PolishToken { stack.push(eval_vanishes_on_last_n_rows(d, c.zk_rows + 1, pt)) } UnnormalizedLagrangeBasis(i) => { - stack.push(unnormalized_lagrange_basis(&d, *i, &pt)) + let offset = if i.zk_rows { + -(c.zk_rows as i32) + i.offset + } else { + i.offset + }; + stack.push(unnormalized_lagrange_basis(&d, offset, &pt)) } Literal(x) => stack.push(*x), Dup => stack.push(stack[stack.len() - 1]), @@ -1587,7 +1598,14 @@ impl Expr> { VanishesOnZeroKnowledgeAndPreviousRows => { Ok(eval_vanishes_on_last_n_rows(d, c.zk_rows + 1, pt)) } - UnnormalizedLagrangeBasis(i) => Ok(unnormalized_lagrange_basis(&d, *i, &pt)), + UnnormalizedLagrangeBasis(i) => { + let offset = if i.zk_rows { + -(c.zk_rows as i32) + i.offset + } else { + i.offset + }; + Ok(unnormalized_lagrange_basis(&d, offset, &pt)) + } Cell(v) => v.evaluate(evals), Cache(_, e) => e.evaluate_(d, pt, evals, c), IfFeature(feature, e1, e2) => { @@ -1649,7 +1667,14 @@ impl Expr { VanishesOnZeroKnowledgeAndPreviousRows => { Ok(eval_vanishes_on_last_n_rows(d, zk_rows + 1, pt)) } - UnnormalizedLagrangeBasis(i) => Ok(unnormalized_lagrange_basis(&d, *i, &pt)), + UnnormalizedLagrangeBasis(i) => { + let offset = if i.zk_rows { + -(zk_rows as i32) + i.offset + } else { + i.offset + }; + Ok(unnormalized_lagrange_basis(&d, offset, &pt)) + } Cell(v) => v.evaluate(evals), Cache(_, e) => e.evaluate(d, pt, zk_rows, evals), IfFeature(feature, e1, e2) => { @@ -1787,10 +1812,17 @@ impl Expr { evals: env.vanishes_on_zero_knowledge_and_previous_rows, }, Expr::Constant(x) => EvalResult::Constant(*x), - Expr::UnnormalizedLagrangeBasis(i) => EvalResult::Evals { - domain: d, - evals: unnormalized_lagrange_evals(env.l0_1, *i, d, env), - }, + Expr::UnnormalizedLagrangeBasis(i) => { + let offset = if i.zk_rows { + -(env.constants.zk_rows as i32) + i.offset + } else { + i.offset + }; + EvalResult::Evals { + domain: d, + evals: unnormalized_lagrange_evals(env.l0_1, offset, d, env), + } + } Expr::Cell(Variable { col, row }) => { let evals: &'a Evaluations> = { match env.get_column(col) { @@ -2481,7 +2513,9 @@ where Double(x) => format!("double({})", x.ocaml(cache)), Constant(x) => x.ocaml(), Cell(v) => format!("cell({})", v.ocaml()), - UnnormalizedLagrangeBasis(i) => format!("unnormalized_lagrange_basis({})", *i), + UnnormalizedLagrangeBasis(i) => { + format!("unnormalized_lagrange_basis({}, {})", i.zk_rows, i.offset) + } VanishesOnZeroKnowledgeAndPreviousRows => { "vanishes_on_zero_knowledge_and_previous_rows".to_string() } @@ -2532,7 +2566,18 @@ where Double(x) => format!("2 ({})", x.latex(cache)), Constant(x) => x.latex(), Cell(v) => v.latex(), - UnnormalizedLagrangeBasis(i) => format!("unnormalized\\_lagrange\\_basis({})", *i), + UnnormalizedLagrangeBasis(RowOffset { + zk_rows: true, + offset: i, + }) => { + format!("unnormalized\\_lagrange\\_basis(zk\\_rows + {})", *i) + } + UnnormalizedLagrangeBasis(RowOffset { + zk_rows: false, + offset: i, + }) => { + format!("unnormalized\\_lagrange\\_basis({})", *i) + } VanishesOnZeroKnowledgeAndPreviousRows => { "vanishes\\_on\\_zero\\_knowledge\\_and\\_previous\\_row".to_string() } @@ -2557,7 +2602,20 @@ where Double(x) => format!("double({})", x.text(cache)), Constant(x) => x.text(), Cell(v) => v.text(), - UnnormalizedLagrangeBasis(i) => format!("unnormalized_lagrange_basis({})", *i), + UnnormalizedLagrangeBasis(RowOffset { + zk_rows: true, + offset: i, + }) => match i.cmp(&0) { + Ordering::Greater => format!("unnormalized_lagrange_basis(zk_rows + {})", *i), + Ordering::Equal => "unnormalized_lagrange_basis(zk_rows)".to_string(), + Ordering::Less => format!("unnormalized_lagrange_basis(zk_rows - {})", (-*i)), + }, + UnnormalizedLagrangeBasis(RowOffset { + zk_rows: false, + offset: i, + }) => { + format!("unnormalized_lagrange_basis({})", *i) + } VanishesOnZeroKnowledgeAndPreviousRows => { "vanishes_on_zero_knowledge_and_previous_rows".to_string() } diff --git a/kimchi/src/circuits/gate.rs b/kimchi/src/circuits/gate.rs index 212bddbbbf..61be85900d 100644 --- a/kimchi/src/circuits/gate.rs +++ b/kimchi/src/circuits/gate.rs @@ -211,6 +211,7 @@ impl CircuitGate { EndoMul => self.verify_endomul::(row, witness, &index.cs), EndoMulScalar => self.verify_endomul_scalar::(row, witness, &index.cs), // TODO: implement the verification for the lookup gate + // See https://github.com/MinaProtocol/mina/issues/14011 Lookup => Ok(()), CairoClaim | CairoInstruction | CairoFlags | CairoTransition => { self.verify_cairo_gate::(row, witness, &index.cs) @@ -299,6 +300,7 @@ impl CircuitGate { } GateType::Lookup => { // TODO: implement the verification for the lookup gate + // See https://github.com/MinaProtocol/mina/issues/14011 vec![] } GateType::CairoClaim => turshi::Claim::constraint_checks(&env, &mut cache), diff --git a/kimchi/src/circuits/lookup/constraints.rs b/kimchi/src/circuits/lookup/constraints.rs index ec4f47f7ca..3b5c38b4d4 100644 --- a/kimchi/src/circuits/lookup/constraints.rs +++ b/kimchi/src/circuits/lookup/constraints.rs @@ -1,6 +1,6 @@ use crate::{ circuits::{ - expr::{prologue::*, Column, ConstantExpr}, + expr::{prologue::*, Column, ConstantExpr, RowOffset}, gate::{CircuitGate, CurrOrNext}, lookup::lookups::{ JointLookup, JointLookupSpec, JointLookupValue, LocalPosition, LookupInfo, @@ -255,6 +255,8 @@ where .iter() .enumerate() .map(|(i, s)| { + // Snake pattern: even chunks of s are direct + // while the odd ones are reversed let (i1, i2) = if i % 2 == 0 { (row, row + 1) } else { @@ -371,7 +373,6 @@ impl LookupConfiguration { pub fn constraints( configuration: &LookupConfiguration, generate_feature_flags: bool, - zk_rows: usize, ) -> Vec> { // Something important to keep in mind is that the last 2 rows of // all columns will have random values in them to maintain zero-knowledge. @@ -601,14 +602,20 @@ pub fn constraints( let aggreg_equation = E::cell(Column::LookupAggreg, Next) * denominator - E::cell(Column::LookupAggreg, Curr) * numerator; - let final_lookup_row: i32 = -(zk_rows as i32) - 1; + let final_lookup_row = RowOffset { + zk_rows: true, + offset: -1, + }; let mut res = vec![ // the accumulator except for the last zk_rows+1 rows // (contains the zk-rows and the last value of the accumulator) E::VanishesOnZeroKnowledgeAndPreviousRows * aggreg_equation, // the initial value of the accumulator - E::UnnormalizedLagrangeBasis(0) * (E::cell(Column::LookupAggreg, Curr) - E::one()), + E::UnnormalizedLagrangeBasis(RowOffset { + zk_rows: false, + offset: 0, + }) * (E::cell(Column::LookupAggreg, Curr) - E::one()), // Check that the final value of the accumulator is 1 E::UnnormalizedLagrangeBasis(final_lookup_row) * (E::cell(Column::LookupAggreg, Curr) - E::one()), @@ -622,7 +629,10 @@ pub fn constraints( final_lookup_row } else { // Check compatibility of the first elements - 0 + RowOffset { + zk_rows: false, + offset: 0, + } }; let mut expr = E::UnnormalizedLagrangeBasis(first_or_last) * (column(Column::LookupSorted(i)) - column(Column::LookupSorted(i + 1))); diff --git a/kimchi/src/circuits/lookup/index.rs b/kimchi/src/circuits/lookup/index.rs index f0be99289d..e4e70a3a7b 100644 --- a/kimchi/src/circuits/lookup/index.rs +++ b/kimchi/src/circuits/lookup/index.rs @@ -21,7 +21,7 @@ use std::iter; use thiserror::Error; /// Represents an error found when computing the lookup constraint system -#[derive(Debug, Error)] +#[derive(Debug, Error, Clone)] pub enum LookupError { #[error("One of the lookup tables has columns of different lengths")] InconsistentTableLength, @@ -32,6 +32,8 @@ pub enum LookupError { }, #[error("The table with id 0 must have an entry of all zeros")] TableIDZeroMustHaveZeroEntry, + #[error("Cannot create a combined table since ids for sub-tables are colliding. The collision type is: {collision_type}")] + LookupTableIdCollision { collision_type: String }, } /// Lookup selectors @@ -200,7 +202,7 @@ impl LookupConstraintSystem { /// Will give error if inputs validation do not match. pub fn create( gates: &[CircuitGate], - lookup_tables: Vec>, + fixed_lookup_tables: Vec>, runtime_tables: Option>>, domain: &EvaluationDomains, zk_rows: usize, @@ -217,14 +219,42 @@ impl LookupConstraintSystem { // product is 1, we cannot use those rows to store any values. let max_num_entries = d1_size - zk_rows - 1; - //~ 2. Get the lookup selectors and lookup tables (TODO: how?) + //~ 2. Get the lookup selectors and lookup tables that are specified implicitly + // by the lookup gates. let (lookup_selectors, gate_lookup_tables) = lookup_info.selector_polynomials_and_tables(domain, gates); - //~ 3. Concatenate runtime lookup tables with the ones used by gates - let mut lookup_tables: Vec<_> = gate_lookup_tables + // Checks whether an iterator contains any duplicates, and if yes, raises + // a corresponding LookupTableIdCollision error. + fn check_id_duplicates<'a, I: Iterator>( + iter: I, + msg: &str, + ) -> Result<(), LookupError> { + use itertools::Itertools; + match iter.duplicates().collect::>() { + dups if !dups.is_empty() => Err(LookupError::LookupTableIdCollision { + collision_type: format!("{}: {:?}", msg, dups).to_string(), + }), + _ => Ok(()), + } + } + + // If there is a gate using a lookup table, this table must not be added + // explicitly to the constraint system. + let fixed_gate_joint_ids: Vec = fixed_lookup_tables + .iter() + .map(|lt| lt.id) + .chain(gate_lookup_tables.iter().map(|lt| lt.id)) + .collect(); + check_id_duplicates( + fixed_gate_joint_ids.iter(), + "duplicates between fixed given and fixed from-gate tables", + )?; + + //~ 3. Concatenate explicit runtime lookup tables with the ones (implicitly) used by gates. + let mut lookup_tables: Vec<_> = fixed_lookup_tables .into_iter() - .chain(lookup_tables) + .chain(gate_lookup_tables) .collect(); let mut has_table_id_0 = false; @@ -232,6 +262,13 @@ impl LookupConstraintSystem { // if we are using runtime tables let (runtime_table_offset, runtime_selector) = if let Some(runtime_tables) = &runtime_tables { + // Check duplicates in runtime table ids + let runtime_tables_ids: Vec = + runtime_tables.iter().map(|rt| rt.id).collect(); + check_id_duplicates(runtime_tables_ids.iter(), "runtime table duplicates")?; + // Runtime table IDs /may/ collide with lookup + // table IDs, so we intentionally do not perform another potential check. + // save the offset of the end of the table let mut runtime_table_offset = 0; for table in &lookup_tables { @@ -399,6 +436,15 @@ impl LookupConstraintSystem { } //~ 6. Pad the end of the concatened table with the dummy value. + // By padding with 0, we constraint the table with ID 0 to + // have a zero entry. + // This is for the rows which do not have a lookup selector, + // see ../../../../book/src/kimchi/lookup.md. + // The zero entry row is contained in the built-in XOR table. + // An error is raised when creating the CS if a user-defined + // table is defined with ID 0 without a row contain zeroes. + // If no such table is used, we artificially add a dummy + // table with ID 0 and a row containing only zeroes. lookup_table .iter_mut() .for_each(|col| col.extend(repeat_n(F::zero(), max_num_entries - col.len()))); @@ -448,3 +494,105 @@ impl LookupConstraintSystem { } } } + +#[cfg(test)] +mod tests { + + use super::{LookupError, LookupTable, RuntimeTableCfg}; + use crate::{ + circuits::constraints::ConstraintSystem, circuits::gate::CircuitGate, + circuits::lookup::tables::xor, circuits::polynomials::range_check, error::SetupError, + }; + use mina_curves::pasta::Fp; + + #[test] + fn test_colliding_table_ids() { + let (_, gates) = CircuitGate::::create_multi_range_check(0); + let collision_id: i32 = 5; + + let cs = ConstraintSystem::::create(gates.clone()) + .lookup(vec![range_check::gadget::lookup_table()]) + .build(); + + assert!( + matches!( + cs, + Err(SetupError::LookupCreation( + LookupError::LookupTableIdCollision { .. } + )) + ), + "LookupConstraintSystem::create(...) must fail due to range table passed twice" + ); + + let cs = ConstraintSystem::::create(gates.clone()) + .lookup(vec![xor::xor_table()]) + .build(); + + assert!( + cs.is_ok(), + "LookupConstraintSystem::create(...) must succeed, no duplicates exist" + ); + + let cs = ConstraintSystem::::create(gates.clone()) + .lookup(vec![ + LookupTable { + id: collision_id, + data: vec![vec![From::from(0); 16]], + }, + LookupTable { + id: collision_id, + data: vec![vec![From::from(1); 16]], + }, + ]) + .build(); + + assert!( + matches!( + cs, + Err(SetupError::LookupCreation( + LookupError::LookupTableIdCollision { .. } + )) + ), + "LookupConstraintSystem::create(...) must fail, collision in fixed ids" + ); + + let cs = ConstraintSystem::::create(gates.clone()) + .runtime(Some(vec![ + RuntimeTableCfg { + id: collision_id, + first_column: vec![From::from(0); 16], + }, + RuntimeTableCfg { + id: collision_id, + first_column: vec![From::from(1); 16], + }, + ])) + .build(); + + assert!( + matches!( + cs, + Err(SetupError::LookupCreation( + LookupError::LookupTableIdCollision { .. } + )) + ), + "LookupConstraintSystem::create(...) must fail, collision in runtime ids" + ); + + let cs = ConstraintSystem::::create(gates.clone()) + .lookup(vec![LookupTable { + id: collision_id, + data: vec![vec![From::from(0); 16]], + }]) + .runtime(Some(vec![RuntimeTableCfg { + id: collision_id, + first_column: vec![From::from(1); 16], + }])) + .build(); + + assert!( + cs.is_ok(), + "LookupConstraintSystem::create(...) must not fail when there is a collision between runtime and lookup ids" + ); + } +} diff --git a/kimchi/src/circuits/lookup/lookups.rs b/kimchi/src/circuits/lookup/lookups.rs index b126e1be00..002b040828 100644 --- a/kimchi/src/circuits/lookup/lookups.rs +++ b/kimchi/src/circuits/lookup/lookups.rs @@ -323,7 +323,6 @@ pub type JointLookupSpec = JointLookup, LookupTableID>; pub type JointLookupValue = JointLookup; impl + From> JointLookupValue { - // TODO: Support multiple tables /// Evaluate the combined value of a joint-lookup. pub fn evaluate(&self, joint_combiner: &F, table_id_combiner: &F) -> F { combine_table_entry( diff --git a/kimchi/src/circuits/lookup/tables/mod.rs b/kimchi/src/circuits/lookup/tables/mod.rs index 0c049f3e59..cd183cb714 100644 --- a/kimchi/src/circuits/lookup/tables/mod.rs +++ b/kimchi/src/circuits/lookup/tables/mod.rs @@ -78,19 +78,15 @@ impl LookupTable where F: FftField, { - /// Return true if the table has an entry containing all zeros. + /// Return true if the table has an entry (row) containing all zeros. pub fn has_zero_entry(&self) -> bool { // reminder: a table is written as a list of columns, // not as a list of row entries. for row in 0..self.len() { - for col in &self.data { - if !col[row].is_zero() { - continue; - } + if self.data.iter().all(|col| col[row].is_zero()) { return true; } } - false } diff --git a/kimchi/src/error.rs b/kimchi/src/error.rs index 5e4a8817b7..8f2e8406a1 100644 --- a/kimchi/src/error.rs +++ b/kimchi/src/error.rs @@ -1,5 +1,6 @@ //! This module implements the [`ProverError`] type. +use crate::circuits::lookup::index::LookupError; // not sure about hierarchy use poly_commitment::error::CommitmentError; use thiserror::Error; @@ -82,6 +83,16 @@ pub enum VerifyError { MissingCommitment(crate::circuits::expr::Column), } +/// Errors that can arise when preparing the setup +#[derive(Error, Debug, Clone)] +pub enum DomainCreationError { + #[error("could not compute the size of domain for {0}")] + DomainSizeFailed(usize), + + #[error("construction of domain {0} for size {1} failed")] + DomainConstructionFailed(String, usize), +} + /// Errors that can arise when preparing the setup #[derive(Error, Debug, Clone)] pub enum SetupError { @@ -89,7 +100,10 @@ pub enum SetupError { ConstraintSystem(String), #[error("the domain could not be constructed: {0}")] - DomainCreation(&'static str), + DomainCreation(DomainCreationError), + + #[error("the lookup constraint system cannot not be constructed: {0}")] + LookupCreation(LookupError), } /// Errors that can arise when creating a verifier index diff --git a/kimchi/src/linearization.rs b/kimchi/src/linearization.rs index 4f85cb920c..566ef58216 100644 --- a/kimchi/src/linearization.rs +++ b/kimchi/src/linearization.rs @@ -38,7 +38,6 @@ use ark_ff::{FftField, PrimeField, SquareRootField, Zero}; pub fn constraints_expr( feature_flags: Option<&FeatureFlags>, generic: bool, - zk_rows: usize, ) -> (Expr>, Alphas) { // register powers of alpha so that we don't reuse them across mutually inclusive constraints let mut powers_of_alpha = Alphas::::default(); @@ -166,8 +165,7 @@ pub fn constraints_expr( if feature_flags.lookup_features.patterns != LookupPatterns::default() { let lookup_configuration = LookupConfiguration::new(LookupInfo::create(feature_flags.lookup_features)); - let constraints = - lookup::constraints::constraints(&lookup_configuration, false, zk_rows); + let constraints = lookup::constraints::constraints(&lookup_configuration, false); // note: the number of constraints depends on the lookup configuration, // specifically the presence of runtime tables. @@ -193,7 +191,7 @@ pub fn constraints_expr( joint_lookup_used: true, }; let lookup_configuration = LookupConfiguration::new(LookupInfo::create(all_features)); - let constraints = lookup::constraints::constraints(&lookup_configuration, true, zk_rows); + let constraints = lookup::constraints::constraints(&lookup_configuration, true); // note: the number of constraints depends on the lookup configuration, // specifically the presence of runtime tables. @@ -224,7 +222,7 @@ pub fn constraints_expr( // flags. if cfg!(feature = "check_feature_flags") { if let Some(feature_flags) = feature_flags { - let (feature_flagged_expr, _) = constraints_expr(None, generic, zk_rows); + let (feature_flagged_expr, _) = constraints_expr(None, generic); let feature_flagged_expr = feature_flagged_expr.apply_feature_flags(feature_flags); assert_eq!(expr, feature_flagged_expr); } @@ -341,11 +339,10 @@ pub fn linearization_columns( pub fn expr_linearization( feature_flags: Option<&FeatureFlags>, generic: bool, - zk_rows: usize, ) -> (Linearization>>, Alphas) { let evaluated_cols = linearization_columns::(feature_flags); - let (expr, powers_of_alpha) = constraints_expr(feature_flags, generic, zk_rows); + let (expr, powers_of_alpha) = constraints_expr(feature_flags, generic); let linearization = expr .linearize(evaluated_cols) diff --git a/kimchi/src/prover.rs b/kimchi/src/prover.rs index 14fe30d365..55a99561c3 100644 --- a/kimchi/src/prover.rs +++ b/kimchi/src/prover.rs @@ -260,7 +260,7 @@ where .interpolate(); //~ 1. Commit (non-hiding) to the negated public input polynomial. - let public_comm = index.srs.commit_non_hiding(&public_poly, num_chunks, None); + let public_comm = index.srs.commit_non_hiding(&public_poly, num_chunks); let public_comm = { index .srs @@ -393,7 +393,7 @@ where let runtime_table_comm = index .srs - .commit(&runtime_table_contribution, num_chunks, None, rng); + .commit(&runtime_table_contribution, num_chunks, rng); // absorb the commitment absorb_commitment(&mut fq_sponge, &runtime_table_comm.commitment); @@ -607,7 +607,7 @@ where let z_poly = index.perm_aggreg(&witness, &beta, &gamma, rng)?; //~ 1. Commit (hidding) to the permutation aggregation polynomial $z$. - let z_comm = index.srs.commit(&z_poly, num_chunks, None, rng); + let z_comm = index.srs.commit(&z_poly, num_chunks, rng); //~ 1. Absorb the permutation aggregation polynomial $z$ with the Fq-Sponge. absorb_commitment(&mut fq_sponge, &z_comm.commitment); @@ -818,11 +818,7 @@ where // lookup { if let Some(lcs) = index.cs.lookup_constraint_system.as_ref() { - let constraints = lookup::constraints::constraints( - &lcs.configuration, - false, - index.cs.zk_rows as usize, - ); + let constraints = lookup::constraints::constraints(&lcs.configuration, false); let constraints_len = u32::try_from(constraints.len()) .expect("not expecting a large amount of constraints"); let lookup_alphas = @@ -870,7 +866,7 @@ where }; //~ 1. commit (hiding) to the quotient polynomial $t$ - let t_comm = { index.srs.commit("ient_poly, 7 * num_chunks, None, rng) }; + let t_comm = { index.srs.commit("ient_poly, 7 * num_chunks, rng) }; //~ 1. Absorb the the commitment of the quotient polynomial with the Fq-Sponge. absorb_commitment(&mut fq_sponge, &t_comm.commitment); @@ -940,7 +936,7 @@ where //~~ * $s_i$ //~~ * $w_i$ //~~ * $z$ - //~~ * lookup (TODO) + //~~ * lookup (TODO, see [this issue](https://github.com/MinaProtocol/mina/issues/13886)) //~~ * generic selector //~~ * poseidon selector //~ @@ -1155,10 +1151,9 @@ where PolyComm { // blinding_f - Z_H(zeta) * blinding_t - unshifted: vec![ + elems: vec![ blinding_f - (zeta_to_domain_size - G::ScalarField::one()) * blinding_t, ], - shifted: None, } }; @@ -1192,7 +1187,7 @@ where .map(|RecursionChallenge { chals, comm }| { ( DensePolynomial::from_coefficients_vec(b_poly_coefficients(chals)), - comm.unshifted.len(), + comm.elems.len(), ) }) .collect::>(); @@ -1227,8 +1222,7 @@ where //~ (and evaluation proofs) in the protocol. //~ First, include the previous challenges, in case we are in a recursive prover. let non_hiding = |d1_size: usize| PolyComm { - unshifted: vec![G::ScalarField::zero(); d1_size], - shifted: None, + elems: vec![G::ScalarField::zero(); d1_size], }; let coefficients_form = DensePolynomialOrEvaluations::DensePolynomial; @@ -1236,12 +1230,11 @@ where let mut polynomials = polys .iter() - .map(|(p, d1_size)| (coefficients_form(p), None, non_hiding(*d1_size))) + .map(|(p, d1_size)| (coefficients_form(p), non_hiding(*d1_size))) .collect::>(); let fixed_hiding = |d1_size: usize| PolyComm { - unshifted: vec![G::ScalarField::one(); d1_size], - shifted: None, + elems: vec![G::ScalarField::one(); d1_size], }; //~ 1. Then, include: @@ -1252,48 +1245,38 @@ where //~~ * the poseidon selector //~~ * the 15 registers/witness columns //~~ * the 6 sigmas - polynomials.push(( - coefficients_form(&public_poly), - None, - fixed_hiding(num_chunks), - )); - polynomials.push((coefficients_form(&ft), None, blinding_ft)); - polynomials.push((coefficients_form(&z_poly), None, z_comm.blinders)); + polynomials.push((coefficients_form(&public_poly), fixed_hiding(num_chunks))); + polynomials.push((coefficients_form(&ft), blinding_ft)); + polynomials.push((coefficients_form(&z_poly), z_comm.blinders)); polynomials.push(( evaluations_form(&index.column_evaluations.generic_selector4), - None, fixed_hiding(num_chunks), )); polynomials.push(( evaluations_form(&index.column_evaluations.poseidon_selector8), - None, fixed_hiding(num_chunks), )); polynomials.push(( evaluations_form(&index.column_evaluations.complete_add_selector4), - None, fixed_hiding(num_chunks), )); polynomials.push(( evaluations_form(&index.column_evaluations.mul_selector8), - None, fixed_hiding(num_chunks), )); polynomials.push(( evaluations_form(&index.column_evaluations.emul_selector8), - None, fixed_hiding(num_chunks), )); polynomials.push(( evaluations_form(&index.column_evaluations.endomul_scalar_selector8), - None, fixed_hiding(num_chunks), )); polynomials.extend( witness_poly .iter() .zip(w_comm.iter()) - .map(|(w, c)| (coefficients_form(w), None, c.blinders.clone())) + .map(|(w, c)| (coefficients_form(w), c.blinders.clone())) .collect::>(), ); polynomials.extend( @@ -1301,13 +1284,13 @@ where .column_evaluations .coefficients8 .iter() - .map(|coefficientm| (evaluations_form(coefficientm), None, non_hiding(num_chunks))) + .map(|coefficientm| (evaluations_form(coefficientm), non_hiding(num_chunks))) .collect::>(), ); polynomials.extend( index.column_evaluations.permutation_coefficients8[0..PERMUTS - 1] .iter() - .map(|w| (evaluations_form(w), None, non_hiding(num_chunks))) + .map(|w| (evaluations_form(w), non_hiding(num_chunks))) .collect::>(), ); @@ -1317,7 +1300,6 @@ where { polynomials.push(( evaluations_form(range_check0_selector8), - None, non_hiding(num_chunks), )); } @@ -1326,7 +1308,6 @@ where { polynomials.push(( evaluations_form(range_check1_selector8), - None, non_hiding(num_chunks), )); } @@ -1337,7 +1318,6 @@ where { polynomials.push(( evaluations_form(foreign_field_add_selector8), - None, non_hiding(num_chunks), )); } @@ -1348,23 +1328,14 @@ where { polynomials.push(( evaluations_form(foreign_field_mul_selector8), - None, non_hiding(num_chunks), )); } if let Some(xor_selector8) = index.column_evaluations.xor_selector8.as_ref() { - polynomials.push(( - evaluations_form(xor_selector8), - None, - non_hiding(num_chunks), - )); + polynomials.push((evaluations_form(xor_selector8), non_hiding(num_chunks))); } if let Some(rot_selector8) = index.column_evaluations.rot_selector8.as_ref() { - polynomials.push(( - evaluations_form(rot_selector8), - None, - non_hiding(num_chunks), - )); + polynomials.push((evaluations_form(rot_selector8), non_hiding(num_chunks))); } //~~ * optionally, the runtime table @@ -1375,17 +1346,13 @@ where let sorted_comms = lookup_context.sorted_comms.as_ref().unwrap(); for (poly, comm) in sorted_poly.iter().zip(sorted_comms) { - polynomials.push((coefficients_form(poly), None, comm.blinders.clone())); + polynomials.push((coefficients_form(poly), comm.blinders.clone())); } //~~ * add the lookup aggreg polynomial let aggreg_poly = lookup_context.aggreg_coeffs.as_ref().unwrap(); let aggreg_comm = lookup_context.aggreg_comm.as_ref().unwrap(); - polynomials.push(( - coefficients_form(aggreg_poly), - None, - aggreg_comm.blinders.clone(), - )); + polynomials.push((coefficients_form(aggreg_poly), aggreg_comm.blinders.clone())); //~~ * add the combined table polynomial let table_blinding = { @@ -1414,28 +1381,23 @@ where if lcs.runtime_selector.is_some() { let runtime_comm = lookup_context.runtime_table_comm.as_ref().unwrap(); - let unshifted = runtime_comm + let elems = runtime_comm .blinders - .unshifted + .elems .iter() .map(|blinding| *joint_combiner * blinding + base_blinding) .collect(); - PolyComm { - unshifted, - shifted: None, - } + PolyComm { elems } } else { - PolyComm { - unshifted: vec![base_blinding; num_chunks], - shifted: None, - } + let elems = vec![base_blinding; num_chunks]; + PolyComm { elems } } }; let joint_lookup_table = lookup_context.joint_lookup_table.as_ref().unwrap(); - polynomials.push((coefficients_form(joint_lookup_table), None, table_blinding)); + polynomials.push((coefficients_form(joint_lookup_table), table_blinding)); //~~ * if present, add the runtime table polynomial if lcs.runtime_selector.is_some() { @@ -1444,7 +1406,6 @@ where polynomials.push(( coefficients_form(runtime_table), - None, runtime_table_comm.blinders.clone(), )); } @@ -1454,27 +1415,21 @@ where if let Some(runtime_lookup_table_selector) = lcs.runtime_selector.as_ref() { polynomials.push(( evaluations_form(runtime_lookup_table_selector), - None, non_hiding(1), )) } if let Some(xor_lookup_selector) = lcs.lookup_selectors.xor.as_ref() { - polynomials.push((evaluations_form(xor_lookup_selector), None, non_hiding(1))) + polynomials.push((evaluations_form(xor_lookup_selector), non_hiding(1))) } if let Some(lookup_gate_selector) = lcs.lookup_selectors.lookup.as_ref() { - polynomials.push((evaluations_form(lookup_gate_selector), None, non_hiding(1))) + polynomials.push((evaluations_form(lookup_gate_selector), non_hiding(1))) } if let Some(range_check_lookup_selector) = lcs.lookup_selectors.range_check.as_ref() { - polynomials.push(( - evaluations_form(range_check_lookup_selector), - None, - non_hiding(1), - )) + polynomials.push((evaluations_form(range_check_lookup_selector), non_hiding(1))) } if let Some(foreign_field_mul_lookup_selector) = lcs.lookup_selectors.ffmul.as_ref() { polynomials.push(( evaluations_form(foreign_field_mul_lookup_selector), - None, non_hiding(1), )) } diff --git a/kimchi/src/prover_index.rs b/kimchi/src/prover_index.rs index 44ee0f6266..523d583e18 100644 --- a/kimchi/src/prover_index.rs +++ b/kimchi/src/prover_index.rs @@ -69,8 +69,7 @@ where cs.endo = endo_q; // pre-compute the linearization - let (linearization, powers_of_alpha) = - expr_linearization(Some(&cs.feature_flags), true, cs.zk_rows as usize); + let (linearization, powers_of_alpha) = expr_linearization(Some(&cs.feature_flags), true); let evaluated_column_coefficients = cs.evaluated_column_coefficients(); diff --git a/kimchi/src/tests/foreign_field_add.rs b/kimchi/src/tests/foreign_field_add.rs index 24c1d5a8c1..760c7fa2d5 100644 --- a/kimchi/src/tests/foreign_field_add.rs +++ b/kimchi/src/tests/foreign_field_add.rs @@ -1490,7 +1490,6 @@ fn test_ffadd_finalization() { let index = { let cs = ConstraintSystem::create(gates.clone()) - .lookup(vec![range_check::gadget::lookup_table()]) .public(num_public_inputs) .build() .unwrap(); diff --git a/kimchi/src/tests/lookup.rs b/kimchi/src/tests/lookup.rs index a674eba78f..d92f62e24b 100644 --- a/kimchi/src/tests/lookup.rs +++ b/kimchi/src/tests/lookup.rs @@ -14,6 +14,7 @@ use mina_poseidon::{ constants::PlonkSpongeConstantsKimchi, sponge::{DefaultFqSponge, DefaultFrSponge}, }; +use rand::prelude::*; use rand::Rng; use std::array; @@ -22,10 +23,12 @@ type BaseSponge = DefaultFqSponge; type ScalarSponge = DefaultFrSponge; fn setup_lookup_proof(use_values_from_table: bool, num_lookups: usize, table_sizes: Vec) { - let lookup_table_values: Vec> = table_sizes + let mut lookup_table_values: Vec> = table_sizes .iter() .map(|size| (0..*size).map(|_| rand::random()).collect()) .collect(); + // Zero table must have a zero row + lookup_table_values[0][0] = From::from(0); let lookup_tables = lookup_table_values .iter() .enumerate() @@ -131,7 +134,9 @@ fn setup_successfull_runtime_table_test( runtime_tables: Vec>, lookups: Vec, ) { - let mut rng = rand::thread_rng(); + let seed: [u8; 32] = thread_rng().gen(); + eprintln!("Seed: {:?}", seed); + let mut rng = StdRng::from_seed(seed); let nb_lookups = lookups.len(); // circuit @@ -194,13 +199,15 @@ fn setup_successfull_runtime_table_test( #[test] fn test_runtime_table() { let num = 5; - let mut rng = rand::thread_rng(); + let seed: [u8; 32] = thread_rng().gen(); + eprintln!("Seed: {:?}", seed); + let mut rng = StdRng::from_seed(seed); let first_column = [8u32, 9, 8, 7, 1]; let len = first_column.len(); let mut runtime_tables_setup = vec![]; - for table_id in 0..num { + for table_id in 1..num + 1 { let cfg = RuntimeTableCfg { id: table_id, first_column: first_column.into_iter().map(Into::into).collect(), @@ -236,7 +243,7 @@ fn test_runtime_table() { for row in 0..20 { // the first register is the table id. We pick one random table. - lookup_cols[0][row] = (rng.gen_range(0..num) as u32).into(); + lookup_cols[0][row] = (rng.gen_range(1..num + 1) as u32).into(); // create queries into our runtime lookup table. // We will set [w1, w2], [w3, w4] and [w5, w6] to randon indexes and @@ -448,7 +455,9 @@ fn test_negative_test_runtime_table_prover_uses_undefined_id_in_index_and_witnes #[test] fn test_runtime_table_with_more_than_one_runtime_table_data_given_by_prover() { - let mut rng = rand::thread_rng(); + let seed: [u8; 32] = thread_rng().gen(); + eprintln!("Seed: {:?}", seed); + let mut rng = StdRng::from_seed(seed); let first_column = [0, 1, 2, 3, 4]; let len = first_column.len(); @@ -551,7 +560,9 @@ fn test_runtime_table_only_one_table_with_id_zero_with_non_zero_entries_fixed_va #[test] fn test_runtime_table_only_one_table_with_id_zero_with_non_zero_entries_random_values() { - let mut rng = rand::thread_rng(); + let seed: [u8; 32] = thread_rng().gen(); + eprintln!("Seed: {:?}", seed); + let mut rng = StdRng::from_seed(seed); let len = rng.gen_range(1usize..1000); let first_column: Vec = (0..len as i32).collect(); @@ -573,3 +584,147 @@ fn test_runtime_table_only_one_table_with_id_zero_with_non_zero_entries_random_v setup_successfull_runtime_table_test(vec![cfg], vec![runtime_table], lookups); } + +// This test verifies that if there is a table with ID 0, it contains a row with only zeroes. +// This is to enforce the constraint we have on the so-called "dummy value". +// FIXME: see https://github.com/o1-labs/proof-systems/issues/1460 +// We should test the error message, "expected" argument of the macro won't be +// allowed anymore in future release, see clippy output. +#[test] +#[should_panic] +fn test_lookup_with_a_table_with_id_zero_but_no_zero_entry() { + let max_len: u32 = 100u32; + let seed: [u8; 32] = thread_rng().gen(); + eprintln!("Seed: {:?}", seed); + let mut rng = StdRng::from_seed(seed); + + // Non zero-length table + let len = 1u32 + rng.gen_range(0u32..max_len); + // Table id is 0 + let table_id: i32 = 0; + // Always include index 0 in the table. Maybe even a few. + let indices: Vec = (0..len) + .map(|i| { + if i == 0 { + 0u32 + } else { + rng.gen_range(0u32..max_len) + } + }) + .map(Into::into) + .collect(); + // But no zero values! + // So we'll get rows with zeroes that are not full-zero-rows. + let values: Vec = (0..len) + .map(|_| rng.gen_range(1u32..max_len)) + .map(Into::into) + .collect(); + let lookup_table = LookupTable { + id: table_id, + data: vec![indices, values], + }; + let lookup_tables = vec![lookup_table]; + let num_lookups = 20; + + // circuit gates + let gates = (0..num_lookups) + .map(|i| CircuitGate::new(GateType::Lookup, Wire::for_row(i), vec![])) + .collect(); + + // 0 everywhere, it should handle the case (0, 0, 0). We simulate a lot of + // lookups with (0, 0, 0). + let witness = array::from_fn(|_col| vec![Fp::zero(); num_lookups]); + + let _ = TestFramework::::default() + .gates(gates) + .witness(witness) + .lookup_tables(lookup_tables) + .setup(); +} + +#[test] +fn test_dummy_value_is_added_in_an_arbitraly_created_table_when_no_table_with_id_0() { + let seed: [u8; 32] = thread_rng().gen(); + eprintln!("Seed: {:?}", seed); + let mut rng = StdRng::from_seed(seed); + let max_len: u32 = 100u32; + let max_table_id: i32 = 100; + + // No zero-length table + let len = rng.gen_range(1u32..max_len); + // No table of ID 0 + let table_id: i32 = rng.gen_range(1i32..max_table_id); + // No index 0 in the table. + let indices: Vec = (0..len) + .map(|_| rng.gen_range(1u32..max_len)) + .map(Into::into) + .collect(); + // No zero value + let values: Vec = (0..len) + .map(|_| rng.gen_range(1u32..max_len)) + .map(Into::into) + .collect(); + let lookup_table = LookupTable { + id: table_id, + data: vec![indices, values], + }; + let lookup_tables = vec![lookup_table]; + let num_lookups = 20; + + // circuit gates + let gates = (0..num_lookups) + .map(|i| CircuitGate::new(GateType::Lookup, Wire::for_row(i), vec![])) + .collect(); + + // 0 everywhere, it should handle the case (0, 0, 0). We simulate a lot of + // lookups with (0, 0, 0). + let witness = array::from_fn(|_col| vec![Fp::zero(); num_lookups]); + + TestFramework::::default() + .gates(gates) + .witness(witness) + .lookup_tables(lookup_tables) + .setup() + .prove_and_verify::() + .unwrap(); +} + +#[test] +fn test_dummy_zero_entry_is_counted_while_computing_domain_size() { + let seed: [u8; 32] = thread_rng().gen(); + eprintln!("Seed: {:?}", seed); + let mut rng = StdRng::from_seed(seed); + + let power_of_2: u32 = rng.gen_range(3..16); + // 4 = zk_rows + 1 for the closing constraint on the polynomial. + let len = (1 << power_of_2) - 3 - 1; + // We want to create a table with an ID different than 0. + let table_id: i32 = rng.gen_range(1..1_000); + let idx: Vec = (1..(len + 1) as i32).map(Into::into).collect(); + let values: Vec = (1..(len + 1)) + .map(|_| UniformRand::rand(&mut rng)) + .collect(); + let lt = LookupTable { + id: table_id, + data: vec![idx, values], + }; + + // Dummy, used for the setup. Only the number of gates must be lower than + // the length of the table to avoid having a bigger circuit than the table + // size, and therefore use it as the main component for the domain size + // computation. + let num_lookups = rng.gen_range(2..len); + let gates = (0..num_lookups) + .map(|i| CircuitGate::new(GateType::Lookup, Wire::for_row(i), vec![])) + .collect(); + let witness = array::from_fn(|_col| vec![Fp::zero(); num_lookups]); + + let setup = TestFramework::::default() + .gates(gates) + .witness(witness) + .lookup_tables(vec![lt]) + .setup(); + let domain_size = setup.prover_index().cs.domain.d1.size; + // As the dummy entry has been added, we reached the next power of two + assert!(domain_size == (1 << (power_of_2 + 1))); +} diff --git a/kimchi/src/tests/range_check.rs b/kimchi/src/tests/range_check.rs index 27240db942..8e46962add 100644 --- a/kimchi/src/tests/range_check.rs +++ b/kimchi/src/tests/range_check.rs @@ -64,15 +64,7 @@ fn create_test_prover_index( CircuitGate::::create_multi_range_check(0) }; - new_index_for_test_with_lookups( - gates, - public_size, - 0, - vec![range_check::gadget::lookup_table()], - None, - false, - None, - ) + new_index_for_test_with_lookups(gates, public_size, 0, vec![], None, false, None) } #[test] diff --git a/kimchi/src/tests/recursion.rs b/kimchi/src/tests/recursion.rs index d7f028acb5..719318eb96 100644 --- a/kimchi/src/tests/recursion.rs +++ b/kimchi/src/tests/recursion.rs @@ -43,7 +43,7 @@ fn test_recursion() { let comm = { let coeffs = b_poly_coefficients(&chals); let b = DensePolynomial::from_coefficients_vec(coeffs); - index.srs.commit_non_hiding(&b, 1, None) + index.srs.commit_non_hiding(&b, 1) }; RecursionChallenge::new(chals, comm) }; diff --git a/kimchi/src/tests/rot.rs b/kimchi/src/tests/rot.rs index f88125cf9b..f9a1308b86 100644 --- a/kimchi/src/tests/rot.rs +++ b/kimchi/src/tests/rot.rs @@ -328,7 +328,6 @@ fn test_rot_finalization() { let index = { let cs = ConstraintSystem::create(gates.clone()) .public(num_public_inputs) - .lookup(vec![rot::lookup_table()]) .build() .unwrap(); let mut srs = SRS::::create(cs.domain.d1.size()); diff --git a/kimchi/src/tests/xor.rs b/kimchi/src/tests/xor.rs index 0344e0aea3..7ab28b4008 100644 --- a/kimchi/src/tests/xor.rs +++ b/kimchi/src/tests/xor.rs @@ -392,7 +392,6 @@ fn test_xor_finalization() { let index = { let cs = ConstraintSystem::create(gates.clone()) - .lookup(vec![xor::lookup_table()]) .public(num_inputs) .build() .unwrap(); diff --git a/kimchi/src/verifier.rs b/kimchi/src/verifier.rs index 0c9cd4aef3..62d9e5d43f 100644 --- a/kimchi/src/verifier.rs +++ b/kimchi/src/verifier.rs @@ -205,38 +205,47 @@ where } } - //~ 1. Sample $\beta$ with the Fq-Sponge. + // --- PlonK - Round 2 + //~ 1. Sample the first permutation challenge $\beta$ with the Fq-Sponge. let beta = fq_sponge.challenge(); - //~ 1. Sample $\gamma$ with the Fq-Sponge. + //~ 1. Sample the second permutation challenge $\gamma$ with the Fq-Sponge. let gamma = fq_sponge.challenge(); //~ 1. If using lookup, absorb the commitment to the aggregation lookup polynomial. - self.commitments.lookup.iter().for_each(|l| { - absorb_commitment(&mut fq_sponge, &l.aggreg); - }); + if index.lookup_index.is_some() { + // Should not fail, as the lookup index is present + let lookup_commits = self + .commitments + .lookup + .as_ref() + .ok_or(VerifyError::LookupCommitmentMissing)?; + absorb_commitment(&mut fq_sponge, &lookup_commits.aggreg); + } //~ 1. Absorb the commitment to the permutation trace with the Fq-Sponge. absorb_commitment(&mut fq_sponge, &self.commitments.z_comm); - //~ 1. Sample $\alpha'$ with the Fq-Sponge. + // --- PlonK - Round 3 + //~ 1. Sample the quotient challenge $\alpha'$ with the Fq-Sponge. let alpha_chal = ScalarChallenge(fq_sponge.challenge()); //~ 1. Derive $\alpha$ from $\alpha'$ using the endomorphism (TODO: details). let alpha = alpha_chal.to_field(endo_r); //~ 1. Enforce that the length of the $t$ commitment is of size 7. - if self.commitments.t_comm.unshifted.len() > chunk_size * 7 { + if self.commitments.t_comm.elems.len() > chunk_size * 7 { return Err(VerifyError::IncorrectCommitmentLength( "t", chunk_size * 7, - self.commitments.t_comm.unshifted.len(), + self.commitments.t_comm.elems.len(), )); } //~ 1. Absorb the commitment to the quotient polynomial $t$ into the argument. absorb_commitment(&mut fq_sponge, &self.commitments.t_comm); + // --- PlonK - Round 4 //~ 1. Sample $\zeta'$ with the Fq-Sponge. let zeta_chal = ScalarChallenge(fq_sponge.challenge()); @@ -453,10 +462,10 @@ where let ft_eval1 = vec![self.ft_eval1]; #[allow(clippy::type_complexity)] - let mut es: Vec<(Vec>, Option)> = - polys.iter().map(|(_, e)| (e.clone(), None)).collect(); - es.push((public_evals.to_vec(), None)); - es.push((vec![ft_eval0, ft_eval1], None)); + let mut es: Vec>> = + polys.iter().map(|(_, e)| e.clone()).collect(); + es.push(public_evals.to_vec()); + es.push(vec![ft_eval0, ft_eval1]); for col in [ Column::Z, Column::Index(GateType::Generic), @@ -551,19 +560,16 @@ where .into_iter() .flatten(), ) { - es.push(( - { - let evals = self - .evals - .get_column(col) - .ok_or(VerifyError::MissingEvaluation(col))?; - vec![evals.zeta.clone(), evals.zeta_omega.clone()] - }, - None, - )) + es.push({ + let evals = self + .evals + .get_column(col) + .ok_or(VerifyError::MissingEvaluation(col))?; + vec![evals.zeta.clone(), evals.zeta_omega.clone()] + }) } - combined_inner_product(&evaluation_points, &v, &u, &es, index.srs().max_poly_size()) + combined_inner_product(&v, &u, &es) }; let oracles = RandomOracles { @@ -795,10 +801,7 @@ where .expect("pre-computed committed lagrange bases not found"); let com: Vec<_> = lgr_comm.iter().take(verifier_index.public).collect(); if public_input.is_empty() { - PolyComm::new( - vec![verifier_index.srs().blinding_commitment(); chunk_size], - None, - ) + PolyComm::new(vec![verifier_index.srs().blinding_commitment(); chunk_size]) } else { let elm: Vec<_> = public_input.iter().map(|s| -*s).collect(); let public_comm = PolyComm::::multi_scalar_mul(&com, &elm); @@ -917,21 +920,18 @@ where evaluations.extend(polys.into_iter().map(|(c, e)| Evaluation { commitment: c, evaluations: e, - degree_bound: None, })); //~~ * public input commitment evaluations.push(Evaluation { commitment: public_comm, evaluations: public_evals.to_vec(), - degree_bound: None, }); //~~ * ft commitment (chunks of it) evaluations.push(Evaluation { commitment: ft_comm, evaluations: vec![vec![ft_eval0], vec![proof.ft_eval1]], - degree_bound: None, }); for col in [ @@ -1015,7 +1015,6 @@ where .ok_or(VerifyError::MissingCommitment(col))? .clone(), evaluations: vec![evals.zeta.clone(), evals.zeta_omega.clone()], - degree_bound: None, }); } @@ -1038,6 +1037,9 @@ where let joint_combiner = oracles .joint_combiner .expect("joint_combiner should be present if lookups are used"); + // The table ID is added as the last column of the vector. + // Therefore, the exponent for the combiner for the table ID is the + // width of the concatenated table, i.e. max_joint_size. let table_id_combiner = joint_combiner .1 .pow([u64::from(li.lookup_info.max_joint_size)]); @@ -1057,7 +1059,6 @@ where evaluations.push(Evaluation { commitment: table_comm, evaluations: vec![lookup_table.zeta.clone(), lookup_table.zeta_omega.clone()], - degree_bound: None, }); // add evaluation of the runtime table polynomial @@ -1074,7 +1075,6 @@ where evaluations.push(Evaluation { commitment: runtime.clone(), evaluations: vec![runtime_eval.zeta, runtime_eval.zeta_omega], - degree_bound: None, }); } } @@ -1125,7 +1125,6 @@ where .ok_or(VerifyError::MissingCommitment(col))? .clone(), evaluations: vec![evals.zeta.clone(), evals.zeta_omega.clone()], - degree_bound: None, }); } diff --git a/kimchi/src/verifier_index.rs b/kimchi/src/verifier_index.rs index 1b0511d800..67ecaeace0 100644 --- a/kimchi/src/verifier_index.rs +++ b/kimchi/src/verifier_index.rs @@ -439,42 +439,42 @@ impl> VerifierIndex // Always present for comm in sigma_comm.iter() { - fq_sponge.absorb_g(&comm.unshifted); + fq_sponge.absorb_g(&comm.elems); } for comm in coefficients_comm.iter() { - fq_sponge.absorb_g(&comm.unshifted); + fq_sponge.absorb_g(&comm.elems); } - fq_sponge.absorb_g(&generic_comm.unshifted); - fq_sponge.absorb_g(&psm_comm.unshifted); - fq_sponge.absorb_g(&complete_add_comm.unshifted); - fq_sponge.absorb_g(&mul_comm.unshifted); - fq_sponge.absorb_g(&emul_comm.unshifted); - fq_sponge.absorb_g(&endomul_scalar_comm.unshifted); + fq_sponge.absorb_g(&generic_comm.elems); + fq_sponge.absorb_g(&psm_comm.elems); + fq_sponge.absorb_g(&complete_add_comm.elems); + fq_sponge.absorb_g(&mul_comm.elems); + fq_sponge.absorb_g(&emul_comm.elems); + fq_sponge.absorb_g(&endomul_scalar_comm.elems); // Optional gates if let Some(range_check0_comm) = range_check0_comm { - fq_sponge.absorb_g(&range_check0_comm.unshifted); + fq_sponge.absorb_g(&range_check0_comm.elems); } if let Some(range_check1_comm) = range_check1_comm { - fq_sponge.absorb_g(&range_check1_comm.unshifted); + fq_sponge.absorb_g(&range_check1_comm.elems); } if let Some(foreign_field_mul_comm) = foreign_field_mul_comm { - fq_sponge.absorb_g(&foreign_field_mul_comm.unshifted); + fq_sponge.absorb_g(&foreign_field_mul_comm.elems); } if let Some(foreign_field_add_comm) = foreign_field_add_comm { - fq_sponge.absorb_g(&foreign_field_add_comm.unshifted); + fq_sponge.absorb_g(&foreign_field_add_comm.elems); } if let Some(xor_comm) = xor_comm { - fq_sponge.absorb_g(&xor_comm.unshifted); + fq_sponge.absorb_g(&xor_comm.elems); } if let Some(rot_comm) = rot_comm { - fq_sponge.absorb_g(&rot_comm.unshifted); + fq_sponge.absorb_g(&rot_comm.elems); } // Lookup index; optional @@ -496,26 +496,26 @@ impl> VerifierIndex }) = lookup_index { for entry in lookup_table { - fq_sponge.absorb_g(&entry.unshifted); + fq_sponge.absorb_g(&entry.elems); } if let Some(table_ids) = table_ids { - fq_sponge.absorb_g(&table_ids.unshifted); + fq_sponge.absorb_g(&table_ids.elems); } if let Some(runtime_tables_selector) = runtime_tables_selector { - fq_sponge.absorb_g(&runtime_tables_selector.unshifted); + fq_sponge.absorb_g(&runtime_tables_selector.elems); } if let Some(xor) = xor { - fq_sponge.absorb_g(&xor.unshifted); + fq_sponge.absorb_g(&xor.elems); } if let Some(lookup) = lookup { - fq_sponge.absorb_g(&lookup.unshifted); + fq_sponge.absorb_g(&lookup.elems); } if let Some(range_check) = range_check { - fq_sponge.absorb_g(&range_check.unshifted); + fq_sponge.absorb_g(&range_check.elems); } if let Some(ffmul) = ffmul { - fq_sponge.absorb_g(&ffmul.unshifted); + fq_sponge.absorb_g(&ffmul.elems); } } fq_sponge.digest_fq() diff --git a/poly-commitment/src/chunked.rs b/poly-commitment/src/chunked.rs index 32cb5e1408..9c3ee5c294 100644 --- a/poly-commitment/src/chunked.rs +++ b/poly-commitment/src/chunked.rs @@ -9,21 +9,19 @@ where C: CommitmentCurve, { /// Multiplies each commitment chunk of f with powers of zeta^n - /// Note that it ignores the shifted part. // TODO(mimoo): better name for this function pub fn chunk_commitment(&self, zeta_n: C::ScalarField) -> Self { let mut res = C::Projective::zero(); // use Horner's to compute chunk[0] + z^n chunk[1] + z^2n chunk[2] + ... // as ( chunk[-1] * z^n + chunk[-2] ) * z^n + chunk[-3] // (https://en.wikipedia.org/wiki/Horner%27s_method) - for chunk in self.unshifted.iter().rev() { + for chunk in self.elems.iter().rev() { res *= zeta_n; res.add_assign_mixed(chunk); } PolyComm { - unshifted: vec![res.into_affine()], - shifted: self.shifted, + elems: vec![res.into_affine()], } } } @@ -33,14 +31,13 @@ where F: Field, { /// Multiplies each blinding chunk of f with powers of zeta^n - /// Note that it ignores the shifted part. // TODO(mimoo): better name for this function pub fn chunk_blinding(&self, zeta_n: F) -> F { let mut res = F::zero(); // use Horner's to compute chunk[0] + z^n chunk[1] + z^2n chunk[2] + ... // as ( chunk[-1] * z^n + chunk[-2] ) * z^n + chunk[-3] // (https://en.wikipedia.org/wiki/Horner%27s_method) - for chunk in self.unshifted.iter().rev() { + for chunk in self.elems.iter().rev() { res *= zeta_n; res += chunk } diff --git a/poly-commitment/src/commitment.rs b/poly-commitment/src/commitment.rs index 3d6cdf2411..bb2469b49f 100644 --- a/poly-commitment/src/commitment.rs +++ b/poly-commitment/src/commitment.rs @@ -39,9 +39,7 @@ use super::evaluation_proof::*; #[serde(bound = "C: CanonicalDeserialize + CanonicalSerialize")] pub struct PolyComm { #[serde_as(as = "Vec")] - pub unshifted: Vec, - #[serde_as(as = "Option")] - pub shifted: Option, + pub elems: Vec, } #[derive(Clone, Debug, Serialize, Deserialize)] @@ -54,8 +52,8 @@ where } impl PolyComm { - pub fn new(unshifted: Vec, shifted: Option) -> Self { - Self { unshifted, shifted } + pub fn new(elems: Vec) -> Self { + Self { elems } } } @@ -68,19 +66,18 @@ where F: FnMut(A) -> B, B: CanonicalDeserialize + CanonicalSerialize, { - let unshifted = self.unshifted.iter().map(|x| f(x.clone())).collect(); - let shifted = self.shifted.as_ref().map(|x| f(x.clone())); - PolyComm { unshifted, shifted } + let elems = self.elems.iter().map(|x| f(x.clone())).collect(); + PolyComm { elems } } - /// Returns the length of the unshifted commitment. + /// Returns the length of the commitment. pub fn len(&self) -> usize { - self.unshifted.len() + self.elems.len() } /// Returns `true` if the commitment is empty. pub fn is_empty(&self) -> bool { - self.unshifted.is_empty() && self.shifted.is_none() + self.elems.is_empty() } } @@ -90,21 +87,16 @@ impl PolyComm { &self, other: &PolyComm, ) -> Option> { - if self.unshifted.len() != other.unshifted.len() { + if self.elems.len() != other.elems.len() { return None; } - let unshifted = self - .unshifted + let elems = self + .elems .iter() - .zip(other.unshifted.iter()) + .zip(other.elems.iter()) .map(|(x, y)| (*x, *y)) .collect(); - let shifted = match (self.shifted, other.shifted) { - (Some(x), Some(y)) => Some((x, y)), - (None, None) => None, - (Some(_), None) | (None, Some(_)) => return None, - }; - Some(PolyComm { unshifted, shifted }) + Some(PolyComm { elems }) } } @@ -159,25 +151,20 @@ impl<'a, 'b, C: AffineCurve> Add<&'a PolyComm> for &'b PolyComm { type Output = PolyComm; fn add(self, other: &'a PolyComm) -> PolyComm { - let mut unshifted = vec![]; - let n1 = self.unshifted.len(); - let n2 = other.unshifted.len(); + let mut elems = vec![]; + let n1 = self.elems.len(); + let n2 = other.elems.len(); for i in 0..std::cmp::max(n1, n2) { let pt = if i < n1 && i < n2 { - self.unshifted[i] + other.unshifted[i] + self.elems[i] + other.elems[i] } else if i < n1 { - self.unshifted[i] + self.elems[i] } else { - other.unshifted[i] + other.elems[i] }; - unshifted.push(pt); + elems.push(pt); } - let shifted = match (self.shifted, other.shifted) { - (None, _) => other.shifted, - (_, None) => self.shifted, - (Some(p1), Some(p2)) => Some(p1 + p2), - }; - PolyComm { unshifted, shifted } + PolyComm { elems } } } @@ -185,37 +172,27 @@ impl<'a, 'b, C: AffineCurve> Sub<&'a PolyComm> for &'b PolyComm { type Output = PolyComm; fn sub(self, other: &'a PolyComm) -> PolyComm { - let mut unshifted = vec![]; - let n1 = self.unshifted.len(); - let n2 = other.unshifted.len(); + let mut elems = vec![]; + let n1 = self.elems.len(); + let n2 = other.elems.len(); for i in 0..std::cmp::max(n1, n2) { let pt = if i < n1 && i < n2 { - self.unshifted[i] + (-other.unshifted[i]) + self.elems[i] + (-other.elems[i]) } else if i < n1 { - self.unshifted[i] + self.elems[i] } else { - other.unshifted[i] + other.elems[i] }; - unshifted.push(pt); + elems.push(pt); } - let shifted = match (self.shifted, other.shifted) { - (None, _) => other.shifted, - (_, None) => self.shifted, - (Some(p1), Some(p2)) => Some(p1 + (-p2)), - }; - PolyComm { unshifted, shifted } + PolyComm { elems } } } impl PolyComm { pub fn scale(&self, c: C::ScalarField) -> PolyComm { PolyComm { - unshifted: self - .unshifted - .iter() - .map(|g| g.mul(c).into_affine()) - .collect(), - shifted: self.shifted.map(|g| g.mul(c).into_affine()), + elems: self.elems.iter().map(|g| g.mul(c).into_affine()).collect(), } } @@ -229,41 +206,27 @@ impl PolyComm { assert_eq!(com.len(), elm.len()); if com.is_empty() || elm.is_empty() { - return Self::new(vec![C::zero()], None); + return Self::new(vec![C::zero()]); } let all_scalars: Vec<_> = elm.iter().map(|s| s.into_repr()).collect(); - let unshifted_size = Iterator::max(com.iter().map(|c| c.unshifted.len())).unwrap(); - let mut unshifted = Vec::with_capacity(unshifted_size); + let elems_size = Iterator::max(com.iter().map(|c| c.elems.len())).unwrap(); + let mut elems = Vec::with_capacity(elems_size); - for chunk in 0..unshifted_size { + for chunk in 0..elems_size { let (points, scalars): (Vec<_>, Vec<_>) = com .iter() .zip(&all_scalars) // get rid of scalars that don't have an associated chunk - .filter_map(|(com, scalar)| com.unshifted.get(chunk).map(|c| (c, scalar))) + .filter_map(|(com, scalar)| com.elems.get(chunk).map(|c| (c, scalar))) .unzip(); let chunk_msm = VariableBaseMSM::multi_scalar_mul::(&points, &scalars); - unshifted.push(chunk_msm.into_affine()); + elems.push(chunk_msm.into_affine()); } - let mut shifted_pairs = com - .iter() - .zip(all_scalars) - // get rid of commitments without a `shifted` part - .filter_map(|(c, s)| c.shifted.map(|c| (c, s))) - .peekable(); - - let shifted = if shifted_pairs.peek().is_none() { - None - } else { - let (points, scalars): (Vec<_>, Vec<_>) = shifted_pairs.unzip(); - Some(VariableBaseMSM::multi_scalar_mul(&points, &scalars).into_affine()) - }; - - Self::new(unshifted, shifted) + Self::new(elems) } } @@ -343,10 +306,7 @@ pub fn absorb_commitment< sponge: &mut EFqSponge, commitment: &PolyComm, ) { - sponge.absorb_g(&commitment.unshifted); - if let Some(shifted) = commitment.shifted.as_ref() { - sponge.absorb_g(&[shifted.clone()]); - } + sponge.absorb_g(&commitment.elems); } /// A useful trait extending AffineCurve for commitments. @@ -443,21 +403,17 @@ pub fn to_group(m: &G::Map, t: ::BaseField /// Computes the linearization of the evaluations of a (potentially split) polynomial. /// Each given `poly` is associated to a matrix where the rows represent the number of evaluated points, /// and the columns represent potential segments (if a polynomial was split in several parts). -/// Note that if one of the polynomial comes specified with a degree bound, -/// the evaluation for the last segment is potentially shifted to meet the proof. #[allow(clippy::type_complexity)] pub fn combined_inner_product( - evaluation_points: &[F], polyscale: &F, evalscale: &F, // TODO(mimoo): needs a type that can get you evaluations or segments - polys: &[(Vec>, Option)], - srs_length: usize, + polys: &[Vec>], ) -> F { let mut res = F::zero(); let mut xi_i = F::one(); - for (evals_tr, shifted) in polys.iter().filter(|(evals_tr, _)| !evals_tr[0].is_empty()) { + for evals_tr in polys.iter().filter(|evals_tr| !evals_tr[0].is_empty()) { // transpose the evaluations let evals = (0..evals_tr[0].len()) .map(|i| evals_tr.iter().map(|v| v[i]).collect::>()) @@ -470,23 +426,6 @@ pub fn combined_inner_product( res += &(xi_i * term); xi_i *= polyscale; } - - if let Some(m) = shifted { - // polyscale^i sum_j evalscale^j elm_j^{N - m} f(elm_j) - let last_evals = if *m >= evals.len() * srs_length { - vec![F::zero(); evaluation_points.len()] - } else { - evals[evals.len() - 1].clone() - }; - let shifted_evals: Vec<_> = evaluation_points - .iter() - .zip(&last_evals) - .map(|(elm, f_elm)| elm.pow([(srs_length - (*m) % srs_length) as u64]) * f_elm) - .collect(); - - res += &(xi_i * DensePolynomial::::eval_polynomial(&shifted_evals, *evalscale)); - xi_i *= polyscale; - } } res } @@ -501,9 +440,6 @@ where /// Contains an evaluation table pub evaluations: Vec>, - - /// optional degree bound - pub degree_bound: Option, } /// Contains the batch evaluation @@ -535,33 +471,17 @@ pub fn combine_commitments( ) { let mut xi_i = G::ScalarField::one(); - for Evaluation { - commitment, - degree_bound, - .. - } in evaluations + for Evaluation { commitment, .. } in evaluations .iter() - .filter(|x| !x.commitment.unshifted.is_empty()) + .filter(|x| !x.commitment.elems.is_empty()) { // iterating over the polynomial segments - for comm_ch in &commitment.unshifted { + for comm_ch in &commitment.elems { scalars.push(rand_base * xi_i); points.push(*comm_ch); xi_i *= polyscale; } - - if let Some(_m) = degree_bound { - if let Some(comm_ch) = commitment.shifted { - if !comm_ch.is_zero() { - // polyscale^i sum_j evalscale^j elm_j^{N - m} f(elm_j) - scalars.push(rand_base * xi_i); - points.push(comm_ch); - - xi_i *= polyscale; - } - } - } } } @@ -579,13 +499,9 @@ pub fn combine_evaluations( vec![G::ScalarField::zero(); num_evals] }; - for Evaluation { - evaluations, - degree_bound, - .. - } in evaluations + for Evaluation { evaluations, .. } in evaluations .iter() - .filter(|x| !x.commitment.unshifted.is_empty()) + .filter(|x| !x.commitment.elems.is_empty()) { // iterating over the polynomial segments for j in 0..evaluations[0].len() { @@ -594,10 +510,6 @@ pub fn combine_evaluations( } xi_i *= polyscale; } - - if let Some(_m) = degree_bound { - todo!("Misaligned chunked commitments are not supported") - } } acc @@ -622,10 +534,9 @@ impl SRSTrait for SRS { &self, plnm: &DensePolynomial, num_chunks: usize, - max: Option, rng: &mut (impl RngCore + CryptoRng), ) -> BlindedCommitment { - self.mask(self.commit_non_hiding(plnm, num_chunks, max), rng) + self.mask(self.commit_non_hiding(plnm, num_chunks), rng) } /// Turns a non-hiding polynomial commitment into a hidding polynomial commitment. Transforms each given `` into `( + wH, w)` with a random `w` per commitment. @@ -660,62 +571,34 @@ impl SRSTrait for SRS { /// This function commits a polynomial using the SRS' basis of size `n`. /// - `plnm`: polynomial to commit to with max size of sections - /// - `num_chunks`: the number of unshifted commitments to be included in the output polynomial commitment - /// - `max`: maximal degree of the polynomial (not inclusive), if none, no degree bound - /// The function returns an unbounded commitment vector (which splits the commitment into several commitments of size at most `n`), - /// as well as an optional bounded commitment (if `max` is set). - /// Note that a maximum degree cannot (and doesn't need to) be enforced via a shift if `max` is a multiple of `n`. + /// - `num_chunks`: the number of commitments to be included in the output polynomial commitment + /// The function returns an unbounded commitment vector + /// (which splits the commitment into several commitments of size at most `n`). fn commit_non_hiding( &self, plnm: &DensePolynomial, num_chunks: usize, - max: Option, ) -> PolyComm { let is_zero = plnm.is_zero(); - let basis_len = self.g.len(); - let coeffs_len = plnm.coeffs.len(); - let coeffs: Vec<_> = plnm.iter().map(|c| c.into_repr()).collect(); // chunk while commiting - let mut unshifted = vec![]; + let mut elems = vec![]; if is_zero { - unshifted.push(G::zero()); + elems.push(G::zero()); } else { coeffs.chunks(self.g.len()).for_each(|coeffs_chunk| { let chunk = VariableBaseMSM::multi_scalar_mul(&self.g, coeffs_chunk); - unshifted.push(chunk.into_affine()); + elems.push(chunk.into_affine()); }); } - for _ in unshifted.len()..num_chunks { - unshifted.push(G::zero()); + for _ in elems.len()..num_chunks { + elems.push(G::zero()); } - // committing only last chunk shifted to the right edge of SRS - let shifted = match max { - None => None, - Some(max) => { - let start = max - (max % basis_len); - if is_zero || start >= coeffs_len { - // polynomial is small, nothing was shifted - Some(G::zero()) - } else if max % basis_len == 0 { - // the number of chunks should tell the verifier everything they need to know - None - } else { - // we shift the last chunk to the right as proof of the degree bound - let shifted = VariableBaseMSM::multi_scalar_mul( - &self.g[basis_len - (max % basis_len)..], - &coeffs[start..], - ); - Some(shifted.into_affine()) - } - } - }; - - PolyComm:: { unshifted, shifted } + PolyComm:: { elems } } fn commit_evaluations_non_hiding( @@ -968,7 +851,7 @@ mod tests { let mut e = vec![Fp::zero(); n]; e[i] = Fp::one(); let p = Evaluations::>::from_vec_and_domain(e, domain).interpolate(); - srs.commit_non_hiding(&p, num_chunks, None) + srs.commit_non_hiding(&p, num_chunks) }) .collect(); @@ -982,21 +865,24 @@ mod tests { } #[test] + // This tests with two chunks. fn test_chunked_lagrange_commitments() { let n = 64; + let divisor = 4; let domain = D::::new(n).unwrap(); - let mut srs = SRS::::create(n / 2); + let mut srs = SRS::::create(n / divisor); srs.add_lagrange_basis(domain); let num_chunks = domain.size() / srs.g.len(); + assert!(num_chunks == divisor); let expected_lagrange_commitments: Vec<_> = (0..n) .map(|i| { let mut e = vec![Fp::zero(); n]; e[i] = Fp::one(); let p = Evaluations::>::from_vec_and_domain(e, domain).interpolate(); - srs.commit_non_hiding(&p, num_chunks, None) + srs.commit_non_hiding(&p, num_chunks) }) .collect(); @@ -1010,6 +896,10 @@ mod tests { } #[test] + // TODO @volhovm I don't understand what this test does and + // whether it is worth leaving. + /// Same as test_chunked_lagrange_commitments, but with a slight + /// offset in the SRS fn test_offset_chunked_lagrange_commitments() { let n = 64; let domain = D::::new(n).unwrap(); @@ -1017,14 +907,16 @@ mod tests { let mut srs = SRS::::create(n / 2 + 1); srs.add_lagrange_basis(domain); + // Is this even taken into account?... let num_chunks = (domain.size() + srs.g.len() - 1) / srs.g.len(); + assert!(num_chunks == 2); let expected_lagrange_commitments: Vec<_> = (0..n) .map(|i| { let mut e = vec![Fp::zero(); n]; e[i] = Fp::one(); let p = Evaluations::>::from_vec_and_domain(e, domain).interpolate(); - srs.commit_non_hiding(&p, num_chunks, Some(64)) + srs.commit_non_hiding(&p, num_chunks) // this requires max = Some(64) }) .collect(); @@ -1048,10 +940,9 @@ mod tests { let srs = SRS::::create(20); let rng = &mut StdRng::from_seed([0u8; 32]); - // commit the two polynomials (and upperbound the second one) - let commitment = srs.commit(&poly1, 1, None, rng); - let upperbound = poly2.degree() + 1; - let bounded_commitment = srs.commit(&poly2, 1, Some(upperbound), rng); + // commit the two polynomials + let commitment1 = srs.commit(&poly1, 1, rng); + let commitment2 = srs.commit(&poly2, 1, rng); // create an aggregated opening proof let (u, v) = (Fp::rand(rng), Fp::rand(rng)); @@ -1061,18 +952,15 @@ mod tests { let polys: Vec<( DensePolynomialOrEvaluations<_, Radix2EvaluationDomain<_>>, - Option, PolyComm<_>, )> = vec![ ( DensePolynomialOrEvaluations::DensePolynomial(&poly1), - None, - commitment.blinders, + commitment1.blinders, ), ( DensePolynomialOrEvaluations::DensePolynomial(&poly2), - Some(upperbound), - bounded_commitment.blinders, + commitment2.blinders, ), ]; let elm = vec![Fp::rand(rng), Fp::rand(rng)]; @@ -1110,40 +998,21 @@ mod tests { let evaluations = vec![ Evaluation { - commitment: commitment.commitment, + commitment: commitment1.commitment, evaluations: poly1_chunked_evals, - degree_bound: None, }, Evaluation { - commitment: bounded_commitment.commitment, + commitment: commitment2.commitment, evaluations: poly2_chunked_evals, - degree_bound: Some(upperbound), }, ]; let combined_inner_product = { let es: Vec<_> = evaluations .iter() - .map( - |Evaluation { - commitment, - evaluations, - degree_bound, - }| { - let bound: Option = (|| { - let b = (*degree_bound)?; - let x = commitment.shifted?; - if x.is_zero() { - None - } else { - Some(b) - } - })(); - (evaluations.clone(), bound) - }, - ) + .map(|Evaluation { evaluations, .. }| evaluations.clone()) .collect(); - combined_inner_product(&elm, &v, &u, &es, srs.g.len()) + combined_inner_product(&v, &u, &es) }; // verify the proof @@ -1186,8 +1055,8 @@ pub mod caml { { fn from(polycomm: PolyComm) -> Self { Self { - unshifted: polycomm.unshifted.into_iter().map(Into::into).collect(), - shifted: polycomm.shifted.map(Into::into), + unshifted: polycomm.elems.into_iter().map(Into::into).collect(), + shifted: None, } } } @@ -1199,8 +1068,8 @@ pub mod caml { { fn from(polycomm: &'a PolyComm) -> Self { Self { - unshifted: polycomm.unshifted.iter().map(Into::into).collect(), - shifted: polycomm.shifted.as_ref().map(Into::into), + unshifted: polycomm.elems.iter().map(Into::into).collect(), + shifted: None, } } } @@ -1210,9 +1079,12 @@ pub mod caml { G: AffineCurve + From, { fn from(camlpolycomm: CamlPolyComm) -> PolyComm { + assert!( + camlpolycomm.shifted.is_none(), + "mina#14628: Shifted commitments are deprecated and must not be used" + ); PolyComm { - unshifted: camlpolycomm.unshifted.into_iter().map(Into::into).collect(), - shifted: camlpolycomm.shifted.map(Into::into), + elems: camlpolycomm.unshifted.into_iter().map(Into::into).collect(), } } } @@ -1222,9 +1094,13 @@ pub mod caml { G: AffineCurve + From<&'a CamlG> + From, { fn from(camlpolycomm: &'a CamlPolyComm) -> PolyComm { + assert!( + camlpolycomm.shifted.is_none(), + "mina#14628: Shifted commitments are deprecated and must not be used" + ); PolyComm { - unshifted: camlpolycomm.unshifted.iter().map(Into::into).collect(), - shifted: camlpolycomm.shifted.as_ref().map(Into::into), + //FIXME something with as_ref() + elems: camlpolycomm.unshifted.iter().map(Into::into).collect(), } } } diff --git a/poly-commitment/src/evaluation_proof.rs b/poly-commitment/src/evaluation_proof.rs index 0b15615b66..6b2e9dcfc3 100644 --- a/poly-commitment/src/evaluation_proof.rs +++ b/poly-commitment/src/evaluation_proof.rs @@ -12,16 +12,11 @@ use serde::{Deserialize, Serialize}; use serde_with::serde_as; use std::iter::Iterator; -enum OptShiftedPolynomial

{ - Unshifted(P), - Shifted(P, usize), -} - // A formal sum of the form // `s_0 * p_0 + ... s_n * p_n` -// where each `s_i` is a scalar and each `p_i` is an optionally shifted polynomial. +// where each `s_i` is a scalar and each `p_i` is a polynomial. #[derive(Default)] -struct ScaledChunkedPolynomial(Vec<(F, OptShiftedPolynomial

)>); +struct ScaledChunkedPolynomial(Vec<(F, P)>); pub enum DensePolynomialOrEvaluations<'a, F: FftField, D: EvaluationDomain> { DensePolynomial(&'a DensePolynomial), @@ -29,13 +24,8 @@ pub enum DensePolynomialOrEvaluations<'a, F: FftField, D: EvaluationDomain> { } impl ScaledChunkedPolynomial { - fn add_unshifted(&mut self, scale: F, p: P) { - self.0.push((scale, OptShiftedPolynomial::Unshifted(p))) - } - - fn add_shifted(&mut self, scale: F, shift: usize, p: P) { - self.0 - .push((scale, OptShiftedPolynomial::Shifted(p, shift))) + fn add_poly(&mut self, scale: F, p: P) { + self.0.push((scale, p)) } } @@ -48,18 +38,8 @@ impl<'a, F: Field> ScaledChunkedPolynomial { .par_iter() .map(|(scale, segment)| { let scale = *scale; - match segment { - OptShiftedPolynomial::Unshifted(segment) => { - let v = segment.par_iter().map(|x| scale * *x).collect(); - DensePolynomial::from_coefficients_vec(v) - } - OptShiftedPolynomial::Shifted(segment, shift) => { - let mut v: Vec<_> = segment.par_iter().map(|x| scale * *x).collect(); - let mut res = vec![F::zero(); *shift]; - res.append(&mut v); - DensePolynomial::from_coefficients_vec(res) - } - } + let v = segment.par_iter().map(|x| scale * *x).collect(); + DensePolynomial::from_coefficients_vec(v) }) .collect(); @@ -85,7 +65,7 @@ pub fn combine_polys>( // If/when we change this, we can add more complicated code to handle different degrees. let degree = plnms .iter() - .fold(None, |acc, (p, _, _)| match p { + .fold(None, |acc, (p, _)| match p { DensePolynomialOrEvaluations::DensePolynomial(_) => acc, DensePolynomialOrEvaluations::Evaluations(_, d) => { if let Some(n) = acc { @@ -97,13 +77,12 @@ pub fn combine_polys>( .unwrap_or(0); vec![G::ScalarField::zero(); degree] }; - // let mut plnm_chunks: Vec<(G::ScalarField, OptShiftedPolynomial<_>)> = vec![]; let mut omega = G::ScalarField::zero(); let mut scale = G::ScalarField::one(); // iterating over polynomials in the batch - for (p_i, degree_bound, omegas) in plnms { + for (p_i, omegas) in plnms { match p_i { DensePolynomialOrEvaluations::Evaluations(evals_i, sub_domain) => { let stride = evals_i.evals.len() / sub_domain.size(); @@ -114,41 +93,23 @@ pub fn combine_polys>( .for_each(|(i, x)| { *x += scale * evals[i * stride]; }); - for j in 0..omegas.unshifted.len() { - omega += &(omegas.unshifted[j] * scale); + for j in 0..omegas.elems.len() { + omega += &(omegas.elems[j] * scale); scale *= &polyscale; } - // We assume here that we have no shifted segment. - // TODO: Remove shifted } DensePolynomialOrEvaluations::DensePolynomial(p_i) => { let mut offset = 0; // iterating over chunks of the polynomial - if let Some(m) = degree_bound { - assert!(p_i.coeffs.len() <= m + 1); - } else { - assert!(omegas.shifted.is_none()); - } - for j in 0..omegas.unshifted.len() { + for j in 0..omegas.elems.len() { let segment = &p_i.coeffs[std::cmp::min(offset, p_i.coeffs.len()) ..std::cmp::min(offset + srs_length, p_i.coeffs.len())]; - // always mixing in the unshifted segments - plnm.add_unshifted(scale, segment); + plnm.add_poly(scale, segment); - omega += &(omegas.unshifted[j] * scale); + omega += &(omegas.elems[j] * scale); scale *= &polyscale; offset += srs_length; - if let Some(m) = degree_bound { - if offset >= *m { - if offset > *m { - // mixing in the shifted segment since degree is bounded - plnm.add_shifted(scale, srs_length - m % srs_length, segment); - } - omega += &(omegas.shifted.unwrap() * scale); - scale *= &polyscale; - } - } } } } @@ -158,7 +119,11 @@ pub fn combine_polys>( if !plnm_evals_part.is_empty() { let n = plnm_evals_part.len(); let max_poly_size = srs_length; - let num_chunks = n / max_poly_size; + let num_chunks = if n == 0 { + 1 + } else { + n / max_poly_size + if n % max_poly_size == 0 { 0 } else { 1 } + }; plnm += &Evaluations::from_vec_and_domain(plnm_evals_part, D::new(n).unwrap()) .interpolate() .to_chunked_polynomial(num_chunks, max_poly_size) @@ -183,15 +148,11 @@ impl SRS { &self, group_map: &G::Map, // TODO(mimoo): create a type for that entry - plnms: &[( - DensePolynomialOrEvaluations, - Option, - PolyComm, - )], // vector of polynomial with optional degree bound and commitment randomness - elm: &[G::ScalarField], // vector of evaluation points - polyscale: G::ScalarField, // scaling factor for polynoms - evalscale: G::ScalarField, // scaling factor for evaluation point powers - mut sponge: EFqSponge, // sponge + plnms: PolynomialsToCombine, // vector of polynomial with commitment randomness + elm: &[G::ScalarField], // vector of evaluation points + polyscale: G::ScalarField, // scaling factor for polynoms + evalscale: G::ScalarField, // scaling factor for evaluation point powers + mut sponge: EFqSponge, // sponge rng: &mut RNG, ) -> OpeningProof where @@ -362,11 +323,7 @@ impl SRS { #[allow(clippy::many_single_char_names)] pub fn prover_polynomials_to_verifier_evaluations>( &self, - plnms: &[( - DensePolynomialOrEvaluations, - Option, - PolyComm, - )], // vector of polynomial with optional degree bound and commitment randomness + plnms: PolynomialsToCombine, elm: &[G::ScalarField], // vector of evaluation points ) -> Vec> where @@ -375,7 +332,7 @@ impl SRS { plnms .iter() .enumerate() - .map(|(i, (poly_or_evals, degree_bound, blinders))| { + .map(|(i, (poly_or_evals, blinders))| { let poly = match poly_or_evals { DensePolynomialOrEvaluations::DensePolynomial(poly) => (*poly).clone(), DensePolynomialOrEvaluations::Evaluations(evals, _) => { @@ -383,9 +340,8 @@ impl SRS { } }; let chunked_polynomial = - poly.to_chunked_polynomial(blinders.unshifted.len(), self.g.len()); - let chunked_commitment = - { self.commit_non_hiding(&poly, blinders.unshifted.len(), None) }; + poly.to_chunked_polynomial(blinders.elems.len(), self.g.len()); + let chunked_commitment = { self.commit_non_hiding(&poly, blinders.elems.len()) }; let masked_commitment = match self.mask_custom(chunked_commitment, blinders) { Ok(comm) => comm, Err(err) => panic!("Error at index {i}: {err}"), @@ -398,8 +354,6 @@ impl SRS { commitment: masked_commitment.commitment, evaluations: chunked_evals, - - degree_bound: *degree_bound, } }) .collect() @@ -433,11 +387,7 @@ impl< fn open::ScalarField>>( srs: &Self::SRS, group_map: &::Map, - plnms: &[( - DensePolynomialOrEvaluations<::ScalarField, D>, - Option, - PolyComm<::ScalarField>, - )], // vector of polynomial with optional degree bound and commitment randomness + plnms: PolynomialsToCombine, elm: &[::ScalarField], // vector of evaluation points polyscale: ::ScalarField, // scaling factor for polynoms evalscale: ::ScalarField, // scaling factor for evaluation point powers diff --git a/poly-commitment/src/lib.rs b/poly-commitment/src/lib.rs index 4d7bac7913..fb7f7491ca 100644 --- a/poly-commitment/src/lib.rs +++ b/poly-commitment/src/lib.rs @@ -37,7 +37,6 @@ pub trait SRS { &self, plnm: &DensePolynomial, num_chunks: usize, - max: Option, rng: &mut (impl RngCore + CryptoRng), ) -> BlindedCommitment; @@ -60,15 +59,13 @@ pub trait SRS { /// This function commits a polynomial using the SRS' basis of size `n`. /// - `plnm`: polynomial to commit to with max size of sections - /// - `max`: maximal degree of the polynomial (not inclusive), if none, no degree bound - /// The function returns an unbounded commitment vector (which splits the commitment into several commitments of size at most `n`), - /// as well as an optional bounded commitment (if `max` is set). - /// Note that a maximum degree cannot (and doesn't need to) be enforced via a shift if `max` is a multiple of `n`. + /// - `num_chunks`: the number of commitments to be included in the output polynomial commitment + /// The function returns an unbounded commitment vector + /// (which splits the commitment into several commitments of size at most `n`). fn commit_non_hiding( &self, plnm: &DensePolynomial, num_chunks: usize, - max: Option, ) -> PolyComm; fn commit_evaluations_non_hiding( @@ -86,9 +83,9 @@ pub trait SRS { } #[allow(type_alias_bounds)] +/// Vector of triples (polynomial itself, degree bound, omegas). type PolynomialsToCombine<'a, G: CommitmentCurve, D: EvaluationDomain> = &'a [( DensePolynomialOrEvaluations<'a, G::ScalarField, D>, - Option, PolyComm, )]; diff --git a/poly-commitment/src/pairing_proof.rs b/poly-commitment/src/pairing_proof.rs index 913cf15d0f..1a581e538b 100644 --- a/poly-commitment/src/pairing_proof.rs +++ b/poly-commitment/src/pairing_proof.rs @@ -1,5 +1,5 @@ use crate::commitment::*; -use crate::evaluation_proof::{combine_polys, DensePolynomialOrEvaluations}; +use crate::evaluation_proof::combine_polys; use crate::srs::SRS; use crate::{CommitmentError, PolynomialsToCombine, SRS as SRSTrait}; use ark_ec::{msm::VariableBaseMSM, AffineCurve, PairingEngine}; @@ -94,11 +94,7 @@ impl< fn open::ScalarField>>( srs: &Self::SRS, _group_map: &::Map, - plnms: &[( - DensePolynomialOrEvaluations<::ScalarField, D>, - Option, - PolyComm<::ScalarField>, - )], // vector of polynomial with optional degree bound and commitment randomness + plnms: PolynomialsToCombine, elm: &[::ScalarField], // vector of evaluation points polyscale: ::ScalarField, // scaling factor for polynoms _evalscale: ::ScalarField, // scaling factor for evaluation point powers @@ -164,10 +160,9 @@ impl< &self, plnm: &DensePolynomial, num_chunks: usize, - max: Option, rng: &mut (impl RngCore + CryptoRng), ) -> BlindedCommitment { - self.full_srs.commit(plnm, num_chunks, max, rng) + self.full_srs.commit(plnm, num_chunks, rng) } fn mask_custom( @@ -190,9 +185,8 @@ impl< &self, plnm: &DensePolynomial, num_chunks: usize, - max: Option, ) -> PolyComm { - self.full_srs.commit_non_hiding(plnm, num_chunks, max) + self.full_srs.commit_non_hiding(plnm, num_chunks) } fn commit_evaluations_non_hiding( @@ -282,10 +276,7 @@ impl< quotient }; - let quotient = srs - .full_srs - .commit_non_hiding("ient_poly, 1, None) - .unshifted[0]; + let quotient = srs.full_srs.commit_non_hiding("ient_poly, 1).elems[0]; Some(PairingProof { quotient, @@ -317,12 +308,12 @@ impl< let blinding_commitment = srs.full_srs.h.mul(self.blinding); let divisor_commitment = srs .verifier_srs - .commit_non_hiding(&divisor_polynomial(elm), 1, None) - .unshifted[0]; + .commit_non_hiding(&divisor_polynomial(elm), 1) + .elems[0]; let eval_commitment = srs .full_srs - .commit_non_hiding(&eval_polynomial(elm, &evals), 1, None) - .unshifted[0] + .commit_non_hiding(&eval_polynomial(elm, &evals), 1) + .elems[0] .into_projective(); let numerator_commitment = { poly_commitment - eval_commitment - blinding_commitment }; @@ -380,18 +371,17 @@ mod tests { let comms: Vec<_> = polynomials .iter() - .map(|p| srs.full_srs.commit(p, 1, None, rng)) + .map(|p| srs.full_srs.commit(p, 1, rng)) .collect(); - let polynomials_and_blinders: Vec<(DensePolynomialOrEvaluations<_, D<_>>, _, _)> = - polynomials - .iter() - .zip(comms.iter()) - .map(|(p, comm)| { - let p = DensePolynomialOrEvaluations::DensePolynomial(p); - (p, None, comm.blinders.clone()) - }) - .collect(); + let polynomials_and_blinders: Vec<(DensePolynomialOrEvaluations<_, D<_>>, _)> = polynomials + .iter() + .zip(comms.iter()) + .map(|(p, comm)| { + let p = DensePolynomialOrEvaluations::DensePolynomial(p); + (p, comm.blinders.clone()) + }) + .collect(); let evaluation_points = vec![ScalarField::rand(rng), ScalarField::rand(rng)]; @@ -409,7 +399,6 @@ mod tests { Evaluation { commitment: commitment.commitment, evaluations, - degree_bound: None, } }) .collect(); diff --git a/poly-commitment/src/srs.rs b/poly-commitment/src/srs.rs index 899b708224..355c420b66 100644 --- a/poly-commitment/src/srs.rs +++ b/poly-commitment/src/srs.rs @@ -178,11 +178,11 @@ impl SRS { // By computing each of these, and recollecting the terms as a vector of polynomial // commitments, we obtain a chunked commitment to the L_i polynomials. let srs_size = self.g.len(); - let num_unshifteds = (n + srs_size - 1) / srs_size; - let mut unshifted = Vec::with_capacity(num_unshifteds); + let num_elems = (n + srs_size - 1) / srs_size; + let mut elems = Vec::with_capacity(num_elems); // For each chunk - for i in 0..num_unshifteds { + for i in 0..num_elems { // Initialize the vector with zero curve points let mut lg: Vec<::Projective> = vec![::Projective::zero(); n]; @@ -195,36 +195,13 @@ impl SRS { // Apply the IFFT domain.ifft_in_place(&mut lg); ::Projective::batch_normalization(lg.as_mut_slice()); - // Append the 'partial Langrange polynomials' to the vector of unshifted chunks - unshifted.push(lg) + // Append the 'partial Langrange polynomials' to the vector of elems chunks + elems.push(lg) } - // If the srs size does not exactly divide the domain size - let shifted: Option::Projective>> = - if n < srs_size || num_unshifteds * srs_size == n { - None - } else { - // Initialize the vector to zero - let mut lg: Vec<::Projective> = - vec![::Projective::zero(); n]; - // Overwrite the terms corresponding to the final chunk with the SRS curve points - // shifted to the right - let start_offset = (num_unshifteds - 1) * srs_size; - let num_terms = n - start_offset; - let srs_start_offset = srs_size - num_terms; - for j in 0..num_terms { - lg[start_offset + j] = self.g[srs_start_offset + j].into_projective() - } - // Apply the IFFT - domain.ifft_in_place(&mut lg); - ::Projective::batch_normalization(lg.as_mut_slice()); - Some(lg) - }; - let chunked_commitments: Vec<_> = (0..n) .map(|i| PolyComm { - unshifted: unshifted.iter().map(|v| v[i].into_affine()).collect(), - shifted: shifted.as_ref().map(|v| v[i].into_affine()), + elems: elems.iter().map(|v| v[i].into_affine()).collect(), }) .collect(); self.lagrange_bases.insert(n, chunked_commitments); diff --git a/poly-commitment/src/tests/batch_15_wires.rs b/poly-commitment/src/tests/batch_15_wires.rs index 570e8e8752..545a788fd8 100644 --- a/poly-commitment/src/tests/batch_15_wires.rs +++ b/poly-commitment/src/tests/batch_15_wires.rs @@ -30,8 +30,6 @@ where let size = 1 << 7; let srs = SRS::::create(size); - let num_chunks = 1; - let group_map = ::Map::setup(); let sponge = DefaultFqSponge::::new( @@ -62,6 +60,8 @@ where } }) .collect::>(); + + // TODO @volhovm remove? let bounds = a .iter() .enumerate() @@ -81,10 +81,19 @@ where let mut start = Instant::now(); let comm = (0..a.len()) .map(|i| { + let n = a[i].len(); + let num_chunks = if n == 0 { + 1 + } else { + n / srs.g.len() + if n % srs.g.len() == 0 { 0 } else { 1 } + }; ( - srs.commit(&a[i].clone(), num_chunks, bounds[i], rng), + srs.commit(&a[i].clone(), num_chunks, rng), x.iter() - .map(|xx| a[i].to_chunked_polynomial(1, size).evaluate_chunks(*xx)) + .map(|xx| { + a[i].to_chunked_polynomial(num_chunks, size) + .evaluate_chunks(*xx) + }) .collect::>(), bounds[i], ) @@ -96,12 +105,10 @@ where let polys: Vec<( DensePolynomialOrEvaluations<_, Radix2EvaluationDomain<_>>, _, - _, )> = (0..a.len()) .map(|i| { ( DensePolynomialOrEvaluations::DensePolynomial(&a[i]), - bounds[i], (comm[i].0).blinders.clone(), ) }) @@ -120,20 +127,9 @@ where let combined_inner_product = { let es: Vec<_> = comm .iter() - .map(|(commitment, evaluations, degree_bound)| { - let bound: Option = (|| { - let b = (*degree_bound)?; - let x = commitment.commitment.shifted?; - if x.is_zero() { - None - } else { - Some(b) - } - })(); - (evaluations.clone(), bound) - }) + .map(|(_, evaluations, _)| evaluations.clone()) .collect(); - combined_inner_product(&x, &polymask, &evalmask, &es, srs.g.len()) + combined_inner_product(&polymask, &evalmask, &es) }; ( @@ -161,7 +157,6 @@ where .map(|poly| Evaluation { commitment: (poly.0).commitment.clone(), evaluations: poly.1.clone(), - degree_bound: poly.2, }) .collect::>(), opening: &proof.5, diff --git a/poly-commitment/src/tests/commitment.rs b/poly-commitment/src/tests/commitment.rs index dedcd0ad6e..38d57994ec 100644 --- a/poly-commitment/src/tests/commitment.rs +++ b/poly-commitment/src/tests/commitment.rs @@ -27,8 +27,6 @@ use std::time::{Duration, Instant}; pub struct Commitment { /// the commitment itself, potentially in chunks chunked_commitment: PolyComm, - /// an optional degree bound - bound: Option, } /// An evaluated commitment (given a number of evaluation points) @@ -76,7 +74,6 @@ impl AggregatedEvaluationProof { /// This function converts an aggregated evaluation proof into something the verify API understands pub fn verify_type( &self, - srs: &SRS, ) -> BatchEvaluationProof, OpeningProof> { let mut coms = vec![]; @@ -85,39 +82,15 @@ impl AggregatedEvaluationProof { coms.push(Evaluation { commitment: eval_com.commit.chunked_commitment.clone(), evaluations: eval_com.chunked_evals.clone(), - degree_bound: eval_com.commit.bound, }); } let combined_inner_product = { let es: Vec<_> = coms .iter() - .map( - |Evaluation { - commitment, - evaluations, - degree_bound, - }| { - let bound: Option = (|| { - let b = (*degree_bound)?; - let x = commitment.shifted?; - if x.is_zero() { - None - } else { - Some(b) - } - })(); - (evaluations.clone(), bound) - }, - ) + .map(|Evaluation { evaluations, .. }| evaluations.clone()) .collect(); - combined_inner_product( - &self.eval_points, - &self.polymask, - &self.evalmask, - &es, - srs.g.len(), - ) + combined_inner_product(&self.polymask, &self.evalmask, &es) }; BatchEvaluationProof { @@ -156,42 +129,40 @@ fn test_randomised(mut rng: &mut RNG) { // create 11 polynomials of random degree (of at most 500) // and commit to them let mut commitments = vec![]; - for i in 0..11 { + for _ in 0..11 { let len: usize = rng.gen(); let len = len % 500; + // TODO @volhovm maybe remove the second case. + // every other polynomial is upperbounded let poly = if len == 0 { DensePolynomial::::zero() } else { DensePolynomial::::rand(len, &mut rng) }; - // every other polynomial is upperbounded - let bound = if i % 2 == 0 { - Some(poly.coeffs.len()) - } else { - None - }; - // create commitments for each polynomial, and evaluate each polynomial at the 7 random points let timer = Instant::now(); let BlindedCommitment { commitment: chunked_commitment, blinders: chunked_blinding, - } = srs.commit(&poly, num_chunks, bound, &mut rng); + } = srs.commit(&poly, num_chunks, &mut rng); time_commit += timer.elapsed(); let mut chunked_evals = vec![]; for point in eval_points.clone() { + let n = poly.len(); + let num_chunks = if n == 0 { + 1 + } else { + n / srs.g.len() + if n % srs.g.len() == 0 { 0 } else { 1 } + }; chunked_evals.push( - poly.to_chunked_polynomial(1, srs.g.len()) + poly.to_chunked_polynomial(num_chunks, srs.g.len()) .evaluate_chunks(point), ); } - let commit = Commitment { - chunked_commitment, - bound, - }; + let commit = Commitment { chunked_commitment }; let eval_commit = EvaluatedCommitment { commit, @@ -209,13 +180,11 @@ fn test_randomised(mut rng: &mut RNG) { #[allow(clippy::type_complexity)] let mut polynomials: Vec<( DensePolynomialOrEvaluations>, - Option, PolyComm<_>, )> = vec![]; for c in &commitments { polynomials.push(( DensePolynomialOrEvaluations::DensePolynomial(&c.poly), - c.eval_commit.commit.bound, c.chunked_blinding.clone(), )); } @@ -257,7 +226,7 @@ fn test_randomised(mut rng: &mut RNG) { let timer = Instant::now(); // batch verify all the proofs - let mut batch: Vec<_> = proofs.iter().map(|p| p.verify_type(&srs)).collect(); + let mut batch: Vec<_> = proofs.iter().map(|p| p.verify_type()).collect(); assert!(srs.verify::, _>(&group_map, &mut batch, &mut rng)); // TODO: move to bench diff --git a/utils/src/dense_polynomial.rs b/utils/src/dense_polynomial.rs index 72560f1057..895e227fe0 100644 --- a/utils/src/dense_polynomial.rs +++ b/utils/src/dense_polynomial.rs @@ -57,6 +57,10 @@ impl ExtendedDensePolynomial for DensePolynomial { chunk_polys.push(DensePolynomial::from_coefficients_vec(vec![])); } + // Ensuring that the number of chunks is the one requested, following + // trait documentation + assert_eq!(chunk_polys.len(), num_chunks); + ChunkedPolynomial { polys: chunk_polys, size: chunk_size,