From b6716eb7be3921fca2dcb85238ae843ee0ea9f2b Mon Sep 17 00:00:00 2001 From: porcuquine Date: Wed, 1 Nov 2023 18:34:44 -0700 Subject: [PATCH] Add non-deterministic ivc test. --- benches/recursive-snark-supernova.rs | 4 + src/supernova/mod.rs | 11 +- src/supernova/test.rs | 296 +++++++++++++++++++++++++++ src/traits/circuit_supernova.rs | 12 +- 4 files changed, 315 insertions(+), 8 deletions(-) diff --git a/benches/recursive-snark-supernova.rs b/benches/recursive-snark-supernova.rs index ca3fcd5e..e7bcf51c 100644 --- a/benches/recursive-snark-supernova.rs +++ b/benches/recursive-snark-supernova.rs @@ -339,6 +339,10 @@ where 1 } + fn circuit_index(&self) -> usize { + 0 + } + fn synthesize>( &self, cs: &mut CS, diff --git a/src/supernova/mod.rs b/src/supernova/mod.rs index b23a5cb2..56413b1a 100644 --- a/src/supernova/mod.rs +++ b/src/supernova/mod.rs @@ -168,8 +168,8 @@ where C2: StepCircuit, { /// Construct a new [PublicParams] - pub fn new>(non_unifrom_circuit: &NC) -> Self { - let num_circuits = non_unifrom_circuit.num_circuits(); + pub fn new>(non_uniform_circuit: &NC) -> Self { + let num_circuits = non_uniform_circuit.num_circuits(); let augmented_circuit_params_primary = SuperNovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true); @@ -179,7 +179,7 @@ where let circuit_shapes = (0..num_circuits) .map(|i| { - let c_primary = non_unifrom_circuit.primary_circuit(i); + let c_primary = non_uniform_circuit.primary_circuit(i); let F_arity = c_primary.arity(); // Initialize ck for the primary let circuit_primary: SuperNovaAugmentedCircuit<'_, G2, C1> = SuperNovaAugmentedCircuit::new( @@ -191,6 +191,7 @@ where ); let mut cs: ShapeCS = ShapeCS::new(); let _ = circuit_primary.synthesize(&mut cs); + // We use the largest commitment_key for all instances let r1cs_shape_primary = cs.r1cs_shape(); CircuitShape::new(r1cs_shape_primary, F_arity) @@ -202,7 +203,7 @@ where let augmented_circuit_params_secondary = SuperNovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false); let ro_consts_secondary: ROConstants = ROConstants::::default(); - let c_secondary = non_unifrom_circuit.secondary_circuit(); + let c_secondary = non_uniform_circuit.secondary_circuit(); let F_arity_secondary = c_secondary.arity(); let ro_consts_circuit_secondary: ROConstantsCircuit = ROConstantsCircuit::::default(); @@ -615,7 +616,7 @@ where let (l_u_primary, l_w_primary) = cs_primary .r1cs_instance_and_witness(&pp[circuit_index].r1cs_shape, &pp.ck_primary) - .map_err(|_| SuperNovaError::NovaError(NovaError::UnSat))?; + .map_err(SuperNovaError::NovaError)?; // Split into `if let`/`else` statement // to avoid `returns a value referencing data owned by closure` error on `&RelaxedR1CSInstance::default` and `RelaxedR1CSWitness::default` diff --git a/src/supernova/test.rs b/src/supernova/test.rs index e08d32d1..bdad3a0d 100644 --- a/src/supernova/test.rs +++ b/src/supernova/test.rs @@ -733,3 +733,299 @@ fn test_supernova_pp_digest() { "3ae4759aa0338bcc6ac11b456c17803467a1f44364992e3f1a0c6344b0135703", ); } + +// y is a non-deterministic hint representing the cube root of the input at a step. +#[derive(Clone, Debug)] +struct CubeRootCheckingCircuit { + y: Option, +} + +impl StepCircuit for CubeRootCheckingCircuit +where + F: PrimeField, +{ + fn arity(&self) -> usize { + 1 + } + + fn circuit_index(&self) -> usize { + 0 + } + + fn synthesize>( + &self, + cs: &mut CS, + _pc: Option<&AllocatedNum>, + z: &[AllocatedNum], + ) -> Result<(Option>, Vec>), SynthesisError> { + let x = &z[0]; + + // we allocate a variable and set it to the provided non-deterministic hint. + let y = AllocatedNum::alloc(cs.namespace(|| "y"), || { + self.y.ok_or(SynthesisError::AssignmentMissing) + })?; + + // We now check if y = x^{1/3} by checking if y^3 = x + let y_sq = y.square(cs.namespace(|| "y_sq"))?; + let y_cube = y_sq.mul(cs.namespace(|| "y_cube"), &y)?; + + cs.enforce( + || "y^3 = x", + |lc| lc + y_cube.get_variable(), + |lc| lc + CS::one(), + |lc| lc + x.get_variable(), + ); + + let next_pc = alloc_const(&mut cs.namespace(|| "next_pc"), F::ONE)?; + + Ok((Some(next_pc), vec![y])) + } +} + +// y is a non-deterministic hint representing the fifth root of the input at a step. +#[derive(Clone, Debug)] +struct FifthRootCheckingCircuit { + y: Option, +} + +impl StepCircuit for FifthRootCheckingCircuit +where + F: PrimeField, +{ + fn arity(&self) -> usize { + 1 + } + + fn circuit_index(&self) -> usize { + 1 + } + + fn synthesize>( + &self, + cs: &mut CS, + _pc: Option<&AllocatedNum>, + z: &[AllocatedNum], + ) -> Result<(Option>, Vec>), SynthesisError> { + let x = &z[0]; + + // we allocate a variable and set it to the provided non-deterministic hint. + let y = AllocatedNum::alloc(cs.namespace(|| "y"), || { + self.y.ok_or(SynthesisError::AssignmentMissing) + })?; + + // We now check if y = x^{1/5} by checking if y^5 = x + let y_sq = y.square(cs.namespace(|| "y_sq"))?; + let y_quad = y_sq.square(cs.namespace(|| "y_quad"))?; + let y_pow_5 = y_quad.mul(cs.namespace(|| "y_fifth"), &y)?; + + cs.enforce( + || "y^5 = x", + |lc| lc + y_pow_5.get_variable(), + |lc| lc + CS::one(), + |lc| lc + x.get_variable(), + ); + + let next_pc = alloc_const(&mut cs.namespace(|| "next_pc"), F::ZERO)?; + + Ok((Some(next_pc), vec![y])) + } +} + +#[derive(Clone, Debug)] +enum RootCheckingCircuit { + Cube(CubeRootCheckingCircuit), + Fifth(FifthRootCheckingCircuit), +} + +impl RootCheckingCircuit { + fn new(num_steps: usize) -> (Vec, Vec) { + let mut powers = Vec::new(); + let rng = &mut rand::rngs::OsRng; + let mut seed = F::random(rng); + + for i in 0..num_steps + 1 { + let seed_sq = seed.clone().square(); + // Cube-root and fifth-root circuits alternate. We compute the hints backward, so the calculations appear to be + // associated with the 'wrong' circuit. The final circuit is discarded, and only the final seed is used (as z_0). + powers.push(if i % 2 == num_steps % 2 { + seed *= seed_sq; + Self::Fifth(FifthRootCheckingCircuit { y: Some(seed) }) + } else { + seed *= seed_sq.clone().square(); + Self::Cube(CubeRootCheckingCircuit { y: Some(seed) }) + }) + } + + // reverse the powers to get roots + let roots = powers.into_iter().rev().collect::>(); + (vec![roots[0].get_y().unwrap()], roots[1..].to_vec()) + } + + fn get_y(&self) -> Option { + match self { + Self::Fifth(x) => x.y, + Self::Cube(x) => x.y, + } + } +} + +impl StepCircuit for RootCheckingCircuit +where + F: PrimeField, +{ + fn arity(&self) -> usize { + 1 + } + + fn circuit_index(&self) -> usize { + match self { + Self::Cube(x) => x.circuit_index(), + Self::Fifth(x) => x.circuit_index(), + } + } + + fn synthesize>( + &self, + cs: &mut CS, + pc: Option<&AllocatedNum>, + z: &[AllocatedNum], + ) -> Result<(Option>, Vec>), SynthesisError> { + match self { + Self::Cube(c) => c.synthesize(cs, pc, z), + Self::Fifth(c) => c.synthesize(cs, pc, z), + } + } +} + +impl + NonUniformCircuit, TrivialSecondaryCircuit> + for RootCheckingCircuit +where + G1: Group::Scalar>, + G2: Group::Scalar>, +{ + fn num_circuits(&self) -> usize { + 2 + } + + fn primary_circuit(&self, circuit_index: usize) -> Self { + match circuit_index { + 0 => Self::Cube(CubeRootCheckingCircuit { y: None }), + 1 => Self::Fifth(FifthRootCheckingCircuit { y: None }), + _ => unreachable!(), + } + } + + fn secondary_circuit(&self) -> TrivialSecondaryCircuit { + TrivialSecondaryCircuit::::default() + } +} + +fn test_nivc_nondet_with() +where + G1: Group::Scalar>, + G2: Group::Scalar>, + // this is due to the reliance on Abomonation + <::Scalar as PrimeField>::Repr: Abomonation, + <::Scalar as PrimeField>::Repr: Abomonation, +{ + let circuit_secondary = TrivialSecondaryCircuit::default(); + + let num_steps = 3; + + // produce non-deterministic hint + let (z0_primary, roots) = RootCheckingCircuit::new(num_steps); + assert_eq!(num_steps, roots.len()); + let z0_secondary = vec![::Scalar::ZERO]; + + // produce public parameters + let pp = PublicParams::< + G1, + G2, + RootCheckingCircuit<::Scalar>, + TrivialSecondaryCircuit<::Scalar>, + >::new(&roots[0]); + // produce a recursive SNARK + + let circuit_primary = &roots[0]; + let mut recursive_snark = RecursiveSNARK::::iter_base_step( + &pp, + circuit_primary.circuit_index(), + circuit_primary, + &circuit_secondary, + Some(G1::Scalar::from(circuit_primary.circuit_index() as u64)), + circuit_primary.circuit_index(), + 2, + &z0_primary, + &z0_secondary, + ) + .map_err(|err| { + print_constraints_name_on_error_index( + &err, + &pp, + circuit_primary, + &circuit_secondary, + as NonUniformCircuit< + G1, + G2, + RootCheckingCircuit, + TrivialSecondaryCircuit, + >>::num_circuits(circuit_primary), + ) + }) + .unwrap(); + + for circuit_primary in roots.iter().take(num_steps) { + let res = recursive_snark.prove_step( + &pp, + circuit_primary.circuit_index(), + circuit_primary, + &circuit_secondary, + ); + assert!(res + .map_err(|err| { + print_constraints_name_on_error_index( + &err, + &pp, + circuit_primary, + &circuit_secondary, + as NonUniformCircuit< + G1, + G2, + RootCheckingCircuit, + TrivialSecondaryCircuit, + >>::num_circuits(circuit_primary), + ) + }) + .is_ok()); + + // verify the recursive SNARK + let res = recursive_snark + .verify(&pp, 0, &z0_primary, &z0_secondary) + .map_err(|err| { + print_constraints_name_on_error_index( + &err, + &pp, + circuit_primary, + &circuit_secondary, + as NonUniformCircuit< + G1, + G2, + RootCheckingCircuit, + TrivialSecondaryCircuit, + >>::num_circuits(circuit_primary), + ) + }); + assert!(res.is_ok()); + } +} + +#[test] +fn test_nivc_nondet() { + type G1 = pasta_curves::pallas::Point; + type G2 = pasta_curves::vesta::Point; + + test_nivc_nondet_with::(); + test_nivc_nondet_with::(); + test_nivc_nondet_with::(); +} diff --git a/src/traits/circuit_supernova.rs b/src/traits/circuit_supernova.rs index 1da4cb49..29d6fe0f 100644 --- a/src/traits/circuit_supernova.rs +++ b/src/traits/circuit_supernova.rs @@ -13,9 +13,7 @@ pub trait StepCircuit: Send + Sync + Clone { fn arity(&self) -> usize; /// Return this `StepCircuit`'s assigned index, for use when enforcing the program counter. - fn circuit_index(&self) -> usize { - 0 - } + fn circuit_index(&self) -> usize; /// Sythesize the circuit for a computation step and return variable /// that corresponds to the output of the step `pc_{i+1}` and `z_{i+1}` @@ -70,6 +68,10 @@ where 1 } + fn circuit_index(&self) -> usize { + 0 + } + fn synthesize>( &self, _cs: &mut CS, @@ -96,6 +98,10 @@ where 1 } + fn circuit_index(&self) -> usize { + 0 + } + fn synthesize>( &self, _cs: &mut CS,