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 pub 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 (u_i1_x_base, _) = LCCCSVar::new_constant(cs.clone(), U_dummy)?.hash(
724 &crh_params,
725 FpVar::<CF1<C1>>::one(),
726 z_0.clone(),
727 z_i1.clone(),
728 )?;
729 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
730 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
731
732 // convert rho_bits to a `NonNativeFieldVar`
733 let rho_nonnat = {
734 let mut bits = rho_bits;
735 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
736 NonNativeUintVar::from(&bits)
737 };
738
739 // CycleFold part
740 // C.1. Compute cf1_u_i.x and cf2_u_i.x
741 let cf_x = vec![
742 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,
743 ];
744
745 // ensure that cf_u has as public inputs the C from main instances U_i, u_i, U_i+1
746 // coordinates of the commitments.
747 // C.2. Construct `cf_u_i`
748 let cf_u_i = CycleFoldCommittedInstanceVar {
749 // cf1_u_i.cmE = 0. Notice that we enforce cmE to be equal to 0 since it is allocated
750 // as 0.
751 cmE: GC2::zero(),
752 // cf1_u_i.u = 1
753 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
754 // cf_u_i.cmW is provided by the prover as witness
755 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf_u_i_cmW.unwrap_or(C2::zero())))?,
756 // cf_u_i.x is computed in step 1
757 x: cf_x,
758 };
759
760 // C.3. nifs.verify (fold_committed_instance), obtains cf_U_{i+1} by folding cf_u_i & cf_U_i.
761 // compute cf_r = H(cf_u_i, cf_U_i, cf_cmT)
762 // cf_r_bits is denoted by rho* in the paper.
763 let cf_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
764 cs.clone(),
765 &self.poseidon_config,
766 cf_U_i_vec,
767 cf_u_i.clone(),
768 cf_cmT.clone(),
769 )?;
770 // Convert cf_r_bits to a `NonNativeFieldVar`
771 let cf_r_nonnat = {
772 let mut bits = cf_r_bits.clone();
773 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
774 NonNativeUintVar::from(&bits)
775 };
776 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
777 let cf_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
778 cf_r_bits,
779 cf_r_nonnat,
780 cf_cmT,
781 cf_U_i,
782 cf_u_i,
783 )?;
784
785 // Back to Primary Part
786 // P.4.b compute and check the second output of F'
787 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
788 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
789 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&crh_params)?;
790 let (cf_u_i1_x_base, _) =
791 CycleFoldCommittedInstanceVar::new_constant(cs.clone(), cf_u_dummy)?
792 .hash(&crh_params)?;
793 let cf_x = FpVar::new_input(cs.clone(), || {
794 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
795 })?;
796 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
797
798 Ok(())
799 }
800}
801
802#[cfg(test)]
803mod tests {
804 use ark_bn254::{constraints::GVar, Fq, Fr, G1Projective as Projective};
805 use ark_ff::BigInteger;
806 use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
807 use ark_r1cs_std::{alloc::AllocVar, fields::fp::FpVar, R1CSVar};
808 use ark_std::{test_rng, UniformRand};
809 use std::time::Instant;
810
811 use super::*;
812 use crate::{
813 ccs::{
814 r1cs::extract_w_x,
815 tests::{get_test_ccs, get_test_z},
816 CCS,
817 },
818 commitment::{pedersen::Pedersen, CommitmentScheme},
819 folding::{
820 circuits::cyclefold::{fold_cyclefold_circuit, CycleFoldCircuit},
821 hypernova::{
822 nimfs::NIMFS,
823 utils::{compute_c, compute_sigmas_thetas},
824 Witness,
825 },
826 nova::{traits::NovaR1CS, CommittedInstance, Witness as NovaWitness},
827 },
828 frontend::tests::CubicFCircuit,
829 transcript::{
830 poseidon::{poseidon_canonical_config, PoseidonTranscript, PoseidonTranscriptVar},
831 Transcript,
832 },
833 utils::get_cm_coordinates,
834 };
835
836 #[test]
837 pub fn test_compute_c_gadget() {
838 // number of LCCCS & CCCS instances to fold in a single step
839 let mu = 32;
840 let nu = 42;
841
842 let mut z_lcccs = Vec::new();
843 for i in 0..mu {
844 let z = get_test_z(i + 3);
845 z_lcccs.push(z);
846 }
847 let mut z_cccs = Vec::new();
848 for i in 0..nu {
849 let z = get_test_z(i + 3);
850 z_cccs.push(z);
851 }
852
853 let ccs: CCS<Fr> = get_test_ccs();
854
855 let mut rng = test_rng();
856 let gamma: Fr = Fr::rand(&mut rng);
857 let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
858 let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
859
860 let (pedersen_params, _) =
861 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
862
863 // Create the LCCCS instances out of z_lcccs
864 let mut lcccs_instances = Vec::new();
865 for z_i in z_lcccs.iter() {
866 let (inst, _) = ccs
867 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
868 .unwrap();
869 lcccs_instances.push(inst);
870 }
871 // Create the CCCS instance out of z_cccs
872 let mut cccs_instances = Vec::new();
873 for z_i in z_cccs.iter() {
874 let (inst, _) = ccs
875 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
876 .unwrap();
877 cccs_instances.push(inst);
878 }
879
880 let sigmas_thetas = compute_sigmas_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime).unwrap();
881
882 let expected_c = compute_c(
883 &ccs,
884 &sigmas_thetas,
885 gamma,
886 &beta,
887 &lcccs_instances
888 .iter()
889 .map(|lcccs| lcccs.r_x.clone())
890 .collect(),
891 &r_x_prime,
892 )
893 .unwrap();
894
895 let cs = ConstraintSystem::<Fr>::new_ref();
896 let mut vec_sigmas = Vec::new();
897 let mut vec_thetas = Vec::new();
898 for sigmas in sigmas_thetas.0 {
899 vec_sigmas
900 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap());
901 }
902 for thetas in sigmas_thetas.1 {
903 vec_thetas
904 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap());
905 }
906 let vec_r_x: Vec<Vec<FpVar<Fr>>> = lcccs_instances
907 .iter()
908 .map(|lcccs| {
909 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap()
910 })
911 .collect();
912 let vec_r_x_prime =
913 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap();
914 let gamma_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(gamma)).unwrap();
915 let beta_var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap();
916
917 let computed_c = compute_c_gadget(
918 cs.clone(),
919 &ccs,
920 vec_sigmas,
921 vec_thetas,
922 gamma_var,
923 beta_var,
924 vec_r_x,
925 vec_r_x_prime,
926 )
927 .unwrap();
928
929 assert_eq!(expected_c, computed_c.value().unwrap());
930 }
931
932 /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step,
933 /// to verify the folding in the NIMFSGadget circuit
934 #[test]
935 pub fn test_nimfs_gadget_verify() {
936 let mut rng = test_rng();
937
938 // Create a basic CCS circuit
939 let ccs = get_test_ccs::<Fr>();
940 let (pedersen_params, _) =
941 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
942
943 let mu = 32;
944 let nu = 42;
945
946 // Generate a mu LCCCS & nu CCCS satisfying witness
947 let mut z_lcccs = Vec::new();
948 for i in 0..mu {
949 let z = get_test_z(i + 3);
950 z_lcccs.push(z);
951 }
952 let mut z_cccs = Vec::new();
953 for i in 0..nu {
954 let z = get_test_z(nu + i + 3);
955 z_cccs.push(z);
956 }
957
958 // Create the LCCCS instances out of z_lcccs
959 let mut lcccs_instances = Vec::new();
960 let mut w_lcccs = Vec::new();
961 for z_i in z_lcccs.iter() {
962 let (running_instance, w) = ccs
963 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
964 .unwrap();
965 lcccs_instances.push(running_instance);
966 w_lcccs.push(w);
967 }
968 // Create the CCCS instance out of z_cccs
969 let mut cccs_instances = Vec::new();
970 let mut w_cccs = Vec::new();
971 for z_i in z_cccs.iter() {
972 let (new_instance, w) = ccs
973 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
974 .unwrap();
975 cccs_instances.push(new_instance);
976 w_cccs.push(w);
977 }
978
979 // Prover's transcript
980 let poseidon_config = poseidon_canonical_config::<Fr>();
981 let mut transcript_p: PoseidonTranscript<Projective> =
982 PoseidonTranscript::<Projective>::new(&poseidon_config);
983
984 // Run the prover side of the multifolding
985 let (proof, folded_lcccs, folded_witness, _) =
986 NIMFS::<Projective, PoseidonTranscript<Projective>>::prove(
987 &mut transcript_p,
988 &ccs,
989 &lcccs_instances,
990 &cccs_instances,
991 &w_lcccs,
992 &w_cccs,
993 )
994 .unwrap();
995
996 // Verifier's transcript
997 let mut transcript_v: PoseidonTranscript<Projective> =
998 PoseidonTranscript::<Projective>::new(&poseidon_config);
999
1000 // Run the verifier side of the multifolding
1001 let folded_lcccs_v = NIMFS::<Projective, PoseidonTranscript<Projective>>::verify(
1002 &mut transcript_v,
1003 &ccs,
1004 &lcccs_instances,
1005 &cccs_instances,
1006 proof.clone(),
1007 )
1008 .unwrap();
1009 assert_eq!(folded_lcccs, folded_lcccs_v);
1010
1011 // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
1012 folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
1013
1014 // allocate circuit inputs
1015 let cs = ConstraintSystem::<Fr>::new_ref();
1016 let lcccs_instancesVar =
1017 Vec::<LCCCSVar<Projective>>::new_witness(cs.clone(), || Ok(lcccs_instances.clone()))
1018 .unwrap();
1019 let cccs_instancesVar =
1020 Vec::<CCCSVar<Projective>>::new_witness(cs.clone(), || Ok(cccs_instances.clone()))
1021 .unwrap();
1022 let proofVar =
1023 ProofVar::<Projective>::new_witness(cs.clone(), || Ok(proof.clone())).unwrap();
1024 let transcriptVar = PoseidonTranscriptVar::<Fr>::new(cs.clone(), &poseidon_config);
1025
1026 let enabled = Boolean::<Fr>::new_witness(cs.clone(), || Ok(true)).unwrap();
1027 let (folded_lcccsVar, _) = NIMFSGadget::<Projective>::verify(
1028 cs.clone(),
1029 &ccs,
1030 transcriptVar,
1031 &lcccs_instancesVar,
1032 &cccs_instancesVar,
1033 proofVar,
1034 enabled,
1035 )
1036 .unwrap();
1037 assert!(cs.is_satisfied().unwrap());
1038 assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u);
1039 }
1040
1041 /// test that checks the native LCCCS.hash vs the R1CS constraints version
1042 #[test]
1043 pub fn test_lcccs_hash() {
1044 let mut rng = test_rng();
1045 let poseidon_config = poseidon_canonical_config::<Fr>();
1046
1047 let ccs = get_test_ccs();
1048 let z1 = get_test_z::<Fr>(3);
1049
1050 let (pedersen_params, _) =
1051 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1052
1053 let i = Fr::from(3_u32);
1054 let z_0 = vec![Fr::from(3_u32)];
1055 let z_i = vec![Fr::from(3_u32)];
1056 let (lcccs, _) = ccs
1057 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, &z1)
1058 .unwrap();
1059 let h = lcccs
1060 .clone()
1061 .hash(&poseidon_config, i, z_0.clone(), z_i.clone())
1062 .unwrap();
1063
1064 let cs = ConstraintSystem::<Fr>::new_ref();
1065
1066 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
1067 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
1068 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
1069 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
1070 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
1071 let (hVar, _) = lcccsVar
1072 .clone()
1073 .hash(&crh_params, iVar.clone(), z_0Var.clone(), z_iVar.clone())
1074 .unwrap();
1075 assert!(cs.is_satisfied().unwrap());
1076
1077 // check that the natively computed and in-circuit computed hashes match
1078 assert_eq!(hVar.value().unwrap(), h);
1079 }
1080
1081 #[test]
1082 pub fn test_augmented_f_circuit() {
1083 let mut rng = test_rng();
1084 let poseidon_config = poseidon_canonical_config::<Fr>();
1085
1086 let start = Instant::now();
1087 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
1088 let mut augmented_f_circuit = AugmentedFCircuit::<
1089 Projective,
1090 Projective2,
1091 GVar2,
1092 CubicFCircuit<Fr>,
1093 >::empty(&poseidon_config, F_circuit, None)
1094 .unwrap();
1095 let ccs = augmented_f_circuit.ccs.clone();
1096 println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed());
1097 println!("CCS m x n: {} x {}", ccs.m, ccs.n);
1098
1099 // CycleFold circuit
1100 let cs2 = ConstraintSystem::<Fq>::new_ref();
1101 let cf_circuit = CycleFoldCircuit::<Projective, GVar>::empty();
1102 cf_circuit.generate_constraints(cs2.clone()).unwrap();
1103 cs2.finalize();
1104 let cs2 = cs2
1105 .into_inner()
1106 .ok_or(Error::NoInnerConstraintSystem)
1107 .unwrap();
1108 let cf_r1cs = extract_r1cs::<Fq>(&cs2);
1109
1110 let (pedersen_params, _) =
1111 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1112 let (cf_pedersen_params, _) =
1113 Pedersen::<Projective2>::setup(&mut rng, cf_r1cs.A.n_cols - cf_r1cs.l - 1).unwrap();
1114
1115 // first step
1116 let z_0 = vec![Fr::from(3_u32)];
1117 let mut z_i = z_0.clone();
1118
1119 // prepare the dummy instances
1120 let W_dummy = Witness::<Fr>::dummy(&ccs);
1121 let U_dummy = LCCCS::<Projective>::dummy(ccs.l, ccs.t, ccs.s);
1122 let w_dummy = W_dummy.clone();
1123 let u_dummy = CCCS::<Projective>::dummy(ccs.l);
1124 let (cf_W_dummy, cf_U_dummy): (NovaWitness<Projective2>, CommittedInstance<Projective2>) =
1125 cf_r1cs.dummy_instance();
1126
1127 // set the initial dummy instances
1128 let mut W_i = W_dummy.clone();
1129 let mut U_i = U_dummy.clone();
1130 let mut w_i = w_dummy.clone();
1131 let mut u_i = u_dummy.clone();
1132 let mut cf_W_i = cf_W_dummy.clone();
1133 let mut cf_U_i = cf_U_dummy.clone();
1134 u_i.x = vec![
1135 U_i.hash(&poseidon_config, Fr::zero(), z_0.clone(), z_i.clone())
1136 .unwrap(),
1137 cf_U_i.hash_cyclefold(&poseidon_config).unwrap(),
1138 ];
1139
1140 let n_steps: usize = 4;
1141 let mut iFr = Fr::zero();
1142 for i in 0..n_steps {
1143 let start = Instant::now();
1144
1145 let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap();
1146
1147 let (U_i1, W_i1);
1148
1149 if i == 0 {
1150 W_i1 = Witness::<Fr>::dummy(&ccs);
1151 U_i1 = LCCCS::dummy(ccs.l, ccs.t, ccs.s);
1152
1153 let u_i1_x = U_i1
1154 .hash(&poseidon_config, Fr::one(), z_0.clone(), z_i1.clone())
1155 .unwrap();
1156
1157 // hash the initial (dummy) CycleFold instance, which is used as the 2nd public
1158 // input in the AugmentedFCircuit
1159 let cf_u_i1_x = cf_U_i.hash_cyclefold(&poseidon_config).unwrap();
1160
1161 augmented_f_circuit =
1162 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1163 _c2: PhantomData,
1164 _gc2: PhantomData,
1165 poseidon_config: poseidon_config.clone(),
1166 ccs: ccs.clone(),
1167 i: Some(Fr::zero()),
1168 i_usize: Some(0),
1169 z_0: Some(z_0.clone()),
1170 z_i: Some(z_i.clone()),
1171 external_inputs: Some(vec![]),
1172 u_i_C: Some(u_i.C),
1173 U_i: Some(U_i.clone()),
1174 U_i1_C: Some(U_i1.C),
1175 F: F_circuit,
1176 x: Some(u_i1_x),
1177 nimfs_proof: None,
1178
1179 // cyclefold values
1180 cf_u_i_cmW: None,
1181 cf_U_i: None,
1182 cf_x: Some(cf_u_i1_x),
1183 cf_cmT: None,
1184 };
1185 } else {
1186 let mut transcript_p: PoseidonTranscript<Projective> =
1187 PoseidonTranscript::<Projective>::new(&poseidon_config.clone());
1188 let (rho_bits, nimfs_proof);
1189 (nimfs_proof, U_i1, W_i1, rho_bits) =
1190 NIMFS::<Projective, PoseidonTranscript<Projective>>::prove(
1191 &mut transcript_p,
1192 &ccs,
1193 &[U_i.clone()],
1194 &[u_i.clone()],
1195 &[W_i.clone()],
1196 &[w_i.clone()],
1197 )
1198 .unwrap();
1199
1200 // sanity check: check the folded instance relation
1201 U_i1.check_relation(&ccs, &W_i1).unwrap();
1202
1203 let u_i1_x = U_i1
1204 .hash(&poseidon_config, iFr + Fr::one(), z_0.clone(), z_i1.clone())
1205 .unwrap();
1206
1207 let rho_Fq = Fq::from_bigint(BigInteger::from_bits_le(&rho_bits)).unwrap();
1208 // CycleFold part:
1209 // get the vector used as public inputs 'x' in the CycleFold circuit
1210 // cyclefold circuit for cmW
1211 let cf_u_i_x = [
1212 vec![rho_Fq],
1213 get_cm_coordinates(&U_i.C),
1214 get_cm_coordinates(&u_i.C),
1215 get_cm_coordinates(&U_i1.C),
1216 ]
1217 .concat();
1218
1219 let cf_circuit = CycleFoldCircuit::<Projective, GVar> {
1220 _gc: PhantomData,
1221 r_bits: Some(rho_bits.clone()),
1222 p1: Some(U_i.clone().C),
1223 p2: Some(u_i.clone().C),
1224 x: Some(cf_u_i_x.clone()),
1225 };
1226
1227 let (_cf_w_i, cf_u_i, cf_W_i1, cf_U_i1, cf_cmT, _) = fold_cyclefold_circuit::<
1228 Projective,
1229 GVar,
1230 Projective2,
1231 GVar2,
1232 CubicFCircuit<Fr>,
1233 Pedersen<Projective>,
1234 Pedersen<Projective2>,
1235 >(
1236 &poseidon_config,
1237 cf_r1cs.clone(),
1238 cf_pedersen_params.clone(),
1239 cf_W_i.clone(), // CycleFold running instance witness
1240 cf_U_i.clone(), // CycleFold running instance
1241 cf_u_i_x, // CycleFold incoming instance
1242 cf_circuit,
1243 )
1244 .unwrap();
1245
1246 // hash the CycleFold folded instance, which is used as the 2nd public input in the
1247 // AugmentedFCircuit
1248 let cf_u_i1_x = cf_U_i1.hash_cyclefold(&poseidon_config).unwrap();
1249
1250 augmented_f_circuit =
1251 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1252 _c2: PhantomData,
1253 _gc2: PhantomData,
1254 poseidon_config: poseidon_config.clone(),
1255 ccs: ccs.clone(),
1256 i: Some(iFr),
1257 i_usize: Some(i),
1258 z_0: Some(z_0.clone()),
1259 z_i: Some(z_i.clone()),
1260 external_inputs: Some(vec![]),
1261 u_i_C: Some(u_i.C),
1262 U_i: Some(U_i.clone()),
1263 U_i1_C: Some(U_i1.C),
1264 F: F_circuit,
1265 x: Some(u_i1_x),
1266 nimfs_proof: Some(nimfs_proof),
1267
1268 // cyclefold values
1269 cf_u_i_cmW: Some(cf_u_i.cmW),
1270 cf_U_i: Some(cf_U_i),
1271 cf_x: Some(cf_u_i1_x),
1272 cf_cmT: Some(cf_cmT),
1273 };
1274
1275 // assign the next round instances
1276 cf_W_i = cf_W_i1;
1277 cf_U_i = cf_U_i1;
1278 }
1279
1280 let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap();
1281 assert!(cs.is_satisfied().unwrap());
1282
1283 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<Fr>(&cs); // includes 1 and public inputs
1284 assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap());
1285 let r1cs_z = [vec![Fr::one()], r1cs_x_i1.clone(), r1cs_w_i1.clone()].concat();
1286 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
1287 // assign them directly to w_i, u_i.
1288 (u_i, w_i) = ccs
1289 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, &r1cs_z)
1290 .unwrap();
1291 u_i.check_relation(&ccs, &w_i).unwrap();
1292
1293 // sanity checks
1294 assert_eq!(w_i.w, r1cs_w_i1);
1295 assert_eq!(u_i.x, r1cs_x_i1);
1296 assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap());
1297 assert_eq!(u_i.x[1], augmented_f_circuit.cf_x.unwrap());
1298 let expected_u_i1_x = U_i1
1299 .hash(&poseidon_config, iFr + Fr::one(), z_0.clone(), z_i1.clone())
1300 .unwrap();
1301 let expected_cf_U_i1_x = cf_U_i.hash_cyclefold(&poseidon_config).unwrap();
1302 // u_i is already u_i1 at this point, check that has the expected value at x[0]
1303 assert_eq!(u_i.x[0], expected_u_i1_x);
1304 assert_eq!(u_i.x[1], expected_cf_U_i1_x);
1305
1306 // set values for next iteration
1307 iFr += Fr::one();
1308 // assign z_{i+1} into z_i
1309 z_i = z_i1.clone();
1310 U_i = U_i1.clone();
1311 W_i = W_i1.clone();
1312
1313 // check the new LCCCS instance relation
1314 U_i.check_relation(&ccs, &W_i).unwrap();
1315 // check the new CCCS instance relation
1316 u_i.check_relation(&ccs, &w_i).unwrap();
1317
1318 // check the CycleFold instance relation
1319 cf_r1cs
1320 .check_relaxed_instance_relation(&cf_W_i, &cf_U_i)
1321 .unwrap();
1322
1323 println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
1324 }
1325 }
1326}