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