@@ -1,9 +1,12 @@
 use ark_ff::PrimeField;
 use ark_std::log2;
 
-use crate::utils::vec::{hadamard, mat_vec_mul, vec_add, vec_scalar_mul, SparseMatrix};
+use crate::utils::vec::{
+    hadamard, is_zero_vec, mat_vec_mul, vec_add, vec_scalar_mul, SparseMatrix,
+};
 use crate::Error;
 
+use super::ArithSerializer;
 use super::{r1cs::R1CS, Arith};
 
 /// CCS represents the Customizable Constraint Systems structure defined in
@@ -35,8 +38,9 @@ /// vector of coefficients
     pub c: Vec<F>,
 }
 
-impl<F: PrimeField> Arith<F> for CCS<F> {
-    fn eval_relation(&self, z: &[F]) -> Result<Vec<F>, Error> {
+impl<F: PrimeField> CCS<F> {
+    /// Evaluates the CCS relation at a given vector of assignments `z`
+    pub fn eval_at_z(&self, z: &[F]) -> Result<Vec<F>, Error> {
         let mut result = vec![F::zero(); self.m];
 
         for i in 0..self.q {
@@ -59,6 +63,25 @@
         Ok(result)
     }
 
+    /// returns a tuple containing (w, x) (witness and public inputs respectively)
+    pub fn split_z(&self, z: &[F]) -> (Vec<F>, Vec<F>) {
+        (z[self.l + 1..].to_vec(), z[1..self.l + 1].to_vec())
+    }
+}
+
+impl<F: PrimeField, W: AsRef<[F]>, U: AsRef<[F]>> Arith<W, U> for CCS<F> {
+    type Evaluation = Vec<F>;
+
+    fn eval_relation(&self, w: &W, u: &U) -> Result<Self::Evaluation, Error> {
+        self.eval_at_z(&[&[F::one()], u.as_ref(), w.as_ref()].concat())
+    }
+
+    fn check_evaluation(_w: &W, _u: &U, e: Self::Evaluation) -> Result<(), Error> {
+        is_zero_vec(&e).then_some(()).ok_or(Error::NotSatisfied)
+    }
+}
+
+impl<F: PrimeField> ArithSerializer for CCS<F> {
     fn params_to_le_bytes(&self) -> Vec<u8> {
         [
             self.l.to_le_bytes(),
@@ -72,14 +95,14 @@ .concat()
     }
 }
 
-impl<F: PrimeField> CCS<F> {
-    pub fn from_r1cs(r1cs: R1CS<F>) -> Self {
-        let m = r1cs.A.n_rows;
-        let n = r1cs.A.n_cols;
+impl<F: PrimeField> From<R1CS<F>> for CCS<F> {
+    fn from(r1cs: R1CS<F>) -> Self {
+        let m = r1cs.num_constraints();
+        let n = r1cs.num_variables();
         CCS {
             m,
             n,
-            l: r1cs.l,
+            l: r1cs.num_public_inputs(),
             s: log2(m) as usize,
             s_prime: log2(n) as usize,
             t: 3,
@@ -91,29 +114,19 @@ c: vec![F::one(), F::one().neg()],
             M: vec![r1cs.A, r1cs.B, r1cs.C],
         }
     }
-
-    pub fn to_r1cs(self) -> R1CS<F> {
-        R1CS::<F> {
-            l: self.l,
-            A: self.M[0].clone(),
-            B: self.M[1].clone(),
-            C: self.M[2].clone(),
-        }
-    }
 }
 
 #[cfg(test)]
 pub mod tests {
     use super::*;
     use crate::{
-        arith::r1cs::tests::{get_test_r1cs, get_test_z as r1cs_get_test_z},
+        arith::r1cs::tests::{get_test_r1cs, get_test_z as r1cs_get_test_z, get_test_z_split},
         utils::vec::is_zero_vec,
     };
     use ark_pallas::Fr;
 
     pub fn get_test_ccs<F: PrimeField>() -> CCS<F> {
-        let r1cs = get_test_r1cs::<F>();
-        CCS::<F>::from_r1cs(r1cs)
+        get_test_r1cs::<F>().into()
     }
     pub fn get_test_z<F: PrimeField>(input: usize) -> Vec<F> {
         r1cs_get_test_z(input)
@@ -122,13 +135,13 @@
     #[test]
     fn test_eval_ccs_relation() {
         let ccs = get_test_ccs::<Fr>();
-        let mut z = get_test_z(3);
+        let (_, x, mut w) = get_test_z_split(3);
 
-        let f_w = ccs.eval_relation(&z).unwrap();
+        let f_w = ccs.eval_relation(&w, &x).unwrap();
         assert!(is_zero_vec(&f_w));
 
-        z[1] = Fr::from(111);
-        let f_w = ccs.eval_relation(&z).unwrap();
+        w[1] = Fr::from(111);
+        let f_w = ccs.eval_relation(&w, &x).unwrap();
         assert!(!is_zero_vec(&f_w));
     }
 
@@ -136,8 +149,8 @@ /// Test that a basic CCS relation can be satisfied
     #[test]
     fn test_check_ccs_relation() {
         let ccs = get_test_ccs::<Fr>();
-        let z = get_test_z(3);
+        let (_, x, w) = get_test_z_split(3);
 
-        ccs.check_relation(&z).unwrap();
+        ccs.check_relation(&w, &x).unwrap();
     }
 }

@@ -1,28 +1,156 @@
-use ark_ff::PrimeField;
+use ark_ec::CurveGroup;
+use ark_relations::r1cs::SynthesisError;
+use ark_std::rand::RngCore;
 
-use crate::Error;
+use crate::{commitment::CommitmentScheme, folding::traits::Dummy, Error};
 
 pub mod ccs;
 pub mod r1cs;
 
-pub trait Arith<F: PrimeField> {
-    /// Evaluate the given Arith structure at `z`, a vector of assignments, and
-    /// return the evaluation.
-    fn eval_relation(&self, z: &[F]) -> Result<Vec<F>, Error>;
+/// `Arith` defines the operations that a constraint system (e.g., R1CS, CCS,
+/// etc.) should support.
+///
+/// Here, `W` is the type of witness, and `U` is the type of statement / public
+/// input / public IO / instance.
+/// Note that the same constraint system may support different types of `W` and
+/// `U`, and the satisfiability check may vary.
+///
+/// For example, both plain R1CS and relaxed R1CS are represented by 3 matrices,
+/// but the types of `W` and `U` are different:
+/// - The plain R1CS has `W` and `U` as vectors of field elements.
+///   
+///   `W = w` and `U = x` satisfy R1CS if `Az ∘ Bz = Cz`, where `z = [1, x, w]`.
+///
+/// - In Nova, Relaxed R1CS has `W` as [`crate::folding::nova::Witness`],
+///   and `U` as [`crate::folding::nova::CommittedInstance`].
+///  
+///   `W = (w, e, ...)` and `U = (u, x, ...)` satisfy Relaxed R1CS if
+///   `Az ∘ Bz = uCz + e`, where `z = [u, x, w]`.
+///   (commitments in `U` are not checked here)
+///
+///   Also, `W` and `U` have non-native field elements as their components when
+///   used as CycleFold witness and instance.
+///
+/// - In ProtoGalaxy, Relaxed R1CS has `W` as [`crate::folding::protogalaxy::Witness`],
+///   and `U` as [`crate::folding::protogalaxy::CommittedInstance`].
+///    
+///   `W = (w, ...)` and `U = (x, e, β, ...)` satisfy Relaxed R1CS if
+///   `e = Σ pow_i(β) v_i`, where `v = Az ∘ Bz - Cz`, `z = [1, x, w]`.
+///   (commitments in `U` are not checked here)
+///
+/// This is also the case of CCS, where `W` and `U` may be vectors of field
+/// elements, [`crate::folding::hypernova::Witness`] and [`crate::folding::hypernova::lcccs::LCCCS`],
+/// or [`crate::folding::hypernova::Witness`] and [`crate::folding::hypernova::cccs::CCCS`].
+pub trait Arith<W, U>: Clone {
+    type Evaluation;
 
-    /// Checks that the given Arith structure is satisfied by a z vector, i.e.,
-    /// if the evaluation is a zero vector
+    /// Returns a dummy witness and instance
+    fn dummy_witness_instance<'a>(&'a self) -> (W, U)
+    where
+        W: Dummy<&'a Self>,
+        U: Dummy<&'a Self>,
+    {
+        (W::dummy(self), U::dummy(self))
+    }
+
+    /// Evaluates the constraint system `self` at witness `w` and instance `u`.
+    /// Returns the evaluation result.
+    ///
+    /// The evaluation result is usually a vector of field elements.
+    /// For instance:
+    /// - Evaluating the plain R1CS at `W = w` and `U = x` returns
+    ///   `Az ∘ Bz - Cz`, where `z = [1, x, w]`.
+    ///
+    /// - Evaluating the relaxed R1CS in Nova at `W = (w, e, ...)` and
+    ///   `U = (u, x, ...)` returns `Az ∘ Bz - uCz`, where `z = [u, x, w]`.
+    ///
+    /// - Evaluating the relaxed R1CS in ProtoGalaxy at `W = (w, ...)` and
+    ///   `U = (x, e, β, ...)` returns `Az ∘ Bz - Cz`, where `z = [1, x, w]`.
+    ///
+    /// However, we use `Self::Evaluation` to represent the evaluation result
+    /// for future extensibility.
+    fn eval_relation(&self, w: &W, u: &U) -> Result<Self::Evaluation, Error>;
+
+    /// Checks if the evaluation result is valid. The witness `w` and instance
+    /// `u` are also parameters, because the validity check may need information
+    /// contained in `w` and/or `u`.
+    ///
+    /// For instance:
+    /// - The evaluation `v` of plain R1CS at satisfying `W` and `U` should be
+    ///   an all-zero vector.
+    ///
+    /// - The evaluation `v` of relaxed R1CS in Nova at satisfying `W` and `U`
+    ///   should be equal to the error term `e` in the witness.
+    ///
+    /// - The evaluation `v` of relaxed R1CS in ProtoGalaxy at satisfying `W`
+    ///   and `U` should satisfy `e = Σ pow_i(β) v_i`, where `e` is the error
+    ///   term in the committed instance.
+    fn check_evaluation(w: &W, u: &U, v: Self::Evaluation) -> Result<(), Error>;
+
+    /// Checks if witness `w` and instance `u` satisfy the constraint system
+    /// `self` by first computing the evaluation result and then checking the
+    /// validity of the evaluation result.
     ///
     /// Used only for testing.
-    fn check_relation(&self, z: &[F]) -> Result<(), Error> {
-        if self.eval_relation(z)?.iter().all(|f| f.is_zero()) {
-            Ok(())
-        } else {
-            Err(Error::NotSatisfied)
-        }
+    fn check_relation(&self, w: &W, u: &U) -> Result<(), Error> {
+        let e = self.eval_relation(w, u)?;
+        Self::check_evaluation(w, u, e)
     }
+}
 
+/// `ArithSerializer` is for serializing constraint systems.
+///
+/// Currently we only support converting parameters to bytes, but in the future
+/// we may consider implementing methods for serializing the actual data (e.g.,
+/// R1CS matrices).
+pub trait ArithSerializer {
     /// Returns the bytes that represent the parameters, that is, the matrices sizes, the amount of
     /// public inputs, etc, without the matrices/polynomials values.
     fn params_to_le_bytes(&self) -> Vec<u8>;
 }
+
+/// `ArithSampler` allows sampling random pairs of witness and instance that
+/// satisfy the constraint system `self`.
+///
+/// This is useful for constructing a zero-knowledge layer for a folding-based
+/// IVC.
+/// An example of such a layer can be found in Appendix D of the [HyperNova]
+/// paper.
+///
+/// Note that we use a separate trait for sampling, because this operation may
+/// not be supported by all witness-instance pairs.
+/// For instance, it is difficult (if not impossible) to do this for `w` and `x`
+/// in a plain R1CS.
+///
+/// [HyperNova]: https://eprint.iacr.org/2023/573.pdf
+pub trait ArithSampler<C: CurveGroup, W, U>: Arith<W, U> {
+    /// Samples a random witness and instance that satisfy the constraint system.
+    fn sample_witness_instance<CS: CommitmentScheme<C, true>>(
+        &self,
+        params: &CS::ProverParams,
+        rng: impl RngCore,
+    ) -> Result<(W, U), Error>;
+}
+
+/// `ArithGadget` defines the in-circuit counterparts of operations specified in
+/// `Arith` on constraint systems.
+pub trait ArithGadget<WVar, UVar> {
+    type Evaluation;
+
+    /// Evaluates the constraint system `self` at witness `w` and instance `u`.
+    /// Returns the evaluation result.
+    fn eval_relation(&self, w: &WVar, u: &UVar) -> Result<Self::Evaluation, SynthesisError>;
+
+    /// Generates constraints for enforcing that witness `w` and instance `u`
+    /// satisfy the constraint system `self` by first computing the evaluation
+    /// result and then checking the validity of the evaluation result.
+    fn enforce_relation(&self, w: &WVar, u: &UVar) -> Result<(), SynthesisError> {
+        let e = self.eval_relation(w, u)?;
+        Self::enforce_evaluation(w, u, e)
+    }
+
+    /// Generates constraints for enforcing that the evaluation result is valid.
+    /// The witness `w` and instance `u` are also parameters, because the
+    /// validity check may need information contained in `w` and/or `u`.
+    fn enforce_evaluation(w: &WVar, u: &UVar, e: Self::Evaluation) -> Result<(), SynthesisError>;
+}

@@ -1,13 +1,13 @@
-use crate::commitment::CommitmentScheme;
-use crate::RngCore;
-use ark_ec::CurveGroup;
 use ark_ff::PrimeField;
 use ark_relations::r1cs::ConstraintSystem;
 use ark_serialize::{CanonicalDeserialize, CanonicalSerialize};
 use ark_std::rand::Rng;
 
-use super::Arith;
-use crate::utils::vec::{hadamard, mat_vec_mul, vec_scalar_mul, vec_sub, SparseMatrix};
+use super::ccs::CCS;
+use super::{Arith, ArithSerializer};
+use crate::utils::vec::{
+    hadamard, is_zero_vec, mat_vec_mul, vec_scalar_mul, vec_sub, SparseMatrix,
+};
 use crate::Error;
 
 #[derive(Debug, Clone, Eq, PartialEq, CanonicalSerialize, CanonicalDeserialize)]
@@ -18,8 +18,9 @@ pub B: SparseMatrix<F>,
     pub C: SparseMatrix<F>,
 }
 
-impl<F: PrimeField> Arith<F> for R1CS<F> {
-    fn eval_relation(&self, z: &[F]) -> Result<Vec<F>, Error> {
+impl<F: PrimeField> R1CS<F> {
+    /// Evaluates the CCS relation at a given vector of variables `z`
+    pub fn eval_at_z(&self, z: &[F]) -> Result<Vec<F>, Error> {
         if z.len() != self.A.n_cols {
             return Err(Error::NotSameLength(
                 "z.len()".to_string(),
@@ -33,12 +34,26 @@ let Az = mat_vec_mul(&self.A, z)?;
         let Bz = mat_vec_mul(&self.B, z)?;
         let Cz = mat_vec_mul(&self.C, z)?;
         // Multiply Cz by z[0] (u) here, allowing this method to be reused for
-        // both relaxed and unrelaxed R1CS.
+        // both relaxed and plain R1CS.
         let uCz = vec_scalar_mul(&Cz, &z[0]);
         let AzBz = hadamard(&Az, &Bz)?;
         vec_sub(&AzBz, &uCz)
     }
+}
 
+impl<F: PrimeField, W: AsRef<[F]>, U: AsRef<[F]>> Arith<W, U> for R1CS<F> {
+    type Evaluation = Vec<F>;
+
+    fn eval_relation(&self, w: &W, u: &U) -> Result<Self::Evaluation, Error> {
+        self.eval_at_z(&[&[F::one()], u.as_ref(), w.as_ref()].concat())
+    }
+
+    fn check_evaluation(_w: &W, _u: &U, e: Self::Evaluation) -> Result<(), Error> {
+        is_zero_vec(&e).then_some(()).ok_or(Error::NotSatisfied)
+    }
+}
+
+impl<F: PrimeField> ArithSerializer for R1CS<F> {
     fn params_to_le_bytes(&self) -> Vec<u8> {
         [
             self.l.to_le_bytes(),
@@ -67,66 +82,41 @@ C: SparseMatrix::rand(rng, n_rows, n_cols),
         }
     }
 
-    /// returns a tuple containing (w, x) (witness and public inputs respectively)
-    pub fn split_z(&self, z: &[F]) -> (Vec<F>, Vec<F>) {
-        (z[self.l + 1..].to_vec(), z[1..self.l + 1].to_vec())
+    #[inline]
+    pub fn num_constraints(&self) -> usize {
+        self.A.n_rows
     }
-}
-
-pub trait RelaxedR1CS<C: CurveGroup, W, U>: Arith<C::ScalarField> {
-    /// returns a dummy running instance (Witness and CommittedInstance) for the current R1CS structure
-    fn dummy_running_instance(&self) -> (W, U);
-
-    /// returns a dummy incoming instance (Witness and CommittedInstance) for the current R1CS structure
-    fn dummy_incoming_instance(&self) -> (W, U);
 
-    /// checks if the given instance is relaxed
-    fn is_relaxed(w: &W, u: &U) -> bool;
-
-    /// extracts `z`, the vector of variables, from the given Witness and CommittedInstance
-    fn extract_z(w: &W, u: &U) -> Vec<C::ScalarField>;
-
-    /// checks if the computed error terms correspond to the actual one in `w`
-    /// or `u`
-    fn check_error_terms(w: &W, u: &U, e: Vec<C::ScalarField>) -> Result<(), Error>;
+    #[inline]
+    pub fn num_public_inputs(&self) -> usize {
+        self.l
+    }
 
-    /// checks the tight (unrelaxed) R1CS relation
-    fn check_tight_relation(&self, w: &W, u: &U) -> Result<(), Error> {
-        if Self::is_relaxed(w, u) {
-            return Err(Error::R1CSUnrelaxedFail);
-        }
+    #[inline]
+    pub fn num_variables(&self) -> usize {
+        self.A.n_cols
+    }
 
-        let z = Self::extract_z(w, u);
-        self.check_relation(&z)
+    #[inline]
+    pub fn num_witnesses(&self) -> usize {
+        self.num_variables() - self.num_public_inputs() - 1
     }
 
-    /// checks the relaxed R1CS relation
-    fn check_relaxed_relation(&self, w: &W, u: &U) -> Result<(), Error> {
-        let z = Self::extract_z(w, u);
-        let e = self.eval_relation(&z)?;
-        Self::check_error_terms(w, u, e)
+    /// returns a tuple containing (w, x) (witness and public inputs respectively)
+    pub fn split_z(&self, z: &[F]) -> (Vec<F>, Vec<F>) {
+        (z[self.l + 1..].to_vec(), z[1..self.l + 1].to_vec())
     }
-
-    // Computes the E term, given A, B, C, z, u
-    fn compute_E(
-        A: &SparseMatrix<C::ScalarField>,
-        B: &SparseMatrix<C::ScalarField>,
-        C: &SparseMatrix<C::ScalarField>,
-        z: &[C::ScalarField],
-        u: &C::ScalarField,
-    ) -> Result<Vec<C::ScalarField>, Error> {
-        let Az = mat_vec_mul(A, z)?;
-        let Bz = mat_vec_mul(B, z)?;
-        let AzBz = hadamard(&Az, &Bz)?;
+}
 
-        let Cz = mat_vec_mul(C, z)?;
-        let uCz = vec_scalar_mul(&Cz, u);
-        vec_sub(&AzBz, &uCz)
+impl<F: PrimeField> From<CCS<F>> for R1CS<F> {
+    fn from(ccs: CCS<F>) -> Self {
+        R1CS::<F> {
+            l: ccs.l,
+            A: ccs.M[0].clone(),
+            B: ccs.M[1].clone(),
+            C: ccs.M[2].clone(),
+        }
     }
-
-    fn sample<CS>(&self, params: &CS::ProverParams, rng: impl RngCore) -> Result<(W, U), Error>
-    where
-        CS: CommitmentScheme<C, true>;
 }
 
 /// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format as R1CS
@@ -173,27 +163,12 @@
 #[cfg(test)]
 pub mod tests {
     use super::*;
-    use crate::folding::nova::{CommittedInstance, Witness};
-    use crate::{
-        commitment::pedersen::Pedersen,
-        utils::vec::{
-            is_zero_vec,
-            tests::{to_F_matrix, to_F_vec},
-        },
+    use crate::utils::vec::{
+        is_zero_vec,
+        tests::{to_F_matrix, to_F_vec},
     };
 
-    use ark_pallas::{Fr, Projective};
-
-    #[test]
-    pub fn sample_relaxed_r1cs() {
-        let rng = rand::rngs::OsRng;
-        let r1cs = get_test_r1cs::<Fr>();
-        let (prover_params, _) = Pedersen::<Projective>::setup(rng, r1cs.A.n_rows).unwrap();
-
-        let sampled: Result<(Witness<Projective>, CommittedInstance<Projective>), _> =
-            r1cs.sample::<Pedersen<Projective, true>>(&prover_params, rng);
-        assert!(sampled.is_ok());
-    }
+    use ark_pallas::Fr;
 
     pub fn get_test_r1cs<F: PrimeField>() -> R1CS<F> {
         // R1CS for: x^3 + x + 5 = y (example from article
@@ -252,20 +227,20 @@ #[test]
     fn test_eval_r1cs_relation() {
         let mut rng = ark_std::test_rng();
         let r1cs = get_test_r1cs::<Fr>();
-        let mut z = get_test_z::<Fr>(rng.gen::<u16>() as usize);
+        let (_, x, mut w) = get_test_z_split::<Fr>(rng.gen::<u16>() as usize);
 
-        let f_w = r1cs.eval_relation(&z).unwrap();
+        let f_w = r1cs.eval_relation(&w, &x).unwrap();
         assert!(is_zero_vec(&f_w));
 
-        z[1] = Fr::from(111);
-        let f_w = r1cs.eval_relation(&z).unwrap();
+        w[1] = Fr::from(111);
+        let f_w = r1cs.eval_relation(&w, &x).unwrap();
         assert!(!is_zero_vec(&f_w));
     }
 
     #[test]
     fn test_check_r1cs_relation() {
         let r1cs = get_test_r1cs::<Fr>();
-        let z = get_test_z(5);
-        r1cs.check_relation(&z).unwrap();
+        let (_, x, w) = get_test_z_split(5);
+        r1cs.check_relation(&w, &x).unwrap();
     }
 }

@@ -3,20 +3,17 @@ use ark_ec::CurveGroup;
 use ark_ff::PrimeField;
 use ark_serialize::CanonicalDeserialize;
 use ark_serialize::CanonicalSerialize;
-use ark_std::One;
-use ark_std::Zero;
-use std::sync::Arc;
-
-use ark_std::rand::Rng;
+use ark_std::{rand::Rng, sync::Arc, One, Zero};
 
 use super::circuits::CCCSVar;
 use super::Witness;
 use crate::arith::{ccs::CCS, Arith};
 use crate::commitment::CommitmentScheme;
-use crate::folding::traits::CommittedInstanceOps;
+use crate::folding::circuits::CF1;
+use crate::folding::traits::{CommittedInstanceOps, Dummy};
 use crate::transcript::AbsorbNonNative;
 use crate::utils::mle::dense_vec_to_dense_mle;
-use crate::utils::vec::mat_vec_mul;
+use crate::utils::vec::{is_zero_vec, mat_vec_mul};
 use crate::utils::virtual_polynomial::{build_eq_x_r_vec, VirtualPolynomial};
 use crate::Error;
 
@@ -93,34 +90,34 @@ Ok(Q)
     }
 }
 
-impl<C: CurveGroup> CCCS<C> {
-    pub fn dummy(l: usize) -> CCCS<C>
-    where
-        C::ScalarField: PrimeField,
-    {
-        CCCS::<C> {
+impl<C: CurveGroup> Dummy<&CCS<CF1<C>>> for CCCS<C> {
+    fn dummy(ccs: &CCS<CF1<C>>) -> Self {
+        Self {
             C: C::zero(),
-            x: vec![C::ScalarField::zero(); l],
+            x: vec![CF1::<C>::zero(); ccs.l],
         }
     }
+}
+
+impl<C: CurveGroup> Arith<Witness<CF1<C>>, CCCS<C>> for CCS<CF1<C>> {
+    type Evaluation = Vec<CF1<C>>;
+
+    fn eval_relation(&self, w: &Witness<CF1<C>>, u: &CCCS<C>) -> Result<Self::Evaluation, Error> {
+        // evaluate CCCS relation
+        self.eval_at_z(&[&[CF1::<C>::one()][..], &u.x, &w.w].concat())
+    }
 
     /// Perform the check of the CCCS instance described at section 4.1,
     /// notice that this method does not check the commitment correctness
-    pub fn check_relation(
-        &self,
-        ccs: &CCS<C::ScalarField>,
-        w: &Witness<C::ScalarField>,
+    fn check_evaluation(
+        _w: &Witness<CF1<C>>,
+        _u: &CCCS<C>,
+        e: Self::Evaluation,
     ) -> Result<(), Error> {
-        // check CCCS relation
-        let z: Vec<C::ScalarField> =
-            [vec![C::ScalarField::one()], self.x.clone(), w.w.to_vec()].concat();
-
         // A CCCS relation is satisfied if the q(x) multivariate polynomial evaluates to zero in
         // the hypercube, evaluating over the whole boolean hypercube for a normal-sized instance
         // would take too much, this checks the CCS relation of the CCCS.
-        ccs.check_relation(&z)?;
-
-        Ok(())
+        is_zero_vec(&e).then_some(()).ok_or(Error::NotSatisfied)
     }
 }
 
@@ -193,7 +190,8 @@ let mut rng = test_rng();
 
         let ccs: CCS<Fr> = get_test_ccs();
         let z = get_test_z(3);
-        ccs.check_relation(&z).unwrap();
+        let (w, x) = ccs.split_z(&z);
+        ccs.check_relation(&w, &x).unwrap();
 
         let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
 
@@ -227,7 +225,8 @@ let mut rng = test_rng();
 
         let ccs: CCS<Fr> = get_test_ccs();
         let z = get_test_z(3);
-        ccs.check_relation(&z).unwrap();
+        let (w, x) = ccs.split_z(&z);
+        ccs.check_relation(&w, &x).unwrap();
 
         // Now test that if we create Q(x) with eq(d,y) where d is inside the hypercube, \sum Q(x) should be G(d) which
         // should be equal to q(d), since G(x) interpolates q(x) inside the hypercube

@@ -42,7 +42,7 @@ utils::EqEvalGadget,
         CF1, CF2,
     },
     nova::get_r1cs_from_cs,
-    traits::CommittedInstanceVarOps,
+    traits::{CommittedInstanceVarOps, Dummy},
 };
 use crate::frontend::FCircuit;
 use crate::utils::virtual_polynomial::VPAuxInfo;
@@ -602,13 +602,13 @@ /// For a stable FCircuit circuit, the CCS parameters can be computed in advance and can be
     /// feed in as parameter for the AugmentedFCircuit::empty method to avoid computing them there.
     pub fn upper_bound_ccs(&self) -> Result<CCS<C1::ScalarField>, Error> {
         let r1cs = get_r1cs_from_cs::<CF1<C1>>(self.clone()).unwrap();
-        let mut ccs = CCS::from_r1cs(r1cs.clone());
+        let mut ccs = CCS::from(r1cs);
 
         let z_0 = vec![C1::ScalarField::zero(); self.F.state_len()];
         let mut W_i = Witness::<C1::ScalarField>::dummy(&ccs);
-        let mut U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
+        let mut U_i = LCCCS::<C1>::dummy(&ccs);
         let mut w_i = W_i.clone();
-        let mut u_i = CCCS::<C1>::dummy(ccs.l);
+        let mut u_i = CCCS::<C1>::dummy(&ccs);
 
         let n_iters = 2;
         for _ in 0..n_iters {
@@ -674,7 +674,7 @@ w: r1cs_w_i1.clone(),
                 r_w: C1::ScalarField::one(),
             };
             W_i = Witness::<C1::ScalarField>::dummy(&ccs);
-            U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
+            U_i = LCCCS::<C1>::dummy(&ccs);
         }
         Ok(ccs)
 
@@ -691,7 +691,7 @@ self.clone().generate_constraints(cs.clone())?;
         cs.finalize();
         let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?;
         let r1cs = extract_r1cs::<C1::ScalarField>(&cs);
-        let ccs = CCS::from_r1cs(r1cs.clone());
+        let ccs = CCS::from(r1cs);
 
         Ok((cs, ccs))
     }
@@ -734,8 +734,8 @@ .external_inputs
                 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
         })?;
 
-        let U_dummy = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
-        let u_dummy = CCCS::<C1>::dummy(self.ccs.l);
+        let U_dummy = LCCCS::<C1>::dummy(&self.ccs);
+        let u_dummy = CCCS::<C1>::dummy(&self.ccs);
 
         let U_i =
             LCCCSVar::<C1>::new_witness(cs.clone(), || Ok(self.U_i.unwrap_or(U_dummy.clone())))?;
@@ -748,7 +748,7 @@ })?;
         let U_i1_C = NonNativeAffineVar::new_witness(cs.clone(), || {
             Ok(self.U_i1_C.unwrap_or_else(C1::zero))
         })?;
-        let nimfs_proof_dummy = NIMFSProof::<C1>::dummy(&self.ccs, MU, NU);
+        let nimfs_proof_dummy = NIMFSProof::<C1>::dummy((&self.ccs, MU, NU));
         let nimfs_proof = ProofVar::<C1>::new_witness(cs.clone(), || {
             Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy))
         })?;
@@ -906,7 +906,8 @@ use super::*;
     use crate::{
         arith::{
             ccs::tests::{get_test_ccs, get_test_z},
-            r1cs::{extract_w_x, RelaxedR1CS},
+            r1cs::extract_w_x,
+            Arith,
         },
         commitment::{pedersen::Pedersen, CommitmentScheme},
         folding::{
@@ -1100,7 +1101,7 @@ .unwrap();
         assert_eq!(folded_lcccs, folded_lcccs_v);
 
         // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
-        folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
+        ccs.check_relation(&folded_witness, &folded_lcccs).unwrap();
 
         // allocate circuit inputs
         let cs = ConstraintSystem::<Fr>::new_ref();
@@ -1248,13 +1249,13 @@ let mut z_i = z_0.clone();
 
         // prepare the dummy instances
         let W_dummy = Witness::<Fr>::dummy(&ccs);
-        let U_dummy = LCCCS::<Projective>::dummy(ccs.l, ccs.t, ccs.s);
+        let U_dummy = LCCCS::<Projective>::dummy(&ccs);
         let w_dummy = W_dummy.clone();
-        let u_dummy = CCCS::<Projective>::dummy(ccs.l);
+        let u_dummy = CCCS::<Projective>::dummy(&ccs);
         let (cf_W_dummy, cf_U_dummy): (
             CycleFoldWitness<Projective2>,
             CycleFoldCommittedInstance<Projective2>,
-        ) = cf_r1cs.dummy_running_instance();
+        ) = cf_r1cs.dummy_witness_instance();
 
         // set the initial dummy instances
         let mut W_i = W_dummy.clone();
@@ -1289,7 +1290,7 @@ let (U_i1, W_i1);
 
             if i == 0 {
                 W_i1 = Witness::<Fr>::dummy(&ccs);
-                U_i1 = LCCCS::dummy(ccs.l, ccs.t, ccs.s);
+                U_i1 = LCCCS::dummy(&ccs);
 
                 let u_i1_x = U_i1.hash(&sponge, pp_hash, Fr::one(), &z_0, &z_i1);
 
@@ -1346,7 +1347,7 @@ )
                 .unwrap();
 
                 // sanity check: check the folded instance relation
-                U_i1.check_relation(&ccs, &W_i1).unwrap();
+                ccs.check_relation(&W_i1, &U_i1).unwrap();
 
                 let u_i1_x = U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), &z_0, &z_i1);
 
@@ -1465,7 +1466,7 @@ // assign them directly to w_i, u_i.
             (u_i, w_i) = ccs
                 .to_cccs::<_, _, Pedersen<Projective>, false>(&mut rng, &pedersen_params, &r1cs_z)
                 .unwrap();
-            u_i.check_relation(&ccs, &w_i).unwrap();
+            ccs.check_relation(&w_i, &u_i).unwrap();
 
             // sanity checks
             assert_eq!(w_i.w, r1cs_w_i1);
@@ -1486,12 +1487,12 @@ U_i = U_i1.clone();
             W_i = W_i1.clone();
 
             // check the new LCCCS instance relation
-            U_i.check_relation(&ccs, &W_i).unwrap();
+            ccs.check_relation(&W_i, &U_i).unwrap();
             // check the new CCCS instance relation
-            u_i.check_relation(&ccs, &w_i).unwrap();
+            ccs.check_relation(&w_i, &u_i).unwrap();
 
             // check the CycleFold instance relation
-            cf_r1cs.check_relaxed_relation(&cf_W_i, &cf_U_i).unwrap();
+            cf_r1cs.check_relation(&cf_W_i, &cf_U_i).unwrap();
 
             println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
         }

@@ -38,8 +38,10 @@ gadgets::{eval_mle, MatrixGadget, SparseMatrixVar},
     vec::poly_from_vec,
 };
 use crate::Error;
-use crate::{arith::ccs::CCS, folding::traits::CommittedInstanceVarOps};
-use crate::{arith::r1cs::R1CS, folding::traits::WitnessVarOps};
+use crate::{
+    arith::{ccs::CCS, r1cs::R1CS},
+    folding::traits::{CommittedInstanceVarOps, Dummy, WitnessVarOps},
+};
 
 /// In-circuit representation of the Witness associated to the CommittedInstance.
 #[derive(Debug, Clone)]
@@ -292,8 +294,8 @@ let z_i = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
             Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
         })?;
 
-        let U_dummy_native = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
-        let u_dummy_native = CCCS::<C1>::dummy(self.ccs.l);
+        let U_dummy_native = LCCCS::<C1>::dummy(&self.ccs);
+        let u_dummy_native = CCCS::<C1>::dummy(&self.ccs);
         let w_dummy_native = Witness::<C1::ScalarField>::new(
             vec![C1::ScalarField::zero(); self.ccs.n - 3 /* (3=2+1, since u_i.x.len=2) */],
         );
@@ -311,7 +313,7 @@ })?;
         let W_i1 = WitnessVar::<C1::ScalarField>::new_witness(cs.clone(), || {
             Ok(self.W_i1.unwrap_or(w_dummy_native.clone()))
         })?;
-        let nimfs_proof_dummy = NIMFSProof::<C1>::dummy(&self.ccs, 1, 1); // mu=1 & nu=1 because the last fold is 2-to-1
+        let nimfs_proof_dummy = NIMFSProof::<C1>::dummy((&self.ccs, 1, 1)); // mu=1 & nu=1 because the last fold is 2-to-1
         let nimfs_proof = NIMFSProofVar::<C1>::new_witness(cs.clone(), || {
             Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy))
         })?;
@@ -373,10 +375,7 @@ use ark_r1cs_std::ToBitsGadget;
 
             let cf_u_dummy_native =
                 CycleFoldCommittedInstance::<C2>::dummy(NovaCycleFoldConfig::<C1>::IO_LEN);
-            let cf_w_dummy_native = CycleFoldWitness::<C2>::dummy(
-                self.cf_r1cs.A.n_cols - 1 - self.cf_r1cs.l,
-                self.cf_E_len,
-            );
+            let cf_w_dummy_native = CycleFoldWitness::<C2>::dummy(&self.cf_r1cs);
             let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
                 Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
             })?;
@@ -527,7 +526,7 @@ let mut rng = test_rng();
         let n_rows = 2_u32.pow(5) as usize;
         let n_cols = 2_u32.pow(5) as usize;
         let r1cs = R1CS::<Fr>::rand(&mut rng, n_rows, n_cols);
-        let ccs = CCS::from_r1cs(r1cs);
+        let ccs = CCS::from(r1cs);
         let z: Vec<Fr> = (0..n_cols).map(|_| Fr::rand(&mut rng)).collect();
 
         let (pedersen_params, _) =

@@ -11,8 +11,10 @@
 use super::circuits::LCCCSVar;
 use super::Witness;
 use crate::arith::ccs::CCS;
+use crate::arith::Arith;
 use crate::commitment::CommitmentScheme;
-use crate::folding::traits::CommittedInstanceOps;
+use crate::folding::circuits::CF1;
+use crate::folding::traits::{CommittedInstanceOps, Dummy};
 use crate::transcript::AbsorbNonNative;
 use crate::utils::mle::dense_vec_to_dense_mle;
 use crate::utils::vec::mat_vec_mul;
@@ -80,42 +82,41 @@ ))
     }
 }
 
-impl<C: CurveGroup> LCCCS<C> {
-    pub fn dummy(l: usize, t: usize, s: usize) -> LCCCS<C>
-    where
-        C::ScalarField: PrimeField,
-    {
-        LCCCS::<C> {
+impl<C: CurveGroup> Dummy<&CCS<CF1<C>>> for LCCCS<C> {
+    fn dummy(ccs: &CCS<CF1<C>>) -> Self {
+        Self {
             C: C::zero(),
-            u: C::ScalarField::zero(),
-            x: vec![C::ScalarField::zero(); l],
-            r_x: vec![C::ScalarField::zero(); s],
-            v: vec![C::ScalarField::zero(); t],
+            u: CF1::<C>::zero(),
+            x: vec![CF1::<C>::zero(); ccs.l],
+            r_x: vec![CF1::<C>::zero(); ccs.s],
+            v: vec![CF1::<C>::zero(); ccs.t],
         }
     }
+}
+
+impl<C: CurveGroup> Arith<Witness<CF1<C>>, LCCCS<C>> for CCS<CF1<C>> {
+    type Evaluation = Vec<CF1<C>>;
 
     /// Perform the check of the LCCCS instance described at section 4.2,
     /// notice that this method does not check the commitment correctness
-    pub fn check_relation(
-        &self,
-        ccs: &CCS<C::ScalarField>,
-        w: &Witness<C::ScalarField>,
-    ) -> Result<(), Error> {
-        // check CCS relation
-        let z: Vec<C::ScalarField> = [vec![self.u], self.x.clone(), w.w.to_vec()].concat();
+    fn eval_relation(&self, w: &Witness<CF1<C>>, u: &LCCCS<C>) -> Result<Self::Evaluation, Error> {
+        let z = [&[u.u][..], &u.x, &w.w].concat();
 
-        let computed_v: Vec<C::ScalarField> = ccs
-            .M
+        self.M
             .iter()
             .map(|M_j| {
-                let Mz_mle = dense_vec_to_dense_mle(ccs.s, &mat_vec_mul(M_j, &z)?);
-                Mz_mle.evaluate(&self.r_x).ok_or(Error::EvaluationFail)
+                let Mz_mle = dense_vec_to_dense_mle(self.s, &mat_vec_mul(M_j, &z)?);
+                Mz_mle.evaluate(&u.r_x).ok_or(Error::EvaluationFail)
             })
-            .collect::<Result<_, Error>>()?;
-        if computed_v != self.v {
-            return Err(Error::NotSatisfied);
-        }
-        Ok(())
+            .collect()
+    }
+
+    fn check_evaluation(
+        _w: &Witness<CF1<C>>,
+        u: &LCCCS<C>,
+        e: Self::Evaluation,
+    ) -> Result<(), Error> {
+        (u.v == e).then_some(()).ok_or(Error::NotSatisfied)
     }
 }
 
@@ -203,7 +204,7 @@
         let n_rows = 2_u32.pow(5) as usize;
         let n_cols = 2_u32.pow(5) as usize;
         let r1cs = R1CS::<Fr>::rand(&mut rng, n_rows, n_cols);
-        let ccs = CCS::from_r1cs(r1cs);
+        let ccs = CCS::from(r1cs);
         let z: Vec<Fr> = (0..n_cols).map(|_| Fr::rand(&mut rng)).collect();
 
         let (pedersen_params, _) =
@@ -237,12 +238,14 @@ let mut rng = test_rng();
 
         let ccs = get_test_ccs();
         let z = get_test_z(3);
-        ccs.check_relation(&z.clone()).unwrap();
+        let (w, x) = ccs.split_z(&z);
+        ccs.check_relation(&w, &x).unwrap();
 
         // Mutate z so that the relation does not hold
         let mut bad_z = z.clone();
         bad_z[3] = Fr::zero();
-        assert!(ccs.check_relation(&bad_z.clone()).is_err());
+        let (bad_w, bad_x) = ccs.split_z(&bad_z);
+        assert!(ccs.check_relation(&bad_w, &bad_x).is_err());
 
         let (pedersen_params, _) =
             Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();

@@ -24,24 +24,27 @@ use decider_eth_circuit::WitnessVar;
 use lcccs::LCCCS;
 use nimfs::NIMFS;
 
+use crate::commitment::CommitmentScheme;
 use crate::constants::NOVA_N_BITS_RO;
-use crate::folding::circuits::{
-    cyclefold::{
-        fold_cyclefold_circuit, CycleFoldCircuit, CycleFoldCommittedInstance, CycleFoldConfig,
-        CycleFoldWitness,
+use crate::folding::{
+    circuits::{
+        cyclefold::{
+            fold_cyclefold_circuit, CycleFoldCircuit, CycleFoldCommittedInstance, CycleFoldConfig,
+            CycleFoldWitness,
+        },
+        CF2,
     },
-    CF2,
+    nova::{get_r1cs_from_cs, PreprocessorParam},
+    traits::{CommittedInstanceOps, Dummy, WitnessOps},
 };
-use crate::folding::nova::{get_r1cs_from_cs, PreprocessorParam};
-use crate::folding::traits::{CommittedInstanceOps, WitnessOps};
 use crate::frontend::FCircuit;
 use crate::utils::{get_cm_coordinates, pp_hash};
 use crate::Error;
-use crate::{arith::r1cs::RelaxedR1CS, commitment::CommitmentScheme};
 use crate::{
     arith::{
         ccs::CCS,
         r1cs::{extract_w_x, R1CS},
+        Arith,
     },
     FoldingScheme, MultiFolding,
 };
@@ -78,8 +81,11 @@ // note: at the current version, we don't use the blinding factors and we set them to 0
         // always.
         Self { w, r_w: F::zero() }
     }
-    pub fn dummy(ccs: &CCS<F>) -> Self {
-        Witness::<F>::new(vec![F::zero(); ccs.n - ccs.l - 1])
+}
+
+impl<F: PrimeField> Dummy<&CCS<F>> for Witness<F> {
+    fn dummy(ccs: &CCS<F>) -> Self {
+        Self::new(vec![F::zero(); ccs.n - ccs.l - 1])
     }
 }
 
@@ -251,7 +257,7 @@ .ccs
             .to_lcccs::<_, _, CS1, H>(&mut rng, &self.cs_pp, &r1cs_z)?;
 
         #[cfg(test)]
-        U_i.check_relation(&self.ccs, &W_i)?;
+        self.ccs.check_relation(&W_i, &U_i)?;
 
         Ok((U_i, W_i))
     }
@@ -273,7 +279,7 @@ .ccs
             .to_cccs::<_, _, CS1, H>(&mut rng, &self.cs_pp, &r1cs_z)?;
 
         #[cfg(test)]
-        u_i.check_relation(&self.ccs, &w_i)?;
+        self.ccs.check_relation(&w_i, &u_i)?;
 
         Ok((u_i, w_i))
     }
@@ -305,10 +311,10 @@ state: Vec<C1::ScalarField>,
         external_inputs: Vec<C1::ScalarField>,
     ) -> Result<Vec<C1::ScalarField>, Error> {
         // prepare the initial dummy instances
-        let U_i = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
-        let mut u_i = CCCS::<C1>::dummy(self.ccs.l);
+        let U_i = LCCCS::<C1>::dummy(&self.ccs);
+        let mut u_i = CCCS::<C1>::dummy(&self.ccs);
         let (_, cf_U_i): (CycleFoldWitness<C2>, CycleFoldCommittedInstance<C2>) =
-            self.cf_r1cs.dummy_running_instance();
+            self.cf_r1cs.dummy_witness_instance();
 
         let sponge = PoseidonSponge::<C1::ScalarField>::new(&self.poseidon_config);
 
@@ -329,7 +335,7 @@ .F
             .step_native(0, state.clone(), external_inputs.clone())?;
 
         // compute u_{i+1}.x
-        let U_i1 = LCCCS::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
+        let U_i1 = LCCCS::dummy(&self.ccs);
         let u_i1_x = U_i1.hash(
             &sponge,
             self.pp_hash,
@@ -498,11 +504,11 @@ let pp_hash = vp.pp_hash()?;
 
         // setup the dummy instances
         let W_dummy = Witness::<C1::ScalarField>::dummy(&ccs);
-        let U_dummy = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
+        let U_dummy = LCCCS::<C1>::dummy(&ccs);
         let w_dummy = W_dummy.clone();
-        let mut u_dummy = CCCS::<C1>::dummy(ccs.l);
+        let mut u_dummy = CCCS::<C1>::dummy(&ccs);
         let (cf_W_dummy, cf_U_dummy): (CycleFoldWitness<C2>, CycleFoldCommittedInstance<C2>) =
-            cf_r1cs.dummy_running_instance();
+            cf_r1cs.dummy_witness_instance();
         u_dummy.x = vec![
             U_dummy.hash(&sponge, pp_hash, C1::ScalarField::zero(), &z_0, &z_0),
             cf_U_dummy.hash_cyclefold(&sponge, pp_hash),
@@ -641,7 +647,7 @@
         if self.i == C1::ScalarField::zero() {
             W_i1 = Witness::<C1::ScalarField>::dummy(&self.ccs);
             W_i1.r_w = self.W_i.r_w;
-            U_i1 = LCCCS::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
+            U_i1 = LCCCS::dummy(&self.ccs);
 
             let u_i1_x = U_i1.hash(
                 &sponge,
@@ -697,7 +703,7 @@ )?;
 
             // sanity check: check the folded instance relation
             #[cfg(test)]
-            U_i1.check_relation(&self.ccs, &W_i1)?;
+            self.ccs.check_relation(&W_i1, &U_i1)?;
 
             let u_i1_x = U_i1.hash(
                 &sponge,
@@ -831,9 +837,9 @@
         #[cfg(test)]
         {
             // check the new LCCCS instance relation
-            self.U_i.check_relation(&self.ccs, &self.W_i)?;
+            self.ccs.check_relation(&self.W_i, &self.U_i)?;
             // check the new CCCS instance relation
-            self.u_i.check_relation(&self.ccs, &self.w_i)?;
+            self.ccs.check_relation(&self.w_i, &self.u_i)?;
         }
 
         Ok(())
@@ -899,12 +905,12 @@ return Err(Error::IVCVerificationFail);
         }
 
         // check LCCCS satisfiability
-        U_i.check_relation(&vp.ccs, &W_i)?;
+        vp.ccs.check_relation(&W_i, &U_i)?;
         // check CCCS satisfiability
-        u_i.check_relation(&vp.ccs, &w_i)?;
+        vp.ccs.check_relation(&w_i, &u_i)?;
 
         // check CycleFold's RelaxedR1CS satisfiability
-        vp.cf_r1cs.check_relaxed_relation(&cf_W_i, &cf_U_i)?;
+        vp.cf_r1cs.check_relation(&cf_W_i, &cf_U_i)?;
 
         Ok(())
     }

@@ -13,6 +13,8 @@ Witness,
 };
 use crate::arith::ccs::CCS;
 use crate::constants::NOVA_N_BITS_RO;
+use crate::folding::circuits::CF1;
+use crate::folding::traits::Dummy;
 use crate::transcript::Transcript;
 use crate::utils::sum_check::structs::{IOPProof as SumCheckProof, IOPProverMessage};
 use crate::utils::sum_check::{IOPSumCheck, SumCheck};
@@ -29,8 +31,8 @@ pub sc_proof: SumCheckProof<C::ScalarField>,
     pub sigmas_thetas: SigmasThetas<C::ScalarField>,
 }
 
-impl<C: CurveGroup> NIMFSProof<C> {
-    pub fn dummy(ccs: &CCS<C::ScalarField>, mu: usize, nu: usize) -> Self {
+impl<C: CurveGroup> Dummy<(&CCS<CF1<C>>, usize, usize)> for NIMFSProof<C> {
+    fn dummy((ccs, mu, nu): (&CCS<CF1<C>>, usize, usize)) -> Self {
         // use 'C::ScalarField::one()' instead of 'zero()' to enforce the NIMFSProof to have the
         // same in-circuit representation to match the number of constraints of an actual proof.
         NIMFSProof::<C> {
@@ -410,8 +412,10 @@ fn test_fold() {
         let ccs = get_test_ccs();
         let z1 = get_test_z::<Fr>(3);
         let z2 = get_test_z::<Fr>(4);
-        ccs.check_relation(&z1).unwrap();
-        ccs.check_relation(&z2).unwrap();
+        let (w1, x1) = ccs.split_z(&z1);
+        let (w2, x2) = ccs.split_z(&z2);
+        ccs.check_relation(&w1, &x1).unwrap();
+        ccs.check_relation(&w2, &x2).unwrap();
 
         let mut rng = test_rng();
         let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
@@ -429,8 +433,8 @@ let (cccs, w2) = ccs
             .to_cccs::<_, Projective, Pedersen<Projective>, false>(&mut rng, &pedersen_params, &z2)
             .unwrap();
 
-        lcccs.check_relation(&ccs, &w1).unwrap();
-        cccs.check_relation(&ccs, &w2).unwrap();
+        ccs.check_relation(&w1, &lcccs).unwrap();
+        ccs.check_relation(&w2, &cccs).unwrap();
 
         let mut rng = test_rng();
         let rho = Fr::rand(&mut rng);
@@ -446,7 +450,7 @@
         let w_folded = NIMFS::<Projective, PoseidonSponge<Fr>>::fold_witness(&[w1], &[w2], rho);
 
         // check lcccs relation
-        folded.check_relation(&ccs, &w_folded).unwrap();
+        ccs.check_relation(&w_folded, &folded).unwrap();
     }
 
     /// Perform multifolding of an LCCCS instance with a CCCS instance (as described in the paper)
@@ -506,7 +510,7 @@ .unwrap();
         assert_eq!(folded_lcccs, folded_lcccs_v);
 
         // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
-        folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
+        ccs.check_relation(&folded_witness, &folded_lcccs).unwrap();
     }
 
     /// Perform multiple steps of multifolding of an LCCCS instance with a CCCS instance
@@ -566,7 +570,7 @@ .unwrap();
             assert_eq!(folded_lcccs, folded_lcccs_v);
 
             // check that the folded instance with the folded witness holds the LCCCS relation
-            folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
+            ccs.check_relation(&folded_witness, &folded_lcccs).unwrap();
 
             running_instance = folded_lcccs;
             w1 = folded_witness;
@@ -652,7 +656,7 @@ .unwrap();
         assert_eq!(folded_lcccs, folded_lcccs_v);
 
         // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
-        folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
+        ccs.check_relation(&folded_witness, &folded_lcccs).unwrap();
     }
 
     /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step
@@ -740,7 +744,7 @@
             assert_eq!(folded_lcccs, folded_lcccs_v);
 
             // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
-            folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
+            ccs.check_relation(&folded_witness, &folded_lcccs).unwrap();
         }
     }
 }

@@ -230,8 +230,10 @@ fn test_compute_sigmas_thetas() {
         let ccs = get_test_ccs();
         let z1 = get_test_z(3);
         let z2 = get_test_z(4);
-        ccs.check_relation(&z1).unwrap();
-        ccs.check_relation(&z2).unwrap();
+        let (w1, x1) = ccs.split_z(&z1);
+        let (w2, x2) = ccs.split_z(&z2);
+        ccs.check_relation(&w1, &x1).unwrap();
+        ccs.check_relation(&w2, &x2).unwrap();
 
         let mut rng = test_rng();
         let gamma: Fr = Fr::rand(&mut rng);
@@ -282,8 +284,10 @@ // generate test CCS & z vectors
         let ccs: CCS<Fr> = get_test_ccs();
         let z1 = get_test_z(3);
         let z2 = get_test_z(4);
-        ccs.check_relation(&z1).unwrap();
-        ccs.check_relation(&z2).unwrap();
+        let (w1, x1) = ccs.split_z(&z1);
+        let (w2, x2) = ccs.split_z(&z2);
+        ccs.check_relation(&w1, &x1).unwrap();
+        ccs.check_relation(&w2, &x2).unwrap();
 
         let gamma: Fr = Fr::rand(&mut rng);
         let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();

@@ -31,7 +31,10 @@ CF1, CF2,
 };
 use crate::frontend::FCircuit;
 use crate::transcript::{AbsorbNonNativeGadget, Transcript, TranscriptVar};
-use crate::{constants::NOVA_N_BITS_RO, folding::traits::CommittedInstanceVarOps};
+use crate::{
+    constants::NOVA_N_BITS_RO,
+    folding::traits::{CommittedInstanceVarOps, Dummy},
+};
 
 /// CommittedInstanceVar contains the u, x, cmE and cmW values which are folded on the main Nova
 /// constraints field (E1::Fr, where E1 is the main curve). The peculiarity is that cmE and cmW are

@@ -40,7 +40,7 @@ nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
     CF1, CF2,
 };
 use crate::folding::nova::NovaCycleFoldConfig;
-use crate::folding::traits::CommittedInstanceVarOps;
+use crate::folding::traits::{CommittedInstanceVarOps, Dummy};
 use crate::frontend::FCircuit;
 use crate::utils::vec::poly_from_vec;
 use crate::Error;
@@ -214,11 +214,8 @@ let z_i = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
             Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
         })?;
 
-        let u_dummy_native = CommittedInstance::<C1>::dummy(2);
-        let w_dummy_native = Witness::<C1>::dummy(
-            self.r1cs.A.n_cols - 3, /* (3=2+1, since u_i.x.len=2) */
-            self.E_len,
-        );
+        let u_dummy_native = CommittedInstance::<C1>::dummy(&self.r1cs);
+        let w_dummy_native = Witness::<C1>::dummy(&self.r1cs);
 
         let u_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
             Ok(self.u_i.unwrap_or(u_dummy_native.clone()))
@@ -436,9 +433,8 @@ let pp_hash = FpVar::<CF1<C2>>::new_input(cs.clone(), || {
             Ok(self.pp_hash.unwrap_or_else(CF1::<C2>::zero))
         })?;
 
-        let cf_u_dummy_native = CommittedInstance::<C2>::dummy(NovaCycleFoldConfig::<C1>::IO_LEN);
-        let w_dummy_native =
-            Witness::<C2>::dummy(self.cf_r1cs.A.n_cols - 1 - self.cf_r1cs.l, self.cf_E_len);
+        let cf_u_dummy_native = CommittedInstance::<C2>::dummy(&self.cf_r1cs);
+        let w_dummy_native = Witness::<C2>::dummy(&self.cf_r1cs);
         let cf_U_i = CommittedInstanceVar::<C2>::new_input(cs.clone(), || {
             Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
         })?;

@@ -29,6 +29,7 @@ circuits::{ChallengeGadget, CommittedInstanceVar},
     nifs::NIFS,
     CommittedInstance, Nova, Witness,
 };
+use crate::commitment::{pedersen::Params as PedersenParams, CommitmentScheme};
 use crate::folding::circuits::{
     cyclefold::{CycleFoldCommittedInstance, CycleFoldWitness},
     nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
@@ -41,10 +42,9 @@ gadgets::{MatrixGadget, SparseMatrixVar, VectorGadget},
     vec::poly_from_vec,
 };
 use crate::Error;
-use crate::{arith::r1cs::R1CS, folding::traits::WitnessVarOps};
 use crate::{
-    commitment::{pedersen::Params as PedersenParams, CommitmentScheme},
-    folding::traits::CommittedInstanceVarOps,
+    arith::r1cs::R1CS,
+    folding::traits::{CommittedInstanceVarOps, Dummy, WitnessVarOps},
 };
 
 #[derive(Debug, Clone)]
@@ -356,11 +356,8 @@ let z_i = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
             Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
         })?;
 
-        let u_dummy_native = CommittedInstance::<C1>::dummy(2);
-        let w_dummy_native = Witness::<C1>::dummy(
-            self.r1cs.A.n_cols - 3, /* (3=2+1, since u_i.x.len=2) */
-            self.E_len,
-        );
+        let u_dummy_native = CommittedInstance::<C1>::dummy(&self.r1cs);
+        let w_dummy_native = Witness::<C1>::dummy(&self.r1cs);
 
         let u_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
             Ok(self.u_i.unwrap_or(u_dummy_native.clone()))
@@ -437,10 +434,7 @@ use ark_r1cs_std::ToBitsGadget;
 
             let cf_u_dummy_native =
                 CycleFoldCommittedInstance::<C2>::dummy(NovaCycleFoldConfig::<C1>::IO_LEN);
-            let w_dummy_native = CycleFoldWitness::<C2>::dummy(
-                self.cf_r1cs.A.n_cols - 1 - self.cf_r1cs.l,
-                self.cf_E_len,
-            );
+            let w_dummy_native = CycleFoldWitness::<C2>::dummy(&self.cf_r1cs);
             let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
                 Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
             })?;
@@ -608,7 +602,6 @@ use crate::arith::{
         r1cs::{
             extract_r1cs, extract_w_x,
             tests::{get_test_r1cs, get_test_z},
-            RelaxedR1CS,
         },
         Arith,
     };
@@ -618,20 +611,18 @@ use crate::frontend::utils::{CubicFCircuit, CustomFCircuit, WrapperCircuit};
     use crate::transcript::poseidon::poseidon_canonical_config;
     use crate::FoldingScheme;
 
-    fn prepare_instances<C: CurveGroup, CS: CommitmentScheme<C>, R: Rng>(
+    // Convert `z` to a witness-instance pair for the relaxed R1CS
+    fn prepare_relaxed_witness_instance<C: CurveGroup, CS: CommitmentScheme<C>, R: Rng>(
         mut rng: R,
         r1cs: &R1CS<C::ScalarField>,
         z: &[C::ScalarField],
-    ) -> (Witness<C>, CommittedInstance<C>)
-    where
-        C::ScalarField: Absorb,
-    {
+    ) -> (Witness<C>, CommittedInstance<C>) {
         let (w, x) = r1cs.split_z(z);
 
         let (cs_pp, _) = CS::setup(&mut rng, max(w.len(), r1cs.A.n_rows)).unwrap();
 
         let mut w = Witness::new::<false>(w, r1cs.A.n_rows, &mut rng);
-        w.E = r1cs.eval_relation(z).unwrap();
+        w.E = r1cs.eval_at_z(z).unwrap();
         let mut u = w.commit::<CS, false>(&cs_pp, x).unwrap();
         u.u = z[0];
 
@@ -643,9 +634,10 @@ fn test_relaxed_r1cs_small_gadget_handcrafted() {
         let rng = &mut thread_rng();
 
         let r1cs: R1CS<Fr> = get_test_r1cs();
+
         let mut z = get_test_z(3);
-        z[0] = Fr::rand(rng);
-        let (w, u) = prepare_instances::<_, Pedersen<Projective>, _>(rng, &r1cs, &z);
+        z[0] = Fr::rand(rng); // Randomize `z[0]` (i.e. `u.u`) to test the relaxed R1CS
+        let (w, u) = prepare_relaxed_witness_instance::<_, Pedersen<Projective>, _>(rng, &r1cs, &z);
 
         let cs = ConstraintSystem::<Fr>::new_ref();
 
@@ -673,12 +665,11 @@ let cs = cs.into_inner().unwrap();
 
         let r1cs = extract_r1cs::<Fr>(&cs);
         let (w, x) = extract_w_x::<Fr>(&cs);
-        let mut z = [vec![Fr::one()], x, w].concat();
-        r1cs.check_relation(&z).unwrap();
+        r1cs.check_relation(&w, &x).unwrap();
 
-        z[0] = Fr::rand(rng);
-        let (w, u) = prepare_instances::<_, Pedersen<Projective>, _>(rng, &r1cs, &z);
-        r1cs.check_relaxed_relation(&w, &u).unwrap();
+        let z = [vec![Fr::rand(rng)], x, w].concat();
+        let (w, u) = prepare_relaxed_witness_instance::<_, Pedersen<Projective>, _>(rng, &r1cs, &z);
+        r1cs.check_relation(&w, &u).unwrap();
 
         // set new CS for the circuit that checks the RelaxedR1CS of our original circuit
         let cs = ConstraintSystem::<Fr>::new_ref();
@@ -767,9 +758,10 @@ cs.finalize();
         let cs = cs.into_inner().unwrap();
         let r1cs = extract_r1cs::<Fq>(&cs);
         let (w, x) = extract_w_x::<Fq>(&cs);
+
         let z = [vec![Fq::rand(rng)], x, w].concat();
-
-        let (w, u) = prepare_instances::<_, Pedersen<Projective2>, _>(rng, &r1cs, &z);
+        let (w, u) =
+            prepare_relaxed_witness_instance::<_, Pedersen<Projective2>, _>(rng, &r1cs, &z);
 
         // natively
         let cs = ConstraintSystem::<Fq>::new_ref();

@@ -19,18 +19,21 @@ use crate::folding::circuits::cyclefold::{
     fold_cyclefold_circuit, CycleFoldCircuit, CycleFoldCommittedInstance, CycleFoldConfig,
     CycleFoldWitness,
 };
-use crate::folding::circuits::CF2;
+use crate::folding::{
+    circuits::{CF1, CF2},
+    traits::Dummy,
+};
 use crate::frontend::FCircuit;
 use crate::transcript::{poseidon::poseidon_canonical_config, AbsorbNonNative, Transcript};
 use crate::utils::vec::is_zero_vec;
 use crate::Error;
 use crate::FoldingScheme;
-use crate::{arith::r1cs::RelaxedR1CS, commitment::CommitmentScheme};
 use crate::{
     arith::r1cs::{extract_r1cs, extract_w_x, R1CS},
     constants::NOVA_N_BITS_RO,
     utils::{get_cm_coordinates, pp_hash},
 };
+use crate::{arith::Arith, commitment::CommitmentScheme};
 
 use circuits::{AugmentedFCircuit, ChallengeGadget, CommittedInstanceVar};
 use nifs::NIFS;
@@ -76,17 +79,23 @@ pub cmW: C,
     pub x: Vec<C::ScalarField>,
 }
 
-impl<C: CurveGroup> CommittedInstance<C> {
-    pub fn dummy(io_len: usize) -> Self {
+impl<C: CurveGroup> Dummy<usize> for CommittedInstance<C> {
+    fn dummy(io_len: usize) -> Self {
         Self {
             cmE: C::zero(),
-            u: C::ScalarField::zero(),
+            u: CF1::<C>::zero(),
             cmW: C::zero(),
-            x: vec![C::ScalarField::zero(); io_len],
+            x: vec![CF1::<C>::zero(); io_len],
         }
     }
 }
 
+impl<C: CurveGroup> Dummy<&R1CS<CF1<C>>> for CommittedInstance<C> {
+    fn dummy(r1cs: &R1CS<CF1<C>>) -> Self {
+        Self::dummy(r1cs.l)
+    }
+}
+
 impl<C: CurveGroup> Absorb for CommittedInstance<C>
 where
     C::ScalarField: Absorb,
@@ -149,18 +158,6 @@ rW,
         }
     }
 
-    pub fn dummy(w_len: usize, e_len: usize) -> Self {
-        let (rW, rE) = (C::ScalarField::zero(), C::ScalarField::zero());
-        let w = vec![C::ScalarField::zero(); w_len];
-
-        Self {
-            E: vec![C::ScalarField::zero(); e_len],
-            rE,
-            W: w,
-            rW,
-        }
-    }
-
     pub fn commit<CS: CommitmentScheme<C, HC>, const HC: bool>(
         &self,
         params: &CS::ProverParams,
@@ -180,6 +177,17 @@ })
     }
 }
 
+impl<C: CurveGroup> Dummy<&R1CS<CF1<C>>> for Witness<C> {
+    fn dummy(r1cs: &R1CS<CF1<C>>) -> Self {
+        Self {
+            E: vec![C::ScalarField::zero(); r1cs.A.n_rows],
+            rE: C::ScalarField::zero(),
+            W: vec![C::ScalarField::zero(); r1cs.A.n_cols - 1 - r1cs.l],
+            rW: C::ScalarField::zero(),
+        }
+    }
+}
+
 impl<C: CurveGroup> WitnessOps<C::ScalarField> for Witness<C> {
     type Var = WitnessVar<C>;
 
@@ -562,9 +570,9 @@ // compute the public params hash
         let pp_hash = vp.pp_hash()?;
 
         // setup the dummy instances
-        let (W_dummy, U_dummy) = r1cs.dummy_running_instance();
-        let (w_dummy, u_dummy) = r1cs.dummy_incoming_instance();
-        let (cf_W_dummy, cf_U_dummy) = cf_r1cs.dummy_running_instance();
+        let (W_dummy, U_dummy) = r1cs.dummy_witness_instance();
+        let (w_dummy, u_dummy) = r1cs.dummy_witness_instance();
+        let (cf_W_dummy, cf_U_dummy) = cf_r1cs.dummy_witness_instance();
 
         // W_dummy=W_0 is a 'dummy witness', all zeroes, but with the size corresponding to the
         // R1CS that we're working with.
@@ -815,10 +823,11 @@ self.cf_U_i = cf_U_i1;
 
             #[cfg(test)]
             {
-                self.cf_r1cs.check_tight_relation(&_cfW_w_i, &cfW_u_i)?;
-                self.cf_r1cs.check_tight_relation(&_cfE_w_i, &cfE_u_i)?;
-                self.cf_r1cs
-                    .check_relaxed_relation(&self.cf_W_i, &self.cf_U_i)?;
+                cfW_u_i.check_incoming()?;
+                cfE_u_i.check_incoming()?;
+                self.cf_r1cs.check_relation(&_cfW_w_i, &cfW_u_i)?;
+                self.cf_r1cs.check_relation(&_cfE_w_i, &cfE_u_i)?;
+                self.cf_r1cs.check_relation(&self.cf_W_i, &self.cf_U_i)?;
             }
         }
 
@@ -850,8 +859,9 @@ self.U_i = U_i1;
 
         #[cfg(test)]
         {
-            self.r1cs.check_tight_relation(&self.w_i, &self.u_i)?;
-            self.r1cs.check_relaxed_relation(&self.W_i, &self.U_i)?;
+            self.u_i.check_incoming()?;
+            self.r1cs.check_relation(&self.w_i, &self.u_i)?;
+            self.r1cs.check_relation(&self.W_i, &self.U_i)?;
         }
 
         Ok(())
@@ -917,13 +927,15 @@ if expected_cf_u_i_x != u_i.x[1] {
             return Err(Error::IVCVerificationFail);
         }
 
-        // check R1CS satisfiability, which also enforces u_i.cmE==0, u_i.u==1
-        vp.r1cs.check_tight_relation(&w_i, &u_i)?;
+        // check R1CS satisfiability, which is equivalent to checking if `u_i`
+        // is an incoming instance and if `w_i` and `u_i` satisfy RelaxedR1CS
+        u_i.check_incoming()?;
+        vp.r1cs.check_relation(&w_i, &u_i)?;
         // check RelaxedR1CS satisfiability
-        vp.r1cs.check_relaxed_relation(&W_i, &U_i)?;
+        vp.r1cs.check_relation(&W_i, &U_i)?;
 
         // check CycleFold RelaxedR1CS satisfiability
-        vp.cf_r1cs.check_relaxed_relation(&cf_W_i, &cf_U_i)?;
+        vp.cf_r1cs.check_relation(&cf_W_i, &cf_U_i)?;
 
         Ok(())
     }

@@ -210,13 +210,16 @@ use ark_ff::{BigInteger, PrimeField};
     use ark_pallas::{Fr, Projective};
     use ark_std::{ops::Mul, test_rng, UniformRand};
 
-    use crate::arith::r1cs::{
-        tests::{get_test_r1cs, get_test_z},
-        RelaxedR1CS,
-    };
     use crate::commitment::pedersen::{Params as PedersenParams, Pedersen};
     use crate::folding::nova::circuits::ChallengeGadget;
     use crate::transcript::poseidon::poseidon_canonical_config;
+    use crate::{
+        arith::{
+            r1cs::tests::{get_test_r1cs, get_test_z},
+            Arith,
+        },
+        folding::traits::Dummy,
+    };
 
     #[allow(clippy::type_complexity)]
     pub(crate) fn prepare_simple_fold_inputs<C>() -> (
@@ -302,13 +305,13 @@ #[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);
+        let (_, x1) = r1cs.split_z(&z1);
 
         let mut rng = ark_std::test_rng();
         let (pedersen_params, _) = Pedersen::<Projective>::setup(&mut rng, r1cs.A.n_cols).unwrap();
 
         // dummy instance, witness and public inputs zeroes
-        let w_dummy = Witness::<Projective>::dummy(w1.len(), r1cs.A.n_rows);
+        let w_dummy = Witness::<Projective>::dummy(&r1cs);
         let mut u_dummy = w_dummy
             .commit::<Pedersen<Projective>, false>(&pedersen_params, vec![Fr::zero(); x1.len()])
             .unwrap();
@@ -318,8 +321,8 @@ let w_i = w_dummy.clone();
         let u_i = u_dummy.clone();
         let W_i = w_dummy.clone();
         let U_i = u_dummy.clone();
-        r1cs.check_relaxed_relation(&w_i, &u_i).unwrap();
-        r1cs.check_relaxed_relation(&W_i, &U_i).unwrap();
+        r1cs.check_relation(&w_i, &u_i).unwrap();
+        r1cs.check_relation(&W_i, &U_i).unwrap();
 
         let r_Fr = Fr::from(3_u32);
 
@@ -336,7 +339,7 @@ let (W_i1, U_i1) = NIFS::<Projective, Pedersen<Projective>>::fold_instances(
             r_Fr, &w_i, &u_i, &W_i, &U_i, &T, cmT,
         )
         .unwrap();
-        r1cs.check_relaxed_relation(&W_i1, &U_i1).unwrap();
+        r1cs.check_relation(&W_i1, &U_i1).unwrap();
     }
 
     // fold 2 instances into one
@@ -350,9 +353,9 @@ let ci3_v = NIFS::<Projective, Pedersen<Projective>>::verify(r, &ci1, &ci2, &cmT);
         assert_eq!(ci3_v, ci3);
 
         // check that relations hold for the 2 inputted instances and the folded one
-        r1cs.check_relaxed_relation(&w1, &ci1).unwrap();
-        r1cs.check_relaxed_relation(&w2, &ci2).unwrap();
-        r1cs.check_relaxed_relation(&w3, &ci3).unwrap();
+        r1cs.check_relation(&w1, &ci1).unwrap();
+        r1cs.check_relation(&w2, &ci2).unwrap();
+        r1cs.check_relation(&w3, &ci3).unwrap();
 
         // check that folded commitments from folded instance (ci) are equal to folding the
         // use folded rE, rW to commit w3
@@ -427,7 +430,7 @@ let mut running_committed_instance = running_instance_w
             .commit::<Pedersen<Projective>, false>(&pedersen_params, x)
             .unwrap();
 
-        r1cs.check_relaxed_relation(&running_instance_w, &running_committed_instance)
+        r1cs.check_relation(&running_instance_w, &running_committed_instance)
             .unwrap();
 
         let num_iters = 10;
@@ -440,7 +443,7 @@ Witness::<Projective>::new::<false>(w.clone(), r1cs.A.n_rows, test_rng());
             let incoming_committed_instance = incoming_instance_w
                 .commit::<Pedersen<Projective>, false>(&pedersen_params, x)
                 .unwrap();
-            r1cs.check_relaxed_relation(&incoming_instance_w, &incoming_committed_instance)
+            r1cs.check_relation(&incoming_instance_w, &incoming_committed_instance)
                 .unwrap();
 
             let r = Fr::rand(&mut rng); // folding challenge would come from the RO
@@ -474,7 +477,7 @@ &incoming_committed_instance,
                 &cmT,
             );
 
-            r1cs.check_relaxed_relation(&folded_w, &folded_committed_instance)
+            r1cs.check_relation(&folded_w, &folded_committed_instance)
                 .unwrap();
 
             // set running_instance for next loop iteration

@@ -1,50 +1,66 @@
 use ark_ec::CurveGroup;
-use ark_std::{rand::RngCore, One, UniformRand};
+use ark_std::{rand::RngCore, UniformRand};
 
 use super::{CommittedInstance, Witness};
-use crate::arith::r1cs::{RelaxedR1CS, R1CS};
+use crate::arith::ArithSampler;
+use crate::arith::{r1cs::R1CS, Arith};
+use crate::commitment::CommitmentScheme;
+use crate::folding::circuits::CF1;
 use crate::Error;
 
-impl<C: CurveGroup> RelaxedR1CS<C, Witness<C>, CommittedInstance<C>> for R1CS<C::ScalarField> {
-    fn dummy_running_instance(&self) -> (Witness<C>, CommittedInstance<C>) {
-        let w_len = self.A.n_cols - 1 - self.l;
-        let w_dummy = Witness::<C>::dummy(w_len, self.A.n_rows);
-        let u_dummy = CommittedInstance::<C>::dummy(self.l);
-        (w_dummy, u_dummy)
-    }
+/// Implements `Arith` for R1CS, where the witness is of type [`Witness`], and
+/// the committed instance is of type [`CommittedInstance`].
+///
+/// Due to the error terms `Witness.E` and `CommittedInstance.u`, R1CS here is
+/// considered as a relaxed R1CS.
+///
+/// One may wonder why we do not provide distinct structs for R1CS and relaxed
+/// R1CS.
+/// This is because both plain R1CS and relaxed R1CS have the same structure:
+/// they are both represented by three matrices.
+/// What makes them different is the error terms, which are not part of the R1CS
+/// struct, but are part of the witness and committed instance.
+///
+/// As a follow-up, one may further ask why not providing a trait for relaxed
+/// R1CS and implement it for the `R1CS` struct, where the relaxed R1CS trait
+/// has methods for relaxed satisfiability check, while the `Arith` trait that
+/// `R1CS` implements has methods for plain satisfiability check.
+/// However, it would be more ideal if we have a single method that can smartly
+/// choose the type of satisfiability check, which would make the code more
+/// generic and easier to maintain.
+///
+/// This is achieved thanks to the new design of the [`Arith`] trait, where we
+/// can implement the trait for the same constraint system with different types
+/// of witnesses and committed instances.
+/// For R1CS, whether it is relaxed or not is now determined by the types of `W`
+/// and `U`: the satisfiability check is relaxed if `W` and `U` are defined by
+/// folding schemes, and plain if they are vectors of field elements.
+impl<C: CurveGroup> Arith<Witness<C>, CommittedInstance<C>> for R1CS<CF1<C>> {
+    type Evaluation = Vec<CF1<C>>;
 
-    fn dummy_incoming_instance(&self) -> (Witness<C>, CommittedInstance<C>) {
-        self.dummy_running_instance()
-    }
-
-    fn is_relaxed(_w: &Witness<C>, u: &CommittedInstance<C>) -> bool {
-        u.cmE != C::zero() || u.u != C::ScalarField::one()
+    fn eval_relation(
+        &self,
+        w: &Witness<C>,
+        u: &CommittedInstance<C>,
+    ) -> Result<Self::Evaluation, Error> {
+        self.eval_at_z(&[&[u.u][..], &u.x, &w.W].concat())
     }
 
-    fn extract_z(w: &Witness<C>, u: &CommittedInstance<C>) -> Vec<C::ScalarField> {
-        [&[u.u][..], &u.x, &w.W].concat()
-    }
-
-    fn check_error_terms(
+    fn check_evaluation(
         w: &Witness<C>,
         _u: &CommittedInstance<C>,
-        e: Vec<C::ScalarField>,
+        e: Self::Evaluation,
     ) -> Result<(), Error> {
-        if w.E == e {
-            Ok(())
-        } else {
-            Err(Error::NotSatisfied)
-        }
+        (w.E == e).then_some(()).ok_or(Error::NotSatisfied)
     }
+}
 
-    fn sample<CS>(
+impl<C: CurveGroup> ArithSampler<C, Witness<C>, CommittedInstance<C>> for R1CS<CF1<C>> {
+    fn sample_witness_instance<CS: CommitmentScheme<C, true>>(
         &self,
         params: &CS::ProverParams,
         mut rng: impl RngCore,
-    ) -> Result<(Witness<C>, CommittedInstance<C>), Error>
-    where
-        CS: crate::commitment::CommitmentScheme<C, true>,
-    {
+    ) -> Result<(Witness<C>, CommittedInstance<C>), Error> {
         // Implements sampling a (committed) RelaxedR1CS
         // See construction 5 in https://eprint.iacr.org/2023/573.pdf
         let u = C::ScalarField::rand(&mut rng);
@@ -61,16 +77,7 @@ let mut z = vec![u];
         z.extend(&x);
         z.extend(&W);
 
-        let E = <Self as RelaxedR1CS<C, Witness<C>, CommittedInstance<C>>>::compute_E(
-            &self.A, &self.B, &self.C, &z, &u,
-        )?;
-
-        debug_assert!(
-            z.len() == self.A.n_cols,
-            "Length of z is {}, while A has {} columns.",
-            z.len(),
-            self.A.n_cols
-        );
+        let E = self.eval_at_z(&z)?;
 
         let witness = Witness { E, rE, W, rW };
         let mut cm_witness = witness.commit::<CS, true>(params, x)?;
@@ -79,7 +86,7 @@ // witness.commit() sets u to 1, we set it to the sampled u value
         cm_witness.u = u;
 
         debug_assert!(
-            self.check_relaxed_relation(&witness, &cm_witness).is_ok(),
+            self.check_relation(&witness, &cm_witness).is_ok(),
             "Sampled a non satisfiable relaxed R1CS, sampled u: {}, computed E: {:?}",
             u,
             witness.E

@@ -35,7 +35,7 @@ use ark_ff::{BigInteger, PrimeField};
 use ark_std::{One, Zero};
 
 use crate::{
-    arith::r1cs::{RelaxedR1CS, R1CS},
+    arith::{r1cs::R1CS, Arith, ArithSampler},
     folding::traits::CommittedInstanceOps,
     RngCore,
 };
@@ -142,7 +142,9 @@ // d. Store folding proof
         let pi = FoldingProof { cmT };
 
         // 2. Sample a satisfying relaxed R1CS instance-witness pair (W_r, U_r)
-        let (W_r, U_r) = nova.r1cs.sample::<CS1>(&nova.cs_pp, &mut rng)?;
+        let (W_r, U_r) = nova
+            .r1cs
+            .sample_witness_instance::<CS1>(&nova.cs_pp, &mut rng)?;
 
         // 3. Fold the instance-witness pair (U_f, W_f) with (U_r, W_r)
         // a. Compute T
@@ -279,10 +281,10 @@ &proof.pi_prime.cmT,
         );
 
         // 5. Check that W^{\prime}_i is a satisfying witness
-        r1cs.check_relaxed_relation(&proof.W_i_prime, &U_i_prime)?;
+        r1cs.check_relation(&proof.W_i_prime, &U_i_prime)?;
 
         // 6. Check that the cyclefold instance-witness pair satisfies the cyclefold relaxed r1cs
-        cf_r1cs.check_relaxed_relation(&proof.cf_W_i, &proof.cf_U_i)?;
+        cf_r1cs.check_relation(&proof.cf_W_i, &proof.cf_U_i)?;
 
         Ok(())
     }
@@ -370,7 +372,7 @@ 3,
         );
         let (_, sampled_committed_instance) = nova
             .r1cs
-            .sample::<Pedersen<Projective, true>>(&nova.cs_pp, rng)
+            .sample_witness_instance::<Pedersen<Projective, true>>(&nova.cs_pp, rng)
             .unwrap();
 
         // proof verification fails with incorrect running instance
@@ -407,7 +409,7 @@ 3,
         );
         let (sampled_committed_witness, _) = nova
             .r1cs
-            .sample::<Pedersen<Projective, true>>(&nova.cs_pp, rng)
+            .sample_witness_instance::<Pedersen<Projective, true>>(&nova.cs_pp, rng)
             .unwrap();
 
         // proof generation fails with incorrect running witness

@@ -33,7 +33,7 @@ },
             nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
             CF1, CF2,
         },
-        traits::CommittedInstanceVarOps,
+        traits::{CommittedInstanceVarOps, Dummy},
     },
     frontend::FCircuit,
     transcript::{AbsorbNonNativeGadget, TranscriptVar},
@@ -47,13 +47,13 @@ #[allow(clippy::type_complexity)]
     pub fn fold_committed_instance<C: CurveGroup, S: CryptographicSponge>(
         transcript: &mut impl TranscriptVar<C::ScalarField, S>,
         // running instance
-        instance: &CommittedInstanceVar<C>,
+        instance: &CommittedInstanceVar<C, true>,
         // incoming instances
-        vec_instances: &[CommittedInstanceVar<C>],
+        vec_instances: &[CommittedInstanceVar<C, false>],
         // polys from P
         F_coeffs: Vec<FpVar<C::ScalarField>>,
         K_coeffs: Vec<FpVar<C::ScalarField>>,
-    ) -> Result<(CommittedInstanceVar<C>, Vec<FpVar<C::ScalarField>>), SynthesisError> {
+    ) -> Result<(CommittedInstanceVar<C, true>, Vec<FpVar<C::ScalarField>>), SynthesisError> {
         let t = instance.betas.len();
 
         // absorb the committed instances
@@ -135,13 +135,13 @@ impl AugmentationGadget {
     #[allow(clippy::type_complexity)]
     pub fn prepare_and_fold_primary<C: CurveGroup, S: CryptographicSponge>(
         transcript: &mut impl TranscriptVar<CF1<C>, S>,
-        U: CommittedInstanceVar<C>,
+        U: CommittedInstanceVar<C, true>,
         u_phis: Vec<NonNativeAffineVar<C>>,
         u_xs: Vec<Vec<FpVar<CF1<C>>>>,
         new_U_phi: NonNativeAffineVar<C>,
         F_coeffs: Vec<FpVar<CF1<C>>>,
         K_coeffs: Vec<FpVar<CF1<C>>>,
-    ) -> Result<(CommittedInstanceVar<C>, Vec<FpVar<CF1<C>>>), SynthesisError> {
+    ) -> Result<(CommittedInstanceVar<C, true>, Vec<FpVar<CF1<C>>>), SynthesisError> {
         assert_eq!(u_phis.len(), u_xs.len());
 
         // Prepare the incoming instances.
@@ -250,7 +250,7 @@ pub(super) z_i: Vec<CF1<C1>>,
     pub(super) external_inputs: Vec<CF1<C1>>,
     pub(super) F: FC, // F circuit
     pub(super) u_i_phi: C1,
-    pub(super) U_i: CommittedInstance<C1>,
+    pub(super) U_i: CommittedInstance<C1, true>,
     pub(super) U_i1_phi: C1,
     pub(super) F_coeffs: Vec<CF1<C1>>,
     pub(super) K_coeffs: Vec<CF1<C1>>,
@@ -278,7 +278,7 @@ t: usize,
         d: usize,
         k: usize,
     ) -> Self {
-        let u_dummy = CommittedInstance::dummy_running(2, t);
+        let u_dummy = CommittedInstance::dummy((2, t));
         let cf_u_dummy =
             CycleFoldCommittedInstance::dummy(ProtoGalaxyCycleFoldConfig::<C1>::IO_LEN);
 
@@ -327,8 +327,8 @@ let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || Ok(self.z_i))?;
         let external_inputs =
             Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || Ok(self.external_inputs))?;
 
-        let u_dummy = CommittedInstance::<C1>::dummy_running(2, self.U_i.betas.len());
-        let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || Ok(self.U_i))?;
+        let u_dummy = CommittedInstance::<C1, true>::dummy((2, self.U_i.betas.len()));
+        let U_i = CommittedInstanceVar::<C1, true>::new_witness(cs.clone(), || Ok(self.U_i))?;
         let u_i_phi = NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.u_i_phi))?;
         let U_i1_phi = NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.U_i1_phi))?;
         let phi_stars =

@@ -0,0 +1,4 @@
+/// `RUNNING` indicates that the committed instance is a running instance.
+pub const RUNNING: bool = true;
+/// `INCOMING` indicates that the committed instance is an incoming instance.
+pub const INCOMING: bool = false;

@@ -14,9 +14,7 @@ use super::utils::{all_powers, betas_star, exponential_powers, pow_i};
 use super::ProtoGalaxyError;
 use super::{CommittedInstance, Witness};
 
-#[cfg(test)]
-use crate::arith::r1cs::RelaxedR1CS;
-use crate::arith::{r1cs::R1CS, Arith};
+use crate::arith::r1cs::R1CS;
 use crate::transcript::Transcript;
 use crate::utils::vec::*;
 use crate::Error;
@@ -38,14 +36,14 @@ pub fn prove(
         transcript: &mut impl Transcript<C::ScalarField>,
         r1cs: &R1CS<C::ScalarField>,
         // running instance
-        instance: &CommittedInstance<C>,
+        instance: &CommittedInstance<C, true>,
         w: &Witness<C::ScalarField>,
         // incoming instances
-        vec_instances: &[CommittedInstance<C>],
+        vec_instances: &[CommittedInstance<C, false>],
         vec_w: &[Witness<C::ScalarField>],
     ) -> Result<
         (
-            CommittedInstance<C>,
+            CommittedInstance<C, true>,
             Witness<C::ScalarField>,
             Vec<C::ScalarField>, // F_X coeffs
             Vec<C::ScalarField>, // K_X coeffs
@@ -97,7 +95,7 @@
         let delta = transcript.get_challenge();
         let deltas = exponential_powers(delta, t);
 
-        let mut f_z = r1cs.eval_relation(&z)?;
+        let mut f_z = r1cs.eval_at_z(&z)?;
         if f_z.len() != m {
             return Err(Error::NotSameLength(
                 "number of constraints in R1CS".to_string(),
@@ -127,15 +125,18 @@
         // sanity check: check that the new randomized instance (the original instance but with
         // 'refreshed' randomness) satisfies the relation.
         #[cfg(test)]
-        r1cs.check_relaxed_relation(
-            w,
-            &CommittedInstance {
-                phi: instance.phi,
-                betas: betas_star.clone(),
-                e: F_alpha,
-                x: instance.x.clone(),
-            },
-        )?;
+        {
+            use crate::arith::Arith;
+            r1cs.check_relation(
+                w,
+                &CommittedInstance::<_, true> {
+                    phi: instance.phi,
+                    betas: betas_star.clone(),
+                    e: F_alpha,
+                    x: instance.x.clone(),
+                },
+            )?;
+        }
 
         let zs: Vec<Vec<C::ScalarField>> = std::iter::once(z.clone())
             .chain(
@@ -178,7 +179,7 @@ for (j, zj) in z.iter().enumerate() {
                     inner[j] += Lh * zj;
                 }
             }
-            let f_ev = r1cs.eval_relation(&inner)?;
+            let f_ev = r1cs.eval_at_z(&inner)?;
 
             G_evals[hi] = cfg_into_iter!(f_ev)
                 .enumerate()
@@ -253,13 +254,13 @@ /// implements the non-interactive Verifier from the folding scheme described in section 4
     pub fn verify(
         transcript: &mut impl Transcript<C::ScalarField>,
         // running instance
-        instance: &CommittedInstance<C>,
+        instance: &CommittedInstance<C, true>,
         // incoming instances
-        vec_instances: &[CommittedInstance<C>],
+        vec_instances: &[CommittedInstance<C, false>],
         // polys from P
         F_coeffs: Vec<C::ScalarField>,
         K_coeffs: Vec<C::ScalarField>,
-    ) -> Result<CommittedInstance<C>, Error> {
+    ) -> Result<CommittedInstance<C, true>, Error> {
         let t = instance.betas.len();
 
         // absorb the committed instances
@@ -395,6 +396,7 @@ use ark_pallas::{Fr, Projective};
     use ark_std::{rand::Rng, UniformRand};
 
     use crate::arith::r1cs::tests::{get_test_r1cs, get_test_z_split};
+    use crate::arith::Arith;
     use crate::commitment::{pedersen::Pedersen, CommitmentScheme};
     use crate::transcript::poseidon::poseidon_canonical_config;
 
@@ -419,9 +421,9 @@ pub fn prepare_inputs<C: CurveGroup>(
         k: usize,
     ) -> (
         Witness<C::ScalarField>,
-        CommittedInstance<C>,
+        CommittedInstance<C, true>,
         Vec<Witness<C::ScalarField>>,
-        Vec<CommittedInstance<C>>,
+        Vec<CommittedInstance<C, false>>,
     ) {
         let mut rng = ark_std::test_rng();
 
@@ -439,7 +441,7 @@ w,
             r_w: C::ScalarField::zero(),
         };
         let phi = Pedersen::<C>::commit(&pedersen_params, &witness.w, &witness.r_w).unwrap();
-        let instance = CommittedInstance::<C> {
+        let instance = CommittedInstance::<C, true> {
             phi,
             betas: betas.clone(),
             e: C::ScalarField::zero(),
@@ -447,7 +449,7 @@ x,
         };
         // same for the other instances
         let mut witnesses: Vec<Witness<C::ScalarField>> = Vec::new();
-        let mut instances: Vec<CommittedInstance<C>> = Vec::new();
+        let mut instances: Vec<CommittedInstance<C, false>> = Vec::new();
         #[allow(clippy::needless_range_loop)]
         for _ in 0..k {
             let (_, x_i, w_i) = get_test_z_split::<C::ScalarField>(rng.gen::<u16>() as usize);
@@ -457,7 +459,7 @@ r_w: C::ScalarField::zero(),
             };
             let phi_i =
                 Pedersen::<C>::commit(&pedersen_params, &witness_i.w, &witness_i.r_w).unwrap();
-            let instance_i = CommittedInstance::<C> {
+            let instance_i = CommittedInstance::<C, false> {
                 phi: phi_i,
                 betas: vec![],
                 e: C::ScalarField::zero(),
@@ -509,7 +511,7 @@ assert_eq!(folded_instance.e, folded_instance_v.e);
         assert!(!folded_instance.e.is_zero());
 
         // check that the folded instance satisfies the relation
-        r1cs.check_relaxed_relation(&folded_witness, &folded_instance)
+        r1cs.check_relation(&folded_witness, &folded_instance)
             .unwrap();
     }
 
@@ -558,7 +560,7 @@
             assert!(!folded_instance.e.is_zero());
 
             // check that the folded instance satisfies the relation
-            r1cs.check_relaxed_relation(&folded_witness, &folded_instance)
+            r1cs.check_relation(&folded_witness, &folded_instance)
                 .unwrap();
 
             running_witness = folded_witness;

@@ -18,10 +18,14 @@ };
 use ark_std::{
     borrow::Borrow, cmp::max, fmt::Debug, log2, marker::PhantomData, rand::RngCore, One, Zero,
 };
+use constants::{INCOMING, RUNNING};
 use num_bigint::BigUint;
 
 use crate::{
-    arith::r1cs::{extract_r1cs, extract_w_x, RelaxedR1CS, R1CS},
+    arith::{
+        r1cs::{extract_r1cs, extract_w_x, R1CS},
+        Arith,
+    },
     commitment::CommitmentScheme,
     folding::circuits::{
         cyclefold::{
@@ -37,6 +41,7 @@ Error, FoldingScheme,
 };
 
 pub mod circuits;
+pub mod constants;
 pub mod folding;
 pub mod traits;
 pub(crate) mod utils;
@@ -44,7 +49,9 @@
 use circuits::AugmentedFCircuit;
 use folding::Folding;
 
-use super::traits::{CommittedInstanceOps, CommittedInstanceVarOps, WitnessOps, WitnessVarOps};
+use super::traits::{
+    CommittedInstanceOps, CommittedInstanceVarOps, Dummy, WitnessOps, WitnessVarOps,
+};
 
 /// Configuration for ProtoGalaxy's CycleFold circuit
 pub struct ProtoGalaxyCycleFoldConfig<C: CurveGroup> {
@@ -62,51 +69,68 @@ /// CycleFold circuit for computing random linear combinations of group elements
 /// in ProtoGalaxy instances.
 pub type ProtoGalaxyCycleFoldCircuit<C, GC> = CycleFoldCircuit<ProtoGalaxyCycleFoldConfig<C>, GC>;
 
+/// The committed instance of ProtoGalaxy.
+///
+/// We use `TYPE` to distinguish between incoming and running instances, as
+/// they have slightly different structures (e.g., length of `betas`) and
+/// behaviors (e.g., in satisfiability checks).
 #[derive(Clone, Debug, PartialEq, Eq)]
-pub struct CommittedInstance<C: CurveGroup> {
+pub struct CommittedInstance<C: CurveGroup, const TYPE: bool> {
     phi: C,
     betas: Vec<C::ScalarField>,
     e: C::ScalarField,
     x: Vec<C::ScalarField>,
 }
 
-impl<C: CurveGroup> CommittedInstance<C> {
-    pub fn dummy_running(io_len: usize, t: usize) -> Self {
+impl<C: CurveGroup, const TYPE: bool> Dummy<(usize, usize)> for CommittedInstance<C, TYPE> {
+    fn dummy((io_len, t): (usize, usize)) -> Self {
+        if TYPE == INCOMING {
+            assert_eq!(t, 0);
+        }
         Self {
             phi: C::zero(),
-            betas: vec![C::ScalarField::zero(); t],
-            e: C::ScalarField::zero(),
-            x: vec![C::ScalarField::zero(); io_len],
+            betas: vec![Zero::zero(); t],
+            e: Zero::zero(),
+            x: vec![Zero::zero(); io_len],
         }
     }
+}
 
-    pub fn dummy_incoming(io_len: usize) -> Self {
-        Self::dummy_running(io_len, 0)
+impl<C: CurveGroup, const TYPE: bool> Dummy<&R1CS<CF1<C>>> for CommittedInstance<C, TYPE> {
+    fn dummy(r1cs: &R1CS<CF1<C>>) -> Self {
+        let t = if TYPE == RUNNING {
+            log2(r1cs.num_constraints()) as usize
+        } else {
+            0
+        };
+        Self::dummy((r1cs.num_public_inputs(), t))
     }
 }
 
-impl<C: CurveGroup> CommittedInstanceOps<C> for CommittedInstance<C> {
-    type Var = CommittedInstanceVar<C>;
+impl<C: CurveGroup, const TYPE: bool> CommittedInstanceOps<C> for CommittedInstance<C, TYPE> {
+    type Var = CommittedInstanceVar<C, TYPE>;
 
     fn get_commitments(&self) -> Vec<C> {
         vec![self.phi]
     }
 
     fn is_incoming(&self) -> bool {
-        self.e == Zero::zero() && self.betas.is_empty()
+        TYPE == INCOMING
     }
 }
 
 #[derive(Clone, Debug)]
-pub struct CommittedInstanceVar<C: CurveGroup> {
+pub struct CommittedInstanceVar<C: CurveGroup, const TYPE: bool> {
     phi: NonNativeAffineVar<C>,
     betas: Vec<FpVar<C::ScalarField>>,
     e: FpVar<C::ScalarField>,
     x: Vec<FpVar<C::ScalarField>>,
 }
 
-impl<C: CurveGroup> AllocVar<CommittedInstance<C>, C::ScalarField> for CommittedInstanceVar<C> {
-    fn new_variable<T: Borrow<CommittedInstance<C>>>(
+impl<C: CurveGroup, const TYPE: bool> AllocVar<CommittedInstance<C, TYPE>, C::ScalarField>
+    for CommittedInstanceVar<C, TYPE>
+{
+    fn new_variable<T: Borrow<CommittedInstance<C, TYPE>>>(
         cs: impl Into<Namespace<C::ScalarField>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
         mode: AllocationMode,
@@ -119,15 +143,19 @@
             Ok(Self {
                 phi: NonNativeAffineVar::new_variable(cs.clone(), || Ok(u.phi), mode)?,
                 betas: Vec::new_variable(cs.clone(), || Ok(u.betas.clone()), mode)?,
-                e: FpVar::new_variable(cs.clone(), || Ok(u.e), mode)?,
+                e: if TYPE == RUNNING {
+                    FpVar::new_variable(cs.clone(), || Ok(u.e), mode)?
+                } else {
+                    FpVar::zero()
+                },
                 x: Vec::new_variable(cs.clone(), || Ok(u.x.clone()), mode)?,
             })
         })
     }
 }
 
-impl<C: CurveGroup> R1CSVar<C::ScalarField> for CommittedInstanceVar<C> {
-    type Value = CommittedInstance<C>;
+impl<C: CurveGroup, const TYPE: bool> R1CSVar<C::ScalarField> for CommittedInstanceVar<C, TYPE> {
+    type Value = CommittedInstance<C, TYPE>;
 
     fn cs(&self) -> ConstraintSystemRef<C::ScalarField> {
         self.phi
@@ -151,7 +179,7 @@ })
     }
 }
 
-impl<C: CurveGroup> CommittedInstanceVarOps<C> for CommittedInstanceVar<C> {
+impl<C: CurveGroup, const TYPE: bool> CommittedInstanceVarOps<C> for CommittedInstanceVar<C, TYPE> {
     type PointVar = NonNativeAffineVar<C>;
 
     fn get_commitments(&self) -> Vec<Self::PointVar> {
@@ -163,11 +191,13 @@ &self.x
     }
 
     fn enforce_incoming(&self) -> Result<(), SynthesisError> {
-        if self.betas.is_empty() {
-            self.e.enforce_equal(&FpVar::zero())
-        } else {
-            Err(SynthesisError::Unsatisfiable)
-        }
+        // We don't need to check if `self` is an incoming instance in-circuit,
+        // because incoming instances and running instances already have
+        // different types of `e` (constant vs witness) when we allocate them
+        // in-circuit.
+        (TYPE == INCOMING)
+            .then_some(())
+            .ok_or(SynthesisError::Unsatisfiable)
     }
 
     fn enforce_partial_equal(&self, other: &Self) -> Result<(), SynthesisError> {
@@ -195,9 +225,9 @@ pub fn commit<CS: CommitmentScheme<C>, C: CurveGroup<ScalarField = F>>(
         &self,
         params: &CS::ProverParams,
         x: Vec<F>,
-    ) -> Result<CommittedInstance<C>, crate::Error> {
+    ) -> Result<CommittedInstance<C, false>, crate::Error> {
         let phi = CS::commit(params, &self.w, &self.r_w)?;
-        Ok(CommittedInstance {
+        Ok(CommittedInstance::<C, false> {
             phi,
             x,
             e: F::zero(),
@@ -206,6 +236,15 @@ })
     }
 }
 
+impl<F: PrimeField> Dummy<&R1CS<F>> for Witness<F> {
+    fn dummy(r1cs: &R1CS<F>) -> Self {
+        Self {
+            w: vec![F::zero(); r1cs.num_witnesses()],
+            r_w: F::zero(),
+        }
+    }
+}
+
 impl<F: PrimeField> WitnessOps<F> for Witness<F> {
     type Var = WitnessVar<F>;
 
@@ -357,9 +396,9 @@ /// current i-th state
     pub z_i: Vec<C1::ScalarField>,
     /// ProtoGalaxy instances
     pub w_i: Witness<C1::ScalarField>,
-    pub u_i: CommittedInstance<C1>,
+    pub u_i: CommittedInstance<C1, false>,
     pub W_i: Witness<C1::ScalarField>,
-    pub U_i: CommittedInstance<C1>,
+    pub U_i: CommittedInstance<C1, true>,
 
     /// CycleFold running instance
     pub cf_W_i: CycleFoldWitness<C2>,
@@ -492,9 +531,10 @@ {
     type PreprocessorParam = (PoseidonConfig<CF1<C1>>, FC);
     type ProverParam = ProverParams<C1, C2, CS1, CS2>;
     type VerifierParam = VerifierParams<C1, C2, CS1, CS2>;
-    type RunningInstance = (CommittedInstance<C1>, Witness<C1::ScalarField>);
-    type IncomingInstance = (CommittedInstance<C1>, Witness<C1::ScalarField>);
-    type MultiCommittedInstanceWithWitness = (CommittedInstance<C1>, Witness<C1::ScalarField>);
+    type RunningInstance = (CommittedInstance<C1, true>, Witness<C1::ScalarField>);
+    type IncomingInstance = (CommittedInstance<C1, false>, Witness<C1::ScalarField>);
+    type MultiCommittedInstanceWithWitness =
+        (CommittedInstance<C1, false>, Witness<C1::ScalarField>);
     type CFInstance = (CycleFoldCommittedInstance<C2>, CycleFoldWitness<C2>);
 
     fn preprocess(
@@ -560,9 +600,9 @@ // compute the public params hash
         let pp_hash = vp.pp_hash()?;
 
         // setup the dummy instances
-        let (W_dummy, U_dummy) = vp.r1cs.dummy_running_instance();
-        let (w_dummy, u_dummy) = vp.r1cs.dummy_incoming_instance();
-        let (cf_W_dummy, cf_U_dummy) = vp.cf_r1cs.dummy_running_instance();
+        let (w_dummy, u_dummy) = vp.r1cs.dummy_witness_instance();
+        let (W_dummy, U_dummy) = vp.r1cs.dummy_witness_instance();
+        let (cf_W_dummy, cf_U_dummy) = vp.cf_r1cs.dummy_witness_instance();
 
         // W_dummy=W_0 is a 'dummy witness', all zeroes, but with the size corresponding to the
         // R1CS that we're working with.
@@ -808,10 +848,11 @@ K_coeffs
                     )?,
                     U_i1
                 );
-                self.cf_r1cs.check_tight_relation(&_cf1_w_i, &cf1_u_i)?;
-                self.cf_r1cs.check_tight_relation(&_cf2_w_i, &cf2_u_i)?;
-                self.cf_r1cs
-                    .check_relaxed_relation(&self.cf_W_i, &self.cf_U_i)?;
+                cf1_u_i.check_incoming()?;
+                cf2_u_i.check_incoming()?;
+                self.cf_r1cs.check_relation(&_cf1_w_i, &cf1_u_i)?;
+                self.cf_r1cs.check_relation(&_cf2_w_i, &cf2_u_i)?;
+                self.cf_r1cs.check_relation(&self.cf_W_i, &self.cf_U_i)?;
             }
 
             self.W_i = W_i1;
@@ -846,8 +887,9 @@ self.u_i = self.w_i.commit::<CS1, C1>(&self.cs_params, x_i1)?;
 
         #[cfg(test)]
         {
-            self.r1cs.check_tight_relation(&self.w_i, &self.u_i)?;
-            self.r1cs.check_relaxed_relation(&self.W_i, &self.U_i)?;
+            self.u_i.check_incoming()?;
+            self.r1cs.check_relation(&self.w_i, &self.u_i)?;
+            self.r1cs.check_relation(&self.W_i, &self.U_i)?;
         }
 
         Ok(())
@@ -904,13 +946,15 @@ if expected_cf_u_i_x != u_i.x[1] {
             return Err(Error::IVCVerificationFail);
         }
 
-        // check R1CS satisfiability
-        vp.r1cs.check_tight_relation(&w_i, &u_i)?;
+        // check R1CS satisfiability, which is equivalent to checking if `u_i`
+        // is an incoming instance and if `w_i` and `u_i` satisfy RelaxedR1CS
+        u_i.check_incoming()?;
+        vp.r1cs.check_relation(&w_i, &u_i)?;
         // check RelaxedR1CS satisfiability
-        vp.r1cs.check_relaxed_relation(&W_i, &U_i)?;
+        vp.r1cs.check_relation(&W_i, &U_i)?;
 
         // check CycleFold RelaxedR1CS satisfiability
-        vp.cf_r1cs.check_relaxed_relation(&cf_W_i, &cf_U_i)?;
+        vp.cf_r1cs.check_relation(&cf_W_i, &cf_U_i)?;
 
         Ok(())
     }

@@ -3,18 +3,20 @@ use ark_ec::CurveGroup;
 use ark_ff::PrimeField;
 use ark_r1cs_std::{fields::fp::FpVar, uint8::UInt8, ToConstraintFieldGadget};
 use ark_relations::r1cs::SynthesisError;
-use ark_std::{cfg_iter, log2, rand::RngCore, One, Zero};
+use ark_std::{cfg_into_iter, log2, One};
 use rayon::prelude::*;
 
-use super::{utils::pow_i, CommittedInstance, CommittedInstanceVar, Witness};
+use super::{constants::RUNNING, utils::pow_i, CommittedInstance, CommittedInstanceVar, Witness};
 use crate::{
-    arith::r1cs::{RelaxedR1CS, R1CS},
+    arith::{r1cs::R1CS, Arith},
+    folding::circuits::CF1,
     transcript::AbsorbNonNative,
+    utils::vec::is_zero_vec,
     Error,
 };
 
 // Implements the trait for absorbing ProtoGalaxy's CommittedInstance.
-impl<C: CurveGroup> Absorb for CommittedInstance<C>
+impl<C: CurveGroup, const TYPE: bool> Absorb for CommittedInstance<C, TYPE>
 where
     C::ScalarField: Absorb,
 {
@@ -33,7 +35,9 @@ }
 }
 
 // Implements the trait for absorbing ProtoGalaxy's CommittedInstanceVar in-circuit.
-impl<C: CurveGroup> AbsorbGadget<C::ScalarField> for CommittedInstanceVar<C> {
+impl<C: CurveGroup, const TYPE: bool> AbsorbGadget<C::ScalarField>
+    for CommittedInstanceVar<C, TYPE>
+{
     fn to_sponge_bytes(&self) -> Result<Vec<UInt8<C::ScalarField>>, SynthesisError> {
         FpVar::batch_to_sponge_bytes(&self.to_sponge_field_elements()?)
     }
@@ -49,69 +53,49 @@ .concat())
     }
 }
 
-impl<C: CurveGroup> RelaxedR1CS<C, Witness<C::ScalarField>, CommittedInstance<C>>
-    for R1CS<C::ScalarField>
+/// Implements `Arith` for R1CS, where the witness is of type [`Witness`], and
+/// the committed instance is of type [`CommittedInstance`].
+///
+/// Due to the error term `CommittedInstance.e`, R1CS here is considered as a
+/// relaxed R1CS.
+///
+/// See `nova/traits.rs` for the rationale behind the design.
+impl<C: CurveGroup, const TYPE: bool> Arith<Witness<CF1<C>>, CommittedInstance<C, TYPE>>
+    for R1CS<CF1<C>>
 {
-    fn dummy_running_instance(&self) -> (Witness<C::ScalarField>, CommittedInstance<C>) {
-        let w_len = self.A.n_cols - 1 - self.l;
-        let w_dummy = Witness::new(vec![C::ScalarField::zero(); w_len]);
-        let u_dummy = CommittedInstance::<C>::dummy_running(self.l, log2(self.A.n_rows) as usize);
-        (w_dummy, u_dummy)
-    }
+    type Evaluation = Vec<CF1<C>>;
 
-    fn dummy_incoming_instance(&self) -> (Witness<C::ScalarField>, CommittedInstance<C>) {
-        let w_len = self.A.n_cols - 1 - self.l;
-        let w_dummy = Witness::new(vec![C::ScalarField::zero(); w_len]);
-        let u_dummy = CommittedInstance::<C>::dummy_incoming(self.l);
-        (w_dummy, u_dummy)
+    fn eval_relation(
+        &self,
+        w: &Witness<CF1<C>>,
+        u: &CommittedInstance<C, TYPE>,
+    ) -> Result<Self::Evaluation, Error> {
+        self.eval_at_z(&[&[C::ScalarField::one()][..], &u.x, &w.w].concat())
     }
 
-    fn is_relaxed(_w: &Witness<C::ScalarField>, u: &CommittedInstance<C>) -> bool {
-        u.e != C::ScalarField::zero() || !u.betas.is_empty()
-    }
-
-    fn extract_z(w: &Witness<C::ScalarField>, u: &CommittedInstance<C>) -> Vec<C::ScalarField> {
-        [&[C::ScalarField::one()][..], &u.x, &w.w].concat()
-    }
-
-    fn check_error_terms(
+    fn check_evaluation(
         _w: &Witness<C::ScalarField>,
-        u: &CommittedInstance<C>,
+        u: &CommittedInstance<C, TYPE>,
         e: Vec<C::ScalarField>,
     ) -> Result<(), Error> {
-        if u.betas.len() != log2(e.len()) as usize {
-            return Err(Error::NotSameLength(
-                "instance.betas.len()".to_string(),
-                u.betas.len(),
-                "log2(e.len())".to_string(),
-                log2(e.len()) as usize,
-            ));
-        }
+        let ok = if TYPE == RUNNING {
+            if u.betas.len() != log2(e.len()) as usize {
+                return Err(Error::NotSameLength(
+                    "instance.betas.len()".to_string(),
+                    u.betas.len(),
+                    "log2(e.len())".to_string(),
+                    log2(e.len()) as usize,
+                ));
+            }
 
-        let r = cfg_iter!(e)
-            .enumerate()
-            .map(|(i, e_i)| pow_i(i, &u.betas) * e_i)
-            .sum();
-        if u.e == r {
-            Ok(())
+            u.e == cfg_into_iter!(e)
+                .enumerate()
+                .map(|(i, e_i)| pow_i(i, &u.betas) * e_i)
+                .sum::<CF1<C>>()
         } else {
-            Err(Error::NotSatisfied)
-        }
-    }
-
-    fn sample<CS>(
-        &self,
-        _params: &CS::ProverParams,
-        _rng: impl RngCore,
-    ) -> Result<(Witness<C::ScalarField>, CommittedInstance<C>), Error>
-    where
-        CS: crate::commitment::CommitmentScheme<C, true>,
-    {
-        // Sampling a random pair of witness and committed instance is required
-        // for the zero-knowledge layer for ProtoGalaxy, which is not supported
-        // yet.
-        // Tracking issue: https://github.com/privacy-scaling-explorations/sonobe/issues/82
-        unimplemented!()
+            is_zero_vec(&e)
+        };
+        ok.then_some(()).ok_or(Error::NotSatisfied)
     }
 }
 
@@ -133,7 +117,7 @@
         let t = rng.gen::<u8>() as usize;
         let io_len = rng.gen::<u8>() as usize;
 
-        let ci = CommittedInstance::<Projective> {
+        let ci = CommittedInstance::<Projective, true> {
             phi: Projective::rand(&mut rng),
             betas: (0..t).map(|_| Fr::rand(&mut rng)).collect(),
             e: Fr::rand(&mut rng),
@@ -146,7 +130,8 @@
         let cs = ConstraintSystem::<Fr>::new_ref();
 
         let ciVar =
-            CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
+            CommittedInstanceVar::<Projective, true>::new_witness(cs.clone(), || Ok(ci.clone()))
+                .unwrap();
         let bytes_var = ciVar.to_sponge_bytes().unwrap();
         let field_elements_var = ciVar.to_sponge_field_elements().unwrap();
 

@@ -119,3 +119,13 @@ /// Returns the openings (i.e., the values being committed to and the
     /// randomness) contained in the witness.
     fn get_openings(&self) -> Vec<(&[FpVar<F>], FpVar<F>)>;
 }
+
+pub trait Dummy<Cfg> {
+    fn dummy(cfg: Cfg) -> Self;
+}
+
+impl<T: Default + Clone> Dummy<usize> for Vec<T> {
+    fn dummy(cfg: usize) -> Self {
+        vec![Default::default(); cfg]
+    }
+}

@@ -8,7 +8,7 @@ use ark_serialize::CanonicalSerialize;
 use ark_std::Zero;
 use sha3::{Digest, Sha3_256};
 
-use crate::arith::Arith;
+use crate::arith::ArithSerializer;
 use crate::commitment::CommitmentScheme;
 use crate::Error;
 
@@ -45,8 +45,8 @@ }
 
 /// returns the hash of the given public parameters of the Folding Scheme
 pub fn pp_hash<C1, C2, CS1, CS2, const H: bool>(
-    arith: &impl Arith<C1::ScalarField>,
-    cf_arith: &impl Arith<C2::ScalarField>,
+    arith: &impl ArithSerializer,
+    cf_arith: &impl ArithSerializer,
     cs_vp: &CS1::VerifierParams,
     cf_cs_vp: &CS2::VerifierParams,
     poseidon_config: &PoseidonConfig<C1::ScalarField>,