1use ark_ec::CurveGroup;
  2use ark_std::{rand::RngCore, UniformRand};
  3
  4use super::{CommittedInstance, Witness};
  5use crate::arith::ArithSampler;
  6use crate::arith::{r1cs::R1CS, Arith};
  7use crate::commitment::CommitmentScheme;
  8use crate::folding::circuits::CF1;
  9use crate::folding::ova::{
 10    CommittedInstance as OvaCommittedInstance, TestingWitness as OvaWitness,
 11};
 12use crate::Error;
 13
 14/// Implements `Arith` for R1CS, where the witness is of type [`Witness`], and
 15/// the committed instance is of type [`CommittedInstance`].
 16///
 17/// Due to the error terms `Witness.E` and `CommittedInstance.u`, R1CS here is
 18/// considered as a relaxed R1CS.
 19///
 20/// One may wonder why we do not provide distinct structs for R1CS and relaxed
 21/// R1CS.
 22/// This is because both plain R1CS and relaxed R1CS have the same structure:
 23/// they are both represented by three matrices.
 24/// What makes them different is the error terms, which are not part of the R1CS
 25/// struct, but are part of the witness and committed instance.
 26///
 27/// As a follow-up, one may further ask why not providing a trait for relaxed
 28/// R1CS and implement it for the `R1CS` struct, where the relaxed R1CS trait
 29/// has methods for relaxed satisfiability check, while the `Arith` trait that
 30/// `R1CS` implements has methods for plain satisfiability check.
 31/// However, it would be more ideal if we have a single method that can smartly
 32/// choose the type of satisfiability check, which would make the code more
 33/// generic and easier to maintain.
 34///
 35/// This is achieved thanks to the new design of the [`Arith`] trait, where we
 36/// can implement the trait for the same constraint system with different types
 37/// of witnesses and committed instances.
 38/// For R1CS, whether it is relaxed or not is now determined by the types of `W`
 39/// and `U`: the satisfiability check is relaxed if `W` and `U` are defined by
 40/// folding schemes, and plain if they are vectors of field elements.
 41impl<C: CurveGroup> Arith<Witness<C>, CommittedInstance<C>> for R1CS<CF1<C>> {
 42    type Evaluation = Vec<CF1<C>>;
 43
 44    fn eval_relation(
 45        &self,
 46        w: &Witness<C>,
 47        u: &CommittedInstance<C>,
 48    ) -> Result<Self::Evaluation, Error> {
 49        self.eval_at_z(&[&[u.u][..], &u.x, &w.W].concat())
 50    }
 51
 52    fn check_evaluation(
 53        w: &Witness<C>,
 54        _u: &CommittedInstance<C>,
 55        e: Self::Evaluation,
 56    ) -> Result<(), Error> {
 57        (w.E == e).then_some(()).ok_or(Error::NotSatisfied)
 58    }
 59}
 60
 61impl<C: CurveGroup> ArithSampler<C, Witness<C>, CommittedInstance<C>> for R1CS<CF1<C>> {
 62    fn sample_witness_instance<CS: CommitmentScheme<C, true>>(
 63        &self,
 64        params: &CS::ProverParams,
 65        mut rng: impl RngCore,
 66    ) -> Result<(Witness<C>, CommittedInstance<C>), Error> {
 67        // Implements sampling a (committed) RelaxedR1CS
 68        // See construction 5 in https://eprint.iacr.org/2023/573.pdf
 69        let u = C::ScalarField::rand(&mut rng);
 70        let rE = C::ScalarField::rand(&mut rng);
 71        let rW = C::ScalarField::rand(&mut rng);
 72
 73        let W = (0..self.A.n_cols - self.l - 1)
 74            .map(|_| C::ScalarField::rand(&mut rng))
 75            .collect();
 76        let x = (0..self.l)
 77            .map(|_| C::ScalarField::rand(&mut rng))
 78            .collect::<Vec<C::ScalarField>>();
 79        let mut z = vec![u];
 80        z.extend(&x);
 81        z.extend(&W);
 82
 83        let E = self.eval_at_z(&z)?;
 84
 85        let witness = Witness { E, rE, W, rW };
 86        let mut cm_witness = witness.commit::<CS, true>(params, x)?;
 87
 88        // witness.commit() sets u to 1, we set it to the sampled u value
 89        cm_witness.u = u;
 90
 91        debug_assert!(
 92            self.check_relation(&witness, &cm_witness).is_ok(),
 93            "Sampled a non satisfiable relaxed R1CS, sampled u: {}, computed E: {:?}",
 94            u,
 95            witness.E
 96        );
 97
 98        Ok((witness, cm_witness))
 99    }
100}
101
102// Sadly, this forces duplication of code. We can try to abstract with more traits if needed..
103impl<C: CurveGroup> Arith<OvaWitness<C>, OvaCommittedInstance<C>> for R1CS<CF1<C>> {
104    type Evaluation = Vec<CF1<C>>;
105
106    fn eval_relation(
107        &self,
108        w: &OvaWitness<C>,
109        u: &OvaCommittedInstance<C>,
110    ) -> Result<Self::Evaluation, Error> {
111        self.eval_at_z(&[&[u.mu], u.x.as_slice(), &w.w].concat())
112    }
113
114    fn check_evaluation(
115        w: &OvaWitness<C>,
116        _u: &OvaCommittedInstance<C>,
117        e: Self::Evaluation,
118    ) -> Result<(), Error> {
119        (w.e == e).then_some(()).ok_or(Error::NotSatisfied)
120    }
121}