(Easy) Supernova feedback (#235)

* fix: rename CircuitShape -> R1CSWithArity

* fix:typos

* chore: make the typos tool usable

* fix: move traits::circuit_supernova inside supernova::circuit

_typos.toml

@@ -0,0 +1,5 @@
+[default]
+extend-ignore-identifiers-re = [
+    # *sigh* this is load-bearing
+    "[Aa]bomonation",
+]

benches/compressed-snark-supernova.rs

@@ -2,12 +2,8 @@
 use arecibo::{
   supernova::NonUniformCircuit,
   supernova::{snark::CompressedSNARK, PublicParams, RecursiveSNARK},
-  traits::{
-    circuit_supernova::{StepCircuit, TrivialTestCircuit},
-    snark::BatchedRelaxedR1CSSNARKTrait,
-    snark::RelaxedR1CSSNARKTrait,
-    Engine,
-  },
+  supernova::{StepCircuit, TrivialTestCircuit},
+  traits::{snark::BatchedRelaxedR1CSSNARKTrait, snark::RelaxedR1CSSNARKTrait, Engine},
 };
 use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError};
 use core::marker::PhantomData;

benches/recursive-snark-supernova.rs

@@ -3,11 +3,8 @@ use arecibo::{
   provider::{PallasEngine, VestaEngine},
   supernova::NonUniformCircuit,
   supernova::{PublicParams, RecursiveSNARK},
-  traits::{
-    circuit_supernova::{StepCircuit, TrivialTestCircuit},
-    snark::default_ck_hint,
-    Engine,
-  },
+  supernova::{StepCircuit, TrivialTestCircuit},
+  traits::{snark::default_ck_hint, Engine},
 };
 use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError};
 use core::marker::PhantomData;

src/lib.rs

@@ -63,14 +63,14 @@ use traits::{
 #[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Abomonation)]
 #[serde(bound = "")]
 #[abomonation_bounds(where <E::Scalar as PrimeField>::Repr: Abomonation)]
-pub struct CircuitShape<E: Engine> {
+pub struct R1CSWithArity<E: Engine> {
   F_arity: usize,
   r1cs_shape: R1CSShape<E>,
 }
 
-impl<E: Engine> SimpleDigestible for CircuitShape<E> {}
+impl<E: Engine> SimpleDigestible for R1CSWithArity<E> {}
 
-impl<E: Engine> CircuitShape<E> {
+impl<E: Engine> R1CSWithArity<E> {
   /// Create a new `CircuitShape`
   pub fn new(r1cs_shape: R1CSShape<E>, F_arity: usize) -> Self {
     Self {
@@ -110,11 +110,11 @@ where
   ro_consts_primary: ROConstants<E1>,
   ro_consts_circuit_primary: ROConstantsCircuit<E2>,
   ck_primary: CommitmentKey<E1>,
-  circuit_shape_primary: CircuitShape<E1>,
+  circuit_shape_primary: R1CSWithArity<E1>,
   ro_consts_secondary: ROConstants<E2>,
   ro_consts_circuit_secondary: ROConstantsCircuit<E1>,
   ck_secondary: CommitmentKey<E2>,
-  circuit_shape_secondary: CircuitShape<E2>,
+  circuit_shape_secondary: R1CSWithArity<E2>,
   augmented_circuit_params_primary: NovaAugmentedCircuitParams,
   augmented_circuit_params_secondary: NovaAugmentedCircuitParams,
   #[abomonation_skip]
@@ -213,7 +213,7 @@ where
     let mut cs: ShapeCS<E1> = ShapeCS::new();
     let _ = circuit_primary.synthesize(&mut cs);
     let (r1cs_shape_primary, ck_primary) = cs.r1cs_shape_and_key(ck_hint1);
-    let circuit_shape_primary = CircuitShape::new(r1cs_shape_primary, F_arity_primary);
+    let circuit_shape_primary = R1CSWithArity::new(r1cs_shape_primary, F_arity_primary);
 
     // Initialize ck for the secondary
     let circuit_secondary: NovaAugmentedCircuit<'_, E1, C2> = NovaAugmentedCircuit::new(
@@ -225,7 +225,7 @@ where
     let mut cs: ShapeCS<E2> = ShapeCS::new();
     let _ = circuit_secondary.synthesize(&mut cs);
     let (r1cs_shape_secondary, ck_secondary) = cs.r1cs_shape_and_key(ck_hint2);
-    let circuit_shape_secondary = CircuitShape::new(r1cs_shape_secondary, F_arity_secondary);
+    let circuit_shape_secondary = R1CSWithArity::new(r1cs_shape_secondary, F_arity_secondary);
 
     Self {
       F_arity_primary,

src/spartan/macros.rs

@@ -1,4 +1,4 @@
-/// Macros to give syntactic sugar for zipWith pattern and variatns.
+/// Macros to give syntactic sugar for zipWith pattern and variants.
 ///
 /// ```ignore
 /// use crate::spartan::zip_with;

src/supernova/Readme.md

@@ -257,8 +257,8 @@ This branch returns $U\_{i+1}[\ ]$, $b\_{X_0}$ as well as the selector $s$.
 If $i \equiv 0$, then the verification circuit must instantiate the inputs as their defaults.
 Namely, it initializes a list $U_0[\ ]$ (different from the input list which is given to the previous branch) with "empty instances" (all group elements are set to the identity).
 
-The ouptut list of instances $U_1[\ ]$ is
-- **Primary curve**: the incomming proof $u$ is trivial, so the result of folding two trivial instances is defined as the trivial relaxed instance.
+The output list of instances $U_1[\ ]$ is
+- **Primary curve**: the incoming proof $u$ is trivial, so the result of folding two trivial instances is defined as the trivial relaxed instance.
 - **Secondary curve**: the instance $U_0[\mathsf{pc}']$ is simply replaced with the relaxation of $u$ using conditional selection.
 
 This branch returns $U_1[\ ]$.
@@ -312,7 +312,7 @@ We then verify that $(u',w')$ is a satisfying circuit, which proves that all rel
 
 We then need to verify that all accumulators $(U[\ ], W[\ ])$ and $(U', W')$ are correct by checking the circuit satisfiability.
 
-## Comparsion of Nova and SuperNova
+## Comparison of Nova and SuperNova
 
 |                                  |         Nova          |          SuperNova           |
 | -------------------------------- | --------------------- | ---------------------------- |

src/supernova/circuit.rs

@@ -1,4 +1,4 @@
-//! Supernova implemetation support arbitrary argumented circuits and running instances.
+//! Supernova implementation support arbitrary argumented circuits and running instances.
 //! There are two Verification Circuits for each argumented circuit: The primary and the secondary.
 //! Each of them is over a Pasta curve but
 //! only the primary executes the next step of the computation.
@@ -11,7 +11,6 @@
 //!    2. R1CS Instance u is folded into Ui[augmented_circuit_index] correctly; just like Nova IVC.
 //!    3. (optional by F logic) F circuit might check `program_counter_{i}` invoked current F circuit is legal or not.
 //!    3. F circuit produce `program_counter_{i+1}` and sent to next round for optionally constraint the next F' argumented circuit.
-
 use crate::{
   constants::NUM_HASH_BITS,
   gadgets::{
@@ -26,10 +25,7 @@ use crate::{
     },
   },
   r1cs::{R1CSInstance, RelaxedR1CSInstance},
-  traits::{
-    circuit_supernova::EnforcingStepCircuit, commitment::CommitmentTrait, Engine, ROCircuitTrait,
-    ROConstantsCircuit,
-  },
+  traits::{commitment::CommitmentTrait, Engine, ROCircuitTrait, ROConstantsCircuit},
   Commitment,
 };
 use bellpepper_core::{
@@ -41,15 +37,127 @@ use bellpepper_core::{
 use bellpepper::gadgets::Assignment;
 
 use abomonation_derive::Abomonation;
-use ff::Field;
+use ff::{Field, PrimeField};
 use itertools::Itertools as _;
 use serde::{Deserialize, Serialize};
+use std::marker::PhantomData;
 
 use crate::supernova::{
   num_ro_inputs,
   utils::{get_from_vec_alloc_relaxed_r1cs, get_selector_vec_from_index},
 };
 
+/// A helper trait for a step of the incremental computation for `SuperNova` (i.e., circuit for F) -- to be implemented by
+/// applications.
+pub trait StepCircuit<F: PrimeField>: Send + Sync + Clone {
+  /// Return the the number of inputs or outputs of each step
+  /// (this method is called only at circuit synthesis time)
+  /// `synthesize` and `output` methods are expected to take as
+  /// input a vector of size equal to arity and output a vector of size equal to arity
+  fn arity(&self) -> usize;
+
+  /// Return this `StepCircuit`'s assigned index, for use when enforcing the program counter.
+  fn circuit_index(&self) -> usize;
+
+  /// Synthesize the circuit for a computation step and return variable
+  /// that corresponds to the output of the step `pc_{i+1}` and `z_{i+1}`
+  fn synthesize<CS: ConstraintSystem<F>>(
+    &self,
+    cs: &mut CS,
+    pc: Option<&AllocatedNum<F>>,
+    z: &[AllocatedNum<F>],
+  ) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedNum<F>>), SynthesisError>;
+}
+
+/// A helper trait for a step of the incremental computation for `SuperNova` (i.e., circuit for F) -- automatically
+/// implemented for `StepCircuit` and used internally to enforce that the circuit selected by the program counter is used
+/// at each step.
+pub trait EnforcingStepCircuit<F: PrimeField>: Send + Sync + Clone + StepCircuit<F> {
+  /// Delegate synthesis to `StepCircuit::synthesize`, and additionally, enforce the constraint that program counter
+  /// `pc`, if supplied, is equal to the circuit's assigned index.
+  fn enforcing_synthesize<CS: ConstraintSystem<F>>(
+    &self,
+    cs: &mut CS,
+    pc: Option<&AllocatedNum<F>>,
+    z: &[AllocatedNum<F>],
+  ) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedNum<F>>), SynthesisError> {
+    if let Some(pc) = pc {
+      let circuit_index = F::from(self.circuit_index() as u64);
+
+      // pc * 1 = circuit_index
+      cs.enforce(
+        || "pc matches circuit index",
+        |lc| lc + pc.get_variable(),
+        |lc| lc + CS::one(),
+        |lc| lc + (circuit_index, CS::one()),
+      );
+    }
+    self.synthesize(cs, pc, z)
+  }
+}
+
+impl<F: PrimeField, S: StepCircuit<F>> EnforcingStepCircuit<F> for S {}
+
+/// A trivial step circuit that simply returns the input
+#[derive(Clone, Debug, Default)]
+pub struct TrivialTestCircuit<F: PrimeField> {
+  _p: PhantomData<F>,
+}
+
+impl<F> StepCircuit<F> for TrivialTestCircuit<F>
+where
+  F: PrimeField,
+{
+  fn arity(&self) -> usize {
+    1
+  }
+
+  fn circuit_index(&self) -> usize {
+    0
+  }
+
+  fn synthesize<CS: ConstraintSystem<F>>(
+    &self,
+    _cs: &mut CS,
+    program_counter: Option<&AllocatedNum<F>>,
+    z: &[AllocatedNum<F>],
+  ) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedNum<F>>), SynthesisError> {
+    Ok((program_counter.cloned(), z.to_vec()))
+  }
+}
+
+/// A trivial step circuit that simply returns the input, for use on the secondary circuit when implementing NIVC.
+/// NOTE: This should not be needed. The secondary circuit doesn't need the program counter at all.
+/// Ideally, the need this fills could be met by `traits::circuit::TrivialTestCircuit` (or equivalent).
+#[derive(Clone, Debug, Default)]
+pub struct TrivialSecondaryCircuit<F: PrimeField> {
+  _p: PhantomData<F>,
+}
+
+impl<F> StepCircuit<F> for TrivialSecondaryCircuit<F>
+where
+  F: PrimeField,
+{
+  fn arity(&self) -> usize {
+    1
+  }
+
+  fn circuit_index(&self) -> usize {
+    0
+  }
+
+  fn synthesize<CS: ConstraintSystem<F>>(
+    &self,
+    _cs: &mut CS,
+    program_counter: Option<&AllocatedNum<F>>,
+    z: &[AllocatedNum<F>],
+  ) -> Result<(Option<AllocatedNum<F>>, Vec<AllocatedNum<F>>), SynthesisError> {
+    assert!(program_counter.is_none());
+    assert_eq!(z.len(), 1, "Arity of trivial step circuit should be 1");
+    Ok((None, z.to_vec()))
+  }
+}
+
 #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Abomonation)]
 pub struct SuperNovaAugmentedCircuitParams {
   limb_width: usize,
@@ -425,7 +533,7 @@ impl<'a, E: Engine, SC: EnforcingStepCircuit<E::Base>> SuperNovaAugmentedCircuit
       let z0_len = self.inputs.as_ref().map_or(0, |inputs| inputs.z0.len());
       if self.step_circuit.arity() != z0_len {
         return Err(SynthesisError::IncompatibleLengthVector(format!(
-          "z0_len {:?} != arity lengh {:?}",
+          "z0_len {:?} != arity length {:?}",
           z0_len,
           self.step_circuit.arity()
         )));
@@ -605,7 +713,8 @@ mod tests {
       {Bn256Engine, GrumpkinEngine}, {PallasEngine, VestaEngine},
       {Secp256k1Engine, Secq256k1Engine},
     },
-    traits::{circuit_supernova::TrivialTestCircuit, snark::default_ck_hint},
+    supernova::circuit::TrivialTestCircuit,
+    traits::snark::default_ck_hint,
   };
   use expect_test::{expect, Expect};