1use crate::commitment::CommitmentScheme;
  2use crate::folding::nova::{CommittedInstance, Witness};
  3use crate::RngCore;
  4use ark_crypto_primitives::sponge::Absorb;
  5use ark_ec::{CurveGroup, Group};
  6use ark_ff::PrimeField;
  7use ark_relations::r1cs::ConstraintSystem;
  8use ark_serialize::{CanonicalDeserialize, CanonicalSerialize};
  9use ark_std::rand::Rng;
 10
 11use super::Arith;
 12use crate::utils::vec::{hadamard, mat_vec_mul, vec_add, vec_scalar_mul, vec_sub, SparseMatrix};
 13use crate::Error;
 14
 15#[derive(Debug, Clone, Eq, PartialEq, CanonicalSerialize, CanonicalDeserialize)]
 16pub struct R1CS<F: PrimeField> {
 17    pub l: usize, // io len
 18    pub A: SparseMatrix<F>,
 19    pub B: SparseMatrix<F>,
 20    pub C: SparseMatrix<F>,
 21}
 22
 23impl<F: PrimeField> Arith<F> for R1CS<F> {
 24    /// check that a R1CS structure is satisfied by a z vector. Only for testing.
 25    fn check_relation(&self, z: &[F]) -> Result<(), Error> {
 26        let Az = mat_vec_mul(&self.A, z)?;
 27        let Bz = mat_vec_mul(&self.B, z)?;
 28        let Cz = mat_vec_mul(&self.C, z)?;
 29        let AzBz = hadamard(&Az, &Bz)?;
 30        if AzBz != Cz {
 31            return Err(Error::NotSatisfied);
 32        }
 33        Ok(())
 34    }
 35
 36    fn params_to_le_bytes(&self) -> Vec<u8> {
 37        [
 38            self.l.to_le_bytes(),
 39            self.A.n_rows.to_le_bytes(),
 40            self.A.n_cols.to_le_bytes(),
 41        ]
 42        .concat()
 43    }
 44}
 45
 46impl<F: PrimeField> R1CS<F> {
 47    pub fn empty() -> Self {
 48        R1CS {
 49            l: 0,
 50            A: SparseMatrix::empty(),
 51            B: SparseMatrix::empty(),
 52            C: SparseMatrix::empty(),
 53        }
 54    }
 55    pub fn rand<R: Rng>(rng: &mut R, n_rows: usize, n_cols: usize) -> Self {
 56        Self {
 57            l: 1,
 58            A: SparseMatrix::rand(rng, n_rows, n_cols),
 59            B: SparseMatrix::rand(rng, n_rows, n_cols),
 60            C: SparseMatrix::rand(rng, n_rows, n_cols),
 61        }
 62    }
 63
 64    /// returns a tuple containing (w, x) (witness and public inputs respectively)
 65    pub fn split_z(&self, z: &[F]) -> (Vec<F>, Vec<F>) {
 66        (z[self.l + 1..].to_vec(), z[1..self.l + 1].to_vec())
 67    }
 68
 69    /// converts the R1CS instance into a RelaxedR1CS as described in
 70    /// [Nova](https://eprint.iacr.org/2021/370.pdf) section 4.1.
 71    pub fn relax(self) -> RelaxedR1CS<F> {
 72        RelaxedR1CS::<F> {
 73            l: self.l,
 74            E: vec![F::zero(); self.A.n_rows],
 75            A: self.A,
 76            B: self.B,
 77            C: self.C,
 78            u: F::one(),
 79        }
 80    }
 81}
 82
 83#[derive(Debug, Clone, Eq, PartialEq)]
 84pub struct RelaxedR1CS<F: PrimeField> {
 85    pub l: usize, // io len
 86    pub A: SparseMatrix<F>,
 87    pub B: SparseMatrix<F>,
 88    pub C: SparseMatrix<F>,
 89    pub u: F,
 90    pub E: Vec<F>,
 91}
 92
 93impl<F: PrimeField> RelaxedR1CS<F> {
 94    /// check that a RelaxedR1CS structure is satisfied by a z vector. Only for testing.
 95    pub fn check_relation(&self, z: &[F]) -> Result<(), Error> {
 96        let Az = mat_vec_mul(&self.A, z)?;
 97        let Bz = mat_vec_mul(&self.B, z)?;
 98        let Cz = mat_vec_mul(&self.C, z)?;
 99        let uCz = vec_scalar_mul(&Cz, &self.u);
100        let uCzE = vec_add(&uCz, &self.E)?;
101        let AzBz = hadamard(&Az, &Bz)?;
102        if AzBz != uCzE {
103            return Err(Error::NotSatisfied);
104        }
105
106        Ok(())
107    }
108
109    // Computes the E term, given A, B, C, z, u
110    fn compute_E(
111        A: &SparseMatrix<F>,
112        B: &SparseMatrix<F>,
113        C: &SparseMatrix<F>,
114        z: &[F],
115        u: &F,
116    ) -> Result<Vec<F>, Error> {
117        let Az = mat_vec_mul(A, z)?;
118        let Bz = mat_vec_mul(B, z)?;
119        let AzBz = hadamard(&Az, &Bz)?;
120
121        let Cz = mat_vec_mul(C, z)?;
122        let uCz = vec_scalar_mul(&Cz, u);
123        vec_sub(&AzBz, &uCz)
124    }
125
126    pub fn check_sampled_relaxed_r1cs(&self, u: F, E: &[F], z: &[F]) -> bool {
127        let sampled = RelaxedR1CS {
128            l: self.l,
129            A: self.A.clone(),
130            B: self.B.clone(),
131            C: self.C.clone(),
132            u,
133            E: E.to_vec(),
134        };
135        sampled.check_relation(z).is_ok()
136    }
137
138    // Implements sampling a (committed) RelaxedR1CS
139    // See construction 5 in https://eprint.iacr.org/2023/573.pdf
140    pub fn sample<C, CS>(
141        &self,
142        params: &CS::ProverParams,
143        mut rng: impl RngCore,
144    ) -> Result<(CommittedInstance<C>, Witness<C>), Error>
145    where
146        C: CurveGroup,
147        C: CurveGroup<ScalarField = F>,
148        <C as Group>::ScalarField: Absorb,
149        CS: CommitmentScheme<C, true>,
150    {
151        let u = C::ScalarField::rand(&mut rng);
152        let rE = C::ScalarField::rand(&mut rng);
153        let rW = C::ScalarField::rand(&mut rng);
154
155        let W = (0..self.A.n_cols - self.l - 1)
156            .map(|_| F::rand(&mut rng))
157            .collect();
158        let x = (0..self.l).map(|_| F::rand(&mut rng)).collect::<Vec<F>>();
159        let mut z = vec![u];
160        z.extend(&x);
161        z.extend(&W);
162
163        let E = RelaxedR1CS::compute_E(&self.A, &self.B, &self.C, &z, &u)?;
164
165        debug_assert!(
166            z.len() == self.A.n_cols,
167            "Length of z is {}, while A has {} columns.",
168            z.len(),
169            self.A.n_cols
170        );
171
172        debug_assert!(
173            self.check_sampled_relaxed_r1cs(u, &E, &z),
174            "Sampled a non satisfiable relaxed R1CS, sampled u: {}, computed E: {:?}",
175            u,
176            E
177        );
178
179        let witness = Witness { E, rE, W, rW };
180        let mut cm_witness = witness.commit::<CS, true>(params, x)?;
181
182        // witness.commit() sets u to 1, we set it to the sampled u value
183        cm_witness.u = u;
184        Ok((cm_witness, witness))
185    }
186}
187
188/// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format as R1CS
189/// struct.
190pub fn extract_r1cs<F: PrimeField>(cs: &ConstraintSystem<F>) -> R1CS<F> {
191    let m = cs.to_matrices().unwrap();
192
193    let n_rows = cs.num_constraints;
194    let n_cols = cs.num_instance_variables + cs.num_witness_variables; // cs.num_instance_variables already counts the 1
195
196    let A = SparseMatrix::<F> {
197        n_rows,
198        n_cols,
199        coeffs: m.a,
200    };
201    let B = SparseMatrix::<F> {
202        n_rows,
203        n_cols,
204        coeffs: m.b,
205    };
206    let C = SparseMatrix::<F> {
207        n_rows,
208        n_cols,
209        coeffs: m.c,
210    };
211
212    R1CS::<F> {
213        l: cs.num_instance_variables - 1, // -1 to subtract the first '1'
214        A,
215        B,
216        C,
217    }
218}
219
220/// extracts the witness and the public inputs from arkworks ConstraintSystem.
221pub fn extract_w_x<F: PrimeField>(cs: &ConstraintSystem<F>) -> (Vec<F>, Vec<F>) {
222    (
223        cs.witness_assignment.clone(),
224        // skip the first element which is '1'
225        cs.instance_assignment[1..].to_vec(),
226    )
227}
228
229#[cfg(test)]
230pub mod tests {
231    use super::*;
232    use crate::{
233        commitment::pedersen::Pedersen,
234        utils::vec::tests::{to_F_matrix, to_F_vec},
235    };
236
237    use ark_pallas::{Fr, Projective};
238
239    #[test]
240    pub fn sample_relaxed_r1cs() {
241        let rng = rand::rngs::OsRng;
242        let r1cs = get_test_r1cs::<Fr>();
243        let (prover_params, _) = Pedersen::<Projective>::setup(rng, r1cs.A.n_rows).unwrap();
244
245        let relaxed_r1cs = r1cs.relax();
246        let sampled =
247            relaxed_r1cs.sample::<Projective, Pedersen<Projective, true>>(&prover_params, rng);
248        assert!(sampled.is_ok());
249    }
250
251    pub fn get_test_r1cs<F: PrimeField>() -> R1CS<F> {
252        // R1CS for: x^3 + x + 5 = y (example from article
253        // https://www.vitalik.ca/general/2016/12/10/qap.html )
254        let A = to_F_matrix::<F>(vec![
255            vec![0, 1, 0, 0, 0, 0],
256            vec![0, 0, 0, 1, 0, 0],
257            vec![0, 1, 0, 0, 1, 0],
258            vec![5, 0, 0, 0, 0, 1],
259        ]);
260        let B = to_F_matrix::<F>(vec![
261            vec![0, 1, 0, 0, 0, 0],
262            vec![0, 1, 0, 0, 0, 0],
263            vec![1, 0, 0, 0, 0, 0],
264            vec![1, 0, 0, 0, 0, 0],
265        ]);
266        let C = to_F_matrix::<F>(vec![
267            vec![0, 0, 0, 1, 0, 0],
268            vec![0, 0, 0, 0, 1, 0],
269            vec![0, 0, 0, 0, 0, 1],
270            vec![0, 0, 1, 0, 0, 0],
271        ]);
272
273        R1CS::<F> { l: 1, A, B, C }
274    }
275
276    pub fn get_test_z<F: PrimeField>(input: usize) -> Vec<F> {
277        // z = (1, io, w)
278        to_F_vec(vec![
279            1,
280            input,                             // io
281            input * input * input + input + 5, // x^3 + x + 5
282            input * input,                     // x^2
283            input * input * input,             // x^2 * x
284            input * input * input + input,     // x^3 + x
285        ])
286    }
287
288    pub fn get_test_z_split<F: PrimeField>(input: usize) -> (F, Vec<F>, Vec<F>) {
289        // z = (1, io, w)
290        (
291            F::one(),
292            to_F_vec(vec![
293                input, // io
294            ]),
295            to_F_vec(vec![
296                input * input * input + input + 5, // x^3 + x + 5
297                input * input,                     // x^2
298                input * input * input,             // x^2 * x
299                input * input * input + input,     // x^3 + x
300            ]),
301        )
302    }
303
304    #[test]
305    fn test_check_relation() {
306        let r1cs = get_test_r1cs::<Fr>();
307        let z = get_test_z(5);
308        r1cs.check_relation(&z).unwrap();
309        r1cs.relax().check_relation(&z).unwrap();
310    }
311}