From 59b8bdb0c476a2eb5426b410727097544393c73e Mon Sep 17 00:00:00 2001 From: arnaucube Date: Tue, 4 Jun 2024 10:57:39 +0200 Subject: [PATCH] Add HyperNova's NIMFS circuit (#99) * add HyperNova's NIMFS verifier circuit * update poseidon usage after rebasing to latest main branch changes --- README.md | 2 +- folding-schemes/src/folding/circuits/mod.rs | 11 +- .../src/folding/hypernova/circuit.rs | 169 ------ .../src/folding/hypernova/circuits.rs | 567 ++++++++++++++++++ folding-schemes/src/folding/hypernova/mod.rs | 2 +- .../src/folding/hypernova/nimfs.rs | 5 +- .../src/folding/hypernova/utils.rs | 1 - folding-schemes/src/folding/nova/circuits.rs | 21 +- folding-schemes/src/folding/nova/cyclefold.rs | 3 +- .../src/folding/nova/decider_eth.rs | 4 +- .../src/folding/nova/decider_eth_circuit.rs | 14 +- folding-schemes/src/folding/nova/mod.rs | 9 +- 12 files changed, 604 insertions(+), 204 deletions(-) delete mode 100644 folding-schemes/src/folding/hypernova/circuit.rs create mode 100644 folding-schemes/src/folding/hypernova/circuits.rs diff --git a/README.md b/README.md index f2a9c80..accbf94 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,7 @@ Detailed usage and design documentation can be found at [Sonobe docs](https://pr ### Folding Schemes introduction -Folding schemes efficitently achieve incrementally verifiable computation (IVC), where the prover recursively proves the correct execution of the incremental computations. +Folding schemes efficiently achieve incrementally verifiable computation (IVC), where the prover recursively proves the correct execution of the incremental computations. Once the IVC iterations are completed, the IVC proof is compressed into the Decider proof, a zkSNARK proof which proves that applying $n$ times the $F$ function (the circuit being folded) to the initial state ($z_0$) results in the final state ($z_n$). diff --git a/folding-schemes/src/folding/circuits/mod.rs b/folding-schemes/src/folding/circuits/mod.rs index 08fa807..3854c43 100644 --- a/folding-schemes/src/folding/circuits/mod.rs +++ b/folding-schemes/src/folding/circuits/mod.rs @@ -1,10 +1,15 @@ /// Circuits and gadgets shared across the different folding schemes. -use ark_ec::CurveGroup; +use ark_ec::{AffineRepr, CurveGroup}; use ark_ff::Field; pub mod nonnative; pub mod sum_check; pub mod utils; -// CF represents the constraints field -pub type CF = <::BaseField as Field>::BasePrimeField; +/// CF1 represents the ConstraintField used for the main folding circuit which is over E1::Fr, where +/// E1 is the main curve where we do the folding. +pub type CF1 = <::Affine as AffineRepr>::ScalarField; +/// CF2 represents the ConstraintField used for the CycleFold circuit which is over E2::Fr=E1::Fq, +/// where E2 is the auxiliary curve (from [CycleFold](https://eprint.iacr.org/2023/1192.pdf) +/// approach) where we check the folding of the commitments (elliptic curve points). +pub type CF2 = <::BaseField as Field>::BasePrimeField; diff --git a/folding-schemes/src/folding/hypernova/circuit.rs b/folding-schemes/src/folding/hypernova/circuit.rs deleted file mode 100644 index 4d0d447..0000000 --- a/folding-schemes/src/folding/hypernova/circuit.rs +++ /dev/null @@ -1,169 +0,0 @@ -/// Implementation of [HyperNova](https://eprint.iacr.org/2023/573.pdf) NIMFS verifier circuit -use ark_ff::PrimeField; -use ark_r1cs_std::{ - alloc::AllocVar, - fields::{fp::FpVar, FieldVar}, -}; -use ark_relations::r1cs::{ConstraintSystemRef, SynthesisError}; - -use crate::ccs::CCS; -use crate::folding::circuits::utils::EqEvalGadget; - -/// computes c from the step 5 in section 5 of HyperNova, adapted to multiple LCCCS & CCCS -/// instances: -/// $$ -/// c = \sum_{i \in [\mu]} \left(\sum_{j \in [t]} \gamma^{i \cdot t + j} \cdot e_i \cdot \sigma_{i,j} \right) -/// + \sum_{k \in [\nu]} \gamma^{\mu \cdot t+k} \cdot e_k \cdot \left( \sum_{i=1}^q c_i \cdot \prod_{j \in S_i} -/// \theta_{k,j} \right) -/// $$ -#[allow(dead_code)] // TMP while the other circuits are not ready -#[allow(clippy::too_many_arguments)] -fn compute_c_gadget( - cs: ConstraintSystemRef, - ccs: &CCS, - vec_sigmas: Vec>>, - vec_thetas: Vec>>, - gamma: FpVar, - beta: Vec>, - vec_r_x: Vec>>, - vec_r_x_prime: Vec>, -) -> Result, SynthesisError> { - let mut e_lcccs = Vec::new(); - for r_x in vec_r_x.iter() { - e_lcccs.push(EqEvalGadget::eq_eval(r_x, &vec_r_x_prime)?); - } - - let mut c = FpVar::::zero(); - let mut current_gamma = FpVar::::one(); - for i in 0..vec_sigmas.len() { - for j in 0..ccs.t { - c += current_gamma.clone() * e_lcccs[i].clone() * vec_sigmas[i][j].clone(); - current_gamma *= gamma.clone(); - } - } - - let ccs_c = Vec::>::new_constant(cs.clone(), ccs.c.clone())?; - let e_k = EqEvalGadget::eq_eval(&beta, &vec_r_x_prime)?; - #[allow(clippy::needless_range_loop)] - for k in 0..vec_thetas.len() { - let mut sum = FpVar::::zero(); - for i in 0..ccs.q { - let mut prod = FpVar::::one(); - for j in ccs.S[i].clone() { - prod *= vec_thetas[k][j].clone(); - } - sum += ccs_c[i].clone() * prod; - } - c += current_gamma.clone() * e_k.clone() * sum; - current_gamma *= gamma.clone(); - } - Ok(c) -} - -#[cfg(test)] -mod tests { - use ark_pallas::{Fr, Projective}; - use ark_r1cs_std::{alloc::AllocVar, fields::fp::FpVar, R1CSVar}; - use ark_relations::r1cs::ConstraintSystem; - use ark_std::{test_rng, UniformRand}; - - use super::*; - use crate::{ - ccs::{ - tests::{get_test_ccs, get_test_z}, - CCS, - }, - commitment::{pedersen::Pedersen, CommitmentScheme}, - folding::hypernova::utils::{compute_c, compute_sigmas_and_thetas}, - }; - - #[test] - pub fn test_compute_c_gadget() { - // number of LCCCS & CCCS instances to fold in a single step - let mu = 32; - let nu = 42; - - let mut z_lcccs = Vec::new(); - for i in 0..mu { - let z = get_test_z(i + 3); - z_lcccs.push(z); - } - let mut z_cccs = Vec::new(); - for i in 0..nu { - let z = get_test_z(i + 3); - z_cccs.push(z); - } - - let ccs: CCS = get_test_ccs(); - - let mut rng = test_rng(); - let gamma: Fr = Fr::rand(&mut rng); - let beta: Vec = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect(); - let r_x_prime: Vec = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect(); - - let (pedersen_params, _) = - Pedersen::::setup(&mut rng, ccs.n - ccs.l - 1).unwrap(); - - // Create the LCCCS instances out of z_lcccs - let mut lcccs_instances = Vec::new(); - for z_i in z_lcccs.iter() { - let (inst, _) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap(); - lcccs_instances.push(inst); - } - // Create the CCCS instance out of z_cccs - let mut cccs_instances = Vec::new(); - for z_i in z_cccs.iter() { - let (inst, _) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap(); - cccs_instances.push(inst); - } - - let sigmas_thetas = compute_sigmas_and_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime); - - let expected_c = compute_c( - &ccs, - &sigmas_thetas, - gamma, - &beta, - &lcccs_instances - .iter() - .map(|lcccs| lcccs.r_x.clone()) - .collect(), - &r_x_prime, - ); - - let cs = ConstraintSystem::::new_ref(); - let mut vec_sigmas = Vec::new(); - let mut vec_thetas = Vec::new(); - for sigmas in sigmas_thetas.0 { - vec_sigmas - .push(Vec::>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap()); - } - for thetas in sigmas_thetas.1 { - vec_thetas - .push(Vec::>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap()); - } - let vec_r_x: Vec>> = lcccs_instances - .iter() - .map(|lcccs| { - Vec::>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap() - }) - .collect(); - let vec_r_x_prime = - Vec::>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap(); - let gamma_var = FpVar::::new_witness(cs.clone(), || Ok(gamma)).unwrap(); - let beta_var = Vec::>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap(); - let computed_c = compute_c_gadget( - cs.clone(), - &ccs, - vec_sigmas, - vec_thetas, - gamma_var, - beta_var, - vec_r_x, - vec_r_x_prime, - ) - .unwrap(); - - assert_eq!(expected_c, computed_c.value().unwrap()); - } -} diff --git a/folding-schemes/src/folding/hypernova/circuits.rs b/folding-schemes/src/folding/hypernova/circuits.rs new file mode 100644 index 0000000..7ebdeef --- /dev/null +++ b/folding-schemes/src/folding/hypernova/circuits.rs @@ -0,0 +1,567 @@ +/// Implementation of [HyperNova](https://eprint.iacr.org/2023/573.pdf) NIMFS verifier circuit +use ark_crypto_primitives::sponge::Absorb; +use ark_ec::{CurveGroup, Group}; +use ark_ff::PrimeField; +use ark_r1cs_std::{ + alloc::{AllocVar, AllocationMode}, + eq::EqGadget, + fields::{fp::FpVar, FieldVar}, +}; +use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError}; +use core::{borrow::Borrow, marker::PhantomData}; + +use super::{cccs::CCCS, lcccs::LCCCS, nimfs::Proof}; +use crate::folding::circuits::{ + nonnative::affine::NonNativeAffineVar, + sum_check::{IOPProofVar, SumCheckVerifierGadget, VPAuxInfoVar}, + utils::EqEvalGadget, + CF1, +}; +use crate::utils::virtual_polynomial::VPAuxInfo; +use crate::{ccs::CCS, transcript::TranscriptVar}; + +/// Committed CCS instance +#[derive(Debug, Clone)] +pub struct CCCSVar +where + ::BaseField: PrimeField, +{ + // Commitment to witness + pub C: NonNativeAffineVar, + // Public input/output + pub x: Vec>>, +} +impl AllocVar, CF1> for CCCSVar +where + C: CurveGroup, + ::BaseField: PrimeField, +{ + fn new_variable>>( + cs: impl Into>>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let C = NonNativeAffineVar::::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?; + let x: Vec> = + Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?; + + Ok(Self { C, x }) + }) + } +} + +/// Linearized Committed CCS instance +#[derive(Debug, Clone)] +pub struct LCCCSVar +where + ::BaseField: PrimeField, +{ + // Commitment to witness + pub C: NonNativeAffineVar, + // Relaxation factor of z for folded LCCCS + pub u: FpVar>, + // Public input/output + pub x: Vec>>, + // Random evaluation point for the v_i + pub r_x: Vec>>, + // Vector of v_i + pub v: Vec>>, +} +impl AllocVar, CF1> for LCCCSVar +where + C: CurveGroup, + ::BaseField: PrimeField, +{ + fn new_variable>>( + cs: impl Into>>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let C = NonNativeAffineVar::::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?; + let u = FpVar::::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?; + let x: Vec> = + Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?; + let r_x: Vec> = + Vec::new_variable(cs.clone(), || Ok(val.borrow().r_x.clone()), mode)?; + let v: Vec> = + Vec::new_variable(cs.clone(), || Ok(val.borrow().v.clone()), mode)?; + + Ok(Self { C, u, x, r_x, v }) + }) + } +} + +/// ProofVar defines a multifolding proof +#[derive(Debug)] +pub struct ProofVar { + pub sc_proof: IOPProofVar, + #[allow(clippy::type_complexity)] + pub sigmas_thetas: (Vec>>>, Vec>>>), +} +impl AllocVar, CF1> for ProofVar +where + C: CurveGroup, + ::BaseField: PrimeField, + ::ScalarField: Absorb, +{ + fn new_variable>>( + cs: impl Into>>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let sc_proof = IOPProofVar::::new_variable( + cs.clone(), + || Ok(val.borrow().sc_proof.clone()), + mode, + )?; + let sigmas: Vec>>> = val + .borrow() + .sigmas_thetas + .0 + .iter() + .map(|sigmas_i| Vec::new_variable(cs.clone(), || Ok(sigmas_i.clone()), mode)) + .collect::>>>, SynthesisError>>()?; + let thetas: Vec>>> = val + .borrow() + .sigmas_thetas + .1 + .iter() + .map(|thetas_i| Vec::new_variable(cs.clone(), || Ok(thetas_i.clone()), mode)) + .collect::>>>, SynthesisError>>()?; + + Ok(Self { + sc_proof, + sigmas_thetas: (sigmas.clone(), thetas.clone()), + }) + }) + } +} + +pub struct NIMFSGadget { + _c: PhantomData, +} +impl NIMFSGadget +where + ::BaseField: PrimeField, +{ + pub fn verify( + cs: ConstraintSystemRef>, + // only used the CCS params, not the matrices + ccs: &CCS, + mut transcript: impl TranscriptVar, + + running_instances: &[LCCCSVar], + new_instances: &[CCCSVar], + proof: ProofVar, + ) -> Result, SynthesisError> { + // get the challenges + let gamma_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"gamma"); + let gamma_scalar: FpVar> = + FpVar::>::new_constant(cs.clone(), gamma_scalar_raw)?; + transcript.absorb(gamma_scalar)?; + let gamma: FpVar> = transcript.get_challenge()?; + + let beta_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"beta"); + let beta_scalar: FpVar> = + FpVar::>::new_constant(cs.clone(), beta_scalar_raw)?; + transcript.absorb(beta_scalar)?; + let beta: Vec>> = transcript.get_challenges(ccs.s)?; + + let vp_aux_info_raw = VPAuxInfo:: { + max_degree: ccs.d + 1, + num_variables: ccs.s, + phantom: PhantomData::, + }; + let vp_aux_info = VPAuxInfoVar::>::new_witness(cs.clone(), || Ok(vp_aux_info_raw))?; + + // sumcheck + // first, compute the expected sumcheck sum: \sum gamma^j v_j + let mut sum_v_j_gamma = FpVar::>::zero(); + let mut gamma_j = FpVar::::one(); + for running_instance in running_instances.iter() { + for j in 0..running_instance.v.len() { + gamma_j *= gamma.clone(); + sum_v_j_gamma += running_instance.v[j].clone() * gamma_j.clone(); + } + } + + // verify the interactive part of the sumcheck + let (e_vars, r_vars) = + SumCheckVerifierGadget::::verify(&proof.sc_proof, &vp_aux_info, &mut transcript)?; + + // extract the randomness from the sumcheck + let r_x_prime = r_vars.clone(); + + // verify the claim c + let computed_c = compute_c_gadget( + cs.clone(), + ccs, + proof.sigmas_thetas.0.clone(), // sigmas + proof.sigmas_thetas.1.clone(), // thetas + gamma, + beta, + running_instances + .iter() + .map(|lcccs| lcccs.r_x.clone()) + .collect(), + r_x_prime.clone(), + )?; + computed_c.enforce_equal(&e_vars[e_vars.len() - 1])?; + + // get the folding challenge + let rho_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"rho"); + let rho_scalar: FpVar> = FpVar::>::new_constant(cs.clone(), rho_scalar_raw)?; + transcript.absorb(rho_scalar)?; + let rho: FpVar> = transcript.get_challenge()?; + + // return the folded instance + Self::fold( + running_instances, + new_instances, + proof.sigmas_thetas, + r_x_prime, + rho, + ) + } + + #[allow(clippy::type_complexity)] + fn fold( + lcccs: &[LCCCSVar], + cccs: &[CCCSVar], + sigmas_thetas: (Vec>>>, Vec>>>), + r_x_prime: Vec>>, + rho: FpVar>, + ) -> Result, SynthesisError> { + let (sigmas, thetas) = (sigmas_thetas.0.clone(), sigmas_thetas.1.clone()); + let mut u_folded: FpVar> = FpVar::zero(); + let mut x_folded: Vec>> = vec![FpVar::zero(); lcccs[0].x.len()]; + let mut v_folded: Vec>> = vec![FpVar::zero(); sigmas[0].len()]; + + let mut rho_i = FpVar::one(); + for i in 0..(lcccs.len() + cccs.len()) { + let u: FpVar>; + let x: Vec>>; + let v: Vec>>; + if i < lcccs.len() { + u = lcccs[i].u.clone(); + x = lcccs[i].x.clone(); + v = sigmas[i].clone(); + } else { + u = FpVar::one(); + x = cccs[i - lcccs.len()].x.clone(); + v = thetas[i - lcccs.len()].clone(); + } + + u_folded += rho_i.clone() * u; + x_folded = x_folded + .iter() + .zip( + x.iter() + .map(|x_i| x_i * rho_i.clone()) + .collect::>>>(), + ) + .map(|(a_i, b_i)| a_i + b_i) + .collect(); + + v_folded = v_folded + .iter() + .zip( + v.iter() + .map(|x_i| x_i * rho_i.clone()) + .collect::>>>(), + ) + .map(|(a_i, b_i)| a_i + b_i) + .collect(); + + rho_i *= rho.clone(); + } + + Ok(LCCCSVar:: { + C: lcccs[0].C.clone(), // WIP this will come from the cyclefold circuit + u: u_folded, + x: x_folded, + r_x: r_x_prime, + v: v_folded, + }) + } +} + +/// computes c from the step 5 in section 5 of HyperNova, adapted to multiple LCCCS & CCCS +/// instances: +/// $$ +/// c = \sum_{i \in [\mu]} \left(\sum_{j \in [t]} \gamma^{i \cdot t + j} \cdot e_i \cdot \sigma_{i,j} \right) +/// + \sum_{k \in [\nu]} \gamma^{\mu \cdot t+k} \cdot e_k \cdot \left( \sum_{i=1}^q c_i \cdot \prod_{j \in S_i} +/// \theta_{k,j} \right) +/// $$ +#[allow(clippy::too_many_arguments)] +fn compute_c_gadget( + cs: ConstraintSystemRef, + ccs: &CCS, + vec_sigmas: Vec>>, + vec_thetas: Vec>>, + gamma: FpVar, + beta: Vec>, + vec_r_x: Vec>>, + vec_r_x_prime: Vec>, +) -> Result, SynthesisError> { + let mut e_lcccs = Vec::new(); + for r_x in vec_r_x.iter() { + e_lcccs.push(EqEvalGadget::eq_eval(r_x, &vec_r_x_prime)?); + } + + let mut c = FpVar::::zero(); + let mut current_gamma = FpVar::::one(); + for i in 0..vec_sigmas.len() { + for j in 0..ccs.t { + c += current_gamma.clone() * e_lcccs[i].clone() * vec_sigmas[i][j].clone(); + current_gamma *= gamma.clone(); + } + } + + let ccs_c = Vec::>::new_constant(cs.clone(), ccs.c.clone())?; + let e_k = EqEvalGadget::eq_eval(&beta, &vec_r_x_prime)?; + #[allow(clippy::needless_range_loop)] + for k in 0..vec_thetas.len() { + let mut sum = FpVar::::zero(); + for i in 0..ccs.q { + let mut prod = FpVar::::one(); + for j in ccs.S[i].clone() { + prod *= vec_thetas[k][j].clone(); + } + sum += ccs_c[i].clone() * prod; + } + c += current_gamma.clone() * e_k.clone() * sum; + current_gamma *= gamma.clone(); + } + Ok(c) +} + +#[cfg(test)] +mod tests { + use ark_pallas::{Fr, Projective}; + use ark_r1cs_std::{alloc::AllocVar, fields::fp::FpVar, R1CSVar}; + use ark_relations::r1cs::ConstraintSystem; + use ark_std::{test_rng, UniformRand}; + + use super::*; + use crate::{ + ccs::{ + tests::{get_test_ccs, get_test_z}, + CCS, + }, + commitment::{pedersen::Pedersen, CommitmentScheme}, + folding::hypernova::{ + nimfs::NIMFS, + utils::{compute_c, compute_sigmas_and_thetas}, + }, + transcript::{ + poseidon::{poseidon_canonical_config, PoseidonTranscript, PoseidonTranscriptVar}, + Transcript, + }, + }; + + #[test] + pub fn test_compute_c_gadget() { + // number of LCCCS & CCCS instances to fold in a single step + let mu = 32; + let nu = 42; + + let mut z_lcccs = Vec::new(); + for i in 0..mu { + let z = get_test_z(i + 3); + z_lcccs.push(z); + } + let mut z_cccs = Vec::new(); + for i in 0..nu { + let z = get_test_z(i + 3); + z_cccs.push(z); + } + + let ccs: CCS = get_test_ccs(); + + let mut rng = test_rng(); + let gamma: Fr = Fr::rand(&mut rng); + let beta: Vec = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect(); + let r_x_prime: Vec = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect(); + + let (pedersen_params, _) = + Pedersen::::setup(&mut rng, ccs.n - ccs.l - 1).unwrap(); + + // Create the LCCCS instances out of z_lcccs + let mut lcccs_instances = Vec::new(); + for z_i in z_lcccs.iter() { + let (inst, _) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap(); + lcccs_instances.push(inst); + } + // Create the CCCS instance out of z_cccs + let mut cccs_instances = Vec::new(); + for z_i in z_cccs.iter() { + let (inst, _) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap(); + cccs_instances.push(inst); + } + + let sigmas_thetas = compute_sigmas_and_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime); + + let expected_c = compute_c( + &ccs, + &sigmas_thetas, + gamma, + &beta, + &lcccs_instances + .iter() + .map(|lcccs| lcccs.r_x.clone()) + .collect(), + &r_x_prime, + ); + + let cs = ConstraintSystem::::new_ref(); + let mut vec_sigmas = Vec::new(); + let mut vec_thetas = Vec::new(); + for sigmas in sigmas_thetas.0 { + vec_sigmas + .push(Vec::>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap()); + } + for thetas in sigmas_thetas.1 { + vec_thetas + .push(Vec::>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap()); + } + let vec_r_x: Vec>> = lcccs_instances + .iter() + .map(|lcccs| { + Vec::>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap() + }) + .collect(); + let vec_r_x_prime = + Vec::>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap(); + let gamma_var = FpVar::::new_witness(cs.clone(), || Ok(gamma)).unwrap(); + let beta_var = Vec::>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap(); + + let computed_c = compute_c_gadget( + cs.clone(), + &ccs, + vec_sigmas, + vec_thetas, + gamma_var, + beta_var, + vec_r_x, + vec_r_x_prime, + ) + .unwrap(); + + assert_eq!(expected_c, computed_c.value().unwrap()); + } + + /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step, + /// to verify the folding in the NIMFSGadget circuit + #[test] + pub fn test_nimfs_gadget_verify() { + let mut rng = test_rng(); + + // Create a basic CCS circuit + let ccs = get_test_ccs::(); + let (pedersen_params, _) = + Pedersen::::setup(&mut rng, ccs.n - ccs.l - 1).unwrap(); + + let mu = 32; + let nu = 42; + + // Generate a mu LCCCS & nu CCCS satisfying witness + let mut z_lcccs = Vec::new(); + for i in 0..mu { + let z = get_test_z(i + 3); + z_lcccs.push(z); + } + let mut z_cccs = Vec::new(); + for i in 0..nu { + let z = get_test_z(nu + i + 3); + z_cccs.push(z); + } + + // Create the LCCCS instances out of z_lcccs + let mut lcccs_instances = Vec::new(); + let mut w_lcccs = Vec::new(); + for z_i in z_lcccs.iter() { + let (running_instance, w) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap(); + lcccs_instances.push(running_instance); + w_lcccs.push(w); + } + // Create the CCCS instance out of z_cccs + let mut cccs_instances = Vec::new(); + let mut w_cccs = Vec::new(); + for z_i in z_cccs.iter() { + let (new_instance, w) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap(); + cccs_instances.push(new_instance); + w_cccs.push(w); + } + + // Prover's transcript + let poseidon_config = poseidon_canonical_config::(); + let mut transcript_p: PoseidonTranscript = + PoseidonTranscript::::new(&poseidon_config); + + // Run the prover side of the multifolding + let (proof, folded_lcccs, folded_witness) = + NIMFS::>::prove( + &mut transcript_p, + &ccs, + &lcccs_instances, + &cccs_instances, + &w_lcccs, + &w_cccs, + ) + .unwrap(); + + // Verifier's transcript + let mut transcript_v: PoseidonTranscript = + PoseidonTranscript::::new(&poseidon_config); + + // Run the verifier side of the multifolding + let folded_lcccs_v = NIMFS::>::verify( + &mut transcript_v, + &ccs, + &lcccs_instances, + &cccs_instances, + proof.clone(), + ) + .unwrap(); + assert_eq!(folded_lcccs, folded_lcccs_v); + + // Check that the folded LCCCS instance is a valid instance with respect to the folded witness + folded_lcccs + .check_relation(&pedersen_params, &ccs, &folded_witness) + .unwrap(); + + // allocate circuit inputs + let cs = ConstraintSystem::::new_ref(); + let lcccs_instancesVar = + Vec::>::new_witness(cs.clone(), || Ok(lcccs_instances.clone())) + .unwrap(); + let cccs_instancesVar = + Vec::>::new_witness(cs.clone(), || Ok(cccs_instances.clone())) + .unwrap(); + let proofVar = + ProofVar::::new_witness(cs.clone(), || Ok(proof.clone())).unwrap(); + let transcriptVar = PoseidonTranscriptVar::::new(cs.clone(), &poseidon_config); + + let folded_lcccsVar = NIMFSGadget::::verify( + cs.clone(), + &ccs, + transcriptVar, + &lcccs_instancesVar, + &cccs_instancesVar, + proofVar, + ) + .unwrap(); + assert!(cs.is_satisfied().unwrap()); + assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u); + } +} diff --git a/folding-schemes/src/folding/hypernova/mod.rs b/folding-schemes/src/folding/hypernova/mod.rs index 5450779..3f7172e 100644 --- a/folding-schemes/src/folding/hypernova/mod.rs +++ b/folding-schemes/src/folding/hypernova/mod.rs @@ -1,6 +1,6 @@ /// Implements the scheme described in [HyperNova](https://eprint.iacr.org/2023/573.pdf) pub mod cccs; -pub mod circuit; +pub mod circuits; pub mod lcccs; pub mod nimfs; pub mod utils; diff --git a/folding-schemes/src/folding/hypernova/nimfs.rs b/folding-schemes/src/folding/hypernova/nimfs.rs index f62ca4f..39c3a81 100644 --- a/folding-schemes/src/folding/hypernova/nimfs.rs +++ b/folding-schemes/src/folding/hypernova/nimfs.rs @@ -54,9 +54,8 @@ where let mut x_folded: Vec = vec![C::ScalarField::zero(); lcccs[0].x.len()]; let mut v_folded: Vec = vec![C::ScalarField::zero(); sigmas[0].len()]; + let mut rho_i = C::ScalarField::one(); for i in 0..(lcccs.len() + cccs.len()) { - let rho_i = rho.pow([i as u64]); - let c: C; let u: C::ScalarField; let x: Vec; @@ -94,6 +93,8 @@ where ) .map(|(a_i, b_i)| *a_i + b_i) .collect(); + + rho_i *= rho; } LCCCS:: { diff --git a/folding-schemes/src/folding/hypernova/utils.rs b/folding-schemes/src/folding/hypernova/utils.rs index c713fcb..50882f3 100644 --- a/folding-schemes/src/folding/hypernova/utils.rs +++ b/folding-schemes/src/folding/hypernova/utils.rs @@ -149,7 +149,6 @@ pub fn compute_g( vec_Ls.append(&mut Ls); } let mut vec_Q: Vec> = Vec::new(); - // for (i, _) in cccs_instances.iter().enumerate() { for z_cccs_i in z_cccs.iter() { let Q = ccs.compute_Q(z_cccs_i, beta); vec_Q.push(Q); diff --git a/folding-schemes/src/folding/nova/circuits.rs b/folding-schemes/src/folding/nova/circuits.rs index 1de1d6b..a45ffff 100644 --- a/folding-schemes/src/folding/nova/circuits.rs +++ b/folding-schemes/src/folding/nova/circuits.rs @@ -8,8 +8,8 @@ use ark_crypto_primitives::sponge::{ poseidon::{constraints::PoseidonSpongeVar, PoseidonConfig, PoseidonSponge}, Absorb, CryptographicSponge, }; -use ark_ec::{AffineRepr, CurveGroup, Group}; -use ark_ff::{Field, PrimeField}; +use ark_ec::{CurveGroup, Group}; +use ark_ff::PrimeField; use ark_r1cs_std::{ alloc::{AllocVar, AllocationMode}, boolean::Boolean, @@ -30,20 +30,15 @@ use super::{ CommittedInstance, }; use crate::constants::N_BITS_RO; -use crate::folding::circuits::nonnative::{ - affine::{nonnative_affine_to_field_elements, NonNativeAffineVar}, - uint::NonNativeUintVar, +use crate::folding::circuits::{ + nonnative::{ + affine::{nonnative_affine_to_field_elements, NonNativeAffineVar}, + uint::NonNativeUintVar, + }, + CF1, CF2, }; use crate::frontend::FCircuit; -/// CF1 represents the ConstraintField used for the main Nova circuit which is over E1::Fr, where -/// E1 is the main curve where we do the folding. -pub type CF1 = <::Affine as AffineRepr>::ScalarField; -/// CF2 represents the ConstraintField used for the CycleFold circuit which is over E2::Fr=E1::Fq, -/// where E2 is the auxiliary curve (from [CycleFold](https://eprint.iacr.org/2023/1192.pdf) -/// approach) where we check the folding of the commitments (elliptic curve points). -pub type CF2 = <::BaseField as Field>::BasePrimeField; - /// CommittedInstanceVar contains the u, x, cmE and cmW values which are folded on the main Nova /// constraints field (E1::Fr, where E1 is the main curve). The peculiarity is that cmE and cmW are /// represented non-natively over the constraint field. diff --git a/folding-schemes/src/folding/nova/cyclefold.rs b/folding-schemes/src/folding/nova/cyclefold.rs index 175e603..6ac5bcd 100644 --- a/folding-schemes/src/folding/nova/cyclefold.rs +++ b/folding-schemes/src/folding/nova/cyclefold.rs @@ -26,10 +26,9 @@ use ark_std::fmt::Debug; use ark_std::{One, Zero}; use core::{borrow::Borrow, marker::PhantomData}; -use super::circuits::CF2; use super::CommittedInstance; use crate::constants::N_BITS_RO; -use crate::folding::circuits::nonnative::uint::NonNativeUintVar; +use crate::folding::circuits::{nonnative::uint::NonNativeUintVar, CF2}; use crate::Error; // public inputs length for the CycleFoldCircuit: |[r, p1.x,y, p2.x,y, p3.x,y]| diff --git a/folding-schemes/src/folding/nova/decider_eth.rs b/folding-schemes/src/folding/nova/decider_eth.rs index 04bccbb..3c1bf15 100644 --- a/folding-schemes/src/folding/nova/decider_eth.rs +++ b/folding-schemes/src/folding/nova/decider_eth.rs @@ -11,13 +11,13 @@ use ark_std::{One, Zero}; use core::marker::PhantomData; pub use super::decider_eth_circuit::{DeciderEthCircuit, KZGChallengesGadget}; -use super::{circuits::CF2, nifs::NIFS, CommittedInstance, Nova}; +use super::{nifs::NIFS, CommittedInstance, Nova}; use crate::commitment::{ kzg::{Proof as KZGProof, KZG}, pedersen::Params as PedersenParams, CommitmentScheme, }; -use crate::folding::circuits::nonnative::affine::NonNativeAffineVar; +use crate::folding::circuits::{nonnative::affine::NonNativeAffineVar, CF2}; use crate::frontend::FCircuit; use crate::Error; use crate::{Decider as DeciderTrait, FoldingScheme}; diff --git a/folding-schemes/src/folding/nova/decider_eth_circuit.rs b/folding-schemes/src/folding/nova/decider_eth_circuit.rs index 18c6657..9ec17cc 100644 --- a/folding-schemes/src/folding/nova/decider_eth_circuit.rs +++ b/folding-schemes/src/folding/nova/decider_eth_circuit.rs @@ -22,14 +22,14 @@ use core::{borrow::Borrow, marker::PhantomData}; use super::{circuits::ChallengeGadget, nifs::NIFS}; use crate::ccs::r1cs::R1CS; use crate::commitment::{pedersen::Params as PedersenParams, CommitmentScheme}; -use crate::folding::circuits::nonnative::{ - affine::{nonnative_affine_to_field_elements, NonNativeAffineVar}, - uint::NonNativeUintVar, -}; -use crate::folding::nova::{ - circuits::{CommittedInstanceVar, CF1, CF2}, - CommittedInstance, Nova, Witness, +use crate::folding::circuits::{ + nonnative::{ + affine::{nonnative_affine_to_field_elements, NonNativeAffineVar}, + uint::NonNativeUintVar, + }, + CF1, CF2, }; +use crate::folding::nova::{circuits::CommittedInstanceVar, CommittedInstance, Nova, Witness}; use crate::frontend::FCircuit; use crate::transcript::{ poseidon::{PoseidonTranscript, PoseidonTranscriptVar}, diff --git a/folding-schemes/src/folding/nova/mod.rs b/folding-schemes/src/folding/nova/mod.rs index accd589..2b11c28 100644 --- a/folding-schemes/src/folding/nova/mod.rs +++ b/folding-schemes/src/folding/nova/mod.rs @@ -15,8 +15,11 @@ use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystem}; use crate::ccs::r1cs::{extract_r1cs, extract_w_x, R1CS}; use crate::commitment::CommitmentScheme; -use crate::folding::circuits::nonnative::{ - affine::nonnative_affine_to_field_elements, uint::nonnative_field_to_field_elements, +use crate::folding::circuits::{ + nonnative::{ + affine::nonnative_affine_to_field_elements, uint::nonnative_field_to_field_elements, + }, + CF2, }; use crate::frontend::FCircuit; use crate::utils::vec::is_zero_vec; @@ -30,7 +33,7 @@ pub mod decider_eth_circuit; pub mod nifs; pub mod traits; -use circuits::{AugmentedFCircuit, ChallengeGadget, CF2}; +use circuits::{AugmentedFCircuit, ChallengeGadget}; use cyclefold::{CycleFoldChallengeGadget, CycleFoldCircuit}; use nifs::NIFS; use traits::NovaR1CS;