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