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};
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.z_0.unwrap_or(vec![CF1::<C1>::zero()]))
314 })?;
315 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
316 Ok(self.z_i.unwrap_or(vec![CF1::<C1>::zero()]))
317 })?;
318
319 let u_dummy_native = CommittedInstance::<C1>::dummy(1);
320 let u_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
321 Ok(self.u_i.unwrap_or(u_dummy_native.clone()))
322 })?;
323 let U_i = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
324 Ok(self.U_i.unwrap_or(u_dummy_native.clone()))
325 })?;
326 let U_i1 = CommittedInstanceVar::<C1>::new_witness(cs.clone(), || {
327 Ok(self.U_i1.unwrap_or(u_dummy_native.clone()))
328 })?;
329 let cmT =
330 NonNativeAffineVar::new_witness(cs.clone(), || Ok(self.cmT.unwrap_or_else(C1::zero)))?;
331 let x =
332 FpVar::<CF1<C1>>::new_input(cs.clone(), || Ok(self.x.unwrap_or_else(CF1::<C1>::zero)))?;
333
334 let crh_params = CRHParametersVar::<C1::ScalarField>::new_constant(
335 cs.clone(),
336 self.poseidon_config.clone(),
337 )?;
338
339 // get z_{i+1} from the F circuit
340 let z_i1 = self.F.generate_step_constraints(cs.clone(), z_i.clone())?;
341
342 let zero = FpVar::<CF1<C1>>::new_constant(cs.clone(), CF1::<C1>::zero())?;
343 let is_not_basecase = i.is_neq(&zero)?;
344
345 // 1. u_i.x == H(i, z_0, z_i, U_i)
346 let u_i_x = U_i
347 .clone()
348 .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
349
350 // check that h == u_i.x
351 (u_i.x[0]).conditional_enforce_equal(&u_i_x, &is_not_basecase)?;
352
353 // 2. u_i.cmE==cm(0), u_i.u==1
354 let zero_x = NonNativeFieldVar::<C1::BaseField, C1::ScalarField>::new_constant(
355 cs.clone(),
356 C1::BaseField::zero(),
357 )?
358 .to_constraint_field()?;
359 let zero_y = NonNativeFieldVar::<C1::BaseField, C1::ScalarField>::new_constant(
360 cs.clone(),
361 C1::BaseField::one(),
362 )?
363 .to_constraint_field()?;
364 (u_i.cmE.x.is_eq(&zero_x)?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
365 (u_i.cmE.y.is_eq(&zero_y)?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
366 (u_i.u.is_one()?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
367
368 // 3. nifs.verify, checks that folding u_i & U_i obtains U_{i+1}.
369 // compute r = H(u_i, U_i, cmT)
370 let r_bits = ChallengeGadget::<C1>::get_challenge_gadget(
371 cs.clone(),
372 &self.poseidon_config,
373 u_i.clone(),
374 U_i.clone(),
375 cmT.clone(),
376 )?;
377 let r = Boolean::le_bits_to_fp_var(&r_bits)?;
378
379 // Notice that NIFSGadget::verify is not checking the folding of cmE & cmW, since it will
380 // be done on the other curve.
381 let nifs_check = NIFSGadget::<C1>::verify(r, u_i.clone(), U_i.clone(), U_i1.clone())?;
382 nifs_check.conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
383
384 // 4. u_{i+1}.x = H(i+1, z_0, z_i+1, U_{i+1}), this is the output of F'
385 let u_i1_x = U_i1.clone().hash(
386 &crh_params,
387 i + FpVar::<CF1<C1>>::one(),
388 z_0.clone(),
389 z_i1.clone(),
390 )?;
391
392 u_i1_x.enforce_equal(&x)?;
393
394 // CycleFold part
395 let cf_u_dummy_native = CommittedInstance::<C2>::dummy(CF_IO_LEN);
396 let cf_u_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
397 Ok(self.cf_u_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
398 })?;
399 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
400 Ok(self.cf_U_i.unwrap_or_else(|| cf_u_dummy_native.clone()))
401 })?;
402 let cf_U_i1 = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
403 Ok(self.cf_U_i1.unwrap_or_else(|| cf_u_dummy_native.clone()))
404 })?;
405 let cf_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf_cmT.unwrap_or_else(C2::zero)))?;
406 // cf_r_nonnat is an auxiliary input
407 let cf_r_nonnat =
408 NonNativeFieldVar::<C2::ScalarField, CF2<C2>>::new_witness(cs.clone(), || {
409 Ok(self.cf_r_nonnat.unwrap_or_else(C2::ScalarField::zero))
410 })?;
411
412 // check that cf_u_i.x == [u_i, U_i, U_{i+1}]
413 let incircuit_x = vec![
414 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,
415 U_i1.cmE.x, U_i1.cmE.y, U_i1.cmW.x, U_i1.cmW.y,
416 ]
417 .concat();
418
419 let mut cf_u_i_x: Vec<FpVar<CF2<C2>>> = vec![];
420 for x_i in cf_u_i.x.iter() {
421 let mut x_fpvar = x_i.to_constraint_field()?;
422 cf_u_i_x.append(&mut x_fpvar);
423 }
424 cf_u_i_x.conditional_enforce_equal(&incircuit_x, &is_not_basecase)?;
425
426 // cf_r_bits is denoted by rho* in the paper
427 let cf_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
428 cs.clone(),
429 &self.poseidon_config,
430 cf_u_i.clone(),
431 cf_U_i.clone(),
432 cf_cmT.clone(),
433 )?;
434 // assert that cf_r_bits == cf_r_nonnat converted to bits. cf_r_nonnat is just an auxiliary
435 // value used to compute RLC of NonNativeFieldVar values, since we can convert
436 // NonNativeFieldVar into Vec<Boolean>, but not in the other direction.
437 let cf_r_nonnat_bits = cf_r_nonnat.to_bits_le()?;
438 cf_r_bits.conditional_enforce_equal(&cf_r_nonnat_bits[..N_BITS_RO], &is_not_basecase)?;
439
440 // check cf_u_i.cmE=0, cf_u_i.u=1
441 (cf_u_i.cmE.is_zero()?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
442 (cf_u_i.u.is_one()?).conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
443
444 // check the fold of all the parameteres of the CycleFold instances, where the elliptic
445 // curve points relations are checked natively in Curve1 circuit (this one)
446 let v = NIFSFullGadget::<C2, GC2>::verify(
447 cf_r_bits,
448 cf_r_nonnat,
449 cf_cmT,
450 cf_U_i,
451 cf_u_i,
452 cf_U_i1,
453 )?;
454 v.conditional_enforce_equal(&Boolean::TRUE, &is_not_basecase)?;
455
456 Ok(())
457 }
458}
459
460#[cfg(test)]
461pub mod tests {
462 use super::*;
463 use ark_ff::BigInteger;
464 use ark_pallas::{Fq, Fr, Projective};
465 use ark_r1cs_std::{alloc::AllocVar, R1CSVar};
466 use ark_relations::r1cs::{ConstraintLayer, ConstraintSystem, TracingMode};
467 use ark_std::One;
468 use ark_std::UniformRand;
469 use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
470 use tracing_subscriber::layer::SubscriberExt;
471
472 use crate::ccs::r1cs::{extract_r1cs, extract_w_x};
473 use crate::folding::nova::nifs::tests::prepare_simple_fold_inputs;
474 use crate::folding::nova::{
475 ivc::get_committed_instance_coordinates, nifs::NIFS, traits::NovaR1CS, Witness,
476 };
477 use crate::frontend::tests::CubicFCircuit;
478 use crate::pedersen::Pedersen;
479 use crate::transcript::poseidon::tests::poseidon_test_config;
480
481 #[test]
482 fn test_committed_instance_var() {
483 let mut rng = ark_std::test_rng();
484
485 let ci = CommittedInstance::<Projective> {
486 cmE: Projective::rand(&mut rng),
487 u: Fr::rand(&mut rng),
488 cmW: Projective::rand(&mut rng),
489 x: vec![Fr::rand(&mut rng); 1],
490 };
491
492 let cs = ConstraintSystem::<Fr>::new_ref();
493 let ciVar =
494 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
495 assert_eq!(ciVar.u.value().unwrap(), ci.u);
496 assert_eq!(ciVar.x.value().unwrap(), ci.x);
497 // the values cmE and cmW are checked in the CycleFold's circuit
498 // CommittedInstanceInCycleFoldVar in
499 // nova::cyclefold::tests::test_committed_instance_cyclefold_var
500 }
501
502 #[test]
503 fn test_nifs_gadget() {
504 let (_, _, _, _, ci1, _, ci2, _, ci3, _, cmT, _, r_Fr) = prepare_simple_fold_inputs();
505
506 let ci3_verifier = NIFS::<Projective>::verify(r_Fr, &ci1, &ci2, &cmT);
507 assert_eq!(ci3_verifier, ci3);
508
509 let cs = ConstraintSystem::<Fr>::new_ref();
510
511 let rVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(r_Fr)).unwrap();
512 let ci1Var =
513 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci1.clone()))
514 .unwrap();
515 let ci2Var =
516 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci2.clone()))
517 .unwrap();
518 let ci3Var =
519 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci3.clone()))
520 .unwrap();
521
522 let nifs_check = NIFSGadget::<Projective>::verify(
523 rVar.clone(),
524 ci1Var.clone(),
525 ci2Var.clone(),
526 ci3Var.clone(),
527 )
528 .unwrap();
529 nifs_check.enforce_equal(&Boolean::<Fr>::TRUE).unwrap();
530 assert!(cs.is_satisfied().unwrap());
531 }
532
533 #[test]
534 fn test_committed_instance_hash() {
535 let mut rng = ark_std::test_rng();
536 let poseidon_config = poseidon_test_config::<Fr>();
537
538 let i = Fr::from(3_u32);
539 let z_0 = vec![Fr::from(3_u32)];
540 let z_i = vec![Fr::from(3_u32)];
541 let ci = CommittedInstance::<Projective> {
542 cmE: Projective::rand(&mut rng),
543 u: Fr::rand(&mut rng),
544 cmW: Projective::rand(&mut rng),
545 x: vec![Fr::rand(&mut rng); 1],
546 };
547
548 // compute the CommittedInstance hash natively
549 let h = ci
550 .hash(&poseidon_config, i, z_0.clone(), z_i.clone())
551 .unwrap();
552
553 let cs = ConstraintSystem::<Fr>::new_ref();
554
555 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
556 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
557 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
558 let ciVar =
559 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(ci.clone())).unwrap();
560
561 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
562
563 // compute the CommittedInstance hash in-circuit
564 let hVar = ciVar.hash(&crh_params, iVar, z_0Var, z_iVar).unwrap();
565 assert!(cs.is_satisfied().unwrap());
566
567 // check that the natively computed and in-circuit computed hashes match
568 assert_eq!(hVar.value().unwrap(), h);
569 }
570
571 // checks that the gadget and native implementations of the challenge computation matcbh
572 #[test]
573 fn test_challenge_gadget() {
574 let mut rng = ark_std::test_rng();
575 let poseidon_config = poseidon_test_config::<Fr>();
576
577 let u_i = CommittedInstance::<Projective> {
578 cmE: Projective::rand(&mut rng),
579 u: Fr::rand(&mut rng),
580 cmW: Projective::rand(&mut rng),
581 x: vec![Fr::rand(&mut rng); 1],
582 };
583 let U_i = CommittedInstance::<Projective> {
584 cmE: Projective::rand(&mut rng),
585 u: Fr::rand(&mut rng),
586 cmW: Projective::rand(&mut rng),
587 x: vec![Fr::rand(&mut rng); 1],
588 };
589 let cmT = Projective::rand(&mut rng);
590
591 // compute the challenge natively
592 let r_bits = ChallengeGadget::<Projective>::get_challenge_native(
593 &poseidon_config,
594 u_i.clone(),
595 U_i.clone(),
596 cmT,
597 )
598 .unwrap();
599 let r = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
600
601 let cs = ConstraintSystem::<Fr>::new_ref();
602 let u_iVar =
603 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(u_i.clone()))
604 .unwrap();
605 let U_iVar =
606 CommittedInstanceVar::<Projective>::new_witness(cs.clone(), || Ok(U_i.clone()))
607 .unwrap();
608 let cmTVar = NonNativeAffineVar::<Fr>::new_witness(cs.clone(), || Ok(cmT)).unwrap();
609
610 // compute the challenge in-circuit
611 let r_bitsVar = ChallengeGadget::<Projective>::get_challenge_gadget(
612 cs.clone(),
613 &poseidon_config,
614 u_iVar,
615 U_iVar,
616 cmTVar,
617 )
618 .unwrap();
619 assert!(cs.is_satisfied().unwrap());
620
621 // check that the natively computed and in-circuit computed hashes match
622 let rVar = Boolean::le_bits_to_fp_var(&r_bitsVar).unwrap();
623 assert_eq!(rVar.value().unwrap(), r);
624 assert_eq!(r_bitsVar.value().unwrap(), r_bits);
625 }
626
627 #[test]
628 /// test_augmented_f_circuit folds the CubicFCircuit circuit in multiple iterations, feeding the
629 /// values into the AugmentedFCircuit.
630 fn test_augmented_f_circuit() {
631 let mut layer = ConstraintLayer::default();
632 layer.mode = TracingMode::OnlyConstraints;
633 let subscriber = tracing_subscriber::Registry::default().with(layer);
634 let _guard = tracing::subscriber::set_default(subscriber);
635
636 let mut rng = ark_std::test_rng();
637 let poseidon_config = poseidon_test_config::<Fr>();
638
639 // compute z vector for the initial instance
640 let cs = ConstraintSystem::<Fr>::new_ref();
641
642 // prepare the circuit to obtain its R1CS
643 let F_circuit = CubicFCircuit::<Fr>::new(());
644 let mut augmented_F_circuit =
645 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>>::empty(
646 &poseidon_config,
647 F_circuit,
648 );
649 augmented_F_circuit
650 .generate_constraints(cs.clone())
651 .unwrap();
652 cs.finalize();
653 println!("num_constraints={:?}", cs.num_constraints());
654 let cs = cs.into_inner().unwrap();
655 let r1cs = extract_r1cs::<Fr>(&cs);
656 let (w, x) = extract_w_x::<Fr>(&cs);
657 assert_eq!(1 + x.len() + w.len(), r1cs.A.n_cols);
658 assert_eq!(r1cs.l, x.len());
659
660 let pedersen_params = Pedersen::<Projective>::new_params(&mut rng, r1cs.A.n_rows);
661
662 // first step, set z_i=z_0=3 and z_{i+1}=35 (initial values)
663 let z_0 = vec![Fr::from(3_u32)];
664 let mut z_i = z_0.clone();
665 let mut z_i1 = vec![Fr::from(35_u32)];
666
667 let w_dummy = Witness::<Projective>::new(vec![Fr::zero(); w.len()], r1cs.A.n_rows);
668 let u_dummy = CommittedInstance::<Projective>::dummy(x.len());
669
670 // W_i is a 'dummy witness', all zeroes, but with the size corresponding to the R1CS that
671 // we're working with.
672 // set U_i <-- dummy instance
673 let mut W_i = w_dummy.clone();
674 let mut U_i = u_dummy.clone();
675 r1cs.check_relaxed_instance_relation(&W_i, &U_i).unwrap();
676
677 let mut w_i = w_dummy.clone();
678 let mut u_i = u_dummy.clone();
679 let (mut W_i1, mut U_i1, mut cmT): (
680 Witness<Projective>,
681 CommittedInstance<Projective>,
682 Projective,
683 ) = (w_dummy.clone(), u_dummy.clone(), Projective::generator());
684 // as expected, dummy instances pass the relaxed_r1cs check
685 r1cs.check_relaxed_instance_relation(&W_i1, &U_i1).unwrap();
686
687 let mut i = Fr::zero();
688 let mut u_i1_x: Fr;
689 for _ in 0..4 {
690 if i == Fr::zero() {
691 // base case: i=0, z_i=z_0, U_i = U_d := dummy instance
692 // u_1.x = H(1, z_0, z_i, U_i)
693 u_i1_x = U_i
694 .hash(&poseidon_config, Fr::one(), z_0.clone(), z_i1.clone())
695 .unwrap();
696
697 // base case
698 augmented_F_circuit =
699 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
700 _gc2: PhantomData,
701 poseidon_config: poseidon_config.clone(),
702 i: Some(i), // = 0
703 z_0: Some(z_0.clone()), // = z_i=3
704 z_i: Some(z_i.clone()),
705 u_i: Some(u_i.clone()), // = dummy
706 U_i: Some(U_i.clone()), // = dummy
707 U_i1: Some(U_i1.clone()), // = dummy
708 cmT: Some(cmT),
709 F: F_circuit,
710 x: Some(u_i1_x),
711 // cyclefold instances (not tested in this test)
712 cf_u_i: None,
713 cf_U_i: None,
714 cf_U_i1: None,
715 cf_cmT: None,
716 cf_r_nonnat: None,
717 };
718 } else {
719 r1cs.check_relaxed_instance_relation(&w_i, &u_i).unwrap();
720 r1cs.check_relaxed_instance_relation(&W_i, &U_i).unwrap();
721
722 // U_{i+1}
723 let T: Vec<Fr>;
724 (T, cmT) = NIFS::<Projective>::compute_cmT(
725 &pedersen_params,
726 &r1cs,
727 &w_i,
728 &u_i,
729 &W_i,
730 &U_i,
731 )
732 .unwrap();
733
734 // get challenge r
735 let r_bits = ChallengeGadget::<Projective>::get_challenge_native(
736 &poseidon_config,
737 u_i.clone(),
738 U_i.clone(),
739 cmT,
740 )
741 .unwrap();
742 let r_Fr = Fr::from_bigint(BigInteger::from_bits_le(&r_bits)).unwrap();
743
744 (W_i1, U_i1) =
745 NIFS::<Projective>::fold_instances(r_Fr, &w_i, &u_i, &W_i, &U_i, &T, cmT)
746 .unwrap();
747
748 r1cs.check_relaxed_instance_relation(&W_i1, &U_i1).unwrap();
749
750 // folded instance output (public input, x)
751 // u_{i+1}.x = H(i+1, z_0, z_{i+1}, U_{i+1})
752 u_i1_x = U_i1
753 .hash(&poseidon_config, i + Fr::one(), z_0.clone(), z_i1.clone())
754 .unwrap();
755
756 // set up dummy cyclefold instances just for the sake of this test. Warning, this
757 // is only because we are in a test were we're not testing the cyclefold side of
758 // things.
759 let cf_W_i = Witness::<Projective2>::new(vec![Fq::zero(); 1], 1);
760 let cf_U_i = CommittedInstance::<Projective2>::dummy(CF_IO_LEN);
761 let cf_u_i_x = [
762 get_committed_instance_coordinates(&u_i),
763 get_committed_instance_coordinates(&U_i),
764 get_committed_instance_coordinates(&U_i1),
765 ]
766 .concat();
767 let cf_u_i = CommittedInstance::<Projective2> {
768 cmE: cf_U_i.cmE,
769 u: Fq::one(),
770 cmW: cf_U_i.cmW,
771 x: cf_u_i_x,
772 };
773 let cf_w_i = cf_W_i.clone();
774 let (cf_T, cf_cmT): (Vec<Fq>, Projective2) =
775 (vec![Fq::zero(); cf_W_i.E.len()], Projective2::zero());
776 let cf_r_bits =
777 CycleFoldChallengeGadget::<Projective2, GVar2>::get_challenge_native(
778 &poseidon_config,
779 cf_u_i.clone(),
780 cf_U_i.clone(),
781 cf_cmT,
782 )
783 .unwrap();
784 let cf_r_Fq = Fq::from_bigint(BigInteger::from_bits_le(&cf_r_bits)).unwrap();
785 let (_, cf_U_i1) = NIFS::<Projective2>::fold_instances(
786 cf_r_Fq, &cf_W_i, &cf_U_i, &cf_w_i, &cf_u_i, &cf_T, cf_cmT,
787 )
788 .unwrap();
789
790 augmented_F_circuit =
791 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
792 _gc2: PhantomData,
793 poseidon_config: poseidon_config.clone(),
794 i: Some(i),
795 z_0: Some(z_0.clone()),
796 z_i: Some(z_i.clone()),
797 u_i: Some(u_i),
798 U_i: Some(U_i.clone()),
799 U_i1: Some(U_i1.clone()),
800 cmT: Some(cmT),
801 F: F_circuit,
802 x: Some(u_i1_x),
803 cf_u_i: Some(cf_u_i),
804 cf_U_i: Some(cf_U_i),
805 cf_U_i1: Some(cf_U_i1),
806 cf_cmT: Some(cf_cmT),
807 cf_r_nonnat: Some(cf_r_Fq),
808 };
809 }
810
811 let cs = ConstraintSystem::<Fr>::new_ref();
812
813 augmented_F_circuit
814 .generate_constraints(cs.clone())
815 .unwrap();
816 let is_satisfied = cs.is_satisfied().unwrap();
817 if !is_satisfied {
818 dbg!(cs.which_is_unsatisfied().unwrap());
819 }
820 assert!(is_satisfied);
821
822 cs.finalize();
823 let cs = cs.into_inner().unwrap();
824 let (w_i1, x_i1) = extract_w_x::<Fr>(&cs);
825 assert_eq!(x_i1.len(), 1);
826 assert_eq!(x_i1[0], u_i1_x);
827
828 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
829 // assign them directly to w_i, u_i.
830 w_i = Witness::<Projective>::new(w_i1.clone(), r1cs.A.n_rows);
831 u_i = w_i.commit(&pedersen_params, vec![u_i1_x]).unwrap();
832
833 r1cs.check_relaxed_instance_relation(&w_i, &u_i).unwrap();
834 r1cs.check_relaxed_instance_relation(&W_i1, &U_i1).unwrap();
835
836 // set values for next iteration
837 i += Fr::one();
838 // advance the F circuit state
839 z_i = z_i1.clone();
840 z_i1 = F_circuit.step_native(z_i.clone()).unwrap();
841 U_i = U_i1.clone();
842 W_i = W_i1.clone();
843 }
844 }
845}