sonobe/src/folding/nova/decider.rs
src/folding/nova/decider.rsRaw
1/// This file implements the onchain (Ethereum's EVM) decider circuit. For non-ethereum use cases,
2/// other more efficient approaches can be used.
3use ark_crypto_primitives::crh::poseidon::constraints::CRHParametersVar;
4use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
5use ark_ec::{CurveGroup, Group};
6use ark_ff::PrimeField;
7use ark_r1cs_std::{
8 alloc::{AllocVar, AllocationMode},
9 boolean::Boolean,
10 eq::EqGadget,
11 fields::{fp::FpVar, nonnative::NonNativeFieldVar, FieldVar},
12 groups::GroupOpsBounds,
13 prelude::CurveVar,
14 ToConstraintFieldGadget,
15};
16use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
17use ark_std::{One, Zero};
18use core::{borrow::Borrow, marker::PhantomData};
19
20use crate::ccs::r1cs::R1CS;
21use crate::folding::nova::{
22 circuits::{CommittedInstanceVar, FCircuit, CF1, CF2},
23 ivc::IVC,
24 CommittedInstance, Witness,
25};
26use crate::pedersen::Params as PedersenParams;
27use crate::utils::gadgets::{
28 hadamard, mat_vec_mul_sparse, vec_add, vec_scalar_mul, SparseMatrixVar,
29};
30
31#[derive(Debug, Clone)]
32pub struct RelaxedR1CSGadget<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>> {
33 _f: PhantomData<F>,
34 _cf: PhantomData<CF>,
35 _fv: PhantomData<FV>,
36}
37impl<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>> RelaxedR1CSGadget<F, CF, FV> {
38 /// performs the RelaxedR1CS check (Az∘Bz==uCz+E)
39 pub fn check(
40 r1cs: R1CSVar<F, CF, FV>,
41 E: Vec<FV>,
42 u: FV,
43 z: Vec<FV>,
44 ) -> Result<(), SynthesisError> {
45 let Az = mat_vec_mul_sparse(r1cs.A, z.clone());
46 let Bz = mat_vec_mul_sparse(r1cs.B, z.clone());
47 let Cz = mat_vec_mul_sparse(r1cs.C, z.clone());
48 let uCz = vec_scalar_mul(&Cz, &u);
49 let uCzE = vec_add(&uCz, &E)?;
50 let AzBz = hadamard(&Az, &Bz)?;
51 for i in 0..AzBz.len() {
52 AzBz[i].enforce_equal(&uCzE[i].clone())?;
53 }
54 Ok(())
55 }
56}
57
58#[derive(Debug, Clone)]
59pub struct R1CSVar<F: PrimeField, CF: PrimeField, FV: FieldVar<F, CF>> {
60 _f: PhantomData<F>,
61 _cf: PhantomData<CF>,
62 _fv: PhantomData<FV>,
63 pub A: SparseMatrixVar<F, CF, FV>,
64 pub B: SparseMatrixVar<F, CF, FV>,
65 pub C: SparseMatrixVar<F, CF, FV>,
66}
67
68impl<F, CF, FV> AllocVar<R1CS<F>, CF> for R1CSVar<F, CF, FV>
69where
70 F: PrimeField,
71 CF: PrimeField,
72 FV: FieldVar<F, CF>,
73{
74 fn new_variable<T: Borrow<R1CS<F>>>(
75 cs: impl Into<Namespace<CF>>,
76 f: impl FnOnce() -> Result<T, SynthesisError>,
77 _mode: AllocationMode,
78 ) -> Result<Self, SynthesisError> {
79 f().and_then(|val| {
80 let cs = cs.into();
81
82 let A = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().A)?;
83 let B = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().B)?;
84 let C = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().C)?;
85
86 Ok(Self {
87 _f: PhantomData,
88 _cf: PhantomData,
89 _fv: PhantomData,
90 A,
91 B,
92 C,
93 })
94 })
95 }
96}
97
98/// In-circuit representation of the Witness associated to the CommittedInstance.
99#[derive(Debug, Clone)]
100pub struct WitnessVar<C: CurveGroup> {
101 pub E: Vec<FpVar<C::ScalarField>>,
102 pub rE: FpVar<C::ScalarField>,
103 pub W: Vec<FpVar<C::ScalarField>>,
104 pub rW: FpVar<C::ScalarField>,
105}
106
107impl<C> AllocVar<Witness<C>, CF1<C>> for WitnessVar<C>
108where
109 C: CurveGroup,
110 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
111{
112 fn new_variable<T: Borrow<Witness<C>>>(
113 cs: impl Into<Namespace<CF1<C>>>,
114 f: impl FnOnce() -> Result<T, SynthesisError>,
115 mode: AllocationMode,
116 ) -> Result<Self, SynthesisError> {
117 f().and_then(|val| {
118 let cs = cs.into();
119
120 let E: Vec<FpVar<C::ScalarField>> =
121 Vec::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?;
122 let rE =
123 FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().rE), mode)?;
124
125 let W: Vec<FpVar<C::ScalarField>> =
126 Vec::new_variable(cs.clone(), || Ok(val.borrow().W.clone()), mode)?;
127 let rW =
128 FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().rW), mode)?;
129
130 Ok(Self { E, rE, W, rW })
131 })
132 }
133}
134
135/// In-circuit representation of the Witness associated to the CommittedInstance, but with
136/// non-native representation, since it is used to represent the CycleFold witness.
137#[derive(Debug, Clone)]
138pub struct CycleFoldWitnessVar<C: CurveGroup> {
139 pub E: Vec<NonNativeFieldVar<C::ScalarField, CF2<C>>>,
140 pub rE: NonNativeFieldVar<C::ScalarField, CF2<C>>,
141 pub W: Vec<NonNativeFieldVar<C::ScalarField, CF2<C>>>,
142 pub rW: NonNativeFieldVar<C::ScalarField, CF2<C>>,
143}
144
145impl<C> AllocVar<Witness<C>, CF2<C>> for CycleFoldWitnessVar<C>
146where
147 C: CurveGroup,
148 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
149{
150 fn new_variable<T: Borrow<Witness<C>>>(
151 cs: impl Into<Namespace<CF2<C>>>,
152 f: impl FnOnce() -> Result<T, SynthesisError>,
153 mode: AllocationMode,
154 ) -> Result<Self, SynthesisError> {
155 f().and_then(|val| {
156 let cs = cs.into();
157
158 let E: Vec<NonNativeFieldVar<C::ScalarField, CF2<C>>> =
159 Vec::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?;
160 let rE = NonNativeFieldVar::<C::ScalarField, CF2<C>>::new_variable(
161 cs.clone(),
162 || Ok(val.borrow().rE),
163 mode,
164 )?;
165
166 let W: Vec<NonNativeFieldVar<C::ScalarField, CF2<C>>> =
167 Vec::new_variable(cs.clone(), || Ok(val.borrow().W.clone()), mode)?;
168 let rW = NonNativeFieldVar::<C::ScalarField, CF2<C>>::new_variable(
169 cs.clone(),
170 || Ok(val.borrow().rW),
171 mode,
172 )?;
173
174 Ok(Self { E, rE, W, rW })
175 })
176 }
177}
178
179/// Circuit that implements the in-circuit checks needed for the onchain (Ethereum's EVM)
180/// verification.
181pub struct DeciderCircuit<C1, GC1, C2, GC2>
182where
183 C1: CurveGroup,
184 GC1: CurveVar<C1, CF2<C1>>,
185 C2: CurveGroup,
186 GC2: CurveVar<C2, CF2<C2>>,
187{
188 _c1: PhantomData<C1>,
189 _gc1: PhantomData<GC1>,
190 _c2: PhantomData<C2>,
191 _gc2: PhantomData<GC2>,
192
193 /// E vector's length of the Nova instance witness
194 pub E_len: usize,
195 /// E vector's length of the CycleFold instance witness
196 pub cf_E_len: usize,
197 /// R1CS of the Augmented Function circuit
198 pub r1cs: R1CS<C1::ScalarField>,
199 /// R1CS of the CycleFold circuit
200 pub cf_r1cs: R1CS<C2::ScalarField>,
201 /// CycleFold PedersenParams, over C2
202 pub cf_pedersen_params: PedersenParams<C2>,
203 pub poseidon_config: PoseidonConfig<CF1<C1>>,
204 pub i: Option<CF1<C1>>,
205 /// initial state
206 pub z_0: Option<Vec<C1::ScalarField>>,
207 /// current i-th state
208 pub z_i: Option<Vec<C1::ScalarField>>,
209 /// Nova instances
210 pub u_i: Option<CommittedInstance<C1>>,
211 pub w_i: Option<Witness<C1>>,
212 pub U_i: Option<CommittedInstance<C1>>,
213 pub W_i: Option<Witness<C1>>,
214 /// CycleFold running instance
215 pub cf_U_i: Option<CommittedInstance<C2>>,
216 pub cf_W_i: Option<Witness<C2>>,
217}
218impl<C1, GC1, C2, GC2> DeciderCircuit<C1, GC1, C2, GC2>
219where
220 C1: CurveGroup,
221 C2: CurveGroup,
222 GC1: CurveVar<C1, CF2<C1>>,
223 GC2: CurveVar<C2, CF2<C2>>,
224{
225 pub fn from_ivc<FC: FCircuit<C1::ScalarField>>(ivc: IVC<C1, GC1, C2, GC2, FC>) -> Self {
226 Self {
227 _c1: PhantomData,
228 _gc1: PhantomData,
229 _c2: PhantomData,
230 _gc2: PhantomData,
231
232 E_len: ivc.W_i.E.len(),
233 cf_E_len: ivc.cf_W_i.E.len(),
234 r1cs: ivc.r1cs,
235 cf_r1cs: ivc.cf_r1cs,
236 cf_pedersen_params: ivc.cf_pedersen_params,
237 poseidon_config: ivc.poseidon_config,
238 i: Some(ivc.i),
239 z_0: Some(ivc.z_0),
240 z_i: Some(ivc.z_i),
241 u_i: Some(ivc.u_i),
242 w_i: Some(ivc.w_i),
243 U_i: Some(ivc.U_i),
244 W_i: Some(ivc.W_i),
245 cf_U_i: Some(ivc.cf_U_i),
246 cf_W_i: Some(ivc.cf_W_i),
247 }
248 }
249}
250
251impl<C1, GC1, C2, GC2> ConstraintSynthesizer<CF1<C1>> for DeciderCircuit<C1, GC1, C2, GC2>
252where
253 C1: CurveGroup,
254 C2: CurveGroup,
255 GC1: CurveVar<C1, CF2<C1>>,
256 GC2: CurveVar<C2, CF2<C2>>,
257 <C1 as CurveGroup>::BaseField: PrimeField,
258 <C2 as CurveGroup>::BaseField: PrimeField,
259 <C1 as Group>::ScalarField: Absorb,
260 <C2 as Group>::ScalarField: Absorb,
261 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
262 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
263{
264 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
265 let r1cs =
266 R1CSVar::<C1::ScalarField, CF1<C1>, FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
267 Ok(self.r1cs.clone())
268 })?;
269
270 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
271 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
272 })?;
273 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
274 Ok(self.z_0.unwrap_or(vec![CF1::<C1>::zero()]))
275 })?;
276 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
277 Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
278 })?;
279
280 let u_dummy_native = CommittedInstance::<C1>::dummy(1);
281 let w_dummy_native = Witness::<C1>::new(
282 vec![C1::ScalarField::zero(); self.r1cs.A.n_cols - 2 /* (2=1+1, since u_i.x.len=1) */],
283 self.E_len,
284 );
285
286 let u_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
287 Ok(self.u_i.unwrap_or(u_dummy_native.clone()))
288 })?;
289 let w_i = WitnessVar::<C1>::new_witness(cs.clone(), || {
290 Ok(self.w_i.unwrap_or(w_dummy_native.clone()))
291 })?;
292 let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
293 Ok(self.U_i.unwrap_or(u_dummy_native.clone()))
294 })?;
295 let W_i = WitnessVar::<C1>::new_witness(cs.clone(), || {
296 Ok(self.W_i.unwrap_or(w_dummy_native.clone()))
297 })?;
298
299 let crh_params = CRHParametersVar::<C1::ScalarField>::new_constant(
300 cs.clone(),
301 self.poseidon_config.clone(),
302 )?;
303
304 // 1. check RelaxedR1CS of u_i
305 let z_u: Vec<FpVar<CF1<C1>>> = [
306 vec![FpVar::<CF1<C1>>::one()],
307 u_i.x.to_vec(),
308 w_i.W.to_vec(),
309 ]
310 .concat();
311 RelaxedR1CSGadget::<C1::ScalarField, CF1<C1>, FpVar<CF1<C1>>>::check(
312 r1cs.clone(),
313 w_i.E,
314 u_i.u.clone(),
315 z_u,
316 )?;
317
318 // 2. check RelaxedR1CS of U_i
319 let z_U: Vec<FpVar<CF1<C1>>> =
320 [vec![U_i.u.clone()], U_i.x.to_vec(), W_i.W.to_vec()].concat();
321 RelaxedR1CSGadget::<C1::ScalarField, CF1<C1>, FpVar<CF1<C1>>>::check(
322 r1cs,
323 W_i.E,
324 U_i.u.clone(),
325 z_U,
326 )?;
327
328 // 3. u_i.cmE==cm(0), u_i.u==1
329 // Here zero_x & zero_y are the x & y coordinates of the zero point affine representation.
330 let zero_x = NonNativeFieldVar::<C1::BaseField, C1::ScalarField>::new_constant(
331 cs.clone(),
332 C1::BaseField::zero(),
333 )?
334 .to_constraint_field()?;
335 let zero_y = NonNativeFieldVar::<C1::BaseField, C1::ScalarField>::new_constant(
336 cs.clone(),
337 C1::BaseField::one(),
338 )?
339 .to_constraint_field()?;
340 (u_i.cmE.x.is_eq(&zero_x)?).enforce_equal(&Boolean::TRUE)?;
341 (u_i.cmE.y.is_eq(&zero_y)?).enforce_equal(&Boolean::TRUE)?;
342 (u_i.u.is_one()?).enforce_equal(&Boolean::TRUE)?;
343
344 // 4. u_i.x == H(i, z_0, z_i, U_i)
345 let u_i_x = U_i
346 .clone()
347 .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
348 (u_i.x[0]).enforce_equal(&u_i_x)?;
349
350 // The following two checks (and their respective allocations) are disabled for normal
351 // tests since they take ~24.5M constraints and would take several minutes (and RAM) to run
352 // the test
353 #[cfg(not(test))]
354 {
355 // imports here instead of at the top of the file, so we avoid having multiple
356 // `#[cfg(not(test))]
357 use crate::folding::nova::cyclefold::{CycleFoldCommittedInstanceVar, CF_IO_LEN};
358 use crate::pedersen::PedersenGadget;
359 use ark_r1cs_std::ToBitsGadget;
360
361 let cf_r1cs = R1CSVar::<
362 C1::BaseField,
363 CF1<C1>,
364 NonNativeFieldVar<C1::BaseField, CF1<C1>>,
365 >::new_witness(cs.clone(), || Ok(self.cf_r1cs.clone()))?;
366
367 let cf_u_dummy_native = CommittedInstance::<C2>::dummy(CF_IO_LEN);
368 let w_dummy_native = Witness::<C2>::new(
369 vec![C2::ScalarField::zero(); self.cf_r1cs.A.n_cols - 1 - self.cf_r1cs.l],
370 self.cf_E_len,
371 );
372 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
373 Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
374 })?;
375 let cf_W_i = CycleFoldWitnessVar::<C2>::new_witness(cs.clone(), || {
376 Ok(self.cf_W_i.unwrap_or(w_dummy_native.clone()))
377 })?;
378
379 // 5. check Pedersen commitments of cf_U_i.{cmE, cmW}
380 let H = GC2::new_constant(cs.clone(), self.cf_pedersen_params.h)?;
381 let G = Vec::<GC2>::new_constant(cs.clone(), self.cf_pedersen_params.generators)?;
382 let cf_W_i_E_bits: Vec<Vec<Boolean<CF1<C1>>>> = cf_W_i
383 .E
384 .iter()
385 .map(|E_i| E_i.to_bits_le().unwrap())
386 .collect();
387 let cf_W_i_W_bits: Vec<Vec<Boolean<CF1<C1>>>> = cf_W_i
388 .W
389 .iter()
390 .map(|W_i| W_i.to_bits_le().unwrap())
391 .collect();
392
393 let computed_cmE = PedersenGadget::<C2, GC2>::commit(
394 H.clone(),
395 G.clone(),
396 cf_W_i_E_bits,
397 cf_W_i.rE.to_bits_le()?,
398 )?;
399 cf_U_i.cmE.enforce_equal(&computed_cmE)?;
400 let computed_cmW =
401 PedersenGadget::<C2, GC2>::commit(H, G, cf_W_i_W_bits, cf_W_i.rW.to_bits_le()?)?;
402 cf_U_i.cmW.enforce_equal(&computed_cmW)?;
403
404 // 6. check RelaxedR1CS of cf_U_i
405 let cf_z_U: Vec<NonNativeFieldVar<C2::ScalarField, CF1<C1>>> =
406 [vec![cf_U_i.u.clone()], cf_U_i.x.to_vec(), cf_W_i.W.to_vec()].concat();
407 RelaxedR1CSGadget::<
408 C2::ScalarField,
409 CF1<C1>,
410 NonNativeFieldVar<C2::ScalarField, CF1<C1>>,
411 >::check(cf_r1cs, cf_W_i.E, cf_U_i.u.clone(), cf_z_U)?;
412 }
413
414 Ok(())
415 }
416}
417
418#[cfg(test)]
419pub mod tests {
420 use super::*;
421 use ark_crypto_primitives::crh::{
422 sha256::{
423 constraints::{Sha256Gadget, UnitVar},
424 Sha256,
425 },
426 CRHScheme, CRHSchemeGadget,
427 };
428 use ark_ff::BigInteger;
429 use ark_pallas::{constraints::GVar, Fq, Fr, Projective};
430 use ark_r1cs_std::{
431 alloc::AllocVar,
432 bits::uint8::UInt8,
433 eq::EqGadget,
434 fields::{fp::FpVar, nonnative::NonNativeFieldVar},
435 };
436 use ark_relations::r1cs::ConstraintSystem;
437 use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
438
439 use crate::folding::nova::circuits::{tests::TestFCircuit, FCircuit};
440 use crate::folding::nova::ivc::IVC;
441 use crate::transcript::poseidon::tests::poseidon_test_config;
442
443 use crate::ccs::r1cs::{
444 tests::{get_test_r1cs, get_test_z},
445 R1CS,
446 };
447 use crate::frontend::arkworks::{extract_r1cs_and_z, tests::TestCircuit};
448
449 #[test]
450 fn test_relaxed_r1cs_small_gadget_handcrafted() {
451 let r1cs: R1CS<Fr> = get_test_r1cs();
452 let rel_r1cs = r1cs.clone().relax();
453 let z = get_test_z(3);
454
455 let cs = ConstraintSystem::<Fr>::new_ref();
456
457 let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
458 let EVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(rel_r1cs.E)).unwrap();
459 let uVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(rel_r1cs.u)).unwrap();
460 let r1csVar = R1CSVar::<Fr, Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
461
462 RelaxedR1CSGadget::<Fr, Fr, FpVar<Fr>>::check(r1csVar, EVar, uVar, zVar).unwrap();
463 assert!(cs.is_satisfied().unwrap());
464 }
465
466 // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been
467 // initialized.
468 fn test_relaxed_r1cs_gadget<CS: ConstraintSynthesizer<Fr>>(circuit: CS) {
469 let cs = ConstraintSystem::<Fr>::new_ref();
470
471 circuit.generate_constraints(cs.clone()).unwrap();
472 cs.finalize();
473 assert!(cs.is_satisfied().unwrap());
474
475 let cs = cs.into_inner().unwrap();
476
477 let (r1cs, z) = extract_r1cs_and_z::<Fr>(&cs);
478 r1cs.check_relation(&z).unwrap();
479
480 let relaxed_r1cs = r1cs.clone().relax();
481 relaxed_r1cs.check_relation(&z).unwrap();
482
483 // set new CS for the circuit that checks the RelaxedR1CS of our original circuit
484 let cs = ConstraintSystem::<Fr>::new_ref();
485 // prepare the inputs for our circuit
486 let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
487 let EVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(relaxed_r1cs.E)).unwrap();
488 let uVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
489 let r1csVar = R1CSVar::<Fr, Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
490
491 RelaxedR1CSGadget::<Fr, Fr, FpVar<Fr>>::check(r1csVar, EVar, uVar, zVar).unwrap();
492 assert!(cs.is_satisfied().unwrap());
493 }
494
495 #[test]
496 fn test_relaxed_r1cs_small_gadget_arkworks() {
497 let x = Fr::from(5_u32);
498 let y = x * x * x + x + Fr::from(5_u32);
499 let circuit = TestCircuit::<Fr> { x, y };
500 test_relaxed_r1cs_gadget(circuit);
501 }
502
503 struct Sha256TestCircuit<F: PrimeField> {
504 _f: PhantomData<F>,
505 pub x: Vec<u8>,
506 pub y: Vec<u8>,
507 }
508 impl<F: PrimeField> ConstraintSynthesizer<F> for Sha256TestCircuit<F> {
509 fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
510 let x = Vec::<UInt8<F>>::new_witness(cs.clone(), || Ok(self.x))?;
511 let y = Vec::<UInt8<F>>::new_input(cs.clone(), || Ok(self.y))?;
512
513 let unitVar = UnitVar::default();
514 let comp_y = <Sha256Gadget<F> as CRHSchemeGadget<Sha256, F>>::evaluate(&unitVar, &x)?;
515 comp_y.0.enforce_equal(&y)?;
516 Ok(())
517 }
518 }
519 #[test]
520 fn test_relaxed_r1cs_medium_gadget_arkworks() {
521 let x = Fr::from(5_u32).into_bigint().to_bytes_le();
522 let y = <Sha256 as CRHScheme>::evaluate(&(), x.clone()).unwrap();
523
524 let circuit = Sha256TestCircuit::<Fr> {
525 _f: PhantomData,
526 x,
527 y,
528 };
529 test_relaxed_r1cs_gadget(circuit);
530 }
531
532 // circuit that has the number of constraints specified in the `n_constraints` parameter. Note
533 // that the generated circuit will have very sparse matrices, so the resulting constraints
534 // number of the RelaxedR1CS gadget must take that into account.
535 struct CustomTestCircuit<F: PrimeField> {
536 _f: PhantomData<F>,
537 pub n_constraints: usize,
538 pub x: F,
539 pub y: F,
540 }
541 impl<F: PrimeField> CustomTestCircuit<F> {
542 fn new(n_constraints: usize) -> Self {
543 let x = F::from(5_u32);
544 let mut y = F::one();
545 for _ in 0..n_constraints - 1 {
546 y *= x;
547 }
548 Self {
549 _f: PhantomData,
550 n_constraints,
551 x,
552 y,
553 }
554 }
555 }
556 impl<F: PrimeField> ConstraintSynthesizer<F> for CustomTestCircuit<F> {
557 fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
558 let x = FpVar::<F>::new_witness(cs.clone(), || Ok(self.x))?;
559 let y = FpVar::<F>::new_input(cs.clone(), || Ok(self.y))?;
560
561 let mut comp_y = FpVar::<F>::new_witness(cs.clone(), || Ok(F::one()))?;
562 for _ in 0..self.n_constraints - 1 {
563 comp_y *= x.clone();
564 }
565
566 comp_y.enforce_equal(&y)?;
567 Ok(())
568 }
569 }
570
571 #[test]
572 fn test_relaxed_r1cs_custom_circuit() {
573 let n_constraints = 10_000;
574 let x = Fr::from(5_u32);
575 let mut y = Fr::one();
576 for _ in 0..n_constraints - 1 {
577 y *= x;
578 }
579
580 let circuit = CustomTestCircuit::<Fr> {
581 _f: PhantomData,
582 n_constraints,
583 x,
584 y,
585 };
586 test_relaxed_r1cs_gadget(circuit);
587 }
588
589 #[test]
590 fn test_relaxed_r1cs_nonnative_circuit() {
591 let cs = ConstraintSystem::<Fq>::new_ref();
592 // in practice we would use CycleFoldCircuit, but is a very big circuit (when computed
593 // non-natively inside the RelaxedR1CS circuit), so in order to have a short test we use a
594 // custom circuit.
595 let circuit = CustomTestCircuit::<Fq>::new(10);
596 circuit.generate_constraints(cs.clone()).unwrap();
597 cs.finalize();
598 let cs = cs.into_inner().unwrap();
599 let (r1cs, z) = extract_r1cs_and_z::<Fq>(&cs);
600
601 let relaxed_r1cs = r1cs.clone().relax();
602
603 // natively
604 let cs = ConstraintSystem::<Fq>::new_ref();
605 let zVar = Vec::<FpVar<Fq>>::new_witness(cs.clone(), || Ok(z.clone())).unwrap();
606 let EVar =
607 Vec::<FpVar<Fq>>::new_witness(cs.clone(), || Ok(relaxed_r1cs.clone().E)).unwrap();
608 let uVar = FpVar::<Fq>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
609 let r1csVar =
610 R1CSVar::<Fq, Fq, FpVar<Fq>>::new_witness(cs.clone(), || Ok(r1cs.clone())).unwrap();
611 RelaxedR1CSGadget::<Fq, Fq, FpVar<Fq>>::check(r1csVar, EVar, uVar, zVar).unwrap();
612
613 // non-natively
614 let cs = ConstraintSystem::<Fr>::new_ref();
615 let zVar = Vec::<NonNativeFieldVar<Fq, Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
616 let EVar = Vec::<NonNativeFieldVar<Fq, Fr>>::new_witness(cs.clone(), || Ok(relaxed_r1cs.E))
617 .unwrap();
618 let uVar =
619 NonNativeFieldVar::<Fq, Fr>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
620 let r1csVar =
621 R1CSVar::<Fq, Fr, NonNativeFieldVar<Fq, Fr>>::new_witness(cs.clone(), || Ok(r1cs))
622 .unwrap();
623 RelaxedR1CSGadget::<Fq, Fr, NonNativeFieldVar<Fq, Fr>>::check(r1csVar, EVar, uVar, zVar)
624 .unwrap();
625 }
626
627 #[test]
628 fn test_decider_circuit() {
629 let mut rng = ark_std::test_rng();
630 let poseidon_config = poseidon_test_config::<Fr>();
631
632 let F_circuit = TestFCircuit::<Fr>::new();
633 let z_0 = vec![Fr::from(3_u32)];
634
635 // generate an IVC and do a step of it
636 let mut ivc = IVC::<Projective, GVar, Projective2, GVar2, TestFCircuit<Fr>>::new(
637 &mut rng,
638 poseidon_config,
639 F_circuit,
640 z_0.clone(),
641 )
642 .unwrap();
643 ivc.prove_step().unwrap();
644 ivc.verify(z_0, 1).unwrap();
645
646 // load the DeciderCircuit from the generated IVC
647 let decider_circuit = DeciderCircuit::<Projective, GVar, Projective2, GVar2>::from_ivc(ivc);
648
649 let cs = ConstraintSystem::<Fr>::new_ref();
650
651 // generate the constraints and check that are satisfied by the inputs
652 decider_circuit.generate_constraints(cs.clone()).unwrap();
653 assert!(cs.is_satisfied().unwrap());
654 dbg!(cs.num_constraints());
655 }
656}