incubating supernova (#2)

* start SuperNova

* setup unit test and start program counter

* experimenting with the RunningClaims selector.

* start conversion of RecursiveSNARK into NivcSnark

* theta function needs to be defined. Starting from public param generator.

* RunningClaims will be a user provide Struct.

* moving CK out

* setup public params in a nice way for SuperNova.

* starting on phi logic

* adding pci into code

* move cks out and also start on U_i and pki as described in paper.

* Start on SuperNova augmented circuit

* work on augmented circuit2

* testing pci as output

* closer to pci fin

* push notes

* more details and analysis of implementation method.

* change to match paper

* clarified wording

* leave write up for review.

* typo

* clarity

* inputize progam_counter

* start on hash of U_i

* swapping wording out for hash of Fpci' pre-image

* testing U_i constraints

* need to rethink how U_i works in the circuit. Might just be a hash.

* decided on how to represent the running instance U_i in the cicruits.

* change to U_i is preset amount of circuits.

* refactor

* got output of hash supernova from circuit

* add new X2 for supernova_hash. All tests are a GO!

* prep for SuperNova circuit sequence checking

* generics for circuit passing

* cleanup

* verify supernova step

* add supernova hash witness check

* cleanup and bug fix

* add Makefile

* fix bugs and cleanup generics

* compile pass but test failed due to shape mismatch

* refactor to fit supernova implementation

* introduce rom concept

* constrain sequence execution by memory commitment

* rom access commitment: program counter manipulation by step circuit

* code cleanup

* constrain pc[i]=z_i[x] in step circuit as well

* remove number of arguments circuit constraint

* adapt latest main

* reuse nova nicv::prove for supernova

* reuse nova runninginstance for supernova

* more util function to serve supernova

* disable supernova by default

* error pruning: arity length check in synthesis function

* primary circuit folding can be single element

* optimise supernova proof size from 2*relax_rc1s to relax_rc1s + 1

* code cosmetics

* cleanup and reuse compute_digest, fix typo

* variable rename and cleanup some leftover

* better naming and cleanup

* proper naming on r1cs_shape

* opt memory usage, remove unnessesary clone trait

* docs decoration

* isolated trait/lib for supernova

* expose supernova module public

* refactor and reuse most of reference

* optimize pc handling in step circuit, opt running instance clone

* fix comment format

* retain constraint in Nova to narrow down the scope

* clean up comment

* add supernova bench

* almost all passed by reference in supernova recursivesnark

* supernova soundness and clippy fix

* fix groupname in supernova bench

* chores: polish reference usage in prove step

* fix bug in recursive snark base case for only success on first running claim

* simplify synthesis error handling

* supernova align naming convention with nova

* fix soundness in supernova sequence constraints

* code cosmetics based on review comments

* optimise util alloc_const and supernova usage

* code cosmetics and clean up

* optimize with less constriants, following-up fixing soundness on const index

* eliminate program_counter from secondary circuit ro, better error handling

* typo fix

* supernova refactor test to separate mod

* clean up UnSatMsg from Nova error

* fix soundness: empty running instance under-constraint

* refactor circuit test to test module

* code cosmetics

* fix soundness: use last_augmented_circuit_index consistently

---------

Co-authored-by: WYATT <[email protected]>

Cargo.toml

@@ -34,6 +34,7 @@ byteorder = "1.4.3"
 thiserror = "1.0"
 halo2curves = { version = "0.4.0", features = ["derive_serde"] }
 group = "0.13.0"
+log = "0.4.17"
 abomonation = "0.7.3"
 abomonation_derive = { git = "https://github.com/winston-h-zhang/abomonation_derive.git" }
 
@@ -70,13 +71,19 @@ harness = false
 name = "sha256"
 harness = false
 
+[[bench]]
+name = "recursive-snark-supernova"
+harness = false
+required-features = ["supernova"]
+
 [features]
 default = []
 # Compiles in portable mode, w/o ISA extensions => binary can be executed on all systems.
 portable = ["pasta-msm/portable"]
 cuda = ["neptune/cuda", "neptune/pasta", "neptune/arity24"]
 opencl = ["neptune/opencl", "neptune/pasta", "neptune/arity24"]
 flamegraph = ["pprof/flamegraph", "pprof/criterion"]
+supernova = []
 
 # This is needed to ensure halo2curves, which imports pasta-curves, uses the *same* traits in bn256_grumpkin
 [patch.crates-io]

benches/recursive-snark-supernova.rs

@@ -0,0 +1,329 @@
+#![allow(non_snake_case)]
+
+use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError};
+use core::marker::PhantomData;
+use criterion::*;
+use ff::PrimeField;
+use nova_snark::{
+  compute_digest,
+  supernova::RecursiveSNARK,
+  supernova::{gen_commitmentkey_by_r1cs, PublicParams, RunningClaim},
+  traits::{
+    circuit_supernova::{StepCircuit, TrivialTestCircuit},
+    Group,
+  },
+};
+use std::time::Duration;
+
+type G1 = pasta_curves::pallas::Point;
+type G2 = pasta_curves::vesta::Point;
+
+// To run these benchmarks, first download `criterion` with `cargo install cargo-criterion`.
+// Then `cargo criterion --bench recursive-snark-supernova`. The results are located in `target/criterion/data/<name-of-benchmark>`.
+// For flamegraphs, run `cargo criterion --bench recursive-snark-supernova --features flamegraph -- --profile-time <secs>`.
+// The results are located in `target/criterion/profile/<name-of-benchmark>`.
+cfg_if::cfg_if! {
+  if #[cfg(feature = "flamegraph")] {
+    criterion_group! {
+      name = recursive_snark_supernova;
+      config = Criterion::default().warm_up_time(Duration::from_millis(3000)).with_profiler(pprof::criterion::PProfProfiler::new(100, pprof::criterion::Output::Flamegraph(None)));
+      targets = bench_one_augmented_circuit_recursive_snark, bench_two_augmented_circuit_recursive_snark
+    }
+  } else {
+    criterion_group! {
+      name = recursive_snark_supernova;
+      config = Criterion::default().warm_up_time(Duration::from_millis(3000));
+      targets = bench_one_augmented_circuit_recursive_snark, bench_two_augmented_circuit_recursive_snark
+    }
+  }
+}
+
+criterion_main!(recursive_snark_supernova);
+
+fn bench_one_augmented_circuit_recursive_snark(c: &mut Criterion) {
+  let num_cons_verifier_circuit_primary = 9819;
+  // we vary the number of constraints in the step circuit
+  for &num_cons_in_augmented_circuit in
+    [9819, 16384, 32768, 65536, 131072, 262144, 524288, 1048576].iter()
+  {
+    // number of constraints in the step circuit
+    let num_cons = num_cons_in_augmented_circuit - num_cons_verifier_circuit_primary;
+
+    let mut group = c.benchmark_group(format!(
+      "RecursiveSNARKSuperNova-1circuit-StepCircuitSize-{num_cons}"
+    ));
+    group.sample_size(10);
+
+    let c_primary = NonTrivialTestCircuit::new(num_cons);
+    let c_secondary = TrivialTestCircuit::default();
+
+    // Structuring running claims
+    let mut running_claim1 = RunningClaim::<
+      G1,
+      G2,
+      NonTrivialTestCircuit<<G1 as Group>::Scalar>,
+      TrivialTestCircuit<<G2 as Group>::Scalar>,
+    >::new(0, c_primary, c_secondary.clone(), 1);
+
+    let (r1cs_shape_primary, r1cs_shape_secondary) = running_claim1.get_r1cs_shape();
+    let ck_primary = gen_commitmentkey_by_r1cs(r1cs_shape_primary);
+    let ck_secondary = gen_commitmentkey_by_r1cs(r1cs_shape_secondary);
+
+    // set unified ck_primary, ck_secondary and update digest
+    running_claim1.set_commitmentkey(ck_primary.clone(), ck_secondary.clone());
+    let digest = compute_digest::<G1, PublicParams<G1, G2>>(&[running_claim1.get_publicparams()]);
+
+    // Bench time to produce a recursive SNARK;
+    // we execute a certain number of warm-up steps since executing
+    // the first step is cheaper than other steps owing to the presence of
+    // a lot of zeros in the satisfying assignment
+    let num_warmup_steps = 10;
+    let z0_primary = vec![<G1 as Group>::Scalar::from(2u64)];
+    let z0_secondary = vec![<G2 as Group>::Scalar::from(2u64)];
+    let initial_program_counter = <G1 as Group>::Scalar::from(0);
+    let mut recursive_snark_option: Option<RecursiveSNARK<G1, G2>> = None;
+
+    for _ in 0..num_warmup_steps {
+      let program_counter = recursive_snark_option
+        .as_ref()
+        .map(|recursive_snark| recursive_snark.get_program_counter())
+        .unwrap_or_else(|| initial_program_counter);
+
+      let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| {
+        RecursiveSNARK::iter_base_step(
+          &running_claim1,
+          digest,
+          program_counter,
+          0,
+          1,
+          &z0_primary,
+          &z0_secondary,
+        )
+        .unwrap()
+      });
+
+      let res = recursive_snark.prove_step(&running_claim1, &z0_primary, &z0_secondary);
+      if let Err(e) = &res {
+        println!("res failed {:?}", e);
+      }
+      assert!(res.is_ok());
+      let res = recursive_snark.verify(&running_claim1, &z0_primary, &z0_secondary);
+      if let Err(e) = &res {
+        println!("res failed {:?}", e);
+      }
+      assert!(res.is_ok());
+      recursive_snark_option = Some(recursive_snark)
+    }
+
+    assert!(recursive_snark_option.is_some());
+    let recursive_snark = recursive_snark_option.unwrap();
+
+    // Benchmark the prove time
+    group.bench_function("Prove", |b| {
+      b.iter(|| {
+        // produce a recursive SNARK for a step of the recursion
+        assert!(black_box(&mut recursive_snark.clone())
+          .prove_step(
+            black_box(&running_claim1),
+            black_box(&[<G1 as Group>::Scalar::from(2u64)]),
+            black_box(&[<G2 as Group>::Scalar::from(2u64)]),
+          )
+          .is_ok());
+      })
+    });
+
+    // Benchmark the verification time
+    group.bench_function("Verify", |b| {
+      b.iter(|| {
+        assert!(black_box(&mut recursive_snark.clone())
+          .verify(
+            black_box(&running_claim1),
+            black_box(&[<G1 as Group>::Scalar::from(2u64)]),
+            black_box(&[<G2 as Group>::Scalar::from(2u64)]),
+          )
+          .is_ok());
+      });
+    });
+    group.finish();
+  }
+}
+
+fn bench_two_augmented_circuit_recursive_snark(c: &mut Criterion) {
+  let num_cons_verifier_circuit_primary = 9819;
+  // we vary the number of constraints in the step circuit
+  for &num_cons_in_augmented_circuit in
+    [9819, 16384, 32768, 65536, 131072, 262144, 524288, 1048576].iter()
+  {
+    // number of constraints in the step circuit
+    let num_cons = num_cons_in_augmented_circuit - num_cons_verifier_circuit_primary;
+
+    let mut group = c.benchmark_group(format!(
+      "RecursiveSNARKSuperNova-2circuit-StepCircuitSize-{num_cons}"
+    ));
+    group.sample_size(10);
+
+    let c_primary = NonTrivialTestCircuit::new(num_cons);
+    let c_secondary = TrivialTestCircuit::default();
+
+    // Structuring running claims
+    let mut running_claim1 = RunningClaim::<
+      G1,
+      G2,
+      NonTrivialTestCircuit<<G1 as Group>::Scalar>,
+      TrivialTestCircuit<<G2 as Group>::Scalar>,
+    >::new(0, c_primary.clone(), c_secondary.clone(), 2);
+
+    // Structuring running claims
+    let mut running_claim2 = RunningClaim::<
+      G1,
+      G2,
+      NonTrivialTestCircuit<<G1 as Group>::Scalar>,
+      TrivialTestCircuit<<G2 as Group>::Scalar>,
+    >::new(1, c_primary, c_secondary.clone(), 2);
+
+    let (r1cs_shape_primary, r1cs_shape_secondary) = running_claim1.get_r1cs_shape();
+    let ck_primary = gen_commitmentkey_by_r1cs(r1cs_shape_primary);
+    let ck_secondary = gen_commitmentkey_by_r1cs(r1cs_shape_secondary);
+
+    // set unified ck_primary, ck_secondary and update digest
+    running_claim1.set_commitmentkey(ck_primary.clone(), ck_secondary.clone());
+    running_claim2.set_commitmentkey(ck_primary.clone(), ck_secondary.clone());
+
+    let digest = compute_digest::<G1, PublicParams<G1, G2>>(&[
+      running_claim1.get_publicparams(),
+      running_claim2.get_publicparams(),
+    ]);
+
+    // Bench time to produce a recursive SNARK;
+    // we execute a certain number of warm-up steps since executing
+    // the first step is cheaper than other steps owing to the presence of
+    // a lot of zeros in the satisfying assignment
+    let num_warmup_steps = 10;
+    let z0_primary = vec![<G1 as Group>::Scalar::from(2u64)];
+    let z0_secondary = vec![<G2 as Group>::Scalar::from(2u64)];
+    let initial_program_counter = <G1 as Group>::Scalar::from(0);
+    let mut recursive_snark_option: Option<RecursiveSNARK<G1, G2>> = None;
+    let mut selected_augmented_circuit = 0;
+
+    for _ in 0..num_warmup_steps {
+      let program_counter = recursive_snark_option
+        .as_ref()
+        .map(|recursive_snark| recursive_snark.get_program_counter())
+        .unwrap_or_else(|| initial_program_counter);
+
+      let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| {
+        RecursiveSNARK::iter_base_step(
+          &running_claim1,
+          digest,
+          program_counter,
+          0,
+          2,
+          &z0_primary,
+          &z0_secondary,
+        )
+        .unwrap()
+      });
+
+      if selected_augmented_circuit == 0 {
+        let res = recursive_snark.prove_step(&running_claim1, &z0_primary, &z0_secondary);
+        if let Err(e) = &res {
+          println!("res failed {:?}", e);
+        }
+        assert!(res.is_ok());
+        let res = recursive_snark.verify(&running_claim1, &z0_primary, &z0_secondary);
+        if let Err(e) = &res {
+          println!("res failed {:?}", e);
+        }
+        assert!(res.is_ok());
+      } else if selected_augmented_circuit == 1 {
+        let res = recursive_snark.prove_step(&running_claim2, &z0_primary, &z0_secondary);
+        if let Err(e) = &res {
+          println!("res failed {:?}", e);
+        }
+        assert!(res.is_ok());
+        let res = recursive_snark.verify(&running_claim2, &z0_primary, &z0_secondary);
+        if let Err(e) = &res {
+          println!("res failed {:?}", e);
+        }
+        assert!(res.is_ok());
+      } else {
+        unimplemented!()
+      }
+      selected_augmented_circuit = (selected_augmented_circuit + 1) % 2;
+      recursive_snark_option = Some(recursive_snark)
+    }
+
+    assert!(recursive_snark_option.is_some());
+    let recursive_snark = recursive_snark_option.unwrap();
+
+    // Benchmark the prove time
+    group.bench_function("Prove", |b| {
+      b.iter(|| {
+        // produce a recursive SNARK for a step of the recursion
+        assert!(black_box(&mut recursive_snark.clone())
+          .prove_step(
+            black_box(&running_claim1),
+            black_box(&[<G1 as Group>::Scalar::from(2u64)]),
+            black_box(&[<G2 as Group>::Scalar::from(2u64)]),
+          )
+          .is_ok());
+      })
+    });
+
+    // Benchmark the verification time
+    group.bench_function("Verify", |b| {
+      b.iter(|| {
+        assert!(black_box(&mut recursive_snark.clone())
+          .verify(
+            black_box(&running_claim1),
+            black_box(&[<G1 as Group>::Scalar::from(2u64)]),
+            black_box(&[<G2 as Group>::Scalar::from(2u64)]),
+          )
+          .is_ok());
+      });
+    });
+    group.finish();
+  }
+}
+
+#[derive(Clone, Debug, Default)]
+struct NonTrivialTestCircuit<F: PrimeField> {
+  num_cons: usize,
+  _p: PhantomData<F>,
+}
+
+impl<F> NonTrivialTestCircuit<F>
+where
+  F: PrimeField,
+{
+  pub fn new(num_cons: usize) -> Self {
+    Self {
+      num_cons,
+      _p: Default::default(),
+    }
+  }
+}
+impl<F> StepCircuit<F> for NonTrivialTestCircuit<F>
+where
+  F: PrimeField,
+{
+  fn arity(&self) -> usize {
+    1
+  }
+
+  fn synthesize<CS: ConstraintSystem<F>>(
+    &self,
+    cs: &mut CS,
+    pc: &AllocatedNum<F>,
+    z: &[AllocatedNum<F>],
+  ) -> Result<(AllocatedNum<F>, Vec<AllocatedNum<F>>), SynthesisError> {
+    // Consider a an equation: `x^2 = y`, where `x` and `y` are respectively the input and output.
+    let mut x = z[0].clone();
+    let mut y = x.clone();
+    for i in 0..self.num_cons {
+      y = x.square(cs.namespace(|| format!("x_sq_{i}")))?;
+      x = y.clone();
+    }
+    Ok((pc.clone(), vec![y]))
+  }
+}

src/bellpepper/mod.rs

@@ -50,7 +50,7 @@ mod tests {
     // First create the shape
     let mut cs: ShapeCS<G> = ShapeCS::new();
     let _ = synthesize_alloc_bit(&mut cs);
-    let (shape, ck) = cs.r1cs_shape();
+    let (shape, ck) = cs.r1cs_shape_with_commitmentkey();
 
     // Now get the assignment
     let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();