Skip to content

Commit

Permalink
SuperNova: Improved RecursiveSNARK::verify (lurk-lang#114)
Browse files Browse the repository at this point in the history
* Use correct pp in RO

* Check validity of **all** instances
Only the last folded circuit was checked

* Additional checks + tidying
  • Loading branch information
adr1anh authored and porcuquine committed Nov 28, 2023
1 parent ea9d411 commit 54b95b7
Show file tree
Hide file tree
Showing 2 changed files with 78 additions and 47 deletions.
113 changes: 76 additions & 37 deletions src/supernova/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ use abomonation::Abomonation;
use abomonation_derive::Abomonation;
use ff::{Field, PrimeField};
use once_cell::sync::OnceCell;
use rayon::prelude::*;
use serde::{Deserialize, Serialize};
use tracing::debug;

Expand All @@ -43,13 +44,6 @@ use circuit::{

use self::error::SuperNovaError;

pub mod error;
pub mod snark;
pub(crate) mod utils;

#[cfg(test)]
mod test;

/// A struct that manages all the digests of the primary circuits of a SuperNova instance
#[derive(Clone, PartialEq, Eq, Serialize, Deserialize)]
pub struct CircuitDigests<G: Group> {
Expand Down Expand Up @@ -797,31 +791,69 @@ where
return Err(SuperNovaError::NovaError(NovaError::ProofVerifyError));
}

// check the (relaxed) R1CS instances public outputs.
if self.l_u_secondary.X.len() != 2 {
// Check lengths of r_primary
if self.r_U_primary.len() != self.num_augmented_circuits
|| self.r_W_primary.len() != self.num_augmented_circuits
{
debug!("r_primary length mismatch");
return Err(SuperNovaError::NovaError(NovaError::ProofVerifyError));
}

self.r_U_primary[circuit_index]
.as_ref()
.map_or(Ok(()), |U| {
if U.X.len() != 2 {
debug!("r_U_primary got instance length {:?} != {:?}", U.X.len(), 2);
// Check that there are no missing instance/witness pairs
self
.r_U_primary
.iter()
.zip(self.r_W_primary.iter())
.enumerate()
.try_for_each(|(i, (u, w))| match (u, w) {
(Some(_), Some(_)) | (None, None) => Ok(()),
_ => {
debug!("r_primary[{:?}]: mismatched instance/witness pair", i);
Err(SuperNovaError::NovaError(NovaError::ProofVerifyError))
} else {
Ok(())
}
})?;

if self.r_U_secondary.X.len() != 2 {
// check we have an instance/witness pair for the circuit_index
if self.r_U_primary[circuit_index].is_none() {
debug!(
"r_U_secondary got instance length {:?} != {:?}",
self.r_U_secondary.X.len(),
2
"r_primary[{:?}]: instance/witness pair is missing",
circuit_index
);
return Err(SuperNovaError::NovaError(NovaError::ProofVerifyError));
}

// check the (relaxed) R1CS instances public outputs.
{
for (i, r_U_primary_i) in self.r_U_primary.iter().enumerate() {
if let Some(u) = r_U_primary_i {
if u.X.len() != 2 {
debug!(
"r_U_primary[{:?}] got instance length {:?} != 2",
i,
u.X.len(),
);
return Err(SuperNovaError::NovaError(NovaError::ProofVerifyError));
}
}
}

if self.l_u_secondary.X.len() != 2 {
debug!(
"l_U_secondary got instance length {:?} != 2",
self.l_u_secondary.X.len(),
);
return Err(SuperNovaError::NovaError(NovaError::ProofVerifyError));
}

if self.r_U_secondary.X.len() != 2 {
debug!(
"r_U_secondary got instance length {:?} != 2",
self.r_U_secondary.X.len(),
);
return Err(SuperNovaError::NovaError(NovaError::ProofVerifyError));
}
}

let num_field_primary_ro = 3 // params_next, i_new, program_counter_new
+ 2 * pp[circuit_index].F_arity // zo, z1
+ (7 + 2 * pp.augmented_circuit_params_primary.get_n_limbs()); // # 1 * (7 + [X0, X1]*#num_limb)
Expand Down Expand Up @@ -857,11 +889,13 @@ where
for e in &self.zi_secondary {
hasher2.absorb(*e);
}
let default_value =
RelaxedR1CSInstance::default(&pp.ck_primary, &pp[circuit_index].r1cs_shape);
self.r_U_primary.iter().for_each(|U| {

self.r_U_primary.iter().enumerate().for_each(|(i, U)| {
U.as_ref()
.unwrap_or(&default_value)
.unwrap_or(&RelaxedR1CSInstance::default(
&pp.ck_primary,
&pp[i].r1cs_shape,
))
.absorb_in_ro(&mut hasher2);
});

Expand All @@ -886,21 +920,20 @@ where
return Err(SuperNovaError::NovaError(NovaError::ProofVerifyError));
}

// check the satisfiability of the provided `circuit_index` instance
let default_instance =
RelaxedR1CSInstance::default(&pp.ck_primary, &pp[circuit_index].r1cs_shape);
let default_witness = RelaxedR1CSWitness::default(&pp[circuit_index].r1cs_shape);
// check the satisfiability of all instance/witness pairs
let (res_r_primary, (res_r_secondary, res_l_secondary)) = rayon::join(
|| {
pp[circuit_index].r1cs_shape.is_sat_relaxed(
&pp.ck_primary,
self.r_U_primary[circuit_index]
.as_ref()
.unwrap_or(&default_instance),
self.r_W_primary[circuit_index]
.as_ref()
.unwrap_or(&default_witness),
)
self
.r_U_primary
.par_iter()
.zip(self.r_W_primary.par_iter())
.enumerate()
.try_for_each(|(i, (u, w))| {
if let (Some(u), Some(w)) = (u, w) {
pp[i].r1cs_shape.is_sat_relaxed(&pp.ck_primary, u, w)?
}
Ok(())
})
},
|| {
rayon::join(
Expand Down Expand Up @@ -1021,3 +1054,9 @@ pub fn circuit_digest<
let circuit_params = CircuitShape::new(cs.r1cs_shape(), F_arity);
circuit_params.digest()
}

pub mod error;
pub(crate) mod utils;

#[cfg(test)]
mod test;
12 changes: 2 additions & 10 deletions src/supernova/snark.rs
Original file line number Diff line number Diff line change
Expand Up @@ -498,11 +498,7 @@ mod test {
let secondary_circuit = TrivialSecondaryCircuit::default();
let test_circuits = TestCircuit::new(NUM_STEPS);

let pp = PublicParams::new(
&test_circuits[0],
&*S1::ck_floor(),
&*S2::ck_floor(),
);
let pp = PublicParams::new(&test_circuits[0], &*S1::ck_floor(), &*S2::ck_floor());

let initial_pc = G1::Scalar::ZERO;
let augmented_circuit_index = field_as_usize(initial_pc);
Expand Down Expand Up @@ -692,11 +688,7 @@ mod test {
let secondary_circuit = TrivialSecondaryCircuit::default();
let test_circuits = BigTestCircuit::new(NUM_STEPS);

let pp = PublicParams::new(
&test_circuits[0],
&*S1::ck_floor(),
&*S2::ck_floor(),
);
let pp = PublicParams::new(&test_circuits[0], &*S1::ck_floor(), &*S2::ck_floor());

let initial_pc = G1::Scalar::ZERO;
let augmented_circuit_index = field_as_usize(initial_pc);
Expand Down

0 comments on commit 54b95b7

Please sign in to comment.