arnaucube
arnaucube/sonobePublic Self-hosted repository
sonobe/folding-schemes/src/folding/hypernova/decider_eth_circuit.rs
folding-schemes/src/folding/hypernova/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::PrimeField;
 10use ark_poly::Polynomial;
 11use ark_r1cs_std::{
 12    alloc::{AllocVar, AllocationMode},
 13    boolean::Boolean,
 14    eq::EqGadget,
 15    fields::fp::FpVar,
 16    groups::GroupOpsBounds,
 17    prelude::CurveVar,
 18    ToConstraintFieldGadget,
 19};
 20use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
 21use ark_std::Zero;
 22use core::{borrow::Borrow, marker::PhantomData};
 23
 24use super::{
 25    circuits::{CCCSVar, LCCCSVar, NIMFSGadget, ProofVar as NIMFSProofVar},
 26    nimfs::{NIMFSProof, NIMFS},
 27    HyperNova, Witness, CCCS, LCCCS,
 28};
 29use crate::arith::ccs::CCS;
 30use crate::arith::r1cs::R1CS;
 31use crate::commitment::{pedersen::Params as PedersenParams, CommitmentScheme};
 32use crate::folding::circuits::{
 33    cyclefold::{CycleFoldCommittedInstance, CycleFoldWitness},
 34    CF1, CF2,
 35};
 36use crate::frontend::FCircuit;
 37use crate::transcript::{Transcript, TranscriptVar};
 38use crate::utils::{
 39    gadgets::{eval_mle, MatrixGadget, SparseMatrixVar},
 40    vec::poly_from_vec,
 41};
 42use crate::Error;
 43
 44/// In-circuit representation of the Witness associated to the CommittedInstance.
 45#[derive(Debug, Clone)]
 46pub struct WitnessVar<F: PrimeField> {
 47    pub w: Vec<FpVar<F>>,
 48    pub r_w: FpVar<F>,
 49}
 50
 51impl<F: PrimeField> AllocVar<Witness<F>, F> for WitnessVar<F> {
 52    fn new_variable<T: Borrow<Witness<F>>>(
 53        cs: impl Into<Namespace<F>>,
 54        f: impl FnOnce() -> Result<T, SynthesisError>,
 55        mode: AllocationMode,
 56    ) -> Result<Self, SynthesisError> {
 57        f().and_then(|val| {
 58            let cs = cs.into();
 59
 60            let w: Vec<FpVar<F>> =
 61                Vec::new_variable(cs.clone(), || Ok(val.borrow().w.clone()), mode)?;
 62            let r_w = FpVar::<F>::new_variable(cs.clone(), || Ok(val.borrow().r_w), mode)?;
 63
 64            Ok(Self { w, r_w })
 65        })
 66    }
 67}
 68
 69/// CCSMatricesVar contains the matrices 'M' of the CCS without the rest of CCS parameters.
 70#[derive(Debug, Clone)]
 71pub struct CCSMatricesVar<F: PrimeField> {
 72    // we only need native representation, so the constraint field==F
 73    pub M: Vec<SparseMatrixVar<F, F, FpVar<F>>>,
 74}
 75
 76impl<F> AllocVar<CCS<F>, F> for CCSMatricesVar<F>
 77where
 78    F: PrimeField,
 79{
 80    fn new_variable<T: Borrow<CCS<F>>>(
 81        cs: impl Into<Namespace<F>>,
 82        f: impl FnOnce() -> Result<T, SynthesisError>,
 83        _mode: AllocationMode,
 84    ) -> Result<Self, SynthesisError> {
 85        f().and_then(|val| {
 86            let cs = cs.into();
 87
 88            let M: Vec<SparseMatrixVar<F, F, FpVar<F>>> = val
 89                .borrow()
 90                .M
 91                .iter()
 92                .map(|M| SparseMatrixVar::<F, F, FpVar<F>>::new_constant(cs.clone(), M.clone()))
 93                .collect::<Result<_, SynthesisError>>()?;
 94
 95            Ok(Self { M })
 96        })
 97    }
 98}
 99
100/// Gadget to check the LCCCS relation both over the native constraint field and over the
101/// non-native constraint field.
102#[derive(Debug, Clone)]
103pub struct LCCCSCheckerGadget {}
104impl LCCCSCheckerGadget {
105    /// performs in-circuit the RelaxedR1CS check for native variables (Az∘Bz==uCz+E)
106    pub fn check<F: PrimeField>(
107        s: usize,
108        ccs_mat: CCSMatricesVar<F>,
109        z: Vec<FpVar<F>>,
110        // LCCCS values
111        r_x: Vec<FpVar<F>>,
112        v: Vec<FpVar<F>>,
113    ) -> Result<(), SynthesisError> {
114        let computed_v: Vec<FpVar<F>> = ccs_mat
115            .M
116            .iter()
117            .map(|M_j| {
118                let Mz = M_j.mul_vector(&z)?;
119                Ok(eval_mle(s, Mz, r_x.clone()))
120            })
121            .collect::<Result<Vec<FpVar<F>>, SynthesisError>>()?;
122
123        (computed_v).enforce_equal(&v)?;
124        Ok(())
125    }
126}
127
128/// Circuit that implements the in-circuit checks needed for the HyperNova's onchain (Ethereum's
129/// EVM) verification.
130#[derive(Clone, Debug)]
131pub struct DeciderEthCircuit<C1, GC1, C2, GC2, CS1, CS2, const H: bool = false>
132where
133    C1: CurveGroup,
134    GC1: CurveVar<C1, CF2<C1>>,
135    C2: CurveGroup,
136    GC2: CurveVar<C2, CF2<C2>>,
137    CS1: CommitmentScheme<C1, H>,
138    CS2: CommitmentScheme<C2, H>,
139{
140    _c1: PhantomData<C1>,
141    _gc1: PhantomData<GC1>,
142    _c2: PhantomData<C2>,
143    _gc2: PhantomData<GC2>,
144    _cs1: PhantomData<CS1>,
145    _cs2: PhantomData<CS2>,
146
147    /// E vector's length of the CycleFold instance witness
148    pub cf_E_len: usize,
149    /// CCS of the Augmented Function circuit
150    pub ccs: CCS<C1::ScalarField>,
151    /// R1CS of the CycleFold circuit
152    pub cf_r1cs: R1CS<C2::ScalarField>,
153    /// CycleFold PedersenParams over C2
154    pub cf_pedersen_params: PedersenParams<C2>,
155    pub poseidon_config: PoseidonConfig<CF1<C1>>,
156    /// public params hash
157    pub pp_hash: Option<C1::ScalarField>,
158    pub i: Option<CF1<C1>>,
159    /// initial state
160    pub z_0: Option<Vec<C1::ScalarField>>,
161    /// current i-th state
162    pub z_i: Option<Vec<C1::ScalarField>>,
163    /// Nova instances
164    pub U_i: Option<LCCCS<C1>>,
165    pub W_i: Option<Witness<C1::ScalarField>>,
166    pub u_i: Option<CCCS<C1>>,
167    pub w_i: Option<Witness<C1::ScalarField>>,
168    pub U_i1: Option<LCCCS<C1>>,
169    pub W_i1: Option<Witness<C1::ScalarField>>,
170    pub nimfs_proof: Option<NIMFSProof<C1>>,
171    // rho_0 is the first and only rho in the 'rho_powers' array, since it comes from NIMFS-folding
172    // only 2 instances.
173    pub rho_0: Option<C1::ScalarField>,
174    /// CycleFold running instance
175    pub cf_U_i: Option<CycleFoldCommittedInstance<C2>>,
176    pub cf_W_i: Option<CycleFoldWitness<C2>>,
177
178    /// KZG challenge & eval
179    pub kzg_challenge: Option<C1::ScalarField>,
180    pub eval_W: Option<C1::ScalarField>,
181}
182
183impl<C1, GC1, C2, GC2, CS1, CS2, const H: bool> DeciderEthCircuit<C1, GC1, C2, GC2, CS1, CS2, H>
184where
185    C1: CurveGroup,
186    C2: CurveGroup,
187    GC1: CurveVar<C1, CF2<C1>> + ToConstraintFieldGadget<CF2<C1>>,
188    GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
189    CS1: CommitmentScheme<C1, H>,
190    // enforce that the CS2 is Pedersen commitment scheme, since we're at Ethereum's EVM decider
191    CS2: CommitmentScheme<C2, H, ProverParams = PedersenParams<C2>>,
192    <C1 as Group>::ScalarField: Absorb,
193    <C1 as CurveGroup>::BaseField: PrimeField,
194{
195    /// returns an instance of the DeciderEthCircuit from the given HyperNova struct
196    pub fn from_hypernova<FC: FCircuit<C1::ScalarField>, const MU: usize, const NU: usize>(
197        hn: HyperNova<C1, GC1, C2, GC2, FC, CS1, CS2, MU, NU, H>,
198    ) -> Result<Self, Error> {
199        // compute the U_{i+1}, W_{i+1}, by folding the last running & incoming instances
200        let mut transcript = PoseidonSponge::<C1::ScalarField>::new(&hn.poseidon_config);
201        transcript.absorb(&hn.pp_hash);
202        let (nimfs_proof, U_i1, W_i1, rho_powers) =
203            NIMFS::<C1, PoseidonSponge<C1::ScalarField>>::prove(
204                &mut transcript,
205                &hn.ccs,
206                &[hn.U_i.clone()],
207                &[hn.u_i.clone()],
208                &[hn.W_i.clone()],
209                &[hn.w_i.clone()],
210            )?;
211
212        // compute the KZG challenges used as inputs in the circuit
213        let kzg_challenge =
214            KZGChallengeGadget::<C1>::get_challenge_native(&mut transcript, U_i1.clone())?;
215
216        // get KZG evals
217        let mut W = W_i1.w.clone();
218        W.extend(
219            std::iter::repeat(C1::ScalarField::zero())
220                .take(W_i1.w.len().next_power_of_two() - W_i1.w.len()),
221        );
222        let p_W = poly_from_vec(W.to_vec())?;
223        let eval_W = p_W.evaluate(&kzg_challenge);
224
225        // ensure that we only have 1 element in rho_powers, since we only NIMFS-fold 2 instances
226        if rho_powers.len() != 1 {
227            return Err(Error::NotExpectedLength(rho_powers.len(), 1));
228        }
229
230        Ok(Self {
231            _c1: PhantomData,
232            _gc1: PhantomData,
233            _c2: PhantomData,
234            _gc2: PhantomData,
235            _cs1: PhantomData,
236            _cs2: PhantomData,
237
238            cf_E_len: hn.cf_W_i.E.len(),
239            ccs: hn.ccs,
240            cf_r1cs: hn.cf_r1cs,
241            cf_pedersen_params: hn.cf_cs_params,
242            poseidon_config: hn.poseidon_config,
243            pp_hash: Some(hn.pp_hash),
244            i: Some(hn.i),
245            z_0: Some(hn.z_0),
246            z_i: Some(hn.z_i),
247            U_i: Some(hn.U_i),
248            W_i: Some(hn.W_i),
249            u_i: Some(hn.u_i),
250            w_i: Some(hn.w_i),
251            U_i1: Some(U_i1),
252            W_i1: Some(W_i1),
253            nimfs_proof: Some(nimfs_proof),
254            rho_0: Some(rho_powers[0]),
255            cf_U_i: Some(hn.cf_U_i),
256            cf_W_i: Some(hn.cf_W_i),
257            kzg_challenge: Some(kzg_challenge),
258            eval_W: Some(eval_W),
259        })
260    }
261}
262
263impl<C1, GC1, C2, GC2, CS1, CS2> ConstraintSynthesizer<CF1<C1>>
264    for DeciderEthCircuit<C1, GC1, C2, GC2, CS1, CS2>
265where
266    C1: CurveGroup,
267    C2: CurveGroup,
268    GC1: CurveVar<C1, CF2<C1>>,
269    GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
270    CS1: CommitmentScheme<C1>,
271    CS2: CommitmentScheme<C2>,
272    C1::ScalarField: PrimeField,
273    <C1 as CurveGroup>::BaseField: PrimeField,
274    <C2 as CurveGroup>::BaseField: PrimeField,
275    <C1 as Group>::ScalarField: Absorb,
276    <C2 as Group>::ScalarField: Absorb,
277    C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
278    for<'b> &'b GC2: GroupOpsBounds<'b, C2, GC2>,
279{
280    fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
281        let ccs_matrices =
282            CCSMatricesVar::<C1::ScalarField>::new_witness(cs.clone(), || Ok(self.ccs.clone()))?;
283
284        let pp_hash = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
285            Ok(self.pp_hash.unwrap_or_else(CF1::<C1>::zero))
286        })?;
287        let i =
288            FpVar::<CF1<C1>>::new_input(cs.clone(), || Ok(self.i.unwrap_or_else(CF1::<C1>::zero)))?;
289        let z_0 = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
290            Ok(self.z_0.unwrap_or(vec![CF1::<C1>::zero()]))
291        })?;
292        let z_i = Vec::<FpVar<CF1<C1>>>::new_input(cs.clone(), || {
293            Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
294        })?;
295
296        let U_dummy_native = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
297        let u_dummy_native = CCCS::<C1>::dummy(self.ccs.l);
298        let w_dummy_native = Witness::<C1::ScalarField>::new(
299            vec![C1::ScalarField::zero(); self.ccs.n - 3 /* (3=2+1, since u_i.x.len=2) */],
300        );
301
302        let U_i = LCCCSVar::<C1>::new_witness(cs.clone(), || {
303            Ok(self.U_i.unwrap_or(U_dummy_native.clone()))
304        })?;
305        let u_i = CCCSVar::<C1>::new_witness(cs.clone(), || {
306            Ok(self.u_i.unwrap_or(u_dummy_native.clone()))
307        })?;
308        // here (U_i1, W_i1) = NIFS.P( (U_i,W_i), (u_i,w_i))
309        let U_i1 = LCCCSVar::<C1>::new_input(cs.clone(), || {
310            Ok(self.U_i1.unwrap_or(U_dummy_native.clone()))
311        })?;
312        let W_i1 = WitnessVar::<C1::ScalarField>::new_witness(cs.clone(), || {
313            Ok(self.W_i1.unwrap_or(w_dummy_native.clone()))
314        })?;
315        let nimfs_proof_dummy = NIMFSProof::<C1>::dummy(&self.ccs, 1, 1); // mu=1 & nu=1 because the last fold is 2-to-1
316        let nimfs_proof = NIMFSProofVar::<C1>::new_witness(cs.clone(), || {
317            Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy))
318        })?;
319
320        // allocate the inputs for the check 6
321        let kzg_challenge = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
322            Ok(self.kzg_challenge.unwrap_or_else(CF1::<C1>::zero))
323        })?;
324        let _eval_W = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
325            Ok(self.eval_W.unwrap_or_else(CF1::<C1>::zero))
326        })?;
327
328        // `sponge` is for digest computation.
329        let sponge = PoseidonSpongeVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
330        // `transcript` is for challenge generation.
331        let mut transcript = sponge.clone();
332        transcript.absorb(&pp_hash)?;
333
334        // NOTE: we use the same enumeration as in Nova's DeciderEthCircuit described at
335        // https://privacy-scaling-explorations.github.io/sonobe-docs/design/nova-decider-onchain.html
336        // in order to make it easier to reason about.
337
338        // 1. check LCCCS relation of U_{i+1}
339        let z_U1: Vec<FpVar<CF1<C1>>> =
340            [vec![U_i1.u.clone()], U_i1.x.to_vec(), W_i1.w.to_vec()].concat();
341        LCCCSCheckerGadget::check(
342            self.ccs.s,
343            ccs_matrices,
344            z_U1,
345            U_i1.r_x.clone(),
346            U_i1.v.clone(),
347        )?;
348
349        // 3.a u_i.x[0] == H(i, z_0, z_i, U_i)
350        let (u_i_x, _) = U_i.clone().hash(
351            &sponge,
352            pp_hash.clone(),
353            i.clone(),
354            z_0.clone(),
355            z_i.clone(),
356        )?;
357        (u_i.x[0]).enforce_equal(&u_i_x)?;
358
359        #[cfg(feature = "light-test")]
360        log::warn!("[WARNING]: Running with the 'light-test' feature, skipping the big part of the DeciderEthCircuit.\n           Only for testing purposes.");
361
362        // The following two checks (and their respective allocations) are disabled for normal
363        // tests since they take several millions of constraints and would take several minutes
364        // (and RAM) to run the test. It is active by default, and not active only when
365        // 'light-test' feature is used.
366        #[cfg(not(feature = "light-test"))]
367        {
368            // imports here instead of at the top of the file, so we avoid having multiple
369            // `#[cfg(not(test))]`
370            use crate::commitment::pedersen::PedersenGadget;
371            use crate::folding::circuits::nonnative::uint::NonNativeUintVar;
372            use crate::folding::nova::decider_eth_circuit::{R1CSVar, RelaxedR1CSGadget};
373            use crate::folding::{
374                circuits::cyclefold::{
375                    CycleFoldCommittedInstanceVar, CycleFoldConfig, CycleFoldWitnessVar,
376                },
377                nova::NovaCycleFoldConfig,
378            };
379            use ark_r1cs_std::ToBitsGadget;
380
381            let cf_u_dummy_native =
382                CycleFoldCommittedInstance::<C2>::dummy(NovaCycleFoldConfig::<C1>::IO_LEN);
383            let cf_w_dummy_native = CycleFoldWitness::<C2>::dummy(
384                self.cf_r1cs.A.n_cols - 1 - self.cf_r1cs.l,
385                self.cf_E_len,
386            );
387            let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
388                Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
389            })?;
390            let cf_W_i = CycleFoldWitnessVar::<C2>::new_witness(cs.clone(), || {
391                Ok(self.cf_W_i.unwrap_or(cf_w_dummy_native.clone()))
392            })?;
393
394            // 3.b u_i.x[1] == H(cf_U_i)
395            let (cf_u_i_x, _) = cf_U_i.clone().hash(&sponge, pp_hash.clone())?;
396            (u_i.x[1]).enforce_equal(&cf_u_i_x)?;
397
398            // 4. check Pedersen commitments of cf_U_i.{cmE, cmW}
399            let H = GC2::new_constant(cs.clone(), self.cf_pedersen_params.h)?;
400            let G = Vec::<GC2>::new_constant(cs.clone(), self.cf_pedersen_params.generators)?;
401            let cf_W_i_E_bits: Result<Vec<Vec<Boolean<CF1<C1>>>>, SynthesisError> =
402                cf_W_i.E.iter().map(|E_i| E_i.to_bits_le()).collect();
403            let cf_W_i_W_bits: Result<Vec<Vec<Boolean<CF1<C1>>>>, SynthesisError> =
404                cf_W_i.W.iter().map(|W_i| W_i.to_bits_le()).collect();
405
406            let computed_cmE = PedersenGadget::<C2, GC2>::commit(
407                H.clone(),
408                G.clone(),
409                cf_W_i_E_bits?,
410                cf_W_i.rE.to_bits_le()?,
411            )?;
412            cf_U_i.cmE.enforce_equal(&computed_cmE)?;
413            let computed_cmW =
414                PedersenGadget::<C2, GC2>::commit(H, G, cf_W_i_W_bits?, cf_W_i.rW.to_bits_le()?)?;
415            cf_U_i.cmW.enforce_equal(&computed_cmW)?;
416
417            let cf_r1cs =
418                R1CSVar::<C1::BaseField, CF1<C1>, NonNativeUintVar<CF1<C1>>>::new_witness(
419                    cs.clone(),
420                    || Ok(self.cf_r1cs.clone()),
421                )?;
422
423            // 5. check RelaxedR1CS of cf_U_i
424            let cf_z_U = [vec![cf_U_i.u.clone()], cf_U_i.x.to_vec(), cf_W_i.W.to_vec()].concat();
425            RelaxedR1CSGadget::check_nonnative(cf_r1cs, cf_W_i.E, cf_U_i.u.clone(), cf_z_U)?;
426        }
427
428        // The following steps are in non-increasing order because the `computed_U_i1` is computed
429        // at step 8, and later used at step 6. Notice that in Nova, we compute U_i1 outside of the
430        // circuit, in the smart contract, but here we're computing it in-circuit, and we reuse the
431        // `rho_vec` computed along the way of computing `computed_U_i1` for the later `rho_powers`
432        // check (6.b).
433
434        // Check 7 is temporary disabled due
435        // https://github.com/privacy-scaling-explorations/sonobe/issues/80
436        log::warn!("[WARNING]: issue #80 (https://github.com/privacy-scaling-explorations/sonobe/issues/80) is not resolved yet.");
437        //
438        // 7. check eval_W==p_W(c_W)
439        // let incircuit_eval_W = evaluate_gadget::<CF1<C1>>(W_i1.W, incircuit_c_W)?;
440        // incircuit_eval_W.enforce_equal(&eval_W)?;
441
442        // 8.a verify the NIMFS.V of the final fold, and check that the obtained rho_powers from the
443        // transcript match the one from the public input (so we avoid the onchain logic of the
444        // verifier computing it).
445        // Notice that the NIMFSGadget performs all the logic except of checking the fold of the
446        // instances C parameter, which would require non-native arithmetic, henceforth we perform
447        // that check outside the circuit.
448        let (computed_U_i1, rho_vec) = NIMFSGadget::<C1>::verify(
449            cs.clone(),
450            &self.ccs.clone(),
451            &mut transcript,
452            &[U_i],
453            &[u_i],
454            nimfs_proof,
455            Boolean::TRUE, // enabled
456        )?;
457
458        // 6.a check KZG challenges
459        // Notice that this step is done after the NIMFS.V, to follow the transcript absorbs order
460        // done outside the circuit, where to compute the challenge it needs first to compute the
461        // U_{i+1} through the NIMFS.V
462        let incircuit_challenge =
463            KZGChallengeGadget::<C1>::get_challenge_gadget(&mut transcript, U_i1.clone())?;
464        incircuit_challenge.enforce_equal(&kzg_challenge)?;
465
466        // 6.b check that the obtained U_{i+1} from the NIMFS.V matches the U_{i+1} from the input,
467        // except for the C parameter, which to compute its folding would require non-native logic
468        // in-circuit, and we defer it to outside the circuit.
469        computed_U_i1.u.enforce_equal(&U_i1.u)?;
470        computed_U_i1.r_x.enforce_equal(&U_i1.r_x)?;
471        computed_U_i1.v.enforce_equal(&U_i1.v)?;
472
473        // 8.b check that the in-circuit computed r is equal to the inputted r.
474        // Notice that rho_vec only contains one element, since at the final fold we are only
475        // folding 2-to-1 instances.
476
477        // Ensure that rho_vec is of length 1, note that this is not enforced at the constraint
478        // level but more as a check for the prover.
479        if rho_vec.len() != 1 {
480            return Err(SynthesisError::Unsatisfiable);
481        }
482
483        let rho_0 = Boolean::le_bits_to_fp_var(&rho_vec[0])?;
484        let external_rho_0 = FpVar::<CF1<C1>>::new_input(cs.clone(), || {
485            Ok(self.rho_0.unwrap_or(CF1::<C1>::zero()))
486        })?;
487        rho_0.enforce_equal(&external_rho_0)?;
488
489        Ok(())
490    }
491}
492
493/// Gadget that computes the KZG challenges, also offers the rust native implementation compatible
494/// with the gadget.
495pub struct KZGChallengeGadget<C: CurveGroup> {
496    _c: PhantomData<C>,
497}
498#[allow(clippy::type_complexity)]
499impl<C> KZGChallengeGadget<C>
500where
501    C: CurveGroup,
502    C::ScalarField: PrimeField,
503    <C as CurveGroup>::BaseField: PrimeField,
504    C::ScalarField: Absorb,
505{
506    pub fn get_challenge_native<T: Transcript<C::ScalarField>>(
507        transcript: &mut T,
508        U_i: LCCCS<C>,
509    ) -> Result<C::ScalarField, Error> {
510        // compute the KZG challenges, which are computed in-circuit and checked that it matches
511        // the inputted one
512        transcript.absorb_nonnative(&U_i.C);
513        Ok(transcript.get_challenge())
514    }
515    // compatible with the native get_challenge_native
516    pub fn get_challenge_gadget<S: CryptographicSponge, T: TranscriptVar<CF1<C>, S>>(
517        transcript: &mut T,
518        U_i: LCCCSVar<C>,
519    ) -> Result<FpVar<C::ScalarField>, SynthesisError> {
520        transcript.absorb(&U_i.C.to_constraint_field()?)?;
521        transcript.get_challenge()
522    }
523}
524
525#[cfg(test)]
526pub mod tests {
527    use ark_bn254::{constraints::GVar, Fr, G1Projective as Projective};
528    use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
529    use ark_relations::r1cs::ConstraintSystem;
530    use ark_std::One;
531    use ark_std::{test_rng, UniformRand};
532
533    use super::*;
534    use crate::commitment::pedersen::Pedersen;
535    use crate::folding::nova::PreprocessorParam;
536    use crate::frontend::tests::CubicFCircuit;
537    use crate::transcript::poseidon::poseidon_canonical_config;
538    use crate::FoldingScheme;
539
540    #[test]
541    fn test_lcccs_checker_gadget() {
542        let mut rng = test_rng();
543        let n_rows = 2_u32.pow(5) as usize;
544        let n_cols = 2_u32.pow(5) as usize;
545        let r1cs = R1CS::<Fr>::rand(&mut rng, n_rows, n_cols);
546        let ccs = CCS::from_r1cs(r1cs);
547        let z: Vec<Fr> = (0..n_cols).map(|_| Fr::rand(&mut rng)).collect();
548
549        let (pedersen_params, _) =
550            Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
551
552        let (lcccs, _) = ccs
553            .to_lcccs::<_, Projective, Pedersen<Projective>, false>(&mut rng, &pedersen_params, &z)
554            .unwrap();
555
556        let cs = ConstraintSystem::<Fr>::new_ref();
557
558        // CCS's (sparse) matrices are constants in the circuit
559        let ccs_mat = CCSMatricesVar::<Fr>::new_constant(cs.clone(), ccs.clone()).unwrap();
560        let zVar = Vec::<FpVar<Fr>>::new_input(cs.clone(), || Ok(z)).unwrap();
561        let r_xVar = Vec::<FpVar<Fr>>::new_input(cs.clone(), || Ok(lcccs.r_x)).unwrap();
562        let vVar = Vec::<FpVar<Fr>>::new_input(cs.clone(), || Ok(lcccs.v)).unwrap();
563
564        LCCCSCheckerGadget::check(ccs.s, ccs_mat, zVar, r_xVar, vVar).unwrap();
565
566        assert!(cs.is_satisfied().unwrap());
567    }
568
569    #[test]
570    fn test_decider_circuit() {
571        let mut rng = ark_std::test_rng();
572        let poseidon_config = poseidon_canonical_config::<Fr>();
573
574        let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
575        let z_0 = vec![Fr::from(3_u32)];
576
577        const MU: usize = 1;
578        const NU: usize = 1;
579
580        type HN = HyperNova<
581            Projective,
582            GVar,
583            Projective2,
584            GVar2,
585            CubicFCircuit<Fr>,
586            Pedersen<Projective>,
587            Pedersen<Projective2>,
588            MU,
589            NU,
590            false,
591        >;
592        let prep_param = PreprocessorParam::<
593            Projective,
594            Projective2,
595            CubicFCircuit<Fr>,
596            Pedersen<Projective>,
597            Pedersen<Projective2>,
598            false,
599        >::new(poseidon_config, F_circuit);
600        let hn_params = HN::preprocess(&mut rng, &prep_param).unwrap();
601
602        // generate a Nova instance and do a step of it
603        let mut hypernova = HN::init(&hn_params, F_circuit, z_0.clone()).unwrap();
604        hypernova
605            .prove_step(&mut rng, vec![], Some((vec![], vec![])))
606            .unwrap();
607
608        let ivc_v = hypernova.clone();
609        let (running_instance, incoming_instance, cyclefold_instance) = ivc_v.instances();
610        HN::verify(
611            hn_params.1, // HN's verifier_params
612            z_0,
613            ivc_v.z_i,
614            Fr::one(),
615            running_instance,
616            incoming_instance,
617            cyclefold_instance,
618        )
619        .unwrap();
620
621        // load the DeciderEthCircuit from the generated Nova instance
622        let decider_circuit = DeciderEthCircuit::<
623            Projective,
624            GVar,
625            Projective2,
626            GVar2,
627            Pedersen<Projective>,
628            Pedersen<Projective2>,
629        >::from_hypernova(hypernova)
630        .unwrap();
631
632        let cs = ConstraintSystem::<Fr>::new_ref();
633
634        // generate the constraints and check that are satisfied by the inputs
635        decider_circuit.generate_constraints(cs.clone()).unwrap();
636        assert!(cs.is_satisfied().unwrap());
637        dbg!(cs.num_constraints());
638    }
639}