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

src/supernova/circuit.rs

@@ -259,17 +259,13 @@ impl<G: Group, SC: SuperNovaStepCircuit<G::Base>> SuperNovaCircuit<G, SC> {
   ) -> Result<Vec<AllocatedRelaxedR1CSInstance<G>>, SynthesisError> {
     let mut cs = cs.namespace(|| "alloc U_i default");
 
-    // The primary circuit just initialize default AllocatedRelaxedR1CSInstance
+    // The primary circuit just initialize single AllocatedRelaxedR1CSInstance
     let U_default = if self.params.is_primary_circuit {
-      (0..u_i_length)
-        .map(|i| {
-          AllocatedRelaxedR1CSInstance::default(
-            cs.namespace(|| format!("Allocate U_default {:?}", i)),
-            self.params.limb_width,
-            self.params.n_limbs,
-          )
-        })
-        .collect::<Result<Vec<AllocatedRelaxedR1CSInstance<G>>, _>>()?
+      vec![AllocatedRelaxedR1CSInstance::default(
+        cs.namespace(|| format!("Allocate primary U_default")),
+        self.params.limb_width,
+        self.params.n_limbs,
+      )?]
     } else {
       // The secondary circuit convert the incoming R1CS instance on index which match circuit index
       let imcomming_r1cs = AllocatedRelaxedR1CSInstance::from_r1cs_instance(
@@ -322,20 +318,22 @@ impl<G: Group, SC: SuperNovaStepCircuit<G::Base>> SuperNovaCircuit<G, SC> {
     arity: usize,
     last_circuit_index_selector: &AllocatedNum<G::Base>,
     program_counter: AllocatedNum<G::Base>,
+    u_i_length: usize,
   ) -> Result<(AllocatedRelaxedR1CSInstance<G>, AllocatedBit), SynthesisError> {
     // Check that u.x[0] = Hash(params, U, i, z0, zi)
     let mut ro = G::ROCircuit::new(
       self.ro_consts.clone(),
       3 // params_next, i_new, program_counter_new
         + 2 * arity // zo, z1
-        + self.u_i_length * (7 + 2 * self.params.n_limbs), // #num of u_i * (7 + [X0, X1]*#num_limb)
+        + u_i_length * (7 + 2 * self.params.n_limbs), // #num of u_i * (7 + [X0, X1]*#num_limb)
     );
     ro.absorb(params.clone());
     ro.absorb(i);
     ro.absorb(program_counter.clone());
 
     // NOTE only witness and DO NOT need to constrain last_circuit_index_selector.
     // Because prover can only make valid IVC proof by folding u into correct U_i[last_circuit_index_selector]
+    // therefore last_circuit_index_selector can be just aux
 
     for e in &z_0 {
       ro.absorb(e.clone());
@@ -430,7 +428,12 @@ impl<G: Group, SC: SuperNovaStepCircuit<G::Base>> Circuit<<G as Group>::Base>
     cs: &mut CS,
   ) -> Result<(), SynthesisError> {
     let arity = self.step_circuit.arity();
-    let u_i_length = self.u_i_length;
+    let u_i_length = if self.params.is_primary_circuit {
+      // primary circuit only fold single running instance from secondary circuit
+      1
+    } else {
+      self.u_i_length
+    };
 
     if self.inputs.is_some() {
       let z0_len = self.inputs.get().map_or(0, |inputs| inputs.z0.len());
@@ -441,6 +444,15 @@ impl<G: Group, SC: SuperNovaStepCircuit<G::Base>> Circuit<<G as Group>::Base>
           self.step_circuit.arity()
         )));
       }
+      let last_circuit_index_selector = self
+        .inputs
+        .get()
+        .map_or(G::Base::ZERO, |inputs| inputs.last_circuit_index_selector);
+      if self.params.is_primary_circuit && last_circuit_index_selector != G::Base::ZERO {
+        return Err(SynthesisError::IncompatibleLengthVector(
+          "primary circuit running instance only valid on index 0".to_string(),
+        ));
+      }
     }
 
     // Allocate all witnesses
@@ -477,6 +489,7 @@ impl<G: Group, SC: SuperNovaStepCircuit<G::Base>> Circuit<<G as Group>::Base>
       arity,
       &last_circuit_index_selector,
       program_counter.clone(),
+      u_i_length,
     )?;
 
     // update AllocatedRelaxedR1CSInstance on index match circuit index
@@ -564,7 +577,7 @@ impl<G: Group, SC: SuperNovaStepCircuit<G::Base>> Circuit<<G as Group>::Base>
       self.ro_consts.clone(),
       3 // params_next, i_new, program_counter_new
         + 2 * arity // zo, z1
-        + self.u_i_length * (7 + 2 * self.params.n_limbs), // #num of u_i * (7 + [X0, X1]*#num_limb)
+        + u_i_length * (7 + 2 * self.params.n_limbs), // #num of u_i * (7 + [X0, X1]*#num_limb)
     );
     ro.absorb(params_next.clone());
     ro.absorb(i_new.clone());

src/supernova/mod.rs

@@ -242,8 +242,8 @@ where
 {
   r_W_primary: Vec<Option<RelaxedR1CSWitness<G1>>>,
   r_U_primary: Vec<Option<RelaxedR1CSInstance<G1>>>,
-  r_W_secondary: Vec<Option<RelaxedR1CSWitness<G2>>>,
-  r_U_secondary: Vec<Option<RelaxedR1CSInstance<G2>>>,
+  r_W_secondary: Option<RelaxedR1CSWitness<G2>>,
+  r_U_secondary: Option<RelaxedR1CSInstance<G2>>,
   l_w_secondary: R1CSWitness<G2>,
   l_u_secondary: R1CSInstance<G2>,
   pp_digest: G1::Scalar,
@@ -372,21 +372,11 @@ where
           .collect::<Vec<Option<RelaxedR1CSInstance<G1>>>>();
         r_U_primary_initial_list[circuit_index] = Some(r_U_primary);
 
-        let mut r_W_secondary_initial_list = (0..u_i_length)
-          .map(|_| None)
-          .collect::<Vec<Option<RelaxedR1CSWitness<G2>>>>();
-        r_W_secondary_initial_list[circuit_index] = Some(r_W_secondary);
-
-        let mut r_U_recondary_initial_list = (0..u_i_length)
-          .map(|_| None)
-          .collect::<Vec<Option<RelaxedR1CSInstance<G2>>>>();
-        r_U_recondary_initial_list[circuit_index] = Some(r_U_secondary);
-
         Ok(Self {
           r_W_primary: r_W_primary_initial_list,
           r_U_primary: r_U_primary_initial_list,
-          r_W_secondary: r_W_secondary_initial_list,
-          r_U_secondary: r_U_recondary_initial_list,
+          r_W_secondary: Some(r_W_secondary),
+          r_U_secondary: Some(r_U_secondary),
           l_w_secondary,
           l_u_secondary,
           pp_digest: pp.digest,
@@ -406,29 +396,20 @@ where
           &pp.ro_consts_secondary,
           &scalar_as_base::<G1>(r_snark.pp_digest),
           &pp.r1cs_shape_secondary,
-          &r_snark
-            .r_U_secondary
-            .get(0)
-            .unwrap_or(&None)
-            .clone()
-            .unwrap_or_else(|| {
-              RelaxedR1CSInstance::default(ck_secondary, &pp.r1cs_shape_secondary)
-            }),
+          &r_snark.r_U_secondary.clone().unwrap_or_else(|| {
+            RelaxedR1CSInstance::default(ck_secondary, &pp.r1cs_shape_secondary)
+          }),
           &r_snark
             .r_W_secondary
-            .get(0)
-            .unwrap_or(&None)
             .clone()
             .unwrap_or_else(|| RelaxedR1CSWitness::default(&pp.r1cs_shape_secondary)),
           &r_snark.l_u_secondary,
           &r_snark.l_w_secondary,
         )?;
 
         // clone and updated running instance on respective circuit_index
-        let mut r_U_secondary_next = r_snark.r_U_secondary.to_vec();
-        r_U_secondary_next[0] = Some(r_U_secondary_folded);
-        let mut r_W_secondary_next = r_snark.r_W_secondary.to_vec();
-        r_W_secondary_next[0] = Some(r_W_secondary_folded);
+        let r_U_secondary_next = Some(r_U_secondary_folded);
+        let r_W_secondary_next = Some(r_W_secondary_folded);
 
         let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
         let inputs_primary: CircuitInputs<G2> = CircuitInputs::new(
@@ -437,17 +418,7 @@ where
           G1::Scalar::from(r_snark.i as u64),
           z0_primary.clone(),
           Some(r_snark.zi_primary.clone()),
-          Some(
-            r_snark
-              .r_U_secondary
-              .iter()
-              .map(|U| {
-                U.clone().unwrap_or_else(|| {
-                  RelaxedR1CSInstance::default(ck_secondary, &pp.r1cs_shape_secondary)
-                })
-              })
-              .collect(),
-          ),
+          r_snark.r_U_secondary.map(|U| vec![U]),
           Some(r_snark.l_u_secondary.clone()),
           Some(Commitment::<G2>::decompress(&nifs_secondary.comm_T)?),
           r_snark.program_counter,
@@ -587,28 +558,29 @@ where
       _ => Ok(()),
     })?;
 
-    self
-      .r_U_secondary
-      .iter()
-      .try_for_each(|U| match U.clone() {
-        Some(U) if U.X.len() != 2 => {
-          println!(
-            "r_U_secondary got instance length {:?} != {:?}",
-            U.X.len(),
-            2
-          );
-          Err(NovaError::ProofVerifyError)
-        }
-        _ => Ok(()),
-      })?;
+    self.r_U_secondary.clone().map_or(Ok(()), |U| {
+      if U.X.len() != 2 {
+        println!(
+          "r_U_secondary got instance length {:?} != {:?}",
+          U.X.len(),
+          2
+        );
+        Err(NovaError::ProofVerifyError)
+      } else {
+        Ok(())
+      }
+    })?;
 
     // check if the output hashes in R1CS instances point to the right running instances
-    let num_field_ro = 3 // params_next, i_new, program_counter_new
+    let num_field_primary_ro = 3 // params_next, i_new, program_counter_new
+    + 2 * pp.F_arity_primary // zo, z1
+    + 1 * (7 + 2 * pp.augmented_circuit_params_primary.n_limbs); // #num of u_i * (7 + [X0, X1]*#num_limb)
+    let num_field_secondary_ro = 3 // params_next, i_new, program_counter_new
     + 2 * pp.F_arity_primary // zo, z1
     + u_i_length * (7 + 2 * pp.augmented_circuit_params_primary.n_limbs); // #num of u_i * (7 + [X0, X1]*#num_limb)
 
     let (hash_primary, hash_secondary) = {
-      let mut hasher = <G2 as Group>::RO::new(pp.ro_consts_secondary.clone(), num_field_ro);
+      let mut hasher = <G2 as Group>::RO::new(pp.ro_consts_secondary.clone(), num_field_primary_ro);
       hasher.absorb(pp.digest);
       hasher.absorb(G1::Scalar::from(self.i as u64));
       hasher.absorb(self.program_counter);
@@ -620,12 +592,11 @@ where
         hasher.absorb(*e);
       }
       self.r_U_secondary.iter().for_each(|U| {
-        U.clone()
-          .unwrap_or_else(|| RelaxedR1CSInstance::default(ck_secondary, &pp.r1cs_shape_secondary))
-          .absorb_in_ro(&mut hasher);
+        U.absorb_in_ro(&mut hasher);
       });
 
-      let mut hasher2 = <G1 as Group>::RO::new(pp.ro_consts_primary.clone(), num_field_ro);
+      let mut hasher2 =
+        <G1 as Group>::RO::new(pp.ro_consts_primary.clone(), num_field_secondary_ro);
       hasher2.absorb(scalar_as_base::<G1>(pp.digest));
       hasher2.absorb(G2::Scalar::from(self.i as u64));
       hasher2.absorb(G2::Scalar::ZERO);
@@ -663,6 +634,9 @@ where
     }
 
     // check the satisfiability of the provided `circuit_index` instance
+    let default_r_U_secondary =
+      RelaxedR1CSInstance::default(ck_secondary, &pp.r1cs_shape_secondary);
+    let default_r_W_secondary = RelaxedR1CSWitness::default(&pp.r1cs_shape_secondary);
     let (res_r_primary, (res_r_secondary, res_l_secondary)) = rayon::join(
       || {
         pp.r1cs_shape_primary.is_sat_relaxed(
@@ -680,14 +654,14 @@ where
           || {
             pp.r1cs_shape_secondary.is_sat_relaxed(
               pp.ck_secondary.as_ref().unwrap(),
-              &self.r_U_secondary[circuit_index]
-                .clone()
-                .unwrap_or_else(|| {
-                  RelaxedR1CSInstance::default(ck_secondary, &pp.r1cs_shape_secondary)
-                }),
-              &self.r_W_secondary[circuit_index]
-                .clone()
-                .unwrap_or_else(|| RelaxedR1CSWitness::default(&pp.r1cs_shape_secondary)),
+              self
+                .r_U_secondary
+                .as_ref()
+                .unwrap_or_else(|| &default_r_U_secondary),
+              &self
+                .r_W_secondary
+                .as_ref()
+                .unwrap_or_else(|| &default_r_W_secondary),
             )
           },
           || {