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