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