From 83f2e079a807547c9c5e10fced56dc8c4dadd3a4 Mon Sep 17 00:00:00 2001 From: Srinath Setty Date: Mon, 3 Apr 2023 18:33:38 -0700 Subject: [PATCH] support proving step circuits with final snark (#159) --- Cargo.toml | 2 +- src/r1cs.rs | 13 +++ src/spartan/pp/mod.rs | 259 +++++++++++++++++++++++++++++++++++++++++- 3 files changed, 271 insertions(+), 3 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index d48b839..aa6871e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "nova-snark" -version = "0.20.0" +version = "0.20.1" authors = ["Srinath Setty "] edition = "2021" description = "Recursive zkSNARKs without trusted setup" diff --git a/src/r1cs.rs b/src/r1cs.rs index 81a1af8..8fed9c5 100644 --- a/src/r1cs.rs +++ b/src/r1cs.rs @@ -578,6 +578,19 @@ impl RelaxedR1CSInstance { r_instance } + /// Initializes a new RelaxedR1CSInstance from an R1CSInstance + pub fn from_r1cs_instance_unchecked( + comm_W: &Commitment, + X: &[G::Scalar], + ) -> RelaxedR1CSInstance { + RelaxedR1CSInstance { + comm_W: *comm_W, + comm_E: Commitment::::default(), + u: G::Scalar::one(), + X: X.to_vec(), + } + } + /// Folds an incoming RelaxedR1CSInstance into the current one pub fn fold( &self, diff --git a/src/spartan/pp/mod.rs b/src/spartan/pp/mod.rs index 7710b35..596aeb8 100644 --- a/src/spartan/pp/mod.rs +++ b/src/spartan/pp/mod.rs @@ -1,6 +1,11 @@ //! This module implements RelaxedR1CSSNARK traits using a spark-based approach to prove evaluations of //! sparse multilinear polynomials involved in Spartan's sum-check protocol, thereby providing a preprocessing SNARK use crate::{ + bellperson::{ + r1cs::{NovaShape, NovaWitness}, + shape_cs::ShapeCS, + solver::SatisfyingAssignment, + }, errors::NovaError, r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness}, spartan::{ @@ -10,12 +15,13 @@ use crate::{ PolyEvalInstance, PolyEvalWitness, }, traits::{ - commitment::CommitmentEngineTrait, evaluation::EvaluationEngineTrait, + circuit::StepCircuit, commitment::CommitmentEngineTrait, evaluation::EvaluationEngineTrait, snark::RelaxedR1CSSNARKTrait, Group, TranscriptEngineTrait, TranscriptReprTrait, }, Commitment, CommitmentKey, }; -use core::cmp::max; +use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError}; +use core::{cmp::max, marker::PhantomData}; use ff::Field; use itertools::concat; use rayon::prelude::*; @@ -1315,3 +1321,252 @@ impl> RelaxedR1CSSNARKTrait> { + z_i: Option>, // inputs to the circuit + sc: SC, // step circuit to be executed +} + +impl> Circuit for SpartanCircuit { + fn synthesize>(self, cs: &mut CS) -> Result<(), SynthesisError> { + // obtain the arity information + let arity = self.sc.arity(); + + // Allocate zi. If inputs.zi is not provided, allocate default value 0 + let zero = vec![G::Scalar::zero(); arity]; + let z_i = (0..arity) + .map(|i| { + AllocatedNum::alloc(cs.namespace(|| format!("zi_{i}")), || { + Ok(self.z_i.as_ref().unwrap_or(&zero)[i]) + }) + }) + .collect::>, _>>()?; + + let z_i_plus_one = self.sc.synthesize(&mut cs.namespace(|| "F"), &z_i)?; + + // inputize both z_i and z_i_plus_one + for (j, input) in z_i.iter().enumerate().take(arity) { + let _ = input.inputize(cs.namespace(|| format!("input {j}"))); + } + for (j, output) in z_i_plus_one.iter().enumerate().take(arity) { + let _ = output.inputize(cs.namespace(|| format!("output {j}"))); + } + + Ok(()) + } +} + +/// A type that holds Spartan's prover key +pub struct SpartanProverKey +where + G: Group, + EE: EvaluationEngineTrait, +{ + F_arity: usize, + S: R1CSShape, + ck: CommitmentKey, + pk: ProverKey, +} + +/// A type that holds Spartan's verifier key +pub struct SpartanVerifierKey +where + G: Group, + EE: EvaluationEngineTrait, +{ + F_arity: usize, + vk: VerifierKey, +} + +/// A direct SNARK proving a step circuit +#[derive(Serialize, Deserialize)] +#[serde(bound = "")] +pub struct SpartanSNARK +where + G: Group, + EE: EvaluationEngineTrait, + C: StepCircuit, +{ + comm_W: Commitment, // commitment to the witness + snark: RelaxedR1CSSNARK, // snark proving the witness is satisfying + _p: PhantomData, +} + +impl, C: StepCircuit> + SpartanSNARK +{ + /// Produces prover and verifier keys for Spartan + pub fn setup(sc: C) -> Result<(SpartanProverKey, SpartanVerifierKey), NovaError> { + let F_arity = sc.arity(); + + // construct a circuit that can be synthesized + let circuit: SpartanCircuit = SpartanCircuit { z_i: None, sc }; + + let mut cs: ShapeCS = ShapeCS::new(); + let _ = circuit.synthesize(&mut cs); + let (S, ck) = cs.r1cs_shape(); + + let (pk, vk) = RelaxedR1CSSNARK::setup(&ck, &S)?; + + let pk = SpartanProverKey { F_arity, S, ck, pk }; + + let vk = SpartanVerifierKey { F_arity, vk }; + + Ok((pk, vk)) + } + + /// Produces a proof of satisfiability of the provided circuit + pub fn prove( + pk: &SpartanProverKey, + sc: C, + z_i: Vec, + ) -> Result { + if z_i.len() != pk.F_arity || sc.output(&z_i).len() != pk.F_arity { + return Err(NovaError::InvalidInitialInputLength); + } + + let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); + + let circuit: SpartanCircuit = SpartanCircuit { z_i: Some(z_i), sc }; + + let _ = circuit.synthesize(&mut cs); + let (u, w) = cs + .r1cs_instance_and_witness(&pk.S, &pk.ck) + .map_err(|_e| NovaError::UnSat)?; + + // convert the instance and witness to relaxed form + let (u_relaxed, w_relaxed) = ( + RelaxedR1CSInstance::from_r1cs_instance_unchecked(&u.comm_W, &u.X), + RelaxedR1CSWitness::from_r1cs_witness(&pk.S, &w), + ); + + // prove the instance using Spartan + let snark = RelaxedR1CSSNARK::prove(&pk.ck, &pk.pk, &u_relaxed, &w_relaxed)?; + + Ok(SpartanSNARK { + comm_W: u.comm_W, + snark, + _p: Default::default(), + }) + } + + /// Verifies a proof of satisfiability + pub fn verify( + &self, + vk: &SpartanVerifierKey, + z_i: Vec, + z_i_plus_one: Vec, + ) -> Result<(), NovaError> { + // check if z_i and z_i_plus_one have lengths according to the provided arity + if z_i.len() != vk.F_arity || z_i_plus_one.len() != vk.F_arity { + return Err(NovaError::InvalidInitialInputLength); + } + + // construct an instance using the provided commitment to the witness and z_i and z_{i+1} + let u_relaxed = RelaxedR1CSInstance::from_r1cs_instance_unchecked( + &self.comm_W, + &z_i + .into_iter() + .chain(z_i_plus_one.into_iter()) + .collect::>(), + ); + + // verify the snark using the constructed instance + self.snark.verify(&vk.vk, &u_relaxed)?; + + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use super::*; + type G = pasta_curves::pallas::Point; + type EE = crate::provider::ipa_pc::EvaluationEngine; + use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; + use core::marker::PhantomData; + use ff::PrimeField; + + #[derive(Clone, Debug, Default)] + struct CubicCircuit { + _p: PhantomData, + } + + impl StepCircuit for CubicCircuit + where + F: PrimeField, + { + fn arity(&self) -> usize { + 1 + } + + fn synthesize>( + &self, + cs: &mut CS, + z: &[AllocatedNum], + ) -> Result>, SynthesisError> { + // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output. + let x = &z[0]; + let x_sq = x.square(cs.namespace(|| "x_sq"))?; + let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), x)?; + let y = AllocatedNum::alloc(cs.namespace(|| "y"), || { + Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64)) + })?; + + cs.enforce( + || "y = x^3 + x + 5", + |lc| { + lc + x_cu.get_variable() + + x.get_variable() + + CS::one() + + CS::one() + + CS::one() + + CS::one() + + CS::one() + }, + |lc| lc + CS::one(), + |lc| lc + y.get_variable(), + ); + + Ok(vec![y]) + } + + fn output(&self, z: &[F]) -> Vec { + vec![z[0] * z[0] * z[0] + z[0] + F::from(5u64)] + } + } + + #[test] + fn test_spartan_snark() { + let circuit = CubicCircuit::default(); + + // produce keys + let (pk, vk) = + SpartanSNARK::::Scalar>>::setup(circuit.clone()).unwrap(); + + let num_steps = 3; + + // setup inputs + let z0 = vec![::Scalar::zero()]; + let mut z_i = z0; + + for _i in 0..num_steps { + // produce a SNARK + let res = SpartanSNARK::prove(&pk, circuit.clone(), z_i.clone()); + assert!(res.is_ok()); + + let z_i_plus_one = circuit.output(&z_i); + + let snark = res.unwrap(); + + // verify the SNARK + let res = snark.verify(&vk, z_i.clone(), z_i_plus_one.clone()); + assert!(res.is_ok()); + + // set input to the next step + z_i = z_i_plus_one.clone(); + } + + // sanity: check the claimed output with a direct computation of the same + assert_eq!(z_i, vec![::Scalar::from(2460515u64)]); + } +}