@@ -23,6 +23,7 @@
 [dev-dependencies]
 ark-pallas = {version="0.4.0", features=["r1cs"]}
 ark-vesta = {version="0.4.0"}
+ark-crypto-primitives = { version = "^0.4.0", default-features = false, features = ["crh"] }
 
 [features]
 default = ["parallel"]

@@ -1,6 +1,7 @@
 use ark_ff::PrimeField;
 
 use crate::utils::vec::*;
+use crate::Error;
 
 #[derive(Debug, Clone, Eq, PartialEq)]
 pub struct R1CS<F: PrimeField> {
@@ -9,17 +10,67 @@ pub A: SparseMatrix<F>,
     pub B: SparseMatrix<F>,
     pub C: SparseMatrix<F>,
 }
+
 impl<F: PrimeField> R1CS<F> {
     /// 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())
     }
+
+    /// check that a R1CS structure is satisfied by a z vector. Only for testing.
+    pub fn check_relation(&self, z: &[F]) -> Result<(), Error> {
+        let Az = mat_vec_mul_sparse(&self.A, z);
+        let Bz = mat_vec_mul_sparse(&self.B, z);
+        let Cz = mat_vec_mul_sparse(&self.C, z);
+        let AzBz = hadamard(&Az, &Bz);
+        assert_eq!(AzBz, Cz);
+
+        Ok(())
+    }
+
+    /// converts the R1CS instance into a RelaxedR1CS as described in
+    /// [Nova](https://eprint.iacr.org/2021/370.pdf) section 4.1.
+    pub fn relax(self) -> RelaxedR1CS<F> {
+        RelaxedR1CS::<F> {
+            l: self.l,
+            E: vec![F::zero(); self.A.n_rows],
+            A: self.A,
+            B: self.B,
+            C: self.C,
+            u: F::one(),
+        }
+    }
+}
+
+#[derive(Debug, Clone, Eq, PartialEq)]
+pub struct RelaxedR1CS<F: PrimeField> {
+    pub l: usize, // io len
+    pub A: SparseMatrix<F>,
+    pub B: SparseMatrix<F>,
+    pub C: SparseMatrix<F>,
+    pub u: F,
+    pub E: Vec<F>,
+}
+impl<F: PrimeField> RelaxedR1CS<F> {
+    /// check that a RelaxedR1CS structure is satisfied by a z vector. Only for testing.
+    pub fn check_relation(&self, z: &[F]) -> Result<(), Error> {
+        let Az = mat_vec_mul_sparse(&self.A, z);
+        let Bz = mat_vec_mul_sparse(&self.B, z);
+        let Cz = mat_vec_mul_sparse(&self.C, z);
+        let uCz = vec_scalar_mul(&Cz, &self.u);
+        let uCzE = vec_add(&uCz, &self.E);
+        let AzBz = hadamard(&Az, &Bz);
+        assert_eq!(AzBz, uCzE);
+
+        Ok(())
+    }
 }
 
 #[cfg(test)]
 pub mod tests {
     use super::*;
     use crate::utils::vec::tests::{to_F_matrix, to_F_vec};
+    use ark_pallas::Fr;
 
     pub fn get_test_r1cs<F: PrimeField>() -> R1CS<F> {
         // R1CS for: x^3 + x + 5 = y (example from article
@@ -56,5 +107,13 @@ input * input,                     // x^2
             input * input * input,             // x^2 * x
             input * input * input + input,     // x^3 + x
         ])
+    }
+
+    #[test]
+    fn test_check_relation() {
+        let r1cs = get_test_r1cs::<Fr>();
+        let z = get_test_z(5);
+        r1cs.check_relation(&z).unwrap();
+        r1cs.relax().check_relation(&z).unwrap();
     }
 }

@@ -0,0 +1,291 @@
+use ark_ec::CurveGroup;
+use ark_ff::{Field, PrimeField};
+use ark_r1cs_std::{
+    alloc::{AllocVar, AllocationMode},
+    eq::EqGadget,
+    fields::{fp::FpVar, FieldVar},
+};
+use ark_relations::r1cs::{Namespace, SynthesisError};
+use core::{borrow::Borrow, marker::PhantomData};
+
+use crate::ccs::r1cs::RelaxedR1CS;
+use crate::utils::vec::SparseMatrix;
+
+pub type ConstraintF<C> = <<C as CurveGroup>::BaseField as Field>::BasePrimeField;
+
+#[derive(Debug, Clone)]
+pub struct RelaxedR1CSGadget<F: PrimeField> {
+    _f: PhantomData<F>,
+}
+impl<F: PrimeField> RelaxedR1CSGadget<F> {
+    /// performs the RelaxedR1CS check (Az∘Bz==uCz+E)
+    pub fn check(rel_r1cs: RelaxedR1CSVar<F>, z: Vec<FpVar<F>>) -> Result<(), SynthesisError> {
+        let Az = mat_vec_mul_sparse(rel_r1cs.A, z.clone());
+        let Bz = mat_vec_mul_sparse(rel_r1cs.B, z.clone());
+        let Cz = mat_vec_mul_sparse(rel_r1cs.C, z.clone());
+        let uCz = vec_scalar_mul(&Cz, &rel_r1cs.u);
+        let uCzE = vec_add(&uCz, &rel_r1cs.E);
+        let AzBz = hadamard(&Az, &Bz);
+        for i in 0..AzBz.len() {
+            AzBz[i].enforce_equal(&uCzE[i].clone())?;
+        }
+        Ok(())
+    }
+}
+
+fn mat_vec_mul_sparse<F: PrimeField>(m: SparseMatrixVar<F>, v: Vec<FpVar<F>>) -> Vec<FpVar<F>> {
+    let mut res = vec![FpVar::<F>::zero(); m.n_rows];
+    for (row_i, row) in m.coeffs.iter().enumerate() {
+        for (value, col_i) in row.iter() {
+            res[row_i] += value * v[*col_i].clone();
+        }
+    }
+    res
+}
+pub fn vec_add<F: PrimeField>(a: &Vec<FpVar<F>>, b: &Vec<FpVar<F>>) -> Vec<FpVar<F>> {
+    assert_eq!(a.len(), b.len());
+    let mut r: Vec<FpVar<F>> = vec![FpVar::<F>::zero(); a.len()];
+    for i in 0..a.len() {
+        r[i] = a[i].clone() + b[i].clone();
+    }
+    r
+}
+pub fn vec_scalar_mul<F: PrimeField>(vec: &Vec<FpVar<F>>, c: &FpVar<F>) -> Vec<FpVar<F>> {
+    let mut result = vec![FpVar::<F>::zero(); vec.len()];
+    for (i, a) in vec.iter().enumerate() {
+        result[i] = a.clone() * c;
+    }
+    result
+}
+pub fn hadamard<F: PrimeField>(a: &Vec<FpVar<F>>, b: &Vec<FpVar<F>>) -> Vec<FpVar<F>> {
+    assert_eq!(a.len(), b.len());
+    let mut r: Vec<FpVar<F>> = vec![FpVar::<F>::zero(); a.len()];
+    for i in 0..a.len() {
+        r[i] = a[i].clone() * b[i].clone();
+    }
+    r
+}
+
+#[derive(Debug, Clone)]
+pub struct SparseMatrixVar<F: PrimeField> {
+    pub n_rows: usize,
+    pub n_cols: usize,
+    // same format as the native SparseMatrix (which follows ark_relations::r1cs::Matrix format
+    pub coeffs: Vec<Vec<(FpVar<F>, usize)>>,
+}
+
+impl<F> AllocVar<SparseMatrix<F>, F> for SparseMatrixVar<F>
+where
+    F: PrimeField,
+{
+    fn new_variable<T: Borrow<SparseMatrix<F>>>(
+        cs: impl Into<Namespace<F>>,
+        f: impl FnOnce() -> Result<T, SynthesisError>,
+        mode: AllocationMode,
+    ) -> Result<Self, SynthesisError> {
+        f().and_then(|val| {
+            let cs = cs.into();
+
+            let mut coeffs: Vec<Vec<(FpVar<F>, usize)>> = Vec::new();
+            for row in val.borrow().coeffs.iter() {
+                let mut rowVar: Vec<(FpVar<F>, usize)> = Vec::new();
+                for &(value, col_i) in row.iter() {
+                    let coeffVar = FpVar::<F>::new_variable(cs.clone(), || Ok(value), mode)?;
+                    rowVar.push((coeffVar, col_i));
+                }
+                coeffs.push(rowVar);
+            }
+
+            Ok(Self {
+                n_rows: val.borrow().n_rows,
+                n_cols: val.borrow().n_cols,
+                coeffs,
+            })
+        })
+    }
+}
+
+#[derive(Debug, Clone)]
+pub struct RelaxedR1CSVar<F: PrimeField> {
+    pub A: SparseMatrixVar<F>,
+    pub B: SparseMatrixVar<F>,
+    pub C: SparseMatrixVar<F>,
+    pub u: FpVar<F>,
+    pub E: Vec<FpVar<F>>,
+}
+
+impl<F> AllocVar<RelaxedR1CS<F>, F> for RelaxedR1CSVar<F>
+where
+    F: PrimeField,
+{
+    fn new_variable<T: Borrow<RelaxedR1CS<F>>>(
+        cs: impl Into<Namespace<F>>,
+        f: impl FnOnce() -> Result<T, SynthesisError>,
+        mode: AllocationMode,
+    ) -> Result<Self, SynthesisError> {
+        f().and_then(|val| {
+            let cs = cs.into();
+
+            let A = SparseMatrixVar::<F>::new_constant(cs.clone(), &val.borrow().A)?;
+            let B = SparseMatrixVar::<F>::new_constant(cs.clone(), &val.borrow().B)?;
+            let C = SparseMatrixVar::<F>::new_constant(cs.clone(), &val.borrow().C)?;
+            let E = Vec::<FpVar<F>>::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?;
+            let u = FpVar::<F>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
+
+            Ok(Self { A, B, C, E, u })
+        })
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use ark_crypto_primitives::crh::{
+        sha256::{
+            constraints::{Sha256Gadget, UnitVar},
+            Sha256,
+        },
+        CRHScheme, CRHSchemeGadget,
+    };
+    use ark_ff::BigInteger;
+    use ark_pallas::Fr;
+    use ark_r1cs_std::{alloc::AllocVar, bits::uint8::UInt8};
+    use ark_relations::r1cs::{
+        ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
+    };
+    use ark_std::One;
+
+    use crate::ccs::r1cs::{
+        tests::{get_test_r1cs, get_test_z},
+        R1CS,
+    };
+    use crate::frontend::arkworks::{extract_r1cs_and_z, tests::TestCircuit};
+
+    #[test]
+    fn test_relaxed_r1cs_small_gadget_handcrafted() {
+        let r1cs: R1CS<Fr> = get_test_r1cs();
+        let rel_r1cs = r1cs.relax();
+        let z = get_test_z(3);
+
+        let cs = ConstraintSystem::<Fr>::new_ref();
+
+        let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
+        let rel_r1csVar = RelaxedR1CSVar::<Fr>::new_witness(cs.clone(), || Ok(rel_r1cs)).unwrap();
+
+        RelaxedR1CSGadget::<Fr>::check(rel_r1csVar, zVar).unwrap();
+        assert!(cs.is_satisfied().unwrap());
+        dbg!(cs.num_constraints());
+    }
+
+    // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been
+    // initialized.
+    fn test_relaxed_r1cs_gadget<CS: ConstraintSynthesizer<Fr>>(circuit: CS) {
+        let cs = ConstraintSystem::<Fr>::new_ref();
+
+        circuit.generate_constraints(cs.clone()).unwrap();
+        cs.finalize();
+        assert!(cs.is_satisfied().unwrap());
+
+        // num constraints of the original circuit
+        dbg!(cs.num_constraints());
+
+        let cs = cs.into_inner().unwrap();
+
+        let (r1cs, z) = extract_r1cs_and_z::<Fr>(&cs);
+        r1cs.check_relation(&z).unwrap();
+
+        let relaxed_r1cs = r1cs.relax();
+        relaxed_r1cs.check_relation(&z).unwrap();
+
+        // set new CS for the circuit that checks the RelaxedR1CS of our original circuit
+        let cs = ConstraintSystem::<Fr>::new_ref();
+        // prepare the inputs for our circuit
+        let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
+        let rel_r1csVar =
+            RelaxedR1CSVar::<Fr>::new_witness(cs.clone(), || Ok(relaxed_r1cs)).unwrap();
+
+        RelaxedR1CSGadget::<Fr>::check(rel_r1csVar, zVar).unwrap();
+        assert!(cs.is_satisfied().unwrap());
+
+        // num constraints of the circuit that checks the RelaxedR1CS of the original circuit
+        dbg!(cs.num_constraints());
+    }
+
+    #[test]
+    fn test_relaxed_r1cs_small_gadget_arkworks() {
+        let x = Fr::from(5_u32);
+        let y = x * x * x + x + Fr::from(5_u32);
+        let circuit = TestCircuit::<Fr> { x, y };
+        test_relaxed_r1cs_gadget(circuit);
+    }
+
+    struct Sha256TestCircuit<F: PrimeField> {
+        _f: PhantomData<F>,
+        pub x: Vec<u8>,
+        pub y: Vec<u8>,
+    }
+    impl<F: PrimeField> ConstraintSynthesizer<F> for Sha256TestCircuit<F> {
+        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
+            let x = Vec::<UInt8<F>>::new_witness(cs.clone(), || Ok(self.x))?;
+            let y = Vec::<UInt8<F>>::new_input(cs.clone(), || Ok(self.y))?;
+
+            let unitVar = UnitVar::default();
+            let comp_y = <Sha256Gadget<F> as CRHSchemeGadget<Sha256, F>>::evaluate(&unitVar, &x)?;
+            comp_y.0.enforce_equal(&y)?;
+            Ok(())
+        }
+    }
+    #[test]
+    fn test_relaxed_r1cs_medium_gadget_arkworks() {
+        let x = Fr::from(5_u32).into_bigint().to_bytes_le();
+        let y = <Sha256 as CRHScheme>::evaluate(&(), x.clone()).unwrap();
+
+        let circuit = Sha256TestCircuit::<Fr> {
+            _f: PhantomData,
+            x,
+            y,
+        };
+        test_relaxed_r1cs_gadget(circuit);
+    }
+
+    // circuit that has the numer of constraints specified in the `n_constraints` parameter. Note
+    // that the generated circuit will have very sparse matrices, so the resulting constraints
+    // number of the RelaxedR1CS gadget must take that into account.
+    struct CustomTestCircuit<F: PrimeField> {
+        _f: PhantomData<F>,
+        pub n_constraints: usize,
+        pub x: F,
+        pub y: F,
+    }
+    impl<F: PrimeField> ConstraintSynthesizer<F> for CustomTestCircuit<F> {
+        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
+            let x = FpVar::<F>::new_witness(cs.clone(), || Ok(self.x))?;
+            let y = FpVar::<F>::new_input(cs.clone(), || Ok(self.y))?;
+
+            let mut comp_y = FpVar::<F>::new_witness(cs.clone(), || Ok(F::one()))?;
+            for _ in 0..self.n_constraints - 1 {
+                comp_y *= x.clone();
+            }
+
+            comp_y.enforce_equal(&y)?;
+            Ok(())
+        }
+    }
+    #[test]
+    fn test_relaxed_r1cs_custom_circuit() {
+        let n_constraints = 10_000;
+        let x = Fr::from(5_u32);
+        let mut y = Fr::one();
+        for _ in 0..n_constraints - 1 {
+            y *= x;
+        }
+
+        let circuit = CustomTestCircuit::<Fr> {
+            _f: PhantomData,
+            n_constraints,
+            x,
+            y,
+        };
+        test_relaxed_r1cs_gadget(circuit);
+    }
+}

@@ -0,0 +1,1 @@
+pub mod circuit;

@@ -0,0 +1,100 @@
+/// arkworks frontend
+use ark_ff::PrimeField;
+use ark_relations::r1cs::ConstraintSystem;
+
+use crate::ccs::r1cs::R1CS;
+use crate::utils::vec::SparseMatrix;
+
+/// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format, and
+/// extracts public inputs and witness into z vector. Returns a tuple containing (R1CS, z).
+pub fn extract_r1cs_and_z<F: PrimeField>(cs: &ConstraintSystem<F>) -> (R1CS<F>, Vec<F>) {
+    let m = cs.to_matrices().unwrap();
+
+    let n_rows = cs.num_constraints;
+    let n_cols = cs.num_instance_variables + cs.num_witness_variables; // cs.num_instance_variables already counts the 1
+
+    let A = SparseMatrix::<F> {
+        n_rows,
+        n_cols,
+        coeffs: m.a,
+    };
+    let B = SparseMatrix::<F> {
+        n_rows,
+        n_cols,
+        coeffs: m.b,
+    };
+    let C = SparseMatrix::<F> {
+        n_rows,
+        n_cols,
+        coeffs: m.c,
+    };
+
+    // z = (1, x, w)
+    let z: Vec<F> = [
+        // 1 is already included in cs.instance_assignment
+        cs.instance_assignment.clone(),
+        cs.witness_assignment.clone(),
+    ]
+    .concat();
+
+    (
+        R1CS::<F> {
+            l: cs.num_instance_variables,
+            A,
+            B,
+            C,
+        },
+        z,
+    )
+}
+
+#[cfg(test)]
+pub mod tests {
+    use super::*;
+    use ark_ff::PrimeField;
+    use ark_pallas::Fr;
+    use ark_r1cs_std::{alloc::AllocVar, eq::EqGadget, fields::fp::FpVar};
+    use ark_relations::r1cs::{
+        ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
+    };
+
+    // TestCircuit implements the R1CS for: x^3 + x + 5 = y (example from article
+    // https://www.vitalik.ca/general/2016/12/10/qap.html )
+    #[derive(Clone, Copy, Debug)]
+    pub struct TestCircuit<F: PrimeField> {
+        pub x: F,
+        pub y: F,
+    }
+    impl<F: PrimeField> ConstraintSynthesizer<F> for TestCircuit<F> {
+        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
+            let x = FpVar::<F>::new_input(cs.clone(), || Ok(self.x))?;
+            let y = FpVar::<F>::new_witness(cs.clone(), || Ok(self.y))?;
+            let five = FpVar::<F>::new_constant(cs.clone(), F::from(5u32))?;
+
+            let comp_y = (&x * &x * &x) + &x + &five;
+            comp_y.enforce_equal(&y)?;
+            Ok(())
+        }
+    }
+
+    #[test]
+    fn test_cs_to_matrices() {
+        let cs = ConstraintSystem::<Fr>::new_ref();
+
+        let x = Fr::from(5_u32);
+        let y = x * x * x + x + Fr::from(5_u32);
+
+        let test_circuit = TestCircuit::<Fr> { x, y };
+        test_circuit.generate_constraints(cs.clone()).unwrap();
+        cs.finalize();
+        assert!(cs.is_satisfied().unwrap());
+
+        let cs = cs.into_inner().unwrap();
+
+        // ensure that num_instance_variables is 2: 1 + 1 public input
+        assert_eq!(cs.num_instance_variables, 2);
+
+        let (r1cs, z) = extract_r1cs_and_z::<Fr>(&cs);
+        r1cs.check_relation(&z).unwrap();
+    }
+}

@@ -0,0 +1,1 @@
+pub mod arkworks;

@@ -10,7 +10,9 @@ pub mod transcript;
 use transcript::Transcript;
 pub mod ccs;
 pub mod constants;
+pub mod decider;
 pub mod folding;
+pub mod frontend;
 pub mod pedersen;
 pub mod utils;
 

@@ -1,4 +1,5 @@
 use ark_ff::PrimeField;
+pub use ark_relations::r1cs::Matrix as R1CSMatrix;
 use ark_std::cfg_iter;
 use rayon::iter::{IndexedParallelIterator, IntoParallelRefIterator, ParallelIterator};
 
@@ -6,7 +7,21 @@ #[derive(Clone, Debug, Eq, PartialEq)]
 pub struct SparseMatrix<F: PrimeField> {
     pub n_rows: usize,
     pub n_cols: usize,
-    pub coeffs: Vec<(usize, usize, F)>,
+    /// coeffs = R1CSMatrix = Vec<Vec<(F, usize)>>, which contains each row and the F is the value
+    /// of the coefficient and the usize indicates the column position
+    pub coeffs: R1CSMatrix<F>,
+}
+
+impl<F: PrimeField> SparseMatrix<F> {
+    pub fn to_dense(&self) -> Vec<Vec<F>> {
+        let mut r: Vec<Vec<F>> = vec![vec![F::zero(); self.n_cols]; self.n_rows];
+        for (row_i, row) in self.coeffs.iter().enumerate() {
+            for &(value, col_i) in row.iter() {
+                r[row_i][col_i] = value;
+            }
+        }
+        r
+    }
 }
 
 pub fn dense_matrix_to_sparse<F: PrimeField>(m: Vec<Vec<F>>) -> SparseMatrix<F> {
@@ -15,12 +30,14 @@ n_rows: m.len(),
         n_cols: m[0].len(),
         coeffs: Vec::new(),
     };
-    for (i, m_i) in m.iter().enumerate() {
-        for (j, m_ij) in m_i.iter().enumerate() {
-            if !m_ij.is_zero() {
-                r.coeffs.push((i, j, *m_ij));
+    for m_row in m.iter() {
+        let mut row: Vec<(F, usize)> = Vec::new();
+        for (col_i, value) in m_row.iter().enumerate() {
+            if !value.is_zero() {
+                row.push((*value, col_i));
             }
         }
+        r.coeffs.push(row);
     }
     r
 }
@@ -75,9 +92,12 @@ }
 
 pub fn mat_vec_mul_sparse<F: PrimeField>(matrix: &SparseMatrix<F>, vector: &[F]) -> Vec<F> {
     let mut res = vec![F::zero(); matrix.n_rows];
-    for &(row, col, value) in matrix.coeffs.iter() {
-        res[row] += value * vector[col];
+    for (row_i, row) in matrix.coeffs.iter().enumerate() {
+        for &(value, col_i) in row.iter() {
+            res[row_i] += value * vector[col_i];
+        }
     }
+
     res
 }
 
@@ -109,6 +129,19 @@ }
         r
     }
 
+    #[test]
+    fn test_dense_sparse_conversions() {
+        let A = to_F_matrix::<Fr>(vec![
+            vec![0, 1, 0, 0, 0, 0],
+            vec![0, 0, 0, 1, 0, 0],
+            vec![0, 1, 0, 0, 1, 0],
+            vec![5, 0, 0, 0, 0, 1],
+        ]);
+        let A_sparse = dense_matrix_to_sparse(A.clone());
+        assert_eq!(A_sparse.to_dense(), A);
+    }
+
+    // test mat_vec_mul & mat_vec_mul_sparse
     #[test]
     fn test_mat_vec_mul() {
         let A = to_F_matrix::<Fr>(vec![