1use crate::{
  2    arith::ArithGadget,
  3    utils::gadgets::{EquivalenceGadget, MatrixGadget, SparseMatrixVar, VectorGadget},
  4};
  5use ark_ff::PrimeField;
  6use ark_r1cs_std::alloc::{AllocVar, AllocationMode};
  7use ark_relations::r1cs::{Namespace, SynthesisError};
  8use ark_std::{borrow::Borrow, marker::PhantomData, One};
  9
 10use super::R1CS;
 11
 12/// An in-circuit representation of the `R1CS` struct.
 13///
 14/// `M` is for the modulo operation involved in the satisfiability check when
 15/// the underlying `FVar` is `NonNativeUintVar`.
 16#[derive(Debug, Clone)]
 17pub struct R1CSMatricesVar<M, FVar> {
 18    _m: PhantomData<M>,
 19    pub A: SparseMatrixVar<FVar>,
 20    pub B: SparseMatrixVar<FVar>,
 21    pub C: SparseMatrixVar<FVar>,
 22}
 23
 24impl<F: PrimeField, ConstraintF: PrimeField, FVar: AllocVar<F, ConstraintF>>
 25    AllocVar<R1CS<F>, ConstraintF> for R1CSMatricesVar<F, FVar>
 26{
 27    fn new_variable<T: Borrow<R1CS<F>>>(
 28        cs: impl Into<Namespace<ConstraintF>>,
 29        f: impl FnOnce() -> Result<T, SynthesisError>,
 30        _mode: AllocationMode,
 31    ) -> Result<Self, SynthesisError> {
 32        f().and_then(|val| {
 33            let cs = cs.into();
 34
 35            Ok(Self {
 36                _m: PhantomData,
 37                A: SparseMatrixVar::<FVar>::new_constant(cs.clone(), &val.borrow().A)?,
 38                B: SparseMatrixVar::<FVar>::new_constant(cs.clone(), &val.borrow().B)?,
 39                C: SparseMatrixVar::<FVar>::new_constant(cs.clone(), &val.borrow().C)?,
 40            })
 41        })
 42    }
 43}
 44
 45impl<M, FVar> R1CSMatricesVar<M, FVar>
 46where
 47    SparseMatrixVar<FVar>: MatrixGadget<FVar>,
 48    [FVar]: VectorGadget<FVar>,
 49{
 50    pub fn eval_at_z(&self, z: &[FVar]) -> Result<(Vec<FVar>, Vec<FVar>), SynthesisError> {
 51        // Multiply Cz by z[0] (u) here, allowing this method to be reused for
 52        // both relaxed and unrelaxed R1CS.
 53        let Az = self.A.mul_vector(z)?;
 54        let Bz = self.B.mul_vector(z)?;
 55        let Cz = self.C.mul_vector(z)?;
 56        let uCz = Cz.mul_scalar(&z[0])?;
 57        let AzBz = Az.hadamard(&Bz)?;
 58        Ok((AzBz, uCz))
 59    }
 60}
 61
 62impl<M, FVar, WVar: AsRef<[FVar]>, UVar: AsRef<[FVar]>> ArithGadget<WVar, UVar>
 63    for R1CSMatricesVar<M, FVar>
 64where
 65    SparseMatrixVar<FVar>: MatrixGadget<FVar>,
 66    [FVar]: VectorGadget<FVar> + EquivalenceGadget<M>,
 67    FVar: Clone + One,
 68{
 69    /// Evaluation is a tuple of two vectors (`AzBz` and `uCz`) instead of a
 70    /// single vector `AzBz - uCz`, because subtraction is not supported for
 71    /// `FVar = NonNativeUintVar`.
 72    type Evaluation = (Vec<FVar>, Vec<FVar>);
 73
 74    fn eval_relation(&self, w: &WVar, u: &UVar) -> Result<Self::Evaluation, SynthesisError> {
 75        self.eval_at_z(&[&[FVar::one()], u.as_ref(), w.as_ref()].concat())
 76    }
 77
 78    fn enforce_evaluation(
 79        _w: &WVar,
 80        _u: &UVar,
 81        (lhs, rhs): Self::Evaluation,
 82    ) -> Result<(), SynthesisError> {
 83        lhs.enforce_equivalent(&rhs)
 84    }
 85}
 86
 87#[cfg(test)]
 88pub mod tests {
 89    use std::cmp::max;
 90
 91    use ark_crypto_primitives::crh::{
 92        sha256::{
 93            constraints::{Sha256Gadget, UnitVar},
 94            Sha256,
 95        },
 96        CRHScheme, CRHSchemeGadget,
 97    };
 98    use ark_ec::CurveGroup;
 99    use ark_ff::BigInteger;
100    use ark_pallas::{Fq, Fr, Projective};
101    use ark_r1cs_std::{bits::uint8::UInt8, eq::EqGadget, fields::fp::FpVar};
102    use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef};
103    use ark_std::{
104        rand::{thread_rng, Rng},
105        One, UniformRand,
106    };
107    use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
108
109    use super::*;
110    use crate::arith::{
111        r1cs::{
112            extract_r1cs, extract_w_x,
113            tests::{get_test_r1cs, get_test_z},
114        },
115        Arith,
116    };
117    use crate::commitment::{pedersen::Pedersen, CommitmentScheme};
118    use crate::folding::{
119        circuits::{
120            cyclefold::{CycleFoldCommittedInstanceVar, CycleFoldWitnessVar},
121            nonnative::uint::NonNativeUintVar,
122        },
123        nova::{
124            circuits::CommittedInstanceVar, decider_eth_circuit::WitnessVar, CommittedInstance,
125            Witness,
126        },
127    };
128    use crate::frontend::{
129        utils::{CubicFCircuit, CustomFCircuit, WrapperCircuit},
130        FCircuit,
131    };
132
133    fn prepare_instances<C: CurveGroup, CS: CommitmentScheme<C>, R: Rng>(
134        mut rng: R,
135        r1cs: &R1CS<C::ScalarField>,
136        z: &[C::ScalarField],
137    ) -> (Witness<C>, CommittedInstance<C>) {
138        let (w, x) = r1cs.split_z(z);
139
140        let (cs_pp, _) = CS::setup(&mut rng, max(w.len(), r1cs.A.n_rows)).unwrap();
141
142        let mut w = Witness::new::<false>(w, r1cs.A.n_rows, &mut rng);
143        w.E = r1cs.eval_at_z(z).unwrap();
144        let mut u = w.commit::<CS, false>(&cs_pp, x).unwrap();
145        u.u = z[0];
146
147        (w, u)
148    }
149
150    #[test]
151    fn test_relaxed_r1cs_small_gadget_handcrafted() {
152        let rng = &mut thread_rng();
153
154        let r1cs: R1CS<Fr> = get_test_r1cs();
155        let mut z = get_test_z(3);
156        z[0] = Fr::rand(rng);
157        let (w, u) = prepare_instances::<_, Pedersen<Projective>, _>(rng, &r1cs, &z);
158
159        let cs = ConstraintSystem::<Fr>::new_ref();
160
161        let wVar = WitnessVar::new_witness(cs.clone(), || Ok(w)).unwrap();
162        let uVar = CommittedInstanceVar::new_witness(cs.clone(), || Ok(u)).unwrap();
163        let r1csVar =
164            R1CSMatricesVar::<Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
165
166        r1csVar.enforce_relation(&wVar, &uVar).unwrap();
167        assert!(cs.is_satisfied().unwrap());
168    }
169
170    // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been
171    // initialized.
172    fn test_relaxed_r1cs_gadget<CS: ConstraintSynthesizer<Fr>>(circuit: CS) {
173        let rng = &mut thread_rng();
174
175        let cs = ConstraintSystem::<Fr>::new_ref();
176
177        circuit.generate_constraints(cs.clone()).unwrap();
178        cs.finalize();
179        assert!(cs.is_satisfied().unwrap());
180
181        let cs = cs.into_inner().unwrap();
182
183        let r1cs = extract_r1cs::<Fr>(&cs).unwrap();
184        let (w, x) = extract_w_x::<Fr>(&cs);
185        r1cs.check_relation(&w, &x).unwrap();
186        let mut z = [vec![Fr::one()], x, w].concat();
187        z[0] = Fr::rand(rng);
188
189        let (w, u) = prepare_instances::<_, Pedersen<Projective>, _>(rng, &r1cs, &z);
190        r1cs.check_relation(&w, &u).unwrap();
191
192        // set new CS for the circuit that checks the RelaxedR1CS of our original circuit
193        let cs = ConstraintSystem::<Fr>::new_ref();
194        // prepare the inputs for our circuit
195        let wVar = WitnessVar::new_witness(cs.clone(), || Ok(w)).unwrap();
196        let uVar = CommittedInstanceVar::new_witness(cs.clone(), || Ok(u)).unwrap();
197        let r1csVar =
198            R1CSMatricesVar::<Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
199
200        r1csVar.enforce_relation(&wVar, &uVar).unwrap();
201        assert!(cs.is_satisfied().unwrap());
202    }
203
204    #[test]
205    fn test_relaxed_r1cs_small_gadget_arkworks() {
206        let z_i = vec![Fr::from(3_u32)];
207        let cubic_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
208        let circuit = WrapperCircuit::<Fr, CubicFCircuit<Fr>> {
209            FC: cubic_circuit,
210            z_i: Some(z_i.clone()),
211            z_i1: Some(cubic_circuit.step_native(0, z_i, vec![]).unwrap()),
212        };
213
214        test_relaxed_r1cs_gadget(circuit);
215    }
216
217    struct Sha256TestCircuit<F: PrimeField> {
218        _f: PhantomData<F>,
219        pub x: Vec<u8>,
220        pub y: Vec<u8>,
221    }
222    impl<F: PrimeField> ConstraintSynthesizer<F> for Sha256TestCircuit<F> {
223        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
224            let x = Vec::<UInt8<F>>::new_witness(cs.clone(), || Ok(self.x))?;
225            let y = Vec::<UInt8<F>>::new_input(cs.clone(), || Ok(self.y))?;
226
227            let unitVar = UnitVar::default();
228            let comp_y = <Sha256Gadget<F> as CRHSchemeGadget<Sha256, F>>::evaluate(&unitVar, &x)?;
229            comp_y.0.enforce_equal(&y)?;
230            Ok(())
231        }
232    }
233    #[test]
234    fn test_relaxed_r1cs_medium_gadget_arkworks() {
235        let x = Fr::from(5_u32).into_bigint().to_bytes_le();
236        let y = <Sha256 as CRHScheme>::evaluate(&(), x.clone()).unwrap();
237
238        let circuit = Sha256TestCircuit::<Fr> {
239            _f: PhantomData,
240            x,
241            y,
242        };
243        test_relaxed_r1cs_gadget(circuit);
244    }
245
246    #[test]
247    fn test_relaxed_r1cs_custom_circuit() {
248        let n_constraints = 10_000;
249        let custom_circuit = CustomFCircuit::<Fr>::new(n_constraints).unwrap();
250        let z_i = vec![Fr::from(5_u32)];
251        let circuit = WrapperCircuit::<Fr, CustomFCircuit<Fr>> {
252            FC: custom_circuit,
253            z_i: Some(z_i.clone()),
254            z_i1: Some(custom_circuit.step_native(0, z_i, vec![]).unwrap()),
255        };
256        test_relaxed_r1cs_gadget(circuit);
257    }
258
259    #[test]
260    fn test_relaxed_r1cs_nonnative_circuit() {
261        let rng = &mut thread_rng();
262
263        let cs = ConstraintSystem::<Fq>::new_ref();
264        // in practice we would use CycleFoldCircuit, but is a very big circuit (when computed
265        // non-natively inside the RelaxedR1CS circuit), so in order to have a short test we use a
266        // custom circuit.
267        let custom_circuit = CustomFCircuit::<Fq>::new(10).unwrap();
268        let z_i = vec![Fq::from(5_u32)];
269        let circuit = WrapperCircuit::<Fq, CustomFCircuit<Fq>> {
270            FC: custom_circuit,
271            z_i: Some(z_i.clone()),
272            z_i1: Some(custom_circuit.step_native(0, z_i, vec![]).unwrap()),
273        };
274        circuit.generate_constraints(cs.clone()).unwrap();
275        cs.finalize();
276        let cs = cs.into_inner().unwrap();
277        let r1cs = extract_r1cs::<Fq>(&cs).unwrap();
278        let (w, x) = extract_w_x::<Fq>(&cs);
279        let z = [vec![Fq::rand(rng)], x, w].concat();
280
281        let (w, u) = prepare_instances::<_, Pedersen<Projective2>, _>(rng, &r1cs, &z);
282
283        // natively
284        let cs = ConstraintSystem::<Fq>::new_ref();
285        let wVar = WitnessVar::new_witness(cs.clone(), || Ok(&w)).unwrap();
286        let uVar = CommittedInstanceVar::new_witness(cs.clone(), || Ok(&u)).unwrap();
287        let r1csVar =
288            R1CSMatricesVar::<Fq, FpVar<Fq>>::new_witness(cs.clone(), || Ok(&r1cs)).unwrap();
289        r1csVar.enforce_relation(&wVar, &uVar).unwrap();
290
291        // non-natively
292        let cs = ConstraintSystem::<Fr>::new_ref();
293        let wVar = CycleFoldWitnessVar::new_witness(cs.clone(), || Ok(w)).unwrap();
294        let uVar =
295            CycleFoldCommittedInstanceVar::<_, GVar2>::new_witness(cs.clone(), || Ok(u)).unwrap();
296        let r1csVar =
297            R1CSMatricesVar::<Fq, NonNativeUintVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs))
298                .unwrap();
299        r1csVar.enforce_relation(&wVar, &uVar).unwrap();
300    }
301}