1use ark_ff::PrimeField;
  2use ark_relations::r1cs::ConstraintSystem;
  3use ark_std::rand::Rng;
  4
  5use crate::utils::vec::{hadamard, mat_vec_mul, vec_add, vec_scalar_mul, SparseMatrix};
  6use crate::Error;
  7
  8#[derive(Debug, Clone, Eq, PartialEq)]
  9pub struct R1CS<F: PrimeField> {
 10    pub l: usize, // io len
 11    pub A: SparseMatrix<F>,
 12    pub B: SparseMatrix<F>,
 13    pub C: SparseMatrix<F>,
 14}
 15
 16impl<F: PrimeField> R1CS<F> {
 17    pub fn rand<R: Rng>(rng: &mut R, n_rows: usize, n_cols: usize) -> Self {
 18        Self {
 19            l: 1,
 20            A: SparseMatrix::rand(rng, n_rows, n_cols),
 21            B: SparseMatrix::rand(rng, n_rows, n_cols),
 22            C: SparseMatrix::rand(rng, n_rows, n_cols),
 23        }
 24    }
 25
 26    /// returns a tuple containing (w, x) (witness and public inputs respectively)
 27    pub fn split_z(&self, z: &[F]) -> (Vec<F>, Vec<F>) {
 28        (z[self.l + 1..].to_vec(), z[1..self.l + 1].to_vec())
 29    }
 30
 31    /// check that a R1CS structure is satisfied by a z vector. Only for testing.
 32    pub fn check_relation(&self, z: &[F]) -> Result<(), Error> {
 33        let Az = mat_vec_mul(&self.A, z)?;
 34        let Bz = mat_vec_mul(&self.B, z)?;
 35        let Cz = mat_vec_mul(&self.C, z)?;
 36        let AzBz = hadamard(&Az, &Bz)?;
 37        if AzBz != Cz {
 38            return Err(Error::NotSatisfied);
 39        }
 40
 41        Ok(())
 42    }
 43
 44    /// converts the R1CS instance into a RelaxedR1CS as described in
 45    /// [Nova](https://eprint.iacr.org/2021/370.pdf) section 4.1.
 46    pub fn relax(self) -> RelaxedR1CS<F> {
 47        RelaxedR1CS::<F> {
 48            l: self.l,
 49            E: vec![F::zero(); self.A.n_rows],
 50            A: self.A,
 51            B: self.B,
 52            C: self.C,
 53            u: F::one(),
 54        }
 55    }
 56}
 57
 58#[derive(Debug, Clone, Eq, PartialEq)]
 59pub struct RelaxedR1CS<F: PrimeField> {
 60    pub l: usize, // io len
 61    pub A: SparseMatrix<F>,
 62    pub B: SparseMatrix<F>,
 63    pub C: SparseMatrix<F>,
 64    pub u: F,
 65    pub E: Vec<F>,
 66}
 67
 68impl<F: PrimeField> RelaxedR1CS<F> {
 69    /// check that a RelaxedR1CS structure is satisfied by a z vector. Only for testing.
 70    pub fn check_relation(&self, z: &[F]) -> Result<(), Error> {
 71        let Az = mat_vec_mul(&self.A, z)?;
 72        let Bz = mat_vec_mul(&self.B, z)?;
 73        let Cz = mat_vec_mul(&self.C, z)?;
 74        let uCz = vec_scalar_mul(&Cz, &self.u);
 75        let uCzE = vec_add(&uCz, &self.E)?;
 76        let AzBz = hadamard(&Az, &Bz)?;
 77        if AzBz != uCzE {
 78            return Err(Error::NotSatisfied);
 79        }
 80
 81        Ok(())
 82    }
 83}
 84
 85/// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format as R1CS
 86/// struct.
 87pub fn extract_r1cs<F: PrimeField>(cs: &ConstraintSystem<F>) -> R1CS<F> {
 88    let m = cs.to_matrices().unwrap();
 89
 90    let n_rows = cs.num_constraints;
 91    let n_cols = cs.num_instance_variables + cs.num_witness_variables; // cs.num_instance_variables already counts the 1
 92
 93    let A = SparseMatrix::<F> {
 94        n_rows,
 95        n_cols,
 96        coeffs: m.a,
 97    };
 98    let B = SparseMatrix::<F> {
 99        n_rows,
100        n_cols,
101        coeffs: m.b,
102    };
103    let C = SparseMatrix::<F> {
104        n_rows,
105        n_cols,
106        coeffs: m.c,
107    };
108
109    R1CS::<F> {
110        l: cs.num_instance_variables - 1, // -1 to subtract the first '1'
111        A,
112        B,
113        C,
114    }
115}
116
117/// extracts the witness and the public inputs from arkworks ConstraintSystem.
118pub fn extract_w_x<F: PrimeField>(cs: &ConstraintSystem<F>) -> (Vec<F>, Vec<F>) {
119    (
120        cs.witness_assignment.clone(),
121        // skip the first element which is '1'
122        cs.instance_assignment[1..].to_vec(),
123    )
124}
125
126#[cfg(test)]
127pub mod tests {
128    use super::*;
129    use crate::utils::vec::tests::{to_F_matrix, to_F_vec};
130
131    use ark_ff::PrimeField;
132    use ark_pallas::Fr;
133
134    pub fn get_test_r1cs<F: PrimeField>() -> R1CS<F> {
135        // R1CS for: x^3 + x + 5 = y (example from article
136        // https://www.vitalik.ca/general/2016/12/10/qap.html )
137        let A = to_F_matrix::<F>(vec![
138            vec![0, 1, 0, 0, 0, 0],
139            vec![0, 0, 0, 1, 0, 0],
140            vec![0, 1, 0, 0, 1, 0],
141            vec![5, 0, 0, 0, 0, 1],
142        ]);
143        let B = to_F_matrix::<F>(vec![
144            vec![0, 1, 0, 0, 0, 0],
145            vec![0, 1, 0, 0, 0, 0],
146            vec![1, 0, 0, 0, 0, 0],
147            vec![1, 0, 0, 0, 0, 0],
148        ]);
149        let C = to_F_matrix::<F>(vec![
150            vec![0, 0, 0, 1, 0, 0],
151            vec![0, 0, 0, 0, 1, 0],
152            vec![0, 0, 0, 0, 0, 1],
153            vec![0, 0, 1, 0, 0, 0],
154        ]);
155
156        R1CS::<F> { l: 1, A, B, C }
157    }
158
159    pub fn get_test_z<F: PrimeField>(input: usize) -> Vec<F> {
160        // z = (1, io, w)
161        to_F_vec(vec![
162            1,
163            input,                             // io
164            input * input * input + input + 5, // x^3 + x + 5
165            input * input,                     // x^2
166            input * input * input,             // x^2 * x
167            input * input * input + input,     // x^3 + x
168        ])
169    }
170
171    #[test]
172    fn test_check_relation() {
173        let r1cs = get_test_r1cs::<Fr>();
174        let z = get_test_z(5);
175        r1cs.check_relation(&z).unwrap();
176        r1cs.relax().check_relation(&z).unwrap();
177    }
178}