From fd942bda713082239738c97c02a1e8ad02ecdfd5 Mon Sep 17 00:00:00 2001 From: arnaucube Date: Wed, 19 Jun 2024 16:31:15 +0200 Subject: [PATCH] Implement HyperNova's AugmentedFCircuit (#112) - add LCCCS.hash methods (native & r1cs) - add HyperNova's AugmentedFCircuit with tests --- .../src/folding/circuits/sum_check.rs | 60 +- folding-schemes/src/folding/hypernova/cccs.rs | 38 +- .../src/folding/hypernova/circuits.rs | 563 +++++++++++++++++- .../src/folding/hypernova/lcccs.rs | 60 +- folding-schemes/src/folding/hypernova/mod.rs | 21 + .../src/folding/hypernova/nimfs.rs | 117 ++-- 6 files changed, 753 insertions(+), 106 deletions(-) diff --git a/folding-schemes/src/folding/circuits/sum_check.rs b/folding-schemes/src/folding/circuits/sum_check.rs index ceda394..f06b4f9 100644 --- a/folding-schemes/src/folding/circuits/sum_check.rs +++ b/folding-schemes/src/folding/circuits/sum_check.rs @@ -1,26 +1,28 @@ -use crate::utils::espresso::sum_check::SumCheck; -use crate::utils::virtual_polynomial::VPAuxInfo; -use crate::{ - transcript::{poseidon::PoseidonTranscript, TranscriptVar}, - utils::sum_check::{structs::IOPProof, IOPSumCheck}, -}; -use ark_crypto_primitives::sponge::Absorb; -use ark_ec::{CurveGroup, Group}; /// Heavily inspired from testudo: https://github.com/cryptonetlab/testudo/tree/master /// Some changes: /// - Typings to better stick to ark_poly's API /// - Uses `folding-schemes`' own `TranscriptVar` trait and `PoseidonTranscriptVar` struct /// - API made closer to gadgets found in `folding-schemes` +use ark_crypto_primitives::sponge::Absorb; +use ark_ec::{CurveGroup, Group}; use ark_ff::PrimeField; use ark_poly::{univariate::DensePolynomial, DenseUVPolynomial}; use ark_r1cs_std::{ alloc::{AllocVar, AllocationMode}, + boolean::Boolean, eq::EqGadget, - fields::fp::FpVar, + fields::{fp::FpVar, FieldVar}, }; use ark_relations::r1cs::{Namespace, SynthesisError}; use std::{borrow::Borrow, marker::PhantomData}; +use crate::utils::espresso::sum_check::SumCheck; +use crate::utils::virtual_polynomial::VPAuxInfo; +use crate::{ + transcript::{poseidon::PoseidonTranscript, TranscriptVar}, + utils::sum_check::{structs::IOPProof, IOPSumCheck}, +}; + #[derive(Clone, Debug)] pub struct DensePolynomialVar { pub coeffs: Vec>, @@ -47,10 +49,16 @@ impl AllocVar, F> for DensePolynomialVar { impl DensePolynomialVar { pub fn eval_at_zero(&self) -> FpVar { + if self.coeffs.is_empty() { + return FpVar::::zero(); + } self.coeffs[0].clone() } pub fn eval_at_one(&self) -> FpVar { + if self.coeffs.is_empty() { + return FpVar::::zero(); + } let mut res = self.coeffs[0].clone(); for i in 1..self.coeffs.len() { res = &res + &self.coeffs[i]; @@ -59,6 +67,9 @@ impl DensePolynomialVar { } pub fn evaluate(&self, r: &FpVar) -> FpVar { + if self.coeffs.is_empty() { + return FpVar::::zero(); + } let mut eval = self.coeffs[0].clone(); let mut power = r.clone(); @@ -73,7 +84,7 @@ impl DensePolynomialVar { #[derive(Clone, Debug)] pub struct IOPProofVar { // We have to be generic over a CurveGroup because instantiating a IOPProofVar will call IOPSumCheck which requires a CurveGroup - pub proofs: Vec>, + pub proofs: Vec>, // = IOPProof.proofs pub claim: FpVar, } @@ -148,6 +159,7 @@ impl SumCheckVerifierGadget { iop_proof_var: &IOPProofVar, poly_aux_info_var: &VPAuxInfoVar, transcript_var: &mut impl TranscriptVar, + enabled: Boolean, ) -> Result<(Vec>, Vec>), SynthesisError> { let mut e_vars = vec![iop_proof_var.claim.clone()]; let mut r_vars: Vec> = Vec::new(); @@ -157,7 +169,7 @@ impl SumCheckVerifierGadget { for poly_var in iop_proof_var.proofs.iter() { let res = poly_var.eval_at_one() + poly_var.eval_at_zero(); let e_var = e_vars.last().ok_or(SynthesisError::Unsatisfiable)?; - res.enforce_equal(e_var)?; + res.conditional_enforce_equal(e_var, &enabled)?; transcript_var.absorb_vec(&poly_var.coeffs)?; let r_i_var = transcript_var.get_challenge()?; e_vars.push(poly_var.evaluate(&r_i_var)); @@ -170,17 +182,6 @@ impl SumCheckVerifierGadget { #[cfg(test)] mod tests { - use crate::{ - folding::circuits::sum_check::{IOPProofVar, VPAuxInfoVar}, - transcript::{ - poseidon::{poseidon_canonical_config, PoseidonTranscript, PoseidonTranscriptVar}, - Transcript, TranscriptVar, - }, - utils::{ - sum_check::{structs::IOPProof, IOPSumCheck, SumCheck}, - virtual_polynomial::VirtualPolynomial, - }, - }; use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb}; use ark_ec::CurveGroup; use ark_ff::Field; @@ -193,7 +194,18 @@ mod tests { use ark_relations::r1cs::ConstraintSystem; use std::sync::Arc; - use super::SumCheckVerifierGadget; + use super::*; + use crate::{ + folding::circuits::sum_check::{IOPProofVar, VPAuxInfoVar}, + transcript::{ + poseidon::{poseidon_canonical_config, PoseidonTranscript, PoseidonTranscriptVar}, + Transcript, TranscriptVar, + }, + utils::{ + sum_check::{structs::IOPProof, IOPSumCheck, SumCheck}, + virtual_polynomial::VirtualPolynomial, + }, + }; pub type TestSumCheckProof = (VirtualPolynomial, PoseidonConfig, IOPProof); @@ -232,10 +244,12 @@ mod tests { IOPProofVar::::new_witness(cs.clone(), || Ok(&sum_check)).unwrap(); let poly_aux_info_var = VPAuxInfoVar::::new_witness(cs.clone(), || Ok(virtual_poly.aux_info)).unwrap(); + let enabled = Boolean::::new_witness(cs.clone(), || Ok(true)).unwrap(); let res = SumCheckVerifierGadget::::verify( &iop_proof_var, &poly_aux_info_var, &mut poseidon_var, + enabled, ); assert!(res.is_ok()); diff --git a/folding-schemes/src/folding/hypernova/cccs.rs b/folding-schemes/src/folding/hypernova/cccs.rs index c13f7d8..1494049 100644 --- a/folding-schemes/src/folding/hypernova/cccs.rs +++ b/folding-schemes/src/folding/hypernova/cccs.rs @@ -6,24 +6,17 @@ use std::sync::Arc; use ark_std::rand::Rng; +use super::Witness; use crate::ccs::CCS; use crate::commitment::{ pedersen::{Params as PedersenParams, Pedersen}, CommitmentScheme, }; -use crate::utils::hypercube::BooleanHypercube; use crate::utils::mle::dense_vec_to_dense_mle; use crate::utils::vec::mat_vec_mul; use crate::utils::virtual_polynomial::{build_eq_x_r_vec, VirtualPolynomial}; use crate::Error; -/// Witness for the LCCCS & CCCS, containing the w vector, and the r_w used as randomness in the Pedersen commitment. -#[derive(Debug, Clone)] -pub struct Witness { - pub w: Vec, - pub r_w: F, // randomness used in the Pedersen commitment of w -} - /// Committed CCS instance #[derive(Debug, Clone)] pub struct CCCS { @@ -92,6 +85,16 @@ impl CCS { } impl CCCS { + pub fn dummy(l: usize) -> CCCS + where + C::ScalarField: PrimeField, + { + CCCS:: { + C: C::zero(), + x: vec![C::ScalarField::zero(); l], + } + } + /// Perform the check of the CCCS instance described at section 4.1 pub fn check_relation( &self, @@ -109,14 +112,10 @@ impl CCCS { let z: Vec = [vec![C::ScalarField::one()], self.x.clone(), w.w.to_vec()].concat(); - // A CCCS relation is satisfied if the q(x) multivariate polynomial evaluates to zero in the hypercube - let q_x = ccs.compute_q(&z)?; - - for x in BooleanHypercube::new(ccs.s) { - if !q_x.evaluate(&x)?.is_zero() { - return Err(Error::NotSatisfied); - } - } + // A CCCS relation is satisfied if the q(x) multivariate polynomial evaluates to zero in + // the hypercube, evaluating over the whole boolean hypercube for a normal-sized instance + // would take too much, this checks the CCS relation of the CCCS. + ccs.check_relation(&z)?; Ok(()) } @@ -124,12 +123,13 @@ impl CCCS { #[cfg(test)] pub mod tests { - use super::*; - use crate::ccs::tests::{get_test_ccs, get_test_z}; + use ark_pallas::Fr; use ark_std::test_rng; use ark_std::UniformRand; - use ark_pallas::Fr; + use super::*; + use crate::ccs::tests::{get_test_ccs, get_test_z}; + use crate::utils::hypercube::BooleanHypercube; /// Do some sanity checks on q(x). It's a multivariable polynomial and it should evaluate to zero inside the /// hypercube, but to not-zero outside the hypercube. diff --git a/folding-schemes/src/folding/hypernova/circuits.rs b/folding-schemes/src/folding/hypernova/circuits.rs index d42330c..06449f4 100644 --- a/folding-schemes/src/folding/hypernova/circuits.rs +++ b/folding-schemes/src/folding/hypernova/circuits.rs @@ -1,24 +1,52 @@ /// Implementation of [HyperNova](https://eprint.iacr.org/2023/573.pdf) NIMFS verifier circuit -use ark_crypto_primitives::sponge::Absorb; +use ark_crypto_primitives::crh::{ + poseidon::constraints::{CRHGadget, CRHParametersVar}, + CRHSchemeGadget, +}; +use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb}; use ark_ec::{CurveGroup, Group}; use ark_ff::PrimeField; use ark_r1cs_std::{ alloc::{AllocVar, AllocationMode}, + boolean::Boolean, eq::EqGadget, fields::{fp::FpVar, FieldVar}, + groups::GroupOpsBounds, + prelude::CurveVar, + R1CSVar, ToConstraintFieldGadget, +}; +use ark_relations::r1cs::{ + ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, Namespace, SynthesisError, }; -use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError}; +use ark_std::{fmt::Debug, ops::Neg, One, Zero}; use core::{borrow::Borrow, marker::PhantomData}; -use super::{cccs::CCCS, lcccs::LCCCS, nimfs::Proof}; +use super::{ + cccs::CCCS, + lcccs::LCCCS, + nimfs::{NIMFSProof, NIMFS}, + Witness, +}; use crate::folding::circuits::{ nonnative::affine::NonNativeAffineVar, sum_check::{IOPProofVar, SumCheckVerifierGadget, VPAuxInfoVar}, utils::EqEvalGadget, - CF1, + CF1, CF2, }; +use crate::folding::nova::get_r1cs_from_cs; +use crate::frontend::FCircuit; use crate::utils::virtual_polynomial::VPAuxInfo; -use crate::{ccs::CCS, transcript::TranscriptVar}; +use crate::Error; +use crate::{ + ccs::{ + r1cs::{extract_r1cs, extract_w_x}, + CCS, + }, + transcript::{ + poseidon::{PoseidonTranscript, PoseidonTranscriptVar}, + Transcript, TranscriptVar, + }, +}; /// Committed CCS instance #[derive(Debug, Clone)] @@ -97,6 +125,41 @@ where } } +impl LCCCSVar +where + C: CurveGroup, + ::ScalarField: Absorb, + ::BaseField: ark_ff::PrimeField, +{ + /// [`LCCCSVar`].hash implements the LCCCS instance hash compatible with the native + /// implementation from LCCCS.hash. + /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the LCCCS. + /// Additionally it returns the vector of the field elements from the self parameters, so they + /// can be reused in other gadgets avoiding recalculating (reconstraining) them. + #[allow(clippy::type_complexity)] + pub fn hash( + self, + crh_params: &CRHParametersVar>, + i: FpVar>, + z_0: Vec>>, + z_i: Vec>>, + ) -> Result<(FpVar>, Vec>>), SynthesisError> { + let U_vec = [ + self.C.to_constraint_field()?, + vec![self.u], + self.x, + self.r_x, + self.v, + ] + .concat(); + let input = [vec![i], z_0, z_i, U_vec.clone()].concat(); + Ok(( + CRHGadget::::evaluate(crh_params, &input)?, + U_vec, + )) + } +} + /// ProofVar defines a multifolding proof #[derive(Debug)] pub struct ProofVar { @@ -104,13 +167,13 @@ pub struct ProofVar { #[allow(clippy::type_complexity)] pub sigmas_thetas: (Vec>>>, Vec>>>), } -impl AllocVar, CF1> for ProofVar +impl AllocVar, CF1> for ProofVar where C: CurveGroup, ::BaseField: PrimeField, ::ScalarField: Absorb, { - fn new_variable>>( + fn new_variable>>( cs: impl Into>>, f: impl FnOnce() -> Result, mode: AllocationMode, @@ -162,7 +225,25 @@ where running_instances: &[LCCCSVar], new_instances: &[CCCSVar], proof: ProofVar, + enabled: Boolean, ) -> Result, SynthesisError> { + // absorb instances to transcript + for U_i in running_instances { + let v = [ + U_i.C.to_constraint_field()?, + vec![U_i.u.clone()], + U_i.x.clone(), + U_i.r_x.clone(), + U_i.v.clone(), + ] + .concat(); + transcript.absorb_vec(&v)?; + } + for u_i in new_instances { + let v = [u_i.C.to_constraint_field()?, u_i.x.clone()].concat(); + transcript.absorb_vec(&v)?; + } + // get the challenges let gamma_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"gamma"); let gamma_scalar: FpVar> = @@ -195,8 +276,12 @@ where } // verify the interactive part of the sumcheck - let (e_vars, r_vars) = - SumCheckVerifierGadget::::verify(&proof.sc_proof, &vp_aux_info, &mut transcript)?; + let (e_vars, r_vars) = SumCheckVerifierGadget::::verify( + &proof.sc_proof, + &vp_aux_info, + &mut transcript, + enabled.clone(), + )?; // extract the randomness from the sumcheck let r_x_prime = r_vars.clone(); @@ -215,7 +300,7 @@ where .collect(), r_x_prime.clone(), )?; - computed_c.enforce_equal(&e_vars[e_vars.len() - 1])?; + computed_c.conditional_enforce_equal(&e_vars[e_vars.len() - 1], &enabled)?; // get the folding challenge let rho_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"rho"); @@ -345,16 +430,310 @@ fn compute_c_gadget( Ok(c) } +#[derive(Debug, Clone)] +pub struct AugmentedFCircuit< + C1: CurveGroup, + C2: CurveGroup, + GC2: CurveVar>, + FC: FCircuit>, +> where + for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>, +{ + pub _c2: PhantomData, + pub _gc2: PhantomData, + pub poseidon_config: PoseidonConfig>, + pub ccs: CCS, // CCS of the AugmentedFCircuit + pub i: Option>, + pub i_usize: Option, + pub z_0: Option>, + pub z_i: Option>, + pub external_inputs: Option>, + pub u_i_C: Option, // u_i.C + pub U_i: Option>, + pub U_i1_C: Option, // U_{i+1}.C + pub F: FC, // F circuit + pub x: Option>, // public input (u_{i+1}.x[0]) + pub nimfs_proof: Option>, +} + +impl AugmentedFCircuit +where + C1: CurveGroup, + C2: CurveGroup, + GC2: CurveVar> + ToConstraintFieldGadget>, + FC: FCircuit>, + ::BaseField: PrimeField, + ::BaseField: PrimeField, + ::ScalarField: Absorb, + ::ScalarField: Absorb, + C1: CurveGroup, + for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>, +{ + pub fn default( + poseidon_config: &PoseidonConfig>, + F_circuit: FC, + ccs: CCS, + ) -> Self { + Self { + _c2: PhantomData, + _gc2: PhantomData, + poseidon_config: poseidon_config.clone(), + ccs, + i: None, + i_usize: None, + z_0: None, + z_i: None, + external_inputs: None, + u_i_C: None, + U_i: None, + U_i1_C: None, + F: F_circuit, + x: None, + nimfs_proof: None, + } + } + + pub fn empty( + poseidon_config: &PoseidonConfig>, + F_circuit: FC, + ccs: Option>, + ) -> Result { + let initial_ccs = CCS { + // m, n, s, s_prime and M will be overwritten by the `upper_bound_ccs' method + m: 0, + n: 0, + l: 2, // io_len + s: 1, + s_prime: 1, + t: 3, // note: this is only supports R1CS for the moment + q: 2, + d: 2, + S: vec![vec![0, 1], vec![2]], + c: vec![C1::ScalarField::one(), C1::ScalarField::one().neg()], + M: vec![], + }; + let mut augmented_f_circuit = Self::default(poseidon_config, F_circuit, initial_ccs); + if ccs.is_some() { + augmented_f_circuit.ccs = ccs.unwrap(); + } else { + augmented_f_circuit.ccs = augmented_f_circuit.upper_bound_ccs()?; + } + Ok(augmented_f_circuit) + } + + /// This method computes the CCS parameters. This is used because there is a circular + /// dependency between the AugmentedFCircuit CCS and the CCS parameters m & n & s & s'. + /// For a stable FCircuit circuit, the CCS parameters can be computed in advance and can be + /// feed in as parameter for the AugmentedFCircuit::empty method to avoid computing them there. + pub fn upper_bound_ccs(&self) -> Result, Error> { + let r1cs = get_r1cs_from_cs::>(self.clone()).unwrap(); + let mut ccs = CCS::from_r1cs(r1cs.clone()); + + let z_0 = vec![C1::ScalarField::zero(); self.F.state_len()]; + let mut W_i = + Witness::::new(vec![C1::ScalarField::zero(); ccs.n - ccs.l - 1]); + let mut U_i = LCCCS::::dummy(ccs.l, ccs.t, ccs.s); + let mut w_i = W_i.clone(); + let mut u_i = CCCS::::dummy(ccs.l); + + let n_iters = 3; + + for _ in 0..n_iters { + let mut transcript_p: PoseidonTranscript = + PoseidonTranscript::::new(&self.poseidon_config.clone()); + let (nimfs_proof, U_i1, _) = NIMFS::>::prove( + &mut transcript_p, + &ccs, + &[U_i.clone()], + &[u_i.clone()], + &[W_i.clone()], + &[w_i.clone()], + ) + .unwrap(); + + let augmented_f_circuit = Self { + _c2: PhantomData, + _gc2: PhantomData, + poseidon_config: self.poseidon_config.clone(), + ccs: ccs.clone(), + i: Some(C1::ScalarField::zero()), + i_usize: Some(0), + z_0: Some(z_0.clone()), + z_i: Some(z_0.clone()), + external_inputs: Some(vec![]), + u_i_C: Some(u_i.C), + U_i: Some(U_i.clone()), + U_i1_C: Some(U_i1.C), + F: self.F.clone(), + x: Some(C1::ScalarField::zero()), + nimfs_proof: Some(nimfs_proof), + }; + + let cs: ConstraintSystem; + (cs, ccs) = augmented_f_circuit.compute_cs_ccs()?; + + // prepare instances for next loop iteration + let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::(&cs); // includes 1 and public inputs + u_i = CCCS:: { + C: u_i.C, + x: r1cs_x_i1, + }; + w_i = Witness:: { + w: r1cs_w_i1.clone(), + r_w: C1::ScalarField::one(), + }; + W_i = Witness::::dummy(&ccs); + U_i = LCCCS::::dummy(ccs.l, ccs.t, ccs.s); + } + Ok(ccs) + } + + /// returns the cs (ConstraintSystem) and the CCS out of the AugmentedFCircuit + #[allow(clippy::type_complexity)] + fn compute_cs_ccs( + &self, + ) -> Result<(ConstraintSystem, CCS), Error> { + let cs = ConstraintSystem::::new_ref(); + self.clone().generate_constraints(cs.clone())?; + cs.finalize(); + let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?; + let r1cs = extract_r1cs::(&cs); + let ccs = CCS::from_r1cs(r1cs.clone()); + + Ok((cs, ccs)) + } +} + +impl ConstraintSynthesizer> for AugmentedFCircuit +where + C1: CurveGroup, + C2: CurveGroup, + GC2: CurveVar> + ToConstraintFieldGadget>, + FC: FCircuit>, + ::BaseField: PrimeField, + ::BaseField: PrimeField, + ::ScalarField: Absorb, + ::ScalarField: Absorb, + C1: CurveGroup, + for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>, +{ + fn generate_constraints(self, cs: ConstraintSystemRef>) -> Result<(), SynthesisError> { + let i = FpVar::>::new_witness(cs.clone(), || { + Ok(self.i.unwrap_or_else(CF1::::zero)) + })?; + let z_0 = Vec::>>::new_witness(cs.clone(), || { + Ok(self + .z_0 + .unwrap_or(vec![CF1::::zero(); self.F.state_len()])) + })?; + let z_i = Vec::>>::new_witness(cs.clone(), || { + Ok(self + .z_i + .unwrap_or(vec![CF1::::zero(); self.F.state_len()])) + })?; + let external_inputs = Vec::>>::new_witness(cs.clone(), || { + Ok(self + .external_inputs + .unwrap_or(vec![CF1::::zero(); self.F.external_inputs_len()])) + })?; + + let U_dummy = LCCCS::::dummy(self.ccs.l, self.ccs.t, self.ccs.s); + + let U_i = + LCCCSVar::::new_witness(cs.clone(), || Ok(self.U_i.unwrap_or(U_dummy.clone())))?; + let U_i1_C = NonNativeAffineVar::new_witness(cs.clone(), || { + Ok(self.U_i1_C.unwrap_or_else(C1::zero)) + })?; + let mu = 1; // Note: at this commit, only 2-to-1 instance fold is supported + let nu = 1; + let nimfs_proof_dummy = NIMFSProof::::dummy(&self.ccs, mu, nu); + let nimfs_proof = ProofVar::::new_witness(cs.clone(), || { + Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy)) + })?; + + let crh_params = CRHParametersVar::::new_constant( + cs.clone(), + self.poseidon_config.clone(), + )?; + + // get z_{i+1} from the F circuit + let i_usize = self.i_usize.unwrap_or(0); + let z_i1 = + self.F + .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?; + + let is_basecase = i.is_zero()?; + let is_not_basecase = is_basecase.not(); + + // Primary Part + // P.1. Compute u_i.x + // u_i.x[0] = H(i, z_0, z_i, U_i) + let (u_i_x, _) = U_i + .clone() + .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?; + + // P.2. Construct u_i + let u_i = CCCSVar:: { + // u_i.C is provided by the prover as witness + C: NonNativeAffineVar::::new_witness(cs.clone(), || { + Ok(self.u_i_C.unwrap_or(C1::zero())) + })?, + // u_i.x is computed in step 1 + x: vec![u_i_x], + }; + + // P.3. NIMFS.verify, obtains U_{i+1} by folding [U_i] & [u_i]. + // Notice that NIMFSGadget::fold_committed_instance does not fold C. We set `U_i1.C` to + // unconstrained witnesses `U_i1_C` respectively. Its correctness will be checked on the + // other curve. + let transcript = + PoseidonTranscriptVar::::new(cs.clone(), &self.poseidon_config); + let mut U_i1 = NIMFSGadget::::verify( + cs.clone(), + &self.ccs.clone(), + transcript, + &[U_i.clone()], + &[u_i.clone()], + nimfs_proof, + is_not_basecase.clone(), + )?; + U_i1.C = U_i1_C; + + // P.4.a compute and check the first output of F' + // Base case: u_{i+1}.x[0] == H((1, z_0, z_{i+1}, U_{i+1}) + // Non-base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{i+1}) + let (u_i1_x, _) = U_i1.clone().hash( + &crh_params, + i + FpVar::>::one(), + z_0.clone(), + z_i1.clone(), + )?; + let (u_i1_x_base, _) = U_i1.hash( + &crh_params, + FpVar::>::one(), + z_0.clone(), + z_i1.clone(), + )?; + + let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?; + x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?; + + Ok(()) + } +} + #[cfg(test)] mod tests { - use ark_pallas::{Fr, Projective}; + use ark_bn254::{Fr, G1Projective as Projective}; + use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2}; use ark_r1cs_std::{alloc::AllocVar, fields::fp::FpVar, R1CSVar}; - use ark_relations::r1cs::ConstraintSystem; use ark_std::{test_rng, UniformRand}; + use std::time::Instant; use super::*; use crate::{ ccs::{ + r1cs::extract_w_x, tests::{get_test_ccs, get_test_z}, CCS, }, @@ -362,7 +741,9 @@ mod tests { folding::hypernova::{ nimfs::NIMFS, utils::{compute_c, compute_sigmas_thetas}, + Witness, }, + frontend::tests::CubicFCircuit, transcript::{ poseidon::{poseidon_canonical_config, PoseidonTranscript, PoseidonTranscriptVar}, Transcript, @@ -553,6 +934,7 @@ mod tests { ProofVar::::new_witness(cs.clone(), || Ok(proof.clone())).unwrap(); let transcriptVar = PoseidonTranscriptVar::::new(cs.clone(), &poseidon_config); + let enabled = Boolean::::new_witness(cs.clone(), || Ok(true)).unwrap(); let folded_lcccsVar = NIMFSGadget::::verify( cs.clone(), &ccs, @@ -560,9 +942,166 @@ mod tests { &lcccs_instancesVar, &cccs_instancesVar, proofVar, + enabled, ) .unwrap(); assert!(cs.is_satisfied().unwrap()); assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u); } + + /// test that checks the native LCCCS.hash vs the R1CS constraints version + #[test] + pub fn test_lcccs_hash() { + let mut rng = test_rng(); + let poseidon_config = poseidon_canonical_config::(); + + let ccs = get_test_ccs(); + let z1 = get_test_z::(3); + + let (pedersen_params, _) = + Pedersen::::setup(&mut rng, ccs.n - ccs.l - 1).unwrap(); + + let i = Fr::from(3_u32); + let z_0 = vec![Fr::from(3_u32)]; + let z_i = vec![Fr::from(3_u32)]; + let (lcccs, _) = ccs.to_lcccs(&mut rng, &pedersen_params, &z1).unwrap(); + let h = lcccs + .clone() + .hash(&poseidon_config, i, z_0.clone(), z_i.clone()) + .unwrap(); + + let cs = ConstraintSystem::::new_ref(); + + let crh_params = CRHParametersVar::::new_constant(cs.clone(), poseidon_config).unwrap(); + let iVar = FpVar::::new_witness(cs.clone(), || Ok(i)).unwrap(); + let z_0Var = Vec::>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap(); + let z_iVar = Vec::>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap(); + let lcccsVar = LCCCSVar::::new_witness(cs.clone(), || Ok(lcccs)).unwrap(); + let (hVar, _) = lcccsVar + .clone() + .hash(&crh_params, iVar.clone(), z_0Var.clone(), z_iVar.clone()) + .unwrap(); + assert!(cs.is_satisfied().unwrap()); + + // check that the natively computed and in-circuit computed hashes match + assert_eq!(hVar.value().unwrap(), h); + } + + #[test] + pub fn test_augmented_f_circuit() { + let mut rng = test_rng(); + let poseidon_config = poseidon_canonical_config::(); + + let start = Instant::now(); + let F_circuit = CubicFCircuit::::new(()).unwrap(); + let mut augmented_f_circuit = AugmentedFCircuit::< + Projective, + Projective2, + GVar2, + CubicFCircuit, + >::empty(&poseidon_config, F_circuit, None) + .unwrap(); + let ccs = augmented_f_circuit.ccs.clone(); + println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed()); + println!("CCS m x n: {} x {}", ccs.m, ccs.n); + + let (pedersen_params, _) = + Pedersen::::setup(&mut rng, ccs.n - ccs.l - 1).unwrap(); + + // first step + let z_0 = vec![Fr::from(3_u32)]; + let mut z_i = z_0.clone(); + + let W_dummy = Witness::::new(vec![Fr::zero(); ccs.n - ccs.l - 1]); + let U_dummy = LCCCS::::dummy(ccs.l, ccs.t, ccs.s); + let w_dummy = W_dummy.clone(); + let u_dummy = CCCS::::dummy(ccs.l); + + // set the initial dummy instances + let mut W_i = W_dummy.clone(); + let mut U_i = U_dummy.clone(); + let mut w_i = w_dummy.clone(); + let mut u_i = u_dummy.clone(); + u_i.x = vec![U_i + .hash(&poseidon_config, Fr::zero(), z_0.clone(), z_i.clone()) + .unwrap()]; + + let n_steps: usize = 4; + let mut iFr = Fr::zero(); + for i in 0..n_steps { + let start = Instant::now(); + let mut transcript_p: PoseidonTranscript = + PoseidonTranscript::::new(&poseidon_config.clone()); + let (nimfs_proof, U_i1, W_i1) = + NIMFS::>::prove( + &mut transcript_p, + &ccs, + &[U_i.clone()], + &[u_i.clone()], + &[W_i.clone()], + &[w_i.clone()], + ) + .unwrap(); + + // sanity check: check the folded instance relation + U_i1.check_relation(&pedersen_params, &ccs, &W_i1).unwrap(); + + let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap(); + let u_i1_x = U_i1 + .hash(&poseidon_config, iFr + Fr::one(), z_0.clone(), z_i1.clone()) + .unwrap(); + + augmented_f_circuit = + AugmentedFCircuit::> { + _c2: PhantomData, + _gc2: PhantomData, + poseidon_config: poseidon_config.clone(), + ccs: ccs.clone(), + i: Some(iFr), + i_usize: Some(i), + z_0: Some(z_0.clone()), + z_i: Some(z_i.clone()), + external_inputs: Some(vec![]), + u_i_C: Some(u_i.C), + U_i: Some(U_i.clone()), + U_i1_C: Some(U_i1.C), + F: F_circuit, + x: Some(u_i1_x), + nimfs_proof: Some(nimfs_proof), + }; + + let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap(); + assert!(cs.is_satisfied().unwrap()); + + let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::(&cs); // includes 1 and public inputs + assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap()); + let r1cs_z = [vec![Fr::one()], r1cs_x_i1, r1cs_w_i1].concat(); + // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we + // assign them directly to w_i, u_i. + (u_i, w_i) = ccs.to_cccs(&mut rng, &pedersen_params, &r1cs_z).unwrap(); + u_i.check_relation(&pedersen_params, &ccs, &w_i).unwrap(); + + // sanity check + assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap()); + let expected_u_i1_x = U_i1 + .hash(&poseidon_config, iFr + Fr::one(), z_0.clone(), z_i1.clone()) + .unwrap(); + // u_i is already u_i1 at this point, check that has the expected value at x[0] + assert_eq!(u_i.x[0], expected_u_i1_x); + + // set values for next iteration + iFr += Fr::one(); + // assign z_{i+1} into z_i + z_i = z_i1.clone(); + U_i = U_i1.clone(); + W_i = W_i1.clone(); + + // check the new LCCCS instance relation + U_i.check_relation(&pedersen_params, &ccs, &W_i).unwrap(); + // check the new CCCS instance relation + u_i.check_relation(&pedersen_params, &ccs, &w_i).unwrap(); + + println!("augmented_f_circuit step {}: {:?}", i, start.elapsed()); + } + } } diff --git a/folding-schemes/src/folding/hypernova/lcccs.rs b/folding-schemes/src/folding/hypernova/lcccs.rs index 52c0527..3616b20 100644 --- a/folding-schemes/src/folding/hypernova/lcccs.rs +++ b/folding-schemes/src/folding/hypernova/lcccs.rs @@ -1,16 +1,21 @@ -use ark_ec::CurveGroup; +use ark_crypto_primitives::{ + crh::{poseidon::CRH, CRHScheme}, + sponge::{poseidon::PoseidonConfig, Absorb}, +}; +use ark_ec::{CurveGroup, Group}; use ark_ff::PrimeField; use ark_poly::DenseMultilinearExtension; use ark_poly::MultilinearExtension; - use ark_std::rand::Rng; +use ark_std::Zero; -use super::cccs::Witness; +use super::Witness; use crate::ccs::CCS; use crate::commitment::{ pedersen::{Params as PedersenParams, Pedersen}, CommitmentScheme, }; +use crate::folding::circuits::nonnative::affine::nonnative_affine_to_field_elements; use crate::utils::mle::dense_vec_to_dense_mle; use crate::utils::vec::mat_vec_mul; use crate::Error; @@ -73,6 +78,19 @@ impl CCS { } impl LCCCS { + pub fn dummy(l: usize, t: usize, s: usize) -> LCCCS + where + C::ScalarField: PrimeField, + { + LCCCS:: { + C: C::zero(), + u: C::ScalarField::zero(), + x: vec![C::ScalarField::zero(); l], + r_x: vec![C::ScalarField::zero(); s], + v: vec![C::ScalarField::zero(); t], + } + } + /// Perform the check of the LCCCS instance described at section 4.2 pub fn check_relation( &self, @@ -104,6 +122,42 @@ impl LCCCS { } } +impl LCCCS +where + ::ScalarField: Absorb, + ::BaseField: ark_ff::PrimeField, +{ + /// hash implements the committed instance hash compatible with the gadget implemented in + /// nova/circuits.rs::CommittedInstanceVar.hash. + /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U_i` is the LCCCS. + pub fn hash( + &self, + poseidon_config: &PoseidonConfig, + i: C::ScalarField, + z_0: Vec, + z_i: Vec, + ) -> Result { + let (C_x, C_y) = nonnative_affine_to_field_elements::(self.C)?; + + CRH::::evaluate( + poseidon_config, + vec![ + vec![i], + z_0, + z_i, + C_x, + C_y, + vec![self.u], + self.x.clone(), + self.r_x.clone(), + self.v.clone(), + ] + .concat(), + ) + .map_err(|e| Error::Other(e.to_string())) + } +} + #[cfg(test)] pub mod tests { use ark_pallas::{Fr, Projective}; diff --git a/folding-schemes/src/folding/hypernova/mod.rs b/folding-schemes/src/folding/hypernova/mod.rs index 3f7172e..5a79969 100644 --- a/folding-schemes/src/folding/hypernova/mod.rs +++ b/folding-schemes/src/folding/hypernova/mod.rs @@ -1,6 +1,27 @@ /// Implements the scheme described in [HyperNova](https://eprint.iacr.org/2023/573.pdf) +use crate::ccs::CCS; +use ark_ff::PrimeField; + pub mod cccs; pub mod circuits; pub mod lcccs; pub mod nimfs; pub mod utils; + +/// Witness for the LCCCS & CCCS, containing the w vector, and the r_w used as randomness in the Pedersen commitment. +#[derive(Debug, Clone, Eq, PartialEq)] +pub struct Witness { + pub w: Vec, + pub r_w: F, +} + +impl Witness { + pub fn new(w: Vec) -> Self { + // note: at the current version, we don't use the blinding factors and we set them to 0 + // always. + Self { w, r_w: F::zero() } + } + pub fn dummy(ccs: &CCS) -> Self { + Witness::::new(vec![F::zero(); ccs.n - ccs.l - 1]) + } +} diff --git a/folding-schemes/src/folding/hypernova/nimfs.rs b/folding-schemes/src/folding/hypernova/nimfs.rs index 8aa6a49..9da471e 100644 --- a/folding-schemes/src/folding/hypernova/nimfs.rs +++ b/folding-schemes/src/folding/hypernova/nimfs.rs @@ -5,13 +5,14 @@ use ark_poly::univariate::DensePolynomial; use ark_poly::{DenseUVPolynomial, Polynomial}; use ark_std::{One, Zero}; -use super::cccs::{Witness, CCCS}; +use super::cccs::CCCS; use super::lcccs::LCCCS; use super::utils::{compute_c, compute_g, compute_sigmas_thetas}; +use super::Witness; use crate::ccs::CCS; +use crate::folding::circuits::nonnative::affine::nonnative_affine_to_field_elements; use crate::transcript::Transcript; -use crate::utils::hypercube::BooleanHypercube; -use crate::utils::sum_check::structs::IOPProof as SumCheckProof; +use crate::utils::sum_check::structs::{IOPProof as SumCheckProof, IOPProverMessage}; use crate::utils::sum_check::{IOPSumCheck, SumCheck}; use crate::utils::virtual_polynomial::VPAuxInfo; use crate::Error; @@ -19,13 +20,33 @@ use crate::Error; use std::fmt::Debug; use std::marker::PhantomData; -/// Proof defines a multifolding proof +/// NIMFSProof defines a multifolding proof #[derive(Clone, Debug)] -pub struct Proof { +pub struct NIMFSProof { pub sc_proof: SumCheckProof, pub sigmas_thetas: SigmasThetas, } +impl NIMFSProof { + pub fn dummy(ccs: &CCS, mu: usize, nu: usize) -> Self { + NIMFSProof:: { + sc_proof: SumCheckProof:: { + point: vec![C::ScalarField::zero(); ccs.d], + proofs: vec![ + IOPProverMessage { + coeffs: vec![C::ScalarField::zero(); ccs.t + 1] + }; + ccs.s + ], + }, + sigmas_thetas: SigmasThetas( + vec![vec![C::ScalarField::zero(); ccs.t]; mu], + vec![vec![C::ScalarField::zero(); ccs.t]; nu], + ), + } + } +} + #[derive(Clone, Debug)] pub struct SigmasThetas(pub Vec>, pub Vec>); @@ -40,6 +61,7 @@ pub struct NIMFS> { impl> NIMFS where ::ScalarField: Absorb, + C::BaseField: PrimeField, { pub fn fold( lcccs: &[LCCCS], @@ -157,8 +179,26 @@ where new_instances: &[CCCS], w_lcccs: &[Witness], w_cccs: &[Witness], - ) -> Result<(Proof, LCCCS, Witness), Error> { - // TODO appends to transcript + ) -> Result<(NIMFSProof, LCCCS, Witness), Error> { + // absorb instances to transcript + for U_i in running_instances { + let (C_x, C_y) = nonnative_affine_to_field_elements::(U_i.C)?; + let v = [ + C_x, + C_y, + vec![U_i.u], + U_i.x.clone(), + U_i.r_x.clone(), + U_i.v.clone(), + ] + .concat(); + transcript.absorb_vec(&v); + } + for u_i in new_instances { + let (C_x, C_y) = nonnative_affine_to_field_elements::(u_i.C)?; + let v = [C_x, C_y, u_i.x.clone()].concat(); + transcript.absorb_vec(&v); + } if running_instances.is_empty() { return Err(Error::Empty); @@ -168,7 +208,6 @@ where } // construct the LCCCS z vector from the relaxation factor, public IO and witness - // XXX this deserves its own function in LCCCS let mut z_lcccs = Vec::new(); for (i, running_instance) in running_instances.iter().enumerate() { let z_1: Vec = [ @@ -206,40 +245,6 @@ where let sumcheck_proof = IOPSumCheck::::prove(&g, transcript) .map_err(|err| Error::SumCheckProveError(err.to_string()))?; - // Note: The following two "sanity checks" are done for this prototype, in a final version - // they should be removed. - // - // Sanity check 1: evaluate g(x) over x \in {0,1} (the boolean hypercube), and check that - // its sum is equal to the extracted_sum from the SumCheck. - ////////////////////////////////////////////////////////////////////// - let mut g_over_bhc = C::ScalarField::zero(); - for x in BooleanHypercube::new(ccs.s) { - g_over_bhc += g.evaluate(&x)?; - } - - // note: this is the sum of g(x) over the whole boolean hypercube - let extracted_sum = IOPSumCheck::::extract_sum(&sumcheck_proof); - - if extracted_sum != g_over_bhc { - return Err(Error::NotEqual); - } - // Sanity check 2: expect \sum v_j * gamma^j to be equal to the sum of g(x) over the - // boolean hypercube (and also equal to the extracted_sum from the SumCheck). - let mut sum_v_j_gamma = C::ScalarField::zero(); - for (i, running_instance) in running_instances.iter().enumerate() { - for j in 0..running_instance.v.len() { - let gamma_j = gamma.pow([(i * ccs.t + j) as u64]); - sum_v_j_gamma += running_instance.v[j] * gamma_j; - } - } - if g_over_bhc != sum_v_j_gamma { - return Err(Error::NotEqual); - } - if extracted_sum != sum_v_j_gamma { - return Err(Error::NotEqual); - } - ////////////////////////////////////////////////////////////////////// - // Step 2: dig into the sumcheck and extract r_x_prime let r_x_prime = sumcheck_proof.point.clone(); @@ -264,7 +269,7 @@ where let folded_witness = Self::fold_witness(w_lcccs, w_cccs, rho); Ok(( - Proof:: { + NIMFSProof:: { sc_proof: sumcheck_proof, sigmas_thetas, }, @@ -281,9 +286,27 @@ where ccs: &CCS, running_instances: &[LCCCS], new_instances: &[CCCS], - proof: Proof, + proof: NIMFSProof, ) -> Result, Error> { - // TODO appends to transcript + // absorb instances to transcript + for U_i in running_instances { + let (C_x, C_y) = nonnative_affine_to_field_elements::(U_i.C)?; + let v = [ + C_x, + C_y, + vec![U_i.u], + U_i.x.clone(), + U_i.r_x.clone(), + U_i.v.clone(), + ] + .concat(); + transcript.absorb_vec(&v); + } + for u_i in new_instances { + let (C_x, C_y) = nonnative_affine_to_field_elements::(u_i.C)?; + let v = [C_x, C_y, u_i.x.clone()].concat(); + transcript.absorb_vec(&v); + } if running_instances.is_empty() { return Err(Error::Empty); @@ -514,11 +537,8 @@ pub mod tests { let n: usize = 10; for i in 3..n { - println!("\niteration: i {}", i); // DBG - // CCS witness let z_2 = get_test_z(i); - println!("z_2 {:?}", z_2); // DBG let (new_instance, w2) = ccs.to_cccs(&mut rng, &pedersen_params, &z_2).unwrap(); @@ -546,7 +566,6 @@ pub mod tests { assert_eq!(folded_lcccs, folded_lcccs_v); // check that the folded instance with the folded witness holds the LCCCS relation - println!("check_relation {}", i); folded_lcccs .check_relation(&pedersen_params, &ccs, &folded_witness) .unwrap();