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