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