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