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