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