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