Recursion implementation (#65)

* recursion attempt

* address clippy

* initialize the running instance and witness of the primary correctly

* add asserts for debugging

* fix a bug in AllocatedPoint

* add debug statements

* fix an issue with how we inputize hashes; remove debug statements

* rename

* cleanup

* speedup tests

* require step_circuit implementors to provide a way to execute step computation

.github/workflows/rust.yml

@@ -20,7 +20,7 @@ jobs:
     - name: Build
       run: cargo build --verbose
     - name: Run tests
-      run: cargo test --verbose
+      run: cargo test --release --verbose
     - name: Check Rustfmt Code Style
       run: cargo fmt --all -- --check
     - name: Check clippy warnings

src/circuit.rs

@@ -93,9 +93,9 @@ where
   SC: StepCircuit<G::Base>,
 {
   params: NIFSVerifierCircuitParams,
+  ro_consts: ROConstantsCircuit<G::Base>,
   inputs: Option<NIFSVerifierCircuitInputs<G>>,
   step_circuit: SC, // The function that is applied for each step
-  ro_consts: ROConstantsCircuit<G::Base>,
 }
 
 impl<G, SC> NIFSVerifierCircuit<G, SC>
@@ -335,10 +335,10 @@ where
     let hash = le_bits_to_num(cs.namespace(|| "convert hash to num"), hash_bits)?;
 
     // Outputs the computed hash and u.X[1] that corresponds to the hash of the other circuit
-    let _ = hash.inputize(cs.namespace(|| "output new hash of this circuit"))?;
     let _ = u
       .X1
       .inputize(cs.namespace(|| "Output unmodified hash of the other circuit"))?;
+    let _ = hash.inputize(cs.namespace(|| "output new hash of this circuit"))?;
 
     Ok(())
   }
@@ -373,6 +373,10 @@ mod tests {
     ) -> Result<AllocatedNum<F>, SynthesisError> {
       Ok(z)
     }
+
+    fn compute(&self, z: &F) -> F {
+      *z
+    }
   }
 
   #[test]

src/gadgets/ecc.rs

@@ -38,7 +38,7 @@ where
       Ok(coords.map_or(Fp::zero(), |c| c.0))
     })?;
     let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
-      Ok(coords.map_or(Fp::zero(), |c| c.0))
+      Ok(coords.map_or(Fp::zero(), |c| c.1))
     })?;
     let is_infinity = AllocatedNum::alloc(cs.namespace(|| "is_infinity"), || {
       Ok(if coords.map_or(true, |c| c.2) {

src/lib.rs

@@ -20,13 +20,14 @@ use crate::bellperson::{
   shape_cs::ShapeCS,
   solver::SatisfyingAssignment,
 };
-use crate::poseidon::ROConstantsCircuit; // TODO: make this a trait so we can use it without the concrete implementation
 use ::bellperson::{Circuit, ConstraintSystem};
 use circuit::{NIFSVerifierCircuit, NIFSVerifierCircuitInputs, NIFSVerifierCircuitParams};
 use constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
 use core::marker::PhantomData;
 use errors::NovaError;
 use ff::Field;
+use nifs::NIFS;
+use poseidon::ROConstantsCircuit; // TODO: make this a trait so we can use it without the concrete implementation
 use r1cs::{
   R1CSGens, R1CSInstance, R1CSShape, R1CSWitness, RelaxedR1CSInstance, RelaxedR1CSWitness,
 };
@@ -148,6 +149,7 @@ where
     pp: &PublicParams<G1, G2, C1, C2>,
     z0_primary: G1::Scalar,
     z0_secondary: G2::Scalar,
+    num_steps: usize,
   ) -> Result<Self, NovaError> {
     // Execute the base case for the primary
     let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
@@ -171,11 +173,6 @@ where
       .r1cs_instance_and_witness(&pp.r1cs_shape_primary, &pp.r1cs_gens_primary)
       .map_err(|_e| NovaError::UnSat)?;
 
-    // check if the base case is satisfied
-    pp.r1cs_shape_primary
-      .is_sat(&pp.r1cs_gens_primary, &u_primary, &w_primary)
-      .map_err(|_e| NovaError::UnSat)?;
-
     // Execute the base case for the secondary
     let mut cs_secondary: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
     let inputs_secondary: NIFSVerifierCircuitInputs<G1> = NIFSVerifierCircuitInputs::new(
@@ -198,26 +195,115 @@ where
       .r1cs_instance_and_witness(&pp.r1cs_shape_secondary, &pp.r1cs_gens_secondary)
       .map_err(|_e| NovaError::UnSat)?;
 
-    // check if the base case is satisfied
+    // execute the remaining steps, alternating between G1 and G2
-    pp.r1cs_shape_secondary
+    let mut l_w_primary = w_primary;
-      .is_sat(&pp.r1cs_gens_secondary, &u_secondary, &w_secondary)
+    let mut l_u_primary = u_primary;
-      .map_err(|_e| NovaError::UnSat)?;
+    let mut r_W_primary =
+      RelaxedR1CSWitness::from_r1cs_witness(&pp.r1cs_shape_primary, &l_w_primary);
+    let mut r_U_primary = RelaxedR1CSInstance::from_r1cs_instance(
+      &pp.r1cs_gens_primary,
+      &pp.r1cs_shape_primary,
+      &l_u_primary,
+    );
+
+    let mut r_W_secondary = RelaxedR1CSWitness::<G2>::default(&pp.r1cs_shape_secondary);
+    let mut r_U_secondary =
+      RelaxedR1CSInstance::<G2>::default(&pp.r1cs_gens_secondary, &pp.r1cs_shape_secondary);
+    let mut l_w_secondary = w_secondary;
+    let mut l_u_secondary = u_secondary;
+
+    let mut z_next_primary = z0_primary;
+    let mut z_next_secondary = z0_secondary;
+
+    // TODO: execute the provided step circuit(s) to feed real z_i into the verifier circuit
+    for i in 1..num_steps {
+      // fold the secondary circuit's instance into r_W_primary
+      let (nifs_secondary, (r_U_next_secondary, r_W_next_secondary)) = NIFS::prove(
+        &pp.r1cs_gens_secondary,
+        &pp._ro_consts_secondary,
+        &pp.r1cs_shape_secondary,
+        &r_U_secondary,
+        &r_W_secondary,
+        &l_u_secondary,
+        &l_w_secondary,
+      )?;
+
+      z_next_primary = pp.c_primary.compute(&z_next_primary);
+      z_next_secondary = pp.c_secondary.compute(&z_next_secondary);
+
+      let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
+      let inputs_primary: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
+        pp.r1cs_shape_secondary.get_digest(),
+        <G2 as Group>::Base::from(i as u64),
+        z0_primary,
+        Some(z_next_primary),
+        Some(r_U_secondary),
+        Some(l_u_secondary),
+        Some(nifs_secondary.comm_T.decompress()?),
+      );
+
+      let circuit_primary: NIFSVerifierCircuit<G2, C1> = NIFSVerifierCircuit::new(
+        pp.params_primary.clone(),
+        Some(inputs_primary),
+        pp.c_primary.clone(),
+        pp.ro_consts_circuit_primary.clone(),
+      );
+      let _ = circuit_primary.synthesize(&mut cs_primary);
+
+      (l_u_primary, l_w_primary) = cs_primary
+        .r1cs_instance_and_witness(&pp.r1cs_shape_primary, &pp.r1cs_gens_primary)
+        .map_err(|_e| NovaError::UnSat)?;
+
+      // fold the secondary circuit's instance into r_W_primary
+      let (nifs_primary, (r_U_next_primary, r_W_next_primary)) = NIFS::prove(
+        &pp.r1cs_gens_primary,
+        &pp._ro_consts_primary,
+        &pp.r1cs_shape_primary,
+        &r_U_primary.clone(),
+        &r_W_primary.clone(),
+        &l_u_primary.clone(),
+        &l_w_primary.clone(),
+      )?;
+
+      let mut cs_secondary: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
+      let inputs_secondary: NIFSVerifierCircuitInputs<G1> = NIFSVerifierCircuitInputs::new(
+        pp.r1cs_shape_primary.get_digest(),
+        <G1 as Group>::Base::from(i as u64),
+        z0_secondary,
+        Some(z_next_secondary),
+        Some(r_U_primary.clone()),
+        Some(l_u_primary.clone()),
+        Some(nifs_primary.comm_T.decompress()?),
+      );
+
+      let circuit_secondary: NIFSVerifierCircuit<G1, C2> = NIFSVerifierCircuit::new(
+        pp.params_secondary.clone(),
+        Some(inputs_secondary),
+        pp.c_secondary.clone(),
+        pp.ro_consts_circuit_secondary.clone(),
+      );
+      let _ = circuit_secondary.synthesize(&mut cs_secondary);
+
+      (l_u_secondary, l_w_secondary) = cs_secondary
+        .r1cs_instance_and_witness(&pp.r1cs_shape_secondary, &pp.r1cs_gens_secondary)
+        .map_err(|_e| NovaError::UnSat)?;
+
+      // update the running instances and witnesses
+      r_U_secondary = r_U_next_secondary;
+      r_W_secondary = r_W_next_secondary;
+      r_U_primary = r_U_next_primary;
+      r_W_primary = r_W_next_primary;
+    }
 
     Ok(Self {
-      r_W_primary: RelaxedR1CSWitness::<G1>::default(&pp.r1cs_shape_primary),
+      r_W_primary,
-      r_U_primary: RelaxedR1CSInstance::<G1>::default(
+      r_U_primary,
-        &pp.r1cs_gens_primary,
+      l_w_primary,
-        &pp.r1cs_shape_primary,
+      l_u_primary,
-      ),
+      r_W_secondary,
-      l_w_primary: w_primary,
+      r_U_secondary,
-      l_u_primary: u_primary,
+      l_w_secondary,
-      r_W_secondary: RelaxedR1CSWitness::<G2>::default(&pp.r1cs_shape_secondary),
+      l_u_secondary,
-      r_U_secondary: RelaxedR1CSInstance::<G2>::default(
-        &pp.r1cs_gens_secondary,
-        &pp.r1cs_shape_secondary,
-      ),
-      l_w_secondary: w_secondary,
-      l_u_secondary: u_secondary,
       _p_c1: Default::default(),
       _p_c2: Default::default(),
     })
@@ -225,18 +311,23 @@ where
 
   /// Verify the correctness of the `RecursiveSNARK`
   pub fn verify(&self, pp: &PublicParams<G1, G2, C1, C2>) -> Result<(), NovaError> {
+    // TODO: perform additional checks on whether (shape_digest, z_0, z_i, i) are correct
+
     pp.r1cs_shape_primary.is_sat_relaxed(
       &pp.r1cs_gens_primary,
       &self.r_U_primary,
       &self.r_W_primary,
     )?;
+
     pp.r1cs_shape_primary
       .is_sat(&pp.r1cs_gens_primary, &self.l_u_primary, &self.l_w_primary)?;
+
     pp.r1cs_shape_secondary.is_sat_relaxed(
       &pp.r1cs_gens_secondary,
       &self.r_U_secondary,
       &self.r_W_secondary,
     )?;
+
     pp.r1cs_shape_secondary.is_sat(
       &pp.r1cs_gens_secondary,
       &self.l_u_secondary,
@@ -272,10 +363,14 @@ mod tests {
     ) -> Result<AllocatedNum<F>, SynthesisError> {
       Ok(z)
     }
+
+    fn compute(&self, z: &F) -> F {
+      *z
+    }
   }
 
   #[test]
-  fn test_base_case() {
+  fn test_ivc() {
     // produce public parameters
     let pp = PublicParams::<
       G1,
@@ -296,6 +391,7 @@ mod tests {
       &pp,
       <G2 as Group>::Base::zero(),
       <G1 as Group>::Base::zero(),
+      3,
     );
     assert!(res.is_ok());
     let recursive_snark = res.unwrap();

src/nifs.rs

@@ -12,7 +12,7 @@ use std::marker::PhantomData;
 
 /// A SNARK that holds the proof of a step of an incremental computation
 pub struct NIFS<G: Group> {
-  comm_T: CompressedCommitment<G::CompressedGroupElement>,
+  pub(crate) comm_T: CompressedCommitment<G::CompressedGroupElement>,
   _p: PhantomData<G>,
 }
 

src/r1cs.rs

@@ -438,6 +438,14 @@ impl<G: Group> RelaxedR1CSWitness<G> {
     }
   }
 
+  /// Initializes a new RelaxedR1CSWitness from an R1CSWitness
+  pub fn from_r1cs_witness(S: &R1CSShape<G>, witness: &R1CSWitness<G>) -> RelaxedR1CSWitness<G> {
+    RelaxedR1CSWitness {
+      W: witness.W.clone(),
+      E: vec![G::Scalar::zero(); S.num_cons],
+    }
+  }
+
   /// Commits to the witness using the supplied generators
   pub fn commit(&self, gens: &R1CSGens<G>) -> (Commitment<G>, Commitment<G>) {
     (self.W.commit(&gens.gens_W), self.E.commit(&gens.gens_E))
@@ -483,6 +491,19 @@ impl<G: Group> RelaxedR1CSInstance<G> {
     }
   }
 
+  /// Initializes a new RelaxedR1CSInstance from an R1CSInstance
+  pub fn from_r1cs_instance(
+    gens: &R1CSGens<G>,
+    S: &R1CSShape<G>,
+    instance: &R1CSInstance<G>,
+  ) -> RelaxedR1CSInstance<G> {
+    let mut r_instance = RelaxedR1CSInstance::default(gens, S);
+    r_instance.comm_W = instance.comm_W;
+    r_instance.u = G::Scalar::one();
+    r_instance.X = instance.X.clone();
+    r_instance
+  }
+
   /// Folds an incoming RelaxedR1CSInstance into the current one
   pub fn fold(
     &self,

src/traits.rs

@@ -143,6 +143,9 @@ pub trait StepCircuit<F: PrimeField> {
     cs: &mut CS,
     z: AllocatedNum<F>,
   ) -> Result<AllocatedNum<F>, SynthesisError>;
+
+  /// Execute the circuit for a computation step and return output
+  fn compute(&self, z: &F) -> F;
 }
 
 impl<F: PrimeField> AppendToTranscriptTrait for F {