Merge branch 'develop' into new_version

.github/workflows/rust.yml

@@ -60,7 +60,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: |

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.

Cargo.toml

@@ -15,6 +15,7 @@ members = [
     "utils",
     "internal-tracing",
 ]
+resolver = "2"
 
 [profile.release]
 lto = true

book/Cargo.toml

@@ -10,4 +10,6 @@ edition = "2021"
 license = "Apache-2.0"
 
 [build-dependencies]
-cargo-spec = { version = "0.5.0" }
+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`).

book/src/specs/kimchi.md

@@ -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.

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"

kimchi/src/circuits/constraints.rs

@@ -683,7 +683,9 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
     /// 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<LookupTable<F>>) -> Self {
         self.lookup_tables = lookup_tables;
@@ -693,8 +695,9 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
     /// 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<Vec<RuntimeTableCfg<F>>>) -> Self {
         self.runtime_tables = runtime_tables;
@@ -736,9 +739,25 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
 
         let lookup_domain_size = {
             // First we sum over the lookup table size
-            let mut lookup_domain_size: usize = lookup_tables.iter().map(|lt| lt.len()).sum();
+            let mut has_table_with_id_0 = false;
+            let mut lookup_domain_size: usize = lookup_tables
+                .iter()
+                .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();
                 }
@@ -757,7 +776,14 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
             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
@@ -784,6 +810,9 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
         //~    ```
         //~
         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;
 

kimchi/src/circuits/gate.rs

@@ -209,6 +209,7 @@ impl<F: PrimeField + SquareRootField> CircuitGate<F> {
             EndoMul => self.verify_endomul::<G>(row, witness, &index.cs),
             EndoMulScalar => self.verify_endomul_scalar::<G>(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::<G>(row, witness, &index.cs)
@@ -303,6 +304,7 @@ impl<F: PrimeField + SquareRootField> CircuitGate<F> {
             }
             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),