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, true>, true>(&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>, false>(&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, false>, false>(
1049 &mut rng,
1050 &pedersen_params,
1051 z_i,
1052 )
1053 .unwrap();
1054 lcccs_instances.push(running_instance);
1055 w_lcccs.push(w);
1056 }
1057 // Create the CCCS instance out of z_cccs
1058 let mut cccs_instances = Vec::new();
1059 let mut w_cccs = Vec::new();
1060 for z_i in z_cccs.iter() {
1061 let (new_instance, w) = ccs
1062 .to_cccs::<_, _, Pedersen<Projective>, false>(&mut rng, &pedersen_params, z_i)
1063 .unwrap();
1064 cccs_instances.push(new_instance);
1065 w_cccs.push(w);
1066 }
1067
1068 // Prover's transcript
1069 let poseidon_config = poseidon_canonical_config::<Fr>();
1070 let mut transcript_p: PoseidonSponge<Fr> = PoseidonSponge::<Fr>::new(&poseidon_config);
1071
1072 // Run the prover side of the multifolding
1073 let (proof, folded_lcccs, folded_witness, _) =
1074 NIMFS::<Projective, PoseidonSponge<Fr>>::prove(
1075 &mut transcript_p,
1076 &ccs,
1077 &lcccs_instances,
1078 &cccs_instances,
1079 &w_lcccs,
1080 &w_cccs,
1081 )
1082 .unwrap();
1083
1084 // Verifier's transcript
1085 let mut transcript_v: PoseidonSponge<Fr> = PoseidonSponge::<Fr>::new(&poseidon_config);
1086
1087 // Run the verifier side of the multifolding
1088 let folded_lcccs_v = NIMFS::<Projective, PoseidonSponge<Fr>>::verify(
1089 &mut transcript_v,
1090 &ccs,
1091 &lcccs_instances,
1092 &cccs_instances,
1093 proof.clone(),
1094 )
1095 .unwrap();
1096 assert_eq!(folded_lcccs, folded_lcccs_v);
1097
1098 // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
1099 folded_lcccs.check_relation(&ccs, &folded_witness).unwrap();
1100
1101 // allocate circuit inputs
1102 let cs = ConstraintSystem::<Fr>::new_ref();
1103 let lcccs_instancesVar =
1104 Vec::<LCCCSVar<Projective>>::new_witness(cs.clone(), || Ok(lcccs_instances.clone()))
1105 .unwrap();
1106 let cccs_instancesVar =
1107 Vec::<CCCSVar<Projective>>::new_witness(cs.clone(), || Ok(cccs_instances.clone()))
1108 .unwrap();
1109 let proofVar =
1110 ProofVar::<Projective>::new_witness(cs.clone(), || Ok(proof.clone())).unwrap();
1111 let mut transcriptVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1112
1113 let enabled = Boolean::<Fr>::new_witness(cs.clone(), || Ok(true)).unwrap();
1114 let (folded_lcccsVar, _) = NIMFSGadget::<Projective>::verify(
1115 cs.clone(),
1116 &ccs,
1117 &mut transcriptVar,
1118 &lcccs_instancesVar,
1119 &cccs_instancesVar,
1120 proofVar,
1121 enabled,
1122 )
1123 .unwrap();
1124 assert!(cs.is_satisfied().unwrap());
1125 assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u);
1126 }
1127
1128 /// test that checks the native LCCCS.hash vs the R1CS constraints version
1129 #[test]
1130 pub fn test_lcccs_hash() {
1131 let mut rng = test_rng();
1132 let poseidon_config = poseidon_canonical_config::<Fr>();
1133 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1134
1135 let ccs = get_test_ccs();
1136 let z1 = get_test_z::<Fr>(3);
1137
1138 let (pedersen_params, _) =
1139 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1140 let pp_hash = Fr::from(42u32); // only for test
1141
1142 let i = Fr::from(3_u32);
1143 let z_0 = vec![Fr::from(3_u32)];
1144 let z_i = vec![Fr::from(3_u32)];
1145 let (lcccs, _) = ccs
1146 .to_lcccs::<_, _, Pedersen<Projective, true>, true>(&mut rng, &pedersen_params, &z1)
1147 .unwrap();
1148 let h = lcccs
1149 .clone()
1150 .hash(&sponge, pp_hash, i, z_0.clone(), z_i.clone());
1151
1152 let cs = ConstraintSystem::<Fr>::new_ref();
1153
1154 let spongeVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1155 let pp_hashVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(pp_hash)).unwrap();
1156 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
1157 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
1158 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
1159 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
1160 let (hVar, _) = lcccsVar
1161 .clone()
1162 .hash(
1163 &spongeVar,
1164 pp_hashVar,
1165 iVar.clone(),
1166 z_0Var.clone(),
1167 z_iVar.clone(),
1168 )
1169 .unwrap();
1170 assert!(cs.is_satisfied().unwrap());
1171
1172 // check that the natively computed and in-circuit computed hashes match
1173 assert_eq!(hVar.value().unwrap(), h);
1174 }
1175
1176 #[test]
1177 pub fn test_augmented_f_circuit() {
1178 let mut rng = test_rng();
1179 let poseidon_config = poseidon_canonical_config::<Fr>();
1180 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1181
1182 let mu = 3;
1183 let nu = 3;
1184
1185 let start = Instant::now();
1186 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
1187 let mut augmented_f_circuit = AugmentedFCircuit::<
1188 Projective,
1189 Projective2,
1190 GVar2,
1191 CubicFCircuit<Fr>,
1192 >::empty(&poseidon_config, F_circuit, None, mu, nu)
1193 .unwrap();
1194 let ccs = augmented_f_circuit.ccs.clone();
1195 println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed());
1196 println!("CCS m x n: {} x {}", ccs.m, ccs.n);
1197
1198 // CycleFold circuit
1199 let cs2 = ConstraintSystem::<Fq>::new_ref();
1200 let cf_circuit = CycleFoldCircuit::<Projective, GVar>::empty(mu + nu);
1201 cf_circuit.generate_constraints(cs2.clone()).unwrap();
1202 cs2.finalize();
1203 let cs2 = cs2
1204 .into_inner()
1205 .ok_or(Error::NoInnerConstraintSystem)
1206 .unwrap();
1207 let cf_r1cs = extract_r1cs::<Fq>(&cs2);
1208 println!("CF m x n: {} x {}", cf_r1cs.A.n_rows, cf_r1cs.A.n_cols);
1209
1210 let (pedersen_params, _) =
1211 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1212 let (cf_pedersen_params, _) =
1213 Pedersen::<Projective2>::setup(&mut rng, cf_r1cs.A.n_cols - cf_r1cs.l - 1).unwrap();
1214
1215 // public params hash
1216 let pp_hash = Fr::from(42u32); // only for test
1217
1218 // first step
1219 let z_0 = vec![Fr::from(3_u32)];
1220 let mut z_i = z_0.clone();
1221
1222 // prepare the dummy instances
1223 let W_dummy = Witness::<Fr>::dummy(&ccs);
1224 let U_dummy = LCCCS::<Projective>::dummy(ccs.l, ccs.t, ccs.s);
1225 let w_dummy = W_dummy.clone();
1226 let u_dummy = CCCS::<Projective>::dummy(ccs.l);
1227 let (cf_W_dummy, cf_U_dummy): (NovaWitness<Projective2>, CommittedInstance<Projective2>) =
1228 cf_r1cs.dummy_instance();
1229
1230 // set the initial dummy instances
1231 let mut W_i = W_dummy.clone();
1232 let mut U_i = U_dummy.clone();
1233 let mut w_i = w_dummy.clone();
1234 let mut u_i = u_dummy.clone();
1235 let mut cf_W_i = cf_W_dummy.clone();
1236 let mut cf_U_i = cf_U_dummy.clone();
1237 u_i.x = vec![
1238 U_i.hash(&sponge, pp_hash, Fr::zero(), z_0.clone(), z_i.clone()),
1239 cf_U_i.hash_cyclefold(&sponge, pp_hash),
1240 ];
1241
1242 let n_steps: usize = 4;
1243 let mut iFr = Fr::zero();
1244 for i in 0..n_steps {
1245 let start = Instant::now();
1246
1247 // for this test, let Us & us be just an array of copies of the U_i & u_i respectively
1248 let Us = vec![U_i.clone(); mu - 1];
1249 let Ws = vec![W_i.clone(); mu - 1];
1250 let us = vec![u_i.clone(); nu - 1];
1251 let ws = vec![w_i.clone(); nu - 1];
1252 let all_Us = [vec![U_i.clone()], Us.clone()].concat();
1253 let all_us = [vec![u_i.clone()], us.clone()].concat();
1254 let all_Ws = [vec![W_i.clone()], Ws].concat();
1255 let all_ws = [vec![w_i.clone()], ws].concat();
1256
1257 let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap();
1258
1259 let (U_i1, W_i1);
1260
1261 if i == 0 {
1262 W_i1 = Witness::<Fr>::dummy(&ccs);
1263 U_i1 = LCCCS::dummy(ccs.l, ccs.t, ccs.s);
1264
1265 let u_i1_x = U_i1.hash(&sponge, pp_hash, Fr::one(), z_0.clone(), z_i1.clone());
1266
1267 // hash the initial (dummy) CycleFold instance, which is used as the 2nd public
1268 // input in the AugmentedFCircuit
1269 let cf_u_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1270
1271 augmented_f_circuit =
1272 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1273 _c2: PhantomData,
1274 _gc2: PhantomData,
1275 poseidon_config: poseidon_config.clone(),
1276 ccs: ccs.clone(),
1277 pp_hash: Some(pp_hash),
1278 mu,
1279 nu,
1280 i: Some(Fr::zero()),
1281 i_usize: Some(0),
1282 z_0: Some(z_0.clone()),
1283 z_i: Some(z_i.clone()),
1284 external_inputs: Some(vec![]),
1285 U_i: Some(U_i.clone()),
1286 Us: Some(Us.clone()),
1287 u_i_C: Some(u_i.C),
1288 us: Some(us.clone()),
1289 U_i1_C: Some(U_i1.C),
1290 F: F_circuit,
1291 x: Some(u_i1_x),
1292 nimfs_proof: None,
1293
1294 // cyclefold values
1295 cf_u_i_cmW: None,
1296 cf_U_i: None,
1297 cf_x: Some(cf_u_i1_x),
1298 cf_cmT: None,
1299 };
1300 } else {
1301 let mut transcript_p: PoseidonSponge<Fr> =
1302 PoseidonSponge::<Fr>::new(&poseidon_config.clone());
1303 transcript_p.absorb(&pp_hash);
1304 let (rho_powers, nimfs_proof);
1305 (nimfs_proof, U_i1, W_i1, rho_powers) =
1306 NIMFS::<Projective, PoseidonSponge<Fr>>::prove(
1307 &mut transcript_p,
1308 &ccs,
1309 &all_Us,
1310 &all_us,
1311 &all_Ws,
1312 &all_ws,
1313 )
1314 .unwrap();
1315
1316 // sanity check: check the folded instance relation
1317 U_i1.check_relation(&ccs, &W_i1).unwrap();
1318
1319 let u_i1_x =
1320 U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), z_0.clone(), z_i1.clone());
1321
1322 let rho_powers_Fq: Vec<Fq> = rho_powers
1323 .iter()
1324 .map(|rho_i| {
1325 Fq::from_bigint(BigInteger::from_bits_le(&rho_i.into_bigint().to_bits_le()))
1326 .unwrap()
1327 })
1328 .collect();
1329 let rho_powers_bits: Vec<Vec<bool>> = rho_powers
1330 .iter()
1331 .map(|rho_i| rho_i.into_bigint().to_bits_le()[..N_BITS_RO].to_vec())
1332 .collect();
1333
1334 // CycleFold part:
1335 // get the vector used as public inputs 'x' in the CycleFold circuit
1336 let cf_u_i_x = [
1337 // all values for multiple instances
1338 rho_powers_Fq,
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_i.C),
1344 us.iter()
1345 .flat_map(|us_i| get_cm_coordinates(&us_i.C))
1346 .collect(),
1347 get_cm_coordinates(&U_i1.C),
1348 ]
1349 .concat();
1350
1351 let cf_circuit = CycleFoldCircuit::<Projective, GVar> {
1352 _gc: PhantomData,
1353 n_points: mu + nu,
1354 r_bits: Some(rho_powers_bits.clone()),
1355 points: Some(
1356 [
1357 vec![U_i.clone().C],
1358 Us.iter().map(|Us_i| Us_i.C).collect(),
1359 vec![u_i.clone().C],
1360 us.iter().map(|us_i| us_i.C).collect(),
1361 ]
1362 .concat(),
1363 ),
1364 x: Some(cf_u_i_x.clone()),
1365 };
1366
1367 // ensure that the CycleFoldCircuit is well defined
1368 assert_eq!(
1369 cf_circuit.r_bits.clone().unwrap().len(),
1370 cf_circuit.n_points - 1
1371 );
1372 assert_eq!(
1373 cf_circuit.points.clone().unwrap().len(),
1374 cf_circuit.n_points
1375 );
1376
1377 let (_cf_w_i, cf_u_i, cf_W_i1, cf_U_i1, cf_cmT, _) = fold_cyclefold_circuit::<
1378 Projective,
1379 GVar,
1380 Projective2,
1381 GVar2,
1382 CubicFCircuit<Fr>,
1383 Pedersen<Projective>,
1384 Pedersen<Projective2>,
1385 false,
1386 >(
1387 mu + nu,
1388 &mut transcript_p,
1389 cf_r1cs.clone(),
1390 cf_pedersen_params.clone(),
1391 pp_hash,
1392 cf_W_i.clone(), // CycleFold running instance witness
1393 cf_U_i.clone(), // CycleFold running instance
1394 cf_u_i_x, // CycleFold incoming instance
1395 cf_circuit,
1396 &mut rng,
1397 )
1398 .unwrap();
1399
1400 // hash the CycleFold folded instance, which is used as the 2nd public input in the
1401 // AugmentedFCircuit
1402 let cf_u_i1_x = cf_U_i1.hash_cyclefold(&sponge, pp_hash);
1403
1404 augmented_f_circuit =
1405 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1406 _c2: PhantomData,
1407 _gc2: PhantomData,
1408 poseidon_config: poseidon_config.clone(),
1409 ccs: ccs.clone(),
1410 pp_hash: Some(pp_hash),
1411 mu,
1412 nu,
1413 i: Some(iFr),
1414 i_usize: Some(i),
1415 z_0: Some(z_0.clone()),
1416 z_i: Some(z_i.clone()),
1417 external_inputs: Some(vec![]),
1418 U_i: Some(U_i.clone()),
1419 Us: Some(Us.clone()),
1420 u_i_C: Some(u_i.C),
1421 us: Some(us.clone()),
1422 U_i1_C: Some(U_i1.C),
1423 F: F_circuit,
1424 x: Some(u_i1_x),
1425 nimfs_proof: Some(nimfs_proof),
1426
1427 // cyclefold values
1428 cf_u_i_cmW: Some(cf_u_i.cmW),
1429 cf_U_i: Some(cf_U_i),
1430 cf_x: Some(cf_u_i1_x),
1431 cf_cmT: Some(cf_cmT),
1432 };
1433
1434 // assign the next round instances
1435 cf_W_i = cf_W_i1;
1436 cf_U_i = cf_U_i1;
1437 }
1438
1439 let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap();
1440 assert!(cs.is_satisfied().unwrap());
1441
1442 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<Fr>(&cs); // includes 1 and public inputs
1443 assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap());
1444 let r1cs_z = [vec![Fr::one()], r1cs_x_i1.clone(), r1cs_w_i1.clone()].concat();
1445 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
1446 // assign them directly to w_i, u_i.
1447 (u_i, w_i) = ccs
1448 .to_cccs::<_, _, Pedersen<Projective>, false>(&mut rng, &pedersen_params, &r1cs_z)
1449 .unwrap();
1450 u_i.check_relation(&ccs, &w_i).unwrap();
1451
1452 // sanity checks
1453 assert_eq!(w_i.w, r1cs_w_i1);
1454 assert_eq!(u_i.x, r1cs_x_i1);
1455 assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap());
1456 assert_eq!(u_i.x[1], augmented_f_circuit.cf_x.unwrap());
1457 let expected_u_i1_x =
1458 U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), z_0.clone(), z_i1.clone());
1459 let expected_cf_U_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1460 // u_i is already u_i1 at this point, check that has the expected value at x[0]
1461 assert_eq!(u_i.x[0], expected_u_i1_x);
1462 assert_eq!(u_i.x[1], expected_cf_U_i1_x);
1463
1464 // set values for next iteration
1465 iFr += Fr::one();
1466 // assign z_{i+1} into z_i
1467 z_i = z_i1.clone();
1468 U_i = U_i1.clone();
1469 W_i = W_i1.clone();
1470
1471 // check the new LCCCS instance relation
1472 U_i.check_relation(&ccs, &W_i).unwrap();
1473 // check the new CCCS instance relation
1474 u_i.check_relation(&ccs, &w_i).unwrap();
1475
1476 // check the CycleFold instance relation
1477 cf_r1cs
1478 .check_relaxed_instance_relation(&cf_W_i, &cf_U_i)
1479 .unwrap();
1480
1481 println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
1482 }
1483 }
1484}