sonobe/folding-schemes/src/folding/hypernova/circuits.rs
folding-schemes/src/folding/hypernova/circuits.rsRaw
1/// Implementation of [HyperNova](https://eprint.iacr.org/2023/573.pdf) circuits
2use ark_crypto_primitives::crh::{
3 poseidon::constraints::{CRHGadget, CRHParametersVar},
4 CRHSchemeGadget,
5};
6use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
7use ark_ec::{CurveGroup, Group};
8use ark_ff::PrimeField;
9use ark_r1cs_std::{
10 alloc::{AllocVar, AllocationMode},
11 boolean::Boolean,
12 eq::EqGadget,
13 fields::{fp::FpVar, FieldVar},
14 groups::GroupOpsBounds,
15 prelude::CurveVar,
16 R1CSVar, ToConstraintFieldGadget,
17};
18use ark_relations::r1cs::{
19 ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, Namespace, SynthesisError,
20};
21use ark_std::{fmt::Debug, ops::Neg, One, Zero};
22use core::{borrow::Borrow, marker::PhantomData};
23
24use super::{
25 cccs::CCCS,
26 lcccs::LCCCS,
27 nimfs::{NIMFSProof, NIMFS},
28 Witness,
29};
30use crate::constants::N_BITS_RO;
31use crate::folding::{
32 circuits::cyclefold::{
33 CycleFoldChallengeGadget, CycleFoldCommittedInstanceVar, NIFSFullGadget, CF_IO_LEN,
34 },
35 circuits::{
36 nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
37 sum_check::{IOPProofVar, SumCheckVerifierGadget, VPAuxInfoVar},
38 utils::EqEvalGadget,
39 CF1, CF2,
40 },
41 nova::{get_r1cs_from_cs, CommittedInstance},
42};
43use crate::frontend::FCircuit;
44use crate::utils::virtual_polynomial::VPAuxInfo;
45use crate::Error;
46use crate::{
47 ccs::{r1cs::extract_r1cs, CCS},
48 transcript::{
49 poseidon::{PoseidonTranscript, PoseidonTranscriptVar},
50 Transcript, TranscriptVar,
51 },
52};
53
54/// Committed CCS instance
55#[derive(Debug, Clone)]
56pub struct CCCSVar<C: CurveGroup>
57where
58 <C as CurveGroup>::BaseField: PrimeField,
59{
60 // Commitment to witness
61 pub C: NonNativeAffineVar<C>,
62 // Public io
63 pub x: Vec<FpVar<CF1<C>>>,
64}
65impl<C> AllocVar<CCCS<C>, CF1<C>> for CCCSVar<C>
66where
67 C: CurveGroup,
68 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
69{
70 fn new_variable<T: Borrow<CCCS<C>>>(
71 cs: impl Into<Namespace<CF1<C>>>,
72 f: impl FnOnce() -> Result<T, SynthesisError>,
73 mode: AllocationMode,
74 ) -> Result<Self, SynthesisError> {
75 f().and_then(|val| {
76 let cs = cs.into();
77
78 let C = NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?;
79 let x: Vec<FpVar<C::ScalarField>> =
80 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
81
82 Ok(Self { C, x })
83 })
84 }
85}
86
87/// Linearized Committed CCS instance
88#[derive(Debug, Clone)]
89pub struct LCCCSVar<C: CurveGroup>
90where
91 <C as CurveGroup>::BaseField: PrimeField,
92{
93 // Commitment to witness
94 pub C: NonNativeAffineVar<C>,
95 // Relaxation factor of z for folded LCCCS
96 pub u: FpVar<CF1<C>>,
97 // Public io
98 pub x: Vec<FpVar<CF1<C>>>,
99 // Random evaluation point for the v_i
100 pub r_x: Vec<FpVar<CF1<C>>>,
101 // Vector of v_i
102 pub v: Vec<FpVar<CF1<C>>>,
103}
104impl<C> AllocVar<LCCCS<C>, CF1<C>> for LCCCSVar<C>
105where
106 C: CurveGroup,
107 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
108{
109 fn new_variable<T: Borrow<LCCCS<C>>>(
110 cs: impl Into<Namespace<CF1<C>>>,
111 f: impl FnOnce() -> Result<T, SynthesisError>,
112 mode: AllocationMode,
113 ) -> Result<Self, SynthesisError> {
114 f().and_then(|val| {
115 let cs = cs.into();
116
117 let C = NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?;
118 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
119 let x: Vec<FpVar<C::ScalarField>> =
120 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
121 let r_x: Vec<FpVar<C::ScalarField>> =
122 Vec::new_variable(cs.clone(), || Ok(val.borrow().r_x.clone()), mode)?;
123 let v: Vec<FpVar<C::ScalarField>> =
124 Vec::new_variable(cs.clone(), || Ok(val.borrow().v.clone()), mode)?;
125
126 Ok(Self { C, u, x, r_x, v })
127 })
128 }
129}
130
131impl<C> LCCCSVar<C>
132where
133 C: CurveGroup,
134 <C as Group>::ScalarField: Absorb,
135 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
136{
137 /// [`LCCCSVar`].hash implements the LCCCS instance hash compatible with the native
138 /// implementation from LCCCS.hash.
139 /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the LCCCS.
140 /// Additionally it returns the vector of the field elements from the self parameters, so they
141 /// can be reused in other gadgets avoiding recalculating (reconstraining) them.
142 #[allow(clippy::type_complexity)]
143 pub fn hash(
144 self,
145 crh_params: &CRHParametersVar<CF1<C>>,
146 i: FpVar<CF1<C>>,
147 z_0: Vec<FpVar<CF1<C>>>,
148 z_i: Vec<FpVar<CF1<C>>>,
149 ) -> Result<(FpVar<CF1<C>>, Vec<FpVar<CF1<C>>>), SynthesisError> {
150 let U_vec = [
151 self.C.to_constraint_field()?,
152 vec![self.u],
153 self.x,
154 self.r_x,
155 self.v,
156 ]
157 .concat();
158 let input = [vec![i], z_0, z_i, U_vec.clone()].concat();
159 Ok((
160 CRHGadget::<C::ScalarField>::evaluate(crh_params, &input)?,
161 U_vec,
162 ))
163 }
164}
165
166/// ProofVar defines a multifolding proof
167#[derive(Debug)]
168pub struct ProofVar<C: CurveGroup> {
169 pub sc_proof: IOPProofVar<C>,
170 #[allow(clippy::type_complexity)]
171 pub sigmas_thetas: (Vec<Vec<FpVar<CF1<C>>>>, Vec<Vec<FpVar<CF1<C>>>>),
172}
173impl<C> AllocVar<NIMFSProof<C>, CF1<C>> for ProofVar<C>
174where
175 C: CurveGroup,
176 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
177 <C as Group>::ScalarField: Absorb,
178{
179 fn new_variable<T: Borrow<NIMFSProof<C>>>(
180 cs: impl Into<Namespace<CF1<C>>>,
181 f: impl FnOnce() -> Result<T, SynthesisError>,
182 mode: AllocationMode,
183 ) -> Result<Self, SynthesisError> {
184 f().and_then(|val| {
185 let cs = cs.into();
186
187 let sc_proof = IOPProofVar::<C>::new_variable(
188 cs.clone(),
189 || Ok(val.borrow().sc_proof.clone()),
190 mode,
191 )?;
192 let sigmas: Vec<Vec<FpVar<CF1<C>>>> = val
193 .borrow()
194 .sigmas_thetas
195 .0
196 .iter()
197 .map(|sigmas_i| Vec::new_variable(cs.clone(), || Ok(sigmas_i.clone()), mode))
198 .collect::<Result<Vec<Vec<FpVar<CF1<C>>>>, SynthesisError>>()?;
199 let thetas: Vec<Vec<FpVar<CF1<C>>>> = val
200 .borrow()
201 .sigmas_thetas
202 .1
203 .iter()
204 .map(|thetas_i| Vec::new_variable(cs.clone(), || Ok(thetas_i.clone()), mode))
205 .collect::<Result<Vec<Vec<FpVar<CF1<C>>>>, SynthesisError>>()?;
206
207 Ok(Self {
208 sc_proof,
209 sigmas_thetas: (sigmas.clone(), thetas.clone()),
210 })
211 })
212 }
213}
214
215pub struct NIMFSGadget<C: CurveGroup> {
216 _c: PhantomData<C>,
217}
218impl<C: CurveGroup> NIMFSGadget<C>
219where
220 <C as CurveGroup>::BaseField: PrimeField,
221{
222 /// Runs (in-circuit) the NIMFS.V, which outputs the new folded LCCCS instance together with
223 /// the rho_bits, which will be used in other parts of the AugmentedFCircuit
224 #[allow(clippy::type_complexity)]
225 pub fn verify(
226 cs: ConstraintSystemRef<CF1<C>>,
227 // only used the CCS params, not the matrices
228 ccs: &CCS<C::ScalarField>,
229 mut transcript: impl TranscriptVar<C::ScalarField>,
230
231 running_instances: &[LCCCSVar<C>],
232 new_instances: &[CCCSVar<C>],
233 proof: ProofVar<C>,
234 enabled: Boolean<C::ScalarField>,
235 ) -> Result<(LCCCSVar<C>, Vec<Boolean<CF1<C>>>), SynthesisError> {
236 // absorb instances to transcript
237 for U_i in running_instances {
238 let v = [
239 U_i.C.to_constraint_field()?,
240 vec![U_i.u.clone()],
241 U_i.x.clone(),
242 U_i.r_x.clone(),
243 U_i.v.clone(),
244 ]
245 .concat();
246 transcript.absorb_vec(&v)?;
247 }
248 for u_i in new_instances {
249 let v = [u_i.C.to_constraint_field()?, u_i.x.clone()].concat();
250 transcript.absorb_vec(&v)?;
251 }
252
253 // get the challenges
254 let gamma_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"gamma");
255 let gamma_scalar: FpVar<CF1<C>> =
256 FpVar::<CF1<C>>::new_constant(cs.clone(), gamma_scalar_raw)?;
257 transcript.absorb(gamma_scalar)?;
258 let gamma: FpVar<CF1<C>> = transcript.get_challenge()?;
259
260 let beta_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"beta");
261 let beta_scalar: FpVar<CF1<C>> =
262 FpVar::<CF1<C>>::new_constant(cs.clone(), beta_scalar_raw)?;
263 transcript.absorb(beta_scalar)?;
264 let beta: Vec<FpVar<CF1<C>>> = transcript.get_challenges(ccs.s)?;
265
266 let vp_aux_info_raw = VPAuxInfo::<C::ScalarField> {
267 max_degree: ccs.d + 1,
268 num_variables: ccs.s,
269 phantom: PhantomData::<C::ScalarField>,
270 };
271 let vp_aux_info = VPAuxInfoVar::<CF1<C>>::new_witness(cs.clone(), || Ok(vp_aux_info_raw))?;
272
273 // sumcheck
274 // first, compute the expected sumcheck sum: \sum gamma^j v_j
275 let mut sum_v_j_gamma = FpVar::<CF1<C>>::zero();
276 let mut gamma_j = FpVar::<C::ScalarField>::one();
277 for running_instance in running_instances.iter() {
278 for j in 0..running_instance.v.len() {
279 gamma_j *= gamma.clone();
280 sum_v_j_gamma += running_instance.v[j].clone() * gamma_j.clone();
281 }
282 }
283
284 // verify the interactive part of the sumcheck
285 let (e_vars, r_vars) = SumCheckVerifierGadget::<C>::verify(
286 &proof.sc_proof,
287 &vp_aux_info,
288 &mut transcript,
289 enabled.clone(),
290 )?;
291
292 // extract the randomness from the sumcheck
293 let r_x_prime = r_vars.clone();
294
295 // verify the claim c
296 let computed_c = compute_c_gadget(
297 cs.clone(),
298 ccs,
299 proof.sigmas_thetas.0.clone(), // sigmas
300 proof.sigmas_thetas.1.clone(), // thetas
301 gamma,
302 beta,
303 running_instances
304 .iter()
305 .map(|lcccs| lcccs.r_x.clone())
306 .collect(),
307 r_x_prime.clone(),
308 )?;
309 computed_c.conditional_enforce_equal(&e_vars[e_vars.len() - 1], &enabled)?;
310
311 // get the folding challenge
312 let rho_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"rho");
313 let rho_scalar: FpVar<CF1<C>> = FpVar::<CF1<C>>::new_constant(cs.clone(), rho_scalar_raw)?;
314 transcript.absorb(rho_scalar)?;
315 let rho_bits: Vec<Boolean<CF1<C>>> = transcript.get_challenge_nbits(N_BITS_RO)?;
316 let rho = Boolean::le_bits_to_fp_var(&rho_bits)?;
317
318 // return the folded instance, together with the rho_bits so they can be used in other
319 // parts of the AugmentedFCircuit
320 Ok((
321 Self::fold(
322 running_instances,
323 new_instances,
324 proof.sigmas_thetas,
325 r_x_prime,
326 rho,
327 )?,
328 rho_bits,
329 ))
330 }
331
332 /// Runs (in-circuit) the verifier side of the fold, computing the new folded LCCCS instance
333 #[allow(clippy::type_complexity)]
334 fn fold(
335 lcccs: &[LCCCSVar<C>],
336 cccs: &[CCCSVar<C>],
337 sigmas_thetas: (Vec<Vec<FpVar<CF1<C>>>>, Vec<Vec<FpVar<CF1<C>>>>),
338 r_x_prime: Vec<FpVar<CF1<C>>>,
339 rho: FpVar<CF1<C>>,
340 ) -> Result<LCCCSVar<C>, SynthesisError> {
341 let (sigmas, thetas) = (sigmas_thetas.0.clone(), sigmas_thetas.1.clone());
342 let mut u_folded: FpVar<CF1<C>> = FpVar::zero();
343 let mut x_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); lcccs[0].x.len()];
344 let mut v_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); sigmas[0].len()];
345
346 let mut rho_i = FpVar::one();
347 for i in 0..(lcccs.len() + cccs.len()) {
348 let u: FpVar<CF1<C>>;
349 let x: Vec<FpVar<CF1<C>>>;
350 let v: Vec<FpVar<CF1<C>>>;
351 if i < lcccs.len() {
352 u = lcccs[i].u.clone();
353 x = lcccs[i].x.clone();
354 v = sigmas[i].clone();
355 } else {
356 u = FpVar::one();
357 x = cccs[i - lcccs.len()].x.clone();
358 v = thetas[i - lcccs.len()].clone();
359 }
360
361 u_folded += rho_i.clone() * u;
362 x_folded = x_folded
363 .iter()
364 .zip(
365 x.iter()
366 .map(|x_i| x_i * rho_i.clone())
367 .collect::<Vec<FpVar<CF1<C>>>>(),
368 )
369 .map(|(a_i, b_i)| a_i + b_i)
370 .collect();
371
372 v_folded = v_folded
373 .iter()
374 .zip(
375 v.iter()
376 .map(|x_i| x_i * rho_i.clone())
377 .collect::<Vec<FpVar<CF1<C>>>>(),
378 )
379 .map(|(a_i, b_i)| a_i + b_i)
380 .collect();
381
382 rho_i *= rho.clone();
383 }
384
385 Ok(LCCCSVar::<C> {
386 C: lcccs[0].C.clone(), // WIP this will come from the cyclefold circuit
387 u: u_folded,
388 x: x_folded,
389 r_x: r_x_prime,
390 v: v_folded,
391 })
392 }
393}
394
395/// Computes c from the step 5 in section 5 of HyperNova, adapted to multiple LCCCS & CCCS
396/// instances:
397/// $$
398/// c = \sum_{i \in [\mu]} \left(\sum_{j \in [t]} \gamma^{i \cdot t + j} \cdot e_i \cdot \sigma_{i,j} \right)
399/// + \sum_{k \in [\nu]} \gamma^{\mu \cdot t+k} \cdot e_k \cdot \left( \sum_{i=1}^q c_i \cdot \prod_{j \in S_i}
400/// \theta_{k,j} \right)
401/// $$
402#[allow(clippy::too_many_arguments)]
403fn compute_c_gadget<F: PrimeField>(
404 cs: ConstraintSystemRef<F>,
405 ccs: &CCS<F>,
406 vec_sigmas: Vec<Vec<FpVar<F>>>,
407 vec_thetas: Vec<Vec<FpVar<F>>>,
408 gamma: FpVar<F>,
409 beta: Vec<FpVar<F>>,
410 vec_r_x: Vec<Vec<FpVar<F>>>,
411 vec_r_x_prime: Vec<FpVar<F>>,
412) -> Result<FpVar<F>, SynthesisError> {
413 let mut e_lcccs = Vec::new();
414 for r_x in vec_r_x.iter() {
415 e_lcccs.push(EqEvalGadget::eq_eval(r_x, &vec_r_x_prime)?);
416 }
417
418 let mut c = FpVar::<F>::zero();
419 let mut current_gamma = FpVar::<F>::one();
420 for i in 0..vec_sigmas.len() {
421 for j in 0..ccs.t {
422 c += current_gamma.clone() * e_lcccs[i].clone() * vec_sigmas[i][j].clone();
423 current_gamma *= gamma.clone();
424 }
425 }
426
427 let ccs_c = Vec::<FpVar<F>>::new_constant(cs.clone(), ccs.c.clone())?;
428 let e_k = EqEvalGadget::eq_eval(&beta, &vec_r_x_prime)?;
429 #[allow(clippy::needless_range_loop)]
430 for k in 0..vec_thetas.len() {
431 let mut sum = FpVar::<F>::zero();
432 for i in 0..ccs.q {
433 let mut prod = FpVar::<F>::one();
434 for j in ccs.S[i].clone() {
435 prod *= vec_thetas[k][j].clone();
436 }
437 sum += ccs_c[i].clone() * prod;
438 }
439 c += current_gamma.clone() * e_k.clone() * sum;
440 current_gamma *= gamma.clone();
441 }
442 Ok(c)
443}
444
445#[derive(Debug, Clone)]
446pub struct AugmentedFCircuit<
447 C1: CurveGroup,
448 C2: CurveGroup,
449 GC2: CurveVar<C2, CF2<C2>>,
450 FC: FCircuit<CF1<C1>>,
451> where
452 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
453{
454 pub _c2: PhantomData<C2>,
455 pub _gc2: PhantomData<GC2>,
456 pub poseidon_config: PoseidonConfig<CF1<C1>>,
457 pub ccs: CCS<C1::ScalarField>, // CCS of the AugmentedFCircuit
458 pub i: Option<CF1<C1>>,
459 pub i_usize: Option<usize>,
460 pub z_0: Option<Vec<C1::ScalarField>>,
461 pub z_i: Option<Vec<C1::ScalarField>>,
462 pub external_inputs: Option<Vec<C1::ScalarField>>,
463 pub u_i_C: Option<C1>, // u_i.C
464 pub U_i: Option<LCCCS<C1>>,
465 pub U_i1_C: Option<C1>, // U_{i+1}.C
466 pub F: FC, // F circuit
467 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
468 pub nimfs_proof: Option<NIMFSProof<C1>>,
469
470 // cyclefold verifier on C1
471 pub cf_u_i_cmW: Option<C2>, // input, cf_u_i.cmW
472 pub cf_U_i: Option<CommittedInstance<C2>>, // input, RelaxedR1CS CycleFold instance
473 pub cf_x: Option<CF1<C1>>, // public input (cf_u_{i+1}.x[1])
474 pub cf_cmT: Option<C2>,
475}
476
477impl<C1, C2, GC2, FC> AugmentedFCircuit<C1, C2, GC2, FC>
478where
479 C1: CurveGroup,
480 C2: CurveGroup,
481 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
482 FC: FCircuit<CF1<C1>>,
483 <C1 as CurveGroup>::BaseField: PrimeField,
484 <C2 as CurveGroup>::BaseField: PrimeField,
485 <C1 as Group>::ScalarField: Absorb,
486 <C2 as Group>::ScalarField: Absorb,
487 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
488 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
489{
490 pub fn default(
491 poseidon_config: &PoseidonConfig<CF1<C1>>,
492 F_circuit: FC,
493 ccs: CCS<C1::ScalarField>,
494 ) -> Self {
495 Self {
496 _c2: PhantomData,
497 _gc2: PhantomData,
498 poseidon_config: poseidon_config.clone(),
499 ccs,
500 i: None,
501 i_usize: None,
502 z_0: None,
503 z_i: None,
504 external_inputs: None,
505 u_i_C: None,
506 U_i: None,
507 U_i1_C: None,
508 F: F_circuit,
509 x: None,
510 nimfs_proof: None,
511 cf_u_i_cmW: None,
512 cf_U_i: None,
513 cf_x: None,
514 cf_cmT: None,
515 }
516 }
517
518 pub fn empty(
519 poseidon_config: &PoseidonConfig<CF1<C1>>,
520 F_circuit: FC,
521 ccs: Option<CCS<C1::ScalarField>>,
522 ) -> Result<Self, Error> {
523 let initial_ccs = CCS {
524 // m, n, s, s_prime and M will be overwritten by the `upper_bound_ccs' method
525 m: 0,
526 n: 0,
527 l: 2, // io_len
528 s: 1,
529 s_prime: 1,
530 t: 3, // note: this is only supports R1CS for the moment
531 q: 2,
532 d: 2,
533 S: vec![vec![0, 1], vec![2]],
534 c: vec![C1::ScalarField::one(), C1::ScalarField::one().neg()],
535 M: vec![],
536 };
537 let mut augmented_f_circuit = Self::default(poseidon_config, F_circuit, initial_ccs);
538 if ccs.is_some() {
539 augmented_f_circuit.ccs = ccs.unwrap();
540 } else {
541 augmented_f_circuit.ccs = augmented_f_circuit.upper_bound_ccs()?;
542 }
543 Ok(augmented_f_circuit)
544 }
545
546 /// This method computes the CCS parameters. This is used because there is a circular
547 /// dependency between the AugmentedFCircuit CCS and the CCS parameters m & n & s & s'.
548 /// For a stable FCircuit circuit, the CCS parameters can be computed in advance and can be
549 /// feed in as parameter for the AugmentedFCircuit::empty method to avoid computing them there.
550 pub fn upper_bound_ccs(&self) -> Result<CCS<C1::ScalarField>, Error> {
551 let r1cs = get_r1cs_from_cs::<CF1<C1>>(self.clone()).unwrap();
552 let ccs = CCS::from_r1cs(r1cs.clone());
553
554 let z_0 = vec![C1::ScalarField::zero(); self.F.state_len()];
555 let W_i = Witness::<C1::ScalarField>::dummy(&ccs);
556 let U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
557 let w_i = W_i.clone();
558 let u_i = CCCS::<C1>::dummy(ccs.l);
559
560 let mut transcript_p: PoseidonTranscript<C1> =
561 PoseidonTranscript::<C1>::new(&self.poseidon_config.clone());
562 let (nimfs_proof, U_i1, _, _) = NIMFS::<C1, PoseidonTranscript<C1>>::prove(
563 &mut transcript_p,
564 &ccs,
565 &[U_i.clone()],
566 &[u_i.clone()],
567 &[W_i.clone()],
568 &[w_i.clone()],
569 )?;
570
571 let augmented_f_circuit = Self {
572 _c2: PhantomData,
573 _gc2: PhantomData,
574 poseidon_config: self.poseidon_config.clone(),
575 ccs: ccs.clone(),
576 i: Some(C1::ScalarField::zero()),
577 i_usize: Some(0),
578 z_0: Some(z_0.clone()),
579 z_i: Some(z_0.clone()),
580 external_inputs: Some(vec![]),
581 u_i_C: Some(u_i.C),
582 U_i: Some(U_i.clone()),
583 U_i1_C: Some(U_i1.C),
584 F: self.F.clone(),
585 x: Some(C1::ScalarField::zero()),
586 nimfs_proof: Some(nimfs_proof),
587 // cyclefold values
588 cf_u_i_cmW: None,
589 cf_U_i: None,
590 cf_x: None,
591 cf_cmT: None,
592 };
593
594 Ok(augmented_f_circuit.compute_cs_ccs()?.1)
595 }
596
597 /// Returns the cs (ConstraintSystem) and the CCS out of the AugmentedFCircuit
598 #[allow(clippy::type_complexity)]
599 fn compute_cs_ccs(
600 &self,
601 ) -> Result<(ConstraintSystem<C1::ScalarField>, CCS<C1::ScalarField>), Error> {
602 let cs = ConstraintSystem::<C1::ScalarField>::new_ref();
603 self.clone().generate_constraints(cs.clone())?;
604 cs.finalize();
605 let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?;
606 let r1cs = extract_r1cs::<C1::ScalarField>(&cs);
607 let ccs = CCS::from_r1cs(r1cs.clone());
608
609 Ok((cs, ccs))
610 }
611}
612
613impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
614where
615 C1: CurveGroup,
616 C2: CurveGroup,
617 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
618 FC: FCircuit<CF1<C1>>,
619 <C1 as CurveGroup>::BaseField: PrimeField,
620 <C2 as CurveGroup>::BaseField: PrimeField,
621 <C1 as Group>::ScalarField: Absorb,
622 <C2 as Group>::ScalarField: Absorb,
623 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
624 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
625{
626 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
627 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
628 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
629 })?;
630 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
631 Ok(self
632 .z_0
633 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
634 })?;
635 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
636 Ok(self
637 .z_i
638 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
639 })?;
640 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
641 Ok(self
642 .external_inputs
643 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
644 })?;
645
646 let U_dummy = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
647
648 let U_i =
649 LCCCSVar::<C1>::new_witness(cs.clone(), || Ok(self.U_i.unwrap_or(U_dummy.clone())))?;
650 let U_i1_C = NonNativeAffineVar::new_witness(cs.clone(), || {
651 Ok(self.U_i1_C.unwrap_or_else(C1::zero))
652 })?;
653 let mu = 1; // Note: at this commit, only 2-to-1 instance fold is supported
654 let nu = 1;
655 let nimfs_proof_dummy = NIMFSProof::<C1>::dummy(&self.ccs, mu, nu);
656 let nimfs_proof = ProofVar::<C1>::new_witness(cs.clone(), || {
657 Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy))
658 })?;
659
660 let cf_u_dummy = CommittedInstance::dummy(CF_IO_LEN);
661 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
662 Ok(self.cf_U_i.unwrap_or(cf_u_dummy.clone()))
663 })?;
664 let cf_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf_cmT.unwrap_or_else(C2::zero)))?;
665
666 let crh_params = CRHParametersVar::<C1::ScalarField>::new_constant(
667 cs.clone(),
668 self.poseidon_config.clone(),
669 )?;
670
671 // get z_{i+1} from the F circuit
672 let i_usize = self.i_usize.unwrap_or(0);
673 let z_i1 =
674 self.F
675 .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?;
676
677 let is_basecase = i.is_zero()?;
678 let is_not_basecase = is_basecase.not();
679
680 // Primary Part
681 // P.1. Compute u_i.x
682 // u_i.x[0] = H(i, z_0, z_i, U_i)
683 let (u_i_x, _) = U_i
684 .clone()
685 .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
686 // u_i.x[1] = H(cf_U_i)
687 let (cf_u_i_x, cf_U_i_vec) = cf_U_i.clone().hash(&crh_params)?;
688
689 // P.2. Construct u_i
690 let u_i = CCCSVar::<C1> {
691 // u_i.C is provided by the prover as witness
692 C: NonNativeAffineVar::<C1>::new_witness(cs.clone(), || {
693 Ok(self.u_i_C.unwrap_or(C1::zero()))
694 })?,
695 // u_i.x is computed in step 1
696 x: vec![u_i_x, cf_u_i_x],
697 };
698
699 // P.3. NIMFS.verify, obtains U_{i+1} by folding [U_i] & [u_i].
700 // Notice that NIMFSGadget::fold_committed_instance does not fold C. We set `U_i1.C` to
701 // unconstrained witnesses `U_i1_C` respectively. Its correctness will be checked on the
702 // other curve.
703 let transcript =
704 PoseidonTranscriptVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
705 let (mut U_i1, rho_bits) = NIMFSGadget::<C1>::verify(
706 cs.clone(),
707 &self.ccs.clone(),
708 transcript,
709 &[U_i.clone()],
710 &[u_i.clone()],
711 nimfs_proof,
712 is_not_basecase.clone(),
713 )?;
714 U_i1.C = U_i1_C;
715
716 // P.4.a compute and check the first output of F'
717 let (u_i1_x, _) = U_i1.clone().hash(
718 &crh_params,
719 i + FpVar::<CF1<C1>>::one(),
720 z_0.clone(),
721 z_i1.clone(),
722 )?;
723 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(C1::ScalarField::zero())))?;
724 x.enforce_equal(&u_i1_x)?;
725
726 // convert rho_bits to a `NonNativeFieldVar`
727 let rho_nonnat = {
728 let mut bits = rho_bits;
729 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
730 NonNativeUintVar::from(&bits)
731 };
732
733 // CycleFold part
734 // C.1. Compute cf1_u_i.x and cf2_u_i.x
735 let cf_x = vec![
736 rho_nonnat, U_i.C.x, U_i.C.y, u_i.C.x, u_i.C.y, U_i1.C.x, U_i1.C.y,
737 ];
738
739 // ensure that cf_u has as public inputs the C from main instances U_i, u_i, U_i+1
740 // coordinates of the commitments.
741 // C.2. Construct `cf_u_i`
742 let cf_u_i = CycleFoldCommittedInstanceVar {
743 // cf1_u_i.cmE = 0. Notice that we enforce cmE to be equal to 0 since it is allocated
744 // as 0.
745 cmE: GC2::zero(),
746 // cf1_u_i.u = 1
747 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
748 // cf_u_i.cmW is provided by the prover as witness
749 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf_u_i_cmW.unwrap_or(C2::zero())))?,
750 // cf_u_i.x is computed in step 1
751 x: cf_x,
752 };
753
754 // C.3. nifs.verify (fold_committed_instance), obtains cf_U_{i+1} by folding cf_u_i & cf_U_i.
755 // compute cf_r = H(cf_u_i, cf_U_i, cf_cmT)
756 // cf_r_bits is denoted by rho* in the paper.
757 let cf_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
758 cs.clone(),
759 &self.poseidon_config,
760 cf_U_i_vec,
761 cf_u_i.clone(),
762 cf_cmT.clone(),
763 )?;
764 // Convert cf_r_bits to a `NonNativeFieldVar`
765 let cf_r_nonnat = {
766 let mut bits = cf_r_bits.clone();
767 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
768 NonNativeUintVar::from(&bits)
769 };
770 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
771 let cf_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
772 cf_r_bits,
773 cf_r_nonnat,
774 cf_cmT,
775 cf_U_i,
776 cf_u_i,
777 )?;
778
779 // Back to Primary Part
780 // P.4.b compute and check the second output of F'
781 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
782 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
783 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&crh_params)?;
784 let (cf_u_i1_x_base, _) =
785 CycleFoldCommittedInstanceVar::new_constant(cs.clone(), cf_u_dummy)?
786 .hash(&crh_params)?;
787 let cf_x = FpVar::new_input(cs.clone(), || {
788 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
789 })?;
790 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
791
792 Ok(())
793 }
794}
795
796#[cfg(test)]
797mod tests {
798 use ark_bn254::{constraints::GVar, Fq, Fr, G1Projective as Projective};
799 use ark_ff::BigInteger;
800 use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
801 use ark_r1cs_std::{alloc::AllocVar, fields::fp::FpVar, R1CSVar};
802 use ark_std::{test_rng, UniformRand};
803 use std::time::Instant;
804
805 use super::*;
806 use crate::{
807 ccs::{
808 r1cs::extract_w_x,
809 tests::{get_test_ccs, get_test_z},
810 CCS,
811 },
812 commitment::{pedersen::Pedersen, CommitmentScheme},
813 folding::{
814 circuits::cyclefold::{fold_cyclefold_circuit, CycleFoldCircuit},
815 hypernova::{
816 nimfs::NIMFS,
817 utils::{compute_c, compute_sigmas_thetas},
818 Witness,
819 },
820 nova::{
821 get_cm_coordinates, traits::NovaR1CS, CommittedInstance, Witness as NovaWitness,
822 },
823 },
824 frontend::tests::CubicFCircuit,
825 transcript::{
826 poseidon::{poseidon_canonical_config, PoseidonTranscript, PoseidonTranscriptVar},
827 Transcript,
828 },
829 };
830
831 #[test]
832 pub fn test_compute_c_gadget() {
833 // number of LCCCS & CCCS instances to fold in a single step
834 let mu = 32;
835 let nu = 42;
836
837 let mut z_lcccs = Vec::new();
838 for i in 0..mu {
839 let z = get_test_z(i + 3);
840 z_lcccs.push(z);
841 }
842 let mut z_cccs = Vec::new();
843 for i in 0..nu {
844 let z = get_test_z(i + 3);
845 z_cccs.push(z);
846 }
847
848 let ccs: CCS<Fr> = get_test_ccs();
849
850 let mut rng = test_rng();
851 let gamma: Fr = Fr::rand(&mut rng);
852 let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
853 let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
854
855 let (pedersen_params, _) =
856 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
857
858 // Create the LCCCS instances out of z_lcccs
859 let mut lcccs_instances = Vec::new();
860 for z_i in z_lcccs.iter() {
861 let (inst, _) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap();
862 lcccs_instances.push(inst);
863 }
864 // Create the CCCS instance out of z_cccs
865 let mut cccs_instances = Vec::new();
866 for z_i in z_cccs.iter() {
867 let (inst, _) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap();
868 cccs_instances.push(inst);
869 }
870
871 let sigmas_thetas = compute_sigmas_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime).unwrap();
872
873 let expected_c = compute_c(
874 &ccs,
875 &sigmas_thetas,
876 gamma,
877 &beta,
878 &lcccs_instances
879 .iter()
880 .map(|lcccs| lcccs.r_x.clone())
881 .collect(),
882 &r_x_prime,
883 )
884 .unwrap();
885
886 let cs = ConstraintSystem::<Fr>::new_ref();
887 let mut vec_sigmas = Vec::new();
888 let mut vec_thetas = Vec::new();
889 for sigmas in sigmas_thetas.0 {
890 vec_sigmas
891 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap());
892 }
893 for thetas in sigmas_thetas.1 {
894 vec_thetas
895 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap());
896 }
897 let vec_r_x: Vec<Vec<FpVar<Fr>>> = lcccs_instances
898 .iter()
899 .map(|lcccs| {
900 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap()
901 })
902 .collect();
903 let vec_r_x_prime =
904 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap();
905 let gamma_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(gamma)).unwrap();
906 let beta_var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap();
907
908 let computed_c = compute_c_gadget(
909 cs.clone(),
910 &ccs,
911 vec_sigmas,
912 vec_thetas,
913 gamma_var,
914 beta_var,
915 vec_r_x,
916 vec_r_x_prime,
917 )
918 .unwrap();
919
920 assert_eq!(expected_c, computed_c.value().unwrap());
921 }
922
923 /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step,
924 /// to verify the folding in the NIMFSGadget circuit
925 #[test]
926 pub fn test_nimfs_gadget_verify() {
927 let mut rng = test_rng();
928
929 // Create a basic CCS circuit
930 let ccs = get_test_ccs::<Fr>();
931 let (pedersen_params, _) =
932 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
933
934 let mu = 32;
935 let nu = 42;
936
937 // Generate a mu LCCCS & nu CCCS satisfying witness
938 let mut z_lcccs = Vec::new();
939 for i in 0..mu {
940 let z = get_test_z(i + 3);
941 z_lcccs.push(z);
942 }
943 let mut z_cccs = Vec::new();
944 for i in 0..nu {
945 let z = get_test_z(nu + i + 3);
946 z_cccs.push(z);
947 }
948
949 // Create the LCCCS instances out of z_lcccs
950 let mut lcccs_instances = Vec::new();
951 let mut w_lcccs = Vec::new();
952 for z_i in z_lcccs.iter() {
953 let (running_instance, w) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap();
954 lcccs_instances.push(running_instance);
955 w_lcccs.push(w);
956 }
957 // Create the CCCS instance out of z_cccs
958 let mut cccs_instances = Vec::new();
959 let mut w_cccs = Vec::new();
960 for z_i in z_cccs.iter() {
961 let (new_instance, w) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap();
962 cccs_instances.push(new_instance);
963 w_cccs.push(w);
964 }
965
966 // Prover's transcript
967 let poseidon_config = poseidon_canonical_config::<Fr>();
968 let mut transcript_p: PoseidonTranscript<Projective> =
969 PoseidonTranscript::<Projective>::new(&poseidon_config);
970
971 // Run the prover side of the multifolding
972 let (proof, folded_lcccs, folded_witness, _) =
973 NIMFS::<Projective, PoseidonTranscript<Projective>>::prove(
974 &mut transcript_p,
975 &ccs,
976 &lcccs_instances,
977 &cccs_instances,
978 &w_lcccs,
979 &w_cccs,
980 )
981 .unwrap();
982
983 // Verifier's transcript
984 let mut transcript_v: PoseidonTranscript<Projective> =
985 PoseidonTranscript::<Projective>::new(&poseidon_config);
986
987 // Run the verifier side of the multifolding
988 let folded_lcccs_v = NIMFS::<Projective, PoseidonTranscript<Projective>>::verify(
989 &mut transcript_v,
990 &ccs,
991 &lcccs_instances,
992 &cccs_instances,
993 proof.clone(),
994 )
995 .unwrap();
996 assert_eq!(folded_lcccs, folded_lcccs_v);
997
998 // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
999 folded_lcccs
1000 .check_relation(&pedersen_params, &ccs, &folded_witness)
1001 .unwrap();
1002
1003 // allocate circuit inputs
1004 let cs = ConstraintSystem::<Fr>::new_ref();
1005 let lcccs_instancesVar =
1006 Vec::<LCCCSVar<Projective>>::new_witness(cs.clone(), || Ok(lcccs_instances.clone()))
1007 .unwrap();
1008 let cccs_instancesVar =
1009 Vec::<CCCSVar<Projective>>::new_witness(cs.clone(), || Ok(cccs_instances.clone()))
1010 .unwrap();
1011 let proofVar =
1012 ProofVar::<Projective>::new_witness(cs.clone(), || Ok(proof.clone())).unwrap();
1013 let transcriptVar = PoseidonTranscriptVar::<Fr>::new(cs.clone(), &poseidon_config);
1014
1015 let enabled = Boolean::<Fr>::new_witness(cs.clone(), || Ok(true)).unwrap();
1016 let (folded_lcccsVar, _) = NIMFSGadget::<Projective>::verify(
1017 cs.clone(),
1018 &ccs,
1019 transcriptVar,
1020 &lcccs_instancesVar,
1021 &cccs_instancesVar,
1022 proofVar,
1023 enabled,
1024 )
1025 .unwrap();
1026 assert!(cs.is_satisfied().unwrap());
1027 assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u);
1028 }
1029
1030 /// test that checks the native LCCCS.hash vs the R1CS constraints version
1031 #[test]
1032 pub fn test_lcccs_hash() {
1033 let mut rng = test_rng();
1034 let poseidon_config = poseidon_canonical_config::<Fr>();
1035
1036 let ccs = get_test_ccs();
1037 let z1 = get_test_z::<Fr>(3);
1038
1039 let (pedersen_params, _) =
1040 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1041
1042 let i = Fr::from(3_u32);
1043 let z_0 = vec![Fr::from(3_u32)];
1044 let z_i = vec![Fr::from(3_u32)];
1045 let (lcccs, _) = ccs.to_lcccs(&mut rng, &pedersen_params, &z1).unwrap();
1046 let h = lcccs
1047 .clone()
1048 .hash(&poseidon_config, i, z_0.clone(), z_i.clone())
1049 .unwrap();
1050
1051 let cs = ConstraintSystem::<Fr>::new_ref();
1052
1053 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
1054 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
1055 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
1056 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
1057 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
1058 let (hVar, _) = lcccsVar
1059 .clone()
1060 .hash(&crh_params, iVar.clone(), z_0Var.clone(), z_iVar.clone())
1061 .unwrap();
1062 assert!(cs.is_satisfied().unwrap());
1063
1064 // check that the natively computed and in-circuit computed hashes match
1065 assert_eq!(hVar.value().unwrap(), h);
1066 }
1067
1068 #[test]
1069 pub fn test_augmented_f_circuit() {
1070 let mut rng = test_rng();
1071 let poseidon_config = poseidon_canonical_config::<Fr>();
1072
1073 let start = Instant::now();
1074 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
1075 let mut augmented_f_circuit = AugmentedFCircuit::<
1076 Projective,
1077 Projective2,
1078 GVar2,
1079 CubicFCircuit<Fr>,
1080 >::empty(&poseidon_config, F_circuit, None)
1081 .unwrap();
1082 let ccs = augmented_f_circuit.ccs.clone();
1083 println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed());
1084 println!("CCS m x n: {} x {}", ccs.m, ccs.n);
1085
1086 // CycleFold circuit
1087 let cs2 = ConstraintSystem::<Fq>::new_ref();
1088 let cf_circuit = CycleFoldCircuit::<Projective, GVar>::empty();
1089 cf_circuit.generate_constraints(cs2.clone()).unwrap();
1090 cs2.finalize();
1091 let cs2 = cs2
1092 .into_inner()
1093 .ok_or(Error::NoInnerConstraintSystem)
1094 .unwrap();
1095 let cf_r1cs = extract_r1cs::<Fq>(&cs2);
1096
1097 let (pedersen_params, _) =
1098 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1099 let (cf_pedersen_params, _) =
1100 Pedersen::<Projective2>::setup(&mut rng, cf_r1cs.A.n_cols - cf_r1cs.l - 1).unwrap();
1101
1102 // first step
1103 let z_0 = vec![Fr::from(3_u32)];
1104 let mut z_i = z_0.clone();
1105
1106 // prepare the dummy instances
1107 let W_dummy = Witness::<Fr>::new(vec![Fr::zero(); ccs.n - ccs.l - 1]);
1108 let U_dummy = LCCCS::<Projective>::dummy(ccs.l, ccs.t, ccs.s);
1109 let w_dummy = W_dummy.clone();
1110 let u_dummy = CCCS::<Projective>::dummy(ccs.l);
1111 let (cf_w_dummy, cf_u_dummy): (NovaWitness<Projective2>, CommittedInstance<Projective2>) =
1112 cf_r1cs.dummy_instance();
1113
1114 // set the initial dummy instances
1115 let mut W_i = W_dummy.clone();
1116 let mut U_i = U_dummy.clone();
1117 let mut w_i = w_dummy.clone();
1118 let mut u_i = u_dummy.clone();
1119 let mut cf_W_i = cf_w_dummy.clone();
1120 let mut cf_U_i = cf_u_dummy.clone();
1121 u_i.x = vec![
1122 U_i.hash(&poseidon_config, Fr::zero(), z_0.clone(), z_i.clone())
1123 .unwrap(),
1124 cf_U_i.hash_cyclefold(&poseidon_config).unwrap(),
1125 ];
1126
1127 let n_steps: usize = 4;
1128 let mut iFr = Fr::zero();
1129 for i in 0..n_steps {
1130 let start = Instant::now();
1131 let mut transcript_p: PoseidonTranscript<Projective> =
1132 PoseidonTranscript::<Projective>::new(&poseidon_config.clone());
1133 let (nimfs_proof, U_i1, W_i1, rho_bits) =
1134 NIMFS::<Projective, PoseidonTranscript<Projective>>::prove(
1135 &mut transcript_p,
1136 &ccs,
1137 &[U_i.clone()],
1138 &[u_i.clone()],
1139 &[W_i.clone()],
1140 &[w_i.clone()],
1141 )
1142 .unwrap();
1143
1144 // sanity check: check the folded instance relation
1145 U_i1.check_relation(&pedersen_params, &ccs, &W_i1).unwrap();
1146
1147 let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap();
1148 let u_i1_x = U_i1
1149 .hash(&poseidon_config, iFr + Fr::one(), z_0.clone(), z_i1.clone())
1150 .unwrap();
1151
1152 if i == 0 {
1153 // hash the initial (dummy) CycleFold instance, which is used as the 2nd public
1154 // input in the AugmentedFCircuit
1155 let cf_u_i1_x = cf_U_i.hash_cyclefold(&poseidon_config).unwrap();
1156
1157 augmented_f_circuit =
1158 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1159 _c2: PhantomData,
1160 _gc2: PhantomData,
1161 poseidon_config: poseidon_config.clone(),
1162 ccs: ccs.clone(),
1163 i: Some(iFr),
1164 i_usize: Some(i),
1165 z_0: Some(z_0.clone()),
1166 z_i: Some(z_i.clone()),
1167 external_inputs: Some(vec![]),
1168 u_i_C: Some(u_i.C),
1169 U_i: Some(U_i.clone()),
1170 U_i1_C: Some(U_i1.C),
1171 F: F_circuit,
1172 x: Some(u_i1_x),
1173 nimfs_proof: Some(nimfs_proof),
1174
1175 // cyclefold values
1176 cf_u_i_cmW: None,
1177 cf_U_i: None,
1178 cf_x: Some(cf_u_i1_x),
1179 cf_cmT: None,
1180 };
1181 } else {
1182 let rho_Fq = Fq::from_bigint(BigInteger::from_bits_le(&rho_bits)).unwrap();
1183 // CycleFold part:
1184 // get the vector used as public inputs 'x' in the CycleFold circuit
1185 // cyclefold circuit for cmW
1186 let cf_u_i_x = [
1187 vec![rho_Fq],
1188 get_cm_coordinates(&U_i.C),
1189 get_cm_coordinates(&u_i.C),
1190 get_cm_coordinates(&U_i1.C),
1191 ]
1192 .concat();
1193
1194 let cf_circuit = CycleFoldCircuit::<Projective, GVar> {
1195 _gc: PhantomData,
1196 r_bits: Some(rho_bits.clone()),
1197 p1: Some(U_i.clone().C),
1198 p2: Some(u_i.clone().C),
1199 x: Some(cf_u_i_x.clone()),
1200 };
1201
1202 let (_cf_w_i, cf_u_i, cf_W_i1, cf_U_i1, cf_cmT, _) = fold_cyclefold_circuit::<
1203 Projective,
1204 GVar,
1205 Projective2,
1206 GVar2,
1207 CubicFCircuit<Fr>,
1208 Pedersen<Projective>,
1209 Pedersen<Projective2>,
1210 >(
1211 &poseidon_config,
1212 cf_r1cs.clone(),
1213 cf_pedersen_params.clone(),
1214 cf_W_i.clone(), // CycleFold running instance witness
1215 cf_U_i.clone(), // CycleFold running instance
1216 cf_u_i_x, // CycleFold incoming instance
1217 cf_circuit,
1218 )
1219 .unwrap();
1220
1221 // hash the CycleFold folded instance, which is used as the 2nd public input in the
1222 // AugmentedFCircuit
1223 let cf_u_i1_x = cf_U_i1.hash_cyclefold(&poseidon_config).unwrap();
1224
1225 augmented_f_circuit =
1226 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1227 _c2: PhantomData,
1228 _gc2: PhantomData,
1229 poseidon_config: poseidon_config.clone(),
1230 ccs: ccs.clone(),
1231 i: Some(iFr),
1232 i_usize: Some(i),
1233 z_0: Some(z_0.clone()),
1234 z_i: Some(z_i.clone()),
1235 external_inputs: Some(vec![]),
1236 u_i_C: Some(u_i.C),
1237 U_i: Some(U_i.clone()),
1238 U_i1_C: Some(U_i1.C),
1239 F: F_circuit,
1240 x: Some(u_i1_x),
1241 nimfs_proof: Some(nimfs_proof),
1242
1243 // cyclefold values
1244 cf_u_i_cmW: Some(cf_u_i.cmW),
1245 cf_U_i: Some(cf_U_i),
1246 cf_x: Some(cf_u_i1_x),
1247 cf_cmT: Some(cf_cmT),
1248 };
1249
1250 // assign the next round instances
1251 cf_W_i = cf_W_i1;
1252 cf_U_i = cf_U_i1;
1253 }
1254
1255 let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap();
1256 assert!(cs.is_satisfied().unwrap());
1257
1258 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<Fr>(&cs); // includes 1 and public inputs
1259 assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap());
1260 let r1cs_z = [vec![Fr::one()], r1cs_x_i1.clone(), r1cs_w_i1.clone()].concat();
1261 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
1262 // assign them directly to w_i, u_i.
1263 (u_i, w_i) = ccs.to_cccs(&mut rng, &pedersen_params, &r1cs_z).unwrap();
1264 u_i.check_relation(&pedersen_params, &ccs, &w_i).unwrap();
1265
1266 // sanity checks
1267 assert_eq!(w_i.w, r1cs_w_i1);
1268 assert_eq!(u_i.x, r1cs_x_i1);
1269 assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap());
1270 assert_eq!(u_i.x[1], augmented_f_circuit.cf_x.unwrap());
1271 let expected_u_i1_x = U_i1
1272 .hash(&poseidon_config, iFr + Fr::one(), z_0.clone(), z_i1.clone())
1273 .unwrap();
1274 let expected_cf_U_i1_x = cf_U_i.hash_cyclefold(&poseidon_config).unwrap();
1275 // u_i is already u_i1 at this point, check that has the expected value at x[0]
1276 assert_eq!(u_i.x[0], expected_u_i1_x);
1277 assert_eq!(u_i.x[1], expected_cf_U_i1_x);
1278
1279 // set values for next iteration
1280 iFr += Fr::one();
1281 // assign z_{i+1} into z_i
1282 z_i = z_i1.clone();
1283 U_i = U_i1.clone();
1284 W_i = W_i1.clone();
1285
1286 // check the new LCCCS instance relation
1287 U_i.check_relation(&pedersen_params, &ccs, &W_i).unwrap();
1288 // check the new CCCS instance relation
1289 u_i.check_relation(&pedersen_params, &ccs, &w_i).unwrap();
1290
1291 // check the CycleFold instance relation
1292 cf_r1cs
1293 .check_relaxed_instance_relation(&cf_W_i, &cf_U_i)
1294 .unwrap();
1295
1296 println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
1297 }
1298 }
1299}