sonobe/folding-schemes/src/folding/nova/decider_circuits.rs
folding-schemes/src/folding/nova/decider_circuits.rsRaw
1/// This file implements the offchain decider circuit. For ethereum use cases, use the
2/// DeciderEthCircuit.
3/// More details can be found at the documentation page:
4/// https://privacy-scaling-explorations.github.io/sonobe-docs/design/nova-decider-offchain.html
5use ark_crypto_primitives::sponge::{
6 constraints::CryptographicSpongeVar,
7 poseidon::{constraints::PoseidonSpongeVar, PoseidonConfig, PoseidonSponge},
8 Absorb, CryptographicSponge,
9};
10use ark_ec::{CurveGroup, Group};
11use ark_ff::{BigInteger, PrimeField};
12use ark_poly::Polynomial;
13use ark_r1cs_std::{
14 alloc::AllocVar,
15 boolean::Boolean,
16 eq::EqGadget,
17 fields::{fp::FpVar, FieldVar},
18 groups::GroupOpsBounds,
19 prelude::CurveVar,
20 ToConstraintFieldGadget,
21};
22use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, SynthesisError};
23use ark_std::Zero;
24use core::marker::PhantomData;
25
26use super::{
27 circuits::{ChallengeGadget, CommittedInstanceVar},
28 decider_eth_circuit::{
29 evaluate_gadget, KZGChallengesGadget, R1CSVar, RelaxedR1CSGadget, WitnessVar,
30 },
31 nifs::NIFS,
32 traits::NIFSTrait,
33 CommittedInstance, Nova, Witness,
34};
35use crate::arith::r1cs::R1CS;
36use crate::commitment::CommitmentScheme;
37use crate::folding::circuits::{
38 cyclefold::{
39 CycleFoldCommittedInstance, CycleFoldCommittedInstanceVar, CycleFoldConfig,
40 CycleFoldWitness,
41 },
42 nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
43 CF1, CF2,
44};
45use crate::folding::nova::NovaCycleFoldConfig;
46use crate::folding::traits::{CommittedInstanceVarOps, Dummy};
47use crate::frontend::FCircuit;
48use crate::utils::vec::poly_from_vec;
49use crate::Error;
50
51/// Circuit that implements part of the in-circuit checks needed for the offchain verification over
52/// the Curve2's BaseField (=Curve1's ScalarField).
53#[derive(Clone, Debug)]
54pub struct DeciderCircuit1<C1, C2, GC2>
55where
56 C1: CurveGroup,
57 C2: CurveGroup,
58 GC2: CurveVar<C2, CF2<C2>>,
59{
60 _c1: PhantomData<C1>,
61 _c2: PhantomData<C2>,
62 _gc2: PhantomData<GC2>,
63
64 /// E vector's length of the Nova instance witness
65 pub E_len: usize,
66 /// E vector's length of the CycleFold instance witness
67 pub cf_E_len: usize,
68 /// R1CS of the Augmented Function circuit
69 pub r1cs: R1CS<C1::ScalarField>,
70 pub poseidon_config: PoseidonConfig<CF1<C1>>,
71 /// public params hash
72 pub pp_hash: Option<C1::ScalarField>,
73 pub i: Option<CF1<C1>>,
74 /// initial state
75 pub z_0: Option<Vec<C1::ScalarField>>,
76 /// current i-th state
77 pub z_i: Option<Vec<C1::ScalarField>>,
78 /// Nova instances
79 pub u_i: Option<CommittedInstance<C1>>,
80 pub w_i: Option<Witness<C1>>,
81 pub U_i: Option<CommittedInstance<C1>>,
82 pub W_i: Option<Witness<C1>>,
83 pub U_i1: Option<CommittedInstance<C1>>,
84 pub W_i1: Option<Witness<C1>>,
85 pub cmT: Option<C1>,
86 pub r: Option<C1::ScalarField>,
87 /// CycleFold running instance
88 pub cf_U_i: Option<CycleFoldCommittedInstance<C2>>,
89
90 /// Commitment Scheme challenges
91 pub cs_c_W: Option<C1::ScalarField>,
92 pub cs_c_E: Option<C1::ScalarField>,
93 /// Evaluations of the committed polynomials at the challenge
94 pub eval_W: Option<C1::ScalarField>,
95 pub eval_E: Option<C1::ScalarField>,
96}
97impl<C1, C2, GC2> DeciderCircuit1<C1, C2, GC2>
98where
99 C1: CurveGroup,
100 <C1 as CurveGroup>::BaseField: PrimeField,
101 <C1 as Group>::ScalarField: Absorb,
102 C2: CurveGroup,
103 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
104 for<'b> &'b GC2: GroupOpsBounds<'b, C2, GC2>,
105{
106 pub fn from_nova<GC1, CS1, CS2, const H: bool, FC: FCircuit<C1::ScalarField>>(
107 nova: Nova<C1, GC1, C2, GC2, FC, CS1, CS2, H>,
108 ) -> Result<Self, Error>
109 where
110 C2: CurveGroup,
111 GC1: CurveVar<C1, CF2<C1>> + ToConstraintFieldGadget<CF2<C1>>,
112 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
113 CS1: CommitmentScheme<C1, H>,
114 CS2: CommitmentScheme<C2, H>,
115 {
116 let mut transcript = PoseidonSponge::<C1::ScalarField>::new(&nova.poseidon_config);
117 // pp_hash is absorbed to transcript at the ChallengeGadget::get_challenge_native call
118
119 // compute the U_{i+1}, W_{i+1}
120 let (T, cmT) = NIFS::<C1, CS1, H>::compute_cmT(
121 &nova.cs_pp,
122 &nova.r1cs.clone(),
123 &nova.w_i.clone(),
124 &nova.u_i.clone(),
125 &nova.W_i.clone(),
126 &nova.U_i.clone(),
127 )?;
128 let r_bits = NIFS::<C1, CS1, H>::get_challenge(
129 &mut transcript,
130 nova.pp_hash,
131 &nova.U_i,
132 &nova.u_i,
133 &cmT,
134 );
135 let r_Fr = C1::ScalarField::from_bigint(BigInteger::from_bits_le(&r_bits))
136 .ok_or(Error::OutOfBounds)?;
137 let (W_i1, U_i1) =
138 NIFS::<C1, CS1, H>::prove(r_Fr, &nova.W_i, &nova.U_i, &nova.w_i, &nova.u_i, &T, &cmT)?;
139
140 // compute the commitment scheme challenges used as inputs in the circuit
141 let (cs_challenge_W, cs_challenge_E) =
142 KZGChallengesGadget::<C1>::get_challenges_native(&mut transcript, U_i1.clone());
143
144 // get evals of the committed polys at the challenges
145 let mut W = W_i1.W.clone();
146 W.extend(
147 std::iter::repeat(C1::ScalarField::zero())
148 .take(W_i1.W.len().next_power_of_two() - W_i1.W.len()),
149 );
150 let mut E = W_i1.E.clone();
151 E.extend(
152 std::iter::repeat(C1::ScalarField::zero())
153 .take(W_i1.E.len().next_power_of_two() - W_i1.E.len()),
154 );
155 let p_W = poly_from_vec(W.to_vec())?;
156 let eval_W = p_W.evaluate(&cs_challenge_W);
157 let p_E = poly_from_vec(E.to_vec())?;
158 let eval_E = p_E.evaluate(&cs_challenge_E);
159
160 Ok(Self {
161 _c1: PhantomData,
162 _c2: PhantomData,
163 _gc2: PhantomData,
164
165 E_len: nova.W_i.E.len(),
166 cf_E_len: nova.cf_W_i.E.len(),
167 r1cs: nova.r1cs,
168 poseidon_config: nova.poseidon_config,
169 pp_hash: Some(nova.pp_hash),
170 i: Some(nova.i),
171 z_0: Some(nova.z_0),
172 z_i: Some(nova.z_i),
173 u_i: Some(nova.u_i),
174 w_i: Some(nova.w_i),
175 U_i: Some(nova.U_i),
176 W_i: Some(nova.W_i),
177 U_i1: Some(U_i1),
178 W_i1: Some(W_i1),
179 cmT: Some(cmT),
180 r: Some(r_Fr),
181 cf_U_i: Some(nova.cf_U_i),
182 cs_c_W: Some(cs_challenge_W),
183 cs_c_E: Some(cs_challenge_E),
184 eval_W: Some(eval_W),
185 eval_E: Some(eval_E),
186 })
187 }
188}
189
190impl<C1, C2, GC2> ConstraintSynthesizer<CF1<C1>> for DeciderCircuit1<C1, C2, GC2>
191where
192 C1: CurveGroup,
193 <C1 as CurveGroup>::BaseField: PrimeField,
194 <C1 as Group>::ScalarField: Absorb,
195 C2: CurveGroup,
196 <C2 as CurveGroup>::BaseField: PrimeField,
197 <C2 as Group>::ScalarField: Absorb,
198 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
199 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
200 for<'b> &'b GC2: GroupOpsBounds<'b, C2, GC2>,
201{
202 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
203 let r1cs =
204 R1CSVar::<C1::ScalarField, CF1<C1>, FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
205 Ok(self.r1cs.clone())
206 })?;
207
208 let pp_hash = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
209 Ok(self.pp_hash.unwrap_or_else(CF1::<C1>::zero))
210 })?;
211 let i =
212 FpVar::<CF1<C1>>::new_input(cs.clone(), || Ok(self.i.unwrap_or_else(CF1::<C1>::zero)))?;
213 let z_0 = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
214 Ok(self.z_0.unwrap_or(vec![CF1::<C1>::zero()]))
215 })?;
216 let z_i = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
217 Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
218 })?;
219
220 let u_dummy_native = CommittedInstance::<C1>::dummy(&self.r1cs);
221 let w_dummy_native = Witness::<C1>::dummy(&self.r1cs);
222
223 let u_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
224 Ok(self.u_i.unwrap_or(u_dummy_native.clone()))
225 })?;
226 let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
227 Ok(self.U_i.unwrap_or(u_dummy_native.clone()))
228 })?;
229 // here (U_i1, W_i1) = NIFS.P( (U_i,W_i), (u_i,w_i))
230 let U_i1 = CommittedInstanceVar::<C1>::new_input(cs.clone(), || {
231 Ok(self.U_i1.unwrap_or(u_dummy_native.clone()))
232 })?;
233 let W_i1 = WitnessVar::<C1>::new_witness(cs.clone(), || {
234 Ok(self.W_i1.unwrap_or(w_dummy_native.clone()))
235 })?;
236
237 // allocate the inputs for the check 6
238 let cs_c_W = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
239 Ok(self.cs_c_W.unwrap_or_else(CF1::<C1>::zero))
240 })?;
241 let cs_c_E = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
242 Ok(self.cs_c_E.unwrap_or_else(CF1::<C1>::zero))
243 })?;
244 let eval_W = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
245 Ok(self.eval_W.unwrap_or_else(CF1::<C1>::zero))
246 })?;
247 let eval_E = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
248 Ok(self.eval_E.unwrap_or_else(CF1::<C1>::zero))
249 })?;
250
251 // `sponge` is for digest computation.
252 let sponge = PoseidonSpongeVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
253 // `transcript` is for challenge generation.
254 let mut transcript = sponge.clone();
255 // notice that the `pp_hash` is absorbed inside the ChallengeGadget::get_challenge_gadget call
256
257 // 2. u_i.cmE==cm(0), u_i.u==1
258 // Here zero is the x & y coordinates of the zero point affine representation.
259 let zero = NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::zero())?;
260 u_i.cmE.x.enforce_equal_unaligned(&zero)?;
261 u_i.cmE.y.enforce_equal_unaligned(&zero)?;
262 (u_i.u.is_one()?).enforce_equal(&Boolean::TRUE)?;
263
264 // 3.a u_i.x[0] == H(i, z_0, z_i, U_i)
265 let (u_i_x, U_i_vec) = U_i.clone().hash(&sponge, &pp_hash, &i, &z_0, &z_i)?;
266 (u_i.x[0]).enforce_equal(&u_i_x)?;
267
268 // 3.b u_i.x[1] == H(cf_U_i)
269 let cf_u_dummy_native =
270 CycleFoldCommittedInstance::<C2>::dummy(NovaCycleFoldConfig::<C1>::IO_LEN);
271 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_input(cs.clone(), || {
272 Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
273 })?;
274 let (cf_u_i_x, _) = cf_U_i.clone().hash(&sponge, pp_hash.clone())?;
275 (u_i.x[1]).enforce_equal(&cf_u_i_x)?;
276
277 // 4. check RelaxedR1CS of U_{i+1}
278 let z_U1: Vec<FpVar<CF1<C1>>> =
279 [vec![U_i1.u.clone()], U_i1.x.to_vec(), W_i1.W.to_vec()].concat();
280 RelaxedR1CSGadget::check_native(r1cs, W_i1.E.clone(), U_i1.u.clone(), z_U1)?;
281
282 // 1.1.a, 5.1 compute NIFS.V and Commitment Scheme challenges.
283 // We need to ensure the order of challenge generation is the same as
284 // the native counterpart, so we first compute the challenges here and
285 // do the actual checks later.
286 let cmT =
287 NonNativeAffineVar::new_input(cs.clone(), || Ok(self.cmT.unwrap_or_else(C1::zero)))?;
288 let r_bits = ChallengeGadget::<C1, CommittedInstance<C1>>::get_challenge_gadget(
289 &mut transcript,
290 pp_hash,
291 U_i_vec,
292 u_i.clone(),
293 Some(cmT.clone()),
294 )?;
295 // 5.1.
296 let (incircuit_c_W, incircuit_c_E) =
297 KZGChallengesGadget::<C1>::get_challenges_gadget(&mut transcript, U_i1.clone())?;
298 incircuit_c_W.enforce_equal(&cs_c_W)?;
299 incircuit_c_E.enforce_equal(&cs_c_E)?;
300
301 // 5.2. check eval_W==p_W(c_W) and eval_E==p_E(c_E)
302 let incircuit_eval_W = evaluate_gadget::<CF1<C1>>(W_i1.W, incircuit_c_W)?;
303 let incircuit_eval_E = evaluate_gadget::<CF1<C1>>(W_i1.E, incircuit_c_E)?;
304 incircuit_eval_W.enforce_equal(&eval_W)?;
305 incircuit_eval_E.enforce_equal(&eval_E)?;
306
307 // 1.1.b check that the NIFS.V challenge matches the one from the public input (so we avoid
308 // the verifier computing it)
309 let r_Fr = Boolean::le_bits_to_fp_var(&r_bits)?;
310 // check that the in-circuit computed r is equal to the inputted r
311 let r =
312 FpVar::<CF1<C1>>::new_input(cs.clone(), || Ok(self.r.unwrap_or_else(CF1::<C1>::zero)))?;
313 r_Fr.enforce_equal(&r)?;
314
315 Ok(())
316 }
317}
318
319/// Circuit that implements part of the in-circuit checks needed for the offchain verification over
320/// the Curve1's BaseField (=Curve2's ScalarField).
321#[derive(Clone, Debug)]
322pub struct DeciderCircuit2<C1, GC1, C2>
323where
324 C1: CurveGroup,
325 C2: CurveGroup,
326{
327 _c1: PhantomData<C1>,
328 _gc1: PhantomData<GC1>,
329 _c2: PhantomData<C2>,
330
331 /// E vector's length of the CycleFold instance witness
332 pub cf_E_len: usize,
333 /// R1CS of the CycleFold circuit
334 pub cf_r1cs: R1CS<C2::ScalarField>,
335 pub poseidon_config: PoseidonConfig<CF1<C2>>,
336 /// public params hash
337 pub pp_hash: Option<C2::ScalarField>,
338
339 /// CycleFold running instance. Notice that here we use Nova's CommittedInstance (instead of
340 /// CycleFoldCommittedInstance), since we are over C2::Fr, so that the CycleFold instances can
341 /// be computed natively
342 pub cf_U_i: Option<CommittedInstance<C2>>,
343 pub cf_W_i: Option<CycleFoldWitness<C2>>,
344 /// Commitment Scheme challenges
345 pub cs_c_W: Option<C2::ScalarField>,
346 pub cs_c_E: Option<C2::ScalarField>,
347 /// Evaluations of the committed polynomials at the challenge
348 pub eval_W: Option<C2::ScalarField>,
349 pub eval_E: Option<C2::ScalarField>,
350}
351impl<C1, GC1, C2> DeciderCircuit2<C1, GC1, C2>
352where
353 C1: CurveGroup,
354 C2: CurveGroup,
355 <C1 as CurveGroup>::BaseField: PrimeField,
356 <C1 as Group>::ScalarField: Absorb,
357 <C2 as CurveGroup>::BaseField: PrimeField,
358 <C2 as Group>::ScalarField: Absorb,
359 GC1: CurveVar<C1, CF2<C1>> + ToConstraintFieldGadget<CF2<C1>>,
360{
361 pub fn from_nova<GC2, CS1, CS2, const H: bool, FC: FCircuit<C1::ScalarField>>(
362 nova: Nova<C1, GC1, C2, GC2, FC, CS1, CS2, H>,
363 ) -> Result<Self, Error>
364 where
365 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
366 CS1: CommitmentScheme<C1, H>,
367 CS2: CommitmentScheme<C2, H>,
368 {
369 // compute the Commitment Scheme challenges of the CycleFold instance commitments, used as
370 // inputs in the circuit
371 let poseidon_config =
372 crate::transcript::poseidon::poseidon_canonical_config::<C2::ScalarField>();
373 let mut transcript = PoseidonSponge::<C2::ScalarField>::new(&poseidon_config);
374 let pp_hash_Fq =
375 C2::ScalarField::from_le_bytes_mod_order(&nova.pp_hash.into_bigint().to_bytes_le());
376 transcript.absorb(&pp_hash_Fq);
377
378 let (cs_challenge_W, cs_challenge_E) =
379 KZGChallengesGadget::<C2>::get_challenges_native(&mut transcript, nova.cf_U_i.clone());
380
381 // get evals of the committed polynomials at the challenge
382 let mut W = nova.cf_W_i.W.clone();
383 W.extend(
384 std::iter::repeat(C2::ScalarField::zero())
385 .take(nova.cf_W_i.W.len().next_power_of_two() - nova.cf_W_i.W.len()),
386 );
387 let mut E = nova.cf_W_i.E.clone();
388 E.extend(
389 std::iter::repeat(C2::ScalarField::zero())
390 .take(nova.cf_W_i.E.len().next_power_of_two() - nova.cf_W_i.E.len()),
391 );
392 let p_W = poly_from_vec(W.to_vec())?;
393 let eval_W = p_W.evaluate(&cs_challenge_W);
394 let p_E = poly_from_vec(E.to_vec())?;
395 let eval_E = p_E.evaluate(&cs_challenge_E);
396
397 Ok(Self {
398 _c1: PhantomData,
399 _gc1: PhantomData,
400 _c2: PhantomData,
401
402 cf_E_len: nova.cf_W_i.E.len(),
403 cf_r1cs: nova.cf_r1cs,
404 poseidon_config,
405 pp_hash: Some(pp_hash_Fq),
406
407 cf_U_i: Some(nova.cf_U_i),
408 cf_W_i: Some(nova.cf_W_i),
409
410 // CycleFold instance commitments challenges
411 cs_c_W: Some(cs_challenge_W),
412 cs_c_E: Some(cs_challenge_E),
413 eval_W: Some(eval_W),
414 eval_E: Some(eval_E),
415 })
416 }
417}
418
419impl<C1, GC1, C2> ConstraintSynthesizer<CF1<C2>> for DeciderCircuit2<C1, GC1, C2>
420where
421 C1: CurveGroup,
422 C2: CurveGroup,
423 <C1 as CurveGroup>::BaseField: PrimeField,
424 <C2 as CurveGroup>::BaseField: PrimeField,
425 <C1 as Group>::ScalarField: Absorb,
426 <C2 as Group>::ScalarField: Absorb,
427 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
428 GC1: CurveVar<C1, CF2<C1>> + ToConstraintFieldGadget<CF2<C1>>,
429 for<'a> &'a GC1: GroupOpsBounds<'a, C1, GC1>,
430{
431 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C2>>) -> Result<(), SynthesisError> {
432 let pp_hash = FpVar::<CF1<C2>>::new_input(cs.clone(), || {
433 Ok(self.pp_hash.unwrap_or_else(CF1::<C2>::zero))
434 })?;
435
436 let cf_u_dummy_native = CommittedInstance::<C2>::dummy(&self.cf_r1cs);
437 let w_dummy_native = Witness::<C2>::dummy(&self.cf_r1cs);
438 let cf_U_i = CommittedInstanceVar::<C2>::new_input(cs.clone(), || {
439 Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
440 })?;
441 let cf_W_i = WitnessVar::<C2>::new_witness(cs.clone(), || {
442 Ok(self.cf_W_i.unwrap_or(w_dummy_native.clone()))
443 })?;
444
445 let cf_r1cs =
446 R1CSVar::<C2::ScalarField, CF1<C2>, FpVar<CF1<C2>>>::new_witness(cs.clone(), || {
447 Ok(self.cf_r1cs.clone())
448 })?;
449
450 // 6. check RelaxedR1CS of cf_U_i
451 let cf_z_U = [vec![cf_U_i.u.clone()], cf_U_i.x.to_vec(), cf_W_i.W.to_vec()].concat();
452 RelaxedR1CSGadget::check_native(cf_r1cs, cf_W_i.E.clone(), cf_U_i.u.clone(), cf_z_U)?;
453
454 // `transcript` is for challenge generation.
455 let mut transcript =
456 PoseidonSpongeVar::<C2::ScalarField>::new(cs.clone(), &self.poseidon_config);
457 transcript.absorb(&pp_hash)?;
458
459 // allocate the inputs for the check 7.1
460 let cs_c_W = FpVar::<CF1<C2>>::new_input(cs.clone(), || {
461 Ok(self.cs_c_W.unwrap_or_else(CF1::<C2>::zero))
462 })?;
463 let cs_c_E = FpVar::<CF1<C2>>::new_input(cs.clone(), || {
464 Ok(self.cs_c_E.unwrap_or_else(CF1::<C2>::zero))
465 })?;
466 // allocate the inputs for the check 7.2
467 let eval_W = FpVar::<CF1<C2>>::new_input(cs.clone(), || {
468 Ok(self.eval_W.unwrap_or_else(CF1::<C2>::zero))
469 })?;
470 let eval_E = FpVar::<CF1<C2>>::new_input(cs.clone(), || {
471 Ok(self.eval_E.unwrap_or_else(CF1::<C2>::zero))
472 })?;
473
474 // 7.1. check the commitment scheme challenges correct computation
475 let (incircuit_c_W, incircuit_c_E) =
476 KZGChallengesGadget::<C2>::get_challenges_gadget(&mut transcript, cf_U_i.clone())?;
477 incircuit_c_W.enforce_equal(&cs_c_W)?;
478 incircuit_c_E.enforce_equal(&cs_c_E)?;
479
480 // 7.2. check eval_W==p_W(c_W) and eval_E==p_E(c_E)
481 let incircuit_eval_W = evaluate_gadget::<CF1<C2>>(cf_W_i.W, incircuit_c_W)?;
482 let incircuit_eval_E = evaluate_gadget::<CF1<C2>>(cf_W_i.E, incircuit_c_E)?;
483 incircuit_eval_W.enforce_equal(&eval_W)?;
484 incircuit_eval_E.enforce_equal(&eval_E)?;
485
486 Ok(())
487 }
488}
489
490#[cfg(test)]
491pub mod tests {
492 use ark_pallas::{constraints::GVar, Fq, Fr, Projective};
493 use ark_relations::r1cs::ConstraintSystem;
494 use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
495
496 use super::*;
497 use crate::commitment::pedersen::Pedersen;
498 use crate::folding::nova::PreprocessorParam;
499 use crate::frontend::utils::CubicFCircuit;
500 use crate::transcript::poseidon::poseidon_canonical_config;
501 use crate::FoldingScheme;
502
503 #[test]
504 fn test_decider_circuits() {
505 let mut rng = ark_std::test_rng();
506 let poseidon_config = poseidon_canonical_config::<Fr>();
507
508 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
509 let z_0 = vec![Fr::from(3_u32)];
510
511 type N = Nova<
512 Projective,
513 GVar,
514 Projective2,
515 GVar2,
516 CubicFCircuit<Fr>,
517 Pedersen<Projective>,
518 Pedersen<Projective2>,
519 false,
520 >;
521
522 let prep_param = PreprocessorParam::<
523 Projective,
524 Projective2,
525 CubicFCircuit<Fr>,
526 Pedersen<Projective>,
527 Pedersen<Projective2>,
528 false,
529 >::new(poseidon_config, F_circuit);
530 let nova_params = N::preprocess(&mut rng, &prep_param).unwrap();
531
532 // generate a Nova instance and do a step of it
533 let mut nova = N::init(&nova_params, F_circuit, z_0.clone()).unwrap();
534 nova.prove_step(&mut rng, vec![], None).unwrap();
535 // verify the IVC
536 let ivc_proof = nova.ivc_proof();
537 N::verify(nova_params.1, ivc_proof).unwrap();
538
539 // load the DeciderCircuit 1 & 2 from the Nova instance
540 let decider_circuit1 =
541 DeciderCircuit1::<Projective, Projective2, GVar2>::from_nova(nova.clone()).unwrap();
542 let decider_circuit2 =
543 DeciderCircuit2::<Projective, GVar, Projective2>::from_nova(nova).unwrap();
544
545 // generate the constraints of both circuits and check that are satisfied by the inputs
546 let cs1 = ConstraintSystem::<Fr>::new_ref();
547 decider_circuit1.generate_constraints(cs1.clone()).unwrap();
548 assert!(cs1.is_satisfied().unwrap());
549 let cs2 = ConstraintSystem::<Fq>::new_ref();
550 decider_circuit2.generate_constraints(cs2.clone()).unwrap();
551 assert!(cs2.is_satisfied().unwrap());
552 }
553}