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