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