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