implement Nova's AugmentedFCircuit (#33)

* impl AugmentedFCircuit non-base case

* add multiple iterations to AugmentedFCircuit test

* implement base case on AugmentedFCircuit and test

* Update cmE of E=0-vec to work as zero point

Update cmE of E=0-vec to work as zero point instead of as cm(0-vec)

* patch r1cs-std dep to a cherry-picked version with the zero-scalar-mult fix

* refactor FCircuit to make it more suitable inside the AugmentedFCircuit

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/" }

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<Boolean<CF<C>>, 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::<Projective, GVar>::check(rbitsVar, p1Var, p2Var, p3Var).unwrap();
+        let check_pass = ECRLC::<Projective, GVar>::check(rbitsVar, p1Var, p2Var, p3Var).unwrap();
+        check_pass.enforce_equal(&Boolean::<Fq>::TRUE).unwrap();
         assert!(cs.is_satisfied().unwrap());
     }
 }

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::<C::BaseField, C::ScalarField>::new_variable(
+                    cs.clone(),
+                    || Ok(C::BaseField::zero()),
+                    mode,
+                )?;
+                let y = NonNativeFieldVar::<C::BaseField, C::ScalarField>::new_variable(
+                    cs.clone(),
+                    || Ok(C::BaseField::one()),
+                    mode,
+                )?;
+                return Ok(Self { x, y });
+            }
             let xy = affine.xy().unwrap();
             let x = NonNativeFieldVar::<C::BaseField, C::ScalarField>::new_variable(
                 cs.clone(),
@@ -58,6 +72,20 @@ where
     <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
 {
     let affine = p.into_affine();
+    if affine.is_zero() {
+        let x =
+            AllocatedNonNativeFieldVar::<C::BaseField, C::ScalarField>::get_limbs_representations(
+                &C::BaseField::zero(),
+                OptimizationType::Weight,
+            )?;
+        let y =
+            AllocatedNonNativeFieldVar::<C::BaseField, C::ScalarField>::get_limbs_representations(
+                &C::BaseField::one(),
+                OptimizationType::Weight,
+            )?;
+        return Ok((x, y));
+    }
+
     let (x, y) = affine.xy().unwrap();
     let x = AllocatedNonNativeFieldVar::<C::BaseField, C::ScalarField>::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::<Fr>::new_ref();
+
+        // dealing with the 'zero' point should not panic when doing the unwrap
+        let p = Projective::zero();
+        NonNativeAffineVar::<Fq, Fr>::new_witness(cs.clone(), || Ok(p)).unwrap();
+    }
+}

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: CurveGroup> {
-    _c: PhantomData<C>,
     u: FpVar<C::ScalarField>,
     x: Vec<FpVar<C::ScalarField>>,
-    #[allow(dead_code)] // tmp while we don't have the code of the AugmentedFGadget
     cmE: NonNativeAffineVar<CF2<C>, C::ScalarField>,
     cmW: NonNativeAffineVar<CF2<C>, C::ScalarField>,
 }
@@ -43,7 +42,7 @@ pub struct CommittedInstanceVar {
 impl<C> AllocVar<CommittedInstance<C>, CF1<C>> for CommittedInstanceVar<C>
 where
     C: CurveGroup,
-    <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
+    <C as ark_ec::CurveGroup>::BaseField: PrimeField,
 {
     fn new_variable<T: Borrow<CommittedInstance<C>>>(
         cs: impl Into<Namespace<CF1<C>>>,
@@ -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<CF1<C>>,
@@ -164,9 +156,9 @@ where
         ci1: CommittedInstanceVar<C>,
         ci2: CommittedInstanceVar<C>,
         ci3: CommittedInstanceVar<C>,
-    ) -> Result<(), SynthesisError> {
+    ) -> Result<Boolean<CF1<C>>, 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::<Vec<FpVar<CF1<C>>>>();
-        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<C, GC>,
         ci2: CommittedInstanceCycleFoldVar<C, GC>,
         ci3: CommittedInstanceCycleFoldVar<C, GC>,
-    ) -> Result<(), SynthesisError> {
+    ) -> Result<Boolean<CF2<C>>, 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::<C, GC>::check(r_bits, ci1.cmW, ci2.cmW, ci3.cmW)?;
+        let second_check = ECRLC::<C, GC>::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<F: PrimeField>: 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<F>,
+        z_i: FpVar<F>,
+    ) -> Result<FpVar<F>, SynthesisError>;
+}
+
+/// AugmentedFCircuit implements the F' circuit (augmented F) defined in
+/// [Nova](https://eprint.iacr.org/2021/370.pdf).
+#[derive(Debug, Clone)]
+pub struct AugmentedFCircuit<C: CurveGroup, FC: FCircuit<CF1<C>>> {
+    pub poseidon_config: PoseidonConfig<CF1<C>>,
+    pub i: Option<CF1<C>>,
+    pub z_0: Option<C::ScalarField>,
+    pub z_i: Option<C::ScalarField>,
+    pub u_i: Option<CommittedInstance<C>>,
+    pub U_i: Option<CommittedInstance<C>>,
+    pub U_i1: Option<CommittedInstance<C>>,
+    pub cmT: Option<C>,
+    pub r: Option<C::ScalarField>, // 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<CF1<C>>,         // public inputs (u_{i+1}.x)
+}
+
+impl<C: CurveGroup, FC: FCircuit<CF1<C>>> ConstraintSynthesizer<CF1<C>> for AugmentedFCircuit<C, FC>
+where
+    C: CurveGroup,
+    <C as CurveGroup>::BaseField: PrimeField,
+    <C as Group>::ScalarField: Absorb,
+{
+    fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C>>) -> Result<(), SynthesisError> {
+        let i =
+            FpVar::<CF1<C>>::new_witness(cs.clone(), || Ok(self.i.unwrap_or_else(CF1::<C>::zero)))?;
+        let z_0 = FpVar::<CF1<C>>::new_witness(cs.clone(), || {
+            Ok(self.z_0.unwrap_or_else(CF1::<C>::zero))
+        })?;
+        let z_i = FpVar::<CF1<C>>::new_witness(cs.clone(), || {
+            Ok(self.z_i.unwrap_or_else(CF1::<C>::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::<C>::zero()],
+        };
+
+        let u_dummy =
+            CommittedInstanceVar::<C>::new_witness(cs.clone(), || Ok(u_dummy_native.clone()))?;
+        let u_i = CommittedInstanceVar::<C>::new_witness(cs.clone(), || {
+            Ok(self.u_i.unwrap_or_else(|| u_dummy_native.clone()))
+        })?;
+        let U_i = CommittedInstanceVar::<C>::new_witness(cs.clone(), || {
+            Ok(self.U_i.unwrap_or_else(|| u_dummy_native.clone()))
+        })?;
+        let U_i1 = CommittedInstanceVar::<C>::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::<CF1<C>>::new_witness(cs.clone(), || Ok(self.r.unwrap_or_else(CF1::<C>::zero)))?; // r will come from higher level transcript
+        let x =
+            FpVar::<CF1<C>>::new_input(cs.clone(), || Ok(self.x.unwrap_or_else(CF1::<C>::zero)))?;
+
+        let crh_params =
+            CRHParametersVar::<C::ScalarField>::new_constant(cs.clone(), self.poseidon_config)?;
+
+        let zero = FpVar::<CF1<C>>::new_constant(cs.clone(), CF1::<C>::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::<C>::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::<CF1<C>>::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::<CF1<C>>::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<F: PrimeField> {
+        z_i: F,  // z_i
+        z_i1: F, // z_{i+1}
+    }
+    impl<F: PrimeField> FCircuit<F> for TestFCircuit<F> {
+        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<F>,
+            z_i: FpVar<F>,
+        ) -> Result<FpVar<F>, SynthesisError> {
+            let five = FpVar::<F>::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::<Projective>::new(w2.clone(), r1cs.A.n_rows);
 
         let mut rng = ark_std::test_rng();
-        let pedersen_params = Pedersen::<Projective>::new_params(&mut rng, r1cs.A.n_cols);
+        let pedersen_params = Pedersen::<Projective>::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::<Fr>();
         let mut tr = PoseidonTranscript::<Projective>::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::<Projective>::prove(&pedersen_params, r_Fr, &r1cs, &w1, &ci1, &w2, &ci2).unwrap();
 
+        let ci3_verifier = NIFS::<Projective>::verify(r_Fr, &ci1, &ci2, &cmT);
+        assert_eq!(ci3_verifier, ci3);
+
         let cs = ConstraintSystem::<Fr>::new_ref();
 
         let rVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(r_Fr)).unwrap();
@@ -294,13 +452,14 @@ mod tests {
             CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci3.clone()))
                 .unwrap();
 
-        NIFSGadget::<Projective>::verify(
+        let nifs_check = NIFSGadget::<Projective>::verify(
             rVar.clone(),
             ci1Var.clone(),
             ci2Var.clone(),
             ci3Var.clone(),
         )
         .unwrap();
+        nifs_check.enforce_equal(&Boolean::<Fr>::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::<Projective, GVar>::verify(r_bitsVar, cmTVar, ci1Var, ci2Var, ci3Var)
-            .unwrap();
+        let nifs_cf_check = NIFSCycleFoldGadget::<Projective, GVar>::verify(
+            r_bitsVar, cmTVar, ci1Var, ci2Var, ci3Var,
+        )
+        .unwrap();
+        nifs_cf_check.enforce_equal(&Boolean::<Fq>::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::<Fr>();
+
+        // compute z vector for the initial instance
+        let cs = ConstraintSystem::<Fr>::new_ref();
+
+        // prepare the circuit to obtain its R1CS
+        let test_F_circuit_dummy = TestFCircuit::<Fr> {
+            z_i: Fr::zero(),
+            z_i1: Fr::zero(),
+        };
+        let mut augmented_F_circuit = AugmentedFCircuit::<Projective, TestFCircuit<Fr>> {
+            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::<Fr>(&cs);
+        let z = extract_z::<Fr>(&cs); // includes 1 and public inputs
+        let (w, x) = r1cs.split_z(&z);
+        let F_witness_len = w.len();
+
+        let mut tr = PoseidonTranscript::<Projective>::new(&poseidon_config);
+
+        let pedersen_params = Pedersen::<Projective>::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::<Fr> { z_i, z_i1 };
+
+        let w_dummy = Witness::<Projective>::new(vec![Fr::zero(); F_witness_len], r1cs.A.n_rows);
+        let u_dummy = CommittedInstance::<Projective>::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::<Projective, TestFCircuit<Fr>> {
+                    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::<Projective>::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::<Projective, TestFCircuit<Fr>> {
+                    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::<Fr>::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::<Fr>(&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::<Projective>::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();
+        }
+    }
 }

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
     <C as Group>::ScalarField: Absorb,
     <C as ark_ec::CurveGroup>::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<C::ScalarField>, 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<C>,
         x: Vec<C::ScalarField>,
     ) -> CommittedInstance<C> {
-        let cmE = Pedersen::commit(params, &self.E, &self.rE);
+        let mut cmE = C::zero();
+        if !is_zero_vec::<C::ScalarField>(&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<C: CurveGroup>(
+    r1cs: &R1CS<C::ScalarField>,
+    W: &Witness<C>,
+    U: &CommittedInstance<C>,
+) -> Result<(), Error> {
+    let mut rel_r1cs = r1cs.clone().relax();
+    rel_r1cs.u = U.u;
+    rel_r1cs.E = W.E.clone();
+
+    let Z: Vec<C::ScalarField> = [vec![U.u], U.x.to_vec(), W.W.to_vec()].concat();
+    rel_r1cs.check_relation(&Z)
+}

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<F: PrimeField>(r1cs: &R1CS<F>, 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::<Fr>();
+        let z1 = get_test_z(3);
+        let (w1, x1) = r1cs.split_z(&z1);
 
-    pub fn check_relaxed_r1cs<F: PrimeField>(r1cs: &R1CS<F>, z: Vec<F>, 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::<Projective>::new_params(&mut rng, r1cs.A.n_cols);
+
+        // dummy instance, witness and public inputs zeroes
+        let w_dummy = Witness::<Projective>::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::<Projective>::prove(&pedersen_params, r_Fr, &r1cs, &w_i, &u_i, &W_i, &U_i)
+                .unwrap();
+
+        let z: Vec<Fr> = [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::<Projective>::prove(&pedersen_params, r, &r1cs, &w1, &ci1, &w2, &ci2).unwrap();
 
         // NIFS.V
         let ci3 = NIFS::<Projective>::verify(r, &ci1, &ci2, &cmT);
+        assert_eq!(ci3, ci3_aux);
 
         // naive check that the folded witness satisfies the relaxed r1cs
         let z3: Vec<Fr> = [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::<Projective>::verify_folded_instance(r, &ci1, &ci2, &ci3, &cmT).unwrap();
 
@@ -259,6 +300,7 @@ mod tests {
             &cmT,
         )
         .unwrap();
+
         NIFS::<Projective>::verify_commitments(
             &mut transcript_v,
             &pedersen_params,
@@ -281,12 +323,12 @@ mod tests {
         // prepare the running instance
         let mut running_instance_w = Witness::<Projective>::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::<Projective>::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;

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<F: PrimeField>(cs: &ConstraintSystem<F>) -> (R1CS<F>, Vec<F>) {
+    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<F: PrimeField>(cs: &ConstraintSystem<F>) -> R1CS<F> {
     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::<F> {
+        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<F: PrimeField>(cs: &ConstraintSystem<F>) -> Vec<F> {
     // z = (1, x, w)
-    let z: Vec<F> = [
+    [
         // 1 is already included in cs.instance_assignment
         cs.instance_assignment.clone(),
         cs.witness_assignment.clone(),
     ]
-    .concat();
-
-    (
-        R1CS::<F> {
-            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::<Fr>(&cs);
         r1cs.check_relation(&z).unwrap();
+        // ensure that number of public inputs (l) is 1
+        assert_eq!(r1cs.l, 1);
     }
 }