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