Merge pull request #2372 from o1-labs/dw/ivc-base-case

IVC: base case - temporary solution

.config/nextest.toml

@@ -0,0 +1,125 @@
+# Copied from https://nexte.st/docs/configuration/
+
+# This is the default config used by nextest. It is embedded in the binary at
+# build time. It may be used as a template for .config/nextest.toml.
+
+[store]
+# The directory under the workspace root at which nextest-related files are
+# written. Profile-specific storage is currently written to dir/<profile-name>.
+dir = "target/nextest"
+
+# This section defines the default nextest profile. Custom profiles are layered
+# on top of the default profile.
+[profile.default]
+# "retries" defines the number of times a test should be retried. If set to a
+# non-zero value, tests that succeed on a subsequent attempt will be marked as
+# flaky. Can be overridden through the `--retries` option.
+# Examples
+# * retries = 3
+# * retries = { backoff = "fixed", count = 2, delay = "1s" }
+# * retries = { backoff = "exponential", count = 10, delay = "1s", jitter = true, max-delay = "10s" }
+retries = 0
+
+# The number of threads to run tests with. Supported values are either an integer or
+# the string "num-cpus". Can be overridden through the `--test-threads` option.
+test-threads = "num-cpus"
+
+# The number of threads required for each test. This is generally used in overrides to
+# mark certain tests as heavier than others. However, it can also be set as a global parameter.
+threads-required = 1
+
+# Show these test statuses in the output.
+#
+# The possible values this can take are:
+# * none: no output
+# * fail: show failed (including exec-failed) tests
+# * retry: show flaky and retried tests
+# * slow: show slow tests
+# * pass: show passed tests
+# * skip: show skipped tests (most useful for CI)
+# * all: all of the above
+#
+# Each value includes all the values above it; for example, "slow" includes
+# failed and retried tests.
+#
+# Can be overridden through the `--status-level` flag.
+status-level = "pass"
+
+# Similar to status-level, show these test statuses at the end of the run.
+final-status-level = "flaky"
+
+# "failure-output" defines when standard output and standard error for failing tests are produced.
+# Accepted values are
+# * "immediate": output failures as soon as they happen
+# * "final": output failures at the end of the test run
+# * "immediate-final": output failures as soon as they happen and at the end of
+#   the test run; combination of "immediate" and "final"
+# * "never": don't output failures at all
+#
+# For large test suites and CI it is generally useful to use "immediate-final".
+#
+# Can be overridden through the `--failure-output` option.
+failure-output = "immediate"
+
+# "success-output" controls production of standard output and standard error on success. This should
+# generally be set to "never".
+success-output = "never"
+
+# Cancel the test run on the first failure. For CI runs, consider setting this
+# to false.
+fail-fast = true
+
+# Treat a test that takes longer than the configured 'period' as slow, and print a message.
+# See <https://nexte.st/book/slow-tests> for more information.
+#
+# Optional: specify the parameter 'terminate-after' with a non-zero integer,
+# which will cause slow tests to be terminated after the specified number of
+# periods have passed.
+# Example: slow-timeout = { period = "60s", terminate-after = 2 }
+slow-timeout = { period = "60s" }
+
+# Treat a test as leaky if after the process is shut down, standard output and standard error
+# aren't closed within this duration.
+#
+# This usually happens in case of a test that creates a child process and lets it inherit those
+# handles, but doesn't clean the child process up (especially when it fails).
+#
+# See <https://nexte.st/book/leaky-tests> for more information.
+leak-timeout = "100ms"
+
+[profile.default.junit]
+# Output a JUnit report into the given file inside 'store.dir/<profile-name>'.
+# If unspecified, JUnit is not written out.
+
+# path = "junit.xml"
+
+# The name of the top-level "report" element in JUnit report. If aggregating
+# reports across different test runs, it may be useful to provide separate names
+# for each report.
+report-name = "nextest-run"
+
+# Whether standard output and standard error for passing tests should be stored in the JUnit report.
+# Output is stored in the <system-out> and <system-err> elements of the <testcase> element.
+store-success-output = false
+
+# Whether standard output and standard error for failing tests should be stored in the JUnit report.
+# Output is stored in the <system-out> and <system-err> elements of the <testcase> element.
+#
+# Note that if a description can be extracted from the output, it is always stored in the
+# <description> element.
+store-failure-output = true
+
+# This profile is activated if MIRI_SYSROOT is set.
+[profile.default-miri]
+
+[profile.ci]
+# Retrying at least twice in case it is a memory issue.
+retries = 2
+
+# Print out output for failing tests as soon as they fail, and also at the end
+# of the run (for easy scrollability).
+failure-output = "immediate-final"
+
+# The number of threads to run tests with. Supported values are either an integer or
+# the string "num-cpus". Can be overridden through the `--test-threads` option.
+test-threads = "num-cpus"

.github/workflows/rust.yml

@@ -163,16 +163,19 @@ jobs:
       #
 
       # https://nexte.st/book/pre-built-binaries.html#using-nextest-in-github-actions
-      - name: Install latest nextest release
+      - name: Install nextest 0.9.67
         run: |
           eval $(opam env)
           # FIXME: update to 0.9.68 when we get rid of 1.71 and 1.72.
           cargo install cargo-nextest@=0.9.67 --locked
 
-      - name: Test with latest nextest release (faster than cargo test)
+      # Completeness tests take a lot of CPU/RAM. It happened in the past that
+      # the CI was failing only on some of them, even though they were correct
+      # FIXME: run the completeness tests
+      - name: Test everything, except tests related to completeness
         run: |
           eval $(opam env)
-          cargo nextest run --all-features --release
+          cargo nextest run --all-features --release --profile ci -E "not test(completeness)"
 
       - name: Doc tests
         run: |

ivc/src/ivc/constraints.rs

@@ -267,31 +267,38 @@ where
     // the constraints that are created in the block block_num will have
     // the form selector(block_num)*C(X) and not just C(X).
 
+    let fold_iteration = env.read_column(IVCColumn::FoldIteration);
     let s0 = env.read_column(IVCColumn::BlockSel(0));
-    env.set_assert_mapper(Box::new(move |x| s0.clone() * x));
+    env.set_assert_mapper(Box::new(move |x| fold_iteration.clone() * s0.clone() * x));
     constrain_inputs(env);
 
+    let fold_iteration = env.read_column(IVCColumn::FoldIteration);
+
     let s1 = env.read_column(IVCColumn::BlockSel(1));
-    env.set_assert_mapper(Box::new(move |x| s1.clone() * x));
+    env.set_assert_mapper(Box::new(move |x| fold_iteration.clone() * s1.clone() * x));
     {
         let mut env = SubEnvColumn::new(env, IVCHashLens {});
         poseidon_8_56_5_3_2::interpreter::apply_permutation(&mut env, &PoseidonBN254Parameters);
     }
 
+    let fold_iteration = env.read_column(IVCColumn::FoldIteration);
     let s2 = env.read_column(IVCColumn::BlockSel(2));
-    env.set_assert_mapper(Box::new(move |x| s2.clone() * x));
+    env.set_assert_mapper(Box::new(move |x| fold_iteration.clone() * s2.clone() * x));
     constrain_scalars(env);
 
+    let fold_iteration = env.read_column(IVCColumn::FoldIteration);
     let s3 = env.read_column(IVCColumn::BlockSel(3));
-    env.set_assert_mapper(Box::new(move |x| s3.clone() * x));
+    env.set_assert_mapper(Box::new(move |x| fold_iteration.clone() * s3.clone() * x));
     constrain_ecadds(env);
 
+    let fold_iteration = env.read_column(IVCColumn::FoldIteration);
     let s4 = env.read_column(IVCColumn::BlockSel(4));
-    env.set_assert_mapper(Box::new(move |x| s4.clone() * x));
+    env.set_assert_mapper(Box::new(move |x| fold_iteration.clone() * s4.clone() * x));
     constrain_challenges(env);
 
+    let fold_iteration = env.read_column(IVCColumn::FoldIteration);
     let s5 = env.read_column(IVCColumn::BlockSel(5));
-    env.set_assert_mapper(Box::new(move |x| s5.clone() * x));
+    env.set_assert_mapper(Box::new(move |x| fold_iteration.clone() * s5.clone() * x));
     constrain_u(env);
 
     env.set_assert_mapper(Box::new(move |x| x));

ivc/src/ivc/interpreter.rs

@@ -862,3 +862,27 @@ pub fn ivc_circuit<F, Ff, Env, PParams, const N_COL_TOTAL: usize, const N_CHALS:
     process_challenges::<_, _, N_COL_TOTAL, N_CHALS>(env, fold_iteration, hash_r, &chal_l, r);
     process_u::<_, _, N_COL_TOTAL>(env, fold_iteration, u_l, r);
 }
+
+/// Base case IVC circuit, completely turned off.
+/// For the base case, we do set the fold iteration to 0, and we don't
+/// do any computation.
+/// As each constraint is multiplied by the fold iteration, this will simulate a
+/// "deactivation" of the IVC circuit.
+// FIXME: this is not the final version.
+pub fn ivc_circuit_base_case<F, Env, const N_COL_TOTAL: usize, const N_CHALS: usize>(env: &mut Env)
+where
+    F: PrimeField,
+    Env: DirectWitnessCap<F, IVCColumn> + HybridCopyCap<F, IVCColumn>,
+{
+    // Assuming tables are initialized to zero we don't even have to do this.
+    let fold_iteration = 0;
+    for block_i in 0..N_BLOCKS {
+        for _i in 0..block_height::<N_COL_TOTAL, N_CHALS>(block_i) {
+            env.write_column(
+                IVCColumn::FoldIteration,
+                &Env::constant(F::from(fold_iteration as u64)),
+            );
+            env.next_row();
+        }
+    }
+}

ivc/src/ivc/mod.rs

@@ -76,13 +76,15 @@ mod tests {
         LT,
     >;
 
+    /// Generic IVC circuit builder.
     fn build_ivc_circuit<
         RNG: RngCore + CryptoRng,
         LT: LookupTableID,
         L: MPrism<Source = LT, Target = IVCLookupTable<Ff1>>,
     >(
         rng: &mut RNG,
         domain_size: usize,
+        fold_iteration: usize,
         lt_lens: L,
     ) -> IVCWitnessBuilderEnvRaw<LT> {
         let mut witness_env = IVCWitnessBuilderEnvRaw::<LT>::create();
@@ -127,7 +129,7 @@ mod tests {
         // TODO add nonzero E/T values.
         ivc_circuit::<_, _, _, _, TEST_N_COL_TOTAL, TEST_N_CHALS>(
             &mut SubEnvLookup::new(&mut witness_env, lt_lens),
-            0,
+            fold_iteration,
             comms_left,
             comms_right,
             comms_output,
@@ -147,12 +149,14 @@ mod tests {
     }
 
     #[test]
-    /// Tests if building the IVC circuit succeeds.
-    pub fn test_ivc_circuit() {
+    /// Tests if building the IVC circuit succeeds when using the general case
+    /// (i.e. fold_iteration != 0).
+    pub fn test_ivc_circuit_general_case() {
         let mut rng = o1_utils::tests::make_test_rng(None);
         build_ivc_circuit::<_, IVCLookupTable<Ff1>, _>(
             &mut rng,
             1 << 15,
+            1,
             IdMPrism::<IVCLookupTable<Ff1>>::default(),
         );
     }
@@ -175,24 +179,86 @@ mod tests {
             });
 
             assert_eq!(constraints_degrees.get(&1), None);
-            assert_eq!(constraints_degrees.get(&2), Some(&221));
-            assert_eq!(constraints_degrees.get(&3), Some(&245));
-            assert_eq!(constraints_degrees.get(&4), Some(&21));
+            assert_eq!(constraints_degrees.get(&2), Some(&6));
+            assert_eq!(constraints_degrees.get(&3), Some(&215));
+            assert_eq!(constraints_degrees.get(&4), Some(&245));
+            assert_eq!(constraints_degrees.get(&5), Some(&21));
+
+            // Maximum degree is 5
+            // - fold_iteration increases by one
+            // - the public selectors increase by one
+            assert!(constraints.iter().all(|c| c.degree(1, 0) <= 5));
+        }
+    }
+
+    #[test]
+    /// Completeness test for the IVC circuit in the general case (i.e.
+    /// fold_iteration != 0).
+    fn test_completeness_ivc_general_case() {
+        let fold_iteration = 1;
+
+        let mut rng = o1_utils::tests::make_test_rng(None);
+
+        let domain_size = 1 << 15;
+
+        let witness_env = build_ivc_circuit::<_, IVCLookupTable<Ff1>, _>(
+            &mut rng,
+            domain_size,
+            fold_iteration,
+            IdMPrism::<IVCLookupTable<Ff1>>::default(),
+        );
+        let relation_witness = witness_env.get_relation_witness(domain_size);
+
+        let mut constraint_env = ConstraintBuilderEnv::<Fp, IVCLookupTable<Ff1>>::create();
+        constrain_ivc::<Ff1, _>(&mut constraint_env);
+        let constraints = constraint_env.get_relation_constraints();
+
+        let mut fixed_selectors: Box<[Vec<Fp>; IVC_NB_TOTAL_FIXED_SELECTORS]> = {
+            Box::new(build_selectors::<_, TEST_N_COL_TOTAL, TEST_N_CHALS>(
+                domain_size,
+            ))
+        };
 
-            // Maximum degree is 4
-            assert!(constraints.iter().all(|c| c.degree(1, 0) <= 4));
+        // Write constants
+        {
+            let rc = PoseidonBN254Parameters.constants();
+            rc.iter().enumerate().for_each(|(round, rcs)| {
+                rcs.iter().enumerate().for_each(|(state_index, rc)| {
+                    let rc = vec![*rc; domain_size];
+                    fixed_selectors[N_BLOCKS + round * IVC_POSEIDON_STATE_SIZE + state_index] = rc;
+                });
+            });
         }
+
+        kimchi_msm::test::test_completeness_generic_no_lookups::<
+            { IVCColumn::N_COL - N_BLOCKS },
+            { IVCColumn::N_COL - N_BLOCKS },
+            0,
+            IVC_NB_TOTAL_FIXED_SELECTORS,
+            _,
+        >(
+            constraints,
+            fixed_selectors,
+            relation_witness,
+            domain_size,
+            &mut rng,
+        );
     }
 
     #[test]
-    fn test_completeness_ivc() {
+    /// Completeness test for the IVC circuit in the base case (i.e.
+    /// fold_iteration = 0).
+    fn test_completeness_ivc_base_case() {
+        let fold_iteration = 0;
+
         let mut rng = o1_utils::tests::make_test_rng(None);
 
         let domain_size = 1 << 15;
 
         let witness_env = build_ivc_circuit::<_, IVCLookupTable<Ff1>, _>(
             &mut rng,
             domain_size,
+            fold_iteration,
             IdMPrism::<IVCLookupTable<Ff1>>::default(),
         );
         let relation_witness = witness_env.get_relation_witness(domain_size);

ivc/src/lib.rs

@@ -110,6 +110,21 @@
 //! the execution of all the rounds, and `q_poseidon` will be a (public
 //! selector) that will be set to `1` on the row that Poseidon will need to be
 //! executed, `0` otherwise.
+//!
+//! ## IVC circuit: base case
+//!
+//! The base case of the IVC circuit is supported by multiplying each constraint
+//! by a fold_iteration column. As it is `0` for the base case, the whole
+//! circuit is "turned off".
+//! We do not want to keep this in the final version, and aim to replace it with
+//! a method that does not increase the degree of the constraints by one. The
+//! column value is also under-constrained for now.
+//!
+//! The code for the base case is handled in
+//! [crate::ivc::interpreter::ivc_circuit_base_case] and the corresponding
+//! constraints are in [crate::ivc::constraints::constrain_ivc]. The fold
+//! iteration column is set at each row by each process_* function in the
+//! interpreter.
 
 pub mod ivc;
 /// Poseidon hash function with 55 full rounds, 0 partial rounds, sbox 7, a