arnaucube
arnaucube/sonobePublic Self-hosted repository
sonobe/folding-schemes/src/folding/nova/decider_eth_circuit.rs
folding-schemes/src/folding/nova/decider_eth_circuit.rsRaw
  1/// This file implements the onchain (Ethereum's EVM) decider circuit. For non-ethereum use cases,
  2/// other more efficient approaches can be used.
  3use ark_crypto_primitives::crh::poseidon::constraints::CRHParametersVar;
  4use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
  5use ark_ec::{CurveGroup, Group};
  6use ark_ff::{BigInteger, PrimeField};
  7use ark_poly::Polynomial;
  8use ark_r1cs_std::{
  9    alloc::{AllocVar, AllocationMode},
 10    boolean::Boolean,
 11    eq::EqGadget,
 12    fields::{fp::FpVar, FieldVar},
 13    groups::GroupOpsBounds,
 14    poly::{domain::Radix2DomainVar, evaluations::univariate::EvaluationsVar},
 15    prelude::CurveVar,
 16    ToConstraintFieldGadget,
 17};
 18use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
 19use ark_std::{log2, Zero};
 20use core::{borrow::Borrow, marker::PhantomData};
 21
 22use super::{circuits::ChallengeGadget, nifs::NIFS};
 23use crate::ccs::r1cs::R1CS;
 24use crate::commitment::{pedersen::Params as PedersenParams, CommitmentScheme};
 25use crate::folding::circuits::{
 26    nonnative::{
 27        affine::{nonnative_affine_to_field_elements, NonNativeAffineVar},
 28        uint::NonNativeUintVar,
 29    },
 30    CF1, CF2,
 31};
 32use crate::folding::nova::{circuits::CommittedInstanceVar, CommittedInstance, Nova, Witness};
 33use crate::frontend::FCircuit;
 34use crate::transcript::{
 35    poseidon::{PoseidonTranscript, PoseidonTranscriptVar},
 36    Transcript, TranscriptVar,
 37};
 38use crate::utils::{
 39    gadgets::{MatrixGadget, SparseMatrixVar, VectorGadget},
 40    vec::poly_from_vec,
 41};
 42use crate::Error;
 43
 44#[derive(Debug, Clone)]
 45pub struct RelaxedR1CSGadget {}
 46impl RelaxedR1CSGadget {
 47    /// performs the RelaxedR1CS check for native variables (Az∘Bz==uCz+E)
 48    pub fn check_native<F: PrimeField>(
 49        r1cs: R1CSVar<F, F, FpVar<F>>,
 50        E: Vec<FpVar<F>>,
 51        u: FpVar<F>,
 52        z: Vec<FpVar<F>>,
 53    ) -> Result<(), SynthesisError> {
 54        let Az = r1cs.A.mul_vector(&z)?;
 55        let Bz = r1cs.B.mul_vector(&z)?;
 56        let Cz = r1cs.C.mul_vector(&z)?;
 57        let uCzE = Cz.mul_scalar(&u)?.add(&E)?;
 58        let AzBz = Az.hadamard(&Bz)?;
 59        AzBz.enforce_equal(&uCzE)?;
 60        Ok(())
 61    }
 62
 63    /// performs the RelaxedR1CS check for non-native variables (Az∘Bz==uCz+E)
 64    pub fn check_nonnative<F: PrimeField, CF: PrimeField>(
 65        r1cs: R1CSVar<F, CF, NonNativeUintVar<CF>>,
 66        E: Vec<NonNativeUintVar<CF>>,
 67        u: NonNativeUintVar<CF>,
 68        z: Vec<NonNativeUintVar<CF>>,
 69    ) -> Result<(), SynthesisError> {
 70        // First we do addition and multiplication without mod F's order
 71        let Az = r1cs.A.mul_vector(&z)?;
 72        let Bz = r1cs.B.mul_vector(&z)?;
 73        let Cz = r1cs.C.mul_vector(&z)?;
 74        let uCzE = Cz.mul_scalar(&u)?.add(&E)?;
 75        let AzBz = Az.hadamard(&Bz)?;
 76
 77        // Then we compare the results by checking if they are congruent
 78        // modulo the field order
 79        AzBz.into_iter()
 80            .zip(uCzE)
 81            .try_for_each(|(a, b)| a.enforce_congruent::<F>(&b))
 82    }
 83}
 84
 85#[derive(Debug, Clone)]
 86pub struct R1CSVar<F: PrimeField, CF: PrimeField, FV: AllocVar<F, CF>> {
 87    _f: PhantomData<F>,
 88    _cf: PhantomData<CF>,
 89    _fv: PhantomData<FV>,
 90    pub A: SparseMatrixVar<F, CF, FV>,
 91    pub B: SparseMatrixVar<F, CF, FV>,
 92    pub C: SparseMatrixVar<F, CF, FV>,
 93}
 94
 95impl<F, CF, FV> AllocVar<R1CS<F>, CF> for R1CSVar<F, CF, FV>
 96where
 97    F: PrimeField,
 98    CF: PrimeField,
 99    FV: AllocVar<F, CF>,
100{
101    fn new_variable<T: Borrow<R1CS<F>>>(
102        cs: impl Into<Namespace<CF>>,
103        f: impl FnOnce() -> Result<T, SynthesisError>,
104        _mode: AllocationMode,
105    ) -> Result<Self, SynthesisError> {
106        f().and_then(|val| {
107            let cs = cs.into();
108
109            let A = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().A)?;
110            let B = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().B)?;
111            let C = SparseMatrixVar::<F, CF, FV>::new_constant(cs.clone(), &val.borrow().C)?;
112
113            Ok(Self {
114                _f: PhantomData,
115                _cf: PhantomData,
116                _fv: PhantomData,
117                A,
118                B,
119                C,
120            })
121        })
122    }
123}
124
125/// In-circuit representation of the Witness associated to the CommittedInstance.
126#[derive(Debug, Clone)]
127pub struct WitnessVar<C: CurveGroup> {
128    pub E: Vec<FpVar<C::ScalarField>>,
129    pub rE: FpVar<C::ScalarField>,
130    pub W: Vec<FpVar<C::ScalarField>>,
131    pub rW: FpVar<C::ScalarField>,
132}
133
134impl<C> AllocVar<Witness<C>, CF1<C>> for WitnessVar<C>
135where
136    C: CurveGroup,
137    <C as ark_ec::CurveGroup>::BaseField: PrimeField,
138{
139    fn new_variable<T: Borrow<Witness<C>>>(
140        cs: impl Into<Namespace<CF1<C>>>,
141        f: impl FnOnce() -> Result<T, SynthesisError>,
142        mode: AllocationMode,
143    ) -> Result<Self, SynthesisError> {
144        f().and_then(|val| {
145            let cs = cs.into();
146
147            let E: Vec<FpVar<C::ScalarField>> =
148                Vec::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?;
149            let rE =
150                FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().rE), mode)?;
151
152            let W: Vec<FpVar<C::ScalarField>> =
153                Vec::new_variable(cs.clone(), || Ok(val.borrow().W.clone()), mode)?;
154            let rW =
155                FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().rW), mode)?;
156
157            Ok(Self { E, rE, W, rW })
158        })
159    }
160}
161
162/// In-circuit representation of the Witness associated to the CommittedInstance, but with
163/// non-native representation, since it is used to represent the CycleFold witness.
164#[derive(Debug, Clone)]
165pub struct CycleFoldWitnessVar<C: CurveGroup> {
166    pub E: Vec<NonNativeUintVar<CF2<C>>>,
167    pub rE: NonNativeUintVar<CF2<C>>,
168    pub W: Vec<NonNativeUintVar<CF2<C>>>,
169    pub rW: NonNativeUintVar<CF2<C>>,
170}
171
172impl<C> AllocVar<Witness<C>, CF2<C>> for CycleFoldWitnessVar<C>
173where
174    C: CurveGroup,
175    <C as ark_ec::CurveGroup>::BaseField: PrimeField,
176{
177    fn new_variable<T: Borrow<Witness<C>>>(
178        cs: impl Into<Namespace<CF2<C>>>,
179        f: impl FnOnce() -> Result<T, SynthesisError>,
180        mode: AllocationMode,
181    ) -> Result<Self, SynthesisError> {
182        f().and_then(|val| {
183            let cs = cs.into();
184
185            let E = Vec::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?;
186            let rE = NonNativeUintVar::new_variable(cs.clone(), || Ok(val.borrow().rE), mode)?;
187
188            let W = Vec::new_variable(cs.clone(), || Ok(val.borrow().W.clone()), mode)?;
189            let rW = NonNativeUintVar::new_variable(cs.clone(), || Ok(val.borrow().rW), mode)?;
190
191            Ok(Self { E, rE, W, rW })
192        })
193    }
194}
195
196/// Circuit that implements the in-circuit checks needed for the onchain (Ethereum's EVM)
197/// verification.
198#[derive(Clone, Debug)]
199pub struct DeciderEthCircuit<C1, GC1, C2, GC2, CS1, CS2>
200where
201    C1: CurveGroup,
202    GC1: CurveVar<C1, CF2<C1>>,
203    C2: CurveGroup,
204    GC2: CurveVar<C2, CF2<C2>>,
205    CS1: CommitmentScheme<C1>,
206    CS2: CommitmentScheme<C2>,
207{
208    _c1: PhantomData<C1>,
209    _gc1: PhantomData<GC1>,
210    _c2: PhantomData<C2>,
211    _gc2: PhantomData<GC2>,
212    _cs1: PhantomData<CS1>,
213    _cs2: PhantomData<CS2>,
214
215    /// E vector's length of the Nova instance witness
216    pub E_len: usize,
217    /// E vector's length of the CycleFold instance witness
218    pub cf_E_len: usize,
219    /// R1CS of the Augmented Function circuit
220    pub r1cs: R1CS<C1::ScalarField>,
221    /// R1CS of the CycleFold circuit
222    pub cf_r1cs: R1CS<C2::ScalarField>,
223    /// CycleFold PedersenParams over C2
224    pub cf_pedersen_params: PedersenParams<C2>,
225    pub poseidon_config: PoseidonConfig<CF1<C1>>,
226    pub i: Option<CF1<C1>>,
227    /// initial state
228    pub z_0: Option<Vec<C1::ScalarField>>,
229    /// current i-th state
230    pub z_i: Option<Vec<C1::ScalarField>>,
231    /// Nova instances
232    pub u_i: Option<CommittedInstance<C1>>,
233    pub w_i: Option<Witness<C1>>,
234    pub U_i: Option<CommittedInstance<C1>>,
235    pub W_i: Option<Witness<C1>>,
236    pub U_i1: Option<CommittedInstance<C1>>,
237    pub W_i1: Option<Witness<C1>>,
238    pub cmT: Option<C1>,
239    pub r: Option<C1::ScalarField>,
240    /// CycleFold running instance
241    pub cf_U_i: Option<CommittedInstance<C2>>,
242    pub cf_W_i: Option<Witness<C2>>,
243
244    /// KZG challenges
245    pub kzg_c_W: Option<C1::ScalarField>,
246    pub kzg_c_E: Option<C1::ScalarField>,
247    pub eval_W: Option<C1::ScalarField>,
248    pub eval_E: Option<C1::ScalarField>,
249}
250impl<C1, GC1, C2, GC2, CS1, CS2> DeciderEthCircuit<C1, GC1, C2, GC2, CS1, CS2>
251where
252    C1: CurveGroup,
253    C2: CurveGroup,
254    GC1: CurveVar<C1, CF2<C1>> + ToConstraintFieldGadget<CF2<C1>>,
255    GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
256    CS1: CommitmentScheme<C1>,
257    // enforce that the CS2 is Pedersen commitment scheme, since we're at Ethereum's EVM decider
258    CS2: CommitmentScheme<C2, ProverParams = PedersenParams<C2>>,
259    <C1 as Group>::ScalarField: Absorb,
260    <C1 as CurveGroup>::BaseField: PrimeField,
261{
262    pub fn from_nova<FC: FCircuit<C1::ScalarField>>(
263        nova: Nova<C1, GC1, C2, GC2, FC, CS1, CS2>,
264    ) -> Result<Self, Error> {
265        // compute the U_{i+1}, W_{i+1}
266        let (T, cmT) = NIFS::<C1, CS1>::compute_cmT(
267            &nova.cs_pp,
268            &nova.r1cs.clone(),
269            &nova.w_i.clone(),
270            &nova.u_i.clone(),
271            &nova.W_i.clone(),
272            &nova.U_i.clone(),
273        )?;
274        let r_bits = ChallengeGadget::<C1>::get_challenge_native(
275            &nova.poseidon_config,
276            nova.U_i.clone(),
277            nova.u_i.clone(),
278            cmT,
279        )?;
280        let r_Fr = C1::ScalarField::from_bigint(BigInteger::from_bits_le(&r_bits))
281            .ok_or(Error::OutOfBounds)?;
282        let (W_i1, U_i1) = NIFS::<C1, CS1>::fold_instances(
283            r_Fr, &nova.W_i, &nova.U_i, &nova.w_i, &nova.u_i, &T, cmT,
284        )?;
285
286        // compute the KZG challenges used as inputs in the circuit
287        let (kzg_challenge_W, kzg_challenge_E) =
288            KZGChallengesGadget::<C1>::get_challenges_native(&nova.poseidon_config, U_i1.clone())?;
289
290        // get KZG evals
291        let mut W = W_i1.W.clone();
292        W.extend(
293            std::iter::repeat(C1::ScalarField::zero())
294                .take(W_i1.W.len().next_power_of_two() - W_i1.W.len()),
295        );
296        let mut E = W_i1.E.clone();
297        E.extend(
298            std::iter::repeat(C1::ScalarField::zero())
299                .take(W_i1.E.len().next_power_of_two() - W_i1.E.len()),
300        );
301        let p_W = poly_from_vec(W.to_vec())?;
302        let eval_W = p_W.evaluate(&kzg_challenge_W);
303        let p_E = poly_from_vec(E.to_vec())?;
304        let eval_E = p_E.evaluate(&kzg_challenge_E);
305
306        Ok(Self {
307            _c1: PhantomData,
308            _gc1: PhantomData,
309            _c2: PhantomData,
310            _gc2: PhantomData,
311            _cs1: PhantomData,
312            _cs2: PhantomData,
313
314            E_len: nova.W_i.E.len(),
315            cf_E_len: nova.cf_W_i.E.len(),
316            r1cs: nova.r1cs,
317            cf_r1cs: nova.cf_r1cs,
318            cf_pedersen_params: nova.cf_cs_pp,
319            poseidon_config: nova.poseidon_config,
320            i: Some(nova.i),
321            z_0: Some(nova.z_0),
322            z_i: Some(nova.z_i),
323            u_i: Some(nova.u_i),
324            w_i: Some(nova.w_i),
325            U_i: Some(nova.U_i),
326            W_i: Some(nova.W_i),
327            U_i1: Some(U_i1),
328            W_i1: Some(W_i1),
329            cmT: Some(cmT),
330            r: Some(r_Fr),
331            cf_U_i: Some(nova.cf_U_i),
332            cf_W_i: Some(nova.cf_W_i),
333            kzg_c_W: Some(kzg_challenge_W),
334            kzg_c_E: Some(kzg_challenge_E),
335            eval_W: Some(eval_W),
336            eval_E: Some(eval_E),
337        })
338    }
339}
340
341impl<C1, GC1, C2, GC2, CS1, CS2> ConstraintSynthesizer<CF1<C1>>
342    for DeciderEthCircuit<C1, GC1, C2, GC2, CS1, CS2>
343where
344    C1: CurveGroup,
345    C2: CurveGroup,
346    GC1: CurveVar<C1, CF2<C1>>,
347    GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
348    CS1: CommitmentScheme<C1>,
349    CS2: CommitmentScheme<C2>,
350    <C1 as CurveGroup>::BaseField: PrimeField,
351    <C2 as CurveGroup>::BaseField: PrimeField,
352    <C1 as Group>::ScalarField: Absorb,
353    <C2 as Group>::ScalarField: Absorb,
354    C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
355    for<'b> &'b GC2: GroupOpsBounds<'b, C2, GC2>,
356{
357    fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
358        let r1cs =
359            R1CSVar::<C1::ScalarField, CF1<C1>, FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
360                Ok(self.r1cs.clone())
361            })?;
362
363        let i =
364            FpVar::<CF1<C1>>::new_input(cs.clone(), || Ok(self.i.unwrap_or_else(CF1::<C1>::zero)))?;
365        let z_0 = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
366            Ok(self.z_0.unwrap_or(vec![CF1::<C1>::zero()]))
367        })?;
368        let z_i = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
369            Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
370        })?;
371
372        let u_dummy_native = CommittedInstance::<C1>::dummy(2);
373        let w_dummy_native = Witness::<C1>::new(
374            vec![C1::ScalarField::zero(); self.r1cs.A.n_cols - 3 /* (3=2+1, since u_i.x.len=2) */],
375            self.E_len,
376        );
377
378        let u_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
379            Ok(self.u_i.unwrap_or(u_dummy_native.clone()))
380        })?;
381        let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
382            Ok(self.U_i.unwrap_or(u_dummy_native.clone()))
383        })?;
384        // here (U_i1, W_i1) = NIFS.P( (U_i,W_i), (u_i,w_i))
385        let U_i1 = CommittedInstanceVar::<C1>::new_input(cs.clone(), || {
386            Ok(self.U_i1.unwrap_or(u_dummy_native.clone()))
387        })?;
388        let W_i1 = WitnessVar::<C1>::new_witness(cs.clone(), || {
389            Ok(self.W_i1.unwrap_or(w_dummy_native.clone()))
390        })?;
391
392        // allocate the inputs for the check 6
393        let kzg_c_W = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
394            Ok(self.kzg_c_W.unwrap_or_else(CF1::<C1>::zero))
395        })?;
396        let kzg_c_E = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
397            Ok(self.kzg_c_E.unwrap_or_else(CF1::<C1>::zero))
398        })?;
399        let _eval_W = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
400            Ok(self.eval_W.unwrap_or_else(CF1::<C1>::zero))
401        })?;
402        let _eval_E = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
403            Ok(self.eval_E.unwrap_or_else(CF1::<C1>::zero))
404        })?;
405
406        let crh_params = CRHParametersVar::<C1::ScalarField>::new_constant(
407            cs.clone(),
408            self.poseidon_config.clone(),
409        )?;
410
411        // 1. check RelaxedR1CS of U_{i+1}
412        let z_U1: Vec<FpVar<CF1<C1>>> =
413            [vec![U_i1.u.clone()], U_i1.x.to_vec(), W_i1.W.to_vec()].concat();
414        RelaxedR1CSGadget::check_native(r1cs, W_i1.E.clone(), U_i1.u.clone(), z_U1)?;
415
416        // 2. u_i.cmE==cm(0), u_i.u==1
417        // Here zero is the x & y coordinates of the zero point affine representation.
418        let zero = NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::zero())?;
419        u_i.cmE.x.enforce_equal_unaligned(&zero)?;
420        u_i.cmE.y.enforce_equal_unaligned(&zero)?;
421        (u_i.u.is_one()?).enforce_equal(&Boolean::TRUE)?;
422
423        // 3.a u_i.x[0] == H(i, z_0, z_i, U_i)
424        let (u_i_x, U_i_vec) =
425            U_i.clone()
426                .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
427        (u_i.x[0]).enforce_equal(&u_i_x)?;
428
429        #[cfg(feature = "light-test")]
430        println!("[WARNING]: Running with the 'light-test' feature, skipping the big part of the DeciderEthCircuit.\n           Only for testing purposes.");
431
432        // The following two checks (and their respective allocations) are disabled for normal
433        // tests since they take several millions of constraints and would take several minutes
434        // (and RAM) to run the test. It is active by default, and not active only when
435        // 'light-test' feature is used.
436        #[cfg(not(feature = "light-test"))]
437        {
438            // imports here instead of at the top of the file, so we avoid having multiple
439            // `#[cfg(not(test))]`
440            use crate::commitment::pedersen::PedersenGadget;
441            use crate::folding::circuits::cyclefold::{CycleFoldCommittedInstanceVar, CF_IO_LEN};
442            use ark_r1cs_std::ToBitsGadget;
443
444            let cf_u_dummy_native = CommittedInstance::<C2>::dummy(CF_IO_LEN);
445            let w_dummy_native = Witness::<C2>::new(
446                vec![C2::ScalarField::zero(); self.cf_r1cs.A.n_cols - 1 - self.cf_r1cs.l],
447                self.cf_E_len,
448            );
449            let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
450                Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
451            })?;
452            let cf_W_i = CycleFoldWitnessVar::<C2>::new_witness(cs.clone(), || {
453                Ok(self.cf_W_i.unwrap_or(w_dummy_native.clone()))
454            })?;
455
456            // 3.b u_i.x[1] == H(cf_U_i)
457            let (cf_u_i_x, _) = cf_U_i.clone().hash(&crh_params)?;
458            (u_i.x[1]).enforce_equal(&cf_u_i_x)?;
459
460            // 4. check Pedersen commitments of cf_U_i.{cmE, cmW}
461            let H = GC2::new_constant(cs.clone(), self.cf_pedersen_params.h)?;
462            let G = Vec::<GC2>::new_constant(cs.clone(), self.cf_pedersen_params.generators)?;
463            let cf_W_i_E_bits: Result<Vec<Vec<Boolean<CF1<C1>>>>, SynthesisError> =
464                cf_W_i.E.iter().map(|E_i| E_i.to_bits_le()).collect();
465            let cf_W_i_W_bits: Result<Vec<Vec<Boolean<CF1<C1>>>>, SynthesisError> =
466                cf_W_i.W.iter().map(|W_i| W_i.to_bits_le()).collect();
467
468            let computed_cmE = PedersenGadget::<C2, GC2>::commit(
469                H.clone(),
470                G.clone(),
471                cf_W_i_E_bits?,
472                cf_W_i.rE.to_bits_le()?,
473            )?;
474            cf_U_i.cmE.enforce_equal(&computed_cmE)?;
475            let computed_cmW =
476                PedersenGadget::<C2, GC2>::commit(H, G, cf_W_i_W_bits?, cf_W_i.rW.to_bits_le()?)?;
477            cf_U_i.cmW.enforce_equal(&computed_cmW)?;
478
479            let cf_r1cs =
480                R1CSVar::<C1::BaseField, CF1<C1>, NonNativeUintVar<CF1<C1>>>::new_witness(
481                    cs.clone(),
482                    || Ok(self.cf_r1cs.clone()),
483                )?;
484
485            // 5. check RelaxedR1CS of cf_U_i
486            let cf_z_U = [vec![cf_U_i.u.clone()], cf_U_i.x.to_vec(), cf_W_i.W.to_vec()].concat();
487            RelaxedR1CSGadget::check_nonnative(cf_r1cs, cf_W_i.E, cf_U_i.u.clone(), cf_z_U)?;
488        }
489
490        // 6. check KZG challenges
491        let (incircuit_c_W, incircuit_c_E) = KZGChallengesGadget::<C1>::get_challenges_gadget(
492            cs.clone(),
493            &self.poseidon_config,
494            U_i1.clone(),
495        )?;
496        incircuit_c_W.enforce_equal(&kzg_c_W)?;
497        incircuit_c_E.enforce_equal(&kzg_c_E)?;
498
499        // Check 7 is temporary disabled due
500        // https://github.com/privacy-scaling-explorations/sonobe/issues/80
501        //
502        // 7. check eval_W==p_W(c_W) and eval_E==p_E(c_E)
503        // let incircuit_eval_W = evaluate_gadget::<CF1<C1>>(W_i1.W, incircuit_c_W)?;
504        // let incircuit_eval_E = evaluate_gadget::<CF1<C1>>(W_i1.E, incircuit_c_E)?;
505        // incircuit_eval_W.enforce_equal(&eval_W)?;
506        // incircuit_eval_E.enforce_equal(&eval_E)?;
507
508        // 8. compute the NIFS.V challenge and check that matches the one from the public input (so we
509        // avoid the verifier computing it)
510        let cmT =
511            NonNativeAffineVar::new_input(cs.clone(), || Ok(self.cmT.unwrap_or_else(C1::zero)))?;
512        let r_bits = ChallengeGadget::<C1>::get_challenge_gadget(
513            cs.clone(),
514            &self.poseidon_config,
515            U_i_vec,
516            u_i.clone(),
517            cmT.clone(),
518        )?;
519        let r_Fr = Boolean::le_bits_to_fp_var(&r_bits)?;
520        // check that the in-circuit computed r is equal to the inputted r
521        let r =
522            FpVar::<CF1<C1>>::new_input(cs.clone(), || Ok(self.r.unwrap_or_else(CF1::<C1>::zero)))?;
523        r_Fr.enforce_equal(&r)?;
524
525        Ok(())
526    }
527}
528
529/// Interpolates the polynomial from the given vector, and then returns it's evaluation at the
530/// given point.
531#[allow(unused)] // unused while check 7 is disabled
532fn evaluate_gadget<F: PrimeField>(
533    v: Vec<FpVar<F>>,
534    point: FpVar<F>,
535) -> Result<FpVar<F>, SynthesisError> {
536    if !v.len().is_power_of_two() {
537        return Err(SynthesisError::Unsatisfiable);
538    }
539    let n = v.len() as u64;
540    let gen = F::get_root_of_unity(n).unwrap();
541    let domain = Radix2DomainVar::new(gen, log2(v.len()) as u64, FpVar::one()).unwrap();
542
543    let evaluations_var = EvaluationsVar::from_vec_and_domain(v, domain, true);
544    evaluations_var.interpolate_and_evaluate(&point)
545}
546
547/// Gadget that computes the KZG challenges, also offers the rust native implementation compatible
548/// with the gadget.
549pub struct KZGChallengesGadget<C: CurveGroup> {
550    _c: PhantomData<C>,
551}
552#[allow(clippy::type_complexity)]
553impl<C> KZGChallengesGadget<C>
554where
555    C: CurveGroup,
556    C::ScalarField: PrimeField,
557    <C as CurveGroup>::BaseField: PrimeField,
558    C::ScalarField: Absorb,
559{
560    pub fn get_challenges_native(
561        poseidon_config: &PoseidonConfig<C::ScalarField>,
562        U_i: CommittedInstance<C>,
563    ) -> Result<(C::ScalarField, C::ScalarField), Error> {
564        let (cmE_x_limbs, cmE_y_limbs) = nonnative_affine_to_field_elements(U_i.cmE)?;
565        let (cmW_x_limbs, cmW_y_limbs) = nonnative_affine_to_field_elements(U_i.cmW)?;
566
567        let transcript = &mut PoseidonTranscript::<C>::new(poseidon_config);
568        // compute the KZG challenges, which are computed in-circuit and checked that it matches
569        // the inputted one
570        transcript.absorb_vec(&cmW_x_limbs);
571        transcript.absorb_vec(&cmW_y_limbs);
572        let challenge_W = transcript.get_challenge();
573        transcript.absorb_vec(&cmE_x_limbs);
574        transcript.absorb_vec(&cmE_y_limbs);
575        let challenge_E = transcript.get_challenge();
576
577        Ok((challenge_W, challenge_E))
578    }
579    // compatible with the native get_challenges_native
580    pub fn get_challenges_gadget(
581        cs: ConstraintSystemRef<C::ScalarField>,
582        poseidon_config: &PoseidonConfig<C::ScalarField>,
583        U_i: CommittedInstanceVar<C>,
584    ) -> Result<(FpVar<C::ScalarField>, FpVar<C::ScalarField>), SynthesisError> {
585        let mut transcript =
586            PoseidonTranscriptVar::<CF1<C>>::new(cs.clone(), &poseidon_config.clone());
587
588        transcript.absorb_vec(&U_i.cmW.to_constraint_field()?[..])?;
589        let challenge_W = transcript.get_challenge()?;
590
591        transcript.absorb_vec(&U_i.cmE.to_constraint_field()?[..])?;
592        let challenge_E = transcript.get_challenge()?;
593
594        Ok((challenge_W, challenge_E))
595    }
596}
597
598#[cfg(test)]
599pub mod tests {
600    use ark_crypto_primitives::crh::{
601        sha256::{
602            constraints::{Sha256Gadget, UnitVar},
603            Sha256,
604        },
605        CRHScheme, CRHSchemeGadget,
606    };
607    use ark_pallas::{constraints::GVar, Fq, Fr, Projective};
608    use ark_r1cs_std::bits::uint8::UInt8;
609    use ark_relations::r1cs::ConstraintSystem;
610    use ark_std::{One, UniformRand};
611    use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
612
613    use super::*;
614    use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z};
615    use crate::ccs::r1cs::{extract_r1cs, extract_w_x};
616    use crate::commitment::pedersen::Pedersen;
617    use crate::folding::nova::{get_cs_params_len, ProverParams, VerifierParams};
618    use crate::frontend::tests::{CubicFCircuit, CustomFCircuit, WrapperCircuit};
619    use crate::transcript::poseidon::poseidon_canonical_config;
620    use crate::FoldingScheme;
621
622    #[test]
623    fn test_relaxed_r1cs_small_gadget_handcrafted() {
624        let r1cs: R1CS<Fr> = get_test_r1cs();
625        let rel_r1cs = r1cs.clone().relax();
626        let z = get_test_z(3);
627
628        let cs = ConstraintSystem::<Fr>::new_ref();
629
630        let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
631        let EVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(rel_r1cs.E)).unwrap();
632        let uVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(rel_r1cs.u)).unwrap();
633        let r1csVar = R1CSVar::<Fr, Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
634
635        RelaxedR1CSGadget::check_native(r1csVar, EVar, uVar, zVar).unwrap();
636        assert!(cs.is_satisfied().unwrap());
637    }
638
639    // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been
640    // initialized.
641    fn test_relaxed_r1cs_gadget<CS: ConstraintSynthesizer<Fr>>(circuit: CS) {
642        let cs = ConstraintSystem::<Fr>::new_ref();
643
644        circuit.generate_constraints(cs.clone()).unwrap();
645        cs.finalize();
646        assert!(cs.is_satisfied().unwrap());
647
648        let cs = cs.into_inner().unwrap();
649
650        let r1cs = extract_r1cs::<Fr>(&cs);
651        let (w, x) = extract_w_x::<Fr>(&cs);
652        let z = [vec![Fr::one()], x, w].concat();
653        r1cs.check_relation(&z).unwrap();
654
655        let relaxed_r1cs = r1cs.clone().relax();
656        relaxed_r1cs.check_relation(&z).unwrap();
657
658        // set new CS for the circuit that checks the RelaxedR1CS of our original circuit
659        let cs = ConstraintSystem::<Fr>::new_ref();
660        // prepare the inputs for our circuit
661        let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
662        let EVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(relaxed_r1cs.E)).unwrap();
663        let uVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
664        let r1csVar = R1CSVar::<Fr, Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
665
666        RelaxedR1CSGadget::check_native(r1csVar, EVar, uVar, zVar).unwrap();
667        assert!(cs.is_satisfied().unwrap());
668    }
669
670    #[test]
671    fn test_relaxed_r1cs_small_gadget_arkworks() {
672        let z_i = vec![Fr::from(3_u32)];
673        let cubic_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
674        let circuit = WrapperCircuit::<Fr, CubicFCircuit<Fr>> {
675            FC: cubic_circuit,
676            z_i: Some(z_i.clone()),
677            z_i1: Some(cubic_circuit.step_native(0, z_i, vec![]).unwrap()),
678        };
679
680        test_relaxed_r1cs_gadget(circuit);
681    }
682
683    struct Sha256TestCircuit<F: PrimeField> {
684        _f: PhantomData<F>,
685        pub x: Vec<u8>,
686        pub y: Vec<u8>,
687    }
688    impl<F: PrimeField> ConstraintSynthesizer<F> for Sha256TestCircuit<F> {
689        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
690            let x = Vec::<UInt8<F>>::new_witness(cs.clone(), || Ok(self.x))?;
691            let y = Vec::<UInt8<F>>::new_input(cs.clone(), || Ok(self.y))?;
692
693            let unitVar = UnitVar::default();
694            let comp_y = <Sha256Gadget<F> as CRHSchemeGadget<Sha256, F>>::evaluate(&unitVar, &x)?;
695            comp_y.0.enforce_equal(&y)?;
696            Ok(())
697        }
698    }
699    #[test]
700    fn test_relaxed_r1cs_medium_gadget_arkworks() {
701        let x = Fr::from(5_u32).into_bigint().to_bytes_le();
702        let y = <Sha256 as CRHScheme>::evaluate(&(), x.clone()).unwrap();
703
704        let circuit = Sha256TestCircuit::<Fr> {
705            _f: PhantomData,
706            x,
707            y,
708        };
709        test_relaxed_r1cs_gadget(circuit);
710    }
711
712    #[test]
713    fn test_relaxed_r1cs_custom_circuit() {
714        let n_constraints = 10_000;
715        let custom_circuit = CustomFCircuit::<Fr>::new(n_constraints).unwrap();
716        let z_i = vec![Fr::from(5_u32)];
717        let circuit = WrapperCircuit::<Fr, CustomFCircuit<Fr>> {
718            FC: custom_circuit,
719            z_i: Some(z_i.clone()),
720            z_i1: Some(custom_circuit.step_native(0, z_i, vec![]).unwrap()),
721        };
722        test_relaxed_r1cs_gadget(circuit);
723    }
724
725    #[test]
726    fn test_relaxed_r1cs_nonnative_circuit() {
727        let cs = ConstraintSystem::<Fq>::new_ref();
728        // in practice we would use CycleFoldCircuit, but is a very big circuit (when computed
729        // non-natively inside the RelaxedR1CS circuit), so in order to have a short test we use a
730        // custom circuit.
731        let custom_circuit = CustomFCircuit::<Fq>::new(10).unwrap();
732        let z_i = vec![Fq::from(5_u32)];
733        let circuit = WrapperCircuit::<Fq, CustomFCircuit<Fq>> {
734            FC: custom_circuit,
735            z_i: Some(z_i.clone()),
736            z_i1: Some(custom_circuit.step_native(0, z_i, vec![]).unwrap()),
737        };
738        circuit.generate_constraints(cs.clone()).unwrap();
739        cs.finalize();
740        let cs = cs.into_inner().unwrap();
741        let r1cs = extract_r1cs::<Fq>(&cs);
742        let (w, x) = extract_w_x::<Fq>(&cs);
743        let z = [vec![Fq::one()], x, w].concat();
744
745        let relaxed_r1cs = r1cs.clone().relax();
746
747        // natively
748        let cs = ConstraintSystem::<Fq>::new_ref();
749        let zVar = Vec::<FpVar<Fq>>::new_witness(cs.clone(), || Ok(z.clone())).unwrap();
750        let EVar =
751            Vec::<FpVar<Fq>>::new_witness(cs.clone(), || Ok(relaxed_r1cs.clone().E)).unwrap();
752        let uVar = FpVar::<Fq>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
753        let r1csVar =
754            R1CSVar::<Fq, Fq, FpVar<Fq>>::new_witness(cs.clone(), || Ok(r1cs.clone())).unwrap();
755        RelaxedR1CSGadget::check_native(r1csVar, EVar, uVar, zVar).unwrap();
756
757        // non-natively
758        let cs = ConstraintSystem::<Fr>::new_ref();
759        let zVar = Vec::new_witness(cs.clone(), || Ok(z)).unwrap();
760        let EVar = Vec::new_witness(cs.clone(), || Ok(relaxed_r1cs.E)).unwrap();
761        let uVar = NonNativeUintVar::<Fr>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
762        let r1csVar =
763            R1CSVar::<Fq, Fr, NonNativeUintVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
764        RelaxedR1CSGadget::check_nonnative(r1csVar, EVar, uVar, zVar).unwrap();
765    }
766
767    #[test]
768    fn test_decider_circuit() {
769        let mut rng = ark_std::test_rng();
770        let poseidon_config = poseidon_canonical_config::<Fr>();
771
772        let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
773        let z_0 = vec![Fr::from(3_u32)];
774
775        // get the CS & CF_CS len
776        let (cs_len, cf_cs_len) =
777            get_cs_params_len::<Projective, GVar, Projective2, GVar2, CubicFCircuit<Fr>>(
778                &poseidon_config,
779                F_circuit,
780            )
781            .unwrap();
782        let (pedersen_params, _) = Pedersen::<Projective>::setup(&mut rng, cs_len).unwrap();
783        let (cf_pedersen_params, _) = Pedersen::<Projective2>::setup(&mut rng, cf_cs_len).unwrap();
784
785        let prover_params =
786            ProverParams::<Projective, Projective2, Pedersen<Projective>, Pedersen<Projective2>> {
787                poseidon_config: poseidon_config.clone(),
788                cs_pp: pedersen_params.clone(),
789                cf_cs_pp: cf_pedersen_params.clone(),
790            };
791
792        type N = Nova<
793            Projective,
794            GVar,
795            Projective2,
796            GVar2,
797            CubicFCircuit<Fr>,
798            Pedersen<Projective>,
799            Pedersen<Projective2>,
800        >;
801
802        // generate a Nova instance and do a step of it
803        let mut nova = N::init(&prover_params, F_circuit, z_0.clone()).unwrap();
804        nova.prove_step(&mut rng, vec![]).unwrap();
805        let ivc_v = nova.clone();
806        let verifier_params = VerifierParams::<
807            Projective,
808            Projective2,
809            Pedersen<Projective>,
810            Pedersen<Projective2>,
811        > {
812            poseidon_config: poseidon_config.clone(),
813            r1cs: ivc_v.clone().r1cs,
814            cf_r1cs: ivc_v.clone().cf_r1cs,
815            cs_vp: pedersen_params,
816            cf_cs_vp: cf_pedersen_params,
817        };
818        let (running_instance, incoming_instance, cyclefold_instance) = ivc_v.instances();
819        N::verify(
820            verifier_params,
821            z_0,
822            ivc_v.z_i,
823            Fr::one(),
824            running_instance,
825            incoming_instance,
826            cyclefold_instance,
827        )
828        .unwrap();
829
830        // load the DeciderEthCircuit from the generated Nova instance
831        let decider_circuit = DeciderEthCircuit::<
832            Projective,
833            GVar,
834            Projective2,
835            GVar2,
836            Pedersen<Projective>,
837            Pedersen<Projective2>,
838        >::from_nova(nova)
839        .unwrap();
840
841        let cs = ConstraintSystem::<Fr>::new_ref();
842
843        // generate the constraints and check that are satisfied by the inputs
844        decider_circuit.generate_constraints(cs.clone()).unwrap();
845        assert!(cs.is_satisfied().unwrap());
846    }
847
848    // checks that the gadget and native implementations of the challenge computation match
849    #[test]
850    fn test_kzg_challenge_gadget() {
851        let mut rng = ark_std::test_rng();
852        let poseidon_config = poseidon_canonical_config::<Fr>();
853
854        let U_i = CommittedInstance::<Projective> {
855            cmE: Projective::rand(&mut rng),
856            u: Fr::rand(&mut rng),
857            cmW: Projective::rand(&mut rng),
858            x: vec![Fr::rand(&mut rng); 1],
859        };
860
861        // compute the challenge natively
862        let (challenge_W, challenge_E) =
863            KZGChallengesGadget::<Projective>::get_challenges_native(&poseidon_config, U_i.clone())
864                .unwrap();
865
866        let cs = ConstraintSystem::<Fr>::new_ref();
867        let U_iVar =
868            CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(U_i.clone()))
869                .unwrap();
870
871        let (challenge_W_Var, challenge_E_Var) =
872            KZGChallengesGadget::<Projective>::get_challenges_gadget(
873                cs.clone(),
874                &poseidon_config,
875                U_iVar,
876            )
877            .unwrap();
878        assert!(cs.is_satisfied().unwrap());
879
880        // check that the natively computed and in-circuit computed hashes match
881        use ark_r1cs_std::R1CSVar;
882        assert_eq!(challenge_W_Var.value().unwrap(), challenge_W);
883        assert_eq!(challenge_E_Var.value().unwrap(), challenge_E);
884    }
885
886    // The test test_polynomial_interpolation is temporary disabled due
887    // https://github.com/privacy-scaling-explorations/sonobe/issues/80
888    // for n<=11 it will work, but for n>11 it will fail with stack overflow.
889    #[ignore]
890    #[test]
891    fn test_polynomial_interpolation() {
892        let mut rng = ark_std::test_rng();
893        let n = 12;
894        let l = 1 << n;
895
896        let v: Vec<Fr> = std::iter::repeat_with(|| Fr::rand(&mut rng))
897            .take(l)
898            .collect();
899        let challenge = Fr::rand(&mut rng);
900
901        use ark_poly::Polynomial;
902        let polynomial = poly_from_vec(v.to_vec()).unwrap();
903        let eval = polynomial.evaluate(&challenge);
904
905        let cs = ConstraintSystem::<Fr>::new_ref();
906        let vVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(v)).unwrap();
907        let challengeVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(challenge)).unwrap();
908
909        let evalVar = evaluate_gadget::<Fr>(vVar, challengeVar).unwrap();
910
911        use ark_r1cs_std::R1CSVar;
912        assert_eq!(evalVar.value().unwrap(), eval);
913        assert!(cs.is_satisfied().unwrap());
914    }
915}