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