sonobe/src/folding/nova/circuits.rs
src/folding/nova/circuits.rsRaw
1use ark_crypto_primitives::crh::{
2 poseidon::constraints::{CRHGadget, CRHParametersVar},
3 poseidon::CRH,
4 CRHScheme, CRHSchemeGadget,
5};
6use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
7use ark_ec::{AffineRepr, CurveGroup, Group};
8use ark_ff::{Field, PrimeField};
9use ark_r1cs_std::{
10 alloc::{AllocVar, AllocationMode},
11 boolean::Boolean,
12 eq::EqGadget,
13 fields::{fp::FpVar, FieldVar},
14 groups::GroupOpsBounds,
15 prelude::CurveVar,
16};
17use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
18use ark_std::fmt::Debug;
19use ark_std::Zero;
20use core::{borrow::Borrow, marker::PhantomData};
21
22use super::CommittedInstance;
23use crate::folding::circuits::{
24 cyclefold::ECRLC,
25 nonnative::{point_to_nonnative_limbs, NonNativeAffineVar},
26};
27
28/// CF1 represents the ConstraintField used for the main Nova circuit which is over E1::Fr, where
29/// E1 is the main curve where we do the folding.
30pub type CF1<C> = <<C as CurveGroup>::Affine as AffineRepr>::ScalarField;
31/// CF2 represents the ConstraintField used for the CycleFold circuit which is over E2::Fr=E1::Fq,
32/// where E2 is the auxiliary curve (from [CycleFold](https://eprint.iacr.org/2023/1192.pdf)
33/// approach) where we check the folding of the commitments.
34pub type CF2<C> = <<C as CurveGroup>::BaseField as Field>::BasePrimeField;
35
36/// CommittedInstanceVar contains the u, x, cmE and cmW values which are folded on the main Nova
37/// constraints field (E1::Fr, where E1 is the main curve).
38#[derive(Debug, Clone)]
39pub struct CommittedInstanceVar<C: CurveGroup> {
40 u: FpVar<C::ScalarField>,
41 x: Vec<FpVar<C::ScalarField>>,
42 cmE: NonNativeAffineVar<C::ScalarField>,
43 cmW: NonNativeAffineVar<C::ScalarField>,
44}
45
46impl<C> AllocVar<CommittedInstance<C>, CF1<C>> for CommittedInstanceVar<C>
47where
48 C: CurveGroup,
49 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
50{
51 fn new_variable<T: Borrow<CommittedInstance<C>>>(
52 cs: impl Into<Namespace<CF1<C>>>,
53 f: impl FnOnce() -> Result<T, SynthesisError>,
54 mode: AllocationMode,
55 ) -> Result<Self, SynthesisError> {
56 f().and_then(|val| {
57 let cs = cs.into();
58
59 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
60 let x: Vec<FpVar<C::ScalarField>> =
61 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
62
63 let cmE = NonNativeAffineVar::<C::ScalarField>::new_variable(
64 cs.clone(),
65 || Ok(val.borrow().cmE),
66 mode,
67 )?;
68 let cmW = NonNativeAffineVar::<C::ScalarField>::new_variable(
69 cs.clone(),
70 || Ok(val.borrow().cmW),
71 mode,
72 )?;
73
74 Ok(Self { u, x, cmE, cmW })
75 })
76 }
77}
78
79impl<C> CommittedInstanceVar<C>
80where
81 C: CurveGroup,
82 <C as Group>::ScalarField: Absorb,
83{
84 /// hash implements the committed instance hash compatible with the native implementation from
85 /// CommittedInstance.hash.
86 /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the
87 /// `CommittedInstance`.
88 fn hash(
89 self,
90 crh_params: &CRHParametersVar<CF1<C>>,
91 i: FpVar<CF1<C>>,
92 z_0: Vec<FpVar<CF1<C>>>,
93 z_i: Vec<FpVar<CF1<C>>>,
94 ) -> Result<FpVar<CF1<C>>, SynthesisError> {
95 let input = vec![
96 vec![i],
97 z_0,
98 z_i,
99 vec![self.u],
100 self.x,
101 self.cmE.x,
102 self.cmE.y,
103 self.cmW.x,
104 self.cmW.y,
105 ]
106 .concat();
107 CRHGadget::<C::ScalarField>::evaluate(crh_params, &input)
108 }
109}
110
111/// CommittedInstanceCycleFoldVar represents the commitments to E and W from the CommittedInstance
112/// on the E2, which are folded on the auxiliary curve constraints field (E2::Fr = E1::Fq).
113pub struct CommittedInstanceCycleFoldVar<C: CurveGroup, GC: CurveVar<C, CF2<C>>>
114where
115 for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
116{
117 _c: PhantomData<C>,
118 cmE: GC,
119 cmW: GC,
120}
121
122impl<C, GC> AllocVar<CommittedInstance<C>, CF2<C>> for CommittedInstanceCycleFoldVar<C, GC>
123where
124 C: CurveGroup,
125 GC: CurveVar<C, CF2<C>>,
126 for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
127{
128 fn new_variable<T: Borrow<CommittedInstance<C>>>(
129 cs: impl Into<Namespace<CF2<C>>>,
130 f: impl FnOnce() -> Result<T, SynthesisError>,
131 mode: AllocationMode,
132 ) -> Result<Self, SynthesisError> {
133 f().and_then(|val| {
134 let cs = cs.into();
135
136 let cmE = GC::new_variable(cs.clone(), || Ok(val.borrow().cmE), mode)?;
137 let cmW = GC::new_variable(cs.clone(), || Ok(val.borrow().cmW), mode)?;
138
139 Ok(Self {
140 _c: PhantomData,
141 cmE,
142 cmW,
143 })
144 })
145 }
146}
147
148/// Implements the circuit that does the checks of the Non-Interactive Folding Scheme Verifier
149/// described in section 4 of [Nova](https://eprint.iacr.org/2021/370.pdf), where the cmE & cmW checks are
150/// delegated to the NIFSCycleFoldGadget.
151pub struct NIFSGadget<C: CurveGroup> {
152 _c: PhantomData<C>,
153}
154
155impl<C: CurveGroup> NIFSGadget<C>
156where
157 C: CurveGroup,
158{
159 /// Implements the constraints for NIFS.V for u and x, since cm(E) and cm(W) are delegated to
160 /// the CycleFold circuit.
161 pub fn verify(
162 r: FpVar<CF1<C>>,
163 ci1: CommittedInstanceVar<C>,
164 ci2: CommittedInstanceVar<C>,
165 ci3: CommittedInstanceVar<C>,
166 ) -> Result<Boolean<CF1<C>>, SynthesisError> {
167 // ensure that: ci3.u == ci1.u + r * ci2.u
168 let first_check = ci3.u.is_eq(&(ci1.u + r.clone() * ci2.u))?;
169
170 // ensure that: ci3.x == ci1.x + r * ci2.x
171 let x_rlc = ci1
172 .x
173 .iter()
174 .zip(ci2.x)
175 .map(|(a, b)| a + &r * &b)
176 .collect::<Vec<FpVar<CF1<C>>>>();
177 let second_check = x_rlc.is_eq(&ci3.x)?;
178
179 first_check.and(&second_check)
180 }
181}
182
183/// NIFSCycleFoldGadget performs the Nova NIFS.V elliptic curve points relation checks in the other
184/// curve following [CycleFold](https://eprint.iacr.org/2023/1192.pdf).
185pub struct NIFSCycleFoldGadget<C: CurveGroup, GC: CurveVar<C, CF2<C>>> {
186 _c: PhantomData<C>,
187 _gc: PhantomData<GC>,
188}
189impl<C: CurveGroup, GC: CurveVar<C, CF2<C>>> NIFSCycleFoldGadget<C, GC>
190where
191 C: CurveGroup,
192 GC: CurveVar<C, CF2<C>>,
193 for<'a> &'a GC: GroupOpsBounds<'a, C, GC>,
194{
195 pub fn verify(
196 r_bits: Vec<Boolean<CF2<C>>>,
197 cmT: GC,
198 ci1: CommittedInstanceCycleFoldVar<C, GC>,
199 ci2: CommittedInstanceCycleFoldVar<C, GC>,
200 ci3: CommittedInstanceCycleFoldVar<C, GC>,
201 ) -> Result<Boolean<CF2<C>>, SynthesisError> {
202 // cm(E) check: ci3.cmE == ci1.cmE + r * cmT + r^2 * ci2.cmE
203 let first_check = ci3.cmE.is_eq(
204 &((ci2.cmE.scalar_mul_le(r_bits.iter())? + cmT).scalar_mul_le(r_bits.iter())?
205 + ci1.cmE),
206 )?;
207 // cm(W) check: ci3.cmW == ci1.cmW + r * ci2.cmW
208 let second_check = ECRLC::<C, GC>::check(r_bits, ci1.cmW, ci2.cmW, ci3.cmW)?;
209
210 first_check.and(&second_check)
211 }
212}
213
214/// FCircuit defines the trait of the circuit of the F function, which is the one being executed
215/// inside the agmented F' function.
216pub trait FCircuit<F: PrimeField>: Clone + Copy + Debug {
217 /// returns a new FCircuit instance
218 fn new() -> Self;
219
220 /// computes the next state values in place, assigning z_{i+1} into z_i, and
221 /// computing the new z_i
222 fn step_native(
223 // this method uses self, so that each FCircuit implementation (and different frontends)
224 // can hold a state if needed to store data to compute the next state.
225 self,
226 z_i: Vec<F>,
227 ) -> Vec<F>;
228
229 /// generates the constraints for the step of F for the given z_i
230 fn generate_step_constraints(
231 // this method uses self, so that each FCircuit implementation (and different frontends)
232 // can hold a state if needed to store data to generate the constraints.
233 self,
234 cs: ConstraintSystemRef<F>,
235 z_i: Vec<FpVar<F>>,
236 ) -> Result<Vec<FpVar<F>>, SynthesisError>;
237}
238
239/// AugmentedFCircuit implements the F' circuit (augmented F) defined in
240/// [Nova](https://eprint.iacr.org/2021/370.pdf).
241#[derive(Debug, Clone)]
242pub struct AugmentedFCircuit<C: CurveGroup, FC: FCircuit<CF1<C>>> {
243 pub poseidon_config: PoseidonConfig<CF1<C>>,
244 pub i: Option<CF1<C>>,
245 pub z_0: Option<Vec<C::ScalarField>>,
246 pub z_i: Option<Vec<C::ScalarField>>,
247 pub u_i: Option<CommittedInstance<C>>,
248 pub U_i: Option<CommittedInstance<C>>,
249 pub U_i1: Option<CommittedInstance<C>>,
250 pub cmT: Option<C>,
251 pub F: FC, // F circuit
252 pub x: Option<CF1<C>>, // public inputs (u_{i+1}.x)
253}
254
255impl<C: CurveGroup, FC: FCircuit<CF1<C>>> AugmentedFCircuit<C, FC> {
256 pub fn empty(poseidon_config: &PoseidonConfig<CF1<C>>, F_circuit: FC) -> Self {
257 Self {
258 poseidon_config: poseidon_config.clone(),
259 i: None,
260 z_0: None,
261 z_i: None,
262 u_i: None,
263 U_i: None,
264 U_i1: None,
265 cmT: None,
266 F: F_circuit,
267 x: None,
268 }
269 }
270}
271
272impl<C: CurveGroup, FC: FCircuit<CF1<C>>> AugmentedFCircuit<C, FC>
273where
274 C: CurveGroup,
275 <C as CurveGroup>::BaseField: PrimeField,
276 <C as Group>::ScalarField: Absorb,
277{
278 pub fn get_challenge_native(
279 poseidon_config: &PoseidonConfig<C::ScalarField>,
280 u_i: CommittedInstance<C>,
281 U_i: CommittedInstance<C>,
282 cmT: C,
283 ) -> Result<C::ScalarField, SynthesisError> {
284 let (u_cmE_x, u_cmE_y) = point_to_nonnative_limbs::<C>(u_i.cmE)?;
285 let (u_cmW_x, u_cmW_y) = point_to_nonnative_limbs::<C>(u_i.cmW)?;
286 let (U_cmE_x, U_cmE_y) = point_to_nonnative_limbs::<C>(U_i.cmE)?;
287 let (U_cmW_x, U_cmW_y) = point_to_nonnative_limbs::<C>(U_i.cmW)?;
288 let (cmT_x, cmT_y) = point_to_nonnative_limbs::<C>(cmT)?;
289
290 let input = vec![
291 vec![u_i.u],
292 u_i.x.clone(),
293 u_cmE_x,
294 u_cmE_y,
295 u_cmW_x,
296 u_cmW_y,
297 vec![U_i.u],
298 U_i.x.clone(),
299 U_cmE_x,
300 U_cmE_y,
301 U_cmW_x,
302 U_cmW_y,
303 cmT_x,
304 cmT_y,
305 ]
306 .concat();
307 Ok(CRH::<C::ScalarField>::evaluate(poseidon_config, input).unwrap())
308 }
309
310 pub fn get_challenge(
311 crh_params: &CRHParametersVar<C::ScalarField>,
312 u_i: CommittedInstanceVar<C>,
313 U_i: CommittedInstanceVar<C>,
314 cmT: NonNativeAffineVar<C::ScalarField>,
315 ) -> Result<FpVar<C::ScalarField>, SynthesisError> {
316 let input = vec![
317 vec![u_i.u.clone()],
318 u_i.x.clone(),
319 u_i.cmE.x,
320 u_i.cmE.y,
321 u_i.cmW.x,
322 u_i.cmW.y,
323 vec![U_i.u.clone()],
324 U_i.x.clone(),
325 U_i.cmE.x,
326 U_i.cmE.y,
327 U_i.cmW.x,
328 U_i.cmW.y,
329 cmT.x,
330 cmT.y,
331 ]
332 .concat();
333 CRHGadget::<C::ScalarField>::evaluate(crh_params, &input)
334 }
335}
336
337impl<C: CurveGroup, FC: FCircuit<CF1<C>>> ConstraintSynthesizer<CF1<C>> for AugmentedFCircuit<C, FC>
338where
339 C: CurveGroup,
340 <C as CurveGroup>::BaseField: PrimeField,
341 <C as Group>::ScalarField: Absorb,
342{
343 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C>>) -> Result<(), SynthesisError> {
344 let i =
345 FpVar::<CF1<C>>::new_witness(cs.clone(), || Ok(self.i.unwrap_or_else(CF1::<C>::zero)))?;
346 let z_0 = Vec::<FpVar<CF1<C>>>::new_witness(cs.clone(), || {
347 Ok(self.z_0.unwrap_or_else(|| vec![CF1::<C>::zero()]))
348 })?;
349 let z_i = Vec::<FpVar<CF1<C>>>::new_witness(cs.clone(), || {
350 Ok(self.z_i.unwrap_or_else(|| vec![CF1::<C>::zero()]))
351 })?;
352
353 let u_dummy_native = CommittedInstance::<C>::dummy(1);
354
355 let u_dummy =
356 CommittedInstanceVar::<C>::new_witness(cs.clone(), || Ok(u_dummy_native.clone()))?;
357 let u_i = CommittedInstanceVar::<C>::new_witness(cs.clone(), || {
358 Ok(self.u_i.unwrap_or_else(|| u_dummy_native.clone()))
359 })?;
360 let U_i = CommittedInstanceVar::<C>::new_witness(cs.clone(), || {
361 Ok(self.U_i.unwrap_or_else(|| u_dummy_native.clone()))
362 })?;
363 let U_i1 = CommittedInstanceVar::<C>::new_witness(cs.clone(), || {
364 Ok(self.U_i1.unwrap_or_else(|| u_dummy_native.clone()))
365 })?;
366 let cmT =
367 NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C::zero)))?;
368 let x =
369 FpVar::<CF1<C>>::new_input(cs.clone(), || Ok(self.x.unwrap_or_else(CF1::<C>::zero)))?;
370
371 let crh_params =
372 CRHParametersVar::<C::ScalarField>::new_constant(cs.clone(), self.poseidon_config)?;
373
374 // get z_{i+1} from the F circuit
375 let z_i1 = self.F.generate_step_constraints(cs.clone(), z_i.clone())?;
376
377 let zero = FpVar::<CF1<C>>::new_constant(cs.clone(), CF1::<C>::zero())?;
378 let is_basecase = i.is_eq(&zero)?;
379 let is_not_basecase = i.is_neq(&zero)?;
380
381 // 1. h_{i+1} = u_i.X == H(i, z_0, z_i, U_i)
382 let u_i_x = U_i
383 .clone()
384 .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
385
386 // check that h == u_i.x
387 (u_i.x[0]).conditional_enforce_equal(&u_i_x, &is_not_basecase)?;
388
389 // 2. u_i.cmE==cm(0), u_i.u==1
390 (u_i.cmE.x.is_eq(&u_dummy.cmE.x)?)
391 .conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
392 (u_i.cmE.y.is_eq(&u_dummy.cmE.y)?)
393 .conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
394 (u_i.u.is_one()?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
395
396 // 3. nifs.verify, checks that folding u_i & U_i obtains U_{i+1}.
397 // compute r = H(u_i, U_i, cmT)
398 let r = Self::get_challenge(&crh_params, u_i.clone(), U_i.clone(), cmT)?;
399
400 // Notice that NIFSGadget::verify is not checking the folding of cmE & cmW, since it will
401 // be done on the other curve.
402 let nifs_check = NIFSGadget::<C>::verify(r, u_i, U_i.clone(), U_i1.clone())?;
403 nifs_check.conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
404
405 // 4. (base case) u_{i+1}.X == H(1, z_0, F(z_0)=F(z_i)=z_i1, U_i) (with U_i being dummy)
406 let u_i1_x_basecase = U_i.hash(
407 &crh_params,
408 FpVar::<CF1<C>>::one(),
409 z_0.clone(),
410 z_i1.clone(),
411 )?;
412
413 // 4. (non-base case). u_{i+1}.x = H(i+1, z_0, z_i+1, U_{i+1}), this is the output of F'
414 let u_i1_x = U_i1.hash(
415 &crh_params,
416 i + FpVar::<CF1<C>>::one(),
417 z_0.clone(),
418 z_i1.clone(),
419 )?;
420
421 // if i==0: check x==u_{i+1}.x_basecase
422 u_i1_x_basecase.conditional_enforce_equal(&x, &is_basecase)?;
423 // else: check x==u_{i+1}.x
424 u_i1_x.conditional_enforce_equal(&x, &is_not_basecase)?;
425
426 Ok(())
427 }
428}
429
430#[cfg(test)]
431pub mod tests {
432 use super::*;
433 use ark_ff::BigInteger;
434 use ark_pallas::{constraints::GVar, Fq, Fr, Projective};
435 use ark_r1cs_std::{alloc::AllocVar, R1CSVar};
436 use ark_relations::r1cs::{ConstraintLayer, ConstraintSystem, TracingMode};
437 use ark_std::One;
438 use ark_std::UniformRand;
439 use tracing_subscriber::layer::SubscriberExt;
440
441 use crate::ccs::r1cs::tests::{get_test_r1cs, get_test_z};
442 use crate::folding::nova::{nifs::NIFS, traits::NovaR1CS, Witness};
443 use crate::frontend::arkworks::{extract_r1cs, extract_z};
444 use crate::pedersen::Pedersen;
445 use crate::transcript::poseidon::{tests::poseidon_test_config, PoseidonTranscript};
446 use crate::transcript::Transcript;
447
448 #[derive(Clone, Copy, Debug)]
449 /// TestFCircuit is a variation of `x^3 + x + 5 = y` (as in
450 /// src/frontend/arkworks/mod.rs#tests::TestCircuit), adapted to have 2 public inputs which are
451 /// used as the state. `z_i` is used as `x`, and `z_{i+1}` is used as `y`, and at the next
452 /// step, `z_{i+1}` will be assigned to `z_i`, and a new `z+{i+1}` will be computted.
453 pub struct TestFCircuit<F: PrimeField> {
454 _f: PhantomData<F>,
455 }
456 impl<F: PrimeField> FCircuit<F> for TestFCircuit<F> {
457 fn new() -> Self {
458 Self { _f: PhantomData }
459 }
460 fn step_native(self, z_i: Vec<F>) -> Vec<F> {
461 vec![z_i[0] * z_i[0] * z_i[0] + z_i[0] + F::from(5_u32)]
462 }
463 fn generate_step_constraints(
464 self,
465 cs: ConstraintSystemRef<F>,
466 z_i: Vec<FpVar<F>>,
467 ) -> Result<Vec<FpVar<F>>, SynthesisError> {
468 let five = FpVar::<F>::new_constant(cs.clone(), F::from(5u32))?;
469 let z_i = z_i[0].clone();
470
471 Ok(vec![&z_i * &z_i * &z_i + &z_i + &five])
472 }
473 }
474
475 #[test]
476 fn test_committed_instance_var() {
477 let mut rng = ark_std::test_rng();
478
479 let ci = CommittedInstance::<Projective> {
480 cmE: Projective::rand(&mut rng),
481 u: Fr::rand(&mut rng),
482 cmW: Projective::rand(&mut rng),
483 x: vec![Fr::rand(&mut rng); 1],
484 };
485
486 let cs = ConstraintSystem::<Fr>::new_ref();
487 let ciVar =
488 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
489 assert_eq!(ciVar.u.value().unwrap(), ci.u);
490 assert_eq!(ciVar.x.value().unwrap(), ci.x);
491
492 // check the instantiation of the CycleFold side:
493 let cs = ConstraintSystem::<Fq>::new_ref();
494 let ciVar =
495 CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs.clone(), || {
496 Ok(ci.clone())
497 })
498 .unwrap();
499 assert_eq!(ciVar.cmE.value().unwrap(), ci.cmE);
500 assert_eq!(ciVar.cmW.value().unwrap(), ci.cmW);
501 }
502
503 #[test]
504 fn test_nifs_gadget() {
505 let r1cs = get_test_r1cs();
506 let z1 = get_test_z(3);
507 let z2 = get_test_z(4);
508 let (w1, x1) = r1cs.split_z(&z1);
509 let (w2, x2) = r1cs.split_z(&z2);
510
511 let w1 = Witness::<Projective>::new(w1.clone(), r1cs.A.n_rows);
512 let w2 = Witness::<Projective>::new(w2.clone(), r1cs.A.n_rows);
513
514 let mut rng = ark_std::test_rng();
515 let pedersen_params = Pedersen::<Projective>::new_params(&mut rng, r1cs.A.n_rows);
516
517 // compute committed instances
518 let ci1 = w1.commit(&pedersen_params, x1.clone()).unwrap();
519 let ci2 = w2.commit(&pedersen_params, x2.clone()).unwrap();
520
521 // NIFS.P
522 let (T, cmT) =
523 NIFS::<Projective>::compute_cmT(&pedersen_params, &r1cs, &w1, &ci1, &w2, &ci2).unwrap();
524
525 // get challenge from transcript, since we're in a test skip absorbing values into
526 // transcript
527 let poseidon_config = poseidon_test_config::<Fr>();
528 let mut tr = PoseidonTranscript::<Projective>::new(&poseidon_config);
529 let r_bits = tr.get_challenge_nbits(128);
530 let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
531
532 let (_, ci3) =
533 NIFS::<Projective>::fold_instances(r_Fr, &w1, &ci1, &w2, &ci2, &T, cmT).unwrap();
534
535 let ci3_verifier = NIFS::<Projective>::verify(r_Fr, &ci1, &ci2, &cmT);
536 assert_eq!(ci3_verifier, ci3);
537
538 let cs = ConstraintSystem::<Fr>::new_ref();
539
540 let rVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(r_Fr)).unwrap();
541 let ci1Var =
542 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci1.clone()))
543 .unwrap();
544 let ci2Var =
545 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci2.clone()))
546 .unwrap();
547 let ci3Var =
548 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci3.clone()))
549 .unwrap();
550
551 let nifs_check = NIFSGadget::<Projective>::verify(
552 rVar.clone(),
553 ci1Var.clone(),
554 ci2Var.clone(),
555 ci3Var.clone(),
556 )
557 .unwrap();
558 nifs_check.enforce_equal(&Boolean::<Fr>::TRUE).unwrap();
559 assert!(cs.is_satisfied().unwrap());
560
561 // cs_CC is the Constraint System on the Curve Cycle auxiliary curve constraints field
562 // (E2::Fr)
563 let cs_CC = ConstraintSystem::<Fq>::new_ref();
564
565 let r_bitsVar = Vec::<Boolean<Fq>>::new_witness(cs_CC.clone(), || Ok(r_bits)).unwrap();
566
567 let cmTVar = GVar::new_witness(cs_CC.clone(), || Ok(cmT)).unwrap();
568 let ci1Var =
569 CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
570 Ok(ci1.clone())
571 })
572 .unwrap();
573 let ci2Var =
574 CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
575 Ok(ci2.clone())
576 })
577 .unwrap();
578 let ci3Var =
579 CommittedInstanceCycleFoldVar::<Projective, GVar>::new_witness(cs_CC.clone(), || {
580 Ok(ci3.clone())
581 })
582 .unwrap();
583
584 let nifs_cf_check = NIFSCycleFoldGadget::<Projective, GVar>::verify(
585 r_bitsVar, cmTVar, ci1Var, ci2Var, ci3Var,
586 )
587 .unwrap();
588 nifs_cf_check.enforce_equal(&Boolean::<Fq>::TRUE).unwrap();
589 assert!(cs_CC.is_satisfied().unwrap());
590 }
591
592 #[test]
593 fn test_committed_instance_hash() {
594 let mut rng = ark_std::test_rng();
595 let poseidon_config = poseidon_test_config::<Fr>();
596
597 let i = Fr::from(3_u32);
598 let z_0 = vec![Fr::from(3_u32)];
599 let z_i = vec![Fr::from(3_u32)];
600 let ci = CommittedInstance::<Projective> {
601 cmE: Projective::rand(&mut rng),
602 u: Fr::rand(&mut rng),
603 cmW: Projective::rand(&mut rng),
604 x: vec![Fr::rand(&mut rng); 1],
605 };
606
607 // compute the CommittedInstance hash natively
608 let h = ci
609 .hash(&poseidon_config, i, z_0.clone(), z_i.clone())
610 .unwrap();
611
612 let cs = ConstraintSystem::<Fr>::new_ref();
613
614 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
615 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
616 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
617 let ciVar =
618 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
619
620 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
621
622 // compute the CommittedInstance hash in-circuit
623 let hVar = ciVar.hash(&crh_params, iVar, z_0Var, z_iVar).unwrap();
624 assert!(cs.is_satisfied().unwrap());
625
626 // check that the natively computed and in-circuit computed hashes match
627 assert_eq!(hVar.value().unwrap(), h);
628 }
629
630 // checks that the gadget and native implementations of the challenge computation matcbh
631 #[test]
632 fn test_challenge_gadget() {
633 let mut rng = ark_std::test_rng();
634 let poseidon_config = poseidon_test_config::<Fr>();
635
636 let u_i = CommittedInstance::<Projective> {
637 cmE: Projective::rand(&mut rng),
638 u: Fr::rand(&mut rng),
639 cmW: Projective::rand(&mut rng),
640 x: vec![Fr::rand(&mut rng); 1],
641 };
642 let U_i = CommittedInstance::<Projective> {
643 cmE: Projective::rand(&mut rng),
644 u: Fr::rand(&mut rng),
645 cmW: Projective::rand(&mut rng),
646 x: vec![Fr::rand(&mut rng); 1],
647 };
648 let cmT = Projective::rand(&mut rng);
649
650 // compute the challenge natively
651 let r = AugmentedFCircuit::<Projective, TestFCircuit<Fr>>::get_challenge_native(
652 &poseidon_config,
653 u_i.clone(),
654 U_i.clone(),
655 cmT,
656 )
657 .unwrap();
658
659 let cs = ConstraintSystem::<Fr>::new_ref();
660 let u_iVar =
661 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(u_i.clone()))
662 .unwrap();
663 let U_iVar =
664 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(U_i.clone()))
665 .unwrap();
666 let cmTVar = NonNativeAffineVar::<Fr>::new_witness(cs.clone(), || Ok(cmT)).unwrap();
667
668 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
669
670 // compute the challenge in-circuit
671 let rVar = AugmentedFCircuit::<Projective, TestFCircuit<Fr>>::get_challenge(
672 &crh_params,
673 u_iVar,
674 U_iVar,
675 cmTVar,
676 )
677 .unwrap();
678 assert!(cs.is_satisfied().unwrap());
679
680 // check that the natively computed and in-circuit computed hashes match
681 assert_eq!(rVar.value().unwrap(), r);
682 }
683
684 #[test]
685 /// test_augmented_f_circuit folds the TestFCircuit circuit in multiple iterations, feeding the
686 /// values into the AugmentedFCircuit.
687 fn test_augmented_f_circuit() {
688 let mut layer = ConstraintLayer::default();
689 layer.mode = TracingMode::OnlyConstraints;
690 let subscriber = tracing_subscriber::Registry::default().with(layer);
691 let _guard = tracing::subscriber::set_default(subscriber);
692
693 let mut rng = ark_std::test_rng();
694 let poseidon_config = poseidon_test_config::<Fr>();
695
696 // compute z vector for the initial instance
697 let cs = ConstraintSystem::<Fr>::new_ref();
698
699 // prepare the circuit to obtain its R1CS
700 let F_circuit = TestFCircuit::<Fr>::new();
701 let mut augmented_F_circuit =
702 AugmentedFCircuit::<Projective, TestFCircuit<Fr>>::empty(&poseidon_config, F_circuit);
703 augmented_F_circuit
704 .generate_constraints(cs.clone())
705 .unwrap();
706 cs.finalize();
707 println!("num_constraints={:?}", cs.num_constraints());
708 let cs = cs.into_inner().unwrap();
709 let r1cs = extract_r1cs::<Fr>(&cs);
710 let z = extract_z::<Fr>(&cs); // includes 1 and public inputs
711 let (w, x) = r1cs.split_z(&z);
712 assert_eq!(z.len(), r1cs.A.n_cols);
713 assert_eq!(1 + x.len() + w.len(), r1cs.A.n_cols);
714 assert_eq!(r1cs.l, x.len());
715
716 let pedersen_params = Pedersen::<Projective>::new_params(&mut rng, r1cs.A.n_rows);
717
718 // first step, set z_i=z_0=3 and z_{i+1}=35 (initial values)
719 let z_0 = vec![Fr::from(3_u32)];
720 let mut z_i = z_0.clone();
721 let mut z_i1 = vec![Fr::from(35_u32)];
722
723 let w_dummy = Witness::<Projective>::new(vec![Fr::zero(); w.len()], r1cs.A.n_rows);
724 let u_dummy = CommittedInstance::<Projective>::dummy(x.len());
725
726 // W_i is a 'dummy witness', all zeroes, but with the size corresponding to the R1CS that
727 // we're working with.
728 // set U_i <-- dummy instance
729 let mut W_i = w_dummy.clone();
730 let mut U_i = u_dummy.clone();
731 r1cs.check_relaxed_instance_relation(&W_i, &U_i).unwrap();
732
733 let mut w_i = w_dummy.clone();
734 let mut u_i = u_dummy.clone();
735 let (mut W_i1, mut U_i1, mut cmT): (
736 Witness<Projective>,
737 CommittedInstance<Projective>,
738 Projective,
739 ) = (w_dummy.clone(), u_dummy.clone(), Projective::generator());
740 // as expected, dummy instances pass the relaxed_r1cs check
741 r1cs.check_relaxed_instance_relation(&W_i1, &U_i1).unwrap();
742
743 let mut i = Fr::zero();
744 let mut u_i1_x: Fr;
745 for _ in 0..4 {
746 if i == Fr::zero() {
747 // base case: i=0, z_i=z_0, U_i = U_d := dummy instance
748 // u_1.x = H(1, z_0, z_i, U_i)
749 u_i1_x = U_i
750 .hash(&poseidon_config, Fr::one(), z_0.clone(), z_i1.clone())
751 .unwrap();
752
753 // base case
754 augmented_F_circuit = AugmentedFCircuit::<Projective, TestFCircuit<Fr>> {
755 poseidon_config: poseidon_config.clone(),
756 i: Some(i), // = 0
757 z_0: Some(z_0.clone()), // = z_i=3
758 z_i: Some(z_i.clone()),
759 u_i: Some(u_i.clone()), // = dummy
760 U_i: Some(U_i.clone()), // = dummy
761 U_i1: Some(U_i1.clone()), // = dummy
762 cmT: Some(cmT),
763 F: F_circuit,
764 x: Some(u_i1_x),
765 };
766 } else {
767 r1cs.check_relaxed_instance_relation(&w_i, &u_i).unwrap();
768 r1cs.check_relaxed_instance_relation(&W_i, &U_i).unwrap();
769
770 // U_{i+1}
771 let T: Vec<Fr>;
772 (T, cmT) = NIFS::<Projective>::compute_cmT(
773 &pedersen_params,
774 &r1cs,
775 &w_i,
776 &u_i,
777 &W_i,
778 &U_i,
779 )
780 .unwrap();
781
782 // get challenge r
783 let r_Fr = AugmentedFCircuit::<Projective, TestFCircuit<Fr>>::get_challenge_native(
784 &poseidon_config,
785 u_i.clone(),
786 U_i.clone(),
787 cmT,
788 )
789 .unwrap();
790
791 (W_i1, U_i1) =
792 NIFS::<Projective>::fold_instances(r_Fr, &w_i, &u_i, &W_i, &U_i, &T, cmT)
793 .unwrap();
794
795 r1cs.check_relaxed_instance_relation(&W_i1, &U_i1).unwrap();
796
797 // folded instance output (public input, x)
798 // u_{i+1}.x = H(i+1, z_0, z_{i+1}, U_{i+1})
799 u_i1_x = U_i1
800 .hash(&poseidon_config, i + Fr::one(), z_0.clone(), z_i1.clone())
801 .unwrap();
802
803 augmented_F_circuit = AugmentedFCircuit::<Projective, TestFCircuit<Fr>> {
804 poseidon_config: poseidon_config.clone(),
805 i: Some(i),
806 z_0: Some(z_0.clone()),
807 z_i: Some(z_i.clone()),
808 u_i: Some(u_i),
809 U_i: Some(U_i.clone()),
810 U_i1: Some(U_i1.clone()),
811 cmT: Some(cmT),
812 F: F_circuit,
813 x: Some(u_i1_x),
814 };
815 }
816
817 let cs = ConstraintSystem::<Fr>::new_ref();
818
819 augmented_F_circuit
820 .generate_constraints(cs.clone())
821 .unwrap();
822 let is_satisfied = cs.is_satisfied().unwrap();
823 if !is_satisfied {
824 println!("{:?}", cs.which_is_unsatisfied());
825 }
826 assert!(is_satisfied);
827
828 cs.finalize();
829 let cs = cs.into_inner().unwrap();
830 // notice that here we use 'Z' (uppercase) to denote the 'z-vector' as in the paper,
831 // not the value 'z' (lowercase) which is the state
832 let Z_i1 = extract_z::<Fr>(&cs);
833 let (w_i1, x_i1) = r1cs.split_z(&Z_i1);
834 assert_eq!(x_i1.len(), 1);
835 assert_eq!(x_i1[0], u_i1_x);
836
837 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
838 // assign them directly to w_i, u_i.
839 w_i = Witness::<Projective>::new(w_i1.clone(), r1cs.A.n_rows);
840 u_i = w_i.commit(&pedersen_params, vec![u_i1_x]).unwrap();
841
842 r1cs.check_relaxed_instance_relation(&w_i, &u_i).unwrap();
843 r1cs.check_relaxed_instance_relation(&W_i1, &U_i1).unwrap();
844
845 // set values for next iteration
846 i += Fr::one();
847 // advance the F circuit state
848 z_i = z_i1.clone();
849 z_i1 = F_circuit.step_native(z_i.clone());
850 U_i = U_i1.clone();
851 W_i = W_i1.clone();
852 }
853 }
854}