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