feat: implement SuperNova

This implements [Supernova](https://eprint.iacr.org/2022/1758), allowing: - a 'pay-as-you-go' cost structure for folding operations, through the SuperNova folding scheme, - a final SNARK that efficiently compresses an instance of this folded proof, through batching techniques. References: - the [blog post](https://blog.lurk-lang.org/posts/arecibo-supernova/#technical-release-note-supernova-protocol-integration-into-nova) goes into our construction, and links to two more specialized notes on [the `CompressedSNARK` for Supernova](https://hackmd.io/@adr1anh/BJw1g0aBT) along with our variant of the [public input padding issue](https://hackmd.io/@adr1anh/Sy08YaVBa). - the Readme at `src/supernova/Readme.md` This backports the following Arecibo PRs: - argumentcomputer/arecibo#2 - argumentcomputer/arecibo#3 - argumentcomputer/arecibo#10 - argumentcomputer/arecibo#16 - argumentcomputer/arecibo#23 - argumentcomputer/arecibo#30 - argumentcomputer/arecibo#28 - argumentcomputer/arecibo#41 - argumentcomputer/arecibo#45 - argumentcomputer/arecibo#50 - argumentcomputer/arecibo#56 - argumentcomputer/arecibo#51 - argumentcomputer/arecibo#72 - argumentcomputer/arecibo#92 - argumentcomputer/arecibo#95 - argumentcomputer/arecibo#97 - argumentcomputer/arecibo#101 - argumentcomputer/arecibo#110 - argumentcomputer/arecibo#106 - argumentcomputer/arecibo#112 - argumentcomputer/arecibo#114 - argumentcomputer/arecibo#119 - argumentcomputer/arecibo#120 - argumentcomputer/arecibo#127 - argumentcomputer/arecibo#123 - argumentcomputer/arecibo#131 - argumentcomputer/arecibo#174 - argumentcomputer/arecibo#175 - argumentcomputer/arecibo#182 Co-authored-by: WYATT <[email protected]> Co-authored-by: Hanting Zhang <[email protected]> Co-authored-by: Ming <[email protected]> Co-authored-by: porcuquine <[email protected]> Co-authored-by: Samuel Burnham <[email protected]> Co-authored-by: Matej Penciak <[email protected]> Co-authored-by: Adrian Hamelink <[email protected]>
microsoft · Dec 18, 2023 · b56a3eb · b56a3eb
1 parent 0fb0b49
commit b56a3eb
Show file tree

Hide file tree

Showing 38 changed files with 8,138 additions and 572 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -34,7 +34,12 @@ byteorder = "1.4.3"
 thiserror = "1.0"
 halo2curves = { version = "0.4.0", features = ["derive_serde"] }
 group = "0.13.0"
+pairing = "0.23.0"
+tap = "1.0.1"
+cfg-if = "1.0.0"
 once_cell = "1.18.0"
+itertools = "0.12.0"
+log = "0.4.20"
 
 [target.'cfg(any(target_arch = "x86_64", target_arch = "aarch64"))'.dependencies]
 pasta-msm = { version = "0.1.4" }
@@ -48,10 +53,10 @@ criterion = { version = "0.4", features = ["html_reports"] }
 flate2 = "1.0"
 hex = "0.4.3"
 pprof = { version = "0.11" }
-cfg-if = "1.0.0"
+rand = "0.8.5"
 sha2 = "0.10.7"
+tracing-test = "0.2.4"
 proptest = "1.2.0"
-rand = "0.8.5"
 
 [[bench]]
 name = "recursive-snark"
@@ -69,6 +74,14 @@ harness = false
 name = "sha256"
 harness = false
 
+[[bench]]
+name = "recursive-snark-supernova"
+harness = false
+
+[[bench]]
+name = "compressed-snark-supernova"
+harness = false
+
 [features]
 default = []
 asm = ["halo2curves/asm"]

diff --git a/benches/compressed-snark-supernova.rs b/benches/compressed-snark-supernova.rs
@@ -0,0 +1,328 @@
+#![allow(non_snake_case)]
+use nova_snark::{
+  supernova::NonUniformCircuit,
+  supernova::{snark::CompressedSNARK, PublicParams, RecursiveSNARK},
+  traits::{
+    circuit_supernova::{StepCircuit, TrivialTestCircuit},
+    snark::BatchedRelaxedR1CSSNARKTrait,
+    snark::RelaxedR1CSSNARKTrait,
+    Engine,
+  },
+};
+use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError};
+use core::marker::PhantomData;
+use criterion::{measurement::WallTime, *};
+use ff::PrimeField;
+use std::time::Duration;
+
+type E1 = nova_snark::provider::PallasEngine;
+type E2 = nova_snark::provider::VestaEngine;
+type EE1 = nova_snark::provider::ipa_pc::EvaluationEngine<E1>;
+type EE2 = nova_snark::provider::ipa_pc::EvaluationEngine<E2>;
+// SNARKs without computation commitmnets
+type S1 = nova_snark::spartan::batched::BatchedRelaxedR1CSSNARK<E1, EE1>;
+type S2 = nova_snark::spartan::snark::RelaxedR1CSSNARK<E2, EE2>;
+// SNARKs with computation commitmnets
+type SS1 = nova_snark::spartan::batched_ppsnark::BatchedRelaxedR1CSSNARK<E1, EE1>;
+type SS2 = nova_snark::spartan::ppsnark::RelaxedR1CSSNARK<E2, EE2>;
+
+// To run these benchmarks, first download `criterion` with `cargo install cargo-criterion`.
+// Then `cargo criterion --bench compressed-snark-supernova`. The results are located in `target/criterion/data/<name-of-benchmark>`.
+// For flamegraphs, run `cargo criterion --bench compressed-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 = compressed_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_compressed_snark, bench_two_augmented_circuit_compressed_snark, bench_two_augmented_circuit_compressed_snark_with_computational_commitments
+    }
+  } else {
+    criterion_group! {
+      name = compressed_snark_supernova;
+      config = Criterion::default().warm_up_time(Duration::from_millis(3000));
+      targets = bench_one_augmented_circuit_compressed_snark, bench_two_augmented_circuit_compressed_snark, bench_two_augmented_circuit_compressed_snark_with_computational_commitments
+    }
+  }
+}
+
+criterion_main!(compressed_snark_supernova);
+
+// This should match the value in test_supernova_recursive_circuit_pasta
+// TODO: This should also be a table matching the num_augmented_circuits in the below
+const NUM_CONS_VERIFIER_CIRCUIT_PRIMARY: usize = 9844;
+const NUM_SAMPLES: usize = 10;
+
+struct NonUniformBench<E1, E2, S>
+where
+  E1: Engine<Base = <E2 as Engine>::Scalar>,
+  E2: Engine<Base = <E1 as Engine>::Scalar>,
+  S: StepCircuit<E2::Scalar> + Default,
+{
+  num_circuits: usize,
+  num_cons: usize,
+  _p: PhantomData<(E1, E2, S)>,
+}
+
+impl<E1, E2, S> NonUniformBench<E1, E2, S>
+where
+  E1: Engine<Base = <E2 as Engine>::Scalar>,
+  E2: Engine<Base = <E1 as Engine>::Scalar>,
+  S: StepCircuit<E2::Scalar> + Default,
+{
+  fn new(num_circuits: usize, num_cons: usize) -> Self {
+    Self {
+      num_circuits,
+      num_cons,
+      _p: Default::default(),
+    }
+  }
+}
+
+impl<E1, E2, S>
+  NonUniformCircuit<E1, E2, NonTrivialTestCircuit<E1::Scalar>, TrivialTestCircuit<E2::Scalar>>
+  for NonUniformBench<E1, E2, S>
+where
+  E1: Engine<Base = <E2 as Engine>::Scalar>,
+  E2: Engine<Base = <E1 as Engine>::Scalar>,
+  S: StepCircuit<E2::Scalar> + Default,
+{
+  fn num_circuits(&self) -> usize {
+    self.num_circuits
+  }
+
+  fn primary_circuit(&self, circuit_index: usize) -> NonTrivialTestCircuit<E1::Scalar> {
+    assert!(
+      circuit_index < self.num_circuits,
+      "Circuit index out of bounds: asked for {circuit_index}, but there are only {} circuits.",
+      self.num_circuits
+    );
+
+    NonTrivialTestCircuit::new(self.num_cons)
+  }
+
+  fn secondary_circuit(&self) -> TrivialTestCircuit<E2::Scalar> {
+    Default::default()
+  }
+}
+
+/// Benchmarks the compressed SNARK at a provided number of constraints
+///
+/// Parameters
+/// - `num_augmented_circuits`: the number of augmented circuits in this configuration
+/// - `group`: the criterion benchmark group
+/// - `num_cons`: the number of constraints in the step circuit
+fn bench_compressed_snark_internal_with_arity<
+  S1: BatchedRelaxedR1CSSNARKTrait<E1>,
+  S2: RelaxedR1CSSNARKTrait<E2>,
+>(
+  group: &mut BenchmarkGroup<'_, WallTime>,
+  num_augmented_circuits: usize,
+  num_cons: usize,
+) {
+  let bench: NonUniformBench<E1, E2, TrivialTestCircuit<<E2 as Engine>::Scalar>> =
+    NonUniformBench::new(num_augmented_circuits, num_cons);
+  let pp = PublicParams::setup(&bench, &*S1::ck_floor(), &*S2::ck_floor());
+
+  let num_steps = 3;
+  let z0_primary = vec![<E1 as Engine>::Scalar::from(2u64)];
+  let z0_secondary = vec![<E2 as Engine>::Scalar::from(2u64)];
+  let mut recursive_snark_option: Option<RecursiveSNARK<E1, E2>> = None;
+  let mut selected_augmented_circuit = 0;
+
+  for _ in 0..num_steps {
+    let mut recursive_snark = recursive_snark_option.unwrap_or_else(|| {
+      RecursiveSNARK::new(
+        &pp,
+        &bench,
+        &bench.primary_circuit(0),
+        &bench.secondary_circuit(),
+        &z0_primary,
+        &z0_secondary,
+      )
+      .unwrap()
+    });
+
+    if selected_augmented_circuit == 0 || selected_augmented_circuit == 1 {
+      let res = recursive_snark.prove_step(
+        &pp,
+        &bench.primary_circuit(selected_augmented_circuit),
+        &bench.secondary_circuit(),
+      );
+      res.expect("Prove step failed");
+
+      let res = recursive_snark.verify(&pp, &z0_primary, &z0_secondary);
+      res.expect("Verify failed");
+    } else {
+      unimplemented!()
+    }
+
+    selected_augmented_circuit = (selected_augmented_circuit + 1) % num_augmented_circuits;
+    recursive_snark_option = Some(recursive_snark)
+  }
+
+  assert!(recursive_snark_option.is_some());
+  let recursive_snark = recursive_snark_option.unwrap();
+
+  let (prover_key, verifier_key) = CompressedSNARK::<_, _, _, _, S1, S2>::setup(&pp).unwrap();
+
+  // Benchmark the prove time
+  group.bench_function("Prove", |b| {
+    b.iter(|| {
+      assert!(CompressedSNARK::<_, _, _, _, S1, S2>::prove(
+        black_box(&pp),
+        black_box(&prover_key),
+        black_box(&recursive_snark)
+      )
+      .is_ok());
+    })
+  });
+
+  let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &prover_key, &recursive_snark);
+
+  assert!(res.is_ok());
+  let compressed_snark = res.unwrap();
+
+  // Benchmark the verification time
+  group.bench_function("Verify", |b| {
+    b.iter(|| {
+      assert!(black_box(&compressed_snark)
+        .verify(
+          black_box(&pp),
+          black_box(&verifier_key),
+          black_box(&z0_primary),
+          black_box(&z0_secondary),
+        )
+        .is_ok());
+    })
+  });
+}
+
+fn bench_one_augmented_circuit_compressed_snark(c: &mut Criterion) {
+  // we vary the number of constraints in the step circuit
+  for &num_cons_in_augmented_circuit in [
+    NUM_CONS_VERIFIER_CIRCUIT_PRIMARY,
+    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!(
+      "CompressedSNARKSuperNova-1circuit-StepCircuitSize-{num_cons}"
+    ));
+    group.sample_size(NUM_SAMPLES);
+
+    bench_compressed_snark_internal_with_arity::<S1, S2>(&mut group, 1, num_cons);
+
+    group.finish();
+  }
+}
+
+fn bench_two_augmented_circuit_compressed_snark(c: &mut Criterion) {
+  // we vary the number of constraints in the step circuit
+  for &num_cons_in_augmented_circuit in [
+    NUM_CONS_VERIFIER_CIRCUIT_PRIMARY,
+    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!(
+      "CompressedSNARKSuperNova-2circuit-StepCircuitSize-{num_cons}"
+    ));
+    group.sample_size(NUM_SAMPLES);
+
+    bench_compressed_snark_internal_with_arity::<S1, S2>(&mut group, 2, num_cons);
+
+    group.finish();
+  }
+}
+
+fn bench_two_augmented_circuit_compressed_snark_with_computational_commitments(c: &mut Criterion) {
+  // we vary the number of constraints in the step circuit
+  for &num_cons_in_augmented_circuit in [
+    NUM_CONS_VERIFIER_CIRCUIT_PRIMARY,
+    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!(
+      "CompressedSNARKSuperNova-Commitments-2circuit-StepCircuitSize-{num_cons}"
+    ));
+    group.sample_size(NUM_SAMPLES);
+
+    bench_compressed_snark_internal_with_arity::<SS1, SS2>(&mut group, 2, num_cons);
+
+    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 circuit_index(&self) -> usize {
+    0
+  }
+
+  fn synthesize<CS: ConstraintSystem<F>>(
+    &self,
+    cs: &mut CS,
+    pc: Option<&AllocatedNum<F>>,
+    z: &[AllocatedNum<F>],
+  ) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedNum<F>>), SynthesisError> {
+    // Consider a an equation: `x^{2 * num_cons} = 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.cloned(), vec![y]))
+  }
+}
diff --git a/benches/compressed-snark.rs b/benches/compressed-snark.rs
@@ -19,10 +19,10 @@ type E1 = PallasEngine;
 type E2 = VestaEngine;
 type EE1 = nova_snark::provider::ipa_pc::EvaluationEngine<E1>;
 type EE2 = nova_snark::provider::ipa_pc::EvaluationEngine<E2>;
-// SNARKs without computational commitments
+// SNARKs without computation commitmnets
 type S1 = nova_snark::spartan::snark::RelaxedR1CSSNARK<E1, EE1>;
 type S2 = nova_snark::spartan::snark::RelaxedR1CSSNARK<E2, EE2>;
-// SNARKs with computational commitments
+// SNARKs with computation commitmnets
 type SS1 = nova_snark::spartan::ppsnark::RelaxedR1CSSNARK<E1, EE1>;
 type SS2 = nova_snark::spartan::ppsnark::RelaxedR1CSSNARK<E2, EE2>;
 type C1 = NonTrivialCircuit<<E1 as Engine>::Scalar>;