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 external_inputs: Option<Vec<C1::ScalarField>>,
262 pub u_i_cmW: Option<C1>,
263 pub U_i: Option<CommittedInstance<C1>>,
264 pub U_i1_cmE: Option<C1>,
265 pub U_i1_cmW: Option<C1>,
266 pub cmT: Option<C1>,
267 pub F: FC, // F circuit
268 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
269
270 // cyclefold verifier on C1
271 // Here 'cf1, cf2' are for each of the CycleFold circuits, corresponding to the fold of cmW and
272 // cmE respectively
273 pub cf1_u_i_cmW: Option<C2>, // input
274 pub cf2_u_i_cmW: Option<C2>, // input
275 pub cf_U_i: Option<CommittedInstance<C2>>, // input
276 pub cf1_cmT: Option<C2>,
277 pub cf2_cmT: Option<C2>,
278 pub cf_x: Option<CF1<C1>>, // public input (u_{i+1}.x[1])
279}
280
281impl<C1: CurveGroup, C2: CurveGroup, GC2: CurveVar<C2, CF2<C2>>, FC: FCircuit<CF1<C1>>>
282 AugmentedFCircuit<C1, C2, GC2, FC>
283where
284 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
285{
286 pub fn empty(poseidon_config: &PoseidonConfig<CF1<C1>>, F_circuit: FC) -> Self {
287 Self {
288 _gc2: PhantomData,
289 poseidon_config: poseidon_config.clone(),
290 i: None,
291 i_usize: None,
292 z_0: None,
293 z_i: None,
294 external_inputs: None,
295 u_i_cmW: None,
296 U_i: None,
297 U_i1_cmE: None,
298 U_i1_cmW: None,
299 cmT: None,
300 F: F_circuit,
301 x: None,
302 // cyclefold values
303 cf1_u_i_cmW: None,
304 cf2_u_i_cmW: None,
305 cf_U_i: None,
306 cf1_cmT: None,
307 cf2_cmT: None,
308 cf_x: None,
309 }
310 }
311}
312
313impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
314where
315 C1: CurveGroup,
316 C2: CurveGroup,
317 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
318 FC: FCircuit<CF1<C1>>,
319 <C1 as CurveGroup>::BaseField: PrimeField,
320 <C2 as CurveGroup>::BaseField: PrimeField,
321 <C1 as Group>::ScalarField: Absorb,
322 <C2 as Group>::ScalarField: Absorb,
323 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
324 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
325{
326 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
327 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
328 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
329 })?;
330 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
331 Ok(self
332 .z_0
333 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
334 })?;
335 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
336 Ok(self
337 .z_i
338 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
339 })?;
340 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
341 Ok(self
342 .external_inputs
343 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
344 })?;
345
346 let u_dummy = CommittedInstance::dummy(2);
347 let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
348 Ok(self.U_i.unwrap_or(u_dummy.clone()))
349 })?;
350 let U_i1_cmE = NonNativeAffineVar::new_witness(cs.clone(), || {
351 Ok(self.U_i1_cmE.unwrap_or_else(C1::zero))
352 })?;
353 let U_i1_cmW = NonNativeAffineVar::new_witness(cs.clone(), || {
354 Ok(self.U_i1_cmW.unwrap_or_else(C1::zero))
355 })?;
356
357 let cmT =
358 NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C1::zero)))?;
359
360 let cf_u_dummy = CommittedInstance::dummy(CF_IO_LEN);
361 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
362 Ok(self.cf_U_i.unwrap_or(cf_u_dummy.clone()))
363 })?;
364 let cf1_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf1_cmT.unwrap_or_else(C2::zero)))?;
365 let cf2_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf2_cmT.unwrap_or_else(C2::zero)))?;
366
367 let crh_params = CRHParametersVar::<C1::ScalarField>::new_constant(
368 cs.clone(),
369 self.poseidon_config.clone(),
370 )?;
371
372 // get z_{i+1} from the F circuit
373 let i_usize = self.i_usize.unwrap_or(0);
374 let z_i1 =
375 self.F
376 .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?;
377
378 let is_basecase = i.is_zero()?;
379
380 // Primary Part
381 // P.1. Compute u_i.x
382 // u_i.x[0] = H(i, z_0, z_i, U_i)
383 let (u_i_x, U_i_vec) =
384 U_i.clone()
385 .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
386 // u_i.x[1] = H(cf_U_i)
387 let (cf_u_i_x, cf_U_i_vec) = cf_U_i.clone().hash(&crh_params)?;
388
389 // P.2. Construct u_i
390 let u_i = CommittedInstanceVar {
391 // u_i.cmE = cm(0)
392 cmE: NonNativeAffineVar::new_constant(cs.clone(), C1::zero())?,
393 // u_i.u = 1
394 u: FpVar::one(),
395 // u_i.cmW is provided by the prover as witness
396 cmW: NonNativeAffineVar::new_witness(cs.clone(), || {
397 Ok(self.u_i_cmW.unwrap_or(C1::zero()))
398 })?,
399 // u_i.x is computed in step 1
400 x: vec![u_i_x, cf_u_i_x],
401 };
402
403 // P.3. nifs.verify, obtains U_{i+1} by folding u_i & U_i .
404
405 // compute r = H(u_i, U_i, cmT)
406 let r_bits = ChallengeGadget::<C1>::get_challenge_gadget(
407 cs.clone(),
408 &self.poseidon_config,
409 U_i_vec,
410 u_i.clone(),
411 cmT.clone(),
412 )?;
413 let r = Boolean::le_bits_to_fp_var(&r_bits)?;
414 // Also convert r_bits to a `NonNativeFieldVar`
415 let r_nonnat = {
416 let mut bits = r_bits;
417 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
418 NonNativeUintVar::from(&bits)
419 };
420
421 // Notice that NIFSGadget::fold_committed_instance does not fold cmE & cmW.
422 // We set `U_i1.cmE` and `U_i1.cmW` to unconstrained witnesses `U_i1_cmE` and `U_i1_cmW`
423 // respectively.
424 // The correctness of them will be checked on the other curve.
425 let mut U_i1 = NIFSGadget::<C1>::fold_committed_instance(r, U_i.clone(), u_i.clone())?;
426 U_i1.cmE = U_i1_cmE;
427 U_i1.cmW = U_i1_cmW;
428
429 // P.4.a compute and check the first output of F'
430 // Base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{\bot})
431 // Non-base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{i+1})
432 let (u_i1_x, _) = U_i1.clone().hash(
433 &crh_params,
434 i + FpVar::<CF1<C1>>::one(),
435 z_0.clone(),
436 z_i1.clone(),
437 )?;
438 let (u_i1_x_base, _) = CommittedInstanceVar::new_constant(cs.clone(), u_dummy)?.hash(
439 &crh_params,
440 FpVar::<CF1<C1>>::one(),
441 z_0.clone(),
442 z_i1.clone(),
443 )?;
444 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
445 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
446
447 // CycleFold part
448 // C.1. Compute cf1_u_i.x and cf2_u_i.x
449 let cfW_x = vec![
450 r_nonnat.clone(),
451 U_i.cmW.x,
452 U_i.cmW.y,
453 u_i.cmW.x,
454 u_i.cmW.y,
455 U_i1.cmW.x,
456 U_i1.cmW.y,
457 ];
458 let cfE_x = vec![
459 r_nonnat, U_i.cmE.x, U_i.cmE.y, cmT.x, cmT.y, U_i1.cmE.x, U_i1.cmE.y,
460 ];
461
462 // ensure that cf1_u & cf2_u have as public inputs the cmW & cmE from main instances U_i,
463 // u_i, U_i+1 coordinates of the commitments
464 // C.2. Construct `cf1_u_i` and `cf2_u_i`
465 let cf1_u_i = CycleFoldCommittedInstanceVar {
466 // cf1_u_i.cmE = 0
467 cmE: GC2::zero(),
468 // cf1_u_i.u = 1
469 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
470 // cf1_u_i.cmW is provided by the prover as witness
471 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf1_u_i_cmW.unwrap_or(C2::zero())))?,
472 // cf1_u_i.x is computed in step 1
473 x: cfW_x,
474 };
475 let cf2_u_i = CycleFoldCommittedInstanceVar {
476 // cf2_u_i.cmE = 0
477 cmE: GC2::zero(),
478 // cf2_u_i.u = 1
479 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
480 // cf2_u_i.cmW is provided by the prover as witness
481 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf2_u_i_cmW.unwrap_or(C2::zero())))?,
482 // cf2_u_i.x is computed in step 1
483 x: cfE_x,
484 };
485
486 // C.3. nifs.verify, obtains cf1_U_{i+1} by folding cf1_u_i & cf_U_i, and then cf_U_{i+1}
487 // by folding cf2_u_i & cf1_U_{i+1}.
488
489 // compute cf1_r = H(cf1_u_i, cf_U_i, cf1_cmT)
490 // cf_r_bits is denoted by rho* in the paper.
491 let cf1_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
492 cs.clone(),
493 &self.poseidon_config,
494 cf_U_i_vec,
495 cf1_u_i.clone(),
496 cf1_cmT.clone(),
497 )?;
498 // Convert cf1_r_bits to a `NonNativeFieldVar`
499 let cf1_r_nonnat = {
500 let mut bits = cf1_r_bits.clone();
501 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
502 NonNativeUintVar::from(&bits)
503 };
504 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
505 let cf1_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
506 cf1_r_bits,
507 cf1_r_nonnat,
508 cf1_cmT,
509 cf_U_i,
510 cf1_u_i,
511 )?;
512
513 // same for cf2_r:
514 let cf2_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
515 cs.clone(),
516 &self.poseidon_config,
517 cf1_U_i1.to_constraint_field()?,
518 cf2_u_i.clone(),
519 cf2_cmT.clone(),
520 )?;
521 let cf2_r_nonnat = {
522 let mut bits = cf2_r_bits.clone();
523 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
524 NonNativeUintVar::from(&bits)
525 };
526 let cf_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
527 cf2_r_bits,
528 cf2_r_nonnat,
529 cf2_cmT,
530 cf1_U_i1, // the output from NIFS.V(cf1_r, cf_U, cfE_u)
531 cf2_u_i,
532 )?;
533
534 // Back to Primary Part
535 // P.4.b compute and check the second output of F'
536 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
537 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
538 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&crh_params)?;
539 let (cf_u_i1_x_base, _) =
540 CycleFoldCommittedInstanceVar::new_constant(cs.clone(), cf_u_dummy)?
541 .hash(&crh_params)?;
542 let cf_x = FpVar::new_input(cs.clone(), || {
543 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
544 })?;
545 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
546
547 Ok(())
548 }
549}
550
551#[cfg(test)]
552pub mod tests {
553 use super::*;
554 use ark_bn254::{Fr, G1Projective as Projective};
555 use ark_ff::BigInteger;
556 use ark_relations::r1cs::ConstraintSystem;
557 use ark_std::UniformRand;
558
559 use crate::commitment::pedersen::Pedersen;
560 use crate::folding::nova::nifs::tests::prepare_simple_fold_inputs;
561 use crate::folding::nova::nifs::NIFS;
562 use crate::transcript::poseidon::poseidon_test_config;
563
564 #[test]
565 fn test_committed_instance_var() {
566 let mut rng = ark_std::test_rng();
567
568 let ci = CommittedInstance::<Projective> {
569 cmE: Projective::rand(&mut rng),
570 u: Fr::rand(&mut rng),
571 cmW: Projective::rand(&mut rng),
572 x: vec![Fr::rand(&mut rng); 1],
573 };
574
575 let cs = ConstraintSystem::<Fr>::new_ref();
576 let ciVar =
577 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
578 assert_eq!(ciVar.u.value().unwrap(), ci.u);
579 assert_eq!(ciVar.x.value().unwrap(), ci.x);
580 // the values cmE and cmW are checked in the CycleFold's circuit
581 // CommittedInstanceInCycleFoldVar in
582 // nova::cyclefold::tests::test_committed_instance_cyclefold_var
583 }
584
585 #[test]
586 fn test_nifs_gadget() {
587 let (_, _, _, _, ci1, _, ci2, _, ci3, _, cmT, _, r_Fr) = prepare_simple_fold_inputs();
588
589 let ci3_verifier = NIFS::<Projective, Pedersen<Projective>>::verify(r_Fr, &ci1, &ci2, &cmT);
590 assert_eq!(ci3_verifier, ci3);
591
592 let cs = ConstraintSystem::<Fr>::new_ref();
593
594 let rVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(r_Fr)).unwrap();
595 let ci1Var =
596 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci1.clone()))
597 .unwrap();
598 let ci2Var =
599 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci2.clone()))
600 .unwrap();
601 let ci3Var =
602 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci3.clone()))
603 .unwrap();
604
605 NIFSGadget::<Projective>::verify(
606 rVar.clone(),
607 ci1Var.clone(),
608 ci2Var.clone(),
609 ci3Var.clone(),
610 )
611 .unwrap();
612 assert!(cs.is_satisfied().unwrap());
613 }
614
615 #[test]
616 fn test_committed_instance_hash() {
617 let mut rng = ark_std::test_rng();
618 let poseidon_config = poseidon_test_config::<Fr>();
619
620 let i = Fr::from(3_u32);
621 let z_0 = vec![Fr::from(3_u32)];
622 let z_i = vec![Fr::from(3_u32)];
623 let ci = CommittedInstance::<Projective> {
624 cmE: Projective::rand(&mut rng),
625 u: Fr::rand(&mut rng),
626 cmW: Projective::rand(&mut rng),
627 x: vec![Fr::rand(&mut rng); 1],
628 };
629
630 // compute the CommittedInstance hash natively
631 let h = ci
632 .hash(&poseidon_config, i, z_0.clone(), z_i.clone())
633 .unwrap();
634
635 let cs = ConstraintSystem::<Fr>::new_ref();
636
637 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
638 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
639 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
640 let ciVar =
641 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
642
643 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
644
645 // compute the CommittedInstance hash in-circuit
646 let (hVar, _) = ciVar.hash(&crh_params, iVar, z_0Var, z_iVar).unwrap();
647 assert!(cs.is_satisfied().unwrap());
648
649 // check that the natively computed and in-circuit computed hashes match
650 assert_eq!(hVar.value().unwrap(), h);
651 }
652
653 // checks that the gadget and native implementations of the challenge computation match
654 #[test]
655 fn test_challenge_gadget() {
656 let mut rng = ark_std::test_rng();
657 let poseidon_config = poseidon_test_config::<Fr>();
658
659 let u_i = CommittedInstance::<Projective> {
660 cmE: Projective::rand(&mut rng),
661 u: Fr::rand(&mut rng),
662 cmW: Projective::rand(&mut rng),
663 x: vec![Fr::rand(&mut rng); 1],
664 };
665 let U_i = CommittedInstance::<Projective> {
666 cmE: Projective::rand(&mut rng),
667 u: Fr::rand(&mut rng),
668 cmW: Projective::rand(&mut rng),
669 x: vec![Fr::rand(&mut rng); 1],
670 };
671 let cmT = Projective::rand(&mut rng);
672
673 // compute the challenge natively
674 let r_bits = ChallengeGadget::<Projective>::get_challenge_native(
675 &poseidon_config,
676 U_i.clone(),
677 u_i.clone(),
678 cmT,
679 )
680 .unwrap();
681 let r = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
682
683 let cs = ConstraintSystem::<Fr>::new_ref();
684 let u_iVar =
685 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(u_i.clone()))
686 .unwrap();
687 let U_iVar =
688 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(U_i.clone()))
689 .unwrap();
690 let cmTVar = NonNativeAffineVar::<Projective>::new_witness(cs.clone(), || Ok(cmT)).unwrap();
691
692 // compute the challenge in-circuit
693 let U_iVar_vec = [
694 vec![U_iVar.u.clone()],
695 U_iVar.x.clone(),
696 U_iVar.cmE.to_constraint_field().unwrap(),
697 U_iVar.cmW.to_constraint_field().unwrap(),
698 ]
699 .concat();
700 let r_bitsVar = ChallengeGadget::<Projective>::get_challenge_gadget(
701 cs.clone(),
702 &poseidon_config,
703 U_iVar_vec,
704 u_iVar,
705 cmTVar,
706 )
707 .unwrap();
708 assert!(cs.is_satisfied().unwrap());
709
710 // check that the natively computed and in-circuit computed hashes match
711 let rVar = Boolean::le_bits_to_fp_var(&r_bitsVar).unwrap();
712 assert_eq!(rVar.value().unwrap(), r);
713 assert_eq!(r_bitsVar.value().unwrap(), r_bits);
714 }
715}