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