Refactor: fix asymmetries between Nova and SuperNova APIs (#993)

* Include the number of steps in the Nova proof type so it can be used for verification

* Remove the need to pass an extra input for `RecursiveSNARKTrait::verify`

* `RecursiveSNARKTrait` no longer needs an arbitrary `ProofOutput` since the index of the last circuit
  is no longer needed for SuperNova proof verification

benches/end2end.rs

@@ -345,12 +345,12 @@ fn verify_benchmark(c: &mut Criterion) {
             let ptr = go_base(&store, state.clone(), s.0, s.1);
             let prover = NovaProver::new(reduction_count, lang_pallas_rc.clone());
             let (frames, _) = evaluate::<Fq, Coproc<Fq>>(None, ptr, &store, limit).unwrap();
-            let (proof, z0, zi, num_steps) = prover.prove(&pp, &frames, &store).unwrap();
+            let (proof, z0, zi, _num_steps) = prover.prove(&pp, &frames, &store).unwrap();
 
             b.iter_batched(
                 || z0.clone(),
                 |z0| {
-                    let result = proof.verify(&pp, &z0, &zi[..], num_steps).unwrap();
+                    let result = proof.verify(&pp, &z0, &zi[..]).unwrap();
                     black_box(result);
                 },
                 BatchSize::LargeInput,
@@ -397,16 +397,14 @@ fn verify_compressed_benchmark(c: &mut Criterion) {
             let ptr = go_base(&store, state.clone(), s.0, s.1);
             let prover = NovaProver::new(reduction_count, lang_pallas_rc.clone());
             let (frames, _) = evaluate::<Fq, Coproc<Fq>>(None, ptr, &store, limit).unwrap();
-            let (proof, z0, zi, num_steps) = prover.prove(&pp, &frames, &store).unwrap();
+            let (proof, z0, zi, _num_steps) = prover.prove(&pp, &frames, &store).unwrap();
 
             let compressed_proof = proof.compress(&pp).unwrap();
 
             b.iter_batched(
                 || z0.clone(),
                 |z0| {
-                    let result = compressed_proof
-                        .verify(&pp, &z0, &zi[..], num_steps)
-                        .unwrap();
+                    let result = compressed_proof.verify(&pp, &z0, &zi[..]).unwrap();
                     black_box(result);
                 },
                 BatchSize::LargeInput,

examples/circom.rs

@@ -127,7 +127,7 @@ fn main() {
     println!("Beginning proof step...");
 
     let proof_start = Instant::now();
-    let (proof, z0, zi, num_steps) = nova_prover
+    let (proof, z0, zi, _num_steps) = nova_prover
         .evaluate_and_prove(&pp, ptr, store.intern_nil(), store, 10000)
         .unwrap();
     let proof_end = proof_start.elapsed();
@@ -137,7 +137,7 @@ fn main() {
     println!("Verifying proof...");
 
     let verify_start = Instant::now();
-    let res = proof.verify(&pp, &z0, &zi, num_steps).unwrap();
+    let res = proof.verify(&pp, &z0, &zi).unwrap();
     let verify_end = verify_start.elapsed();
 
     println!("Verify took {verify_end:?}");

examples/sha256_ivc.rs

@@ -87,7 +87,7 @@ fn main() {
 
     println!("Beginning proof step...");
     let proof_start = Instant::now();
-    let (proof, z0, zi, num_steps) = tracing_texray::examine(tracing::info_span!("bang!"))
+    let (proof, z0, zi, _num_steps) = tracing_texray::examine(tracing::info_span!("bang!"))
         .in_scope(|| {
             nova_prover
                 .evaluate_and_prove(&pp, call, store.intern_nil(), store, 10000)
@@ -100,7 +100,7 @@ fn main() {
     println!("Verifying proof...");
 
     let verify_start = Instant::now();
-    assert!(proof.verify(&pp, &z0, &zi, num_steps).unwrap());
+    assert!(proof.verify(&pp, &z0, &zi).unwrap());
     let verify_end = verify_start.elapsed();
 
     println!("Verify took {:?}", verify_end);
@@ -113,7 +113,7 @@ fn main() {
     println!("Compression took {:?}", compress_end);
 
     let compressed_verify_start = Instant::now();
-    let res = compressed_proof.verify(&pp, &z0, &zi, num_steps).unwrap();
+    let res = compressed_proof.verify(&pp, &z0, &zi).unwrap();
     let compressed_verify_end = compressed_verify_start.elapsed();
 
     println!("Final verification took {:?}", compressed_verify_end);

examples/sha256_nivc.rs

@@ -95,17 +95,16 @@ fn main() {
 
     println!("Beginning proof step...");
     let proof_start = Instant::now();
-    let ((proof, last_circuit_index), z0, zi, _num_steps) =
-        tracing_texray::examine(tracing::info_span!("bang!"))
-            .in_scope(|| supernova_prover.prove(&pp, &frames, store).unwrap());
+    let (proof, z0, zi, _num_steps) = tracing_texray::examine(tracing::info_span!("bang!"))
+        .in_scope(|| supernova_prover.prove(&pp, &frames, store).unwrap());
     let proof_end = proof_start.elapsed();
 
     println!("Proofs took {:?}", proof_end);
 
     println!("Verifying proof...");
 
     let verify_start = Instant::now();
-    assert!(proof.verify(&pp, &z0, &zi, last_circuit_index).unwrap());
+    assert!(proof.verify(&pp, &z0, &zi).unwrap());
     let verify_end = verify_start.elapsed();
 
     println!("Verify took {:?}", verify_end);
@@ -118,9 +117,7 @@ fn main() {
     println!("Compression took {:?}", compress_end);
 
     let compressed_verify_start = Instant::now();
-    let res = compressed_proof
-        .verify(&pp, &z0, &zi, last_circuit_index)
-        .unwrap();
+    let res = compressed_proof.verify(&pp, &z0, &zi).unwrap();
     let compressed_verify_end = compressed_verify_start.elapsed();
 
     println!("Final verification took {:?}", compressed_verify_end);

src/cli/lurk_proof.rs

@@ -139,7 +139,6 @@ pub(crate) enum LurkProof<
         proof: nova::Proof<'a, F, C, M>,
         public_inputs: Vec<F>,
         public_outputs: Vec<F>,
-        num_steps: usize,
         rc: usize,
         lang: Lang<F, C>,
     },
@@ -209,15 +208,14 @@ where
                 proof,
                 public_inputs,
                 public_outputs,
-                num_steps,
                 rc,
                 lang,
             } => {
                 tracing::info!("Loading public parameters");
                 let instance =
                     Instance::new(*rc, Arc::new(lang.clone()), true, Kind::NovaPublicParams);
                 let pp = public_params(&instance)?;
-                Ok(proof.verify(&pp, public_inputs, public_outputs, *num_steps)?)
+                Ok(proof.verify(&pp, public_inputs, public_outputs)?)
             }
         }
     }

src/cli/repl/meta_cmd.rs

@@ -860,7 +860,6 @@ enum ProtocolProof<
     Nova {
         args: LurkData<F>,
         proof: nova::Proof<'a, F, C, M>,
-        num_steps: usize,
     },
 }
 
@@ -1074,21 +1073,8 @@ impl MetaCmd<F> {
             match load::<LurkProof<'_, _, _, MultiFrame<'_, _, Coproc<F>>>>(&proof_path(
                 &proof_key,
             ))? {
-                LurkProof::Nova {
-                    proof,
-                    public_inputs: _,
-                    public_outputs: _,
-                    num_steps,
-                    ..
-                } => {
-                    dump(
-                        ProtocolProof::Nova {
-                            args,
-                            proof,
-                            num_steps,
-                        },
-                        &path,
-                    )?;
+                LurkProof::Nova { proof, .. } => {
+                    dump(ProtocolProof::Nova { args, proof }, &path)?;
                     println!("Protocol proof saved at {path}");
                     Ok(())
                 }
@@ -1122,7 +1108,6 @@ impl MetaCmd<F> {
                 ProtocolProof::Nova {
                     args: LurkData { z_ptr, z_dag },
                     proof,
-                    num_steps,
                 } => {
                     let args =
                         z_dag.populate_store(&z_ptr, &repl.store, &mut Default::default())?;
@@ -1141,7 +1126,6 @@ impl MetaCmd<F> {
                         &pp,
                         &repl.store.to_scalar_vector(&cek_io[..3]),
                         &repl.store.to_scalar_vector(&cek_io[3..]),
-                        num_steps,
                     )? {
                         bail!("Proof verification failed")
                     }

src/cli/repl/mod.rs

@@ -317,13 +317,12 @@ impl Repl<F> {
                     info!("Compressing proof");
                     let proof = proof.compress(&pp)?;
                     assert_eq!(self.rc * num_steps, pad(n_frames, self.rc));
-                    assert!(proof.verify(&pp, &public_inputs, &public_outputs, num_steps)?);
+                    assert!(proof.verify(&pp, &public_inputs, &public_outputs)?);
 
                     let lurk_proof = LurkProof::Nova {
                         proof,
                         public_inputs,
                         public_outputs,
-                        num_steps,
                         rc: self.rc,
                         lang: (*self.lang).clone(),
                     };

src/proof/mod.rs

@@ -180,12 +180,6 @@ pub trait RecursiveSNARKTrait<
     /// Associated type for public parameters
     type PublicParams;
 
-    /// Main output of `prove_recursively`, encoding the actual proof
-    type ProveOutput;
-
-    /// Extra input for `verify` to be defined as needed
-    type ExtraVerifyInput;
-
     /// Type for error potentially thrown during verification
     type ErrorType;
 
@@ -197,20 +191,13 @@ pub trait RecursiveSNARKTrait<
         store: &'a M::Store,
         reduction_count: usize,
         lang: Arc<Lang<F, C>>,
-    ) -> Result<Self::ProveOutput, ProofError>;
+    ) -> Result<Self, ProofError>;
 
     /// Compress a proof
     fn compress(self, pp: &Self::PublicParams) -> Result<Self, ProofError>;
 
     /// Verify the proof given the public parameters, the input and output values
-    /// and the extra custom argument defined by who implements this trait.
-    fn verify(
-        &self,
-        pp: &Self::PublicParams,
-        z0: &[F],
-        zi: &[F],
-        extra: Self::ExtraVerifyInput,
-    ) -> Result<bool, Self::ErrorType>;
+    fn verify(&self, pp: &Self::PublicParams, z0: &[F], zi: &[F]) -> Result<bool, Self::ErrorType>;
 
     /// Return the `z0_secondary`
     #[inline]
@@ -257,18 +244,8 @@ pub trait Prover<'a, F: CurveCycleEquipped, C: Coprocessor<F> + 'a, M: MultiFram
     /// Associated type for public parameters
     type PublicParams;
 
-    /// Main output of `prove`, encoding the actual proof
-    type ProveOutput;
-
     /// Assiciated proof type, which must implement `RecursiveSNARKTrait`
-    type RecursiveSnark: RecursiveSNARKTrait<
-        'a,
-        F,
-        C,
-        M,
-        PublicParams = Self::PublicParams,
-        ProveOutput = Self::ProveOutput,
-    >;
+    type RecursiveSnark: RecursiveSNARKTrait<'a, F, C, M, PublicParams = Self::PublicParams>;
 
     /// Returns a reference to the prover's FoldingMode
     fn folding_mode(&self) -> &FoldingMode;
@@ -285,7 +262,7 @@ pub trait Prover<'a, F: CurveCycleEquipped, C: Coprocessor<F> + 'a, M: MultiFram
         pp: &Self::PublicParams,
         frames: &[M::EvalFrame],
         store: &'a M::Store,
-    ) -> Result<(Self::ProveOutput, Vec<F>, Vec<F>, usize), ProofError> {
+    ) -> Result<(Self::RecursiveSnark, Vec<F>, Vec<F>, usize), ProofError> {
         store.hydrate_z_cache();
         let z0 = M::io_to_scalar_vector(store, frames[0].input());
         let zi = M::io_to_scalar_vector(store, frames.last().unwrap().output());
@@ -318,7 +295,7 @@ pub trait Prover<'a, F: CurveCycleEquipped, C: Coprocessor<F> + 'a, M: MultiFram
         env: M::Ptr,
         store: &'a M::Store,
         limit: usize,
-    ) -> Result<(Self::ProveOutput, Vec<F>, Vec<F>, usize), ProofError> {
+    ) -> Result<(Self::RecursiveSnark, Vec<F>, Vec<F>, usize), ProofError> {
         let eval_config = self.folding_mode().eval_config(self.lang());
         let frames = M::build_frames(expr, env, store, limit, &eval_config)?;
         self.prove(pp, &frames, store)

src/proof/nova.rs

@@ -157,14 +157,18 @@ where
     <<E1<F> as Engine>::Scalar as ff::PrimeField>::Repr: Abomonation,
     <<E2<F> as Engine>::Scalar as ff::PrimeField>::Repr: Abomonation,
 {
-    /// A proof for the intermediate steps of a recursive computation
+    /// A proof for the intermediate steps of a recursive computation along with
+    /// the number of steps used for verification
     Recursive(
         Box<RecursiveSNARK<E1<F>, E2<F>, M, C2<F>>>,
+        usize,
         PhantomData<&'a C>,
     ),
-    /// A proof for the final step of a recursive computation
+    /// A proof for the final step of a recursive computation along with the number
+    /// of steps used for verification
     Compressed(
         Box<CompressedSNARK<E1<F>, E2<F>, M, C2<F>, SS1<F>, SS2<F>>>,
+        usize,
         PhantomData<&'a C>,
     ),
 }
@@ -235,11 +239,6 @@ where
 {
     type PublicParams = PublicParams<F, M>;
 
-    type ProveOutput = Self;
-
-    /// The number of steps
-    type ExtraVerifyInput = usize;
-
     type ErrorType = NovaError;
 
     #[tracing::instrument(skip_all, name = "nova::prove_recursively")]
@@ -261,7 +260,8 @@ where
         let (_circuit_primary, circuit_secondary): (M, TrivialCircuit<<E2<F> as Engine>::Scalar>) =
             circuits(reduction_count, lang);
 
-        tracing::debug!("steps.len: {}", steps.len());
+        let num_steps = steps.len();
+        tracing::debug!("steps.len: {num_steps}");
 
         // produce a recursive SNARK
         let mut recursive_snark: Option<RecursiveSNARK<E1<F>, E2<F>, M, C2<F>>> = None;
@@ -353,38 +353,38 @@ where
 
         Ok(Self::Recursive(
             Box::new(recursive_snark.unwrap()),
+            num_steps,
             PhantomData,
         ))
     }
 
     fn compress(self, pp: &PublicParams<F, M>) -> Result<Self, ProofError> {
-        match &self {
-            Self::Recursive(recursive_snark, _) => Ok(Self::Compressed(
+        match self {
+            Self::Recursive(recursive_snark, num_steps, _) => Ok(Self::Compressed(
                 Box::new(CompressedSNARK::<_, _, _, _, SS1<F>, SS2<F>>::prove(
                     &pp.pp,
                     &pp.pk,
-                    recursive_snark,
+                    &recursive_snark,
                 )?),
+                num_steps,
                 PhantomData,
             )),
             Self::Compressed(..) => Ok(self),
         }
     }
 
-    fn verify(
-        &self,
-        pp: &Self::PublicParams,
-        z0: &[F],
-        zi: &[F],
-        num_steps: usize,
-    ) -> Result<bool, Self::ErrorType> {
+    fn verify(&self, pp: &Self::PublicParams, z0: &[F], zi: &[F]) -> Result<bool, Self::ErrorType> {
         let (z0_primary, zi_primary) = (z0, zi);
         let z0_secondary = Self::z0_secondary();
         let zi_secondary = &z0_secondary;
 
         let (zi_primary_verified, zi_secondary_verified) = match self {
-            Self::Recursive(p, _) => p.verify(&pp.pp, num_steps, z0_primary, &z0_secondary)?,
-            Self::Compressed(p, _) => p.verify(&pp.vk, num_steps, z0_primary, &z0_secondary)?,
+            Self::Recursive(p, num_steps, _) => {
+                p.verify(&pp.pp, *num_steps, z0_primary, &z0_secondary)?
+            }
+            Self::Compressed(p, num_steps, _) => {
+                p.verify(&pp.vk, *num_steps, z0_primary, &z0_secondary)?
+            }
         };
 
         Ok(zi_primary == zi_primary_verified && zi_secondary == &zi_secondary_verified)
@@ -428,7 +428,6 @@ where
     <<E2<F> as Engine>::Scalar as ff::PrimeField>::Repr: Abomonation,
 {
     type PublicParams = PublicParams<F, M>;
-    type ProveOutput = Proof<'a, F, C, M>;
     type RecursiveSnark = Proof<'a, F, C, M>;
 
     #[inline]