diff --git a/src/decider/circuit.rs b/src/decider/circuit.rs deleted file mode 100644 index b008560..0000000 --- a/src/decider/circuit.rs +++ /dev/null @@ -1,391 +0,0 @@ -use ark_ec::CurveGroup; -use ark_ff::{Field, PrimeField}; -use ark_r1cs_std::{ - alloc::{AllocVar, AllocationMode}, - fields::FieldVar, -}; -use ark_relations::r1cs::{Namespace, SynthesisError}; -use core::{borrow::Borrow, marker::PhantomData}; - -use crate::ccs::r1cs::RelaxedR1CS; -use crate::utils::vec::SparseMatrix; -use crate::Error; - -pub type ConstraintF = <::BaseField as Field>::BasePrimeField; - -#[derive(Debug, Clone)] -pub struct RelaxedR1CSGadget> { - _f: PhantomData, - _cf: PhantomData, - _fv: PhantomData, -} -impl> RelaxedR1CSGadget { - /// performs the RelaxedR1CS check (Az∘Bz==uCz+E) - pub fn check(rel_r1cs: RelaxedR1CSVar, z: Vec) -> Result<(), Error> { - let Az = mat_vec_mul_sparse(rel_r1cs.A, z.clone()); - let Bz = mat_vec_mul_sparse(rel_r1cs.B, z.clone()); - let Cz = mat_vec_mul_sparse(rel_r1cs.C, z.clone()); - let uCz = vec_scalar_mul(&Cz, &rel_r1cs.u); - let uCzE = vec_add(&uCz, &rel_r1cs.E)?; - let AzBz = hadamard(&Az, &Bz)?; - for i in 0..AzBz.len() { - AzBz[i].enforce_equal(&uCzE[i].clone())?; - } - Ok(()) - } -} - -fn mat_vec_mul_sparse>( - m: SparseMatrixVar, - v: Vec, -) -> Vec { - let mut res = vec![FV::zero(); m.n_rows]; - for (row_i, row) in m.coeffs.iter().enumerate() { - for (value, col_i) in row.iter() { - res[row_i] += value.clone().mul(&v[*col_i].clone()); - } - } - res -} -pub fn vec_add>( - a: &Vec, - b: &Vec, -) -> Result, Error> { - if a.len() != b.len() { - return Err(Error::NotSameLength( - "a.len()".to_string(), - a.len(), - "b.len()".to_string(), - b.len(), - )); - } - let mut r: Vec = vec![FV::zero(); a.len()]; - for i in 0..a.len() { - r[i] = a[i].clone() + b[i].clone(); - } - Ok(r) -} -pub fn vec_scalar_mul>( - vec: &Vec, - c: &FV, -) -> Vec { - let mut result = vec![FV::zero(); vec.len()]; - for (i, a) in vec.iter().enumerate() { - result[i] = a.clone() * c; - } - result -} -pub fn hadamard>( - a: &Vec, - b: &Vec, -) -> Result, Error> { - if a.len() != b.len() { - return Err(Error::NotSameLength( - "a.len()".to_string(), - a.len(), - "b.len()".to_string(), - b.len(), - )); - } - let mut r: Vec = vec![FV::zero(); a.len()]; - for i in 0..a.len() { - r[i] = a[i].clone() * b[i].clone(); - } - Ok(r) -} - -#[derive(Debug, Clone)] -pub struct SparseMatrixVar> { - _f: PhantomData, - _cf: PhantomData, - _fv: PhantomData, - pub n_rows: usize, - pub n_cols: usize, - // same format as the native SparseMatrix (which follows ark_relations::r1cs::Matrix format - pub coeffs: Vec>, -} - -impl AllocVar, CF> for SparseMatrixVar -where - F: PrimeField, - CF: PrimeField, - FV: FieldVar, -{ - fn new_variable>>( - cs: impl Into>, - f: impl FnOnce() -> Result, - mode: AllocationMode, - ) -> Result { - f().and_then(|val| { - let cs = cs.into(); - - let mut coeffs: Vec> = Vec::new(); - for row in val.borrow().coeffs.iter() { - let mut rowVar: Vec<(FV, usize)> = Vec::new(); - for &(value, col_i) in row.iter() { - let coeffVar = FV::new_variable(cs.clone(), || Ok(value), mode)?; - rowVar.push((coeffVar, col_i)); - } - coeffs.push(rowVar); - } - - Ok(Self { - _f: PhantomData, - _cf: PhantomData, - _fv: PhantomData, - n_rows: val.borrow().n_rows, - n_cols: val.borrow().n_cols, - coeffs, - }) - }) - } -} - -#[derive(Debug, Clone)] -pub struct RelaxedR1CSVar> { - _f: PhantomData, - _cf: PhantomData, - _fv: PhantomData, - pub A: SparseMatrixVar, - pub B: SparseMatrixVar, - pub C: SparseMatrixVar, - pub u: FV, - pub E: Vec, -} - -impl AllocVar, CF> for RelaxedR1CSVar -where - F: PrimeField, - CF: PrimeField, - FV: FieldVar, -{ - fn new_variable>>( - cs: impl Into>, - f: impl FnOnce() -> Result, - mode: AllocationMode, - ) -> Result { - f().and_then(|val| { - let cs = cs.into(); - - let A = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().A)?; - let B = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().B)?; - let C = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().C)?; - let E = Vec::::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?; - let u = FV::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?; - - Ok(Self { - _f: PhantomData, - _cf: PhantomData, - _fv: PhantomData, - A, - B, - C, - E, - u, - }) - }) - } -} - -#[cfg(test)] -mod tests { - use super::*; - use ark_crypto_primitives::crh::{ - sha256::{ - constraints::{Sha256Gadget, UnitVar}, - Sha256, - }, - CRHScheme, CRHSchemeGadget, - }; - use ark_ff::BigInteger; - use ark_pallas::{Fq, Fr}; - use ark_r1cs_std::{ - alloc::AllocVar, - bits::uint8::UInt8, - eq::EqGadget, - fields::{fp::FpVar, nonnative::NonNativeFieldVar}, - }; - use ark_relations::r1cs::{ - ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError, - }; - use ark_std::One; - - use crate::ccs::r1cs::{ - tests::{get_test_r1cs, get_test_z}, - R1CS, - }; - use crate::frontend::arkworks::{extract_r1cs_and_z, tests::TestCircuit}; - - #[test] - fn test_relaxed_r1cs_small_gadget_handcrafted() { - let r1cs: R1CS = get_test_r1cs(); - let rel_r1cs = r1cs.relax(); - let z = get_test_z(3); - - let cs = ConstraintSystem::::new_ref(); - - let zVar = Vec::>::new_witness(cs.clone(), || Ok(z)).unwrap(); - let rel_r1csVar = - RelaxedR1CSVar::>::new_witness(cs.clone(), || Ok(rel_r1cs)).unwrap(); - - RelaxedR1CSGadget::>::check(rel_r1csVar, zVar).unwrap(); - assert!(cs.is_satisfied().unwrap()); - } - - // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been - // initialized. - fn test_relaxed_r1cs_gadget>(circuit: CS) { - let cs = ConstraintSystem::::new_ref(); - - circuit.generate_constraints(cs.clone()).unwrap(); - cs.finalize(); - assert!(cs.is_satisfied().unwrap()); - - let cs = cs.into_inner().unwrap(); - - let (r1cs, z) = extract_r1cs_and_z::(&cs); - r1cs.check_relation(&z).unwrap(); - - let relaxed_r1cs = r1cs.relax(); - relaxed_r1cs.check_relation(&z).unwrap(); - - // set new CS for the circuit that checks the RelaxedR1CS of our original circuit - let cs = ConstraintSystem::::new_ref(); - // prepare the inputs for our circuit - let zVar = Vec::>::new_witness(cs.clone(), || Ok(z)).unwrap(); - let rel_r1csVar = - RelaxedR1CSVar::>::new_witness(cs.clone(), || Ok(relaxed_r1cs)) - .unwrap(); - - RelaxedR1CSGadget::>::check(rel_r1csVar, zVar).unwrap(); - assert!(cs.is_satisfied().unwrap()); - } - - #[test] - fn test_relaxed_r1cs_small_gadget_arkworks() { - let x = Fr::from(5_u32); - let y = x * x * x + x + Fr::from(5_u32); - let circuit = TestCircuit:: { x, y }; - test_relaxed_r1cs_gadget(circuit); - } - - struct Sha256TestCircuit { - _f: PhantomData, - pub x: Vec, - pub y: Vec, - } - impl ConstraintSynthesizer for Sha256TestCircuit { - fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { - let x = Vec::>::new_witness(cs.clone(), || Ok(self.x))?; - let y = Vec::>::new_input(cs.clone(), || Ok(self.y))?; - - let unitVar = UnitVar::default(); - let comp_y = as CRHSchemeGadget>::evaluate(&unitVar, &x)?; - comp_y.0.enforce_equal(&y)?; - Ok(()) - } - } - #[test] - fn test_relaxed_r1cs_medium_gadget_arkworks() { - let x = Fr::from(5_u32).into_bigint().to_bytes_le(); - let y = ::evaluate(&(), x.clone()).unwrap(); - - let circuit = Sha256TestCircuit:: { - _f: PhantomData, - x, - y, - }; - test_relaxed_r1cs_gadget(circuit); - } - - // circuit that has the number of constraints specified in the `n_constraints` parameter. Note - // that the generated circuit will have very sparse matrices, so the resulting constraints - // number of the RelaxedR1CS gadget must take that into account. - struct CustomTestCircuit { - _f: PhantomData, - pub n_constraints: usize, - pub x: F, - pub y: F, - } - impl CustomTestCircuit { - fn new(n_constraints: usize) -> Self { - let x = F::from(5_u32); - let mut y = F::one(); - for _ in 0..n_constraints - 1 { - y *= x; - } - Self { - _f: PhantomData, - n_constraints, - x, - y, - } - } - } - impl ConstraintSynthesizer for CustomTestCircuit { - fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { - let x = FpVar::::new_witness(cs.clone(), || Ok(self.x))?; - let y = FpVar::::new_input(cs.clone(), || Ok(self.y))?; - - let mut comp_y = FpVar::::new_witness(cs.clone(), || Ok(F::one()))?; - for _ in 0..self.n_constraints - 1 { - comp_y *= x.clone(); - } - - comp_y.enforce_equal(&y)?; - Ok(()) - } - } - - #[test] - fn test_relaxed_r1cs_custom_circuit() { - let n_constraints = 10_000; - let x = Fr::from(5_u32); - let mut y = Fr::one(); - for _ in 0..n_constraints - 1 { - y *= x; - } - - let circuit = CustomTestCircuit:: { - _f: PhantomData, - n_constraints, - x, - y, - }; - test_relaxed_r1cs_gadget(circuit); - } - - #[test] - fn test_relaxed_r1cs_nonnative_circuit() { - let cs = ConstraintSystem::::new_ref(); - // in practice we would use CycleFoldCircuit, but is a very big circuit (when computed - // non-natively inside the RelaxedR1CS circuit), so in order to have a short test we use a - // custom circuit. - let circuit = CustomTestCircuit::::new(10); - circuit.generate_constraints(cs.clone()).unwrap(); - cs.finalize(); - let cs = cs.into_inner().unwrap(); - let (r1cs, z) = extract_r1cs_and_z::(&cs); - - let relaxed_r1cs = r1cs.relax(); - - // natively - let cs = ConstraintSystem::::new_ref(); - let zVar = Vec::>::new_witness(cs.clone(), || Ok(z.clone())).unwrap(); - let rel_r1csVar = RelaxedR1CSVar::>::new_witness(cs.clone(), || { - Ok(relaxed_r1cs.clone()) - }) - .unwrap(); - RelaxedR1CSGadget::>::check(rel_r1csVar, zVar).unwrap(); - - // non-natively - let cs = ConstraintSystem::::new_ref(); - let zVar = Vec::>::new_witness(cs.clone(), || Ok(z)).unwrap(); - let rel_r1csVar = - RelaxedR1CSVar::>::new_witness(cs.clone(), || { - Ok(relaxed_r1cs) - }) - .unwrap(); - RelaxedR1CSGadget::>::check(rel_r1csVar, zVar).unwrap(); - } -} diff --git a/src/decider/mod.rs b/src/decider/mod.rs deleted file mode 100644 index db89e61..0000000 --- a/src/decider/mod.rs +++ /dev/null @@ -1 +0,0 @@ -pub mod circuit; diff --git a/src/folding/nova/circuits.rs b/src/folding/nova/circuits.rs index a15e7f3..afa7cc5 100644 --- a/src/folding/nova/circuits.rs +++ b/src/folding/nova/circuits.rs @@ -46,10 +46,10 @@ pub type CF2 = <::BaseField as Field>::BasePrimeField; /// represented non-natively over the constraint field. #[derive(Debug, Clone)] pub struct CommittedInstanceVar { - u: FpVar, - x: Vec>, - cmE: NonNativeAffineVar, - cmW: NonNativeAffineVar, + pub u: FpVar, + pub x: Vec>, + pub cmE: NonNativeAffineVar, + pub cmW: NonNativeAffineVar, } impl AllocVar, CF1> for CommittedInstanceVar @@ -94,7 +94,7 @@ where /// CommittedInstance.hash. /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the /// `CommittedInstance`. - fn hash( + pub fn hash( self, crh_params: &CRHParametersVar>, i: FpVar>, diff --git a/src/folding/nova/decider.rs b/src/folding/nova/decider.rs new file mode 100644 index 0000000..adafc01 --- /dev/null +++ b/src/folding/nova/decider.rs @@ -0,0 +1,656 @@ +/// This file implements the onchain (Ethereum's EVM) decider circuit. For non-ethereum use cases, +/// other more efficient approaches can be used. +use ark_crypto_primitives::crh::poseidon::constraints::CRHParametersVar; +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, nonnative::NonNativeFieldVar, FieldVar}, + groups::GroupOpsBounds, + prelude::CurveVar, + ToConstraintFieldGadget, +}; +use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError}; +use ark_std::{One, Zero}; +use core::{borrow::Borrow, marker::PhantomData}; + +use crate::ccs::r1cs::R1CS; +use crate::folding::nova::{ + circuits::{CommittedInstanceVar, FCircuit, CF1, CF2}, + ivc::IVC, + CommittedInstance, Witness, +}; +use crate::pedersen::Params as PedersenParams; +use crate::utils::gadgets::{ + hadamard, mat_vec_mul_sparse, vec_add, vec_scalar_mul, SparseMatrixVar, +}; + +#[derive(Debug, Clone)] +pub struct RelaxedR1CSGadget> { + _f: PhantomData, + _cf: PhantomData, + _fv: PhantomData, +} +impl> RelaxedR1CSGadget { + /// performs the RelaxedR1CS check (Az∘Bz==uCz+E) + pub fn check( + r1cs: R1CSVar, + E: Vec, + u: FV, + z: Vec, + ) -> Result<(), SynthesisError> { + let Az = mat_vec_mul_sparse(r1cs.A, z.clone()); + let Bz = mat_vec_mul_sparse(r1cs.B, z.clone()); + let Cz = mat_vec_mul_sparse(r1cs.C, z.clone()); + let uCz = vec_scalar_mul(&Cz, &u); + let uCzE = vec_add(&uCz, &E)?; + let AzBz = hadamard(&Az, &Bz)?; + for i in 0..AzBz.len() { + AzBz[i].enforce_equal(&uCzE[i].clone())?; + } + Ok(()) + } +} + +#[derive(Debug, Clone)] +pub struct R1CSVar> { + _f: PhantomData, + _cf: PhantomData, + _fv: PhantomData, + pub A: SparseMatrixVar, + pub B: SparseMatrixVar, + pub C: SparseMatrixVar, +} + +impl AllocVar, CF> for R1CSVar +where + F: PrimeField, + CF: PrimeField, + FV: FieldVar, +{ + fn new_variable>>( + cs: impl Into>, + f: impl FnOnce() -> Result, + _mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let A = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().A)?; + let B = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().B)?; + let C = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().C)?; + + Ok(Self { + _f: PhantomData, + _cf: PhantomData, + _fv: PhantomData, + A, + B, + C, + }) + }) + } +} + +/// In-circuit representation of the Witness associated to the CommittedInstance. +#[derive(Debug, Clone)] +pub struct WitnessVar { + pub E: Vec>, + pub rE: FpVar, + pub W: Vec>, + pub rW: FpVar, +} + +impl AllocVar, CF1> for WitnessVar +where + C: CurveGroup, + ::BaseField: PrimeField, +{ + fn new_variable>>( + cs: impl Into>>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let E: Vec> = + Vec::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?; + let rE = + FpVar::::new_variable(cs.clone(), || Ok(val.borrow().rE), mode)?; + + let W: Vec> = + Vec::new_variable(cs.clone(), || Ok(val.borrow().W.clone()), mode)?; + let rW = + FpVar::::new_variable(cs.clone(), || Ok(val.borrow().rW), mode)?; + + Ok(Self { E, rE, W, rW }) + }) + } +} + +/// In-circuit representation of the Witness associated to the CommittedInstance, but with +/// non-native representation, since it is used to represent the CycleFold witness. +#[derive(Debug, Clone)] +pub struct CycleFoldWitnessVar { + pub E: Vec>>, + pub rE: NonNativeFieldVar>, + pub W: Vec>>, + pub rW: NonNativeFieldVar>, +} + +impl AllocVar, CF2> for CycleFoldWitnessVar +where + C: CurveGroup, + ::BaseField: PrimeField, +{ + fn new_variable>>( + cs: impl Into>>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let E: Vec>> = + Vec::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?; + let rE = NonNativeFieldVar::>::new_variable( + cs.clone(), + || Ok(val.borrow().rE), + mode, + )?; + + let W: Vec>> = + Vec::new_variable(cs.clone(), || Ok(val.borrow().W.clone()), mode)?; + let rW = NonNativeFieldVar::>::new_variable( + cs.clone(), + || Ok(val.borrow().rW), + mode, + )?; + + Ok(Self { E, rE, W, rW }) + }) + } +} + +/// Circuit that implements the in-circuit checks needed for the onchain (Ethereum's EVM) +/// verification. +pub struct DeciderCircuit +where + C1: CurveGroup, + GC1: CurveVar>, + C2: CurveGroup, + GC2: CurveVar>, +{ + _c1: PhantomData, + _gc1: PhantomData, + _c2: PhantomData, + _gc2: PhantomData, + + /// E vector's length of the Nova instance witness + pub E_len: usize, + /// E vector's length of the CycleFold instance witness + pub cf_E_len: usize, + /// R1CS of the Augmented Function circuit + pub r1cs: R1CS, + /// R1CS of the CycleFold circuit + pub cf_r1cs: R1CS, + /// CycleFold PedersenParams, over C2 + pub cf_pedersen_params: PedersenParams, + pub poseidon_config: PoseidonConfig>, + pub i: Option>, + /// initial state + pub z_0: Option>, + /// current i-th state + pub z_i: Option>, + /// Nova instances + pub u_i: Option>, + pub w_i: Option>, + pub U_i: Option>, + pub W_i: Option>, + /// CycleFold running instance + pub cf_U_i: Option>, + pub cf_W_i: Option>, +} +impl DeciderCircuit +where + C1: CurveGroup, + C2: CurveGroup, + GC1: CurveVar>, + GC2: CurveVar>, +{ + pub fn from_ivc>(ivc: IVC) -> Self { + Self { + _c1: PhantomData, + _gc1: PhantomData, + _c2: PhantomData, + _gc2: PhantomData, + + E_len: ivc.W_i.E.len(), + cf_E_len: ivc.cf_W_i.E.len(), + r1cs: ivc.r1cs, + cf_r1cs: ivc.cf_r1cs, + cf_pedersen_params: ivc.cf_pedersen_params, + poseidon_config: ivc.poseidon_config, + i: Some(ivc.i), + z_0: Some(ivc.z_0), + z_i: Some(ivc.z_i), + u_i: Some(ivc.u_i), + w_i: Some(ivc.w_i), + U_i: Some(ivc.U_i), + W_i: Some(ivc.W_i), + cf_U_i: Some(ivc.cf_U_i), + cf_W_i: Some(ivc.cf_W_i), + } + } +} + +impl ConstraintSynthesizer> for DeciderCircuit +where + C1: CurveGroup, + C2: CurveGroup, + GC1: CurveVar>, + GC2: CurveVar>, + ::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 r1cs = + R1CSVar::, FpVar>>::new_witness(cs.clone(), || { + Ok(self.r1cs.clone()) + })?; + + 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()])) + })?; + let z_i = Vec::>>::new_witness(cs.clone(), || { + Ok(self.z_i.unwrap_or(vec![CF1::::zero()])) + })?; + + let u_dummy_native = CommittedInstance::::dummy(1); + let w_dummy_native = Witness::::new( + vec![C1::ScalarField::zero(); self.r1cs.A.n_cols - 2 /* (2=1+1, since u_i.x.len=1) */], + self.E_len, + ); + + let u_i = CommittedInstanceVar::::new_witness(cs.clone(), || { + Ok(self.u_i.unwrap_or(u_dummy_native.clone())) + })?; + let w_i = WitnessVar::::new_witness(cs.clone(), || { + Ok(self.w_i.unwrap_or(w_dummy_native.clone())) + })?; + let U_i = CommittedInstanceVar::::new_witness(cs.clone(), || { + Ok(self.U_i.unwrap_or(u_dummy_native.clone())) + })?; + let W_i = WitnessVar::::new_witness(cs.clone(), || { + Ok(self.W_i.unwrap_or(w_dummy_native.clone())) + })?; + + let crh_params = CRHParametersVar::::new_constant( + cs.clone(), + self.poseidon_config.clone(), + )?; + + // 1. check RelaxedR1CS of u_i + let z_u: Vec>> = [ + vec![FpVar::>::one()], + u_i.x.to_vec(), + w_i.W.to_vec(), + ] + .concat(); + RelaxedR1CSGadget::, FpVar>>::check( + r1cs.clone(), + w_i.E, + u_i.u.clone(), + z_u, + )?; + + // 2. check RelaxedR1CS of U_i + let z_U: Vec>> = + [vec![U_i.u.clone()], U_i.x.to_vec(), W_i.W.to_vec()].concat(); + RelaxedR1CSGadget::, FpVar>>::check( + r1cs, + W_i.E, + U_i.u.clone(), + z_U, + )?; + + // 3. u_i.cmE==cm(0), u_i.u==1 + // Here zero_x & zero_y are the x & y coordinates of the zero point affine representation. + let zero_x = NonNativeFieldVar::::new_constant( + cs.clone(), + C1::BaseField::zero(), + )? + .to_constraint_field()?; + let zero_y = NonNativeFieldVar::::new_constant( + cs.clone(), + C1::BaseField::one(), + )? + .to_constraint_field()?; + (u_i.cmE.x.is_eq(&zero_x)?).enforce_equal(&Boolean::TRUE)?; + (u_i.cmE.y.is_eq(&zero_y)?).enforce_equal(&Boolean::TRUE)?; + (u_i.u.is_one()?).enforce_equal(&Boolean::TRUE)?; + + // 4. u_i.x == 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())?; + (u_i.x[0]).enforce_equal(&u_i_x)?; + + // The following two checks (and their respective allocations) are disabled for normal + // tests since they take ~24.5M constraints and would take several minutes (and RAM) to run + // the test + #[cfg(not(test))] + { + // imports here instead of at the top of the file, so we avoid having multiple + // `#[cfg(not(test))] + use crate::folding::nova::cyclefold::{CycleFoldCommittedInstanceVar, CF_IO_LEN}; + use crate::pedersen::PedersenGadget; + use ark_r1cs_std::ToBitsGadget; + + let cf_r1cs = R1CSVar::< + C1::BaseField, + CF1, + NonNativeFieldVar>, + >::new_witness(cs.clone(), || Ok(self.cf_r1cs.clone()))?; + + let cf_u_dummy_native = CommittedInstance::::dummy(CF_IO_LEN); + let w_dummy_native = Witness::::new( + vec![C2::ScalarField::zero(); self.cf_r1cs.A.n_cols - 1 - self.cf_r1cs.l], + self.cf_E_len, + ); + let cf_U_i = CycleFoldCommittedInstanceVar::::new_witness(cs.clone(), || { + Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone())) + })?; + let cf_W_i = CycleFoldWitnessVar::::new_witness(cs.clone(), || { + Ok(self.cf_W_i.unwrap_or(w_dummy_native.clone())) + })?; + + // 5. check Pedersen commitments of cf_U_i.{cmE, cmW} + let H = GC2::new_constant(cs.clone(), self.cf_pedersen_params.h)?; + let G = Vec::::new_constant(cs.clone(), self.cf_pedersen_params.generators)?; + let cf_W_i_E_bits: Vec>>> = cf_W_i + .E + .iter() + .map(|E_i| E_i.to_bits_le().unwrap()) + .collect(); + let cf_W_i_W_bits: Vec>>> = cf_W_i + .W + .iter() + .map(|W_i| W_i.to_bits_le().unwrap()) + .collect(); + + let computed_cmE = PedersenGadget::::commit( + H.clone(), + G.clone(), + cf_W_i_E_bits, + cf_W_i.rE.to_bits_le()?, + )?; + cf_U_i.cmE.enforce_equal(&computed_cmE)?; + let computed_cmW = + PedersenGadget::::commit(H, G, cf_W_i_W_bits, cf_W_i.rW.to_bits_le()?)?; + cf_U_i.cmW.enforce_equal(&computed_cmW)?; + + // 6. check RelaxedR1CS of cf_U_i + let cf_z_U: Vec>> = + [vec![cf_U_i.u.clone()], cf_U_i.x.to_vec(), cf_W_i.W.to_vec()].concat(); + RelaxedR1CSGadget::< + C2::ScalarField, + CF1, + NonNativeFieldVar>, + >::check(cf_r1cs, cf_W_i.E, cf_U_i.u.clone(), cf_z_U)?; + } + + Ok(()) + } +} + +#[cfg(test)] +pub mod tests { + use super::*; + use ark_crypto_primitives::crh::{ + sha256::{ + constraints::{Sha256Gadget, UnitVar}, + Sha256, + }, + CRHScheme, CRHSchemeGadget, + }; + use ark_ff::BigInteger; + use ark_pallas::{constraints::GVar, Fq, Fr, Projective}; + use ark_r1cs_std::{ + alloc::AllocVar, + bits::uint8::UInt8, + eq::EqGadget, + fields::{fp::FpVar, nonnative::NonNativeFieldVar}, + }; + use ark_relations::r1cs::ConstraintSystem; + use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2}; + + use crate::folding::nova::circuits::{tests::TestFCircuit, FCircuit}; + use crate::folding::nova::ivc::IVC; + use crate::transcript::poseidon::tests::poseidon_test_config; + + use crate::ccs::r1cs::{ + tests::{get_test_r1cs, get_test_z}, + R1CS, + }; + use crate::frontend::arkworks::{extract_r1cs_and_z, tests::TestCircuit}; + + #[test] + fn test_relaxed_r1cs_small_gadget_handcrafted() { + let r1cs: R1CS = get_test_r1cs(); + let rel_r1cs = r1cs.clone().relax(); + let z = get_test_z(3); + + let cs = ConstraintSystem::::new_ref(); + + let zVar = Vec::>::new_witness(cs.clone(), || Ok(z)).unwrap(); + let EVar = Vec::>::new_witness(cs.clone(), || Ok(rel_r1cs.E)).unwrap(); + let uVar = FpVar::::new_witness(cs.clone(), || Ok(rel_r1cs.u)).unwrap(); + let r1csVar = R1CSVar::>::new_witness(cs.clone(), || Ok(r1cs)).unwrap(); + + RelaxedR1CSGadget::>::check(r1csVar, EVar, uVar, zVar).unwrap(); + assert!(cs.is_satisfied().unwrap()); + } + + // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been + // initialized. + fn test_relaxed_r1cs_gadget>(circuit: CS) { + let cs = ConstraintSystem::::new_ref(); + + circuit.generate_constraints(cs.clone()).unwrap(); + cs.finalize(); + assert!(cs.is_satisfied().unwrap()); + + let cs = cs.into_inner().unwrap(); + + let (r1cs, z) = extract_r1cs_and_z::(&cs); + r1cs.check_relation(&z).unwrap(); + + let relaxed_r1cs = r1cs.clone().relax(); + relaxed_r1cs.check_relation(&z).unwrap(); + + // set new CS for the circuit that checks the RelaxedR1CS of our original circuit + let cs = ConstraintSystem::::new_ref(); + // prepare the inputs for our circuit + let zVar = Vec::>::new_witness(cs.clone(), || Ok(z)).unwrap(); + let EVar = Vec::>::new_witness(cs.clone(), || Ok(relaxed_r1cs.E)).unwrap(); + let uVar = FpVar::::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap(); + let r1csVar = R1CSVar::>::new_witness(cs.clone(), || Ok(r1cs)).unwrap(); + + RelaxedR1CSGadget::>::check(r1csVar, EVar, uVar, zVar).unwrap(); + assert!(cs.is_satisfied().unwrap()); + } + + #[test] + fn test_relaxed_r1cs_small_gadget_arkworks() { + let x = Fr::from(5_u32); + let y = x * x * x + x + Fr::from(5_u32); + let circuit = TestCircuit:: { x, y }; + test_relaxed_r1cs_gadget(circuit); + } + + struct Sha256TestCircuit { + _f: PhantomData, + pub x: Vec, + pub y: Vec, + } + impl ConstraintSynthesizer for Sha256TestCircuit { + fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { + let x = Vec::>::new_witness(cs.clone(), || Ok(self.x))?; + let y = Vec::>::new_input(cs.clone(), || Ok(self.y))?; + + let unitVar = UnitVar::default(); + let comp_y = as CRHSchemeGadget>::evaluate(&unitVar, &x)?; + comp_y.0.enforce_equal(&y)?; + Ok(()) + } + } + #[test] + fn test_relaxed_r1cs_medium_gadget_arkworks() { + let x = Fr::from(5_u32).into_bigint().to_bytes_le(); + let y = ::evaluate(&(), x.clone()).unwrap(); + + let circuit = Sha256TestCircuit:: { + _f: PhantomData, + x, + y, + }; + test_relaxed_r1cs_gadget(circuit); + } + + // circuit that has the number of constraints specified in the `n_constraints` parameter. Note + // that the generated circuit will have very sparse matrices, so the resulting constraints + // number of the RelaxedR1CS gadget must take that into account. + struct CustomTestCircuit { + _f: PhantomData, + pub n_constraints: usize, + pub x: F, + pub y: F, + } + impl CustomTestCircuit { + fn new(n_constraints: usize) -> Self { + let x = F::from(5_u32); + let mut y = F::one(); + for _ in 0..n_constraints - 1 { + y *= x; + } + Self { + _f: PhantomData, + n_constraints, + x, + y, + } + } + } + impl ConstraintSynthesizer for CustomTestCircuit { + fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { + let x = FpVar::::new_witness(cs.clone(), || Ok(self.x))?; + let y = FpVar::::new_input(cs.clone(), || Ok(self.y))?; + + let mut comp_y = FpVar::::new_witness(cs.clone(), || Ok(F::one()))?; + for _ in 0..self.n_constraints - 1 { + comp_y *= x.clone(); + } + + comp_y.enforce_equal(&y)?; + Ok(()) + } + } + + #[test] + fn test_relaxed_r1cs_custom_circuit() { + let n_constraints = 10_000; + let x = Fr::from(5_u32); + let mut y = Fr::one(); + for _ in 0..n_constraints - 1 { + y *= x; + } + + let circuit = CustomTestCircuit:: { + _f: PhantomData, + n_constraints, + x, + y, + }; + test_relaxed_r1cs_gadget(circuit); + } + + #[test] + fn test_relaxed_r1cs_nonnative_circuit() { + let cs = ConstraintSystem::::new_ref(); + // in practice we would use CycleFoldCircuit, but is a very big circuit (when computed + // non-natively inside the RelaxedR1CS circuit), so in order to have a short test we use a + // custom circuit. + let circuit = CustomTestCircuit::::new(10); + circuit.generate_constraints(cs.clone()).unwrap(); + cs.finalize(); + let cs = cs.into_inner().unwrap(); + let (r1cs, z) = extract_r1cs_and_z::(&cs); + + let relaxed_r1cs = r1cs.clone().relax(); + + // natively + let cs = ConstraintSystem::::new_ref(); + let zVar = Vec::>::new_witness(cs.clone(), || Ok(z.clone())).unwrap(); + let EVar = + Vec::>::new_witness(cs.clone(), || Ok(relaxed_r1cs.clone().E)).unwrap(); + let uVar = FpVar::::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap(); + let r1csVar = + R1CSVar::>::new_witness(cs.clone(), || Ok(r1cs.clone())).unwrap(); + RelaxedR1CSGadget::>::check(r1csVar, EVar, uVar, zVar).unwrap(); + + // non-natively + let cs = ConstraintSystem::::new_ref(); + let zVar = Vec::>::new_witness(cs.clone(), || Ok(z)).unwrap(); + let EVar = Vec::>::new_witness(cs.clone(), || Ok(relaxed_r1cs.E)) + .unwrap(); + let uVar = + NonNativeFieldVar::::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap(); + let r1csVar = + R1CSVar::>::new_witness(cs.clone(), || Ok(r1cs)) + .unwrap(); + RelaxedR1CSGadget::>::check(r1csVar, EVar, uVar, zVar) + .unwrap(); + } + + #[test] + fn test_decider_circuit() { + let mut rng = ark_std::test_rng(); + let poseidon_config = poseidon_test_config::(); + + let F_circuit = TestFCircuit::::new(); + let z_0 = vec![Fr::from(3_u32)]; + + // generate an IVC and do a step of it + let mut ivc = IVC::>::new( + &mut rng, + poseidon_config, + F_circuit, + z_0.clone(), + ) + .unwrap(); + ivc.prove_step().unwrap(); + ivc.verify(z_0, 1).unwrap(); + + // load the DeciderCircuit from the generated IVC + let decider_circuit = DeciderCircuit::::from_ivc(ivc); + + let cs = ConstraintSystem::::new_ref(); + + // generate the constraints and check that are satisfied by the inputs + decider_circuit.generate_constraints(cs.clone()).unwrap(); + assert!(cs.is_satisfied().unwrap()); + dbg!(cs.num_constraints()); + } +} diff --git a/src/folding/nova/ivc.rs b/src/folding/nova/ivc.rs index 20cbb3c..2c4f156 100644 --- a/src/folding/nova/ivc.rs +++ b/src/folding/nova/ivc.rs @@ -33,23 +33,31 @@ where _gc1: PhantomData, _c2: PhantomData, _gc2: PhantomData, - r1cs: R1CS, - cf_r1cs: R1CS, // Notice that this is a different set of R1CS constraints than the 'r1cs'. This is the R1CS of the CycleFoldCircuit - poseidon_config: PoseidonConfig, - pedersen_params: PedersenParams, // PedersenParams over C1 - cf_pedersen_params: PedersenParams, // CycleFold PedersenParams, over C2 - F: FC, // F circuit - i: C1::ScalarField, - z_0: Vec, - z_i: Vec, - w_i: Witness, - u_i: CommittedInstance, - W_i: Witness, - U_i: CommittedInstance, - - // cyclefold running instance - cf_W_i: Witness, - cf_U_i: CommittedInstance, + /// R1CS of the Augmented Function circuit + pub r1cs: R1CS, + /// R1CS of the CycleFold circuit + pub cf_r1cs: R1CS, + pub poseidon_config: PoseidonConfig, + /// PedersenParams over C1 + pub pedersen_params: PedersenParams, + /// CycleFold PedersenParams, over C2 + pub cf_pedersen_params: PedersenParams, + /// F circuit, the circuit that is being folded + pub F: FC, + pub i: C1::ScalarField, + /// initial state + pub z_0: Vec, + /// current i-th state + pub z_i: Vec, + /// Nova instances + pub w_i: Witness, + pub u_i: CommittedInstance, + pub W_i: Witness, + pub U_i: CommittedInstance, + + /// CycleFold running instance + pub cf_W_i: Witness, + pub cf_U_i: CommittedInstance, } impl IVC diff --git a/src/folding/nova/mod.rs b/src/folding/nova/mod.rs index 04d216e..a6e3eb6 100644 --- a/src/folding/nova/mod.rs +++ b/src/folding/nova/mod.rs @@ -14,6 +14,7 @@ use crate::Error; pub mod circuits; pub mod cyclefold; +pub mod decider; pub mod ivc; pub mod nifs; pub mod traits; diff --git a/src/lib.rs b/src/lib.rs index ffc19c8..873cdb3 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -10,7 +10,6 @@ pub mod transcript; use transcript::Transcript; pub mod ccs; pub mod constants; -pub mod decider; pub mod folding; pub mod frontend; pub mod pedersen; diff --git a/src/pedersen.rs b/src/pedersen.rs index 7d0a8c5..8285714 100644 --- a/src/pedersen.rs +++ b/src/pedersen.rs @@ -1,6 +1,9 @@ use ark_ec::CurveGroup; +use ark_ff::Field; +use ark_r1cs_std::{boolean::Boolean, groups::GroupOpsBounds, prelude::CurveVar}; +use ark_relations::r1cs::SynthesisError; use ark_std::{rand::Rng, UniformRand}; -use std::marker::PhantomData; +use core::marker::PhantomData; use crate::utils::vec::{vec_add, vec_scalar_mul}; @@ -9,14 +12,14 @@ use crate::Error; #[derive(Debug, Clone, Eq, PartialEq)] pub struct Proof { - R: C, - u: Vec, - r_u: C::ScalarField, + pub R: C, + pub u: Vec, + pub r_u: C::ScalarField, } #[derive(Debug, Clone, Eq, PartialEq)] pub struct Params { - h: C, + pub h: C, pub generators: Vec, } @@ -111,13 +114,52 @@ impl Pedersen { } } +pub type CF = <::BaseField as Field>::BasePrimeField; + +pub struct PedersenGadget +where + C: CurveGroup, + GC: CurveVar>, +{ + _cf: PhantomData>, + _c: PhantomData, + _gc: PhantomData, +} + +impl PedersenGadget +where + C: CurveGroup, + GC: CurveVar>, + + ::BaseField: ark_ff::PrimeField, + for<'a> &'a GC: GroupOpsBounds<'a, C, GC>, +{ + pub fn commit( + h: GC, + g: Vec, + v: Vec>>>, + r: Vec>>, + ) -> Result { + let mut res = GC::zero(); + res += h.scalar_mul_le(r.iter())?; + for (i, v_i) in v.iter().enumerate() { + res += g[i].scalar_mul_le(v_i.iter())?; + } + Ok(res) + } +} + #[cfg(test)] mod tests { + use ark_ff::{BigInteger, PrimeField}; + use ark_pallas::{constraints::GVar, Fq, Fr, Projective}; + use ark_r1cs_std::{alloc::AllocVar, bits::boolean::Boolean, eq::EqGadget}; + use ark_relations::r1cs::ConstraintSystem; + use ark_std::UniformRand; + use super::*; use crate::transcript::poseidon::{tests::poseidon_test_config, PoseidonTranscript}; - use ark_pallas::{Fr, Projective}; - #[test] fn test_pedersen_vector() { let mut rng = ark_std::test_rng(); @@ -140,4 +182,41 @@ mod tests { let proof = Pedersen::::prove(¶ms, &mut transcript_p, &cm, &v, &r).unwrap(); Pedersen::::verify(¶ms, &mut transcript_v, cm, proof).unwrap(); } + + #[test] + fn test_pedersen_circuit() { + let mut rng = ark_std::test_rng(); + + const n: usize = 10; + // setup params + let params = Pedersen::::new_params(&mut rng, n); + + let v: Vec = std::iter::repeat_with(|| Fr::rand(&mut rng)) + .take(n) + .collect(); + let r: Fr = Fr::rand(&mut rng); + let cm = Pedersen::::commit(¶ms, &v, &r).unwrap(); + + // circuit + let cs = ConstraintSystem::::new_ref(); + + let v_bits: Vec> = v.iter().map(|val| val.into_bigint().to_bits_le()).collect(); + let r_bits: Vec = r.into_bigint().to_bits_le(); + + // prepare inputs + let vVar: Vec>> = v_bits + .iter() + .map(|val_bits| { + Vec::>::new_witness(cs.clone(), || Ok(val_bits.clone())).unwrap() + }) + .collect(); + let rVar = Vec::>::new_witness(cs.clone(), || Ok(r_bits)).unwrap(); + let gVar = Vec::::new_witness(cs.clone(), || Ok(params.generators)).unwrap(); + let hVar = GVar::new_witness(cs.clone(), || Ok(params.h)).unwrap(); + let expected_cmVar = GVar::new_witness(cs.clone(), || Ok(cm)).unwrap(); + + // use the gadget + let cmVar = PedersenGadget::::commit(hVar, gVar, vVar, rVar).unwrap(); + cmVar.enforce_equal(&expected_cmVar).unwrap(); + } } diff --git a/src/utils/gadgets.rs b/src/utils/gadgets.rs new file mode 100644 index 0000000..dc0db11 --- /dev/null +++ b/src/utils/gadgets.rs @@ -0,0 +1,105 @@ +use ark_ff::PrimeField; +use ark_r1cs_std::{ + alloc::{AllocVar, AllocationMode}, + fields::FieldVar, +}; +use ark_relations::r1cs::{Namespace, SynthesisError}; +use core::{borrow::Borrow, marker::PhantomData}; + +use crate::utils::vec::SparseMatrix; + +pub fn mat_vec_mul_sparse>( + m: SparseMatrixVar, + v: Vec, +) -> Vec { + let mut res = vec![FV::zero(); m.n_rows]; + for (row_i, row) in m.coeffs.iter().enumerate() { + for (value, col_i) in row.iter() { + res[row_i] += value.clone().mul(&v[*col_i].clone()); + } + } + res +} +pub fn vec_add>( + a: &Vec, + b: &Vec, +) -> Result, SynthesisError> { + if a.len() != b.len() { + return Err(SynthesisError::Unsatisfiable); + } + let mut r: Vec = vec![FV::zero(); a.len()]; + for i in 0..a.len() { + r[i] = a[i].clone() + b[i].clone(); + } + Ok(r) +} +pub fn vec_scalar_mul>( + vec: &Vec, + c: &FV, +) -> Vec { + let mut result = vec![FV::zero(); vec.len()]; + for (i, a) in vec.iter().enumerate() { + result[i] = a.clone() * c; + } + result +} +pub fn hadamard>( + a: &Vec, + b: &Vec, +) -> Result, SynthesisError> { + if a.len() != b.len() { + return Err(SynthesisError::Unsatisfiable); + } + let mut r: Vec = vec![FV::zero(); a.len()]; + for i in 0..a.len() { + r[i] = a[i].clone() * b[i].clone(); + } + Ok(r) +} + +#[derive(Debug, Clone)] +pub struct SparseMatrixVar> { + _f: PhantomData, + _cf: PhantomData, + _fv: PhantomData, + pub n_rows: usize, + pub n_cols: usize, + // same format as the native SparseMatrix (which follows ark_relations::r1cs::Matrix format + pub coeffs: Vec>, +} + +impl AllocVar, CF> for SparseMatrixVar +where + F: PrimeField, + CF: PrimeField, + FV: FieldVar, +{ + fn new_variable>>( + cs: impl Into>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let mut coeffs: Vec> = Vec::new(); + for row in val.borrow().coeffs.iter() { + let mut rowVar: Vec<(FV, usize)> = Vec::new(); + for &(value, col_i) in row.iter() { + let coeffVar = FV::new_variable(cs.clone(), || Ok(value), mode)?; + rowVar.push((coeffVar, col_i)); + } + coeffs.push(rowVar); + } + + Ok(Self { + _f: PhantomData, + _cf: PhantomData, + _fv: PhantomData, + n_rows: val.borrow().n_rows, + n_cols: val.borrow().n_cols, + coeffs, + }) + }) + } +} diff --git a/src/utils/mod.rs b/src/utils/mod.rs index 31e71dd..a095df0 100644 --- a/src/utils/mod.rs +++ b/src/utils/mod.rs @@ -1,4 +1,5 @@ pub mod bit; +pub mod gadgets; pub mod hypercube; pub mod lagrange_poly; pub mod mle;