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