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