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::CommittedInstance;
27use crate::constants::N_BITS_RO;
28use crate::folding::circuits::{
29 cyclefold::{
30 CycleFoldChallengeGadget, CycleFoldCommittedInstanceVar, NIFSFullGadget, CF_IO_LEN,
31 },
32 nonnative::{
33 affine::{nonnative_affine_to_field_elements, NonNativeAffineVar},
34 uint::NonNativeUintVar,
35 },
36 CF1, CF2,
37};
38use crate::frontend::FCircuit;
39
40/// CommittedInstanceVar contains the u, x, cmE and cmW values which are folded on the main Nova
41/// constraints field (E1::Fr, where E1 is the main curve). The peculiarity is that cmE and cmW are
42/// represented non-natively over the constraint field.
43#[derive(Debug, Clone)]
44pub struct CommittedInstanceVar<C: CurveGroup>
45where
46 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
47{
48 pub u: FpVar<C::ScalarField>,
49 pub x: Vec<FpVar<C::ScalarField>>,
50 pub cmE: NonNativeAffineVar<C>,
51 pub cmW: NonNativeAffineVar<C>,
52}
53
54impl<C> AllocVar<CommittedInstance<C>, CF1<C>> for CommittedInstanceVar<C>
55where
56 C: CurveGroup,
57 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
58{
59 fn new_variable<T: Borrow<CommittedInstance<C>>>(
60 cs: impl Into<Namespace<CF1<C>>>,
61 f: impl FnOnce() -> Result<T, SynthesisError>,
62 mode: AllocationMode,
63 ) -> Result<Self, SynthesisError> {
64 f().and_then(|val| {
65 let cs = cs.into();
66
67 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
68 let x: Vec<FpVar<C::ScalarField>> =
69 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
70
71 let cmE =
72 NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().cmE), mode)?;
73 let cmW =
74 NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().cmW), mode)?;
75
76 Ok(Self { u, x, cmE, cmW })
77 })
78 }
79}
80
81impl<C> CommittedInstanceVar<C>
82where
83 C: CurveGroup,
84 <C as Group>::ScalarField: Absorb,
85 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
86{
87 /// hash implements the committed instance hash compatible with the native implementation from
88 /// CommittedInstance.hash.
89 /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the
90 /// `CommittedInstance`.
91 /// Additionally it returns the vector of the field elements from the self parameters, so they
92 /// can be reused in other gadgets avoiding recalculating (reconstraining) them.
93 #[allow(clippy::type_complexity)]
94 pub fn hash(
95 self,
96 crh_params: &CRHParametersVar<CF1<C>>,
97 i: FpVar<CF1<C>>,
98 z_0: Vec<FpVar<CF1<C>>>,
99 z_i: Vec<FpVar<CF1<C>>>,
100 ) -> Result<(FpVar<CF1<C>>, Vec<FpVar<CF1<C>>>), SynthesisError> {
101 let U_vec = [
102 vec![self.u],
103 self.x,
104 self.cmE.to_constraint_field()?,
105 self.cmW.to_constraint_field()?,
106 ]
107 .concat();
108 let input = [vec![i], z_0, z_i, U_vec.clone()].concat();
109 Ok((
110 CRHGadget::<C::ScalarField>::evaluate(crh_params, &input)?,
111 U_vec,
112 ))
113 }
114}
115
116/// Implements the circuit that does the checks of the Non-Interactive Folding Scheme Verifier
117/// described in section 4 of [Nova](https://eprint.iacr.org/2021/370.pdf), where the cmE & cmW checks are
118/// delegated to the NIFSCycleFoldGadget.
119pub struct NIFSGadget<C: CurveGroup> {
120 _c: PhantomData<C>,
121}
122
123impl<C: CurveGroup> NIFSGadget<C>
124where
125 C: CurveGroup,
126 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
127{
128 pub fn fold_committed_instance(
129 r: FpVar<CF1<C>>,
130 ci1: CommittedInstanceVar<C>, // U_i
131 ci2: CommittedInstanceVar<C>, // u_i
132 ) -> Result<CommittedInstanceVar<C>, SynthesisError> {
133 Ok(CommittedInstanceVar {
134 cmE: NonNativeAffineVar::new_constant(ConstraintSystemRef::None, C::zero())?,
135 cmW: NonNativeAffineVar::new_constant(ConstraintSystemRef::None, C::zero())?,
136 // ci3.u = ci1.u + r * ci2.u
137 u: ci1.u + &r * ci2.u,
138 // ci3.x = ci1.x + r * ci2.x
139 x: ci1
140 .x
141 .iter()
142 .zip(ci2.x)
143 .map(|(a, b)| a + &r * &b)
144 .collect::<Vec<FpVar<CF1<C>>>>(),
145 })
146 }
147
148 /// Implements the constraints for NIFS.V for u and x, since cm(E) and cm(W) are delegated to
149 /// the CycleFold circuit.
150 pub fn verify(
151 r: FpVar<CF1<C>>,
152 ci1: CommittedInstanceVar<C>, // U_i
153 ci2: CommittedInstanceVar<C>, // u_i
154 ci3: CommittedInstanceVar<C>, // U_{i+1}
155 ) -> Result<(), SynthesisError> {
156 let ci = Self::fold_committed_instance(r, ci1, ci2)?;
157
158 ci.u.enforce_equal(&ci3.u)?;
159 ci.x.enforce_equal(&ci3.x)?;
160
161 Ok(())
162 }
163}
164
165/// ChallengeGadget computes the RO challenge used for the Nova instances NIFS, it contains a
166/// rust-native and a in-circuit compatible versions.
167pub struct ChallengeGadget<C: CurveGroup> {
168 _c: PhantomData<C>,
169}
170impl<C: CurveGroup> ChallengeGadget<C>
171where
172 C: CurveGroup,
173 <C as CurveGroup>::BaseField: PrimeField,
174 <C as Group>::ScalarField: Absorb,
175{
176 pub fn get_challenge_native(
177 poseidon_config: &PoseidonConfig<C::ScalarField>,
178 U_i: CommittedInstance<C>,
179 u_i: CommittedInstance<C>,
180 cmT: C,
181 ) -> Result<Vec<bool>, SynthesisError> {
182 let (U_cmE_x, U_cmE_y) = nonnative_affine_to_field_elements::<C>(U_i.cmE)?;
183 let (U_cmW_x, U_cmW_y) = nonnative_affine_to_field_elements::<C>(U_i.cmW)?;
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 (cmT_x, cmT_y) = nonnative_affine_to_field_elements::<C>(cmT)?;
187
188 let mut sponge = PoseidonSponge::<C::ScalarField>::new(poseidon_config);
189 let input = vec![
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 vec![u_i.u],
197 u_i.x.clone(),
198 u_cmE_x,
199 u_cmE_y,
200 u_cmW_x,
201 u_cmW_y,
202 cmT_x,
203 cmT_y,
204 ]
205 .concat();
206 sponge.absorb(&input);
207 let bits = sponge.squeeze_bits(N_BITS_RO);
208 Ok(bits)
209 }
210
211 // compatible with the native get_challenge_native
212 pub fn get_challenge_gadget(
213 cs: ConstraintSystemRef<C::ScalarField>,
214 poseidon_config: &PoseidonConfig<C::ScalarField>,
215 U_i_vec: Vec<FpVar<CF1<C>>>, // apready processed input, so we don't have to recompute these values
216 u_i: CommittedInstanceVar<C>,
217 cmT: NonNativeAffineVar<C>,
218 ) -> Result<Vec<Boolean<C::ScalarField>>, SynthesisError> {
219 let mut sponge = PoseidonSpongeVar::<C::ScalarField>::new(cs, poseidon_config);
220
221 let input: Vec<FpVar<C::ScalarField>> = [
222 U_i_vec,
223 vec![u_i.u.clone()],
224 u_i.x.clone(),
225 u_i.cmE.to_constraint_field()?,
226 u_i.cmW.to_constraint_field()?,
227 cmT.to_constraint_field()?,
228 ]
229 .concat();
230 sponge.absorb(&input)?;
231 let bits = sponge.squeeze_bits(N_BITS_RO)?;
232 Ok(bits)
233 }
234}
235
236/// AugmentedFCircuit implements the F' circuit (augmented F) defined in
237/// [Nova](https://eprint.iacr.org/2021/370.pdf) together with the extra constraints defined in
238/// [CycleFold](https://eprint.iacr.org/2023/1192.pdf).
239#[derive(Debug, Clone)]
240pub struct AugmentedFCircuit<
241 C1: CurveGroup,
242 C2: CurveGroup,
243 GC2: CurveVar<C2, CF2<C2>>,
244 FC: FCircuit<CF1<C1>>,
245> where
246 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
247{
248 pub _gc2: PhantomData<GC2>,
249 pub poseidon_config: PoseidonConfig<CF1<C1>>,
250 pub i: Option<CF1<C1>>,
251 pub i_usize: Option<usize>,
252 pub z_0: Option<Vec<C1::ScalarField>>,
253 pub z_i: Option<Vec<C1::ScalarField>>,
254 pub external_inputs: Option<Vec<C1::ScalarField>>,
255 pub u_i_cmW: Option<C1>,
256 pub U_i: Option<CommittedInstance<C1>>,
257 pub U_i1_cmE: Option<C1>,
258 pub U_i1_cmW: Option<C1>,
259 pub cmT: Option<C1>,
260 pub F: FC, // F circuit
261 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
262
263 // cyclefold verifier on C1
264 // Here 'cf1, cf2' are for each of the CycleFold circuits, corresponding to the fold of cmW and
265 // cmE respectively
266 pub cf1_u_i_cmW: Option<C2>, // input
267 pub cf2_u_i_cmW: Option<C2>, // input
268 pub cf_U_i: Option<CommittedInstance<C2>>, // input
269 pub cf1_cmT: Option<C2>,
270 pub cf2_cmT: Option<C2>,
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 external_inputs: None,
288 u_i_cmW: None,
289 U_i: None,
290 U_i1_cmE: None,
291 U_i1_cmW: None,
292 cmT: None,
293 F: F_circuit,
294 x: None,
295 // cyclefold values
296 cf1_u_i_cmW: None,
297 cf2_u_i_cmW: None,
298 cf_U_i: None,
299 cf1_cmT: None,
300 cf2_cmT: None,
301 cf_x: None,
302 }
303 }
304}
305
306impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
307where
308 C1: CurveGroup,
309 C2: CurveGroup,
310 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
311 FC: FCircuit<CF1<C1>>,
312 <C1 as CurveGroup>::BaseField: PrimeField,
313 <C2 as CurveGroup>::BaseField: PrimeField,
314 <C1 as Group>::ScalarField: Absorb,
315 <C2 as Group>::ScalarField: Absorb,
316 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
317 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
318{
319 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
320 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
321 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
322 })?;
323 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
324 Ok(self
325 .z_0
326 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
327 })?;
328 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
329 Ok(self
330 .z_i
331 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
332 })?;
333 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
334 Ok(self
335 .external_inputs
336 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_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 =
368 self.F
369 .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?;
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_canonical_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_canonical_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_canonical_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}