clean up secondary circuit

benches/recursive-snark-supernova.rs

@@ -94,7 +94,7 @@ fn bench_one_augmented_circuit_recursive_snark(c: &mut Criterion) {
         RecursiveSNARK::iter_base_step(
           &running_claim1,
           digest,
-          program_counter,
+          Some(program_counter),
           0,
           1,
           &z0_primary,
@@ -216,7 +216,7 @@ fn bench_two_augmented_circuit_recursive_snark(c: &mut Criterion) {
         RecursiveSNARK::iter_base_step(
           &running_claim1,
           digest,
-          program_counter,
+          Some(program_counter),
           0,
           2,
           &z0_primary,
@@ -315,16 +315,16 @@ where
   fn synthesize<CS: ConstraintSystem<F>>(
     &self,
     cs: &mut CS,
-    pc: &AllocatedNum<F>,
+    pc: Option<&AllocatedNum<F>>,
     z: &[AllocatedNum<F>],
-  ) -> Result<(AllocatedNum<F>, Vec<AllocatedNum<F>>), SynthesisError> {
+  ) -> Result<(Option<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]))
+    Ok((pc.cloned(), vec![y]))
   }
 }

src/supernova/circuit.rs

@@ -76,7 +76,7 @@ pub struct SuperNovaAugmentedCircuitInputs<'a, G: Group> {
   U: Option<&'a [Option<RelaxedR1CSInstance<G>>]>,
   u: Option<&'a R1CSInstance<G>>,
   T: Option<&'a Commitment<G>>,
-  program_counter: G::Base,
+  program_counter: Option<G::Base>,
   last_augmented_circuit_index: G::Base,
 }
 
@@ -91,7 +91,7 @@ impl<'a, G: Group> SuperNovaAugmentedCircuitInputs<'a, G> {
     U: Option<&'a [Option<RelaxedR1CSInstance<G>>]>,
     u: Option<&'a R1CSInstance<G>>,
     T: Option<&'a Commitment<G>>,
-    program_counter: G::Base,
+    program_counter: Option<G::Base>,
     last_augmented_circuit_index: G::Base,
   ) -> Self {
     Self {
@@ -178,7 +178,15 @@ impl<'a, G: Group, SC: StepCircuit<G::Base>> SuperNovaAugmentedCircuit<'a, G, SC
     let program_counter = if self.params.is_primary_circuit {
       Some(AllocatedNum::alloc(
         cs.namespace(|| "program_counter"),
-        || Ok(self.inputs.get()?.program_counter),
+        || {
+          Ok(
+            self
+              .inputs
+              .get()?
+              .program_counter
+              .expect("program_counter missing"),
+          )
+        },
       )?)
     } else {
       None
@@ -330,14 +338,21 @@ impl<'a, G: Group, SC: StepCircuit<G::Base>> SuperNovaAugmentedCircuit<'a, G, SC
     let mut ro = G::ROCircuit::new(
       self.ro_consts.clone(),
       2 // params_next, i_new
-      + program_counter.as_ref().map_or(0, |_| 1) // optional program counter
+      + program_counter.as_ref().map_or(0, |_|
+                                        usize::from(self.params.is_primary_circuit)
+      ) // optional program counter
         + 2 * arity // zo, z1
         + num_augmented_circuits * (7 + 2 * self.params.n_limbs), // #num_augmented_circuits * (7 + [X0, X1]*#num_limb)
     );
     ro.absorb(&params);
     ro.absorb(&i);
-    if let Some(program_counter) = program_counter.as_ref() {
-      ro.absorb(program_counter)
+
+    if self.params.is_primary_circuit {
+      if let Some(program_counter) = program_counter.as_ref() {
+        ro.absorb(program_counter)
+      } else {
+        Err(SynthesisError::AssignmentMissing)?
+      }
     }
 
     for e in &z_0 {
@@ -407,7 +422,7 @@ impl<'a, G: Group, SC: StepCircuit<G::Base>> SuperNovaAugmentedCircuit<'a, G, SC
   pub fn synthesize<CS: ConstraintSystem<<G as Group>::Base>>(
     self,
     cs: &mut CS,
-  ) -> Result<(AllocatedNum<G::Base>, Vec<AllocatedNum<G::Base>>), SynthesisError> {
+  ) -> Result<(Option<AllocatedNum<G::Base>>, Vec<AllocatedNum<G::Base>>), SynthesisError> {
     // NOTE `last_augmented_circuit_index` is aux without any constraint.
     // Reason is prover can only produce valid running instance by folding u into proper U_i[last_augmented_circuit_index]
     // However, there is crucial pre-asumption: `last_augmented_circuit_index` must within range [0, num_augmented_circuits)
@@ -534,16 +549,12 @@ impl<'a, G: Group, SC: StepCircuit<G::Base>> SuperNovaAugmentedCircuit<'a, G, SC
       &Boolean::from(is_base_case),
     )?;
 
-    let (program_counter_new, z_next) = if let Some(program_counter) = &program_counter {
-      self
-        .step_circuit
-        .synthesize(&mut cs.namespace(|| "F"), program_counter, &z_input)?
-    } else {
-      let zero_program_counter = alloc_zero(cs.namespace(|| "zero pc"))?;
-      self
-        .step_circuit
-        .synthesize(&mut cs.namespace(|| "F"), &zero_program_counter, &z_input)?
-    };
+    let (program_counter_new, z_next) = self.step_circuit.synthesize(
+      &mut cs.namespace(|| "F"),
+      program_counter.as_ref(),
+      &z_input,
+    )?;
+
     if z_next.len() != arity {
       return Err(SynthesisError::IncompatibleLengthVector(
         "z_next".to_string(),
@@ -576,7 +587,11 @@ impl<'a, G: Group, SC: StepCircuit<G::Base>> SuperNovaAugmentedCircuit<'a, G, SC
     ro.absorb(&i_next);
     // optionally absorb program counter if exist
     if program_counter.is_some() {
-      ro.absorb(&program_counter_new)
+      ro.absorb(
+        program_counter_new
+          .as_ref()
+          .expect("new program counter missing"),
+      )
     }
     for e in &z_0 {
       ro.absorb(e);

src/supernova/mod.rs

@@ -259,7 +259,7 @@ where
   pub fn iter_base_step<C1: StepCircuit<G1::Scalar>, C2: StepCircuit<G2::Scalar>>(
     claim: &RunningClaim<G1, G2, C1, C2>,
     pp_digest: G1::Scalar,
-    initial_program_counter: G1::Scalar,
+    initial_program_counter: Option<G1::Scalar>,
     first_augmented_circuit_index: usize,
     num_augmented_circuits: usize,
     z0_primary: &[G1::Scalar],
@@ -329,7 +329,7 @@ where
         None,
         Some(&u_primary),
         None,
-        G2::Scalar::ZERO, // secondary circuit never constrain/bump program counter
+        None,
         G2::Scalar::from(claim.augmented_circuit_index as u64),
       );
     let circuit_secondary: SuperNovaAugmentedCircuit<'_, G1, C2> = SuperNovaAugmentedCircuit::new(
@@ -379,6 +379,7 @@ where
       })
       .collect::<Result<Vec<<G1 as Group>::Scalar>, SuperNovaError>>()?;
     let zi_primary_pc_next = zi_primary_pc_next
+      .expect("zi_primary_pc_next missing")
       .get_value()
       .ok_or(SuperNovaError::NovaError(NovaError::SynthesisError))?;
     let zi_secondary = zi_secondary
@@ -473,7 +474,7 @@ where
         Some(&self.r_U_secondary),
         Some(&self.l_u_secondary),
         Some(&T),
-        self.program_counter,
+        Some(self.program_counter),
         G1::Scalar::ZERO,
       );
 
@@ -540,7 +541,7 @@ where
         Some(&self.r_U_primary),
         Some(&l_u_primary),
         Some(&binding),
-        G2::Scalar::ZERO, // secondary circuit never constrain/bump program counter
+        None,
         G2::Scalar::from(claim.get_augmented_circuit_index() as u64),
       );
 
@@ -573,6 +574,7 @@ where
       })
       .collect::<Result<Vec<<G1 as Group>::Scalar>, SuperNovaError>>()?;
     let zi_primary_pc_next = zi_primary_pc_next
+      .expect("zi_primary_pc_next missing")
       .get_value()
       .ok_or(SuperNovaError::NovaError(NovaError::SynthesisError))?;
     let zi_secondary = zi_secondary
@@ -659,7 +661,7 @@ where
 
     // secondary circuit
     let num_field_secondary_ro = 2 // params_next, i_new
-    + 2 * pp.F_arity_primary // zo, z1
+    + 2 * pp.F_arity_secondary // zo, z1
     + self.num_augmented_circuits * (7 + 2 * pp.augmented_circuit_params_primary.get_n_limbs()); // #num_augmented_circuits * (7 + [X0, X1]*#num_limb)
 
     let (hash_primary, hash_secondary) = {
@@ -810,3 +812,14 @@ where
 
   (ck_primary, ck_secondary)
 }
+
+/// SuperNova helper trait, for implementors that provide sets of sub-circuits to be proved via NIVC.
+pub trait CircuitSet<G: Group> {
+  /// Initial program counter, defaults to zero.
+  fn initial_program_counter(&self) -> G::Scalar {
+    G::Scalar::ZERO
+  }
+
+  /// How many augmented circuits are provided?
+  fn num_augmented_circuits(&self) -> usize;
+}