From 01a006b120942f712d4d06e5777845bf3e3dce84 Mon Sep 17 00:00:00 2001 From: Samuel Judson Date: Tue, 9 Apr 2024 13:58:58 -0400 Subject: [PATCH] HyperNova Gadgets (#141) * Restructure gadgets folder. * Start to scratch out rough IVC. * Start to scratch out in-circuit verifier folding. * Various fixes and reconfigurations. * More cleanup. * More scratching at in-circuit sumcheck. * More work on in-circuit recursive sumcheck. * Various fixes to trait bounds and related rearrangement. * More fixes. * Rename. * Remove IVC to separate gadgets and IVC PRs. * Debug verification circuit. * More updates. * Get gadgets building. * Update proof objects. * Formatting and work towards tests. * Test compiling. * More work on gadgets. * Get tests passing. * Fix clippy. * Remove debugging call forgot to remove. * Remove debugging call forgot to remove, again. * Remove part of IVC sketching that I missed previously. --- nova/src/ccs/mod.rs | 47 +- nova/src/circuits/nova/pcd/augmented.rs | 4 +- .../src/circuits/nova/sequential/augmented.rs | 6 +- nova/src/circuits/supernova/augmented.rs | 6 +- nova/src/folding/cyclefold/mod.rs | 5 - nova/src/folding/hypernova/cyclefold/mod.rs | 9 + .../folding/hypernova/cyclefold/nimfs/mod.rs | 12 +- nova/src/folding/hypernova/ml_sumcheck/mod.rs | 2 +- nova/src/folding/hypernova/mod.rs | 2 +- nova/src/folding/hypernova/nimfs.rs | 47 +- nova/src/folding/mod.rs | 2 +- nova/src/gadgets/cyclefold/hypernova/mod.rs | 450 ++++++++++++ .../gadgets/cyclefold/hypernova/primary.rs | 561 +++++++++++++++ nova/src/gadgets/cyclefold/mod.rs | 643 +---------------- nova/src/gadgets/cyclefold/nova/mod.rs | 645 ++++++++++++++++++ .../gadgets/cyclefold/{ => nova}/primary.rs | 0 nova/src/gadgets/cyclefold/secondary.rs | 2 +- 17 files changed, 1757 insertions(+), 686 deletions(-) create mode 100644 nova/src/gadgets/cyclefold/hypernova/mod.rs create mode 100644 nova/src/gadgets/cyclefold/hypernova/primary.rs create mode 100644 nova/src/gadgets/cyclefold/nova/mod.rs rename nova/src/gadgets/cyclefold/{ => nova}/primary.rs (100%) diff --git a/nova/src/ccs/mod.rs b/nova/src/ccs/mod.rs index 80fe4dfa9..9fccc45c8 100644 --- a/nova/src/ccs/mod.rs +++ b/nova/src/ccs/mod.rs @@ -166,7 +166,7 @@ pub struct CCSWitness { } /// A type that holds an CCS instance. -#[derive(Clone, Eq, PartialEq, CanonicalSerialize, CanonicalDeserialize)] +#[derive(CanonicalSerialize, CanonicalDeserialize)] pub struct CCSInstance> { /// Commitment to witness. pub commitment_W: C::Commitment, @@ -254,6 +254,35 @@ impl> CCSInstance { } } +impl> fmt::Debug for CCSInstance +where + C::Commitment: fmt::Debug, +{ + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("CCSInstance") + .field("commitment_W", &self.commitment_W) + .field("X", &self.X) + .finish() + } +} + +impl> Clone for CCSInstance { + fn clone(&self) -> Self { + Self { + commitment_W: self.commitment_W.clone(), + X: self.X.clone(), + } + } +} + +impl> PartialEq for CCSInstance { + fn eq(&self, other: &Self) -> bool { + self.commitment_W == other.commitment_W && self.X == other.X + } +} + +impl> Eq for CCSInstance where C::Commitment: Eq {} + impl Absorb for LCCSInstance where G: CurveGroup + AbsorbNonNative, @@ -313,7 +342,8 @@ impl> LCCSInstance { sigmas: &[G::ScalarField], thetas: &[G::ScalarField], ) -> Result { - // uX1 = (u, X_1), oX2 = (1, x_2) + // in concept, uX1 = (u_1, x_1), oX2 = (1, x_2) + // however, we don't guarantee oX2[0] = 1 during construction, so elide it during folding let (uX1, comm_W1) = (&self.X, self.commitment_W.clone()); let (oX2, comm_W2) = (&U2.X, U2.commitment_W.clone()); @@ -351,7 +381,7 @@ impl> LCCSInstance { } /// A type that holds an LCCS instance. -#[derive(Clone, CanonicalSerialize, CanonicalDeserialize)] +#[derive(CanonicalSerialize, CanonicalDeserialize)] pub struct LCCSInstance> { /// Commitment to MLE of witness. /// @@ -379,6 +409,17 @@ where } } +impl> Clone for LCCSInstance { + fn clone(&self) -> Self { + Self { + commitment_W: self.commitment_W.clone(), + X: self.X.clone(), + rs: self.rs.clone(), + vs: self.vs.clone(), + } + } +} + impl> PartialEq for LCCSInstance { fn eq(&self, other: &Self) -> bool { self.commitment_W == other.commitment_W diff --git a/nova/src/circuits/nova/pcd/augmented.rs b/nova/src/circuits/nova/pcd/augmented.rs index 1c5e0b01f..3ed643a7e 100644 --- a/nova/src/circuits/nova/pcd/augmented.rs +++ b/nova/src/circuits/nova/pcd/augmented.rs @@ -28,8 +28,10 @@ use crate::{ secondary::Circuit as SecondaryCircuit, }, gadgets::cyclefold::{ - multifold, multifold_with_relaxed, primary, secondary, NonNativeAffineVar, + nova::{multifold, multifold_with_relaxed, primary}, + secondary, }, + gadgets::nonnative::short_weierstrass::NonNativeAffineVar, }; pub const SQUEEZE_NATIVE_ELEMENTS_NUM: usize = 1; diff --git a/nova/src/circuits/nova/sequential/augmented.rs b/nova/src/circuits/nova/sequential/augmented.rs index 430a49d8e..c2bf8f2bc 100644 --- a/nova/src/circuits/nova/sequential/augmented.rs +++ b/nova/src/circuits/nova/sequential/augmented.rs @@ -26,7 +26,11 @@ use crate::{ nimfs::{NIMFSProof, R1CSInstance, R1CSShape, RelaxedR1CSInstance}, secondary::Circuit as SecondaryCircuit, }, - gadgets::cyclefold::{multifold, primary, secondary, NonNativeAffineVar}, + gadgets::cyclefold::{ + nova::{multifold, primary}, + secondary, + }, + gadgets::nonnative::short_weierstrass::NonNativeAffineVar, }; pub const SQUEEZE_NATIVE_ELEMENTS_NUM: usize = 1; diff --git a/nova/src/circuits/supernova/augmented.rs b/nova/src/circuits/supernova/augmented.rs index 732072f8b..241862e7b 100644 --- a/nova/src/circuits/supernova/augmented.rs +++ b/nova/src/circuits/supernova/augmented.rs @@ -27,7 +27,11 @@ use crate::{ nimfs::{NIMFSProof, R1CSInstance, RelaxedR1CSInstance}, secondary::Circuit as SecondaryCircuit, }, - gadgets::cyclefold::{multifold, primary, secondary, NonNativeAffineVar}, + gadgets::cyclefold::{ + nova::{multifold, primary}, + secondary, + }, + gadgets::nonnative::short_weierstrass::NonNativeAffineVar, }; pub const SQUEEZE_NATIVE_ELEMENTS_NUM: usize = 1; diff --git a/nova/src/folding/cyclefold/mod.rs b/nova/src/folding/cyclefold/mod.rs index 465eac850..d3bc1ab0e 100644 --- a/nova/src/folding/cyclefold/mod.rs +++ b/nova/src/folding/cyclefold/mod.rs @@ -10,8 +10,3 @@ pub(crate) type R1CSInstance = r1cs::R1CSInstance, C>; pub(crate) type R1CSWitness = r1cs::R1CSWitness>; pub(crate) type RelaxedR1CSInstance = r1cs::RelaxedR1CSInstance, C>; pub(crate) type RelaxedR1CSWitness = r1cs::RelaxedR1CSWitness>; - -pub(crate) type CCSShape = ccs::CCSShape>; -pub(crate) type CCSInstance = ccs::CCSInstance, C>; -pub(crate) type CCSWitness = ccs::CCSWitness>; -pub(crate) type LCCSInstance = ccs::LCCSInstance, C>; diff --git a/nova/src/folding/hypernova/cyclefold/mod.rs b/nova/src/folding/hypernova/cyclefold/mod.rs index 419595773..d068f7cff 100644 --- a/nova/src/folding/hypernova/cyclefold/mod.rs +++ b/nova/src/folding/hypernova/cyclefold/mod.rs @@ -3,12 +3,21 @@ pub(crate) mod nimfs; pub(crate) use super::super::cyclefold::secondary; +use crate::ccs; +use ark_ec::short_weierstrass::Projective; use ark_std::fmt::Display; use super::nimfs::Error as HNFoldingError; use crate::ccs::Error as CCSError; use crate::r1cs::Error as R1CSError; +pub(crate) type HNProof = super::nimfs::NIMFSProof, RO>; + +pub(crate) type CCSShape = ccs::CCSShape>; +pub(crate) type CCSInstance = ccs::CCSInstance, C>; +pub(crate) type CCSWitness = ccs::CCSWitness>; +pub(crate) type LCCSInstance = ccs::LCCSInstance, C>; + #[derive(Debug, Clone, Copy)] pub enum Error { R1CS(R1CSError), diff --git a/nova/src/folding/hypernova/cyclefold/nimfs/mod.rs b/nova/src/folding/hypernova/cyclefold/nimfs/mod.rs index 751fbb153..113f9117d 100644 --- a/nova/src/folding/hypernova/cyclefold/nimfs/mod.rs +++ b/nova/src/folding/hypernova/cyclefold/nimfs/mod.rs @@ -9,17 +9,13 @@ use ark_spartan::polycommitments::{PolyCommitmentScheme, PolyCommitmentTrait}; use crate::commitment::{Commitment, CommitmentScheme}; -use crate::folding::hypernova::nimfs::NIMFSProof as HNProof; +pub(crate) use crate::folding::hypernova::nimfs::NIMFSProof as HNProof; pub use crate::folding::hypernova::nimfs::SQUEEZE_ELEMENTS_BIT_SIZE; -use super::{secondary, Error}; +pub(crate) use super::{secondary, CCSInstance, CCSShape, CCSWitness, Error, LCCSInstance}; +pub(crate) use crate::folding::cyclefold::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness}; use crate::{absorb::CryptographicSpongeExt, r1cs, utils::cast_field_element_unique}; -pub(crate) use crate::folding::cyclefold::{ - CCSInstance, CCSShape, CCSWitness, LCCSInstance, R1CSShape, RelaxedR1CSInstance, - RelaxedR1CSWitness, -}; - /// Non-interactive multi-folding scheme proof. pub struct NIMFSProof< G1: SWCurveConfig, @@ -28,7 +24,6 @@ pub struct NIMFSProof< C2: CommitmentScheme>, RO, > { - pub(crate) commitment_T: C2::Commitment, pub(crate) commitment_W_proof: secondary::Proof, pub(crate) hypernova_proof: HNProof, RO>, _poly_commitment: PhantomData, @@ -121,7 +116,6 @@ where let commitment_W_proof = secondary::Proof { commitment_T, U: W_comm_trace.0 }; let proof = Self { - commitment_T, commitment_W_proof, hypernova_proof, _poly_commitment: PhantomData, diff --git a/nova/src/folding/hypernova/ml_sumcheck/mod.rs b/nova/src/folding/hypernova/ml_sumcheck/mod.rs index b3d09fd85..f848aa404 100644 --- a/nova/src/folding/hypernova/ml_sumcheck/mod.rs +++ b/nova/src/folding/hypernova/ml_sumcheck/mod.rs @@ -11,7 +11,7 @@ use ark_ff::PrimeField; use ark_std::{fmt::Display, marker::PhantomData}; mod data_structures; -mod protocol; +pub(crate) mod protocol; #[cfg(test)] mod tests; diff --git a/nova/src/folding/hypernova/mod.rs b/nova/src/folding/hypernova/mod.rs index 7138363a9..5007baf47 100644 --- a/nova/src/folding/hypernova/mod.rs +++ b/nova/src/folding/hypernova/mod.rs @@ -1,4 +1,4 @@ pub mod cyclefold; pub mod nimfs; -mod ml_sumcheck; +pub(crate) mod ml_sumcheck; diff --git a/nova/src/folding/hypernova/nimfs.rs b/nova/src/folding/hypernova/nimfs.rs index e9fa2dc39..acda01a8a 100644 --- a/nova/src/folding/hypernova/nimfs.rs +++ b/nova/src/folding/hypernova/nimfs.rs @@ -107,11 +107,9 @@ where unsafe { cast_field_element::(&rho) }; let s: usize = ((shape.num_constraints - 1).checked_ilog2().unwrap_or(0) + 1) as usize; - let rvec_shape = vec![SQUEEZE_ELEMENTS_BIT_SIZE; s]; - let gamma: G::ScalarField = - random_oracle.squeeze_field_elements_with_sizes(&[SQUEEZE_ELEMENTS_BIT_SIZE])[0]; - let beta = random_oracle.squeeze_field_elements_with_sizes(rvec_shape.as_slice()); + let gamma: G::ScalarField = random_oracle.squeeze_field_elements(1)[0]; + let beta = random_oracle.squeeze_field_elements(s); let z1 = [U1.X.as_slice(), W1.W.as_slice()].concat(); let z2 = [U2.X.as_slice(), W2.W.as_slice()].concat(); @@ -150,17 +148,17 @@ where let (sumcheck_proof, sumcheck_state) = MLSumcheck::prove_as_subprotocol(random_oracle, &g); - let rs = sumcheck_state.randomness; + let rs_p = sumcheck_state.randomness; let sigmas: Vec = ark_std::cfg_iter!(&shape.Ms) - .map(|M| vec_to_ark_mle(M.multiply_vec(&z1).as_slice()).evaluate(&rs)) + .map(|M| vec_to_ark_mle(M.multiply_vec(&z1).as_slice()).evaluate(&rs_p)) .collect(); let thetas: Vec = ark_std::cfg_iter!(&shape.Ms) - .map(|M| vec_to_ark_mle(M.multiply_vec(&z2).as_slice()).evaluate(&rs)) + .map(|M| vec_to_ark_mle(M.multiply_vec(&z2).as_slice()).evaluate(&rs_p)) .collect(); - let U = U1.fold(U2, &rho_scalar, &rs, &sigmas, &thetas)?; + let U = U1.fold(U2, &rho_scalar, &rs_p, &sigmas, &thetas)?; let W = W1.fold(W2, &rho_scalar)?; Ok(( @@ -195,14 +193,18 @@ where unsafe { cast_field_element::(&rho) }; let s: usize = ((shape.num_constraints - 1).checked_ilog2().unwrap_or(0) + 1) as usize; - let rvec_shape = vec![SQUEEZE_ELEMENTS_BIT_SIZE; s]; - let gamma: G::ScalarField = - random_oracle.squeeze_field_elements_with_sizes(&[SQUEEZE_ELEMENTS_BIT_SIZE])[0]; - let beta = random_oracle.squeeze_field_elements_with_sizes(rvec_shape.as_slice()); + let gamma: G::ScalarField = random_oracle.squeeze_field_elements(1)[0]; + let beta = random_oracle.squeeze_field_elements(s); + + let gamma_powers: Vec = (1..=shape.num_matrices) + .map(|j| gamma.pow([j as u64])) + .collect(); - let claimed_sum = (1..=shape.num_matrices) - .map(|j| gamma.pow([j as u64]) * U1.vs[j - 1]) + let claimed_sum = gamma_powers + .iter() + .zip(U1.vs.iter()) + .map(|(a, b)| *a * b) .sum(); let sumcheck_subclaim = MLSumcheck::verify_as_subprotocol( @@ -212,19 +214,22 @@ where &self.sumcheck_proof, )?; - let rs = sumcheck_subclaim.point; + let rs_p = sumcheck_subclaim.point; let eq1 = EqPolynomial::new(U1.rs.clone()); let eqrs = vec_to_ark_mle(eq1.evals().as_slice()); - let e1 = eqrs.evaluate(&rs); + let e1 = eqrs.evaluate(&rs_p); let eq2 = EqPolynomial::new(beta); let eqb = vec_to_ark_mle(eq2.evals().as_slice()); - let e2 = eqb.evaluate(&rs); + let e2 = eqb.evaluate(&rs_p); - let cl: G::ScalarField = (1..=shape.num_matrices) - .map(|j| gamma.pow([j as u64]) * e1 * self.sigmas[j - 1]) - .sum(); + let cl: G::ScalarField = gamma_powers + .iter() + .zip(self.sigmas.iter()) + .map(|(a, b)| *a * b) + .sum::() + * e1; let cr: G::ScalarField = (0..shape.num_multisets) .map(|i| { @@ -241,7 +246,7 @@ where return Err(Error::InconsistentSubclaim); } - let U = U1.fold(U2, &rho_scalar, &rs, &self.sigmas, &self.thetas)?; + let U = U1.fold(U2, &rho_scalar, &rs_p, &self.sigmas, &self.thetas)?; Ok((U, rho)) } diff --git a/nova/src/folding/mod.rs b/nova/src/folding/mod.rs index 50f86c49a..009aeb5ab 100644 --- a/nova/src/folding/mod.rs +++ b/nova/src/folding/mod.rs @@ -1,4 +1,4 @@ pub mod hypernova; pub mod nova; -mod cyclefold; +pub(crate) mod cyclefold; diff --git a/nova/src/gadgets/cyclefold/hypernova/mod.rs b/nova/src/gadgets/cyclefold/hypernova/mod.rs new file mode 100644 index 000000000..875b96fe8 --- /dev/null +++ b/nova/src/gadgets/cyclefold/hypernova/mod.rs @@ -0,0 +1,450 @@ +#![allow(unused)] +#![deny(unsafe_code)] + +use ark_crypto_primitives::sponge::constraints::{CryptographicSpongeVar, SpongeWithGadget}; +use ark_ec::{ + short_weierstrass::{Projective, SWCurveConfig}, + AdditiveGroup, +}; +use ark_ff::{Field, PrimeField}; +use ark_r1cs_std::{ + boolean::Boolean, + eq::EqGadget, + fields::{fp::FpVar, FieldVar}, + R1CSVar, +}; +use ark_relations::r1cs::SynthesisError; +use ark_spartan::polycommitments::PolyCommitmentScheme; + +pub(crate) mod primary; + +use crate::{ + commitment::CommitmentScheme, + folding::hypernova::{ + cyclefold::{nimfs::SQUEEZE_ELEMENTS_BIT_SIZE, CCSShape}, + ml_sumcheck::protocol::verifier::SQUEEZE_NATIVE_ELEMENTS_NUM, + }, + gadgets::{ + cyclefold::secondary, + nonnative::{cast_field_element_unique, short_weierstrass::NonNativeAffineVar}, + }, +}; + +pub fn multifold( + config: &>::Parameters, + vk: &FpVar, + shape: &CCSShape, + U: &primary::LCCSInstanceFromR1CSVar, + U_secondary: &secondary::RelaxedR1CSInstanceVar, + u: &primary::CCSInstanceFromR1CSVar, + commitment_W_proof: &secondary::ProofVar, + hypernova_proof: &primary::ProofFromR1CSVar, + should_enforce: &Boolean, +) -> Result< + ( + primary::LCCSInstanceFromR1CSVar, + secondary::RelaxedR1CSInstanceVar, + ), + SynthesisError, +> +where + G1: SWCurveConfig, + G2: SWCurveConfig, + C1: PolyCommitmentScheme>, + C2: CommitmentScheme>, + G1::BaseField: PrimeField, + G2::BaseField: PrimeField, + RO: SpongeWithGadget, +{ + let cs = U.cs(); + let mut random_oracle = RO::Var::new(cs.clone(), config); + + random_oracle.absorb(&U_secondary)?; + + random_oracle.absorb(&vk)?; + random_oracle.absorb(&U.var())?; + random_oracle.absorb(&u.var())?; + + let (rho, rho_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let rho = &rho[0]; + let rho_bits = &rho_bits[0]; + let rho_scalar = Boolean::le_bits_to_fp_var(rho_bits)?; + + // HyperNova Verification Circuit - implementation is specific to R1CS origin for constraints + + debug_assert!(shape.num_matrices == 3); + debug_assert!(shape.num_multisets == 2); + debug_assert!(shape.max_cardinality == 2); + + let s: usize = ((shape.num_constraints - 1).checked_ilog2().unwrap_or(0) + 1) as usize; + + let gamma: FpVar = random_oracle.squeeze_field_elements(1)?[0].clone(); + let beta: Vec> = random_oracle.squeeze_field_elements(s)?; + + let gamma_powers: Vec> = (1..=shape.num_matrices) + .map(|j| gamma.pow_le(&Boolean::constant_vec_from_bytes(&j.to_le_bytes()))) + .collect::>, SynthesisError>>()?; + + let mut expected: FpVar = gamma_powers.iter().zip(U.var().vs.iter()).fold( + FpVar::::Constant(G1::ScalarField::ZERO), + |acc, (a, b)| acc + (a * b), + ); + + // (i, \prod_{j != i} (i - j)) + let interpolation_constants = [ + (G1::ScalarField::from(0), G1::ScalarField::from(-6)), // (0 - 1)(0 - 2)(0 - 3) = -6 + (G1::ScalarField::from(1), G1::ScalarField::from(2)), // (1 - 0)(1 - 2)(1 - 3) = 2 + (G1::ScalarField::from(2), G1::ScalarField::from(-2)), // (2 - 0)(2 - 1)(2 - 3) = -2 + (G1::ScalarField::from(3), G1::ScalarField::from(6)), // (3 - 0)(3 - 1)(3 - 2) = 6 + ]; + + random_oracle.absorb(&hypernova_proof.var().poly_info.var())?; + + let mut rs_p: Vec> = vec![]; + for round in 0..s { + random_oracle.absorb(&hypernova_proof.var().sumcheck_proof[round])?; + let r = random_oracle.squeeze_field_elements(SQUEEZE_NATIVE_ELEMENTS_NUM)?[0].clone(); + random_oracle.absorb(&r)?; + + let evals = &hypernova_proof.var().sumcheck_proof[round]; + expected.conditional_enforce_equal(&(&evals[0] + &evals[1]), should_enforce)?; + + // lagrange interpolate and evaluate polynomial + + // \prod_{j} x - j + let prod: FpVar = (0..(shape.max_cardinality + 2)).fold( + FpVar::::Constant(G1::ScalarField::ONE), + |acc, i| acc * (&r - interpolation_constants[i].0), + ); + + // p(x) = \sum_{i} (\prod_{j} x - j) * y[i] / (x - i) * (\prod_{j != i} (i - j)) + // = \sum_{i} y[i] * (\prod_{j != i} x - j) / (\prod_{j != i} i - j) + // = \sum_{i} y[i] * (\prod_{j != i} (x - j) / (j - i)) + expected = (0..(shape.max_cardinality + 2)) + .map(|i| { + let num = &prod * &evals[i]; + let denom = (&r - interpolation_constants[i].0) * interpolation_constants[i].1; + num.mul_by_inverse(&denom) + }) + .collect::>, SynthesisError>>()? + .iter() + .sum(); + + rs_p.push(r); + } + + let e1 = (0..U.var().rs.len()) + .map(|i| { + &U.var().rs[i] * &rs_p[i] + + (FpVar::::Constant(G1::ScalarField::ONE) - &U.var().rs[i]) + * (FpVar::::Constant(G1::ScalarField::ONE) - &rs_p[i]) + }) + .fold( + FpVar::::Constant(G1::ScalarField::ONE), + |acc, x| acc * x, + ); + + let e2 = (0..beta.len()) + .map(|i| { + &beta[i] * &rs_p[i] + + (FpVar::::Constant(G1::ScalarField::ONE) - &beta[i]) + * (FpVar::::Constant(G1::ScalarField::ONE) - &rs_p[i]) + }) + .fold( + FpVar::::Constant(G1::ScalarField::ONE), + |acc, x| acc * x, + ); + + let cl = gamma_powers + .iter() + .zip(hypernova_proof.var().sigmas.iter()) + .fold( + FpVar::::Constant(G1::ScalarField::ZERO), + |acc, (a, b)| acc + (a * b), + ) + * e1; + + let cr = (0..shape.num_multisets) + .map(|i| { + shape.cSs[i].1.iter().fold( + FpVar::::Constant(shape.cSs[i].0), + |acc, j| acc * &hypernova_proof.var().thetas[*j], + ) + }) + .fold( + FpVar::::Constant(G1::ScalarField::ZERO), + |acc, x| acc + x, + ) + * gamma.pow_le(&Boolean::constant_vec_from_bytes( + &(shape.num_matrices + 1).to_le_bytes(), + ))? + * e2; + + expected.conditional_enforce_equal(&(cl + cr), should_enforce)?; + + // End HyperNova Verification Circuit + + let secondary::ProofVar { + U: comm_W_secondary_instance, + commitment_T, + } = &commitment_W_proof; + + // The rest of the secondary public input is reconstructed from primary instances. + let comm_W_secondary_instance = secondary::R1CSInstanceVar::from_allocated_input( + comm_W_secondary_instance, + &U.var().commitment_W, + &u.var().commitment_W, + )?; + let (rho_secondary, g_out) = comm_W_secondary_instance.parse_secondary_io::()?; + rho_secondary.conditional_enforce_equal(rho, should_enforce)?; + + let commitment_W = g_out; + random_oracle.absorb(&comm_W_secondary_instance)?; + random_oracle.absorb(&commitment_T)?; + random_oracle.absorb(&cast_field_element_unique::(rho)?)?; + + let (rho_p, rho_p_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let rho_p = &rho_p[0]; + let rho_p_bits = &rho_p_bits[0]; + + let folded_U = primary::LCCSInstanceFromR1CSVar::new( + commitment_W, + U.var() + .X + .iter() + .zip(u.var().X.iter()) // by assertion, u.X[0] = 1 + .map(|(a, b)| a + &rho_scalar * b) + .collect(), + rs_p, + hypernova_proof + .var() + .sigmas + .iter() + .zip(hypernova_proof.var().thetas.iter()) + .map(|(a, b)| a + &rho_scalar * b) + .collect(), + ); + + let U_secondary = U_secondary.fold(&[( + (&comm_W_secondary_instance, None), + commitment_T, + rho_p, + rho_p_bits, + )])?; + + Ok((folded_U, U_secondary)) +} + +#[cfg(test)] +mod tests { + use super::*; + + use crate::poseidon_config; + use crate::{ + ccs::mle::vec_to_mle, + folding::hypernova::cyclefold::{ + nimfs::{ + CCSInstance, CCSWitness, LCCSInstance, NIMFSProof, RelaxedR1CSInstance, + RelaxedR1CSWitness, + }, + secondary as multifold_secondary, + }, + pedersen::PedersenCommitment, + r1cs::tests::to_field_elements, + test_utils::setup_test_ccs, + }; + use ark_crypto_primitives::sponge::{poseidon::PoseidonSponge, Absorb}; + use ark_ec::short_weierstrass::{Projective, SWCurveConfig}; + use ark_ff::Field; + use ark_r1cs_std::{fields::fp::FpVar, prelude::AllocVar, R1CSVar}; + use ark_relations::r1cs::ConstraintSystem; + use ark_spartan::polycommitments::zeromorph::Zeromorph; + use ark_std::{test_rng, UniformRand}; + + use rayon::iter::{IntoParallelRefIterator, ParallelIterator}; + + #[test] + fn verify_in_circuit() { + verify_in_circuit_with_cycle::< + ark_bn254::g1::Config, + ark_grumpkin::GrumpkinConfig, + Zeromorph, + PedersenCommitment, + >() + .unwrap(); + } + + fn verify_in_circuit_with_cycle() -> Result<(), SynthesisError> + where + G1: SWCurveConfig, + G2: SWCurveConfig, + C1: PolyCommitmentScheme>, + C2: CommitmentScheme, SetupAux = ()>, + G1::BaseField: PrimeField + Absorb, + G2::BaseField: PrimeField + Absorb, + { + let config = poseidon_config(); + + let vk = G1::ScalarField::ONE; + + let mut rng = test_rng(); + let (shape, u, w, ck) = setup_test_ccs::(3, None, Some(&mut rng)); + + let shape_secondary = multifold_secondary::setup_shape::()?; + + let pp_secondary = C2::setup( + shape_secondary.num_vars + shape_secondary.num_constraints, + &(), + ); + + let X = to_field_elements::>((vec![0; shape.num_io]).as_slice()); + let W = CCSWitness::zero(&shape); + + let commitment_W = W.commit::(&ck); + + let s = (shape.num_constraints - 1).checked_ilog2().unwrap_or(0) + 1; + let rs: Vec = (0..s).map(|_| G1::ScalarField::rand(&mut rng)).collect(); + + let z = [X.as_slice(), W.W.as_slice()].concat(); + let vs: Vec = ark_std::cfg_iter!(&shape.Ms) + .map(|M| { + vec_to_mle(M.multiply_vec(&z).as_slice()).evaluate::>(rs.as_slice()) + }) + .collect(); + + let U = + LCCSInstance::::new(&shape, &commitment_W, &X, rs.as_slice(), vs.as_slice()) + .unwrap(); + + let U_secondary = RelaxedR1CSInstance::::new(&shape_secondary); + let W_secondary = RelaxedR1CSWitness::::zero(&shape_secondary); + + let (proof, (folded_U, folded_W), (folded_U_secondary, folded_W_secondary)) = + NIMFSProof::<_, _, _, _, PoseidonSponge>::prove( + &pp_secondary, + &config, + &vk, + (&shape, &shape_secondary), + (&U, &W), + (&U_secondary, &W_secondary), + (&u, &w), + ) + .unwrap(); + + let cs = ConstraintSystem::::new_ref(); + let U_cs = primary::LCCSInstanceFromR1CSVar::::new_input(cs.clone(), || Ok(&U))?; + let U_secondary_cs = + secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { + Ok(&U_secondary) + })?; + let u_cs = primary::CCSInstanceFromR1CSVar::::new_input(cs.clone(), || Ok(&u))?; + + let hypernova_proof = &proof.hypernova_proof; + let comm_W_proof = &proof.commitment_W_proof; + + let vk_cs = FpVar::new_input(cs.clone(), || Ok(vk))?; + let hypernova_proof = + primary::ProofFromR1CSVar::>::new_input( + cs.clone(), + || Ok(hypernova_proof), + )?; + let comm_W_proof = + secondary::ProofVar::::new_input(cs.clone(), || Ok(comm_W_proof))?; + + let (_U_cs, _U_secondary_cs) = multifold::>( + &config, + &vk_cs, + &shape, + &U_cs, + &U_secondary_cs, + &u_cs, + &comm_W_proof, + &hypernova_proof, + &Boolean::TRUE, + )?; + + let _U = _U_cs.value()?; + let _U_secondary = _U_secondary_cs.value()?; + + assert_eq!(_U, folded_U); + shape.is_satisfied_linearized(&_U, &folded_W, &ck).unwrap(); + + assert_eq!(_U_secondary, folded_U_secondary); + shape_secondary + .is_relaxed_satisfied(&_U_secondary, &folded_W_secondary, &pp_secondary) + .unwrap(); + + assert!(cs.is_satisfied().unwrap()); + + // another round. + let (_, u, w, _) = setup_test_ccs(5, Some(&ck), Some(&mut rng)); + + let (proof, (folded_U_2, folded_W_2), (folded_U_secondary_2, folded_W_secondary_2)) = + NIMFSProof::<_, _, _, _, PoseidonSponge>::prove( + &pp_secondary, + &config, + &vk, + (&shape, &shape_secondary), + (&folded_U, &folded_W), + (&folded_U_secondary, &folded_W_secondary), + (&u, &w), + ) + .unwrap(); + + let cs = ConstraintSystem::::new_ref(); + let U_cs = + primary::LCCSInstanceFromR1CSVar::::new_input(cs.clone(), || Ok(&folded_U))?; + let U_secondary_cs = + secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { + Ok(&folded_U_secondary) + })?; + let u_cs = primary::CCSInstanceFromR1CSVar::::new_input(cs.clone(), || Ok(&u))?; + + let hypernova_proof = &proof.hypernova_proof; + let comm_W_proof = &proof.commitment_W_proof; + + let vk_cs = FpVar::new_input(cs.clone(), || Ok(vk))?; + let hypernova_proof = + primary::ProofFromR1CSVar::>::new_input( + cs.clone(), + || Ok(hypernova_proof), + )?; + let comm_W_proof = + secondary::ProofVar::::new_input(cs.clone(), || Ok(comm_W_proof))?; + + let (_U_cs, _U_secondary_cs) = multifold::>( + &config, + &vk_cs, + &shape, + &U_cs, + &U_secondary_cs, + &u_cs, + &comm_W_proof, + &hypernova_proof, + &Boolean::TRUE, + )?; + + let _U = _U_cs.value()?; + let _U_secondary = _U_secondary_cs.value()?; + + assert_eq!(_U, folded_U_2); + shape + .is_satisfied_linearized(&_U, &folded_W_2, &ck) + .unwrap(); + + assert_eq!(_U_secondary, folded_U_secondary_2); + shape_secondary + .is_relaxed_satisfied(&_U_secondary, &folded_W_secondary_2, &pp_secondary) + .unwrap(); + + assert!(cs.is_satisfied().unwrap()); + + Ok(()) + } +} diff --git a/nova/src/gadgets/cyclefold/hypernova/primary.rs b/nova/src/gadgets/cyclefold/hypernova/primary.rs new file mode 100644 index 000000000..2521b092c --- /dev/null +++ b/nova/src/gadgets/cyclefold/hypernova/primary.rs @@ -0,0 +1,561 @@ +use std::{borrow::Borrow, marker::PhantomData}; + +use ark_crypto_primitives::sponge::constraints::{AbsorbGadget, SpongeWithGadget}; +use ark_ec::short_weierstrass::{Projective, SWCurveConfig}; +use ark_ff::{Field, PrimeField}; +use ark_r1cs_std::{ + alloc::{AllocVar, AllocationMode}, + boolean::Boolean, + fields::{fp::FpVar, FieldVar}, + select::CondSelectGadget, + uint8::UInt8, + R1CSVar, +}; +use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError}; +use ark_spartan::polycommitments::{PolyCommitmentScheme, PolyCommitmentTrait}; +use ark_std::fmt::Debug; + +use super::NonNativeAffineVar; +use crate::folding::hypernova::cyclefold::{CCSInstance, HNProof, LCCSInstance}; +use crate::folding::hypernova::ml_sumcheck::PolynomialInfo; + +#[must_use] +#[derive(Debug)] +pub struct CCSInstanceVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + /// Commitment to witness. + pub commitment_W: NonNativeAffineVar, + /// Public input of non-linearized instance. + pub X: Vec>, + + _commitment_scheme: PhantomData, +} + +impl Clone for CCSInstanceVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + fn clone(&self) -> Self { + Self { + commitment_W: self.commitment_W.clone(), + X: self.X.clone(), + _commitment_scheme: self._commitment_scheme, + } + } +} + +#[derive(Debug, Clone)] +pub struct CCSInstanceFromR1CSVar(CCSInstanceVar) +where + G1: SWCurveConfig, + G1::BaseField: PrimeField; + +impl CCSInstanceFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + pub(super) fn var(&self) -> &CCSInstanceVar { + &self.0 + } +} + +impl R1CSVar for CCSInstanceFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + C1: PolyCommitmentScheme>, +{ + type Value = CCSInstance; + + fn cs(&self) -> ConstraintSystemRef { + self.var() + .X + .iter() + .fold(ConstraintSystemRef::None, |cs, x| cs.or(x.cs())) + .or(self.var().commitment_W.cs()) + } + + fn value(&self) -> Result { + let commitment_W = self.var().commitment_W.value()?; + let X = self.var().X.value()?; + Ok(CCSInstance { + commitment_W: vec![commitment_W].into(), + X, + }) + } +} + +impl AllocVar, G1::ScalarField> for CCSInstanceFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + C1: PolyCommitmentScheme>, +{ + fn new_variable>>( + cs: impl Into>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + let ns = cs.into(); + let cs = ns.cs(); + + let r1cs = f()?; + let X = &r1cs.borrow().X; + // Only allocate valid instance, which starts with F::ONE. + assert_eq!(X[0], G1::ScalarField::ONE); + + let commitment_W = NonNativeAffineVar::new_variable( + cs.clone(), + || { + Ok::, SynthesisError>( + r1cs.borrow() + .commitment_W + .clone() + .try_into_affine_point() + .unwrap() + .into(), + ) + }, + mode, + )?; + let alloc_X = X[1..] + .iter() + .map(|x| FpVar::::new_variable(cs.clone(), || Ok(x), mode)); + let X = std::iter::once(Ok(FpVar::constant(G1::ScalarField::ONE))) + .chain(alloc_X) + .collect::>()?; + + Ok(Self(CCSInstanceVar { + commitment_W, + X, + _commitment_scheme: PhantomData, + })) + } +} + +impl AbsorbGadget for CCSInstanceVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + C1: PolyCommitmentScheme>, +{ + fn to_sponge_bytes(&self) -> Result>, SynthesisError> { + unreachable!() + } + + fn to_sponge_field_elements(&self) -> Result>, SynthesisError> { + Ok([ + self.commitment_W.to_sponge_field_elements()?, + (&self.X[1..]).to_sponge_field_elements()?, + ] + .concat()) + } +} + +#[must_use] +#[derive(Debug)] +pub struct LCCSInstanceVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + /// Commitment to witness. + pub commitment_W: NonNativeAffineVar, + /// Public input of linearized instance. Expected to start with `u`. + pub X: Vec>, + /// Random evaluation point of linearized instance. + pub rs: Vec>, + /// Target evaluations for linearized instance. + pub vs: Vec>, + + _commitment_scheme: PhantomData, +} + +impl Clone for LCCSInstanceVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + fn clone(&self) -> Self { + Self { + commitment_W: self.commitment_W.clone(), + X: self.X.clone(), + rs: self.rs.clone(), + vs: self.vs.clone(), + _commitment_scheme: self._commitment_scheme, + } + } +} + +#[derive(Debug, Clone)] +pub struct LCCSInstanceFromR1CSVar(LCCSInstanceVar) +where + G1: SWCurveConfig, + G1::BaseField: PrimeField; + +impl LCCSInstanceFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + pub(super) fn new( + commitment_W: NonNativeAffineVar, + X: Vec>, + rs: Vec>, + vs: Vec>, + ) -> Self { + Self(LCCSInstanceVar { + commitment_W, + X, + rs, + vs, + _commitment_scheme: PhantomData, + }) + } + + pub(super) fn var(&self) -> &LCCSInstanceVar { + &self.0 + } +} + +impl R1CSVar for LCCSInstanceFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + C1: PolyCommitmentScheme>, +{ + type Value = LCCSInstance; + + fn cs(&self) -> ConstraintSystemRef { + self.var() + .X + .iter() + .fold(ConstraintSystemRef::None, |cs, x| cs.or(x.cs())) + .or(self.var().commitment_W.cs()) + .or(self.var().rs.cs()) + .or(self.var().vs.cs()) + } + + fn value(&self) -> Result { + let commitment_W = self.var().commitment_W.value()?; + + let X = self.var().X.value()?; + let rs = self.var().rs.value()?; + let vs = self.var().vs.value()?; + Ok(LCCSInstance { + commitment_W: vec![commitment_W].into(), + X, + rs, + vs, + }) + } +} + +impl AllocVar, G1::ScalarField> for LCCSInstanceFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + C1: PolyCommitmentScheme>, +{ + fn new_variable>>( + cs: impl Into>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + let ns = cs.into(); + let cs = ns.cs(); + + let r1cs = f()?; + let X = &r1cs.borrow().X; + let rs = &r1cs.borrow().rs; + let vs = &r1cs.borrow().vs; + + let commitment_W = NonNativeAffineVar::new_variable( + cs.clone(), + || { + Ok::, SynthesisError>( + r1cs.borrow() + .commitment_W + .clone() + .try_into_affine_point() + .unwrap() + .into(), + ) + }, + mode, + )?; + + let X = X + .iter() + .map(|x| FpVar::::new_variable(cs.clone(), || Ok(x), mode)) + .collect::>()?; + + let rs = rs + .iter() + .map(|r| FpVar::::new_variable(cs.clone(), || Ok(r), mode)) + .collect::>()?; + + let vs = vs + .iter() + .map(|v| FpVar::::new_variable(cs.clone(), || Ok(v), mode)) + .collect::>()?; + + Ok(Self(LCCSInstanceVar { + commitment_W, + X, + rs, + vs, + _commitment_scheme: PhantomData, + })) + } +} + +impl AbsorbGadget for LCCSInstanceVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + C1: PolyCommitmentScheme>, +{ + fn to_sponge_bytes(&self) -> Result>, SynthesisError> { + unreachable!() + } + + fn to_sponge_field_elements(&self) -> Result>, SynthesisError> { + Ok([ + self.commitment_W.to_sponge_field_elements()?, + self.X.to_sponge_field_elements()?, + self.rs.to_sponge_field_elements()?, + self.vs.to_sponge_field_elements()?, + ] + .concat()) + } +} + +impl CondSelectGadget for LCCSInstanceVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + C1: PolyCommitmentScheme>, +{ + fn conditionally_select( + cond: &Boolean, + true_value: &Self, + false_value: &Self, + ) -> Result { + let commitment_W = cond.select(&true_value.commitment_W, &false_value.commitment_W)?; + + let X = true_value + .X + .iter() + .zip(&false_value.X) + .map(|(x1, x2)| cond.select(x1, x2)) + .collect::>()?; + + let rs = true_value + .rs + .iter() + .zip(&false_value.rs) + .map(|(x1, x2)| cond.select(x1, x2)) + .collect::>()?; + + let vs = true_value + .vs + .iter() + .zip(&false_value.vs) + .map(|(x1, x2)| cond.select(x1, x2)) + .collect::>()?; + + Ok(Self { + commitment_W, + X, + rs, + vs, + _commitment_scheme: PhantomData, + }) + } +} + +#[derive(Debug, Clone)] +pub struct PolynomialInfoVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + pub(crate) max_multiplicands: FpVar, + pub(crate) num_variables: FpVar, + pub(crate) num_terms: FpVar, +} + +#[derive(Debug, Clone)] +pub struct PolynomialInfoFromR1CSVar(PolynomialInfoVar) +where + G1: SWCurveConfig, + G1::BaseField: PrimeField; + +impl PolynomialInfoFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + pub(super) fn var(&self) -> &PolynomialInfoVar { + &self.0 + } +} + +impl AllocVar for PolynomialInfoFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + fn new_variable>( + _cs: impl Into>, + f: impl FnOnce() -> Result, + _mode: AllocationMode, + ) -> Result { + let r1cs = f()?; + let max_multiplicands = r1cs.borrow().max_multiplicands as u32; + let num_variables = r1cs.borrow().num_variables as u32; + let num_terms = r1cs.borrow().num_terms as u32; + + let max_multiplicands = + FpVar::::Constant(G1::ScalarField::from(max_multiplicands)); + let num_variables = + FpVar::::Constant(G1::ScalarField::from(num_variables)); + let num_terms = FpVar::::Constant(G1::ScalarField::from(num_terms)); + + Ok(Self(PolynomialInfoVar { + max_multiplicands, + num_variables, + num_terms, + })) + } +} + +impl AbsorbGadget for PolynomialInfoVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, +{ + fn to_sponge_bytes(&self) -> Result>, SynthesisError> { + unreachable!() + } + + fn to_sponge_field_elements(&self) -> Result>, SynthesisError> { + Ok([ + self.max_multiplicands.to_sponge_field_elements()?, + self.num_variables.to_sponge_field_elements()?, + self.num_terms.to_sponge_field_elements()?, + ] + .concat()) + } +} + +#[derive(Debug)] +pub struct ProofVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + RO: SpongeWithGadget, +{ + pub(crate) sumcheck_proof: Vec>>, + pub(crate) poly_info: PI, + pub(crate) sigmas: Vec>, + pub(crate) thetas: Vec>, + _random_oracle: PhantomData, +} + +impl Clone for ProofVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + PI: Clone, + RO: SpongeWithGadget, +{ + fn clone(&self) -> Self { + Self { + sumcheck_proof: self.sumcheck_proof.clone(), + poly_info: self.poly_info.clone(), + sigmas: self.sigmas.clone(), + thetas: self.thetas.clone(), + _random_oracle: self._random_oracle, + } + } +} + +#[derive(Debug, Clone)] +pub struct ProofFromR1CSVar(ProofVar, RO>) +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + RO: SpongeWithGadget; + +impl ProofFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + RO: SpongeWithGadget, +{ + pub(super) fn var(&self) -> &ProofVar, RO> { + &self.0 + } +} + +impl AllocVar, G1::ScalarField> for ProofFromR1CSVar +where + G1: SWCurveConfig, + G1::BaseField: PrimeField, + RO: SpongeWithGadget, +{ + fn new_variable>>( + cs: impl Into>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + let ns = cs.into(); + let cs = ns.cs(); + + let r1cs = f()?; + let sumcheck_proof = &r1cs.borrow().sumcheck_proof; + let poly_info = &r1cs.borrow().poly_info; + let sigmas = &r1cs.borrow().sigmas; + let thetas = &r1cs.borrow().thetas; + + let sumcheck_proof = sumcheck_proof + .iter() + .map(|msg| { + msg.evaluations + .iter() + .map(|eval| { + FpVar::::new_variable(cs.clone(), || Ok(eval), mode) + }) + .collect() + }) + .collect::>()?; + + let poly_info = + PolynomialInfoFromR1CSVar::::new_variable(cs.clone(), || Ok(poly_info), mode)?; + + let sigmas = sigmas + .iter() + .map(|sigma| FpVar::::new_variable(cs.clone(), || Ok(sigma), mode)) + .collect::>()?; + + let thetas = thetas + .iter() + .map(|theta| FpVar::::new_variable(cs.clone(), || Ok(theta), mode)) + .collect::>()?; + + Ok(Self(ProofVar { + sumcheck_proof, + poly_info, + sigmas, + thetas, + _random_oracle: PhantomData, + })) + } +} diff --git a/nova/src/gadgets/cyclefold/mod.rs b/nova/src/gadgets/cyclefold/mod.rs index 7c947f177..424a813c9 100644 --- a/nova/src/gadgets/cyclefold/mod.rs +++ b/nova/src/gadgets/cyclefold/mod.rs @@ -1,642 +1,3 @@ -#![deny(unsafe_code)] - -use ark_crypto_primitives::sponge::constraints::{CryptographicSpongeVar, SpongeWithGadget}; -use ark_ec::short_weierstrass::{Projective, SWCurveConfig}; -use ark_ff::PrimeField; -use ark_r1cs_std::{ - boolean::Boolean, - eq::EqGadget, - fields::{fp::FpVar, FieldVar}, - groups::curves::short_weierstrass::ProjectiveVar, - R1CSVar, ToBitsGadget, -}; -use ark_relations::r1cs::SynthesisError; - -pub(crate) mod primary; +pub(crate) mod hypernova; +pub(crate) mod nova; pub(crate) mod secondary; - -pub use super::nonnative::{cast_field_element_unique, short_weierstrass::NonNativeAffineVar}; -use crate::{ - commitment::CommitmentScheme, folding::nova::cyclefold::nimfs::SQUEEZE_ELEMENTS_BIT_SIZE, -}; - -pub fn multifold( - config: &>::Parameters, - vk: &FpVar, - U: &primary::RelaxedR1CSInstanceVar, - U_secondary: &secondary::RelaxedR1CSInstanceVar, - u: &primary::R1CSInstanceVar, - commitment_T: &NonNativeAffineVar, - proof_secondary: (&secondary::ProofVar, &secondary::ProofVar), - should_enforce: &Boolean, -) -> Result< - ( - primary::RelaxedR1CSInstanceVar, - secondary::RelaxedR1CSInstanceVar, - ), - SynthesisError, -> -where - G1: SWCurveConfig, - G2: SWCurveConfig, - C1: CommitmentScheme>, - C2: CommitmentScheme>, - G1::BaseField: PrimeField, - G2::BaseField: PrimeField, - RO: SpongeWithGadget, -{ - let cs = U.cs(); - let mut random_oracle = RO::Var::new(cs.clone(), config); - - random_oracle.absorb(&vk)?; - random_oracle.absorb(&U)?; - random_oracle.absorb(&u)?; - random_oracle.absorb(&U_secondary)?; - random_oracle.absorb(&commitment_T)?; - - let (r_0, r_0_bits) = random_oracle - .squeeze_nonnative_field_elements_with_sizes::(&[ - SQUEEZE_ELEMENTS_BIT_SIZE, - ])?; - let r_0 = &r_0[0]; - let r_0_bits = &r_0_bits[0]; - let r_0_scalar = Boolean::le_bits_to_fp_var(r_0_bits)?; - - let secondary::ProofVar { - U: comm_E_secondary_instance, - commitment_T: _commitment_T, - } = &proof_secondary.0; - - // The rest of the secondary public input is reconstructed from primary instances. - let comm_E_secondary_instance = secondary::R1CSInstanceVar::from_allocated_input( - comm_E_secondary_instance, - &U.commitment_E, - commitment_T, - )?; - let (r_0_secondary, g_out) = comm_E_secondary_instance.parse_secondary_io::()?; - r_0_secondary.conditional_enforce_equal(r_0, should_enforce)?; - - let commitment_E = g_out; - - random_oracle.absorb(&comm_E_secondary_instance)?; - random_oracle.absorb(&_commitment_T)?; - random_oracle.absorb(&r_0_scalar)?; - - let (r_1, r_1_bits) = random_oracle - .squeeze_nonnative_field_elements_with_sizes::(&[ - SQUEEZE_ELEMENTS_BIT_SIZE, - ])?; - let r_1 = &r_1[0]; - let r_1_bits = &r_1_bits[0]; - - let secondary::ProofVar { - U: comm_W_secondary_instance, - commitment_T: __commitment_T, - } = &proof_secondary.1; - - // See the above comment for `comm_E_secondary_instance`. - let comm_W_secondary_instance = secondary::R1CSInstanceVar::from_allocated_input( - comm_W_secondary_instance, - &U.commitment_W, - &u.commitment_W, - )?; - let (r_0_secondary, g_out) = comm_W_secondary_instance.parse_secondary_io::()?; - r_0_secondary.conditional_enforce_equal(r_0, should_enforce)?; - - let commitment_W = g_out; - random_oracle.absorb(&comm_W_secondary_instance)?; - random_oracle.absorb(&__commitment_T)?; - random_oracle.absorb(&cast_field_element_unique::(r_1)?)?; - - let (r_2, r_2_bits) = random_oracle - .squeeze_nonnative_field_elements_with_sizes::(&[ - SQUEEZE_ELEMENTS_BIT_SIZE, - ])?; - let r_2 = &r_2[0]; - let r_2_bits = &r_2_bits[0]; - - let folded_U = primary::RelaxedR1CSInstanceVar::::new( - commitment_W, - commitment_E, - U.X.iter() - .zip(&u.X) - .map(|(a, b)| a + &r_0_scalar * b) - .collect(), - ); - - let U_secondary = U_secondary.fold(&[ - ( - (&comm_E_secondary_instance, None), - _commitment_T, - r_1, - r_1_bits, - ), - ( - (&comm_W_secondary_instance, None), - __commitment_T, - r_2, - r_2_bits, - ), - ])?; - - Ok((folded_U, U_secondary)) -} - -pub fn multifold_with_relaxed( - config: &>::Parameters, - vk: &FpVar, - U1: &primary::RelaxedR1CSInstanceVar, - U_secondary: &secondary::RelaxedR1CSInstanceVar, - U2: &primary::RelaxedR1CSInstanceVar, - U2_secondary: &secondary::RelaxedR1CSInstanceVar, - commitment_T: &NonNativeAffineVar, - commitment_T_secondary: &ProjectiveVar>, - proof_secondary: ( - &[secondary::ProofVar; 2], // commitment to E requires 2 proofs. - &secondary::ProofVar, - ), - should_enforce: &Boolean, -) -> Result< - ( - primary::RelaxedR1CSInstanceVar, - secondary::RelaxedR1CSInstanceVar, - ), - SynthesisError, -> -where - G1: SWCurveConfig, - G2: SWCurveConfig, - C1: CommitmentScheme>, - C2: CommitmentScheme>, - G1::BaseField: PrimeField, - G2::BaseField: PrimeField, - RO: SpongeWithGadget, -{ - let cs = U1.cs(); - let mut random_oracle = RO::Var::new(cs.clone(), config); - - random_oracle.absorb(&vk)?; - random_oracle.absorb(&U1)?; - random_oracle.absorb(&U2)?; - random_oracle.absorb(&U_secondary)?; - random_oracle.absorb(&commitment_T)?; - - let (r_0, r_0_bits) = random_oracle - .squeeze_nonnative_field_elements_with_sizes::(&[ - SQUEEZE_ELEMENTS_BIT_SIZE, - ])?; - let r_0 = &r_0[0]; - let r_0_bits = &r_0_bits[0]; - let r_0_scalar = Boolean::le_bits_to_fp_var(r_0_bits)?; - let r_0_scalar_square = r_0_scalar.square()?; - - let secondary::ProofVar { - U: comm_E_secondary_instance_0, - commitment_T: _commitment_T_0, - } = &proof_secondary.0[0]; - // The rest of the secondary public input is reconstructed from primary instances. - let comm_E_secondary_instance_0 = secondary::R1CSInstanceVar::from_allocated_input( - comm_E_secondary_instance_0, - &U1.commitment_E, - commitment_T, - )?; - let (r_0_secondary, g_out) = comm_E_secondary_instance_0.parse_secondary_io::()?; - r_0_secondary.conditional_enforce_equal(r_0, should_enforce)?; - - random_oracle.absorb(&comm_E_secondary_instance_0)?; - random_oracle.absorb(&_commitment_T_0)?; - random_oracle.absorb(&r_0_scalar)?; - - let (r_1, r_1_bits) = random_oracle - .squeeze_nonnative_field_elements_with_sizes::(&[ - SQUEEZE_ELEMENTS_BIT_SIZE, - ])?; - let r_1 = &r_1[0]; - let r_1_bits = &r_1_bits[0]; - - let secondary::ProofVar { - U: comm_E_secondary_instance_1, - commitment_T: _commitment_T_1, - } = &proof_secondary.0[1]; - let comm_E_secondary_instance_1 = secondary::R1CSInstanceVar::from_allocated_input( - comm_E_secondary_instance_1, - &g_out, - &U2.commitment_E, - )?; - let (r_0_secondary, g_out) = comm_E_secondary_instance_1.parse_secondary_io::()?; - // TODO: `r` shouldn't be contained in secondary vars, reconstruct it from ro output. - for (r_square_bit, r_0_bit) in r_0_scalar_square - .to_bits_le()? - .iter() - .zip(&r_0_secondary.to_bits_le()?) - { - r_square_bit.conditional_enforce_equal(r_0_bit, should_enforce)?; - } - - let commitment_E = g_out; - - random_oracle.absorb(&comm_E_secondary_instance_1)?; - random_oracle.absorb(&_commitment_T_1)?; - random_oracle.absorb(&cast_field_element_unique::(r_1)?)?; - - let (r_2, r_2_bits) = random_oracle - .squeeze_nonnative_field_elements_with_sizes::(&[ - SQUEEZE_ELEMENTS_BIT_SIZE, - ])?; - let r_2 = &r_2[0]; - let r_2_bits = &r_2_bits[0]; - - let secondary::ProofVar { - U: comm_W_secondary_instance, - commitment_T: __commitment_T, - } = &proof_secondary.1; - // See the above comment for `comm_E_secondary_instance`. - let comm_W_secondary_instance = secondary::R1CSInstanceVar::from_allocated_input( - comm_W_secondary_instance, - &U1.commitment_W, - &U2.commitment_W, - )?; - let (r_0_secondary, g_out) = comm_W_secondary_instance.parse_secondary_io::()?; - r_0_secondary.conditional_enforce_equal(r_0, should_enforce)?; - - let commitment_W = g_out; - - random_oracle.absorb(&comm_W_secondary_instance)?; - random_oracle.absorb(&__commitment_T)?; - random_oracle.absorb(&cast_field_element_unique::(r_2)?)?; - - let (r_3, r_3_bits) = random_oracle - .squeeze_nonnative_field_elements_with_sizes::(&[ - SQUEEZE_ELEMENTS_BIT_SIZE, - ])?; - let r_3 = &r_3[0]; - let r_3_bits = &r_3_bits[0]; - - let folded_U = primary::RelaxedR1CSInstanceVar::::new( - commitment_W, - commitment_E, - U1.X.iter() - .zip(&U2.X) - .map(|(x1, x2)| x1 + &r_0_scalar * x2) - .collect(), - ); - - let U1_secondary = U_secondary.fold(&[ - ( - (&comm_E_secondary_instance_0, None), - _commitment_T_0, - r_1, - &r_1_bits[..], - ), - ( - (&comm_E_secondary_instance_1, None), - _commitment_T_1, - r_2, - r_2_bits, - ), - ( - (&comm_W_secondary_instance, None), - __commitment_T, - r_3, - r_3_bits, - ), - ])?; - - random_oracle.absorb(&cast_field_element_unique::(r_3)?)?; - random_oracle.absorb(&U1_secondary)?; - random_oracle.absorb(&U2_secondary)?; - random_oracle.absorb(&commitment_T_secondary)?; - - let (r, r_bits) = - random_oracle.squeeze_nonnative_field_elements_with_sizes::(&[ - SQUEEZE_ELEMENTS_BIT_SIZE, - ])?; - let r = &r[0]; - let r_bits = &r_bits[0]; - - let U_secondary = U1_secondary.fold(&[( - (&U2_secondary.into(), Some(&U2_secondary.commitment_E)), - commitment_T_secondary, - r, - &r_bits[..], - )])?; - - Ok((folded_U, U_secondary)) -} - -#[cfg(test)] -mod tests { - use super::*; - use crate::{ - folding::nova::cyclefold::{ - nimfs::{NIMFSProof, RelaxedR1CSInstance, RelaxedR1CSWitness}, - secondary as multifold_secondary, - }, - pedersen::PedersenCommitment, - poseidon_config, - test_utils::setup_test_r1cs, - }; - use ark_crypto_primitives::sponge::{poseidon::PoseidonSponge, Absorb}; - - use ark_ff::Field; - use ark_r1cs_std::{fields::fp::FpVar, prelude::AllocVar, R1CSVar}; - use ark_relations::r1cs::ConstraintSystem; - - #[test] - fn verify_in_circuit() { - verify_in_circuit_with_cycle::< - ark_pallas::PallasConfig, - ark_vesta::VestaConfig, - PedersenCommitment, - PedersenCommitment, - >() - .unwrap(); - } - - fn verify_in_circuit_with_cycle() -> Result<(), SynthesisError> - where - G1: SWCurveConfig, - G2: SWCurveConfig, - C1: CommitmentScheme, SetupAux = ()>, - C2: CommitmentScheme, SetupAux = ()>, - G1::BaseField: PrimeField + Absorb, - G2::BaseField: PrimeField + Absorb, - C1::PP: Clone, - { - let config = poseidon_config(); - - let vk = G1::ScalarField::ONE; - - let (shape, u, w, pp) = setup_test_r1cs::(3, None, &()); - let shape_secondary = multifold_secondary::setup_shape::()?; - - let pp_secondary = C2::setup( - shape_secondary.num_vars + shape_secondary.num_constraints, - &(), - ); - - let U = RelaxedR1CSInstance::::new(&shape); - let W = RelaxedR1CSWitness::::zero(&shape); - - let U_secondary = RelaxedR1CSInstance::::new(&shape_secondary); - let W_secondary = RelaxedR1CSWitness::::zero(&shape_secondary); - - let (proof, (folded_U, folded_W), (folded_U_secondary, folded_W_secondary)) = - NIMFSProof::<_, _, _, _, PoseidonSponge>::prove( - &pp, - &pp_secondary, - &config, - &vk, - (&shape, &shape_secondary), - (&U, &W), - (&U_secondary, &W_secondary), - (&u, &w), - ) - .unwrap(); - - let cs = ConstraintSystem::::new_ref(); - let U_cs = primary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || Ok(&U))?; - let U_secondary_cs = - secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { - Ok(&U_secondary) - })?; - let u_cs = primary::R1CSInstanceVar::::new_input(cs.clone(), || Ok(&u))?; - - let commitment_T_cs = - NonNativeAffineVar::new_input(cs.clone(), || Ok(proof.commitment_T.into()))?; - - let comm_E_proof = &proof.commitment_E_proof; - let comm_W_proof = &proof.commitment_W_proof; - - let vk_cs = FpVar::new_input(cs.clone(), || Ok(vk))?; - let comm_E_proof = - secondary::ProofVar::::new_input(cs.clone(), || Ok(&comm_E_proof[0]))?; - let comm_W_proof = - secondary::ProofVar::::new_input(cs.clone(), || Ok(comm_W_proof))?; - let proof_cs = (&comm_E_proof, &comm_W_proof); - - let (_U_cs, _U_secondary_cs) = multifold::>( - &config, - &vk_cs, - &U_cs, - &U_secondary_cs, - &u_cs, - &commitment_T_cs, - proof_cs, - &Boolean::TRUE, - )?; - - let _U = _U_cs.value()?; - let _U_secondary = _U_secondary_cs.value()?; - - assert_eq!(_U, folded_U); - shape.is_relaxed_satisfied(&_U, &folded_W, &pp).unwrap(); - - assert_eq!(_U_secondary, folded_U_secondary); - shape_secondary - .is_relaxed_satisfied(&_U_secondary, &folded_W_secondary, &pp_secondary) - .unwrap(); - - assert!(cs.is_satisfied().unwrap()); - - // another round. - let (_, u, w, _) = setup_test_r1cs::(5, Some(&pp), &()); - - let (proof, (folded_U_2, folded_W_2), (folded_U_secondary_2, folded_W_secondary_2)) = - NIMFSProof::<_, _, _, _, PoseidonSponge>::prove( - &pp, - &pp_secondary, - &config, - &vk, - (&shape, &shape_secondary), - (&folded_U, &folded_W), - (&folded_U_secondary, &folded_W_secondary), - (&u, &w), - ) - .unwrap(); - - let cs = ConstraintSystem::::new_ref(); - let U_cs = - primary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || Ok(&folded_U))?; - let U_secondary_cs = - secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { - Ok(&folded_U_secondary) - })?; - let u_cs = primary::R1CSInstanceVar::::new_input(cs.clone(), || Ok(&u))?; - - let commitment_T_cs = - NonNativeAffineVar::new_input(cs.clone(), || Ok(proof.commitment_T.into()))?; - - let comm_E_proof = &proof.commitment_E_proof; - let comm_W_proof = &proof.commitment_W_proof; - - let vk_cs = FpVar::new_input(cs.clone(), || Ok(vk))?; - let comm_E_proof = - secondary::ProofVar::::new_input(cs.clone(), || Ok(&comm_E_proof[0]))?; - let comm_W_proof = - secondary::ProofVar::::new_input(cs.clone(), || Ok(comm_W_proof))?; - let proof_cs = (&comm_E_proof, &comm_W_proof); - - let (_U_cs, _U_secondary_cs) = multifold::>( - &config, - &vk_cs, - &U_cs, - &U_secondary_cs, - &u_cs, - &commitment_T_cs, - proof_cs, - &Boolean::TRUE, - )?; - - let _U = _U_cs.value()?; - let _U_secondary = _U_secondary_cs.value()?; - - assert_eq!(_U, folded_U_2); - shape.is_relaxed_satisfied(&_U, &folded_W_2, &pp).unwrap(); - - assert_eq!(_U_secondary, folded_U_secondary_2); - shape_secondary - .is_relaxed_satisfied(&_U_secondary, &folded_W_secondary_2, &pp_secondary) - .unwrap(); - - assert!(cs.is_satisfied().unwrap()); - - Ok(()) - } - - #[test] - fn verify_relaxed_in_circuit() { - verify_relaxed_in_circuit_with_cycle::< - ark_pallas::PallasConfig, - ark_vesta::VestaConfig, - PedersenCommitment, - PedersenCommitment, - >() - .unwrap(); - } - - fn verify_relaxed_in_circuit_with_cycle() -> Result<(), SynthesisError> - where - G1: SWCurveConfig, - G2: SWCurveConfig, - C1: CommitmentScheme, SetupAux = ()>, - C2: CommitmentScheme, SetupAux = ()>, - G1::BaseField: PrimeField + Absorb, - G2::BaseField: PrimeField + Absorb, - C1::PP: Clone, - { - let config = poseidon_config(); - - let vk = G1::ScalarField::ONE; - - let (shape, u, w, pp) = setup_test_r1cs::(3, None, &()); - let shape_secondary = multifold_secondary::setup_shape::()?; - - let pp_secondary = C2::setup( - shape_secondary.num_vars + shape_secondary.num_constraints, - &(), - ); - - let U = RelaxedR1CSInstance::::new(&shape); - let W = RelaxedR1CSWitness::::zero(&shape); - - let U_secondary = RelaxedR1CSInstance::::new(&shape_secondary); - let W_secondary = RelaxedR1CSWitness::::zero(&shape_secondary); - let (_, (U2, W2), (U2_secondary, W2_secondary)) = - NIMFSProof::<_, _, _, _, PoseidonSponge>::prove( - &pp, - &pp_secondary, - &config, - &vk, - (&shape, &shape_secondary), - (&U, &W), - (&U_secondary, &W_secondary), - (&u, &w), - ) - .unwrap(); - - let (_, u, w, _) = setup_test_r1cs::(5, Some(&pp), &()); - let U1 = RelaxedR1CSInstance::from(&u); - let W1 = RelaxedR1CSWitness::from_r1cs_witness(&shape, &w); - - let U1_secondary = RelaxedR1CSInstance::::new(&shape_secondary); - let W1_secondary = RelaxedR1CSWitness::::zero(&shape_secondary); - - let (proof, (U, W), (U_secondary, W_secondary)) = - NIMFSProof::<_, _, _, _, PoseidonSponge>::prove_with_relaxed( - &pp, - &pp_secondary, - &config, - &vk, - (&shape, &shape_secondary), - (&U1, &W1), - (&U1_secondary, &W1_secondary), - (&U2, &W2), - (&U2_secondary, &W2_secondary), - ) - .unwrap(); - - let cs = ConstraintSystem::::new_ref(); - - let U1_cs = primary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || Ok(&U1))?; - let U1_secondary_cs = - secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { - Ok(&U1_secondary) - })?; - let U2_cs = primary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || Ok(&U2))?; - let U2_secondary_cs = - secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { - Ok(&U2_secondary) - })?; - let commitment_T_secondary_cs = > as AllocVar< - Projective, - G2::BaseField, - >>::new_input(cs.clone(), || { - Ok(proof.proof_secondary.commitment_T.into()) - })?; - - let commitment_T_cs = - NonNativeAffineVar::new_input(cs.clone(), || Ok(proof.commitment_T.into()))?; - - let comm_E_proof = &proof.commitment_E_proof; - let comm_W_proof = &proof.commitment_W_proof; - - let vk_cs = FpVar::new_input(cs.clone(), || Ok(vk))?; - let comm_E_proof = [ - secondary::ProofVar::::new_input(cs.clone(), || Ok(&comm_E_proof[0]))?, - secondary::ProofVar::::new_input(cs.clone(), || Ok(&comm_E_proof[1]))?, - ]; - let comm_W_proof = - secondary::ProofVar::::new_input(cs.clone(), || Ok(comm_W_proof))?; - let proof_cs = (&comm_E_proof, &comm_W_proof); - - let (_U_cs, _U_secondary_cs) = - multifold_with_relaxed::>( - &config, - &vk_cs, - &U1_cs, - &U1_secondary_cs, - &U2_cs, - &U2_secondary_cs, - &commitment_T_cs, - &commitment_T_secondary_cs, - proof_cs, - &Boolean::TRUE, - )?; - - let _U = _U_cs.value()?; - let _U_secondary = _U_secondary_cs.value()?; - - assert_eq!(_U, U); - shape.is_relaxed_satisfied(&U, &W, &pp).unwrap(); - - assert_eq!(_U_secondary, U_secondary); - shape_secondary - .is_relaxed_satisfied(&U_secondary, &W_secondary, &pp_secondary) - .unwrap(); - - assert!(cs.is_satisfied().unwrap()); - - Ok(()) - } -} diff --git a/nova/src/gadgets/cyclefold/nova/mod.rs b/nova/src/gadgets/cyclefold/nova/mod.rs new file mode 100644 index 000000000..85f908207 --- /dev/null +++ b/nova/src/gadgets/cyclefold/nova/mod.rs @@ -0,0 +1,645 @@ +#![deny(unsafe_code)] + +use ark_crypto_primitives::sponge::constraints::{CryptographicSpongeVar, SpongeWithGadget}; +use ark_ec::short_weierstrass::{Projective, SWCurveConfig}; +use ark_ff::PrimeField; +use ark_r1cs_std::{ + boolean::Boolean, + eq::EqGadget, + fields::{fp::FpVar, FieldVar}, + groups::curves::short_weierstrass::ProjectiveVar, + R1CSVar, ToBitsGadget, +}; +use ark_relations::r1cs::SynthesisError; + +pub(crate) mod primary; + +use crate::{ + commitment::CommitmentScheme, + folding::nova::cyclefold::nimfs::SQUEEZE_ELEMENTS_BIT_SIZE, + gadgets::{ + cyclefold::secondary, + nonnative::{cast_field_element_unique, short_weierstrass::NonNativeAffineVar}, + }, +}; + +pub fn multifold( + config: &>::Parameters, + vk: &FpVar, + U: &primary::RelaxedR1CSInstanceVar, + U_secondary: &secondary::RelaxedR1CSInstanceVar, + u: &primary::R1CSInstanceVar, + commitment_T: &NonNativeAffineVar, + proof_secondary: (&secondary::ProofVar, &secondary::ProofVar), + should_enforce: &Boolean, +) -> Result< + ( + primary::RelaxedR1CSInstanceVar, + secondary::RelaxedR1CSInstanceVar, + ), + SynthesisError, +> +where + G1: SWCurveConfig, + G2: SWCurveConfig, + C1: CommitmentScheme>, + C2: CommitmentScheme>, + G1::BaseField: PrimeField, + G2::BaseField: PrimeField, + RO: SpongeWithGadget, +{ + let cs = U.cs(); + let mut random_oracle = RO::Var::new(cs.clone(), config); + + random_oracle.absorb(&vk)?; + random_oracle.absorb(&U)?; + random_oracle.absorb(&u)?; + random_oracle.absorb(&U_secondary)?; + random_oracle.absorb(&commitment_T)?; + + let (r_0, r_0_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let r_0 = &r_0[0]; + let r_0_bits = &r_0_bits[0]; + let r_0_scalar = Boolean::le_bits_to_fp_var(r_0_bits)?; + + let secondary::ProofVar { + U: comm_E_secondary_instance, + commitment_T: _commitment_T, + } = &proof_secondary.0; + + // The rest of the secondary public input is reconstructed from primary instances. + let comm_E_secondary_instance = secondary::R1CSInstanceVar::from_allocated_input( + comm_E_secondary_instance, + &U.commitment_E, + commitment_T, + )?; + let (r_0_secondary, g_out) = comm_E_secondary_instance.parse_secondary_io::()?; + r_0_secondary.conditional_enforce_equal(r_0, should_enforce)?; + + let commitment_E = g_out; + + random_oracle.absorb(&comm_E_secondary_instance)?; + random_oracle.absorb(&_commitment_T)?; + random_oracle.absorb(&r_0_scalar)?; + + let (r_1, r_1_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let r_1 = &r_1[0]; + let r_1_bits = &r_1_bits[0]; + + let secondary::ProofVar { + U: comm_W_secondary_instance, + commitment_T: __commitment_T, + } = &proof_secondary.1; + + // See the above comment for `comm_E_secondary_instance`. + let comm_W_secondary_instance = secondary::R1CSInstanceVar::from_allocated_input( + comm_W_secondary_instance, + &U.commitment_W, + &u.commitment_W, + )?; + let (r_0_secondary, g_out) = comm_W_secondary_instance.parse_secondary_io::()?; + r_0_secondary.conditional_enforce_equal(r_0, should_enforce)?; + + let commitment_W = g_out; + random_oracle.absorb(&comm_W_secondary_instance)?; + random_oracle.absorb(&__commitment_T)?; + random_oracle.absorb(&cast_field_element_unique::(r_1)?)?; + + let (r_2, r_2_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let r_2 = &r_2[0]; + let r_2_bits = &r_2_bits[0]; + + let folded_U = primary::RelaxedR1CSInstanceVar::::new( + commitment_W, + commitment_E, + U.X.iter() + .zip(&u.X) + .map(|(a, b)| a + &r_0_scalar * b) + .collect(), + ); + + let U_secondary = U_secondary.fold(&[ + ( + (&comm_E_secondary_instance, None), + _commitment_T, + r_1, + r_1_bits, + ), + ( + (&comm_W_secondary_instance, None), + __commitment_T, + r_2, + r_2_bits, + ), + ])?; + + Ok((folded_U, U_secondary)) +} + +pub fn multifold_with_relaxed( + config: &>::Parameters, + vk: &FpVar, + U1: &primary::RelaxedR1CSInstanceVar, + U_secondary: &secondary::RelaxedR1CSInstanceVar, + U2: &primary::RelaxedR1CSInstanceVar, + U2_secondary: &secondary::RelaxedR1CSInstanceVar, + commitment_T: &NonNativeAffineVar, + commitment_T_secondary: &ProjectiveVar>, + proof_secondary: ( + &[secondary::ProofVar; 2], // commitment to E requires 2 proofs. + &secondary::ProofVar, + ), + should_enforce: &Boolean, +) -> Result< + ( + primary::RelaxedR1CSInstanceVar, + secondary::RelaxedR1CSInstanceVar, + ), + SynthesisError, +> +where + G1: SWCurveConfig, + G2: SWCurveConfig, + C1: CommitmentScheme>, + C2: CommitmentScheme>, + G1::BaseField: PrimeField, + G2::BaseField: PrimeField, + RO: SpongeWithGadget, +{ + let cs = U1.cs(); + let mut random_oracle = RO::Var::new(cs.clone(), config); + + random_oracle.absorb(&vk)?; + random_oracle.absorb(&U1)?; + random_oracle.absorb(&U2)?; + random_oracle.absorb(&U_secondary)?; + random_oracle.absorb(&commitment_T)?; + + let (r_0, r_0_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let r_0 = &r_0[0]; + let r_0_bits = &r_0_bits[0]; + let r_0_scalar = Boolean::le_bits_to_fp_var(r_0_bits)?; + let r_0_scalar_square = r_0_scalar.square()?; + + let secondary::ProofVar { + U: comm_E_secondary_instance_0, + commitment_T: _commitment_T_0, + } = &proof_secondary.0[0]; + // The rest of the secondary public input is reconstructed from primary instances. + let comm_E_secondary_instance_0 = secondary::R1CSInstanceVar::from_allocated_input( + comm_E_secondary_instance_0, + &U1.commitment_E, + commitment_T, + )?; + let (r_0_secondary, g_out) = comm_E_secondary_instance_0.parse_secondary_io::()?; + r_0_secondary.conditional_enforce_equal(r_0, should_enforce)?; + + random_oracle.absorb(&comm_E_secondary_instance_0)?; + random_oracle.absorb(&_commitment_T_0)?; + random_oracle.absorb(&r_0_scalar)?; + + let (r_1, r_1_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let r_1 = &r_1[0]; + let r_1_bits = &r_1_bits[0]; + + let secondary::ProofVar { + U: comm_E_secondary_instance_1, + commitment_T: _commitment_T_1, + } = &proof_secondary.0[1]; + let comm_E_secondary_instance_1 = secondary::R1CSInstanceVar::from_allocated_input( + comm_E_secondary_instance_1, + &g_out, + &U2.commitment_E, + )?; + let (r_0_secondary, g_out) = comm_E_secondary_instance_1.parse_secondary_io::()?; + // TODO: `r` shouldn't be contained in secondary vars, reconstruct it from ro output. + for (r_square_bit, r_0_bit) in r_0_scalar_square + .to_bits_le()? + .iter() + .zip(&r_0_secondary.to_bits_le()?) + { + r_square_bit.conditional_enforce_equal(r_0_bit, should_enforce)?; + } + + let commitment_E = g_out; + + random_oracle.absorb(&comm_E_secondary_instance_1)?; + random_oracle.absorb(&_commitment_T_1)?; + random_oracle.absorb(&cast_field_element_unique::(r_1)?)?; + + let (r_2, r_2_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let r_2 = &r_2[0]; + let r_2_bits = &r_2_bits[0]; + + let secondary::ProofVar { + U: comm_W_secondary_instance, + commitment_T: __commitment_T, + } = &proof_secondary.1; + // See the above comment for `comm_E_secondary_instance`. + let comm_W_secondary_instance = secondary::R1CSInstanceVar::from_allocated_input( + comm_W_secondary_instance, + &U1.commitment_W, + &U2.commitment_W, + )?; + let (r_0_secondary, g_out) = comm_W_secondary_instance.parse_secondary_io::()?; + r_0_secondary.conditional_enforce_equal(r_0, should_enforce)?; + + let commitment_W = g_out; + + random_oracle.absorb(&comm_W_secondary_instance)?; + random_oracle.absorb(&__commitment_T)?; + random_oracle.absorb(&cast_field_element_unique::(r_2)?)?; + + let (r_3, r_3_bits) = random_oracle + .squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let r_3 = &r_3[0]; + let r_3_bits = &r_3_bits[0]; + + let folded_U = primary::RelaxedR1CSInstanceVar::::new( + commitment_W, + commitment_E, + U1.X.iter() + .zip(&U2.X) + .map(|(x1, x2)| x1 + &r_0_scalar * x2) + .collect(), + ); + + let U1_secondary = U_secondary.fold(&[ + ( + (&comm_E_secondary_instance_0, None), + _commitment_T_0, + r_1, + &r_1_bits[..], + ), + ( + (&comm_E_secondary_instance_1, None), + _commitment_T_1, + r_2, + r_2_bits, + ), + ( + (&comm_W_secondary_instance, None), + __commitment_T, + r_3, + r_3_bits, + ), + ])?; + + random_oracle.absorb(&cast_field_element_unique::(r_3)?)?; + random_oracle.absorb(&U1_secondary)?; + random_oracle.absorb(&U2_secondary)?; + random_oracle.absorb(&commitment_T_secondary)?; + + let (r, r_bits) = + random_oracle.squeeze_nonnative_field_elements_with_sizes::(&[ + SQUEEZE_ELEMENTS_BIT_SIZE, + ])?; + let r = &r[0]; + let r_bits = &r_bits[0]; + + let U_secondary = U1_secondary.fold(&[( + (&U2_secondary.into(), Some(&U2_secondary.commitment_E)), + commitment_T_secondary, + r, + &r_bits[..], + )])?; + + Ok((folded_U, U_secondary)) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::{ + folding::nova::cyclefold::{ + nimfs::{NIMFSProof, RelaxedR1CSInstance, RelaxedR1CSWitness}, + secondary as multifold_secondary, + }, + pedersen::PedersenCommitment, + poseidon_config, + test_utils::setup_test_r1cs, + }; + use ark_crypto_primitives::sponge::{poseidon::PoseidonSponge, Absorb}; + + use ark_ff::Field; + use ark_r1cs_std::{fields::fp::FpVar, prelude::AllocVar, R1CSVar}; + use ark_relations::r1cs::ConstraintSystem; + + #[test] + fn verify_in_circuit() { + verify_in_circuit_with_cycle::< + ark_pallas::PallasConfig, + ark_vesta::VestaConfig, + PedersenCommitment, + PedersenCommitment, + >() + .unwrap(); + } + + fn verify_in_circuit_with_cycle() -> Result<(), SynthesisError> + where + G1: SWCurveConfig, + G2: SWCurveConfig, + C1: CommitmentScheme, SetupAux = ()>, + C2: CommitmentScheme, SetupAux = ()>, + G1::BaseField: PrimeField + Absorb, + G2::BaseField: PrimeField + Absorb, + C1::PP: Clone, + { + let config = poseidon_config(); + + let vk = G1::ScalarField::ONE; + + let (shape, u, w, pp) = setup_test_r1cs::(3, None, &()); + let shape_secondary = multifold_secondary::setup_shape::()?; + + let pp_secondary = C2::setup( + shape_secondary.num_vars + shape_secondary.num_constraints, + &(), + ); + + let U = RelaxedR1CSInstance::::new(&shape); + let W = RelaxedR1CSWitness::::zero(&shape); + + let U_secondary = RelaxedR1CSInstance::::new(&shape_secondary); + let W_secondary = RelaxedR1CSWitness::::zero(&shape_secondary); + + let (proof, (folded_U, folded_W), (folded_U_secondary, folded_W_secondary)) = + NIMFSProof::<_, _, _, _, PoseidonSponge>::prove( + &pp, + &pp_secondary, + &config, + &vk, + (&shape, &shape_secondary), + (&U, &W), + (&U_secondary, &W_secondary), + (&u, &w), + ) + .unwrap(); + + let cs = ConstraintSystem::::new_ref(); + let U_cs = primary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || Ok(&U))?; + let U_secondary_cs = + secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { + Ok(&U_secondary) + })?; + let u_cs = primary::R1CSInstanceVar::::new_input(cs.clone(), || Ok(&u))?; + + let commitment_T_cs = + NonNativeAffineVar::new_input(cs.clone(), || Ok(proof.commitment_T.into()))?; + + let comm_E_proof = &proof.commitment_E_proof; + let comm_W_proof = &proof.commitment_W_proof; + + let vk_cs = FpVar::new_input(cs.clone(), || Ok(vk))?; + let comm_E_proof = + secondary::ProofVar::::new_input(cs.clone(), || Ok(&comm_E_proof[0]))?; + let comm_W_proof = + secondary::ProofVar::::new_input(cs.clone(), || Ok(comm_W_proof))?; + let proof_cs = (&comm_E_proof, &comm_W_proof); + + let (_U_cs, _U_secondary_cs) = multifold::>( + &config, + &vk_cs, + &U_cs, + &U_secondary_cs, + &u_cs, + &commitment_T_cs, + proof_cs, + &Boolean::TRUE, + )?; + + let _U = _U_cs.value()?; + let _U_secondary = _U_secondary_cs.value()?; + + assert_eq!(_U, folded_U); + shape.is_relaxed_satisfied(&_U, &folded_W, &pp).unwrap(); + + assert_eq!(_U_secondary, folded_U_secondary); + shape_secondary + .is_relaxed_satisfied(&_U_secondary, &folded_W_secondary, &pp_secondary) + .unwrap(); + + assert!(cs.is_satisfied().unwrap()); + + // another round. + let (_, u, w, _) = setup_test_r1cs::(5, Some(&pp), &()); + + let (proof, (folded_U_2, folded_W_2), (folded_U_secondary_2, folded_W_secondary_2)) = + NIMFSProof::<_, _, _, _, PoseidonSponge>::prove( + &pp, + &pp_secondary, + &config, + &vk, + (&shape, &shape_secondary), + (&folded_U, &folded_W), + (&folded_U_secondary, &folded_W_secondary), + (&u, &w), + ) + .unwrap(); + + let cs = ConstraintSystem::::new_ref(); + let U_cs = + primary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || Ok(&folded_U))?; + let U_secondary_cs = + secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { + Ok(&folded_U_secondary) + })?; + let u_cs = primary::R1CSInstanceVar::::new_input(cs.clone(), || Ok(&u))?; + + let commitment_T_cs = + NonNativeAffineVar::new_input(cs.clone(), || Ok(proof.commitment_T.into()))?; + + let comm_E_proof = &proof.commitment_E_proof; + let comm_W_proof = &proof.commitment_W_proof; + + let vk_cs = FpVar::new_input(cs.clone(), || Ok(vk))?; + let comm_E_proof = + secondary::ProofVar::::new_input(cs.clone(), || Ok(&comm_E_proof[0]))?; + let comm_W_proof = + secondary::ProofVar::::new_input(cs.clone(), || Ok(comm_W_proof))?; + let proof_cs = (&comm_E_proof, &comm_W_proof); + + let (_U_cs, _U_secondary_cs) = multifold::>( + &config, + &vk_cs, + &U_cs, + &U_secondary_cs, + &u_cs, + &commitment_T_cs, + proof_cs, + &Boolean::TRUE, + )?; + + let _U = _U_cs.value()?; + let _U_secondary = _U_secondary_cs.value()?; + + assert_eq!(_U, folded_U_2); + shape.is_relaxed_satisfied(&_U, &folded_W_2, &pp).unwrap(); + + assert_eq!(_U_secondary, folded_U_secondary_2); + shape_secondary + .is_relaxed_satisfied(&_U_secondary, &folded_W_secondary_2, &pp_secondary) + .unwrap(); + + assert!(cs.is_satisfied().unwrap()); + + Ok(()) + } + + #[test] + fn verify_relaxed_in_circuit() { + verify_relaxed_in_circuit_with_cycle::< + ark_pallas::PallasConfig, + ark_vesta::VestaConfig, + PedersenCommitment, + PedersenCommitment, + >() + .unwrap(); + } + + fn verify_relaxed_in_circuit_with_cycle() -> Result<(), SynthesisError> + where + G1: SWCurveConfig, + G2: SWCurveConfig, + C1: CommitmentScheme, SetupAux = ()>, + C2: CommitmentScheme, SetupAux = ()>, + G1::BaseField: PrimeField + Absorb, + G2::BaseField: PrimeField + Absorb, + C1::PP: Clone, + { + let config = poseidon_config(); + + let vk = G1::ScalarField::ONE; + + let (shape, u, w, pp) = setup_test_r1cs::(3, None, &()); + let shape_secondary = multifold_secondary::setup_shape::()?; + + let pp_secondary = C2::setup( + shape_secondary.num_vars + shape_secondary.num_constraints, + &(), + ); + + let U = RelaxedR1CSInstance::::new(&shape); + let W = RelaxedR1CSWitness::::zero(&shape); + + let U_secondary = RelaxedR1CSInstance::::new(&shape_secondary); + let W_secondary = RelaxedR1CSWitness::::zero(&shape_secondary); + let (_, (U2, W2), (U2_secondary, W2_secondary)) = + NIMFSProof::<_, _, _, _, PoseidonSponge>::prove( + &pp, + &pp_secondary, + &config, + &vk, + (&shape, &shape_secondary), + (&U, &W), + (&U_secondary, &W_secondary), + (&u, &w), + ) + .unwrap(); + + let (_, u, w, _) = setup_test_r1cs::(5, Some(&pp), &()); + let U1 = RelaxedR1CSInstance::from(&u); + let W1 = RelaxedR1CSWitness::from_r1cs_witness(&shape, &w); + + let U1_secondary = RelaxedR1CSInstance::::new(&shape_secondary); + let W1_secondary = RelaxedR1CSWitness::::zero(&shape_secondary); + + let (proof, (U, W), (U_secondary, W_secondary)) = + NIMFSProof::<_, _, _, _, PoseidonSponge>::prove_with_relaxed( + &pp, + &pp_secondary, + &config, + &vk, + (&shape, &shape_secondary), + (&U1, &W1), + (&U1_secondary, &W1_secondary), + (&U2, &W2), + (&U2_secondary, &W2_secondary), + ) + .unwrap(); + + let cs = ConstraintSystem::::new_ref(); + + let U1_cs = primary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || Ok(&U1))?; + let U1_secondary_cs = + secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { + Ok(&U1_secondary) + })?; + let U2_cs = primary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || Ok(&U2))?; + let U2_secondary_cs = + secondary::RelaxedR1CSInstanceVar::::new_input(cs.clone(), || { + Ok(&U2_secondary) + })?; + let commitment_T_secondary_cs = > as AllocVar< + Projective, + G2::BaseField, + >>::new_input(cs.clone(), || { + Ok(proof.proof_secondary.commitment_T.into()) + })?; + + let commitment_T_cs = + NonNativeAffineVar::new_input(cs.clone(), || Ok(proof.commitment_T.into()))?; + + let comm_E_proof = &proof.commitment_E_proof; + let comm_W_proof = &proof.commitment_W_proof; + + let vk_cs = FpVar::new_input(cs.clone(), || Ok(vk))?; + let comm_E_proof = [ + secondary::ProofVar::::new_input(cs.clone(), || Ok(&comm_E_proof[0]))?, + secondary::ProofVar::::new_input(cs.clone(), || Ok(&comm_E_proof[1]))?, + ]; + let comm_W_proof = + secondary::ProofVar::::new_input(cs.clone(), || Ok(comm_W_proof))?; + let proof_cs = (&comm_E_proof, &comm_W_proof); + + let (_U_cs, _U_secondary_cs) = + multifold_with_relaxed::>( + &config, + &vk_cs, + &U1_cs, + &U1_secondary_cs, + &U2_cs, + &U2_secondary_cs, + &commitment_T_cs, + &commitment_T_secondary_cs, + proof_cs, + &Boolean::TRUE, + )?; + + let _U = _U_cs.value()?; + let _U_secondary = _U_secondary_cs.value()?; + + assert_eq!(_U, U); + shape.is_relaxed_satisfied(&U, &W, &pp).unwrap(); + + assert_eq!(_U_secondary, U_secondary); + shape_secondary + .is_relaxed_satisfied(&U_secondary, &W_secondary, &pp_secondary) + .unwrap(); + + assert!(cs.is_satisfied().unwrap()); + + Ok(()) + } +} diff --git a/nova/src/gadgets/cyclefold/primary.rs b/nova/src/gadgets/cyclefold/nova/primary.rs similarity index 100% rename from nova/src/gadgets/cyclefold/primary.rs rename to nova/src/gadgets/cyclefold/nova/primary.rs diff --git a/nova/src/gadgets/cyclefold/secondary.rs b/nova/src/gadgets/cyclefold/secondary.rs index 141b1b396..e30c259a4 100644 --- a/nova/src/gadgets/cyclefold/secondary.rs +++ b/nova/src/gadgets/cyclefold/secondary.rs @@ -21,13 +21,13 @@ use ark_r1cs_std::{ }; use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError}; -use super::{cast_field_element_unique, NonNativeAffineVar}; use crate::{ commitment::CommitmentScheme, folding::nova::cyclefold::{ nimfs::{R1CSInstance, RelaxedR1CSInstance}, secondary::{Circuit as SecondaryCircuit, Proof}, }, + gadgets::nonnative::{cast_field_element_unique, short_weierstrass::NonNativeAffineVar}, }; #[must_use]