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::sponge::{
3 constraints::CryptographicSpongeVar,
4 poseidon::{constraints::PoseidonSpongeVar, PoseidonSponge},
5 CryptographicSponge,
6};
7use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
8use ark_ec::{CurveGroup, Group};
9use ark_ff::PrimeField;
10use ark_r1cs_std::{
11 alloc::{AllocVar, AllocationMode},
12 boolean::Boolean,
13 eq::EqGadget,
14 fields::{fp::FpVar, FieldVar},
15 groups::GroupOpsBounds,
16 prelude::CurveVar,
17 R1CSVar, ToConstraintFieldGadget,
18};
19use ark_relations::r1cs::{
20 ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, Namespace, SynthesisError,
21};
22use ark_std::{fmt::Debug, ops::Neg, One, Zero};
23use core::{borrow::Borrow, marker::PhantomData};
24
25use super::{
26 cccs::CCCS,
27 lcccs::LCCCS,
28 nimfs::{NIMFSProof, NIMFS},
29 Witness,
30};
31use crate::constants::N_BITS_RO;
32use crate::folding::{
33 circuits::cyclefold::{
34 CycleFoldChallengeGadget, CycleFoldCommittedInstanceVar, NIFSFullGadget, CF_IO_LEN,
35 },
36 circuits::{
37 nonnative::{affine::NonNativeAffineVar, uint::NonNativeUintVar},
38 sum_check::{IOPProofVar, SumCheckVerifierGadget, VPAuxInfoVar},
39 utils::EqEvalGadget,
40 CF1, CF2,
41 },
42 nova::{get_r1cs_from_cs, CommittedInstance},
43};
44use crate::frontend::FCircuit;
45use crate::utils::virtual_polynomial::VPAuxInfo;
46use crate::Error;
47use crate::{
48 arith::{ccs::CCS, r1cs::extract_r1cs},
49 transcript::TranscriptVar,
50};
51
52/// Committed CCS instance
53#[derive(Debug, Clone)]
54pub struct CCCSVar<C: CurveGroup>
55where
56 <C as CurveGroup>::BaseField: PrimeField,
57{
58 // Commitment to witness
59 pub C: NonNativeAffineVar<C>,
60 // Public io
61 pub x: Vec<FpVar<CF1<C>>>,
62}
63impl<C> AllocVar<CCCS<C>, CF1<C>> for CCCSVar<C>
64where
65 C: CurveGroup,
66 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
67{
68 fn new_variable<T: Borrow<CCCS<C>>>(
69 cs: impl Into<Namespace<CF1<C>>>,
70 f: impl FnOnce() -> Result<T, SynthesisError>,
71 mode: AllocationMode,
72 ) -> Result<Self, SynthesisError> {
73 f().and_then(|val| {
74 let cs = cs.into();
75
76 let C = NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?;
77 let x: Vec<FpVar<C::ScalarField>> =
78 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
79
80 Ok(Self { C, x })
81 })
82 }
83}
84
85/// Linearized Committed CCS instance
86#[derive(Debug, Clone)]
87pub struct LCCCSVar<C: CurveGroup>
88where
89 <C as CurveGroup>::BaseField: PrimeField,
90{
91 // Commitment to witness
92 pub C: NonNativeAffineVar<C>,
93 // Relaxation factor of z for folded LCCCS
94 pub u: FpVar<CF1<C>>,
95 // Public io
96 pub x: Vec<FpVar<CF1<C>>>,
97 // Random evaluation point for the v_i
98 pub r_x: Vec<FpVar<CF1<C>>>,
99 // Vector of v_i
100 pub v: Vec<FpVar<CF1<C>>>,
101}
102impl<C> AllocVar<LCCCS<C>, CF1<C>> for LCCCSVar<C>
103where
104 C: CurveGroup,
105 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
106{
107 fn new_variable<T: Borrow<LCCCS<C>>>(
108 cs: impl Into<Namespace<CF1<C>>>,
109 f: impl FnOnce() -> Result<T, SynthesisError>,
110 mode: AllocationMode,
111 ) -> Result<Self, SynthesisError> {
112 f().and_then(|val| {
113 let cs = cs.into();
114
115 let C = NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?;
116 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
117 let x: Vec<FpVar<C::ScalarField>> =
118 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
119 let r_x: Vec<FpVar<C::ScalarField>> =
120 Vec::new_variable(cs.clone(), || Ok(val.borrow().r_x.clone()), mode)?;
121 let v: Vec<FpVar<C::ScalarField>> =
122 Vec::new_variable(cs.clone(), || Ok(val.borrow().v.clone()), mode)?;
123
124 Ok(Self { C, u, x, r_x, v })
125 })
126 }
127}
128
129impl<C> LCCCSVar<C>
130where
131 C: CurveGroup,
132 <C as Group>::ScalarField: Absorb,
133 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
134{
135 /// [`LCCCSVar`].hash implements the LCCCS instance hash compatible with the native
136 /// implementation from LCCCS.hash.
137 /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the LCCCS.
138 /// Additionally it returns the vector of the field elements from the self parameters, so they
139 /// can be reused in other gadgets avoiding recalculating (reconstraining) them.
140 #[allow(clippy::type_complexity)]
141 pub fn hash(
142 self,
143 sponge: &PoseidonSpongeVar<CF1<C>>,
144 pp_hash: FpVar<CF1<C>>,
145 i: FpVar<CF1<C>>,
146 z_0: Vec<FpVar<CF1<C>>>,
147 z_i: Vec<FpVar<CF1<C>>>,
148 ) -> Result<(FpVar<CF1<C>>, Vec<FpVar<CF1<C>>>), SynthesisError> {
149 let mut sponge = sponge.clone();
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 sponge.absorb(&pp_hash)?;
159 sponge.absorb(&i)?;
160 sponge.absorb(&z_0)?;
161 sponge.absorb(&z_i)?;
162 sponge.absorb(&U_vec)?;
163 Ok((sponge.squeeze_field_elements(1)?.pop().unwrap(), U_vec))
164 }
165}
166
167/// ProofVar defines a multifolding proof
168#[derive(Debug)]
169pub struct ProofVar<C: CurveGroup> {
170 pub sc_proof: IOPProofVar<C::ScalarField>,
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::ScalarField>::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<S: CryptographicSponge, T: TranscriptVar<C::ScalarField, S>>(
227 cs: ConstraintSystemRef<CF1<C>>,
228 // only used the CCS params, not the matrices
229 ccs: &CCS<C::ScalarField>,
230 transcript: &mut T,
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(&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(&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::ScalarField>::verify(
286 &proof.sc_proof,
287 &vp_aux_info,
288 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 pp_hash: Option<CF1<C1>>,
459 pub i: Option<CF1<C1>>,
460 pub i_usize: Option<usize>,
461 pub z_0: Option<Vec<C1::ScalarField>>,
462 pub z_i: Option<Vec<C1::ScalarField>>,
463 pub external_inputs: Option<Vec<C1::ScalarField>>,
464 pub u_i_C: Option<C1>, // u_i.C
465 pub U_i: Option<LCCCS<C1>>,
466 pub U_i1_C: Option<C1>, // U_{i+1}.C
467 pub F: FC, // F circuit
468 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
469 pub nimfs_proof: Option<NIMFSProof<C1>>,
470
471 // cyclefold verifier on C1
472 pub cf_u_i_cmW: Option<C2>, // input, cf_u_i.cmW
473 pub cf_U_i: Option<CommittedInstance<C2>>, // input, RelaxedR1CS CycleFold instance
474 pub cf_x: Option<CF1<C1>>, // public input (cf_u_{i+1}.x[1])
475 pub cf_cmT: Option<C2>,
476}
477
478impl<C1, C2, GC2, FC> AugmentedFCircuit<C1, C2, GC2, FC>
479where
480 C1: CurveGroup,
481 C2: CurveGroup,
482 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
483 FC: FCircuit<CF1<C1>>,
484 <C1 as CurveGroup>::BaseField: PrimeField,
485 <C2 as CurveGroup>::BaseField: PrimeField,
486 <C1 as Group>::ScalarField: Absorb,
487 <C2 as Group>::ScalarField: Absorb,
488 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
489 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
490{
491 pub fn default(
492 poseidon_config: &PoseidonConfig<CF1<C1>>,
493 F_circuit: FC,
494 ccs: CCS<C1::ScalarField>,
495 ) -> Self {
496 Self {
497 _c2: PhantomData,
498 _gc2: PhantomData,
499 poseidon_config: poseidon_config.clone(),
500 ccs,
501 pp_hash: None,
502 i: None,
503 i_usize: None,
504 z_0: None,
505 z_i: None,
506 external_inputs: None,
507 u_i_C: None,
508 U_i: None,
509 U_i1_C: None,
510 F: F_circuit,
511 x: None,
512 nimfs_proof: None,
513 cf_u_i_cmW: None,
514 cf_U_i: None,
515 cf_x: None,
516 cf_cmT: None,
517 }
518 }
519
520 pub fn empty(
521 poseidon_config: &PoseidonConfig<CF1<C1>>,
522 F_circuit: FC,
523 ccs: Option<CCS<C1::ScalarField>>,
524 ) -> Result<Self, Error> {
525 let initial_ccs = CCS {
526 // m, n, s, s_prime and M will be overwritten by the `upper_bound_ccs' method
527 m: 0,
528 n: 0,
529 l: 2, // io_len
530 s: 1,
531 s_prime: 1,
532 t: 3, // note: this is only supports R1CS for the moment
533 q: 2,
534 d: 2,
535 S: vec![vec![0, 1], vec![2]],
536 c: vec![C1::ScalarField::one(), C1::ScalarField::one().neg()],
537 M: vec![],
538 };
539 let mut augmented_f_circuit = Self::default(poseidon_config, F_circuit, initial_ccs);
540 if ccs.is_some() {
541 augmented_f_circuit.ccs = ccs.unwrap();
542 } else {
543 augmented_f_circuit.ccs = augmented_f_circuit.upper_bound_ccs()?;
544 }
545 Ok(augmented_f_circuit)
546 }
547
548 /// This method computes the CCS parameters. This is used because there is a circular
549 /// dependency between the AugmentedFCircuit CCS and the CCS parameters m & n & s & s'.
550 /// For a stable FCircuit circuit, the CCS parameters can be computed in advance and can be
551 /// feed in as parameter for the AugmentedFCircuit::empty method to avoid computing them there.
552 pub fn upper_bound_ccs(&self) -> Result<CCS<C1::ScalarField>, Error> {
553 let r1cs = get_r1cs_from_cs::<CF1<C1>>(self.clone()).unwrap();
554 let ccs = CCS::from_r1cs(r1cs.clone());
555
556 let z_0 = vec![C1::ScalarField::zero(); self.F.state_len()];
557 let W_i = Witness::<C1::ScalarField>::dummy(&ccs);
558 let U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
559 let w_i = W_i.clone();
560 let u_i = CCCS::<C1>::dummy(ccs.l);
561
562 let mut transcript_p: PoseidonSponge<C1::ScalarField> =
563 PoseidonSponge::<C1::ScalarField>::new(&self.poseidon_config.clone());
564 // since this is only for the number of constraints, no need to absorb the pp_hash here
565 let (nimfs_proof, U_i1, _, _) = NIMFS::<C1, PoseidonSponge<C1::ScalarField>>::prove(
566 &mut transcript_p,
567 &ccs,
568 &[U_i.clone()],
569 &[u_i.clone()],
570 &[W_i.clone()],
571 &[w_i.clone()],
572 )?;
573
574 let augmented_f_circuit = Self {
575 _c2: PhantomData,
576 _gc2: PhantomData,
577 poseidon_config: self.poseidon_config.clone(),
578 ccs: ccs.clone(),
579 pp_hash: Some(C1::ScalarField::zero()),
580 i: Some(C1::ScalarField::zero()),
581 i_usize: Some(0),
582 z_0: Some(z_0.clone()),
583 z_i: Some(z_0.clone()),
584 external_inputs: Some(vec![]),
585 u_i_C: Some(u_i.C),
586 U_i: Some(U_i.clone()),
587 U_i1_C: Some(U_i1.C),
588 F: self.F.clone(),
589 x: Some(C1::ScalarField::zero()),
590 nimfs_proof: Some(nimfs_proof),
591 // cyclefold values
592 cf_u_i_cmW: None,
593 cf_U_i: None,
594 cf_x: None,
595 cf_cmT: None,
596 };
597
598 Ok(augmented_f_circuit.compute_cs_ccs()?.1)
599 }
600
601 /// Returns the cs (ConstraintSystem) and the CCS out of the AugmentedFCircuit
602 #[allow(clippy::type_complexity)]
603 pub fn compute_cs_ccs(
604 &self,
605 ) -> Result<(ConstraintSystem<C1::ScalarField>, CCS<C1::ScalarField>), Error> {
606 let cs = ConstraintSystem::<C1::ScalarField>::new_ref();
607 self.clone().generate_constraints(cs.clone())?;
608 cs.finalize();
609 let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?;
610 let r1cs = extract_r1cs::<C1::ScalarField>(&cs);
611 let ccs = CCS::from_r1cs(r1cs.clone());
612
613 Ok((cs, ccs))
614 }
615}
616
617impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
618where
619 C1: CurveGroup,
620 C2: CurveGroup,
621 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
622 FC: FCircuit<CF1<C1>>,
623 <C1 as CurveGroup>::BaseField: PrimeField,
624 <C2 as CurveGroup>::BaseField: PrimeField,
625 <C1 as Group>::ScalarField: Absorb,
626 <C2 as Group>::ScalarField: Absorb,
627 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
628 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
629{
630 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
631 let pp_hash = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
632 Ok(self.pp_hash.unwrap_or_else(CF1::<C1>::zero))
633 })?;
634 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
635 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
636 })?;
637 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
638 Ok(self
639 .z_0
640 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
641 })?;
642 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
643 Ok(self
644 .z_i
645 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
646 })?;
647 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
648 Ok(self
649 .external_inputs
650 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
651 })?;
652
653 let U_dummy = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
654
655 let U_i =
656 LCCCSVar::<C1>::new_witness(cs.clone(), || Ok(self.U_i.unwrap_or(U_dummy.clone())))?;
657 let U_i1_C = NonNativeAffineVar::new_witness(cs.clone(), || {
658 Ok(self.U_i1_C.unwrap_or_else(C1::zero))
659 })?;
660 let mu = 1; // Note: at this commit, only 2-to-1 instance fold is supported
661 let nu = 1;
662 let nimfs_proof_dummy = NIMFSProof::<C1>::dummy(&self.ccs, mu, nu);
663 let nimfs_proof = ProofVar::<C1>::new_witness(cs.clone(), || {
664 Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy))
665 })?;
666
667 let cf_u_dummy = CommittedInstance::dummy(CF_IO_LEN);
668 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
669 Ok(self.cf_U_i.unwrap_or(cf_u_dummy.clone()))
670 })?;
671 let cf_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf_cmT.unwrap_or_else(C2::zero)))?;
672
673 let sponge = PoseidonSpongeVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
674
675 // get z_{i+1} from the F circuit
676 let i_usize = self.i_usize.unwrap_or(0);
677 let z_i1 =
678 self.F
679 .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?;
680
681 let is_basecase = i.is_zero()?;
682 let is_not_basecase = is_basecase.not();
683
684 // Primary Part
685 // P.1. Compute u_i.x
686 // u_i.x[0] = H(i, z_0, z_i, U_i)
687 let (u_i_x, _) = U_i.clone().hash(
688 &sponge,
689 pp_hash.clone(),
690 i.clone(),
691 z_0.clone(),
692 z_i.clone(),
693 )?;
694 // u_i.x[1] = H(cf_U_i)
695 let (cf_u_i_x, cf_U_i_vec) = cf_U_i.clone().hash(&sponge, pp_hash.clone())?;
696
697 // P.2. Construct u_i
698 let u_i = CCCSVar::<C1> {
699 // u_i.C is provided by the prover as witness
700 C: NonNativeAffineVar::<C1>::new_witness(cs.clone(), || {
701 Ok(self.u_i_C.unwrap_or(C1::zero()))
702 })?,
703 // u_i.x is computed in step 1
704 x: vec![u_i_x, cf_u_i_x],
705 };
706
707 // P.3. NIMFS.verify, obtains U_{i+1} by folding [U_i] & [u_i].
708 // Notice that NIMFSGadget::fold_committed_instance does not fold C. We set `U_i1.C` to
709 // unconstrained witnesses `U_i1_C` respectively. Its correctness will be checked on the
710 // other curve.
711 let mut transcript = PoseidonSpongeVar::new(cs.clone(), &self.poseidon_config);
712 transcript.absorb(&pp_hash)?;
713 let (mut U_i1, rho_bits) = NIMFSGadget::<C1>::verify(
714 cs.clone(),
715 &self.ccs.clone(),
716 &mut transcript,
717 &[U_i.clone()],
718 &[u_i.clone()],
719 nimfs_proof,
720 is_not_basecase.clone(),
721 )?;
722 U_i1.C = U_i1_C;
723
724 // P.4.a compute and check the first output of F'
725 let (u_i1_x, _) = U_i1.clone().hash(
726 &sponge,
727 pp_hash.clone(),
728 i + FpVar::<CF1<C1>>::one(),
729 z_0.clone(),
730 z_i1.clone(),
731 )?;
732 let (u_i1_x_base, _) = LCCCSVar::new_constant(cs.clone(), U_dummy)?.hash(
733 &sponge,
734 pp_hash.clone(),
735 FpVar::<CF1<C1>>::one(),
736 z_0.clone(),
737 z_i1.clone(),
738 )?;
739 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
740 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
741
742 // convert rho_bits to a `NonNativeFieldVar`
743 let rho_nonnat = {
744 let mut bits = rho_bits;
745 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
746 NonNativeUintVar::from(&bits)
747 };
748
749 // CycleFold part
750 // C.1. Compute cf1_u_i.x and cf2_u_i.x
751 let cf_x = vec![
752 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,
753 ];
754
755 // ensure that cf_u has as public inputs the C from main instances U_i, u_i, U_i+1
756 // coordinates of the commitments.
757 // C.2. Construct `cf_u_i`
758 let cf_u_i = CycleFoldCommittedInstanceVar {
759 // cf1_u_i.cmE = 0. Notice that we enforce cmE to be equal to 0 since it is allocated
760 // as 0.
761 cmE: GC2::zero(),
762 // cf1_u_i.u = 1
763 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
764 // cf_u_i.cmW is provided by the prover as witness
765 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf_u_i_cmW.unwrap_or(C2::zero())))?,
766 // cf_u_i.x is computed in step 1
767 x: cf_x,
768 };
769
770 // C.3. nifs.verify (fold_committed_instance), obtains cf_U_{i+1} by folding cf_u_i & cf_U_i.
771 // compute cf_r = H(cf_u_i, cf_U_i, cf_cmT)
772 // cf_r_bits is denoted by rho* in the paper.
773 let cf_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
774 &mut transcript,
775 pp_hash.clone(),
776 cf_U_i_vec,
777 cf_u_i.clone(),
778 cf_cmT.clone(),
779 )?;
780 // Convert cf_r_bits to a `NonNativeFieldVar`
781 let cf_r_nonnat = {
782 let mut bits = cf_r_bits.clone();
783 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
784 NonNativeUintVar::from(&bits)
785 };
786 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
787 let cf_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
788 cf_r_bits,
789 cf_r_nonnat,
790 cf_cmT,
791 cf_U_i,
792 cf_u_i,
793 )?;
794
795 // Back to Primary Part
796 // P.4.b compute and check the second output of F'
797 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
798 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
799 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&sponge, pp_hash.clone())?;
800 let (cf_u_i1_x_base, _) =
801 CycleFoldCommittedInstanceVar::new_constant(cs.clone(), cf_u_dummy)?
802 .hash(&sponge, pp_hash)?;
803 let cf_x = FpVar::new_input(cs.clone(), || {
804 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
805 })?;
806 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
807
808 Ok(())
809 }
810}
811
812#[cfg(test)]
813mod tests {
814 use ark_bn254::{constraints::GVar, Fq, Fr, G1Projective as Projective};
815 use ark_ff::BigInteger;
816 use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
817 use ark_std::{test_rng, UniformRand};
818 use std::time::Instant;
819
820 use super::*;
821 use crate::{
822 arith::{
823 ccs::tests::{get_test_ccs, get_test_z},
824 r1cs::extract_w_x,
825 },
826 commitment::{pedersen::Pedersen, CommitmentScheme},
827 folding::{
828 circuits::cyclefold::{fold_cyclefold_circuit, CycleFoldCircuit},
829 hypernova::utils::{compute_c, compute_sigmas_thetas},
830 nova::{traits::NovaR1CS, Witness as NovaWitness},
831 },
832 frontend::tests::CubicFCircuit,
833 transcript::poseidon::poseidon_canonical_config,
834 utils::get_cm_coordinates,
835 };
836
837 #[test]
838 pub fn test_compute_c_gadget() {
839 // number of LCCCS & CCCS instances to fold in a single step
840 let mu = 32;
841 let nu = 42;
842
843 let mut z_lcccs = Vec::new();
844 for i in 0..mu {
845 let z = get_test_z(i + 3);
846 z_lcccs.push(z);
847 }
848 let mut z_cccs = Vec::new();
849 for i in 0..nu {
850 let z = get_test_z(i + 3);
851 z_cccs.push(z);
852 }
853
854 let ccs: CCS<Fr> = get_test_ccs();
855
856 let mut rng = test_rng();
857 let gamma: Fr = Fr::rand(&mut rng);
858 let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
859 let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
860
861 let (pedersen_params, _) =
862 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
863
864 // Create the LCCCS instances out of z_lcccs
865 let mut lcccs_instances = Vec::new();
866 for z_i in z_lcccs.iter() {
867 let (inst, _) = ccs
868 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
869 .unwrap();
870 lcccs_instances.push(inst);
871 }
872 // Create the CCCS instance out of z_cccs
873 let mut cccs_instances = Vec::new();
874 for z_i in z_cccs.iter() {
875 let (inst, _) = ccs
876 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
877 .unwrap();
878 cccs_instances.push(inst);
879 }
880
881 let sigmas_thetas = compute_sigmas_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime).unwrap();
882
883 let expected_c = compute_c(
884 &ccs,
885 &sigmas_thetas,
886 gamma,
887 &beta,
888 &lcccs_instances
889 .iter()
890 .map(|lcccs| lcccs.r_x.clone())
891 .collect(),
892 &r_x_prime,
893 )
894 .unwrap();
895
896 let cs = ConstraintSystem::<Fr>::new_ref();
897 let mut vec_sigmas = Vec::new();
898 let mut vec_thetas = Vec::new();
899 for sigmas in sigmas_thetas.0 {
900 vec_sigmas
901 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap());
902 }
903 for thetas in sigmas_thetas.1 {
904 vec_thetas
905 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap());
906 }
907 let vec_r_x: Vec<Vec<FpVar<Fr>>> = lcccs_instances
908 .iter()
909 .map(|lcccs| {
910 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap()
911 })
912 .collect();
913 let vec_r_x_prime =
914 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap();
915 let gamma_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(gamma)).unwrap();
916 let beta_var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap();
917
918 let computed_c = compute_c_gadget(
919 cs.clone(),
920 &ccs,
921 vec_sigmas,
922 vec_thetas,
923 gamma_var,
924 beta_var,
925 vec_r_x,
926 vec_r_x_prime,
927 )
928 .unwrap();
929
930 assert_eq!(expected_c, computed_c.value().unwrap());
931 }
932
933 /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step,
934 /// to verify the folding in the NIMFSGadget circuit
935 #[test]
936 pub fn test_nimfs_gadget_verify() {
937 let mut rng = test_rng();
938
939 // Create a basic CCS circuit
940 let ccs = get_test_ccs::<Fr>();
941 let (pedersen_params, _) =
942 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
943
944 let mu = 32;
945 let nu = 42;
946
947 // Generate a mu LCCCS & nu CCCS satisfying witness
948 let mut z_lcccs = Vec::new();
949 for i in 0..mu {
950 let z = get_test_z(i + 3);
951 z_lcccs.push(z);
952 }
953 let mut z_cccs = Vec::new();
954 for i in 0..nu {
955 let z = get_test_z(nu + i + 3);
956 z_cccs.push(z);
957 }
958
959 // Create the LCCCS instances out of z_lcccs
960 let mut lcccs_instances = Vec::new();
961 let mut w_lcccs = Vec::new();
962 for z_i in z_lcccs.iter() {
963 let (running_instance, w) = ccs
964 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
965 .unwrap();
966 lcccs_instances.push(running_instance);
967 w_lcccs.push(w);
968 }
969 // Create the CCCS instance out of z_cccs
970 let mut cccs_instances = Vec::new();
971 let mut w_cccs = Vec::new();
972 for z_i in z_cccs.iter() {
973 let (new_instance, w) = ccs
974 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
975 .unwrap();
976 cccs_instances.push(new_instance);
977 w_cccs.push(w);
978 }
979
980 // Prover's transcript
981 let poseidon_config = poseidon_canonical_config::<Fr>();
982 let mut transcript_p: PoseidonSponge<Fr> = PoseidonSponge::<Fr>::new(&poseidon_config);
983
984 // Run the prover side of the multifolding
985 let (proof, folded_lcccs, folded_witness, _) =
986 NIMFS::<Projective, PoseidonSponge<Fr>>::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: PoseidonSponge<Fr> = PoseidonSponge::<Fr>::new(&poseidon_config);
998
999 // Run the verifier side of the multifolding
1000 let folded_lcccs_v = NIMFS::<Projective, PoseidonSponge<Fr>>::verify(
1001 &mut transcript_v,
1002 &ccs,
1003 &lcccs_instances,
1004 &cccs_instances,
1005 proof.clone(),
1006 )
1007 .unwrap();
1008 assert_eq!(folded_lcccs, folded_lcccs_v);
1009
1010 // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
1011 folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
1012
1013 // allocate circuit inputs
1014 let cs = ConstraintSystem::<Fr>::new_ref();
1015 let lcccs_instancesVar =
1016 Vec::<LCCCSVar<Projective>>::new_witness(cs.clone(), || Ok(lcccs_instances.clone()))
1017 .unwrap();
1018 let cccs_instancesVar =
1019 Vec::<CCCSVar<Projective>>::new_witness(cs.clone(), || Ok(cccs_instances.clone()))
1020 .unwrap();
1021 let proofVar =
1022 ProofVar::<Projective>::new_witness(cs.clone(), || Ok(proof.clone())).unwrap();
1023 let mut transcriptVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1024
1025 let enabled = Boolean::<Fr>::new_witness(cs.clone(), || Ok(true)).unwrap();
1026 let (folded_lcccsVar, _) = NIMFSGadget::<Projective>::verify(
1027 cs.clone(),
1028 &ccs,
1029 &mut transcriptVar,
1030 &lcccs_instancesVar,
1031 &cccs_instancesVar,
1032 proofVar,
1033 enabled,
1034 )
1035 .unwrap();
1036 assert!(cs.is_satisfied().unwrap());
1037 assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u);
1038 }
1039
1040 /// test that checks the native LCCCS.hash vs the R1CS constraints version
1041 #[test]
1042 pub fn test_lcccs_hash() {
1043 let mut rng = test_rng();
1044 let poseidon_config = poseidon_canonical_config::<Fr>();
1045 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
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 let pp_hash = Fr::from(42u32); // only for test
1053
1054 let i = Fr::from(3_u32);
1055 let z_0 = vec![Fr::from(3_u32)];
1056 let z_i = vec![Fr::from(3_u32)];
1057 let (lcccs, _) = ccs
1058 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, &z1)
1059 .unwrap();
1060 let h = lcccs
1061 .clone()
1062 .hash(&sponge, pp_hash, i, z_0.clone(), z_i.clone());
1063
1064 let cs = ConstraintSystem::<Fr>::new_ref();
1065
1066 let spongeVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1067 let pp_hashVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(pp_hash)).unwrap();
1068 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
1069 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
1070 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
1071 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
1072 let (hVar, _) = lcccsVar
1073 .clone()
1074 .hash(
1075 &spongeVar,
1076 pp_hashVar,
1077 iVar.clone(),
1078 z_0Var.clone(),
1079 z_iVar.clone(),
1080 )
1081 .unwrap();
1082 assert!(cs.is_satisfied().unwrap());
1083
1084 // check that the natively computed and in-circuit computed hashes match
1085 assert_eq!(hVar.value().unwrap(), h);
1086 }
1087
1088 #[test]
1089 pub fn test_augmented_f_circuit() {
1090 let mut rng = test_rng();
1091 let poseidon_config = poseidon_canonical_config::<Fr>();
1092 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1093
1094 let start = Instant::now();
1095 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
1096 let mut augmented_f_circuit = AugmentedFCircuit::<
1097 Projective,
1098 Projective2,
1099 GVar2,
1100 CubicFCircuit<Fr>,
1101 >::empty(&poseidon_config, F_circuit, None)
1102 .unwrap();
1103 let ccs = augmented_f_circuit.ccs.clone();
1104 println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed());
1105 println!("CCS m x n: {} x {}", ccs.m, ccs.n);
1106
1107 // CycleFold circuit
1108 let cs2 = ConstraintSystem::<Fq>::new_ref();
1109 let cf_circuit = CycleFoldCircuit::<Projective, GVar>::empty();
1110 cf_circuit.generate_constraints(cs2.clone()).unwrap();
1111 cs2.finalize();
1112 let cs2 = cs2
1113 .into_inner()
1114 .ok_or(Error::NoInnerConstraintSystem)
1115 .unwrap();
1116 let cf_r1cs = extract_r1cs::<Fq>(&cs2);
1117
1118 let (pedersen_params, _) =
1119 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1120 let (cf_pedersen_params, _) =
1121 Pedersen::<Projective2>::setup(&mut rng, cf_r1cs.A.n_cols - cf_r1cs.l - 1).unwrap();
1122
1123 // public params hash
1124 let pp_hash = Fr::from(42u32); // only for test
1125
1126 // first step
1127 let z_0 = vec![Fr::from(3_u32)];
1128 let mut z_i = z_0.clone();
1129
1130 // prepare the dummy instances
1131 let W_dummy = Witness::<Fr>::dummy(&ccs);
1132 let U_dummy = LCCCS::<Projective>::dummy(ccs.l, ccs.t, ccs.s);
1133 let w_dummy = W_dummy.clone();
1134 let u_dummy = CCCS::<Projective>::dummy(ccs.l);
1135 let (cf_W_dummy, cf_U_dummy): (NovaWitness<Projective2>, CommittedInstance<Projective2>) =
1136 cf_r1cs.dummy_instance();
1137
1138 // set the initial dummy instances
1139 let mut W_i = W_dummy.clone();
1140 let mut U_i = U_dummy.clone();
1141 let mut w_i = w_dummy.clone();
1142 let mut u_i = u_dummy.clone();
1143 let mut cf_W_i = cf_W_dummy.clone();
1144 let mut cf_U_i = cf_U_dummy.clone();
1145 u_i.x = vec![
1146 U_i.hash(&sponge, pp_hash, Fr::zero(), z_0.clone(), z_i.clone()),
1147 cf_U_i.hash_cyclefold(&sponge, pp_hash),
1148 ];
1149
1150 let n_steps: usize = 4;
1151 let mut iFr = Fr::zero();
1152 for i in 0..n_steps {
1153 let start = Instant::now();
1154
1155 let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap();
1156
1157 let (U_i1, W_i1);
1158
1159 if i == 0 {
1160 W_i1 = Witness::<Fr>::dummy(&ccs);
1161 U_i1 = LCCCS::dummy(ccs.l, ccs.t, ccs.s);
1162
1163 let u_i1_x = U_i1.hash(&sponge, pp_hash, Fr::one(), z_0.clone(), z_i1.clone());
1164
1165 // hash the initial (dummy) CycleFold instance, which is used as the 2nd public
1166 // input in the AugmentedFCircuit
1167 let cf_u_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1168
1169 augmented_f_circuit =
1170 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1171 _c2: PhantomData,
1172 _gc2: PhantomData,
1173 poseidon_config: poseidon_config.clone(),
1174 ccs: ccs.clone(),
1175 pp_hash: Some(pp_hash),
1176 i: Some(Fr::zero()),
1177 i_usize: Some(0),
1178 z_0: Some(z_0.clone()),
1179 z_i: Some(z_i.clone()),
1180 external_inputs: Some(vec![]),
1181 u_i_C: Some(u_i.C),
1182 U_i: Some(U_i.clone()),
1183 U_i1_C: Some(U_i1.C),
1184 F: F_circuit,
1185 x: Some(u_i1_x),
1186 nimfs_proof: None,
1187
1188 // cyclefold values
1189 cf_u_i_cmW: None,
1190 cf_U_i: None,
1191 cf_x: Some(cf_u_i1_x),
1192 cf_cmT: None,
1193 };
1194 } else {
1195 let mut transcript_p: PoseidonSponge<Fr> =
1196 PoseidonSponge::<Fr>::new(&poseidon_config.clone());
1197 transcript_p.absorb(&pp_hash);
1198 let (rho_bits, nimfs_proof);
1199 (nimfs_proof, U_i1, W_i1, rho_bits) =
1200 NIMFS::<Projective, PoseidonSponge<Fr>>::prove(
1201 &mut transcript_p,
1202 &ccs,
1203 &[U_i.clone()],
1204 &[u_i.clone()],
1205 &[W_i.clone()],
1206 &[w_i.clone()],
1207 )
1208 .unwrap();
1209
1210 // sanity check: check the folded instance relation
1211 U_i1.check_relation(&ccs, &W_i1).unwrap();
1212
1213 let u_i1_x =
1214 U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), z_0.clone(), z_i1.clone());
1215
1216 let rho_Fq = Fq::from_bigint(BigInteger::from_bits_le(&rho_bits)).unwrap();
1217 // CycleFold part:
1218 // get the vector used as public inputs 'x' in the CycleFold circuit
1219 // cyclefold circuit for cmW
1220 let cf_u_i_x = [
1221 vec![rho_Fq],
1222 get_cm_coordinates(&U_i.C),
1223 get_cm_coordinates(&u_i.C),
1224 get_cm_coordinates(&U_i1.C),
1225 ]
1226 .concat();
1227
1228 let cf_circuit = CycleFoldCircuit::<Projective, GVar> {
1229 _gc: PhantomData,
1230 r_bits: Some(rho_bits.clone()),
1231 p1: Some(U_i.clone().C),
1232 p2: Some(u_i.clone().C),
1233 x: Some(cf_u_i_x.clone()),
1234 };
1235
1236 let (_cf_w_i, cf_u_i, cf_W_i1, cf_U_i1, cf_cmT, _) = fold_cyclefold_circuit::<
1237 Projective,
1238 GVar,
1239 Projective2,
1240 GVar2,
1241 CubicFCircuit<Fr>,
1242 Pedersen<Projective>,
1243 Pedersen<Projective2>,
1244 >(
1245 &mut transcript_p,
1246 cf_r1cs.clone(),
1247 cf_pedersen_params.clone(),
1248 pp_hash,
1249 cf_W_i.clone(), // CycleFold running instance witness
1250 cf_U_i.clone(), // CycleFold running instance
1251 cf_u_i_x, // CycleFold incoming instance
1252 cf_circuit,
1253 )
1254 .unwrap();
1255
1256 // hash the CycleFold folded instance, which is used as the 2nd public input in the
1257 // AugmentedFCircuit
1258 let cf_u_i1_x = cf_U_i1.hash_cyclefold(&sponge, pp_hash);
1259
1260 augmented_f_circuit =
1261 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1262 _c2: PhantomData,
1263 _gc2: PhantomData,
1264 poseidon_config: poseidon_config.clone(),
1265 ccs: ccs.clone(),
1266 pp_hash: Some(pp_hash),
1267 i: Some(iFr),
1268 i_usize: Some(i),
1269 z_0: Some(z_0.clone()),
1270 z_i: Some(z_i.clone()),
1271 external_inputs: Some(vec![]),
1272 u_i_C: Some(u_i.C),
1273 U_i: Some(U_i.clone()),
1274 U_i1_C: Some(U_i1.C),
1275 F: F_circuit,
1276 x: Some(u_i1_x),
1277 nimfs_proof: Some(nimfs_proof),
1278
1279 // cyclefold values
1280 cf_u_i_cmW: Some(cf_u_i.cmW),
1281 cf_U_i: Some(cf_U_i),
1282 cf_x: Some(cf_u_i1_x),
1283 cf_cmT: Some(cf_cmT),
1284 };
1285
1286 // assign the next round instances
1287 cf_W_i = cf_W_i1;
1288 cf_U_i = cf_U_i1;
1289 }
1290
1291 let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap();
1292 assert!(cs.is_satisfied().unwrap());
1293
1294 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<Fr>(&cs); // includes 1 and public inputs
1295 assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap());
1296 let r1cs_z = [vec![Fr::one()], r1cs_x_i1.clone(), r1cs_w_i1.clone()].concat();
1297 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
1298 // assign them directly to w_i, u_i.
1299 (u_i, w_i) = ccs
1300 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, &r1cs_z)
1301 .unwrap();
1302 u_i.check_relation(&ccs, &w_i).unwrap();
1303
1304 // sanity checks
1305 assert_eq!(w_i.w, r1cs_w_i1);
1306 assert_eq!(u_i.x, r1cs_x_i1);
1307 assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap());
1308 assert_eq!(u_i.x[1], augmented_f_circuit.cf_x.unwrap());
1309 let expected_u_i1_x =
1310 U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), z_0.clone(), z_i1.clone());
1311 let expected_cf_U_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1312 // u_i is already u_i1 at this point, check that has the expected value at x[0]
1313 assert_eq!(u_i.x[0], expected_u_i1_x);
1314 assert_eq!(u_i.x[1], expected_cf_U_i1_x);
1315
1316 // set values for next iteration
1317 iFr += Fr::one();
1318 // assign z_{i+1} into z_i
1319 z_i = z_i1.clone();
1320 U_i = U_i1.clone();
1321 W_i = W_i1.clone();
1322
1323 // check the new LCCCS instance relation
1324 U_i.check_relation(&ccs, &W_i).unwrap();
1325 // check the new CCCS instance relation
1326 u_i.check_relation(&ccs, &w_i).unwrap();
1327
1328 // check the CycleFold instance relation
1329 cf_r1cs
1330 .check_relaxed_instance_relation(&cf_W_i, &cf_U_i)
1331 .unwrap();
1332
1333 println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
1334 }
1335 }
1336}