diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 9a90f44..9c2fc63 100644 --- a/.github/workflows/rust.yml +++ b/.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 diff --git a/src/circuit.rs b/src/circuit.rs index 243212e..927dee7 100644 --- a/src/circuit.rs +++ b/src/circuit.rs @@ -93,9 +93,9 @@ where SC: StepCircuit, { params: NIFSVerifierCircuitParams, + ro_consts: ROConstantsCircuit, inputs: Option>, step_circuit: SC, // The function that is applied for each step - ro_consts: ROConstantsCircuit, } impl NIFSVerifierCircuit @@ -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, SynthesisError> { Ok(z) } + + fn compute(&self, z: &F) -> F { + *z + } } #[test] diff --git a/src/gadgets/ecc.rs b/src/gadgets/ecc.rs index 3e10353..85f72d3 100644 --- a/src/gadgets/ecc.rs +++ b/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) { diff --git a/src/lib.rs b/src/lib.rs index 73664a2..13e9d0f 100644 --- a/src/lib.rs +++ b/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, z0_primary: G1::Scalar, z0_secondary: G2::Scalar, + num_steps: usize, ) -> Result { // Execute the base case for the primary let mut cs_primary: SatisfyingAssignment = 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 = SatisfyingAssignment::new(); let inputs_secondary: NIFSVerifierCircuitInputs = 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 - pp.r1cs_shape_secondary - .is_sat(&pp.r1cs_gens_secondary, &u_secondary, &w_secondary) - .map_err(|_e| NovaError::UnSat)?; + // execute the remaining steps, alternating between G1 and G2 + let mut l_w_primary = w_primary; + let mut l_u_primary = u_primary; + 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, + ); - Ok(Self { - r_W_primary: RelaxedR1CSWitness::::default(&pp.r1cs_shape_primary), - r_U_primary: RelaxedR1CSInstance::::default( - &pp.r1cs_gens_primary, - &pp.r1cs_shape_primary, - ), - l_w_primary: w_primary, - l_u_primary: u_primary, - r_W_secondary: RelaxedR1CSWitness::::default(&pp.r1cs_shape_secondary), - r_U_secondary: RelaxedR1CSInstance::::default( + let mut r_W_secondary = RelaxedR1CSWitness::::default(&pp.r1cs_shape_secondary); + let mut r_U_secondary = + RelaxedR1CSInstance::::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, - ), - l_w_secondary: w_secondary, - l_u_secondary: u_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 = SatisfyingAssignment::new(); + let inputs_primary: NIFSVerifierCircuitInputs = NIFSVerifierCircuitInputs::new( + pp.r1cs_shape_secondary.get_digest(), + ::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 = 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 = SatisfyingAssignment::new(); + let inputs_secondary: NIFSVerifierCircuitInputs = NIFSVerifierCircuitInputs::new( + pp.r1cs_shape_primary.get_digest(), + ::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 = 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, + r_U_primary, + l_w_primary, + l_u_primary, + r_W_secondary, + r_U_secondary, + l_w_secondary, + l_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) -> 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, 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, ::Base::zero(), ::Base::zero(), + 3, ); assert!(res.is_ok()); let recursive_snark = res.unwrap(); diff --git a/src/nifs.rs b/src/nifs.rs index 0cbcfe4..45cd0d2 100644 --- a/src/nifs.rs +++ b/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 { - comm_T: CompressedCommitment, + pub(crate) comm_T: CompressedCommitment, _p: PhantomData, } diff --git a/src/r1cs.rs b/src/r1cs.rs index 51bcffa..c140e24 100644 --- a/src/r1cs.rs +++ b/src/r1cs.rs @@ -438,6 +438,14 @@ impl RelaxedR1CSWitness { } } + /// Initializes a new RelaxedR1CSWitness from an R1CSWitness + pub fn from_r1cs_witness(S: &R1CSShape, witness: &R1CSWitness) -> RelaxedR1CSWitness { + 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) -> (Commitment, Commitment) { (self.W.commit(&gens.gens_W), self.E.commit(&gens.gens_E)) @@ -483,6 +491,19 @@ impl RelaxedR1CSInstance { } } + /// Initializes a new RelaxedR1CSInstance from an R1CSInstance + pub fn from_r1cs_instance( + gens: &R1CSGens, + S: &R1CSShape, + instance: &R1CSInstance, + ) -> RelaxedR1CSInstance { + 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, diff --git a/src/traits.rs b/src/traits.rs index 136124f..b65698c 100644 --- a/src/traits.rs +++ b/src/traits.rs @@ -143,6 +143,9 @@ pub trait StepCircuit { cs: &mut CS, z: AllocatedNum, ) -> Result, SynthesisError>; + + /// Execute the circuit for a computation step and return output + fn compute(&self, z: &F) -> F; } impl AppendToTranscriptTrait for F {