sonobe/folding-schemes/src/folding/nova/circuits.rs
folding-schemes/src/folding/nova/circuits.rsRaw
1/// contains [Nova](https://eprint.iacr.org/2021/370.pdf) related circuits
2use ark_crypto_primitives::crh::{
3 poseidon::constraints::{CRHGadget, CRHParametersVar},
4 CRHSchemeGadget,
5};
6use ark_crypto_primitives::sponge::{
7 constraints::CryptographicSpongeVar,
8 poseidon::{constraints::PoseidonSpongeVar, PoseidonConfig, PoseidonSponge},
9 Absorb, CryptographicSponge,
10};
11use ark_ec::{AffineRepr, CurveGroup, Group};
12use ark_ff::{Field, PrimeField};
13use ark_r1cs_std::{
14 alloc::{AllocVar, AllocationMode},
15 boolean::Boolean,
16 eq::EqGadget,
17 fields::{fp::FpVar, nonnative::NonNativeFieldVar, FieldVar},
18 groups::GroupOpsBounds,
19 prelude::CurveVar,
20 R1CSVar, ToConstraintFieldGadget,
21};
22use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
23use ark_std::{fmt::Debug, Zero};
24use core::{borrow::Borrow, marker::PhantomData};
25
26use super::{
27 cyclefold::{
28 CycleFoldChallengeGadget, CycleFoldCommittedInstanceVar, NIFSFullGadget, CF_IO_LEN,
29 },
30 CommittedInstance,
31};
32use crate::folding::circuits::nonnative::{nonnative_affine_to_field_elements, NonNativeAffineVar};
33use crate::frontend::FCircuit;
34use crate::{constants::N_BITS_RO, folding::circuits::nonnative::nonnative_field_var_from_le_bits};
35
36/// CF1 represents the ConstraintField used for the main Nova circuit which is over E1::Fr, where
37/// E1 is the main curve where we do the folding.
38pub type CF1<C> = <<C as CurveGroup>::Affine as AffineRepr>::ScalarField;
39/// CF2 represents the ConstraintField used for the CycleFold circuit which is over E2::Fr=E1::Fq,
40/// where E2 is the auxiliary curve (from [CycleFold](https://eprint.iacr.org/2023/1192.pdf)
41/// approach) where we check the folding of the commitments (elliptic curve points).
42pub type CF2<C> = <<C as CurveGroup>::BaseField as Field>::BasePrimeField;
43
44/// CommittedInstanceVar contains the u, x, cmE and cmW values which are folded on the main Nova
45/// constraints field (E1::Fr, where E1 is the main curve). The peculiarity is that cmE and cmW are
46/// represented non-natively over the constraint field.
47#[derive(Debug, Clone)]
48pub struct CommittedInstanceVar<C: CurveGroup>
49where
50 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
51{
52 pub u: FpVar<C::ScalarField>,
53 pub x: Vec<FpVar<C::ScalarField>>,
54 pub cmE: NonNativeAffineVar<C>,
55 pub cmW: NonNativeAffineVar<C>,
56}
57
58impl<C> AllocVar<CommittedInstance<C>, CF1<C>> for CommittedInstanceVar<C>
59where
60 C: CurveGroup,
61 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
62{
63 fn new_variable<T: Borrow<CommittedInstance<C>>>(
64 cs: impl Into<Namespace<CF1<C>>>,
65 f: impl FnOnce() -> Result<T, SynthesisError>,
66 mode: AllocationMode,
67 ) -> Result<Self, SynthesisError> {
68 f().and_then(|val| {
69 let cs = cs.into();
70
71 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
72 let x: Vec<FpVar<C::ScalarField>> =
73 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
74
75 let cmE =
76 NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().cmE), mode)?;
77 let cmW =
78 NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().cmW), mode)?;
79
80 Ok(Self { u, x, cmE, cmW })
81 })
82 }
83}
84
85impl<C> CommittedInstanceVar<C>
86where
87 C: CurveGroup,
88 <C as Group>::ScalarField: Absorb,
89 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
90{
91 /// hash implements the committed instance hash compatible with the native implementation from
92 /// CommittedInstance.hash.
93 /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the
94 /// `CommittedInstance`.
95 /// Additionally it returns the vector of the field elements from the self parameters, so they
96 /// can be reused in other gadgets avoiding recalculating (reconstraining) them.
97 #[allow(clippy::type_complexity)]
98 pub fn hash(
99 self,
100 crh_params: &CRHParametersVar<CF1<C>>,
101 i: FpVar<CF1<C>>,
102 z_0: Vec<FpVar<CF1<C>>>,
103 z_i: Vec<FpVar<CF1<C>>>,
104 ) -> Result<(FpVar<CF1<C>>, Vec<FpVar<CF1<C>>>), SynthesisError> {
105 let U_vec = [
106 vec![self.u],
107 self.x,
108 self.cmE.to_constraint_field()?,
109 self.cmW.to_constraint_field()?,
110 ]
111 .concat();
112 let input = [vec![i], z_0, z_i, U_vec.clone()].concat();
113 Ok((
114 CRHGadget::<C::ScalarField>::evaluate(crh_params, &input)?,
115 U_vec,
116 ))
117 }
118}
119
120/// Implements the circuit that does the checks of the Non-Interactive Folding Scheme Verifier
121/// described in section 4 of [Nova](https://eprint.iacr.org/2021/370.pdf), where the cmE & cmW checks are
122/// delegated to the NIFSCycleFoldGadget.
123pub struct NIFSGadget<C: CurveGroup> {
124 _c: PhantomData<C>,
125}
126
127impl<C: CurveGroup> NIFSGadget<C>
128where
129 C: CurveGroup,
130 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
131{
132 pub fn fold_committed_instance(
133 r: FpVar<CF1<C>>,
134 ci1: CommittedInstanceVar<C>, // U_i
135 ci2: CommittedInstanceVar<C>, // u_i
136 ) -> Result<CommittedInstanceVar<C>, SynthesisError> {
137 Ok(CommittedInstanceVar {
138 cmE: NonNativeAffineVar::new_constant(ConstraintSystemRef::None, C::zero())?,
139 cmW: NonNativeAffineVar::new_constant(ConstraintSystemRef::None, C::zero())?,
140 // ci3.u = ci1.u + r * ci2.u
141 u: ci1.u + &r * ci2.u,
142 // ci3.x = ci1.x + r * ci2.x
143 x: ci1
144 .x
145 .iter()
146 .zip(ci2.x)
147 .map(|(a, b)| a + &r * &b)
148 .collect::<Vec<FpVar<CF1<C>>>>(),
149 })
150 }
151
152 /// Implements the constraints for NIFS.V for u and x, since cm(E) and cm(W) are delegated to
153 /// the CycleFold circuit.
154 pub fn verify(
155 r: FpVar<CF1<C>>,
156 ci1: CommittedInstanceVar<C>, // U_i
157 ci2: CommittedInstanceVar<C>, // u_i
158 ci3: CommittedInstanceVar<C>, // U_{i+1}
159 ) -> Result<(), SynthesisError> {
160 let ci = Self::fold_committed_instance(r, ci1, ci2)?;
161
162 ci.u.enforce_equal(&ci3.u)?;
163 ci.x.enforce_equal(&ci3.x)?;
164
165 Ok(())
166 }
167}
168
169/// ChallengeGadget computes the RO challenge used for the Nova instances NIFS, it contains a
170/// rust-native and a in-circuit compatible versions.
171pub struct ChallengeGadget<C: CurveGroup> {
172 _c: PhantomData<C>,
173}
174impl<C: CurveGroup> ChallengeGadget<C>
175where
176 C: CurveGroup,
177 <C as CurveGroup>::BaseField: PrimeField,
178 <C as Group>::ScalarField: Absorb,
179{
180 pub fn get_challenge_native(
181 poseidon_config: &PoseidonConfig<C::ScalarField>,
182 U_i: CommittedInstance<C>,
183 u_i: CommittedInstance<C>,
184 cmT: C,
185 ) -> Result<Vec<bool>, SynthesisError> {
186 let (U_cmE_x, U_cmE_y) = nonnative_affine_to_field_elements::<C>(U_i.cmE)?;
187 let (U_cmW_x, U_cmW_y) = nonnative_affine_to_field_elements::<C>(U_i.cmW)?;
188 let (u_cmE_x, u_cmE_y) = nonnative_affine_to_field_elements::<C>(u_i.cmE)?;
189 let (u_cmW_x, u_cmW_y) = nonnative_affine_to_field_elements::<C>(u_i.cmW)?;
190 let (cmT_x, cmT_y) = nonnative_affine_to_field_elements::<C>(cmT)?;
191
192 let mut sponge = PoseidonSponge::<C::ScalarField>::new(poseidon_config);
193 let input = vec![
194 vec![U_i.u],
195 U_i.x.clone(),
196 U_cmE_x,
197 U_cmE_y,
198 U_cmW_x,
199 U_cmW_y,
200 vec![u_i.u],
201 u_i.x.clone(),
202 u_cmE_x,
203 u_cmE_y,
204 u_cmW_x,
205 u_cmW_y,
206 cmT_x,
207 cmT_y,
208 ]
209 .concat();
210 sponge.absorb(&input);
211 let bits = sponge.squeeze_bits(N_BITS_RO);
212 Ok(bits)
213 }
214
215 // compatible with the native get_challenge_native
216 pub fn get_challenge_gadget(
217 cs: ConstraintSystemRef<C::ScalarField>,
218 poseidon_config: &PoseidonConfig<C::ScalarField>,
219 U_i_vec: Vec<FpVar<CF1<C>>>, // apready processed input, so we don't have to recompute these values
220 u_i: CommittedInstanceVar<C>,
221 cmT: NonNativeAffineVar<C>,
222 ) -> Result<Vec<Boolean<C::ScalarField>>, SynthesisError> {
223 let mut sponge = PoseidonSpongeVar::<C::ScalarField>::new(cs, poseidon_config);
224
225 let input: Vec<FpVar<C::ScalarField>> = [
226 U_i_vec,
227 vec![u_i.u.clone()],
228 u_i.x.clone(),
229 u_i.cmE.to_constraint_field()?,
230 u_i.cmW.to_constraint_field()?,
231 cmT.to_constraint_field()?,
232 ]
233 .concat();
234 sponge.absorb(&input)?;
235 let bits = sponge.squeeze_bits(N_BITS_RO)?;
236 Ok(bits)
237 }
238}
239
240/// AugmentedFCircuit implements the F' circuit (augmented F) defined in
241/// [Nova](https://eprint.iacr.org/2021/370.pdf) together with the extra constraints defined in
242/// [CycleFold](https://eprint.iacr.org/2023/1192.pdf).
243#[derive(Debug, Clone)]
244pub struct AugmentedFCircuit<
245 C1: CurveGroup,
246 C2: CurveGroup,
247 GC2: CurveVar<C2, CF2<C2>>,
248 FC: FCircuit<CF1<C1>>,
249> where
250 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
251{
252 pub _gc2: PhantomData<GC2>,
253 pub poseidon_config: PoseidonConfig<CF1<C1>>,
254 pub i: Option<CF1<C1>>,
255 pub i_usize: Option<usize>,
256 pub z_0: Option<Vec<C1::ScalarField>>,
257 pub z_i: Option<Vec<C1::ScalarField>>,
258 pub u_i_cmW: Option<C1>,
259 pub U_i: Option<CommittedInstance<C1>>,
260 pub U_i1_cmE: Option<C1>,
261 pub U_i1_cmW: Option<C1>,
262 pub cmT: Option<C1>,
263 pub F: FC, // F circuit
264 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
265
266 // cyclefold verifier on C1
267 // Here 'cf1, cf2' are for each of the CycleFold circuits, corresponding to the fold of cmW and
268 // cmE respectively
269 pub cf1_u_i_cmW: Option<C2>, // input
270 pub cf2_u_i_cmW: Option<C2>, // input
271 pub cf_U_i: Option<CommittedInstance<C2>>, // input
272 pub cf1_cmT: Option<C2>,
273 pub cf2_cmT: Option<C2>,
274 pub cf_x: Option<CF1<C1>>, // public input (u_{i+1}.x[1])
275}
276
277impl<C1: CurveGroup, C2: CurveGroup, GC2: CurveVar<C2, CF2<C2>>, FC: FCircuit<CF1<C1>>>
278 AugmentedFCircuit<C1, C2, GC2, FC>
279where
280 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
281{
282 pub fn empty(poseidon_config: &PoseidonConfig<CF1<C1>>, F_circuit: FC) -> Self {
283 Self {
284 _gc2: PhantomData,
285 poseidon_config: poseidon_config.clone(),
286 i: None,
287 i_usize: None,
288 z_0: None,
289 z_i: None,
290 u_i_cmW: None,
291 U_i: None,
292 U_i1_cmE: None,
293 U_i1_cmW: None,
294 cmT: None,
295 F: F_circuit,
296 x: None,
297 // cyclefold values
298 cf1_u_i_cmW: None,
299 cf2_u_i_cmW: None,
300 cf_U_i: None,
301 cf1_cmT: None,
302 cf2_cmT: None,
303 cf_x: None,
304 }
305 }
306}
307
308impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
309where
310 C1: CurveGroup,
311 C2: CurveGroup,
312 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
313 FC: FCircuit<CF1<C1>>,
314 <C1 as CurveGroup>::BaseField: PrimeField,
315 <C2 as CurveGroup>::BaseField: PrimeField,
316 <C1 as Group>::ScalarField: Absorb,
317 <C2 as Group>::ScalarField: Absorb,
318 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
319 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
320{
321 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
322 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
323 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
324 })?;
325 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
326 Ok(self
327 .z_0
328 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
329 })?;
330 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
331 Ok(self
332 .z_i
333 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
334 })?;
335
336 let u_dummy = CommittedInstance::dummy(2);
337 let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
338 Ok(self.U_i.unwrap_or(u_dummy.clone()))
339 })?;
340 let U_i1_cmE = NonNativeAffineVar::new_witness(cs.clone(), || {
341 Ok(self.U_i1_cmE.unwrap_or_else(C1::zero))
342 })?;
343 let U_i1_cmW = NonNativeAffineVar::new_witness(cs.clone(), || {
344 Ok(self.U_i1_cmW.unwrap_or_else(C1::zero))
345 })?;
346
347 let cmT =
348 NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C1::zero)))?;
349
350 let cf_u_dummy = CommittedInstance::dummy(CF_IO_LEN);
351 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
352 Ok(self.cf_U_i.unwrap_or(cf_u_dummy.clone()))
353 })?;
354 let cf1_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf1_cmT.unwrap_or_else(C2::zero)))?;
355 let cf2_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf2_cmT.unwrap_or_else(C2::zero)))?;
356
357 let crh_params = CRHParametersVar::<C1::ScalarField>::new_constant(
358 cs.clone(),
359 self.poseidon_config.clone(),
360 )?;
361
362 // get z_{i+1} from the F circuit
363 let i_usize = self.i_usize.unwrap_or(0);
364 let z_i1 = self
365 .F
366 .generate_step_constraints(cs.clone(), i_usize, z_i.clone())?;
367
368 let is_basecase = i.is_zero()?;
369
370 // Primary Part
371 // P.1. Compute u_i.x
372 // u_i.x[0] = H(i, z_0, z_i, U_i)
373 let (u_i_x, U_i_vec) =
374 U_i.clone()
375 .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
376 // u_i.x[1] = H(cf_U_i)
377 let (cf_u_i_x, cf_U_i_vec) = cf_U_i.clone().hash(&crh_params)?;
378
379 // P.2. Construct u_i
380 let u_i = CommittedInstanceVar {
381 // u_i.cmE = cm(0)
382 cmE: NonNativeAffineVar::new_constant(cs.clone(), C1::zero())?,
383 // u_i.u = 1
384 u: FpVar::one(),
385 // u_i.cmW is provided by the prover as witness
386 cmW: NonNativeAffineVar::new_witness(cs.clone(), || {
387 Ok(self.u_i_cmW.unwrap_or(C1::zero()))
388 })?,
389 // u_i.x is computed in step 1
390 x: vec![u_i_x, cf_u_i_x],
391 };
392
393 // P.3. nifs.verify, obtains U_{i+1} by folding u_i & U_i .
394
395 // compute r = H(u_i, U_i, cmT)
396 let r_bits = ChallengeGadget::<C1>::get_challenge_gadget(
397 cs.clone(),
398 &self.poseidon_config,
399 U_i_vec,
400 u_i.clone(),
401 cmT.clone(),
402 )?;
403 let r = Boolean::le_bits_to_fp_var(&r_bits)?;
404 // Also convert r_bits to a `NonNativeFieldVar`
405 let r_nonnat = nonnative_field_var_from_le_bits(cs.clone(), &r_bits)?;
406
407 // Notice that NIFSGadget::fold_committed_instance does not fold cmE & cmW.
408 // We set `U_i1.cmE` and `U_i1.cmW` to unconstrained witnesses `U_i1_cmE` and `U_i1_cmW`
409 // respectively.
410 // The correctness of them will be checked on the other curve.
411 let mut U_i1 = NIFSGadget::<C1>::fold_committed_instance(r, U_i.clone(), u_i.clone())?;
412 U_i1.cmE = U_i1_cmE;
413 U_i1.cmW = U_i1_cmW;
414
415 // P.4.a compute and check the first output of F'
416 // Base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{\bot})
417 // Non-base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{i+1})
418 let (u_i1_x, _) = U_i1.clone().hash(
419 &crh_params,
420 i + FpVar::<CF1<C1>>::one(),
421 z_0.clone(),
422 z_i1.clone(),
423 )?;
424 let (u_i1_x_base, _) = CommittedInstanceVar::new_constant(cs.clone(), u_dummy)?.hash(
425 &crh_params,
426 FpVar::<CF1<C1>>::one(),
427 z_0.clone(),
428 z_i1.clone(),
429 )?;
430 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
431 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
432
433 // CycleFold part
434 // C.1. Compute cf1_u_i.x and cf2_u_i.x
435 let cfW_x = vec![
436 r_nonnat.clone(),
437 U_i.cmW.x,
438 U_i.cmW.y,
439 u_i.cmW.x,
440 u_i.cmW.y,
441 U_i1.cmW.x,
442 U_i1.cmW.y,
443 ];
444 let cfE_x = vec![
445 r_nonnat, U_i.cmE.x, U_i.cmE.y, cmT.x, cmT.y, U_i1.cmE.x, U_i1.cmE.y,
446 ];
447
448 // ensure that cf1_u & cf2_u have as public inputs the cmW & cmE from main instances U_i,
449 // u_i, U_i+1 coordinates of the commitments
450 // C.2. Construct `cf1_u_i` and `cf2_u_i`
451 let cf1_u_i = CycleFoldCommittedInstanceVar {
452 // cf1_u_i.cmE = 0
453 cmE: GC2::zero(),
454 // cf1_u_i.u = 1
455 u: NonNativeFieldVar::one(),
456 // cf1_u_i.cmW is provided by the prover as witness
457 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf1_u_i_cmW.unwrap_or(C2::zero())))?,
458 // cf1_u_i.x is computed in step 1
459 x: cfW_x,
460 };
461 let cf2_u_i = CycleFoldCommittedInstanceVar {
462 // cf2_u_i.cmE = 0
463 cmE: GC2::zero(),
464 // cf2_u_i.u = 1
465 u: NonNativeFieldVar::one(),
466 // cf2_u_i.cmW is provided by the prover as witness
467 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf2_u_i_cmW.unwrap_or(C2::zero())))?,
468 // cf2_u_i.x is computed in step 1
469 x: cfE_x,
470 };
471
472 // C.3. nifs.verify, obtains cf1_U_{i+1} by folding cf1_u_i & cf_U_i, and then cf_U_{i+1}
473 // by folding cf2_u_i & cf1_U_{i+1}.
474
475 // compute cf1_r = H(cf1_u_i, cf_U_i, cf1_cmT)
476 // cf_r_bits is denoted by rho* in the paper.
477 let cf1_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
478 cs.clone(),
479 &self.poseidon_config,
480 cf_U_i_vec,
481 cf1_u_i.clone(),
482 cf1_cmT.clone(),
483 )?;
484 // Convert cf1_r_bits to a `NonNativeFieldVar`
485 let cf1_r_nonnat = nonnative_field_var_from_le_bits(cs.clone(), &cf1_r_bits)?;
486 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
487 let cf1_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
488 cf1_r_bits,
489 cf1_r_nonnat,
490 cf1_cmT,
491 cf_U_i,
492 cf1_u_i,
493 )?;
494
495 // same for cf2_r:
496 let cf2_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
497 cs.clone(),
498 &self.poseidon_config,
499 cf1_U_i1.to_constraint_field()?,
500 cf2_u_i.clone(),
501 cf2_cmT.clone(),
502 )?;
503 let cf2_r_nonnat = nonnative_field_var_from_le_bits(cs.clone(), &cf2_r_bits)?;
504 let cf_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
505 cf2_r_bits,
506 cf2_r_nonnat,
507 cf2_cmT,
508 cf1_U_i1, // the output from NIFS.V(cf1_r, cf_U, cfE_u)
509 cf2_u_i,
510 )?;
511
512 // Back to Primary Part
513 // P.4.b compute and check the second output of F'
514 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
515 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
516 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&crh_params)?;
517 let (cf_u_i1_x_base, _) =
518 CycleFoldCommittedInstanceVar::new_constant(cs.clone(), cf_u_dummy)?
519 .hash(&crh_params)?;
520 let cf_x = FpVar::new_input(cs.clone(), || {
521 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
522 })?;
523 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
524
525 Ok(())
526 }
527}
528
529#[cfg(test)]
530pub mod tests {
531 use super::*;
532 use ark_bn254::{Fr, G1Projective as Projective};
533 use ark_ff::BigInteger;
534 use ark_relations::r1cs::ConstraintSystem;
535 use ark_std::UniformRand;
536
537 use crate::commitment::pedersen::Pedersen;
538 use crate::folding::nova::nifs::tests::prepare_simple_fold_inputs;
539 use crate::folding::nova::nifs::NIFS;
540 use crate::transcript::poseidon::poseidon_test_config;
541
542 #[test]
543 fn test_committed_instance_var() {
544 let mut rng = ark_std::test_rng();
545
546 let ci = CommittedInstance::<Projective> {
547 cmE: Projective::rand(&mut rng),
548 u: Fr::rand(&mut rng),
549 cmW: Projective::rand(&mut rng),
550 x: vec![Fr::rand(&mut rng); 1],
551 };
552
553 let cs = ConstraintSystem::<Fr>::new_ref();
554 let ciVar =
555 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
556 assert_eq!(ciVar.u.value().unwrap(), ci.u);
557 assert_eq!(ciVar.x.value().unwrap(), ci.x);
558 // the values cmE and cmW are checked in the CycleFold's circuit
559 // CommittedInstanceInCycleFoldVar in
560 // nova::cyclefold::tests::test_committed_instance_cyclefold_var
561 }
562
563 #[test]
564 fn test_nifs_gadget() {
565 let (_, _, _, _, ci1, _, ci2, _, ci3, _, cmT, _, r_Fr) = prepare_simple_fold_inputs();
566
567 let ci3_verifier = NIFS::<Projective, Pedersen<Projective>>::verify(r_Fr, &ci1, &ci2, &cmT);
568 assert_eq!(ci3_verifier, ci3);
569
570 let cs = ConstraintSystem::<Fr>::new_ref();
571
572 let rVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(r_Fr)).unwrap();
573 let ci1Var =
574 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci1.clone()))
575 .unwrap();
576 let ci2Var =
577 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci2.clone()))
578 .unwrap();
579 let ci3Var =
580 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci3.clone()))
581 .unwrap();
582
583 NIFSGadget::<Projective>::verify(
584 rVar.clone(),
585 ci1Var.clone(),
586 ci2Var.clone(),
587 ci3Var.clone(),
588 )
589 .unwrap();
590 assert!(cs.is_satisfied().unwrap());
591 }
592
593 #[test]
594 fn test_committed_instance_hash() {
595 let mut rng = ark_std::test_rng();
596 let poseidon_config = poseidon_test_config::<Fr>();
597
598 let i = Fr::from(3_u32);
599 let z_0 = vec![Fr::from(3_u32)];
600 let z_i = vec![Fr::from(3_u32)];
601 let ci = CommittedInstance::<Projective> {
602 cmE: Projective::rand(&mut rng),
603 u: Fr::rand(&mut rng),
604 cmW: Projective::rand(&mut rng),
605 x: vec![Fr::rand(&mut rng); 1],
606 };
607
608 // compute the CommittedInstance hash natively
609 let h = ci
610 .hash(&poseidon_config, i, z_0.clone(), z_i.clone())
611 .unwrap();
612
613 let cs = ConstraintSystem::<Fr>::new_ref();
614
615 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
616 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
617 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
618 let ciVar =
619 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
620
621 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
622
623 // compute the CommittedInstance hash in-circuit
624 let (hVar, _) = ciVar.hash(&crh_params, iVar, z_0Var, z_iVar).unwrap();
625 assert!(cs.is_satisfied().unwrap());
626
627 // check that the natively computed and in-circuit computed hashes match
628 assert_eq!(hVar.value().unwrap(), h);
629 }
630
631 // checks that the gadget and native implementations of the challenge computation match
632 #[test]
633 fn test_challenge_gadget() {
634 let mut rng = ark_std::test_rng();
635 let poseidon_config = poseidon_test_config::<Fr>();
636
637 let u_i = CommittedInstance::<Projective> {
638 cmE: Projective::rand(&mut rng),
639 u: Fr::rand(&mut rng),
640 cmW: Projective::rand(&mut rng),
641 x: vec![Fr::rand(&mut rng); 1],
642 };
643 let U_i = CommittedInstance::<Projective> {
644 cmE: Projective::rand(&mut rng),
645 u: Fr::rand(&mut rng),
646 cmW: Projective::rand(&mut rng),
647 x: vec![Fr::rand(&mut rng); 1],
648 };
649 let cmT = Projective::rand(&mut rng);
650
651 // compute the challenge natively
652 let r_bits = ChallengeGadget::<Projective>::get_challenge_native(
653 &poseidon_config,
654 U_i.clone(),
655 u_i.clone(),
656 cmT,
657 )
658 .unwrap();
659 let r = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
660
661 let cs = ConstraintSystem::<Fr>::new_ref();
662 let u_iVar =
663 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(u_i.clone()))
664 .unwrap();
665 let U_iVar =
666 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(U_i.clone()))
667 .unwrap();
668 let cmTVar = NonNativeAffineVar::<Projective>::new_witness(cs.clone(), || Ok(cmT)).unwrap();
669
670 // compute the challenge in-circuit
671 let U_iVar_vec = [
672 vec![U_iVar.u.clone()],
673 U_iVar.x.clone(),
674 U_iVar.cmE.to_constraint_field().unwrap(),
675 U_iVar.cmW.to_constraint_field().unwrap(),
676 ]
677 .concat();
678 let r_bitsVar = ChallengeGadget::<Projective>::get_challenge_gadget(
679 cs.clone(),
680 &poseidon_config,
681 U_iVar_vec,
682 u_iVar,
683 cmTVar,
684 )
685 .unwrap();
686 assert!(cs.is_satisfied().unwrap());
687
688 // check that the natively computed and in-circuit computed hashes match
689 let rVar = Boolean::le_bits_to_fp_var(&r_bitsVar).unwrap();
690 assert_eq!(rVar.value().unwrap(), r);
691 assert_eq!(r_bitsVar.value().unwrap(), r_bits);
692 }
693}