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