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, ToBitsGadget, 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 cf_io_len, CycleFoldChallengeGadget, CycleFoldCommittedInstanceVar, NIFSFullGadget,
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_powers, 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
232 running_instances: &[LCCCSVar<C>], // U
233 new_instances: &[CCCSVar<C>], // u
234 proof: ProofVar<C>,
235 enabled: Boolean<C::ScalarField>,
236 ) -> Result<(LCCCSVar<C>, Vec<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(&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(&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::ScalarField>::verify(
287 &proof.sc_proof,
288 &vp_aux_info,
289 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 // Self::fold will return the folded instance, together with the rho's powers vector so
320 // they can be used in other parts of the AugmentedFCircuit
321 Self::fold(
322 running_instances,
323 new_instances,
324 proof.sigmas_thetas,
325 r_x_prime,
326 rho,
327 )
328 }
329
330 /// Runs (in-circuit) the verifier side of the fold, computing the new folded LCCCS instance
331 #[allow(clippy::type_complexity)]
332 fn fold(
333 lcccs: &[LCCCSVar<C>],
334 cccs: &[CCCSVar<C>],
335 sigmas_thetas: (Vec<Vec<FpVar<CF1<C>>>>, Vec<Vec<FpVar<CF1<C>>>>),
336 r_x_prime: Vec<FpVar<CF1<C>>>,
337 rho: FpVar<CF1<C>>,
338 ) -> Result<(LCCCSVar<C>, Vec<Vec<Boolean<CF1<C>>>>), SynthesisError> {
339 let (sigmas, thetas) = (sigmas_thetas.0.clone(), sigmas_thetas.1.clone());
340 let mut u_folded: FpVar<CF1<C>> = FpVar::zero();
341 let mut x_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); lcccs[0].x.len()];
342 let mut v_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); sigmas[0].len()];
343
344 let mut rho_vec: Vec<Vec<Boolean<CF1<C>>>> =
345 vec![vec![Boolean::FALSE; N_BITS_RO]; lcccs.len() + cccs.len() - 1];
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 // compute the next power of rho
383 rho_i *= rho.clone();
384 // crop the size of rho_i to N_BITS_RO
385 let rho_i_bits = rho_i.to_bits_le()?;
386 rho_i = Boolean::le_bits_to_fp_var(&rho_i_bits[..N_BITS_RO])?;
387 if i < lcccs.len() + cccs.len() - 1 {
388 // store the cropped rho_i into the rho_vec
389 rho_vec[i] = rho_i_bits[..N_BITS_RO].to_vec();
390 }
391 }
392
393 // return the folded instance, together with the rho's powers vector so they can be used in
394 // other parts of the AugmentedFCircuit
395 Ok((
396 LCCCSVar::<C> {
397 // C this is later overwritten by the U_{i+1}.C value checked by the cyclefold circuit
398 C: lcccs[0].C.clone(),
399 u: u_folded,
400 x: x_folded,
401 r_x: r_x_prime,
402 v: v_folded,
403 },
404 rho_vec,
405 ))
406 }
407}
408
409/// Computes c from the step 5 in section 5 of HyperNova, adapted to multiple LCCCS & CCCS
410/// instances:
411/// $$
412/// c = \sum_{i \in [\mu]} \left(\sum_{j \in [t]} \gamma^{i \cdot t + j} \cdot e_i \cdot \sigma_{i,j} \right)
413/// + \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}
414/// \theta_{k,j} \right)
415/// $$
416#[allow(clippy::too_many_arguments)]
417fn compute_c_gadget<F: PrimeField>(
418 cs: ConstraintSystemRef<F>,
419 ccs: &CCS<F>,
420 vec_sigmas: Vec<Vec<FpVar<F>>>,
421 vec_thetas: Vec<Vec<FpVar<F>>>,
422 gamma: FpVar<F>,
423 beta: Vec<FpVar<F>>,
424 vec_r_x: Vec<Vec<FpVar<F>>>,
425 vec_r_x_prime: Vec<FpVar<F>>,
426) -> Result<FpVar<F>, SynthesisError> {
427 let mut e_lcccs = Vec::new();
428 for r_x in vec_r_x.iter() {
429 e_lcccs.push(EqEvalGadget::eq_eval(r_x, &vec_r_x_prime)?);
430 }
431
432 let mut c = FpVar::<F>::zero();
433 let mut current_gamma = FpVar::<F>::one();
434 for i in 0..vec_sigmas.len() {
435 for j in 0..ccs.t {
436 c += current_gamma.clone() * e_lcccs[i].clone() * vec_sigmas[i][j].clone();
437 current_gamma *= gamma.clone();
438 }
439 }
440
441 let ccs_c = Vec::<FpVar<F>>::new_constant(cs.clone(), ccs.c.clone())?;
442 let e_k = EqEvalGadget::eq_eval(&beta, &vec_r_x_prime)?;
443 #[allow(clippy::needless_range_loop)]
444 for k in 0..vec_thetas.len() {
445 let mut sum = FpVar::<F>::zero();
446 for i in 0..ccs.q {
447 let mut prod = FpVar::<F>::one();
448 for j in ccs.S[i].clone() {
449 prod *= vec_thetas[k][j].clone();
450 }
451 sum += ccs_c[i].clone() * prod;
452 }
453 c += current_gamma.clone() * e_k.clone() * sum;
454 current_gamma *= gamma.clone();
455 }
456 Ok(c)
457}
458
459#[derive(Debug, Clone)]
460pub struct AugmentedFCircuit<
461 C1: CurveGroup,
462 C2: CurveGroup,
463 GC2: CurveVar<C2, CF2<C2>>,
464 FC: FCircuit<CF1<C1>>,
465> where
466 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
467{
468 pub _c2: PhantomData<C2>,
469 pub _gc2: PhantomData<GC2>,
470 pub poseidon_config: PoseidonConfig<CF1<C1>>,
471 pub ccs: CCS<C1::ScalarField>, // CCS of the AugmentedFCircuit
472 pub pp_hash: Option<CF1<C1>>,
473 pub mu: usize, // max number of LCCCS instances to be folded
474 pub nu: usize, // max number of CCCS instances to be folded
475 pub i: Option<CF1<C1>>,
476 pub i_usize: Option<usize>,
477 pub z_0: Option<Vec<C1::ScalarField>>,
478 pub z_i: Option<Vec<C1::ScalarField>>,
479 pub external_inputs: Option<Vec<C1::ScalarField>>,
480 pub U_i: Option<LCCCS<C1>>,
481 pub Us: Option<Vec<LCCCS<C1>>>, // other U_i's to be folded that are not the main running instance
482 pub u_i_C: Option<C1>, // u_i.C
483 pub us: Option<Vec<CCCS<C1>>>, // other u_i's to be folded that are not the main incoming instance
484 pub U_i1_C: Option<C1>, // U_{i+1}.C
485 pub F: FC, // F circuit
486 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
487 pub nimfs_proof: Option<NIMFSProof<C1>>,
488
489 // cyclefold verifier on C1
490 pub cf_u_i_cmW: Option<C2>, // input, cf_u_i.cmW
491 pub cf_U_i: Option<CommittedInstance<C2>>, // input, RelaxedR1CS CycleFold instance
492 pub cf_x: Option<CF1<C1>>, // public input (cf_u_{i+1}.x[1])
493 pub cf_cmT: Option<C2>,
494}
495
496impl<C1, C2, GC2, FC> AugmentedFCircuit<C1, C2, GC2, FC>
497where
498 C1: CurveGroup,
499 C2: CurveGroup,
500 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
501 FC: FCircuit<CF1<C1>>,
502 <C1 as CurveGroup>::BaseField: PrimeField,
503 <C2 as CurveGroup>::BaseField: PrimeField,
504 <C1 as Group>::ScalarField: Absorb,
505 <C2 as Group>::ScalarField: Absorb,
506 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
507 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
508{
509 pub fn default(
510 poseidon_config: &PoseidonConfig<CF1<C1>>,
511 F_circuit: FC,
512 ccs: CCS<C1::ScalarField>,
513 mu: usize,
514 nu: usize,
515 ) -> Result<Self, Error> {
516 if mu < 1 || nu < 1 {
517 return Err(Error::CantBeZero("mu,nu".to_string()));
518 }
519 Ok(Self {
520 _c2: PhantomData,
521 _gc2: PhantomData,
522 poseidon_config: poseidon_config.clone(),
523 ccs,
524 pp_hash: None,
525 mu,
526 nu,
527 i: None,
528 i_usize: None,
529 z_0: None,
530 z_i: None,
531 external_inputs: None,
532 U_i: None,
533 Us: None,
534 u_i_C: None,
535 us: None,
536 U_i1_C: None,
537 F: F_circuit,
538 x: None,
539 nimfs_proof: None,
540 cf_u_i_cmW: None,
541 cf_U_i: None,
542 cf_x: None,
543 cf_cmT: None,
544 })
545 }
546
547 pub fn empty(
548 poseidon_config: &PoseidonConfig<CF1<C1>>,
549 F: FC, // FCircuit
550 ccs: Option<CCS<C1::ScalarField>>,
551 mu: usize,
552 nu: usize,
553 ) -> Result<Self, Error> {
554 let initial_ccs = CCS {
555 // m, n, s, s_prime and M will be overwritten by the `upper_bound_ccs' method
556 m: 0,
557 n: 0,
558 l: 2, // io_len
559 s: 1,
560 s_prime: 1,
561 t: 3, // note: this is only supports R1CS for the moment
562 q: 2,
563 d: 2,
564 S: vec![vec![0, 1], vec![2]],
565 c: vec![C1::ScalarField::one(), C1::ScalarField::one().neg()],
566 M: vec![],
567 };
568 let mut augmented_f_circuit = Self::default(poseidon_config, F, initial_ccs, mu, nu)?;
569 if ccs.is_some() {
570 augmented_f_circuit.ccs = ccs.unwrap();
571 } else {
572 augmented_f_circuit.ccs = augmented_f_circuit.upper_bound_ccs()?;
573 }
574 Ok(augmented_f_circuit)
575 }
576
577 /// This method computes the CCS parameters. This is used because there is a circular
578 /// dependency between the AugmentedFCircuit CCS and the CCS parameters m & n & s & s'.
579 /// For a stable FCircuit circuit, the CCS parameters can be computed in advance and can be
580 /// feed in as parameter for the AugmentedFCircuit::empty method to avoid computing them there.
581 pub fn upper_bound_ccs(&self) -> Result<CCS<C1::ScalarField>, Error> {
582 let r1cs = get_r1cs_from_cs::<CF1<C1>>(self.clone()).unwrap();
583 let mut ccs = CCS::from_r1cs(r1cs.clone());
584
585 let z_0 = vec![C1::ScalarField::zero(); self.F.state_len()];
586 let mut W_i = Witness::<C1::ScalarField>::dummy(&ccs);
587 let mut U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
588 let mut w_i = W_i.clone();
589 let mut u_i = CCCS::<C1>::dummy(ccs.l);
590
591 let n_iters = 2;
592 for _ in 0..n_iters {
593 let Us = vec![U_i.clone(); self.mu - 1];
594 let Ws = vec![W_i.clone(); self.mu - 1];
595 let us = vec![u_i.clone(); self.nu - 1];
596 let ws = vec![w_i.clone(); self.nu - 1];
597
598 let all_Us = [vec![U_i.clone()], Us.clone()].concat();
599 let all_us = [vec![u_i.clone()], us.clone()].concat();
600 let all_Ws = [vec![W_i.clone()], Ws].concat();
601 let all_ws = [vec![w_i.clone()], ws].concat();
602
603 let mut transcript_p: PoseidonSponge<C1::ScalarField> =
604 PoseidonSponge::<C1::ScalarField>::new(&self.poseidon_config.clone());
605 // since this is only for the number of constraints, no need to absorb the pp_hash here
606 let (nimfs_proof, U_i1, _, _) = NIMFS::<C1, PoseidonSponge<C1::ScalarField>>::prove(
607 &mut transcript_p,
608 &ccs,
609 &all_Us,
610 &all_us,
611 &all_Ws,
612 &all_ws,
613 )?;
614
615 let augmented_f_circuit = Self {
616 _c2: PhantomData,
617 _gc2: PhantomData,
618 poseidon_config: self.poseidon_config.clone(),
619 ccs: ccs.clone(),
620 pp_hash: Some(C1::ScalarField::zero()),
621 mu: self.mu,
622 nu: self.nu,
623 i: Some(C1::ScalarField::zero()),
624 i_usize: Some(0),
625 z_0: Some(z_0.clone()),
626 z_i: Some(z_0.clone()),
627 external_inputs: Some(vec![C1::ScalarField::zero(); self.F.external_inputs_len()]),
628 U_i: Some(U_i.clone()),
629 Us: Some(Us),
630 u_i_C: Some(u_i.C),
631 us: Some(us),
632 U_i1_C: Some(U_i1.C),
633 F: self.F.clone(),
634 x: Some(C1::ScalarField::zero()),
635 nimfs_proof: Some(nimfs_proof),
636 // cyclefold values
637 cf_u_i_cmW: None,
638 cf_U_i: None,
639 cf_x: None,
640 cf_cmT: None,
641 };
642
643 let cs: ConstraintSystem<C1::ScalarField>;
644 (cs, ccs) = augmented_f_circuit.compute_cs_ccs()?;
645 // prepare instances for next loop iteration
646 use crate::arith::r1cs::extract_w_x;
647 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<C1::ScalarField>(&cs);
648 u_i = CCCS::<C1> {
649 C: u_i.C,
650 x: r1cs_x_i1,
651 };
652 w_i = Witness::<C1::ScalarField> {
653 w: r1cs_w_i1.clone(),
654 r_w: C1::ScalarField::one(),
655 };
656 W_i = Witness::<C1::ScalarField>::dummy(&ccs);
657 U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
658 }
659 Ok(ccs)
660
661 // Ok(augmented_f_circuit.compute_cs_ccs()?.1)
662 }
663
664 /// Returns the cs (ConstraintSystem) and the CCS out of the AugmentedFCircuit
665 #[allow(clippy::type_complexity)]
666 pub fn compute_cs_ccs(
667 &self,
668 ) -> Result<(ConstraintSystem<C1::ScalarField>, CCS<C1::ScalarField>), Error> {
669 let cs = ConstraintSystem::<C1::ScalarField>::new_ref();
670 self.clone().generate_constraints(cs.clone())?;
671 cs.finalize();
672 let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?;
673 let r1cs = extract_r1cs::<C1::ScalarField>(&cs);
674 let ccs = CCS::from_r1cs(r1cs.clone());
675
676 Ok((cs, ccs))
677 }
678}
679
680impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
681where
682 C1: CurveGroup,
683 C2: CurveGroup,
684 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
685 FC: FCircuit<CF1<C1>>,
686 <C1 as CurveGroup>::BaseField: PrimeField,
687 <C2 as CurveGroup>::BaseField: PrimeField,
688 <C1 as Group>::ScalarField: Absorb,
689 <C2 as Group>::ScalarField: Absorb,
690 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
691 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
692{
693 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
694 let pp_hash = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
695 Ok(self.pp_hash.unwrap_or_else(CF1::<C1>::zero))
696 })?;
697 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
698 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
699 })?;
700 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
701 Ok(self
702 .z_0
703 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
704 })?;
705 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
706 Ok(self
707 .z_i
708 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
709 })?;
710 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
711 Ok(self
712 .external_inputs
713 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
714 })?;
715
716 let U_dummy = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
717 let u_dummy = CCCS::<C1>::dummy(self.ccs.l);
718
719 let U_i =
720 LCCCSVar::<C1>::new_witness(cs.clone(), || Ok(self.U_i.unwrap_or(U_dummy.clone())))?;
721 let Us = Vec::<LCCCSVar<C1>>::new_witness(cs.clone(), || {
722 Ok(self.Us.unwrap_or(vec![U_dummy.clone(); self.mu - 1]))
723 })?;
724 let us = Vec::<CCCSVar<C1>>::new_witness(cs.clone(), || {
725 Ok(self.us.unwrap_or(vec![u_dummy.clone(); self.mu - 1]))
726 })?;
727 let U_i1_C = NonNativeAffineVar::new_witness(cs.clone(), || {
728 Ok(self.U_i1_C.unwrap_or_else(C1::zero))
729 })?;
730 let nimfs_proof_dummy = NIMFSProof::<C1>::dummy(&self.ccs, self.mu, self.nu);
731 let nimfs_proof = ProofVar::<C1>::new_witness(cs.clone(), || {
732 Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy))
733 })?;
734
735 let cf_u_dummy = CommittedInstance::dummy(cf_io_len(self.mu + self.nu));
736 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
737 Ok(self.cf_U_i.unwrap_or(cf_u_dummy.clone()))
738 })?;
739 let cf_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf_cmT.unwrap_or_else(C2::zero)))?;
740
741 let sponge = PoseidonSpongeVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
742
743 // get z_{i+1} from the F circuit
744 let i_usize = self.i_usize.unwrap_or(0);
745 let z_i1 =
746 self.F
747 .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?;
748
749 let is_basecase = i.is_zero()?;
750 let is_not_basecase = is_basecase.not();
751
752 // Primary Part
753 // P.1. Compute u_i.x
754 // u_i.x[0] = H(i, z_0, z_i, U_i)
755 let (u_i_x, _) = U_i.clone().hash(
756 &sponge,
757 pp_hash.clone(),
758 i.clone(),
759 z_0.clone(),
760 z_i.clone(),
761 )?;
762 // u_i.x[1] = H(cf_U_i)
763 let (cf_u_i_x, cf_U_i_vec) = cf_U_i.clone().hash(&sponge, pp_hash.clone())?;
764
765 // P.2. Construct u_i
766 let u_i = CCCSVar::<C1> {
767 // u_i.C is provided by the prover as witness
768 C: NonNativeAffineVar::<C1>::new_witness(cs.clone(), || {
769 Ok(self.u_i_C.unwrap_or(C1::zero()))
770 })?,
771 // u_i.x is computed in step 1
772 x: vec![u_i_x, cf_u_i_x],
773 };
774
775 let all_Us = [vec![U_i.clone()], Us].concat();
776 let all_us = [vec![u_i.clone()], us].concat();
777
778 // P.3. NIMFS.verify, obtains U_{i+1} by folding [U_i] & [u_i].
779 // Notice that NIMFSGadget::fold_committed_instance does not fold C. We set `U_i1.C` to
780 // unconstrained witnesses `U_i1_C` respectively. Its correctness will be checked on the
781 // other curve.
782 let mut transcript = PoseidonSpongeVar::new(cs.clone(), &self.poseidon_config);
783 transcript.absorb(&pp_hash)?;
784 let (mut U_i1, rho_vec) = NIMFSGadget::<C1>::verify(
785 cs.clone(),
786 &self.ccs.clone(),
787 &mut transcript,
788 &all_Us,
789 &all_us,
790 nimfs_proof,
791 is_not_basecase.clone(),
792 )?;
793 U_i1.C = U_i1_C;
794
795 // P.4.a compute and check the first output of F'
796 let (u_i1_x, _) = U_i1.clone().hash(
797 &sponge,
798 pp_hash.clone(),
799 i + FpVar::<CF1<C1>>::one(),
800 z_0.clone(),
801 z_i1.clone(),
802 )?;
803 let (u_i1_x_base, _) = LCCCSVar::new_constant(cs.clone(), U_dummy)?.hash(
804 &sponge,
805 pp_hash.clone(),
806 FpVar::<CF1<C1>>::one(),
807 z_0.clone(),
808 z_i1.clone(),
809 )?;
810 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
811 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
812
813 // convert rho_bits of the rho_vec to a `NonNativeFieldVar`
814 let rho_vec_nonnat = rho_vec
815 .iter()
816 .map(|rho_i| {
817 let mut bits = rho_i.clone();
818 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
819 NonNativeUintVar::from(&bits)
820 })
821 .collect();
822
823 // CycleFold part
824 // C.1. Compute cf1_u_i.x and cf2_u_i.x
825 let cf_x: Vec<NonNativeUintVar<CF2<C2>>> = [
826 rho_vec_nonnat,
827 all_Us
828 .iter()
829 .flat_map(|U| vec![U.C.x.clone(), U.C.y.clone()])
830 .collect(),
831 all_us
832 .iter()
833 .flat_map(|u| vec![u.C.x.clone(), u.C.y.clone()])
834 .collect(),
835 vec![U_i1.C.x, U_i1.C.y],
836 ]
837 .concat();
838
839 // ensure that cf_u has as public inputs the C from main instances U_i, u_i, U_i+1
840 // coordinates of the commitments.
841 // C.2. Construct `cf_u_i`
842 let cf_u_i = CycleFoldCommittedInstanceVar::<C2, GC2> {
843 // cf1_u_i.cmE = 0. Notice that we enforce cmE to be equal to 0 since it is allocated
844 // as 0.
845 cmE: GC2::zero(),
846 // cf1_u_i.u = 1
847 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
848 // cf_u_i.cmW is provided by the prover as witness
849 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf_u_i_cmW.unwrap_or(C2::zero())))?,
850 // cf_u_i.x is computed in step 1
851 x: cf_x,
852 };
853
854 // C.3. nifs.verify (fold_committed_instance), obtains cf_U_{i+1} by folding cf_u_i & cf_U_i.
855 // compute cf_r = H(cf_u_i, cf_U_i, cf_cmT)
856 // cf_r_bits is denoted by rho* in the paper.
857 let cf_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
858 &mut transcript,
859 pp_hash.clone(),
860 cf_U_i_vec,
861 cf_u_i.clone(),
862 cf_cmT.clone(),
863 )?;
864 // Convert cf_r_bits to a `NonNativeFieldVar`
865 let cf_r_nonnat = {
866 let mut bits = cf_r_bits.clone();
867 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
868 NonNativeUintVar::from(&bits)
869 };
870 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
871 let cf_U_i1 = NIFSFullGadget::<C2, GC2>::fold_committed_instance(
872 cf_r_bits,
873 cf_r_nonnat,
874 cf_cmT,
875 cf_U_i,
876 cf_u_i,
877 )?;
878
879 // Back to Primary Part
880 // P.4.b compute and check the second output of F'
881 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
882 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
883 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&sponge, pp_hash.clone())?;
884 let (cf_u_i1_x_base, _) =
885 CycleFoldCommittedInstanceVar::new_constant(cs.clone(), cf_u_dummy)?
886 .hash(&sponge, pp_hash)?;
887 let cf_x = FpVar::new_input(cs.clone(), || {
888 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
889 })?;
890 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
891
892 Ok(())
893 }
894}
895
896#[cfg(test)]
897mod tests {
898 use ark_bn254::{constraints::GVar, Fq, Fr, G1Projective as Projective};
899 use ark_ff::BigInteger;
900 use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
901 use ark_std::{test_rng, UniformRand};
902 use std::time::Instant;
903
904 use super::*;
905 use crate::{
906 arith::{
907 ccs::tests::{get_test_ccs, get_test_z},
908 r1cs::extract_w_x,
909 },
910 commitment::{pedersen::Pedersen, CommitmentScheme},
911 folding::{
912 circuits::cyclefold::{fold_cyclefold_circuit, CycleFoldCircuit},
913 hypernova::utils::{compute_c, compute_sigmas_thetas},
914 nova::{traits::NovaR1CS, Witness as NovaWitness},
915 },
916 frontend::tests::CubicFCircuit,
917 transcript::poseidon::poseidon_canonical_config,
918 utils::get_cm_coordinates,
919 };
920
921 #[test]
922 pub fn test_compute_c_gadget() {
923 // number of LCCCS & CCCS instances to fold in a single step
924 let mu = 32;
925 let nu = 42;
926
927 let mut z_lcccs = Vec::new();
928 for i in 0..mu {
929 let z = get_test_z(i + 3);
930 z_lcccs.push(z);
931 }
932 let mut z_cccs = Vec::new();
933 for i in 0..nu {
934 let z = get_test_z(i + 3);
935 z_cccs.push(z);
936 }
937
938 let ccs: CCS<Fr> = get_test_ccs();
939
940 let mut rng = test_rng();
941 let gamma: Fr = Fr::rand(&mut rng);
942 let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
943 let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
944
945 let (pedersen_params, _) =
946 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
947
948 // Create the LCCCS instances out of z_lcccs
949 let mut lcccs_instances = Vec::new();
950 for z_i in z_lcccs.iter() {
951 let (inst, _) = ccs
952 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
953 .unwrap();
954 lcccs_instances.push(inst);
955 }
956 // Create the CCCS instance out of z_cccs
957 let mut cccs_instances = Vec::new();
958 for z_i in z_cccs.iter() {
959 let (inst, _) = ccs
960 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
961 .unwrap();
962 cccs_instances.push(inst);
963 }
964
965 let sigmas_thetas = compute_sigmas_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime).unwrap();
966
967 let expected_c = compute_c(
968 &ccs,
969 &sigmas_thetas,
970 gamma,
971 &beta,
972 &lcccs_instances
973 .iter()
974 .map(|lcccs| lcccs.r_x.clone())
975 .collect(),
976 &r_x_prime,
977 )
978 .unwrap();
979
980 let cs = ConstraintSystem::<Fr>::new_ref();
981 let mut vec_sigmas = Vec::new();
982 let mut vec_thetas = Vec::new();
983 for sigmas in sigmas_thetas.0 {
984 vec_sigmas
985 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap());
986 }
987 for thetas in sigmas_thetas.1 {
988 vec_thetas
989 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap());
990 }
991 let vec_r_x: Vec<Vec<FpVar<Fr>>> = lcccs_instances
992 .iter()
993 .map(|lcccs| {
994 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap()
995 })
996 .collect();
997 let vec_r_x_prime =
998 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap();
999 let gamma_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(gamma)).unwrap();
1000 let beta_var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap();
1001
1002 let computed_c = compute_c_gadget(
1003 cs.clone(),
1004 &ccs,
1005 vec_sigmas,
1006 vec_thetas,
1007 gamma_var,
1008 beta_var,
1009 vec_r_x,
1010 vec_r_x_prime,
1011 )
1012 .unwrap();
1013
1014 assert_eq!(expected_c, computed_c.value().unwrap());
1015 }
1016
1017 /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step,
1018 /// to verify the folding in the NIMFSGadget circuit
1019 #[test]
1020 pub fn test_nimfs_gadget_verify() {
1021 let mut rng = test_rng();
1022
1023 // Create a basic CCS circuit
1024 let ccs = get_test_ccs::<Fr>();
1025 let (pedersen_params, _) =
1026 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1027
1028 let mu = 32;
1029 let nu = 42;
1030
1031 // Generate a mu LCCCS & nu CCCS satisfying witness
1032 let mut z_lcccs = Vec::new();
1033 for i in 0..mu {
1034 let z = get_test_z(i + 3);
1035 z_lcccs.push(z);
1036 }
1037 let mut z_cccs = Vec::new();
1038 for i in 0..nu {
1039 let z = get_test_z(nu + i + 3);
1040 z_cccs.push(z);
1041 }
1042
1043 // Create the LCCCS instances out of z_lcccs
1044 let mut lcccs_instances = Vec::new();
1045 let mut w_lcccs = Vec::new();
1046 for z_i in z_lcccs.iter() {
1047 let (running_instance, w) = ccs
1048 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
1049 .unwrap();
1050 lcccs_instances.push(running_instance);
1051 w_lcccs.push(w);
1052 }
1053 // Create the CCCS instance out of z_cccs
1054 let mut cccs_instances = Vec::new();
1055 let mut w_cccs = Vec::new();
1056 for z_i in z_cccs.iter() {
1057 let (new_instance, w) = ccs
1058 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, z_i)
1059 .unwrap();
1060 cccs_instances.push(new_instance);
1061 w_cccs.push(w);
1062 }
1063
1064 // Prover's transcript
1065 let poseidon_config = poseidon_canonical_config::<Fr>();
1066 let mut transcript_p: PoseidonSponge<Fr> = PoseidonSponge::<Fr>::new(&poseidon_config);
1067
1068 // Run the prover side of the multifolding
1069 let (proof, folded_lcccs, folded_witness, _) =
1070 NIMFS::<Projective, PoseidonSponge<Fr>>::prove(
1071 &mut transcript_p,
1072 &ccs,
1073 &lcccs_instances,
1074 &cccs_instances,
1075 &w_lcccs,
1076 &w_cccs,
1077 )
1078 .unwrap();
1079
1080 // Verifier's transcript
1081 let mut transcript_v: PoseidonSponge<Fr> = PoseidonSponge::<Fr>::new(&poseidon_config);
1082
1083 // Run the verifier side of the multifolding
1084 let folded_lcccs_v = NIMFS::<Projective, PoseidonSponge<Fr>>::verify(
1085 &mut transcript_v,
1086 &ccs,
1087 &lcccs_instances,
1088 &cccs_instances,
1089 proof.clone(),
1090 )
1091 .unwrap();
1092 assert_eq!(folded_lcccs, folded_lcccs_v);
1093
1094 // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
1095 folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
1096
1097 // allocate circuit inputs
1098 let cs = ConstraintSystem::<Fr>::new_ref();
1099 let lcccs_instancesVar =
1100 Vec::<LCCCSVar<Projective>>::new_witness(cs.clone(), || Ok(lcccs_instances.clone()))
1101 .unwrap();
1102 let cccs_instancesVar =
1103 Vec::<CCCSVar<Projective>>::new_witness(cs.clone(), || Ok(cccs_instances.clone()))
1104 .unwrap();
1105 let proofVar =
1106 ProofVar::<Projective>::new_witness(cs.clone(), || Ok(proof.clone())).unwrap();
1107 let mut transcriptVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1108
1109 let enabled = Boolean::<Fr>::new_witness(cs.clone(), || Ok(true)).unwrap();
1110 let (folded_lcccsVar, _) = NIMFSGadget::<Projective>::verify(
1111 cs.clone(),
1112 &ccs,
1113 &mut transcriptVar,
1114 &lcccs_instancesVar,
1115 &cccs_instancesVar,
1116 proofVar,
1117 enabled,
1118 )
1119 .unwrap();
1120 assert!(cs.is_satisfied().unwrap());
1121 assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u);
1122 }
1123
1124 /// test that checks the native LCCCS.hash vs the R1CS constraints version
1125 #[test]
1126 pub fn test_lcccs_hash() {
1127 let mut rng = test_rng();
1128 let poseidon_config = poseidon_canonical_config::<Fr>();
1129 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1130
1131 let ccs = get_test_ccs();
1132 let z1 = get_test_z::<Fr>(3);
1133
1134 let (pedersen_params, _) =
1135 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1136 let pp_hash = Fr::from(42u32); // only for test
1137
1138 let i = Fr::from(3_u32);
1139 let z_0 = vec![Fr::from(3_u32)];
1140 let z_i = vec![Fr::from(3_u32)];
1141 let (lcccs, _) = ccs
1142 .to_lcccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, &z1)
1143 .unwrap();
1144 let h = lcccs
1145 .clone()
1146 .hash(&sponge, pp_hash, i, z_0.clone(), z_i.clone());
1147
1148 let cs = ConstraintSystem::<Fr>::new_ref();
1149
1150 let spongeVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1151 let pp_hashVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(pp_hash)).unwrap();
1152 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
1153 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
1154 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
1155 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
1156 let (hVar, _) = lcccsVar
1157 .clone()
1158 .hash(
1159 &spongeVar,
1160 pp_hashVar,
1161 iVar.clone(),
1162 z_0Var.clone(),
1163 z_iVar.clone(),
1164 )
1165 .unwrap();
1166 assert!(cs.is_satisfied().unwrap());
1167
1168 // check that the natively computed and in-circuit computed hashes match
1169 assert_eq!(hVar.value().unwrap(), h);
1170 }
1171
1172 #[test]
1173 pub fn test_augmented_f_circuit() {
1174 let mut rng = test_rng();
1175 let poseidon_config = poseidon_canonical_config::<Fr>();
1176 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1177
1178 let mu = 3;
1179 let nu = 3;
1180
1181 let start = Instant::now();
1182 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
1183 let mut augmented_f_circuit = AugmentedFCircuit::<
1184 Projective,
1185 Projective2,
1186 GVar2,
1187 CubicFCircuit<Fr>,
1188 >::empty(&poseidon_config, F_circuit, None, mu, nu)
1189 .unwrap();
1190 let ccs = augmented_f_circuit.ccs.clone();
1191 println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed());
1192 println!("CCS m x n: {} x {}", ccs.m, ccs.n);
1193
1194 // CycleFold circuit
1195 let cs2 = ConstraintSystem::<Fq>::new_ref();
1196 let cf_circuit = CycleFoldCircuit::<Projective, GVar>::empty(mu + nu);
1197 cf_circuit.generate_constraints(cs2.clone()).unwrap();
1198 cs2.finalize();
1199 let cs2 = cs2
1200 .into_inner()
1201 .ok_or(Error::NoInnerConstraintSystem)
1202 .unwrap();
1203 let cf_r1cs = extract_r1cs::<Fq>(&cs2);
1204 println!("CF m x n: {} x {}", cf_r1cs.A.n_rows, cf_r1cs.A.n_cols);
1205
1206 let (pedersen_params, _) =
1207 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1208 let (cf_pedersen_params, _) =
1209 Pedersen::<Projective2>::setup(&mut rng, cf_r1cs.A.n_cols - cf_r1cs.l - 1).unwrap();
1210
1211 // public params hash
1212 let pp_hash = Fr::from(42u32); // only for test
1213
1214 // first step
1215 let z_0 = vec![Fr::from(3_u32)];
1216 let mut z_i = z_0.clone();
1217
1218 // prepare the dummy instances
1219 let W_dummy = Witness::<Fr>::dummy(&ccs);
1220 let U_dummy = LCCCS::<Projective>::dummy(ccs.l, ccs.t, ccs.s);
1221 let w_dummy = W_dummy.clone();
1222 let u_dummy = CCCS::<Projective>::dummy(ccs.l);
1223 let (cf_W_dummy, cf_U_dummy): (NovaWitness<Projective2>, CommittedInstance<Projective2>) =
1224 cf_r1cs.dummy_instance();
1225
1226 // set the initial dummy instances
1227 let mut W_i = W_dummy.clone();
1228 let mut U_i = U_dummy.clone();
1229 let mut w_i = w_dummy.clone();
1230 let mut u_i = u_dummy.clone();
1231 let mut cf_W_i = cf_W_dummy.clone();
1232 let mut cf_U_i = cf_U_dummy.clone();
1233 u_i.x = vec![
1234 U_i.hash(&sponge, pp_hash, Fr::zero(), z_0.clone(), z_i.clone()),
1235 cf_U_i.hash_cyclefold(&sponge, pp_hash),
1236 ];
1237
1238 let n_steps: usize = 4;
1239 let mut iFr = Fr::zero();
1240 for i in 0..n_steps {
1241 let start = Instant::now();
1242
1243 // for this test, let Us & us be just an array of copies of the U_i & u_i respectively
1244 let Us = vec![U_i.clone(); mu - 1];
1245 let Ws = vec![W_i.clone(); mu - 1];
1246 let us = vec![u_i.clone(); nu - 1];
1247 let ws = vec![w_i.clone(); nu - 1];
1248 let all_Us = [vec![U_i.clone()], Us.clone()].concat();
1249 let all_us = [vec![u_i.clone()], us.clone()].concat();
1250 let all_Ws = [vec![W_i.clone()], Ws].concat();
1251 let all_ws = [vec![w_i.clone()], ws].concat();
1252
1253 let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap();
1254
1255 let (U_i1, W_i1);
1256
1257 if i == 0 {
1258 W_i1 = Witness::<Fr>::dummy(&ccs);
1259 U_i1 = LCCCS::dummy(ccs.l, ccs.t, ccs.s);
1260
1261 let u_i1_x = U_i1.hash(&sponge, pp_hash, Fr::one(), z_0.clone(), z_i1.clone());
1262
1263 // hash the initial (dummy) CycleFold instance, which is used as the 2nd public
1264 // input in the AugmentedFCircuit
1265 let cf_u_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1266
1267 augmented_f_circuit =
1268 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1269 _c2: PhantomData,
1270 _gc2: PhantomData,
1271 poseidon_config: poseidon_config.clone(),
1272 ccs: ccs.clone(),
1273 pp_hash: Some(pp_hash),
1274 mu,
1275 nu,
1276 i: Some(Fr::zero()),
1277 i_usize: Some(0),
1278 z_0: Some(z_0.clone()),
1279 z_i: Some(z_i.clone()),
1280 external_inputs: Some(vec![]),
1281 U_i: Some(U_i.clone()),
1282 Us: Some(Us.clone()),
1283 u_i_C: Some(u_i.C),
1284 us: Some(us.clone()),
1285 U_i1_C: Some(U_i1.C),
1286 F: F_circuit,
1287 x: Some(u_i1_x),
1288 nimfs_proof: None,
1289
1290 // cyclefold values
1291 cf_u_i_cmW: None,
1292 cf_U_i: None,
1293 cf_x: Some(cf_u_i1_x),
1294 cf_cmT: None,
1295 };
1296 } else {
1297 let mut transcript_p: PoseidonSponge<Fr> =
1298 PoseidonSponge::<Fr>::new(&poseidon_config.clone());
1299 transcript_p.absorb(&pp_hash);
1300 let (rho_powers, nimfs_proof);
1301 (nimfs_proof, U_i1, W_i1, rho_powers) =
1302 NIMFS::<Projective, PoseidonSponge<Fr>>::prove(
1303 &mut transcript_p,
1304 &ccs,
1305 &all_Us,
1306 &all_us,
1307 &all_Ws,
1308 &all_ws,
1309 )
1310 .unwrap();
1311
1312 // sanity check: check the folded instance relation
1313 U_i1.check_relation(&ccs, &W_i1).unwrap();
1314
1315 let u_i1_x =
1316 U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), z_0.clone(), z_i1.clone());
1317
1318 let rho_powers_Fq: Vec<Fq> = rho_powers
1319 .iter()
1320 .map(|rho_i| {
1321 Fq::from_bigint(BigInteger::from_bits_le(&rho_i.into_bigint().to_bits_le()))
1322 .unwrap()
1323 })
1324 .collect();
1325 let rho_powers_bits: Vec<Vec<bool>> = rho_powers
1326 .iter()
1327 .map(|rho_i| rho_i.into_bigint().to_bits_le()[..N_BITS_RO].to_vec())
1328 .collect();
1329
1330 // CycleFold part:
1331 // get the vector used as public inputs 'x' in the CycleFold circuit
1332 let cf_u_i_x = [
1333 // all values for multiple instances
1334 rho_powers_Fq,
1335 get_cm_coordinates(&U_i.C),
1336 Us.iter()
1337 .flat_map(|Us_i| get_cm_coordinates(&Us_i.C))
1338 .collect(),
1339 get_cm_coordinates(&u_i.C),
1340 us.iter()
1341 .flat_map(|us_i| get_cm_coordinates(&us_i.C))
1342 .collect(),
1343 get_cm_coordinates(&U_i1.C),
1344 ]
1345 .concat();
1346
1347 let cf_circuit = CycleFoldCircuit::<Projective, GVar> {
1348 _gc: PhantomData,
1349 n_points: mu + nu,
1350 r_bits: Some(rho_powers_bits.clone()),
1351 points: Some(
1352 [
1353 vec![U_i.clone().C],
1354 Us.iter().map(|Us_i| Us_i.C).collect(),
1355 vec![u_i.clone().C],
1356 us.iter().map(|us_i| us_i.C).collect(),
1357 ]
1358 .concat(),
1359 ),
1360 x: Some(cf_u_i_x.clone()),
1361 };
1362
1363 // ensure that the CycleFoldCircuit is well defined
1364 assert_eq!(
1365 cf_circuit.r_bits.clone().unwrap().len(),
1366 cf_circuit.n_points - 1
1367 );
1368 assert_eq!(
1369 cf_circuit.points.clone().unwrap().len(),
1370 cf_circuit.n_points
1371 );
1372
1373 let (_cf_w_i, cf_u_i, cf_W_i1, cf_U_i1, cf_cmT, _) = fold_cyclefold_circuit::<
1374 Projective,
1375 GVar,
1376 Projective2,
1377 GVar2,
1378 CubicFCircuit<Fr>,
1379 Pedersen<Projective>,
1380 Pedersen<Projective2>,
1381 >(
1382 mu + nu,
1383 &mut transcript_p,
1384 cf_r1cs.clone(),
1385 cf_pedersen_params.clone(),
1386 pp_hash,
1387 cf_W_i.clone(), // CycleFold running instance witness
1388 cf_U_i.clone(), // CycleFold running instance
1389 cf_u_i_x, // CycleFold incoming instance
1390 cf_circuit,
1391 )
1392 .unwrap();
1393
1394 // hash the CycleFold folded instance, which is used as the 2nd public input in the
1395 // AugmentedFCircuit
1396 let cf_u_i1_x = cf_U_i1.hash_cyclefold(&sponge, pp_hash);
1397
1398 augmented_f_circuit =
1399 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1400 _c2: PhantomData,
1401 _gc2: PhantomData,
1402 poseidon_config: poseidon_config.clone(),
1403 ccs: ccs.clone(),
1404 pp_hash: Some(pp_hash),
1405 mu,
1406 nu,
1407 i: Some(iFr),
1408 i_usize: Some(i),
1409 z_0: Some(z_0.clone()),
1410 z_i: Some(z_i.clone()),
1411 external_inputs: Some(vec![]),
1412 U_i: Some(U_i.clone()),
1413 Us: Some(Us.clone()),
1414 u_i_C: Some(u_i.C),
1415 us: Some(us.clone()),
1416 U_i1_C: Some(U_i1.C),
1417 F: F_circuit,
1418 x: Some(u_i1_x),
1419 nimfs_proof: Some(nimfs_proof),
1420
1421 // cyclefold values
1422 cf_u_i_cmW: Some(cf_u_i.cmW),
1423 cf_U_i: Some(cf_U_i),
1424 cf_x: Some(cf_u_i1_x),
1425 cf_cmT: Some(cf_cmT),
1426 };
1427
1428 // assign the next round instances
1429 cf_W_i = cf_W_i1;
1430 cf_U_i = cf_U_i1;
1431 }
1432
1433 let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap();
1434 assert!(cs.is_satisfied().unwrap());
1435
1436 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<Fr>(&cs); // includes 1 and public inputs
1437 assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap());
1438 let r1cs_z = [vec![Fr::one()], r1cs_x_i1.clone(), r1cs_w_i1.clone()].concat();
1439 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
1440 // assign them directly to w_i, u_i.
1441 (u_i, w_i) = ccs
1442 .to_cccs::<_, _, Pedersen<Projective>>(&mut rng, &pedersen_params, &r1cs_z)
1443 .unwrap();
1444 u_i.check_relation(&ccs, &w_i).unwrap();
1445
1446 // sanity checks
1447 assert_eq!(w_i.w, r1cs_w_i1);
1448 assert_eq!(u_i.x, r1cs_x_i1);
1449 assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap());
1450 assert_eq!(u_i.x[1], augmented_f_circuit.cf_x.unwrap());
1451 let expected_u_i1_x =
1452 U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), z_0.clone(), z_i1.clone());
1453 let expected_cf_U_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1454 // u_i is already u_i1 at this point, check that has the expected value at x[0]
1455 assert_eq!(u_i.x[0], expected_u_i1_x);
1456 assert_eq!(u_i.x[1], expected_cf_U_i1_x);
1457
1458 // set values for next iteration
1459 iFr += Fr::one();
1460 // assign z_{i+1} into z_i
1461 z_i = z_i1.clone();
1462 U_i = U_i1.clone();
1463 W_i = W_i1.clone();
1464
1465 // check the new LCCCS instance relation
1466 U_i.check_relation(&ccs, &W_i).unwrap();
1467 // check the new CCCS instance relation
1468 u_i.check_relation(&ccs, &w_i).unwrap();
1469
1470 // check the CycleFold instance relation
1471 cf_r1cs
1472 .check_relaxed_instance_relation(&cf_W_i, &cf_U_i)
1473 .unwrap();
1474
1475 println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
1476 }
1477 }
1478}