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_params,
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_params,
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::nova::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 super::*;
601 use ark_crypto_primitives::crh::{
602 sha256::{
603 constraints::{Sha256Gadget, UnitVar},
604 Sha256,
605 },
606 CRHScheme, CRHSchemeGadget,
607 };
608 use ark_pallas::{constraints::GVar, Fq, Fr, Projective};
609 use ark_r1cs_std::bits::uint8::UInt8;
610 use ark_relations::r1cs::ConstraintSystem;
611 use ark_std::{One, UniformRand};
612 use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
613
614 use crate::commitment::pedersen::Pedersen;
615 use crate::folding::nova::{get_cs_params_len, ProverParams, VerifierParams};
616 use crate::frontend::tests::{CubicFCircuit, CustomFCircuit, WrapperCircuit};
617 use crate::transcript::poseidon::poseidon_canonical_config;
618 use crate::FoldingScheme;
619
620 use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z};
621 use crate::ccs::r1cs::{extract_r1cs, extract_w_x};
622
623 #[test]
624 fn test_relaxed_r1cs_small_gadget_handcrafted() {
625 let r1cs: R1CS<Fr> = get_test_r1cs();
626 let rel_r1cs = r1cs.clone().relax();
627 let z = get_test_z(3);
628
629 let cs = ConstraintSystem::<Fr>::new_ref();
630
631 let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
632 let EVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(rel_r1cs.E)).unwrap();
633 let uVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(rel_r1cs.u)).unwrap();
634 let r1csVar = R1CSVar::<Fr, Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
635
636 RelaxedR1CSGadget::check_native(r1csVar, EVar, uVar, zVar).unwrap();
637 assert!(cs.is_satisfied().unwrap());
638 }
639
640 // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been
641 // initialized.
642 fn test_relaxed_r1cs_gadget<CS: ConstraintSynthesizer<Fr>>(circuit: CS) {
643 let cs = ConstraintSystem::<Fr>::new_ref();
644
645 circuit.generate_constraints(cs.clone()).unwrap();
646 cs.finalize();
647 assert!(cs.is_satisfied().unwrap());
648
649 let cs = cs.into_inner().unwrap();
650
651 let r1cs = extract_r1cs::<Fr>(&cs);
652 let (w, x) = extract_w_x::<Fr>(&cs);
653 let z = [vec![Fr::one()], x, w].concat();
654 r1cs.check_relation(&z).unwrap();
655
656 let relaxed_r1cs = r1cs.clone().relax();
657 relaxed_r1cs.check_relation(&z).unwrap();
658
659 // set new CS for the circuit that checks the RelaxedR1CS of our original circuit
660 let cs = ConstraintSystem::<Fr>::new_ref();
661 // prepare the inputs for our circuit
662 let zVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z)).unwrap();
663 let EVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(relaxed_r1cs.E)).unwrap();
664 let uVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
665 let r1csVar = R1CSVar::<Fr, Fr, FpVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
666
667 RelaxedR1CSGadget::check_native(r1csVar, EVar, uVar, zVar).unwrap();
668 assert!(cs.is_satisfied().unwrap());
669 }
670
671 #[test]
672 fn test_relaxed_r1cs_small_gadget_arkworks() {
673 let z_i = vec![Fr::from(3_u32)];
674 let cubic_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
675 let circuit = WrapperCircuit::<Fr, CubicFCircuit<Fr>> {
676 FC: cubic_circuit,
677 z_i: Some(z_i.clone()),
678 z_i1: Some(cubic_circuit.step_native(0, z_i, vec![]).unwrap()),
679 };
680
681 test_relaxed_r1cs_gadget(circuit);
682 }
683
684 struct Sha256TestCircuit<F: PrimeField> {
685 _f: PhantomData<F>,
686 pub x: Vec<u8>,
687 pub y: Vec<u8>,
688 }
689 impl<F: PrimeField> ConstraintSynthesizer<F> for Sha256TestCircuit<F> {
690 fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
691 let x = Vec::<UInt8<F>>::new_witness(cs.clone(), || Ok(self.x))?;
692 let y = Vec::<UInt8<F>>::new_input(cs.clone(), || Ok(self.y))?;
693
694 let unitVar = UnitVar::default();
695 let comp_y = <Sha256Gadget<F> as CRHSchemeGadget<Sha256, F>>::evaluate(&unitVar, &x)?;
696 comp_y.0.enforce_equal(&y)?;
697 Ok(())
698 }
699 }
700 #[test]
701 fn test_relaxed_r1cs_medium_gadget_arkworks() {
702 let x = Fr::from(5_u32).into_bigint().to_bytes_le();
703 let y = <Sha256 as CRHScheme>::evaluate(&(), x.clone()).unwrap();
704
705 let circuit = Sha256TestCircuit::<Fr> {
706 _f: PhantomData,
707 x,
708 y,
709 };
710 test_relaxed_r1cs_gadget(circuit);
711 }
712
713 #[test]
714 fn test_relaxed_r1cs_custom_circuit() {
715 let n_constraints = 10_000;
716 let custom_circuit = CustomFCircuit::<Fr>::new(n_constraints).unwrap();
717 let z_i = vec![Fr::from(5_u32)];
718 let circuit = WrapperCircuit::<Fr, CustomFCircuit<Fr>> {
719 FC: custom_circuit,
720 z_i: Some(z_i.clone()),
721 z_i1: Some(custom_circuit.step_native(0, z_i, vec![]).unwrap()),
722 };
723 test_relaxed_r1cs_gadget(circuit);
724 }
725
726 #[test]
727 fn test_relaxed_r1cs_nonnative_circuit() {
728 let cs = ConstraintSystem::<Fq>::new_ref();
729 // in practice we would use CycleFoldCircuit, but is a very big circuit (when computed
730 // non-natively inside the RelaxedR1CS circuit), so in order to have a short test we use a
731 // custom circuit.
732 let custom_circuit = CustomFCircuit::<Fq>::new(10).unwrap();
733 let z_i = vec![Fq::from(5_u32)];
734 let circuit = WrapperCircuit::<Fq, CustomFCircuit<Fq>> {
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 circuit.generate_constraints(cs.clone()).unwrap();
740 cs.finalize();
741 let cs = cs.into_inner().unwrap();
742 let r1cs = extract_r1cs::<Fq>(&cs);
743 let (w, x) = extract_w_x::<Fq>(&cs);
744 let z = [vec![Fq::one()], x, w].concat();
745
746 let relaxed_r1cs = r1cs.clone().relax();
747
748 // natively
749 let cs = ConstraintSystem::<Fq>::new_ref();
750 let zVar = Vec::<FpVar<Fq>>::new_witness(cs.clone(), || Ok(z.clone())).unwrap();
751 let EVar =
752 Vec::<FpVar<Fq>>::new_witness(cs.clone(), || Ok(relaxed_r1cs.clone().E)).unwrap();
753 let uVar = FpVar::<Fq>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
754 let r1csVar =
755 R1CSVar::<Fq, Fq, FpVar<Fq>>::new_witness(cs.clone(), || Ok(r1cs.clone())).unwrap();
756 RelaxedR1CSGadget::check_native(r1csVar, EVar, uVar, zVar).unwrap();
757
758 // non-natively
759 let cs = ConstraintSystem::<Fr>::new_ref();
760 let zVar = Vec::new_witness(cs.clone(), || Ok(z)).unwrap();
761 let EVar = Vec::new_witness(cs.clone(), || Ok(relaxed_r1cs.E)).unwrap();
762 let uVar = NonNativeUintVar::<Fr>::new_witness(cs.clone(), || Ok(relaxed_r1cs.u)).unwrap();
763 let r1csVar =
764 R1CSVar::<Fq, Fr, NonNativeUintVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs)).unwrap();
765 RelaxedR1CSGadget::check_nonnative(r1csVar, EVar, uVar, zVar).unwrap();
766 }
767
768 #[test]
769 fn test_decider_circuit() {
770 let mut rng = ark_std::test_rng();
771 let poseidon_config = poseidon_canonical_config::<Fr>();
772
773 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
774 let z_0 = vec![Fr::from(3_u32)];
775
776 // get the CS & CF_CS len
777 let (cs_len, cf_cs_len) =
778 get_cs_params_len::<Projective, GVar, Projective2, GVar2, CubicFCircuit<Fr>>(
779 &poseidon_config,
780 F_circuit,
781 )
782 .unwrap();
783 let (pedersen_params, _) = Pedersen::<Projective>::setup(&mut rng, cs_len).unwrap();
784 let (cf_pedersen_params, _) = Pedersen::<Projective2>::setup(&mut rng, cf_cs_len).unwrap();
785
786 let prover_params =
787 ProverParams::<Projective, Projective2, Pedersen<Projective>, Pedersen<Projective2>> {
788 poseidon_config: poseidon_config.clone(),
789 cs_params: pedersen_params,
790 cf_cs_params: cf_pedersen_params,
791 };
792
793 type NOVA = Nova<
794 Projective,
795 GVar,
796 Projective2,
797 GVar2,
798 CubicFCircuit<Fr>,
799 Pedersen<Projective>,
800 Pedersen<Projective2>,
801 >;
802
803 // generate a Nova instance and do a step of it
804 let mut nova = NOVA::init(&prover_params, F_circuit, z_0.clone()).unwrap();
805 nova.prove_step(vec![]).unwrap();
806 let ivc_v = nova.clone();
807 let verifier_params = VerifierParams::<Projective, Projective2> {
808 poseidon_config: poseidon_config.clone(),
809 r1cs: ivc_v.clone().r1cs,
810 cf_r1cs: ivc_v.clone().cf_r1cs,
811 };
812 let (running_instance, incoming_instance, cyclefold_instance) = ivc_v.instances();
813 NOVA::verify(
814 verifier_params,
815 z_0,
816 ivc_v.z_i,
817 Fr::one(),
818 running_instance,
819 incoming_instance,
820 cyclefold_instance,
821 )
822 .unwrap();
823
824 // load the DeciderEthCircuit from the generated Nova instance
825 let decider_circuit = DeciderEthCircuit::<
826 Projective,
827 GVar,
828 Projective2,
829 GVar2,
830 Pedersen<Projective>,
831 Pedersen<Projective2>,
832 >::from_nova(nova)
833 .unwrap();
834
835 let cs = ConstraintSystem::<Fr>::new_ref();
836
837 // generate the constraints and check that are satisfied by the inputs
838 decider_circuit.generate_constraints(cs.clone()).unwrap();
839 assert!(cs.is_satisfied().unwrap());
840 }
841
842 // checks that the gadget and native implementations of the challenge computation match
843 #[test]
844 fn test_kzg_challenge_gadget() {
845 let mut rng = ark_std::test_rng();
846 let poseidon_config = poseidon_canonical_config::<Fr>();
847
848 let U_i = CommittedInstance::<Projective> {
849 cmE: Projective::rand(&mut rng),
850 u: Fr::rand(&mut rng),
851 cmW: Projective::rand(&mut rng),
852 x: vec![Fr::rand(&mut rng); 1],
853 };
854
855 // compute the challenge natively
856 let (challenge_W, challenge_E) =
857 KZGChallengesGadget::<Projective>::get_challenges_native(&poseidon_config, U_i.clone())
858 .unwrap();
859
860 let cs = ConstraintSystem::<Fr>::new_ref();
861 let U_iVar =
862 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(U_i.clone()))
863 .unwrap();
864
865 let (challenge_W_Var, challenge_E_Var) =
866 KZGChallengesGadget::<Projective>::get_challenges_gadget(
867 cs.clone(),
868 &poseidon_config,
869 U_iVar,
870 )
871 .unwrap();
872 assert!(cs.is_satisfied().unwrap());
873
874 // check that the natively computed and in-circuit computed hashes match
875 use ark_r1cs_std::R1CSVar;
876 assert_eq!(challenge_W_Var.value().unwrap(), challenge_W);
877 assert_eq!(challenge_E_Var.value().unwrap(), challenge_E);
878 }
879
880 // The test test_polynomial_interpolation is temporary disabled due
881 // https://github.com/privacy-scaling-explorations/sonobe/issues/80
882 // for n<=11 it will work, but for n>11 it will fail with stack overflow.
883 #[ignore]
884 #[test]
885 fn test_polynomial_interpolation() {
886 let mut rng = ark_std::test_rng();
887 let n = 12;
888 let l = 1 << n;
889
890 let v: Vec<Fr> = std::iter::repeat_with(|| Fr::rand(&mut rng))
891 .take(l)
892 .collect();
893 let challenge = Fr::rand(&mut rng);
894
895 use ark_poly::Polynomial;
896 let polynomial = poly_from_vec(v.to_vec()).unwrap();
897 let eval = polynomial.evaluate(&challenge);
898
899 let cs = ConstraintSystem::<Fr>::new_ref();
900 let vVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(v)).unwrap();
901 let challengeVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(challenge)).unwrap();
902
903 let evalVar = evaluate_gadget::<Fr>(vVar, challengeVar).unwrap();
904
905 use ark_r1cs_std::R1CSVar;
906 assert_eq!(evalVar.value().unwrap(), eval);
907 assert!(cs.is_satisfied().unwrap());
908 }
909}