diff --git a/Cargo.toml b/Cargo.toml index 69f276b..dde7c9a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,7 +10,7 @@ ark-poly = "^0.4.0" ark-std = "^0.4.0" ark-crypto-primitives = { version = "^0.4.0", default-features = false, features = ["r1cs", "sponge", "crh"] } ark-relations = { version = "^0.4.0", default-features = false } -ark-r1cs-std = { version = "^0.4.0", default-features = false } +ark-r1cs-std = { default-features = false } # use latest version from the patch ark-circom = { git = "https://github.com/gakonst/ark-circom.git" } thiserror = "1.0" rayon = "1.7.0" @@ -26,6 +26,8 @@ espresso_transcript = {git="https://github.com/EspressoSystems/hyperplonk", pack ark-pallas = {version="0.4.0", features=["r1cs"]} ark-vesta = {version="0.4.0"} ark-bn254 = "0.4.0" +tracing = { version = "0.1", default-features = false, features = [ "attributes" ] } +tracing-subscriber = { version = "0.2" } [features] default = ["parallel", "nova", "hypernova"] @@ -37,3 +39,11 @@ parallel = [ "ark-ff/parallel", "ark-poly/parallel", ] + +# The following patch is to use a version of ark-r1cs-std compatible with +# v0.4.0 but that includes a cherry-picked commit from after v0.4.0 which fixes +# the in-circuit scalar multiplication of the zero point. The commit is from +# https://github.com/arkworks-rs/r1cs-std/pull/124, without including other +# changes done between v0.4.0 and this fix which would break compatibility. +[patch.crates-io] +ark-r1cs-std = { git = "https://github.com/arnaucube/ark-r1cs-std-cherry-picked/" } diff --git a/src/folding/circuits/cyclefold.rs b/src/folding/circuits/cyclefold.rs index 9b3c708..83709e4 100644 --- a/src/folding/circuits/cyclefold.rs +++ b/src/folding/circuits/cyclefold.rs @@ -21,9 +21,8 @@ impl>> ECRLC { p1: GC, p2: GC, p3: GC, - ) -> Result<(), SynthesisError> { - p3.enforce_equal(&(p1 + p2.scalar_mul_le(r_bits.iter())?))?; - Ok(()) + ) -> Result>, SynthesisError> { + p3.is_eq(&(p1 + p2.scalar_mul_le(r_bits.iter())?)) } } @@ -32,7 +31,7 @@ mod tests { use super::*; use ark_ff::{BigInteger, PrimeField}; use ark_pallas::{constraints::GVar, Fq, Fr, Projective}; - use ark_r1cs_std::alloc::AllocVar; + use ark_r1cs_std::{alloc::AllocVar, eq::EqGadget}; use ark_relations::r1cs::ConstraintSystem; use ark_std::UniformRand; use std::ops::Mul; @@ -59,7 +58,8 @@ mod tests { let p3Var = GVar::new_witness(cs.clone(), || Ok(p3)).unwrap(); // check ECRLC circuit - ECRLC::::check(rbitsVar, p1Var, p2Var, p3Var).unwrap(); + let check_pass = ECRLC::::check(rbitsVar, p1Var, p2Var, p3Var).unwrap(); + check_pass.enforce_equal(&Boolean::::TRUE).unwrap(); assert!(cs.is_satisfied().unwrap()); } } diff --git a/src/folding/circuits/nonnative.rs b/src/folding/circuits/nonnative.rs index f5a37a9..08e1545 100644 --- a/src/folding/circuits/nonnative.rs +++ b/src/folding/circuits/nonnative.rs @@ -6,6 +6,7 @@ use ark_r1cs_std::{ fields::nonnative::NonNativeFieldVar, }; use ark_relations::r1cs::{Namespace, SynthesisError}; +use ark_std::{One, Zero}; use core::borrow::Borrow; /// NonNativeAffineVar represents an elliptic curve point in Affine represenation in the non-native @@ -31,6 +32,19 @@ where let cs = cs.into(); let affine = val.borrow().into_affine(); + if affine.is_zero() { + let x = NonNativeFieldVar::::new_variable( + cs.clone(), + || Ok(C::BaseField::zero()), + mode, + )?; + let y = NonNativeFieldVar::::new_variable( + cs.clone(), + || Ok(C::BaseField::one()), + mode, + )?; + return Ok(Self { x, y }); + } let xy = affine.xy().unwrap(); let x = NonNativeFieldVar::::new_variable( cs.clone(), @@ -58,6 +72,20 @@ where ::BaseField: ark_ff::PrimeField, { let affine = p.into_affine(); + if affine.is_zero() { + let x = + AllocatedNonNativeFieldVar::::get_limbs_representations( + &C::BaseField::zero(), + OptimizationType::Weight, + )?; + let y = + AllocatedNonNativeFieldVar::::get_limbs_representations( + &C::BaseField::one(), + OptimizationType::Weight, + )?; + return Ok((x, y)); + } + let (x, y) = affine.xy().unwrap(); let x = AllocatedNonNativeFieldVar::::get_limbs_representations( x, @@ -69,3 +97,21 @@ where )?; Ok((x, y)) } + +#[cfg(test)] +mod tests { + use super::*; + use ark_pallas::{Fq, Fr, Projective}; + use ark_r1cs_std::alloc::AllocVar; + use ark_relations::r1cs::ConstraintSystem; + use ark_std::Zero; + + #[test] + fn test_alloc_nonnativeaffinevar_zero() { + let cs = ConstraintSystem::::new_ref(); + + // dealing with the 'zero' point should not panic when doing the unwrap + let p = Projective::zero(); + NonNativeAffineVar::::new_witness(cs.clone(), || Ok(p)).unwrap(); + } +} diff --git a/src/folding/nova/circuits.rs b/src/folding/nova/circuits.rs index 6557941..b33ae45 100644 --- a/src/folding/nova/circuits.rs +++ b/src/folding/nova/circuits.rs @@ -2,19 +2,20 @@ use ark_crypto_primitives::crh::{ poseidon::constraints::{CRHGadget, CRHParametersVar}, CRHSchemeGadget, }; -use ark_crypto_primitives::sponge::Absorb; +use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb}; use ark_ec::{AffineRepr, CurveGroup, Group}; -use ark_ff::Field; +use ark_ff::{Field, PrimeField}; use ark_r1cs_std::{ alloc::{AllocVar, AllocationMode}, boolean::Boolean, eq::EqGadget, - fields::fp::FpVar, + fields::{fp::FpVar, FieldVar}, groups::GroupOpsBounds, prelude::CurveVar, ToConstraintFieldGadget, }; -use ark_relations::r1cs::{Namespace, SynthesisError}; +use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError}; +use ark_std::Zero; use core::{borrow::Borrow, marker::PhantomData}; use super::CommittedInstance; @@ -32,10 +33,8 @@ pub type CF2 = <::BaseField as Field>::BasePrimeField; /// constraints field (E1::Fr, where E1 is the main curve). #[derive(Debug, Clone)] pub struct CommittedInstanceVar { - _c: PhantomData, u: FpVar, x: Vec>, - #[allow(dead_code)] // tmp while we don't have the code of the AugmentedFGadget cmE: NonNativeAffineVar, C::ScalarField>, cmW: NonNativeAffineVar, C::ScalarField>, } @@ -43,7 +42,7 @@ pub struct CommittedInstanceVar { impl AllocVar, CF1> for CommittedInstanceVar where C: CurveGroup, - ::BaseField: ark_ff::PrimeField, + ::BaseField: PrimeField, { fn new_variable>>( cs: impl Into>>, @@ -68,13 +67,7 @@ where mode, )?; - Ok(Self { - _c: PhantomData, - u, - x, - cmE, - cmW, - }) + Ok(Self { u, x, cmE, cmW }) }) } } @@ -88,7 +81,6 @@ 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`. - #[allow(dead_code)] // tmp while we don't have the code of the AugmentedFGadget fn hash( self, crh_params: &CRHParametersVar>, @@ -164,9 +156,9 @@ where ci1: CommittedInstanceVar, ci2: CommittedInstanceVar, ci3: CommittedInstanceVar, - ) -> Result<(), SynthesisError> { + ) -> Result>, SynthesisError> { // ensure that: ci3.u == ci1.u + r * ci2.u - ci3.u.enforce_equal(&(ci1.u + r.clone() * ci2.u))?; + let first_check = ci3.u.is_eq(&(ci1.u + r.clone() * ci2.u))?; // ensure that: ci3.x == ci1.x + r * ci2.x let x_rlc = ci1 @@ -175,9 +167,9 @@ where .zip(ci2.x) .map(|(a, b)| a + &r * &b) .collect::>>>(); - x_rlc.enforce_equal(&ci3.x)?; + let second_check = x_rlc.is_eq(&ci3.x)?; - Ok(()) + first_check.and(&second_check) } } @@ -199,14 +191,145 @@ where ci1: CommittedInstanceCycleFoldVar, ci2: CommittedInstanceCycleFoldVar, ci3: CommittedInstanceCycleFoldVar, - ) -> Result<(), SynthesisError> { + ) -> Result>, SynthesisError> { // cm(E) check: ci3.cmE == ci1.cmE + r * cmT + r^2 * ci2.cmE - ci3.cmE.enforce_equal( + let first_check = ci3.cmE.is_eq( &((ci2.cmE.scalar_mul_le(r_bits.iter())? + cmT).scalar_mul_le(r_bits.iter())? + ci1.cmE), )?; // cm(W) check: ci3.cmW == ci1.cmW + r * ci2.cmW - ECRLC::::check(r_bits, ci1.cmW, ci2.cmW, ci3.cmW)?; + let second_check = ECRLC::::check(r_bits, ci1.cmW, ci2.cmW, ci3.cmW)?; + + first_check.and(&second_check) + } +} + +/// FCircuit defines the trait of the circuit of the F function, which is the one being executed +/// inside the agmented F' function. +pub trait FCircuit: Copy { + /// method that returns z_i (input), z_{i+1} (output) + fn public(self) -> (F, F); + + /// method that computes the next state values in place, assigning z_{i+1} into z_i, and + /// computing the new z_i + fn step_native(&mut self); + fn step_circuit( + self, + cs: ConstraintSystemRef, + z_i: FpVar, + ) -> Result, SynthesisError>; +} + +/// AugmentedFCircuit implements the F' circuit (augmented F) defined in +/// [Nova](https://eprint.iacr.org/2021/370.pdf). +#[derive(Debug, Clone)] +pub struct AugmentedFCircuit>> { + pub poseidon_config: PoseidonConfig>, + pub i: Option>, + pub z_0: Option, + pub z_i: Option, + pub u_i: Option>, + pub U_i: Option>, + pub U_i1: Option>, + pub cmT: Option, + pub r: Option, // This will not be an input and derived from a hash internally in the circuit (poseidon transcript) + pub F: FC, // F circuit + pub x: Option>, // public inputs (u_{i+1}.x) +} + +impl>> ConstraintSynthesizer> for AugmentedFCircuit +where + C: CurveGroup, + ::BaseField: PrimeField, + ::ScalarField: Absorb, +{ + 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 = FpVar::>::new_witness(cs.clone(), || { + Ok(self.z_0.unwrap_or_else(CF1::::zero)) + })?; + let z_i = FpVar::>::new_witness(cs.clone(), || { + Ok(self.z_i.unwrap_or_else(CF1::::zero)) + })?; + + // get z_{i+1} from the F circuit + let z_i1 = self.F.step_circuit(cs.clone(), z_i.clone())?; + + let u_dummy_native = CommittedInstance { + cmE: C::zero(), + u: C::ScalarField::zero(), + cmW: C::zero(), + x: vec![CF1::::zero()], + }; + + let u_dummy = + CommittedInstanceVar::::new_witness(cs.clone(), || Ok(u_dummy_native.clone()))?; + let u_i = CommittedInstanceVar::::new_witness(cs.clone(), || { + Ok(self.u_i.unwrap_or_else(|| u_dummy_native.clone())) + })?; + let U_i = CommittedInstanceVar::::new_witness(cs.clone(), || { + Ok(self.U_i.unwrap_or_else(|| u_dummy_native.clone())) + })?; + let U_i1 = CommittedInstanceVar::::new_witness(cs.clone(), || { + Ok(self.U_i1.unwrap_or_else(|| u_dummy_native.clone())) + })?; + let _cmT = + NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C::zero)))?; + let r = + FpVar::>::new_witness(cs.clone(), || Ok(self.r.unwrap_or_else(CF1::::zero)))?; // r will come from higher level transcript + let x = + FpVar::>::new_input(cs.clone(), || Ok(self.x.unwrap_or_else(CF1::::zero)))?; + + let crh_params = + CRHParametersVar::::new_constant(cs.clone(), self.poseidon_config)?; + + let zero = FpVar::>::new_constant(cs.clone(), CF1::::zero())?; + let is_basecase = i.is_eq(&zero)?; + let is_not_basecase = i.is_neq(&zero)?; + + // 1. h_{i+1} = 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())?; + + // check that h == u_i.x + (u_i.x[0]).conditional_enforce_equal(&u_i_x, &is_not_basecase)?; + + // 2. u_i.cmE==cm(0), u_i.u==1 + (u_i.cmE.x.is_eq(&u_dummy.cmE.x)?) + .conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?; + (u_i.cmE.y.is_eq(&u_dummy.cmE.y)?) + .conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?; + (u_i.u.is_one()?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?; + + // 3. nifs.verify, checks that folding u_i & U_i obtains U_{i+1}. + // Notice that NIFSGadget::verify is not checking the folding of cmE & cmW, since it will + // be done on the other curve. + let nifs_check = NIFSGadget::::verify(r, u_i, U_i.clone(), U_i1.clone())?; + nifs_check.conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?; + + // 4. (base case) u_{i+1}.X == H(1, z_0, F(z_0)=F(z_i)=z_i1, U_i) (with U_i being dummy) + let u_i1_x_basecase = U_i.hash( + &crh_params, + FpVar::>::one(), + z_0.clone(), + z_i1.clone(), + )?; + + // 4. (non-base case). u_{i+1}.x = H(i+1, z_0, z_i+1, U_{i+1}), this is the output of F' + let u_i1_x = U_i1.hash( + &crh_params, + i + FpVar::>::one(), + z_0.clone(), + z_i1.clone(), + )?; + + // if i==0: check x==u_{i+1}.x_basecase + u_i1_x_basecase.conditional_enforce_equal(&x, &is_basecase)?; + // else: check x==u_{i+1}.x + u_i1_x.conditional_enforce_equal(&x, &is_not_basecase)?; + Ok(()) } } @@ -214,18 +337,50 @@ where #[cfg(test)] mod tests { use super::*; - use ark_ff::{BigInteger, PrimeField}; + use ark_ff::BigInteger; use ark_pallas::{constraints::GVar, Fq, Fr, Projective}; use ark_r1cs_std::{alloc::AllocVar, R1CSVar}; - use ark_relations::r1cs::ConstraintSystem; + use ark_relations::r1cs::{ConstraintLayer, ConstraintSystem, TracingMode}; + use ark_std::One; use ark_std::UniformRand; + use tracing_subscriber::layer::SubscriberExt; use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z}; - use crate::folding::nova::{nifs::NIFS, Witness}; + use crate::constants::N_BITS_CHALLENGE; + use crate::folding::nova::{check_instance_relation, nifs::NIFS, Witness}; + use crate::frontend::arkworks::{extract_r1cs, extract_z}; use crate::pedersen::Pedersen; use crate::transcript::poseidon::{tests::poseidon_test_config, PoseidonTranscript}; use crate::transcript::Transcript; + #[derive(Clone, Copy, Debug)] + /// TestFCircuit is a variation of `x^3 + x + 5 = y` (as in + /// src/frontend/arkworks/mod.rs#tests::TestCircuit), adapted to have 2 public inputs which are + /// used as the state. `z_i` is used as `x`, and `z_{i+1}` is used as `y`, and at the next + /// step, `z_{i+1}` will be assigned to `z_i`, and a new `z+{i+1}` will be computted. + pub struct TestFCircuit { + z_i: F, // z_i + z_i1: F, // z_{i+1} + } + impl FCircuit for TestFCircuit { + fn public(self) -> (F, F) { + (self.z_i, self.z_i1) + } + fn step_native(&mut self) { + self.z_i = self.z_i1; + self.z_i1 = self.z_i * self.z_i * self.z_i + self.z_i + F::from(5_u32); + } + fn step_circuit( + self, + cs: ConstraintSystemRef, + z_i: FpVar, + ) -> Result, SynthesisError> { + let five = FpVar::::new_constant(cs.clone(), F::from(5u32))?; + + Ok(&z_i * &z_i * &z_i + &z_i + &five) + } + } + #[test] fn test_committed_instance_var() { let mut rng = ark_std::test_rng(); @@ -266,7 +421,7 @@ mod tests { let w2 = Witness::::new(w2.clone(), r1cs.A.n_rows); let mut rng = ark_std::test_rng(); - let pedersen_params = Pedersen::::new_params(&mut rng, r1cs.A.n_cols); + let pedersen_params = Pedersen::::new_params(&mut rng, r1cs.A.n_rows); // compute committed instances let ci1 = w1.commit(&pedersen_params, x1.clone()); @@ -275,12 +430,15 @@ mod tests { // get challenge from transcript let poseidon_config = poseidon_test_config::(); let mut tr = PoseidonTranscript::::new(&poseidon_config); - let r_bits = tr.get_challenge_nbits(128); + let r_bits = tr.get_challenge_nbits(N_BITS_CHALLENGE); let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap(); let (_w3, ci3, _T, cmT) = NIFS::::prove(&pedersen_params, r_Fr, &r1cs, &w1, &ci1, &w2, &ci2).unwrap(); + let ci3_verifier = NIFS::::verify(r_Fr, &ci1, &ci2, &cmT); + assert_eq!(ci3_verifier, ci3); + let cs = ConstraintSystem::::new_ref(); let rVar = FpVar::::new_witness(cs.clone(), || Ok(r_Fr)).unwrap(); @@ -294,13 +452,14 @@ mod tests { CommittedInstanceVar::::new_witness(cs.clone(), || Ok(ci3.clone())) .unwrap(); - NIFSGadget::::verify( + let nifs_check = NIFSGadget::::verify( rVar.clone(), ci1Var.clone(), ci2Var.clone(), ci3Var.clone(), ) .unwrap(); + nifs_check.enforce_equal(&Boolean::::TRUE).unwrap(); assert!(cs.is_satisfied().unwrap()); // cs_CC is the Constraint System on the Curve Cycle auxiliary curve constraints field @@ -326,8 +485,11 @@ mod tests { }) .unwrap(); - NIFSCycleFoldGadget::::verify(r_bitsVar, cmTVar, ci1Var, ci2Var, ci3Var) - .unwrap(); + let nifs_cf_check = NIFSCycleFoldGadget::::verify( + r_bitsVar, cmTVar, ci1Var, ci2Var, ci3Var, + ) + .unwrap(); + nifs_cf_check.enforce_equal(&Boolean::::TRUE).unwrap(); assert!(cs_CC.is_satisfied().unwrap()); } @@ -366,4 +528,184 @@ mod tests { // check that the natively computed and in-circuit computed hashes match assert_eq!(hVar.value().unwrap(), h); } + + #[test] + /// test_augmented_f_circuit folds the TestFCircuit circuit in multiple iterations, feeding the + /// values into the AugmentedFCircuit. + fn test_augmented_f_circuit() { + let mut layer = ConstraintLayer::default(); + layer.mode = TracingMode::OnlyConstraints; + let subscriber = tracing_subscriber::Registry::default().with(layer); + let _guard = tracing::subscriber::set_default(subscriber); + + let mut rng = ark_std::test_rng(); + let poseidon_config = poseidon_test_config::(); + + // compute z vector for the initial instance + let cs = ConstraintSystem::::new_ref(); + + // prepare the circuit to obtain its R1CS + let test_F_circuit_dummy = TestFCircuit:: { + z_i: Fr::zero(), + z_i1: Fr::zero(), + }; + let mut augmented_F_circuit = AugmentedFCircuit::> { + poseidon_config: poseidon_config.clone(), + i: None, + z_0: None, + z_i: None, + u_i: None, + U_i: None, + U_i1: None, + cmT: None, + r: None, + F: test_F_circuit_dummy, + x: None, + }; + augmented_F_circuit + .generate_constraints(cs.clone()) + .unwrap(); + cs.finalize(); + let cs = cs.into_inner().unwrap(); + let r1cs = extract_r1cs::(&cs); + let z = extract_z::(&cs); // includes 1 and public inputs + let (w, x) = r1cs.split_z(&z); + let F_witness_len = w.len(); + + let mut tr = PoseidonTranscript::::new(&poseidon_config); + + let pedersen_params = Pedersen::::new_params(&mut rng, r1cs.A.n_rows); + + // first step + let z_0 = Fr::from(3_u32); + let mut z_i = z_0; + let mut z_i1 = Fr::from(35_u32); + + // set the circuit to be folded with z_i=z_0=3 and z_{i+1}=35 (initial values) + let mut test_F_circuit = TestFCircuit:: { z_i, z_i1 }; + + let w_dummy = Witness::::new(vec![Fr::zero(); F_witness_len], r1cs.A.n_rows); + let u_dummy = CommittedInstance::::dummy(x.len()); + + // Wi is a 'dummy witness', all zeroes, but with the size corresponding to the R1CS that + // we're working with. + // set U_i <-- dummay instance + let mut W_i = w_dummy.clone(); + let mut U_i = u_dummy.clone(); + check_instance_relation(&r1cs, &W_i, &U_i).unwrap(); + + let mut w_i = w_dummy.clone(); + let mut u_i = u_dummy.clone(); + let (mut W_i1, mut U_i1, mut _T, mut cmT) = ( + w_dummy.clone(), + u_dummy.clone(), + vec![], + Projective::generator(), + ); + // as expected, dummy instances pass the relaxed_r1cs check + check_instance_relation(&r1cs, &W_i1, &U_i1).unwrap(); + + let mut i = Fr::zero(); + let mut u_i1_x: Fr; + let n_steps: usize = 4; + for _ in 0..n_steps { + if i == Fr::zero() { + // base case: i=0, z_i=z_0, U_i = U_d := dummy instance + // u_1.x = H(1, z_0, z_i, U_i) + u_i1_x = U_i.hash(&poseidon_config, Fr::one(), z_0, z_i1).unwrap(); + + // base case + augmented_F_circuit = AugmentedFCircuit::> { + poseidon_config: poseidon_config.clone(), + i: Some(i), // = 0 + z_0: Some(z_0), // = z_i=3 + z_i: Some(z_i), + u_i: Some(u_i.clone()), // = dummy + U_i: Some(U_i.clone()), // = dummy + U_i1: Some(U_i1.clone()), // = dummy + cmT: Some(cmT), + r: Some(Fr::one()), + F: test_F_circuit, + x: Some(u_i1_x), + }; + } else { + // get challenge from transcript (since this is a test, we skip absorbing values to + // the transcript for simplicity) + let r_bits = tr.get_challenge_nbits(N_BITS_CHALLENGE); + let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap(); + + check_instance_relation(&r1cs, &w_i, &u_i).unwrap(); + check_instance_relation(&r1cs, &W_i, &U_i).unwrap(); + + // U_{i+1} + (W_i1, U_i1, _T, cmT) = NIFS::::prove( + &pedersen_params, + r_Fr, + &r1cs, + &w_i, + &u_i, + &W_i, + &U_i, + ) + .unwrap(); + + check_instance_relation(&r1cs, &W_i1, &U_i1).unwrap(); + + // folded instance output (public input, x) + // u_{i+1}.x = H(i+1, z_0, z_{i+1}, U_{i+1}) + u_i1_x = U_i1 + .hash(&poseidon_config, i + Fr::one(), z_0, z_i1) + .unwrap(); + + augmented_F_circuit = AugmentedFCircuit::> { + poseidon_config: poseidon_config.clone(), + i: Some(i), + z_0: Some(z_0), + z_i: Some(z_i), + u_i: Some(u_i), + U_i: Some(U_i.clone()), + U_i1: Some(U_i1.clone()), + cmT: Some(cmT), + r: Some(r_Fr), + F: test_F_circuit, + x: Some(u_i1_x), + }; + } + + let cs = ConstraintSystem::::new_ref(); + + augmented_F_circuit + .generate_constraints(cs.clone()) + .unwrap(); + let is_satisfied = cs.is_satisfied().unwrap(); + if !is_satisfied { + println!("{:?}", cs.which_is_unsatisfied()); + } + assert!(is_satisfied); + + cs.finalize(); + let cs = cs.into_inner().unwrap(); + // notice that here we use 'Z' (uppercase) to denote the 'z-vector' as in the paper, + // not the value 'z_i' (lowercase) which is the next state + let Z_i1 = extract_z::(&cs); + let (w_i1, x_i1) = r1cs.split_z(&Z_i1); + assert_eq!(x_i1.len(), 1); + assert_eq!(x_i1[0], u_i1_x); + + // 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. + w_i = Witness::::new(w_i1.clone(), r1cs.A.n_rows); + u_i = w_i.commit(&pedersen_params, vec![u_i1_x]); + + check_instance_relation(&r1cs, &w_i, &u_i).unwrap(); + check_instance_relation(&r1cs, &W_i1, &U_i1).unwrap(); + + // set values for next iteration + i += Fr::one(); + test_F_circuit.step_native(); // advance the F circuit state + (z_i, z_i1) = test_F_circuit.public(); + U_i = U_i1.clone(); + W_i = W_i1.clone(); + } + } } diff --git a/src/folding/nova/mod.rs b/src/folding/nova/mod.rs index 704f068..b196a69 100644 --- a/src/folding/nova/mod.rs +++ b/src/folding/nova/mod.rs @@ -7,8 +7,10 @@ use ark_ec::{CurveGroup, Group}; use ark_std::fmt::Debug; use ark_std::{One, Zero}; +use crate::ccs::r1cs::R1CS; use crate::folding::circuits::nonnative::point_to_nonnative_limbs; use crate::pedersen::{Params as PedersenParams, Pedersen}; +use crate::utils::vec::is_zero_vec; use crate::Error; pub mod circuits; @@ -27,12 +29,12 @@ where ::ScalarField: Absorb, ::BaseField: ark_ff::PrimeField, { - pub fn empty() -> Self { - CommittedInstance { + pub fn dummy(io_len: usize) -> Self { + Self { cmE: C::zero(), - u: C::ScalarField::one(), + u: C::ScalarField::zero(), cmW: C::zero(), - x: Vec::new(), + x: vec![C::ScalarField::zero(); io_len], } } @@ -81,7 +83,7 @@ where pub fn new(w: Vec, e_len: usize) -> Self { Self { E: vec![C::ScalarField::zero(); e_len], - rE: C::ScalarField::one(), + rE: C::ScalarField::zero(), // because we use C::zero() as cmE W: w, rW: C::ScalarField::one(), } @@ -91,7 +93,10 @@ where params: &PedersenParams, x: Vec, ) -> CommittedInstance { - let cmE = Pedersen::commit(params, &self.E, &self.rE); + let mut cmE = C::zero(); + if !is_zero_vec::(&self.E) { + cmE = Pedersen::commit(params, &self.E, &self.rE); + } let cmW = Pedersen::commit(params, &self.W, &self.rW); CommittedInstance { cmE, @@ -101,3 +106,16 @@ where } } } + +pub fn check_instance_relation( + r1cs: &R1CS, + W: &Witness, + U: &CommittedInstance, +) -> Result<(), Error> { + let mut rel_r1cs = r1cs.clone().relax(); + rel_r1cs.u = U.u; + rel_r1cs.E = W.E.clone(); + + let Z: Vec = [vec![U.u], U.x.to_vec(), W.W.to_vec()].concat(); + rel_r1cs.check_relation(&Z) +} diff --git a/src/folding/nova/nifs.rs b/src/folding/nova/nifs.rs index 1628ddc..e3d7609 100644 --- a/src/folding/nova/nifs.rs +++ b/src/folding/nova/nifs.rs @@ -181,19 +181,55 @@ where } #[cfg(test)] -mod tests { +pub mod tests { use super::*; - use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z}; - use crate::transcript::poseidon::{tests::poseidon_test_config, PoseidonTranscript}; use ark_ff::PrimeField; use ark_pallas::{Fr, Projective}; - use ark_std::UniformRand; + use ark_std::{ops::Mul, UniformRand, Zero}; + + use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z}; + use crate::transcript::poseidon::{tests::poseidon_test_config, PoseidonTranscript}; + use crate::utils::vec::vec_scalar_mul; + + pub fn check_relaxed_r1cs(r1cs: &R1CS, z: &[F], u: &F, E: &[F]) -> bool { + let Az = mat_vec_mul_sparse(&r1cs.A, z); + let Bz = mat_vec_mul_sparse(&r1cs.B, z); + let Cz = mat_vec_mul_sparse(&r1cs.C, z); + hadamard(&Az, &Bz).unwrap() == vec_add(&vec_scalar_mul(&Cz, u), E).unwrap() + } + + // fold 2 dummy instances and check that the folded instance holds the relaxed R1CS relation + #[test] + fn test_nifs_fold_dummy() { + let r1cs = get_test_r1cs::(); + let z1 = get_test_z(3); + let (w1, x1) = r1cs.split_z(&z1); - pub fn check_relaxed_r1cs(r1cs: &R1CS, z: Vec, u: F, E: &[F]) { - let Az = mat_vec_mul_sparse(&r1cs.A, &z); - let Bz = mat_vec_mul_sparse(&r1cs.B, &z); - let Cz = mat_vec_mul_sparse(&r1cs.C, &z); - assert_eq!(hadamard(&Az, &Bz), vec_add(&vec_scalar_mul(&Cz, &u), E)); + let mut rng = ark_std::test_rng(); + let pedersen_params = Pedersen::::new_params(&mut rng, r1cs.A.n_cols); + + // dummy instance, witness and public inputs zeroes + let w_dummy = Witness::::new(vec![Fr::zero(); w1.len()], r1cs.A.n_rows); + let mut u_dummy = w_dummy.commit(&pedersen_params, vec![Fr::zero(); x1.len()]); + u_dummy.u = Fr::zero(); + + let w_i = w_dummy.clone(); + let u_i = u_dummy.clone(); + let W_i = w_dummy.clone(); + let U_i = u_dummy.clone(); + let z_dummy = vec![Fr::zero(); z1.len()]; + assert!(check_relaxed_r1cs(&r1cs, &z_dummy, &u_i.u, &w_i.E)); + assert!(check_relaxed_r1cs(&r1cs, &z_dummy, &U_i.u, &W_i.E)); + + let r_Fr = Fr::from(3_u32); + + let (W_i1, U_i1, _, _) = + NIFS::::prove(&pedersen_params, r_Fr, &r1cs, &w_i, &u_i, &W_i, &U_i) + .unwrap(); + + let z: Vec = [vec![U_i1.u], U_i1.x.to_vec(), W_i1.W.to_vec()].concat(); + assert_eq!(z.len(), z1.len()); + assert!(check_relaxed_r1cs(&r1cs, &z, &U_i1.u, &W_i1.E)); } // fold 2 instances into one @@ -218,11 +254,12 @@ mod tests { let ci2 = w2.commit(&pedersen_params, x2.clone()); // NIFS.P - let (w3, _, T, cmT) = + let (w3, ci3_aux, T, cmT) = NIFS::::prove(&pedersen_params, r, &r1cs, &w1, &ci1, &w2, &ci2).unwrap(); // NIFS.V let ci3 = NIFS::::verify(r, &ci1, &ci2, &cmT); + assert_eq!(ci3, ci3_aux); // naive check that the folded witness satisfies the relaxed r1cs let z3: Vec = [vec![ci3.u], ci3.x.to_vec(), w3.W.to_vec()].concat(); @@ -230,9 +267,9 @@ mod tests { let z3_aux = vec_add(&z1, &vec_scalar_mul(&z2, &r)).unwrap(); assert_eq!(z3, z3_aux); // check that relations hold for the 2 inputted instances and the folded one - check_relaxed_r1cs(&r1cs, z1, ci1.u, &w1.E); - check_relaxed_r1cs(&r1cs, z2, ci2.u, &w2.E); - check_relaxed_r1cs(&r1cs, z3, ci3.u, &w3.E); + assert!(check_relaxed_r1cs(&r1cs, &z1, &ci1.u, &w1.E)); + assert!(check_relaxed_r1cs(&r1cs, &z2, &ci2.u, &w2.E)); + assert!(check_relaxed_r1cs(&r1cs, &z3, &ci3.u, &w3.E)); // check that folded commitments from folded instance (ci) are equal to folding the // use folded rE, rW to commit w3 @@ -240,6 +277,10 @@ mod tests { assert_eq!(ci3_expected.cmE, ci3.cmE); assert_eq!(ci3_expected.cmW, ci3.cmW); + // next equalities should hold since we started from two cmE of zero-vector E's + assert_eq!(ci3.cmE, cmT.mul(r)); + assert_eq!(w3.E, vec_scalar_mul(&T, &r)); + // NIFS.Verify_Folded_Instance: NIFS::::verify_folded_instance(r, &ci1, &ci2, &ci3, &cmT).unwrap(); @@ -259,6 +300,7 @@ mod tests { &cmT, ) .unwrap(); + NIFS::::verify_commitments( &mut transcript_v, &pedersen_params, @@ -281,12 +323,12 @@ mod tests { // prepare the running instance let mut running_instance_w = Witness::::new(w.clone(), r1cs.A.n_rows); let mut running_committed_instance = running_instance_w.commit(&pedersen_params, x); - check_relaxed_r1cs( + assert!(check_relaxed_r1cs( &r1cs, - z, - running_committed_instance.u, + &z, + &running_committed_instance.u, &running_instance_w.E, - ); + )); let num_iters = 10; for i in 0..num_iters { @@ -295,12 +337,12 @@ mod tests { let (w, x) = r1cs.split_z(&incomming_instance_z); let incomming_instance_w = Witness::::new(w.clone(), r1cs.A.n_rows); let incomming_committed_instance = incomming_instance_w.commit(&pedersen_params, x); - check_relaxed_r1cs( + assert!(check_relaxed_r1cs( &r1cs, - incomming_instance_z.clone(), - incomming_committed_instance.u, + &incomming_instance_z.clone(), + &incomming_committed_instance.u, &incomming_instance_w.E, - ); + )); let r = Fr::rand(&mut rng); // folding challenge would come from the transcript @@ -331,7 +373,12 @@ mod tests { ] .concat(); - check_relaxed_r1cs(&r1cs, folded_z, folded_committed_instance.u, &folded_w.E); + assert!(check_relaxed_r1cs( + &r1cs, + &folded_z, + &folded_committed_instance.u, + &folded_w.E + )); // set running_instance for next loop iteration running_instance_w = folded_w; diff --git a/src/frontend/arkworks/mod.rs b/src/frontend/arkworks/mod.rs index 644b912..35b93c3 100644 --- a/src/frontend/arkworks/mod.rs +++ b/src/frontend/arkworks/mod.rs @@ -8,6 +8,17 @@ use crate::utils::vec::SparseMatrix; /// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format, and /// extracts public inputs and witness into z vector. Returns a tuple containing (R1CS, z). pub fn extract_r1cs_and_z(cs: &ConstraintSystem) -> (R1CS, Vec) { + let r1cs = extract_r1cs(cs); + + // z = (1, x, w) + let z = extract_z(cs); + + (r1cs, z) +} + +/// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format as R1CS +/// struct. +pub fn extract_r1cs(cs: &ConstraintSystem) -> R1CS { let m = cs.to_matrices().unwrap(); let n_rows = cs.num_constraints; @@ -29,23 +40,23 @@ pub fn extract_r1cs_and_z(cs: &ConstraintSystem) -> (R1CS, coeffs: m.c, }; + R1CS:: { + l: cs.num_instance_variables - 1, // -1 to substract the first '1' + A, + B, + C, + } +} + +/// extracts public inputs and witness into z vector from arkworks ConstraintSystem. +pub fn extract_z(cs: &ConstraintSystem) -> Vec { // z = (1, x, w) - let z: Vec = [ + [ // 1 is already included in cs.instance_assignment cs.instance_assignment.clone(), cs.witness_assignment.clone(), ] - .concat(); - - ( - R1CS:: { - l: cs.num_instance_variables, - A, - B, - C, - }, - z, - ) + .concat() } #[cfg(test)] @@ -96,5 +107,7 @@ pub mod tests { let (r1cs, z) = extract_r1cs_and_z::(&cs); r1cs.check_relation(&z).unwrap(); + // ensure that number of public inputs (l) is 1 + assert_eq!(r1cs.l, 1); } }