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