diff --git a/benches/compressed-snark.rs b/benches/compressed-snark.rs index 4ae9741..4effe26 100644 --- a/benches/compressed-snark.rs +++ b/benches/compressed-snark.rs @@ -17,8 +17,8 @@ type G1 = pasta_curves::pallas::Point; type G2 = pasta_curves::vesta::Point; type EE1 = nova_snark::provider::ipa_pc::EvaluationEngine; type EE2 = nova_snark::provider::ipa_pc::EvaluationEngine; -type S1 = nova_snark::spartan::RelaxedR1CSSNARK; -type S2 = nova_snark::spartan::RelaxedR1CSSNARK; +type S1 = nova_snark::spartan::snark::RelaxedR1CSSNARK; +type S2 = nova_snark::spartan::snark::RelaxedR1CSSNARK; type C1 = NonTrivialTestCircuit<::Scalar>; type C2 = TrivialTestCircuit<::Scalar>; diff --git a/examples/minroot.rs b/examples/minroot.rs index 3220417..75c2d41 100644 --- a/examples/minroot.rs +++ b/examples/minroot.rs @@ -262,8 +262,8 @@ fn main() { let start = Instant::now(); type EE1 = nova_snark::provider::ipa_pc::EvaluationEngine; type EE2 = nova_snark::provider::ipa_pc::EvaluationEngine; - type S1 = nova_snark::spartan::RelaxedR1CSSNARK; - type S2 = nova_snark::spartan::RelaxedR1CSSNARK; + type S1 = nova_snark::spartan::snark::RelaxedR1CSSNARK; + type S2 = nova_snark::spartan::snark::RelaxedR1CSSNARK; let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &pk, &recursive_snark); println!( diff --git a/src/lib.rs b/src/lib.rs index 0509f0f..bc48c93 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -799,10 +799,10 @@ mod tests { use super::*; type EE1 = provider::ipa_pc::EvaluationEngine; type EE2 = provider::ipa_pc::EvaluationEngine; - type S1 = spartan::RelaxedR1CSSNARK>; - type S2 = spartan::RelaxedR1CSSNARK>; - type S1Prime = spartan::pp::RelaxedR1CSSNARK>; - type S2Prime = spartan::pp::RelaxedR1CSSNARK>; + type S1 = spartan::snark::RelaxedR1CSSNARK>; + type S2 = spartan::snark::RelaxedR1CSSNARK>; + type S1Prime = spartan::ppsnark::RelaxedR1CSSNARK>; + type S2Prime = spartan::ppsnark::RelaxedR1CSSNARK>; use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError}; use core::marker::PhantomData; diff --git a/src/spartan/direct.rs b/src/spartan/direct.rs new file mode 100644 index 0000000..6122299 --- /dev/null +++ b/src/spartan/direct.rs @@ -0,0 +1,265 @@ +//! This module provides interfaces to directly prove a step circuit by using Spartan SNARK. +//! In particular, it supports any SNARK that implements RelaxedR1CSSNARK trait +//! (e.g., with the SNARKs implemented in ppsnark.rs or snark.rs). +use crate::{ + bellperson::{ + r1cs::{NovaShape, NovaWitness}, + shape_cs::ShapeCS, + solver::SatisfyingAssignment, + }, + errors::NovaError, + r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness}, + traits::{circuit::StepCircuit, snark::RelaxedR1CSSNARKTrait, Group}, + Commitment, CommitmentKey, +}; +use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError}; +use core::marker::PhantomData; +use ff::Field; +use serde::{Deserialize, Serialize}; + +struct DirectCircuit> { + z_i: Option>, // inputs to the circuit + sc: SC, // step circuit to be executed +} + +impl> Circuit for DirectCircuit { + 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 the prover key +#[derive(Clone, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct ProverKey +where + G: Group, + S: RelaxedR1CSSNARKTrait, +{ + S: R1CSShape, + ck: CommitmentKey, + pk: S::ProverKey, +} + +/// A type that holds the verifier key +#[derive(Clone, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct VerifierKey +where + G: Group, + S: RelaxedR1CSSNARKTrait, +{ + vk: S::VerifierKey, +} + +/// A direct SNARK proving a step circuit +#[derive(Clone, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct DirectSNARK +where + G: Group, + S: RelaxedR1CSSNARKTrait, + C: StepCircuit, +{ + comm_W: Commitment, // commitment to the witness + snark: S, // snark proving the witness is satisfying + _p: PhantomData, +} + +impl, C: StepCircuit> DirectSNARK { + /// Produces prover and verifier keys for the direct SNARK + pub fn setup(sc: C) -> Result<(ProverKey, VerifierKey), NovaError> { + // construct a circuit that can be synthesized + let circuit: DirectCircuit = DirectCircuit { z_i: None, sc }; + + let mut cs: ShapeCS = ShapeCS::new(); + let _ = circuit.synthesize(&mut cs); + let (shape, ck) = cs.r1cs_shape(); + + let (pk, vk) = S::setup(&ck, &shape)?; + + let pk = ProverKey { S: shape, ck, pk }; + + let vk = VerifierKey { vk }; + + Ok((pk, vk)) + } + + /// Produces a proof of satisfiability of the provided circuit + pub fn prove(pk: &ProverKey, sc: C, z_i: &[G::Scalar]) -> Result { + let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); + + let circuit: DirectCircuit = DirectCircuit { + z_i: Some(z_i.to_vec()), + 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 = S::prove(&pk.ck, &pk.pk, &u_relaxed, &w_relaxed)?; + + Ok(DirectSNARK { + comm_W: u.comm_W, + snark, + _p: Default::default(), + }) + } + + /// Verifies a proof of satisfiability + pub fn verify(&self, vk: &VerifierKey, io: &[G::Scalar]) -> Result<(), NovaError> { + // 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, io); + + // verify the snark using the constructed instance + self.snark.verify(&vk.vk, &u_relaxed)?; + + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::provider::bn256_grumpkin::bn256; + 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_direct_snark() { + type G = pasta_curves::pallas::Point; + type EE = crate::provider::ipa_pc::EvaluationEngine; + type S = crate::spartan::snark::RelaxedR1CSSNARK; + type Spp = crate::spartan::ppsnark::RelaxedR1CSSNARK; + test_direct_snark_with::(); + test_direct_snark_with::(); + + type G2 = bn256::Point; + type EE2 = crate::provider::ipa_pc::EvaluationEngine; + type S2 = crate::spartan::snark::RelaxedR1CSSNARK; + type S2pp = crate::spartan::ppsnark::RelaxedR1CSSNARK; + test_direct_snark_with::(); + test_direct_snark_with::(); + } + + fn test_direct_snark_with>() { + let circuit = CubicCircuit::default(); + + // produce keys + let (pk, vk) = + DirectSNARK::::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 = DirectSNARK::prove(&pk, circuit.clone(), &z_i); + assert!(res.is_ok()); + + let z_i_plus_one = circuit.output(&z_i); + + let snark = res.unwrap(); + + // verify the SNARK + let io = z_i + .clone() + .into_iter() + .chain(z_i_plus_one.clone().into_iter()) + .collect::>(); + let res = snark.verify(&vk, &io); + 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)]); + } +} diff --git a/src/spartan/mod.rs b/src/spartan/mod.rs index e3c4c01..a8ef022 100644 --- a/src/spartan/mod.rs +++ b/src/spartan/mod.rs @@ -1,25 +1,18 @@ //! This module implements RelaxedR1CSSNARKTrait using Spartan that is generic //! over the polynomial commitment and evaluation argument (i.e., a PCS) +//! We provide two implementations, one in snark.rs (which does not use any preprocessing) +//! and another in ppsnark.rs (which uses preprocessing to keep the verifier's state small if the PCS scheme provides a succinct verifier) +//! We also provide direct.rs that allows proving a step circuit directly with either of the two SNARKs. +pub mod direct; mod math; pub(crate) mod polynomial; -pub mod pp; +pub mod ppsnark; +pub mod snark; mod sumcheck; -use crate::{ - compute_digest, - errors::NovaError, - r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness}, - traits::{ - evaluation::EvaluationEngineTrait, snark::RelaxedR1CSSNARKTrait, Group, TranscriptEngineTrait, - }, - Commitment, CommitmentKey, -}; +use crate::{traits::Group, Commitment}; use ff::Field; -use itertools::concat; -use polynomial::{EqPolynomial, MultilinearPolynomial, SparsePolynomial}; -use rayon::prelude::*; -use serde::{Deserialize, Serialize}; -use sumcheck::SumcheckProof; +use polynomial::SparsePolynomial; fn powers(s: &G::Scalar, n: usize) -> Vec { assert!(n >= 1); @@ -123,510 +116,3 @@ impl PolyEvalInstance { } } } - -/// A type that represents the prover's key -#[derive(Serialize, Deserialize)] -#[serde(bound = "")] -pub struct ProverKey> { - pk_ee: EE::ProverKey, - S: R1CSShape, - vk_digest: G::Scalar, // digest of the verifier's key -} - -/// A type that represents the verifier's key -#[derive(Serialize, Deserialize)] -#[serde(bound = "")] -pub struct VerifierKey> { - vk_ee: EE::VerifierKey, - S: R1CSShape, - digest: G::Scalar, -} - -/// A succinct proof of knowledge of a witness to a relaxed R1CS instance -/// The proof is produced using Spartan's combination of the sum-check and -/// the commitment to a vector viewed as a polynomial commitment -#[derive(Serialize, Deserialize)] -#[serde(bound = "")] -pub struct RelaxedR1CSSNARK> { - sc_proof_outer: SumcheckProof, - claims_outer: (G::Scalar, G::Scalar, G::Scalar), - eval_E: G::Scalar, - sc_proof_inner: SumcheckProof, - eval_W: G::Scalar, - sc_proof_batch: SumcheckProof, - evals_batch: Vec, - eval_arg: EE::EvaluationArgument, -} - -impl> RelaxedR1CSSNARKTrait - for RelaxedR1CSSNARK -{ - type ProverKey = ProverKey; - type VerifierKey = VerifierKey; - - fn setup( - ck: &CommitmentKey, - S: &R1CSShape, - ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> { - let (pk_ee, vk_ee) = EE::setup(ck); - - let S = S.pad(); - - let vk = { - let mut vk = VerifierKey { - vk_ee, - S: S.clone(), - digest: G::Scalar::ZERO, - }; - vk.digest = compute_digest::>(&vk); - vk - }; - - let pk = ProverKey { - pk_ee, - S, - vk_digest: vk.digest, - }; - - Ok((pk, vk)) - } - - /// produces a succinct proof of satisfiability of a RelaxedR1CS instance - fn prove( - ck: &CommitmentKey, - pk: &Self::ProverKey, - U: &RelaxedR1CSInstance, - W: &RelaxedR1CSWitness, - ) -> Result { - let W = W.pad(&pk.S); // pad the witness - let mut transcript = G::TE::new(b"RelaxedR1CSSNARK"); - - // sanity check that R1CSShape has certain size characteristics - assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons); - assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars); - assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io); - assert!(pk.S.num_io < pk.S.num_vars); - - // append the digest of vk (which includes R1CS matrices) and the RelaxedR1CSInstance to the transcript - transcript.absorb(b"vk", &pk.vk_digest); - transcript.absorb(b"U", U); - - // compute the full satisfying assignment by concatenating W.W, U.u, and U.X - let mut z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]); - - let (num_rounds_x, num_rounds_y) = ( - (pk.S.num_cons as f64).log2() as usize, - ((pk.S.num_vars as f64).log2() as usize + 1), - ); - - // outer sum-check - let tau = (0..num_rounds_x) - .map(|_i| transcript.squeeze(b"t")) - .collect::, NovaError>>()?; - - let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals()); - let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = { - let (poly_Az, poly_Bz, poly_Cz) = pk.S.multiply_vec(&z)?; - let poly_uCz_E = (0..pk.S.num_cons) - .map(|i| U.u * poly_Cz[i] + W.E[i]) - .collect::>(); - ( - MultilinearPolynomial::new(poly_Az), - MultilinearPolynomial::new(poly_Bz), - MultilinearPolynomial::new(poly_Cz), - MultilinearPolynomial::new(poly_uCz_E), - ) - }; - - let comb_func_outer = - |poly_A_comp: &G::Scalar, - poly_B_comp: &G::Scalar, - poly_C_comp: &G::Scalar, - poly_D_comp: &G::Scalar| - -> G::Scalar { *poly_A_comp * (*poly_B_comp * *poly_C_comp - *poly_D_comp) }; - let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_additive_term( - &G::Scalar::ZERO, // claim is zero - num_rounds_x, - &mut poly_tau, - &mut poly_Az, - &mut poly_Bz, - &mut poly_uCz_E, - comb_func_outer, - &mut transcript, - )?; - - // claims from the end of sum-check - let (claim_Az, claim_Bz): (G::Scalar, G::Scalar) = (claims_outer[1], claims_outer[2]); - let claim_Cz = poly_Cz.evaluate(&r_x); - let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x); - transcript.absorb( - b"claims_outer", - &[claim_Az, claim_Bz, claim_Cz, eval_E].as_slice(), - ); - - // inner sum-check - let r = transcript.squeeze(b"r")?; - let claim_inner_joint = claim_Az + r * claim_Bz + r * r * claim_Cz; - - let poly_ABC = { - // compute the initial evaluation table for R(\tau, x) - let evals_rx = EqPolynomial::new(r_x.clone()).evals(); - - // Bounds "row" variables of (A, B, C) matrices viewed as 2d multilinear polynomials - let compute_eval_table_sparse = - |S: &R1CSShape, rx: &[G::Scalar]| -> (Vec, Vec, Vec) { - assert_eq!(rx.len(), S.num_cons); - - let inner = |M: &Vec<(usize, usize, G::Scalar)>, M_evals: &mut Vec| { - for (row, col, val) in M { - M_evals[*col] += rx[*row] * val; - } - }; - - let (A_evals, (B_evals, C_evals)) = rayon::join( - || { - let mut A_evals: Vec = vec![G::Scalar::ZERO; 2 * S.num_vars]; - inner(&S.A, &mut A_evals); - A_evals - }, - || { - rayon::join( - || { - let mut B_evals: Vec = vec![G::Scalar::ZERO; 2 * S.num_vars]; - inner(&S.B, &mut B_evals); - B_evals - }, - || { - let mut C_evals: Vec = vec![G::Scalar::ZERO; 2 * S.num_vars]; - inner(&S.C, &mut C_evals); - C_evals - }, - ) - }, - ); - - (A_evals, B_evals, C_evals) - }; - - let (evals_A, evals_B, evals_C) = compute_eval_table_sparse(&pk.S, &evals_rx); - - assert_eq!(evals_A.len(), evals_B.len()); - assert_eq!(evals_A.len(), evals_C.len()); - (0..evals_A.len()) - .into_par_iter() - .map(|i| evals_A[i] + r * evals_B[i] + r * r * evals_C[i]) - .collect::>() - }; - - let poly_z = { - z.resize(pk.S.num_vars * 2, G::Scalar::ZERO); - z - }; - - let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar { - *poly_A_comp * *poly_B_comp - }; - let (sc_proof_inner, r_y, _claims_inner) = SumcheckProof::prove_quad( - &claim_inner_joint, - num_rounds_y, - &mut MultilinearPolynomial::new(poly_ABC), - &mut MultilinearPolynomial::new(poly_z), - comb_func, - &mut transcript, - )?; - - // add additional claims about W and E polynomials to the list from CC - let mut w_u_vec = Vec::new(); - let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_y[1..]); - w_u_vec.push(( - PolyEvalWitness { p: W.W.clone() }, - PolyEvalInstance { - c: U.comm_W, - x: r_y[1..].to_vec(), - e: eval_W, - }, - )); - - w_u_vec.push(( - PolyEvalWitness { p: W.E }, - PolyEvalInstance { - c: U.comm_E, - x: r_x, - e: eval_E, - }, - )); - - // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point. - // For example, eval_W =? W(r_y[1..]) and eval_E =? E(r_x) into - // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz) - // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz), - // where gamma is a public challenge - // Since commitments to W and E are homomorphic, the verifier can compute a commitment - // to the batched polynomial. - assert!(w_u_vec.len() >= 2); - - let (w_vec, u_vec): (Vec>, Vec>) = - w_u_vec.into_iter().unzip(); - let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size - let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points - - // generate a challenge - let rho = transcript.squeeze(b"r")?; - let num_claims = w_vec_padded.len(); - let powers_of_rho = powers::(&rho, num_claims); - let claim_batch_joint = u_vec_padded - .iter() - .zip(powers_of_rho.iter()) - .map(|(u, p)| u.e * p) - .sum(); - - let mut polys_left: Vec> = w_vec_padded - .iter() - .map(|w| MultilinearPolynomial::new(w.p.clone())) - .collect(); - let mut polys_right: Vec> = u_vec_padded - .iter() - .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals())) - .collect(); - - let num_rounds_z = u_vec_padded[0].x.len(); - let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar { - *poly_A_comp * *poly_B_comp - }; - let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch( - &claim_batch_joint, - num_rounds_z, - &mut polys_left, - &mut polys_right, - &powers_of_rho, - comb_func, - &mut transcript, - )?; - - let (claims_batch_left, _): (Vec, Vec) = claims_batch; - - transcript.absorb(b"l", &claims_batch_left.as_slice()); - - // we now combine evaluation claims at the same point rz into one - let gamma = transcript.squeeze(b"g")?; - let powers_of_gamma: Vec = powers::(&gamma, num_claims); - let comm_joint = u_vec_padded - .iter() - .zip(powers_of_gamma.iter()) - .map(|(u, g_i)| u.c * *g_i) - .fold(Commitment::::default(), |acc, item| acc + item); - let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma); - let eval_joint = claims_batch_left - .iter() - .zip(powers_of_gamma.iter()) - .map(|(e, g_i)| *e * *g_i) - .sum(); - - let eval_arg = EE::prove( - ck, - &pk.pk_ee, - &mut transcript, - &comm_joint, - &poly_joint.p, - &r_z, - &eval_joint, - )?; - - Ok(RelaxedR1CSSNARK { - sc_proof_outer, - claims_outer: (claim_Az, claim_Bz, claim_Cz), - eval_E, - sc_proof_inner, - eval_W, - sc_proof_batch, - evals_batch: claims_batch_left, - eval_arg, - }) - } - - /// verifies a proof of satisfiability of a RelaxedR1CS instance - fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance) -> Result<(), NovaError> { - let mut transcript = G::TE::new(b"RelaxedR1CSSNARK"); - - // append the digest of R1CS matrices and the RelaxedR1CSInstance to the transcript - transcript.absorb(b"vk", &vk.digest); - transcript.absorb(b"U", U); - - let (num_rounds_x, num_rounds_y) = ( - (vk.S.num_cons as f64).log2() as usize, - ((vk.S.num_vars as f64).log2() as usize + 1), - ); - - // outer sum-check - let tau = (0..num_rounds_x) - .map(|_i| transcript.squeeze(b"t")) - .collect::, NovaError>>()?; - - let (claim_outer_final, r_x) = - self - .sc_proof_outer - .verify(G::Scalar::ZERO, num_rounds_x, 3, &mut transcript)?; - - // verify claim_outer_final - let (claim_Az, claim_Bz, claim_Cz) = self.claims_outer; - let taus_bound_rx = EqPolynomial::new(tau).evaluate(&r_x); - let claim_outer_final_expected = - taus_bound_rx * (claim_Az * claim_Bz - U.u * claim_Cz - self.eval_E); - if claim_outer_final != claim_outer_final_expected { - return Err(NovaError::InvalidSumcheckProof); - } - - transcript.absorb( - b"claims_outer", - &[ - self.claims_outer.0, - self.claims_outer.1, - self.claims_outer.2, - self.eval_E, - ] - .as_slice(), - ); - - // inner sum-check - let r = transcript.squeeze(b"r")?; - let claim_inner_joint = - self.claims_outer.0 + r * self.claims_outer.1 + r * r * self.claims_outer.2; - - let (claim_inner_final, r_y) = - self - .sc_proof_inner - .verify(claim_inner_joint, num_rounds_y, 2, &mut transcript)?; - - // verify claim_inner_final - let eval_Z = { - let eval_X = { - // constant term - let mut poly_X = vec![(0, U.u)]; - //remaining inputs - poly_X.extend( - (0..U.X.len()) - .map(|i| (i + 1, U.X[i])) - .collect::>(), - ); - SparsePolynomial::new((vk.S.num_vars as f64).log2() as usize, poly_X).evaluate(&r_y[1..]) - }; - (G::Scalar::ONE - r_y[0]) * self.eval_W + r_y[0] * eval_X - }; - - // compute evaluations of R1CS matrices - let multi_evaluate = |M_vec: &[&[(usize, usize, G::Scalar)]], - r_x: &[G::Scalar], - r_y: &[G::Scalar]| - -> Vec { - let evaluate_with_table = - |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar { - (0..M.len()) - .collect::>() - .par_iter() - .map(|&i| { - let (row, col, val) = M[i]; - T_x[row] * T_y[col] * val - }) - .reduce(|| G::Scalar::ZERO, |acc, x| acc + x) - }; - - let (T_x, T_y) = rayon::join( - || EqPolynomial::new(r_x.to_vec()).evals(), - || EqPolynomial::new(r_y.to_vec()).evals(), - ); - - (0..M_vec.len()) - .collect::>() - .par_iter() - .map(|&i| evaluate_with_table(M_vec[i], &T_x, &T_y)) - .collect() - }; - - let evals = multi_evaluate(&[&vk.S.A, &vk.S.B, &vk.S.C], &r_x, &r_y); - - let claim_inner_final_expected = (evals[0] + r * evals[1] + r * r * evals[2]) * eval_Z; - if claim_inner_final != claim_inner_final_expected { - return Err(NovaError::InvalidSumcheckProof); - } - - // add claims about W and E polynomials - let u_vec: Vec> = vec![ - PolyEvalInstance { - c: U.comm_W, - x: r_y[1..].to_vec(), - e: self.eval_W, - }, - PolyEvalInstance { - c: U.comm_E, - x: r_x, - e: self.eval_E, - }, - ]; - - let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points - - // generate a challenge - let rho = transcript.squeeze(b"r")?; - let num_claims = u_vec.len(); - let powers_of_rho = powers::(&rho, num_claims); - let claim_batch_joint = u_vec - .iter() - .zip(powers_of_rho.iter()) - .map(|(u, p)| u.e * p) - .sum(); - - let num_rounds_z = u_vec_padded[0].x.len(); - let (claim_batch_final, r_z) = - self - .sc_proof_batch - .verify(claim_batch_joint, num_rounds_z, 2, &mut transcript)?; - - let claim_batch_final_expected = { - let poly_rz = EqPolynomial::new(r_z.clone()); - let evals = u_vec_padded - .iter() - .map(|u| poly_rz.evaluate(&u.x)) - .collect::>(); - - evals - .iter() - .zip(self.evals_batch.iter()) - .zip(powers_of_rho.iter()) - .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i) - .sum() - }; - - if claim_batch_final != claim_batch_final_expected { - return Err(NovaError::InvalidSumcheckProof); - } - - transcript.absorb(b"l", &self.evals_batch.as_slice()); - - // we now combine evaluation claims at the same point rz into one - let gamma = transcript.squeeze(b"g")?; - let powers_of_gamma: Vec = powers::(&gamma, num_claims); - let comm_joint = u_vec_padded - .iter() - .zip(powers_of_gamma.iter()) - .map(|(u, g_i)| u.c * *g_i) - .fold(Commitment::::default(), |acc, item| acc + item); - let eval_joint = self - .evals_batch - .iter() - .zip(powers_of_gamma.iter()) - .map(|(e, g_i)| *e * *g_i) - .sum(); - - // verify - EE::verify( - &vk.vk_ee, - &mut transcript, - &comm_joint, - &r_z, - &eval_joint, - &self.eval_arg, - )?; - - Ok(()) - } -} diff --git a/src/spartan/pp.rs b/src/spartan/ppsnark.rs similarity index 89% rename from src/spartan/pp.rs rename to src/spartan/ppsnark.rs index 5c9018c..7d64c8c 100644 --- a/src/spartan/pp.rs +++ b/src/spartan/ppsnark.rs @@ -1,11 +1,8 @@ //! 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 +//! The verifier in this preprocessing SNARK maintains a commitment to R1CS matrices. This is beneficial when using a +//! polynomial commitment scheme in which the verifier's costs is succinct. use crate::{ - bellperson::{ - r1cs::{NovaShape, NovaWitness}, - shape_cs::ShapeCS, - solver::SatisfyingAssignment, - }, compute_digest, errors::NovaError, r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness}, @@ -17,7 +14,6 @@ use crate::{ PolyEvalInstance, PolyEvalWitness, SparsePolynomial, }, traits::{ - circuit::StepCircuit, commitment::{CommitmentEngineTrait, CommitmentTrait}, evaluation::EvaluationEngineTrait, snark::RelaxedR1CSSNARKTrait, @@ -25,7 +21,6 @@ use crate::{ }, Commitment, CommitmentKey, CompressedCommitment, }; -use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError}; use core::{cmp::max, marker::PhantomData}; use ff::{Field, PrimeField}; use itertools::concat; @@ -2045,245 +2040,3 @@ 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 -#[derive(Clone, Serialize, Deserialize)] -#[serde(bound = "")] -pub struct SpartanProverKey -where - G: Group, - EE: EvaluationEngineTrait, -{ - S: R1CSShape, - ck: CommitmentKey, - pk: ProverKey, -} - -/// A type that holds Spartan's verifier key -#[derive(Clone, Serialize, Deserialize)] -#[serde(bound = "")] -pub struct SpartanVerifierKey -where - G: Group, - EE: EvaluationEngineTrait, -{ - vk: VerifierKey, -} - -/// A direct SNARK proving a step circuit -#[derive(Clone, 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> { - // 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 { S, ck, pk }; - - let vk = SpartanVerifierKey { vk }; - - Ok((pk, vk)) - } - - /// Produces a proof of satisfiability of the provided circuit - pub fn prove(pk: &SpartanProverKey, sc: C, z_i: &[G::Scalar]) -> Result { - let mut cs: SatisfyingAssignment = SatisfyingAssignment::new(); - - let circuit: SpartanCircuit = SpartanCircuit { - z_i: Some(z_i.to_vec()), - 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, io: &[G::Scalar]) -> Result<(), NovaError> { - // 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, io); - - // verify the snark using the constructed instance - self.snark.verify(&vk.vk, &u_relaxed)?; - - Ok(()) - } -} - -#[cfg(test)] -mod tests { - use super::*; - use crate::provider::bn256_grumpkin::bn256; - 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() { - type G = pasta_curves::pallas::Point; - type EE = crate::provider::ipa_pc::EvaluationEngine; - - test_spartan_snark_with::(); - test_spartan_snark_with::<_, crate::provider::ipa_pc::EvaluationEngine>(); - } - - fn test_spartan_snark_with>() { - 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); - assert!(res.is_ok()); - - let z_i_plus_one = circuit.output(&z_i); - - let snark = res.unwrap(); - - // verify the SNARK - let io = z_i - .clone() - .into_iter() - .chain(z_i_plus_one.clone().into_iter()) - .collect::>(); - let res = snark.verify(&vk, &io); - 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)]); - } -} diff --git a/src/spartan/snark.rs b/src/spartan/snark.rs new file mode 100644 index 0000000..018765b --- /dev/null +++ b/src/spartan/snark.rs @@ -0,0 +1,532 @@ +//! This module implements RelaxedR1CSSNARKTrait using Spartan that is generic +//! over the polynomial commitment and evaluation argument (i.e., a PCS) +//! This version of Spartan does not use preprocessing so the verifier keeps the entire +//! description of R1CS matrices. This is essentially optimal for the verifier when using +//! an IPA-based polynomial commitment scheme. + +use crate::{ + compute_digest, + errors::NovaError, + r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness}, + spartan::{ + polynomial::{EqPolynomial, MultilinearPolynomial, SparsePolynomial}, + powers, + sumcheck::SumcheckProof, + PolyEvalInstance, PolyEvalWitness, + }, + traits::{ + evaluation::EvaluationEngineTrait, snark::RelaxedR1CSSNARKTrait, Group, TranscriptEngineTrait, + }, + Commitment, CommitmentKey, +}; +use ff::Field; +use itertools::concat; +use rayon::prelude::*; +use serde::{Deserialize, Serialize}; + +/// A type that represents the prover's key +#[derive(Serialize, Deserialize)] +#[serde(bound = "")] +pub struct ProverKey> { + pk_ee: EE::ProverKey, + S: R1CSShape, + vk_digest: G::Scalar, // digest of the verifier's key +} + +/// A type that represents the verifier's key +#[derive(Serialize, Deserialize)] +#[serde(bound = "")] +pub struct VerifierKey> { + vk_ee: EE::VerifierKey, + S: R1CSShape, + digest: G::Scalar, +} + +/// A succinct proof of knowledge of a witness to a relaxed R1CS instance +/// The proof is produced using Spartan's combination of the sum-check and +/// the commitment to a vector viewed as a polynomial commitment +#[derive(Serialize, Deserialize)] +#[serde(bound = "")] +pub struct RelaxedR1CSSNARK> { + sc_proof_outer: SumcheckProof, + claims_outer: (G::Scalar, G::Scalar, G::Scalar), + eval_E: G::Scalar, + sc_proof_inner: SumcheckProof, + eval_W: G::Scalar, + sc_proof_batch: SumcheckProof, + evals_batch: Vec, + eval_arg: EE::EvaluationArgument, +} + +impl> RelaxedR1CSSNARKTrait + for RelaxedR1CSSNARK +{ + type ProverKey = ProverKey; + type VerifierKey = VerifierKey; + + fn setup( + ck: &CommitmentKey, + S: &R1CSShape, + ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> { + let (pk_ee, vk_ee) = EE::setup(ck); + + let S = S.pad(); + + let vk = { + let mut vk = VerifierKey { + vk_ee, + S: S.clone(), + digest: G::Scalar::ZERO, + }; + vk.digest = compute_digest::>(&vk); + vk + }; + + let pk = ProverKey { + pk_ee, + S, + vk_digest: vk.digest, + }; + + Ok((pk, vk)) + } + + /// produces a succinct proof of satisfiability of a RelaxedR1CS instance + fn prove( + ck: &CommitmentKey, + pk: &Self::ProverKey, + U: &RelaxedR1CSInstance, + W: &RelaxedR1CSWitness, + ) -> Result { + let W = W.pad(&pk.S); // pad the witness + let mut transcript = G::TE::new(b"RelaxedR1CSSNARK"); + + // sanity check that R1CSShape has certain size characteristics + assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons); + assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars); + assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io); + assert!(pk.S.num_io < pk.S.num_vars); + + // append the digest of vk (which includes R1CS matrices) and the RelaxedR1CSInstance to the transcript + transcript.absorb(b"vk", &pk.vk_digest); + transcript.absorb(b"U", U); + + // compute the full satisfying assignment by concatenating W.W, U.u, and U.X + let mut z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]); + + let (num_rounds_x, num_rounds_y) = ( + (pk.S.num_cons as f64).log2() as usize, + ((pk.S.num_vars as f64).log2() as usize + 1), + ); + + // outer sum-check + let tau = (0..num_rounds_x) + .map(|_i| transcript.squeeze(b"t")) + .collect::, NovaError>>()?; + + let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals()); + let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = { + let (poly_Az, poly_Bz, poly_Cz) = pk.S.multiply_vec(&z)?; + let poly_uCz_E = (0..pk.S.num_cons) + .map(|i| U.u * poly_Cz[i] + W.E[i]) + .collect::>(); + ( + MultilinearPolynomial::new(poly_Az), + MultilinearPolynomial::new(poly_Bz), + MultilinearPolynomial::new(poly_Cz), + MultilinearPolynomial::new(poly_uCz_E), + ) + }; + + let comb_func_outer = + |poly_A_comp: &G::Scalar, + poly_B_comp: &G::Scalar, + poly_C_comp: &G::Scalar, + poly_D_comp: &G::Scalar| + -> G::Scalar { *poly_A_comp * (*poly_B_comp * *poly_C_comp - *poly_D_comp) }; + let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_additive_term( + &G::Scalar::ZERO, // claim is zero + num_rounds_x, + &mut poly_tau, + &mut poly_Az, + &mut poly_Bz, + &mut poly_uCz_E, + comb_func_outer, + &mut transcript, + )?; + + // claims from the end of sum-check + let (claim_Az, claim_Bz): (G::Scalar, G::Scalar) = (claims_outer[1], claims_outer[2]); + let claim_Cz = poly_Cz.evaluate(&r_x); + let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x); + transcript.absorb( + b"claims_outer", + &[claim_Az, claim_Bz, claim_Cz, eval_E].as_slice(), + ); + + // inner sum-check + let r = transcript.squeeze(b"r")?; + let claim_inner_joint = claim_Az + r * claim_Bz + r * r * claim_Cz; + + let poly_ABC = { + // compute the initial evaluation table for R(\tau, x) + let evals_rx = EqPolynomial::new(r_x.clone()).evals(); + + // Bounds "row" variables of (A, B, C) matrices viewed as 2d multilinear polynomials + let compute_eval_table_sparse = + |S: &R1CSShape, rx: &[G::Scalar]| -> (Vec, Vec, Vec) { + assert_eq!(rx.len(), S.num_cons); + + let inner = |M: &Vec<(usize, usize, G::Scalar)>, M_evals: &mut Vec| { + for (row, col, val) in M { + M_evals[*col] += rx[*row] * val; + } + }; + + let (A_evals, (B_evals, C_evals)) = rayon::join( + || { + let mut A_evals: Vec = vec![G::Scalar::ZERO; 2 * S.num_vars]; + inner(&S.A, &mut A_evals); + A_evals + }, + || { + rayon::join( + || { + let mut B_evals: Vec = vec![G::Scalar::ZERO; 2 * S.num_vars]; + inner(&S.B, &mut B_evals); + B_evals + }, + || { + let mut C_evals: Vec = vec![G::Scalar::ZERO; 2 * S.num_vars]; + inner(&S.C, &mut C_evals); + C_evals + }, + ) + }, + ); + + (A_evals, B_evals, C_evals) + }; + + let (evals_A, evals_B, evals_C) = compute_eval_table_sparse(&pk.S, &evals_rx); + + assert_eq!(evals_A.len(), evals_B.len()); + assert_eq!(evals_A.len(), evals_C.len()); + (0..evals_A.len()) + .into_par_iter() + .map(|i| evals_A[i] + r * evals_B[i] + r * r * evals_C[i]) + .collect::>() + }; + + let poly_z = { + z.resize(pk.S.num_vars * 2, G::Scalar::ZERO); + z + }; + + let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar { + *poly_A_comp * *poly_B_comp + }; + let (sc_proof_inner, r_y, _claims_inner) = SumcheckProof::prove_quad( + &claim_inner_joint, + num_rounds_y, + &mut MultilinearPolynomial::new(poly_ABC), + &mut MultilinearPolynomial::new(poly_z), + comb_func, + &mut transcript, + )?; + + // add additional claims about W and E polynomials to the list from CC + let mut w_u_vec = Vec::new(); + let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_y[1..]); + w_u_vec.push(( + PolyEvalWitness { p: W.W.clone() }, + PolyEvalInstance { + c: U.comm_W, + x: r_y[1..].to_vec(), + e: eval_W, + }, + )); + + w_u_vec.push(( + PolyEvalWitness { p: W.E }, + PolyEvalInstance { + c: U.comm_E, + x: r_x, + e: eval_E, + }, + )); + + // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point. + // For example, eval_W =? W(r_y[1..]) and eval_E =? E(r_x) into + // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz) + // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz), + // where gamma is a public challenge + // Since commitments to W and E are homomorphic, the verifier can compute a commitment + // to the batched polynomial. + assert!(w_u_vec.len() >= 2); + + let (w_vec, u_vec): (Vec>, Vec>) = + w_u_vec.into_iter().unzip(); + let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size + let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points + + // generate a challenge + let rho = transcript.squeeze(b"r")?; + let num_claims = w_vec_padded.len(); + let powers_of_rho = powers::(&rho, num_claims); + let claim_batch_joint = u_vec_padded + .iter() + .zip(powers_of_rho.iter()) + .map(|(u, p)| u.e * p) + .sum(); + + let mut polys_left: Vec> = w_vec_padded + .iter() + .map(|w| MultilinearPolynomial::new(w.p.clone())) + .collect(); + let mut polys_right: Vec> = u_vec_padded + .iter() + .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals())) + .collect(); + + let num_rounds_z = u_vec_padded[0].x.len(); + let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar { + *poly_A_comp * *poly_B_comp + }; + let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch( + &claim_batch_joint, + num_rounds_z, + &mut polys_left, + &mut polys_right, + &powers_of_rho, + comb_func, + &mut transcript, + )?; + + let (claims_batch_left, _): (Vec, Vec) = claims_batch; + + transcript.absorb(b"l", &claims_batch_left.as_slice()); + + // we now combine evaluation claims at the same point rz into one + let gamma = transcript.squeeze(b"g")?; + let powers_of_gamma: Vec = powers::(&gamma, num_claims); + let comm_joint = u_vec_padded + .iter() + .zip(powers_of_gamma.iter()) + .map(|(u, g_i)| u.c * *g_i) + .fold(Commitment::::default(), |acc, item| acc + item); + let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma); + let eval_joint = claims_batch_left + .iter() + .zip(powers_of_gamma.iter()) + .map(|(e, g_i)| *e * *g_i) + .sum(); + + let eval_arg = EE::prove( + ck, + &pk.pk_ee, + &mut transcript, + &comm_joint, + &poly_joint.p, + &r_z, + &eval_joint, + )?; + + Ok(RelaxedR1CSSNARK { + sc_proof_outer, + claims_outer: (claim_Az, claim_Bz, claim_Cz), + eval_E, + sc_proof_inner, + eval_W, + sc_proof_batch, + evals_batch: claims_batch_left, + eval_arg, + }) + } + + /// verifies a proof of satisfiability of a RelaxedR1CS instance + fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance) -> Result<(), NovaError> { + let mut transcript = G::TE::new(b"RelaxedR1CSSNARK"); + + // append the digest of R1CS matrices and the RelaxedR1CSInstance to the transcript + transcript.absorb(b"vk", &vk.digest); + transcript.absorb(b"U", U); + + let (num_rounds_x, num_rounds_y) = ( + (vk.S.num_cons as f64).log2() as usize, + ((vk.S.num_vars as f64).log2() as usize + 1), + ); + + // outer sum-check + let tau = (0..num_rounds_x) + .map(|_i| transcript.squeeze(b"t")) + .collect::, NovaError>>()?; + + let (claim_outer_final, r_x) = + self + .sc_proof_outer + .verify(G::Scalar::ZERO, num_rounds_x, 3, &mut transcript)?; + + // verify claim_outer_final + let (claim_Az, claim_Bz, claim_Cz) = self.claims_outer; + let taus_bound_rx = EqPolynomial::new(tau).evaluate(&r_x); + let claim_outer_final_expected = + taus_bound_rx * (claim_Az * claim_Bz - U.u * claim_Cz - self.eval_E); + if claim_outer_final != claim_outer_final_expected { + return Err(NovaError::InvalidSumcheckProof); + } + + transcript.absorb( + b"claims_outer", + &[ + self.claims_outer.0, + self.claims_outer.1, + self.claims_outer.2, + self.eval_E, + ] + .as_slice(), + ); + + // inner sum-check + let r = transcript.squeeze(b"r")?; + let claim_inner_joint = + self.claims_outer.0 + r * self.claims_outer.1 + r * r * self.claims_outer.2; + + let (claim_inner_final, r_y) = + self + .sc_proof_inner + .verify(claim_inner_joint, num_rounds_y, 2, &mut transcript)?; + + // verify claim_inner_final + let eval_Z = { + let eval_X = { + // constant term + let mut poly_X = vec![(0, U.u)]; + //remaining inputs + poly_X.extend( + (0..U.X.len()) + .map(|i| (i + 1, U.X[i])) + .collect::>(), + ); + SparsePolynomial::new((vk.S.num_vars as f64).log2() as usize, poly_X).evaluate(&r_y[1..]) + }; + (G::Scalar::ONE - r_y[0]) * self.eval_W + r_y[0] * eval_X + }; + + // compute evaluations of R1CS matrices + let multi_evaluate = |M_vec: &[&[(usize, usize, G::Scalar)]], + r_x: &[G::Scalar], + r_y: &[G::Scalar]| + -> Vec { + let evaluate_with_table = + |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar { + (0..M.len()) + .collect::>() + .par_iter() + .map(|&i| { + let (row, col, val) = M[i]; + T_x[row] * T_y[col] * val + }) + .reduce(|| G::Scalar::ZERO, |acc, x| acc + x) + }; + + let (T_x, T_y) = rayon::join( + || EqPolynomial::new(r_x.to_vec()).evals(), + || EqPolynomial::new(r_y.to_vec()).evals(), + ); + + (0..M_vec.len()) + .collect::>() + .par_iter() + .map(|&i| evaluate_with_table(M_vec[i], &T_x, &T_y)) + .collect() + }; + + let evals = multi_evaluate(&[&vk.S.A, &vk.S.B, &vk.S.C], &r_x, &r_y); + + let claim_inner_final_expected = (evals[0] + r * evals[1] + r * r * evals[2]) * eval_Z; + if claim_inner_final != claim_inner_final_expected { + return Err(NovaError::InvalidSumcheckProof); + } + + // add claims about W and E polynomials + let u_vec: Vec> = vec![ + PolyEvalInstance { + c: U.comm_W, + x: r_y[1..].to_vec(), + e: self.eval_W, + }, + PolyEvalInstance { + c: U.comm_E, + x: r_x, + e: self.eval_E, + }, + ]; + + let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points + + // generate a challenge + let rho = transcript.squeeze(b"r")?; + let num_claims = u_vec.len(); + let powers_of_rho = powers::(&rho, num_claims); + let claim_batch_joint = u_vec + .iter() + .zip(powers_of_rho.iter()) + .map(|(u, p)| u.e * p) + .sum(); + + let num_rounds_z = u_vec_padded[0].x.len(); + let (claim_batch_final, r_z) = + self + .sc_proof_batch + .verify(claim_batch_joint, num_rounds_z, 2, &mut transcript)?; + + let claim_batch_final_expected = { + let poly_rz = EqPolynomial::new(r_z.clone()); + let evals = u_vec_padded + .iter() + .map(|u| poly_rz.evaluate(&u.x)) + .collect::>(); + + evals + .iter() + .zip(self.evals_batch.iter()) + .zip(powers_of_rho.iter()) + .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i) + .sum() + }; + + if claim_batch_final != claim_batch_final_expected { + return Err(NovaError::InvalidSumcheckProof); + } + + transcript.absorb(b"l", &self.evals_batch.as_slice()); + + // we now combine evaluation claims at the same point rz into one + let gamma = transcript.squeeze(b"g")?; + let powers_of_gamma: Vec = powers::(&gamma, num_claims); + let comm_joint = u_vec_padded + .iter() + .zip(powers_of_gamma.iter()) + .map(|(u, g_i)| u.c * *g_i) + .fold(Commitment::::default(), |acc, item| acc + item); + let eval_joint = self + .evals_batch + .iter() + .zip(powers_of_gamma.iter()) + .map(|(e, g_i)| *e * *g_i) + .sum(); + + // verify + EE::verify( + &vk.vk_ee, + &mut transcript, + &comm_joint, + &r_z, + &eval_joint, + &self.eval_arg, + )?; + + Ok(()) + } +}