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, Dummy},
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);
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);
610 let mut w_i = W_i.clone();
611 let mut u_i = CCCS::<C1>::dummy(&ccs);
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);
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);
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);
738 let u_dummy = CCCS::<C1>::dummy(&self.ccs);
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,
910 Arith,
911 },
912 commitment::{pedersen::Pedersen, CommitmentScheme},
913 folding::{
914 circuits::cyclefold::{fold_cyclefold_circuit, CycleFoldWitness},
915 hypernova::{
916 utils::{compute_c, compute_sigmas_thetas},
917 HyperNovaCycleFoldCircuit,
918 },
919 traits::CommittedInstanceOps,
920 },
921 frontend::utils::CubicFCircuit,
922 transcript::poseidon::poseidon_canonical_config,
923 utils::get_cm_coordinates,
924 };
925
926 #[test]
927 pub fn test_compute_c_gadget() {
928 // number of LCCCS & CCCS instances to fold in a single step
929 let mu = 32;
930 let nu = 42;
931
932 let mut z_lcccs = Vec::new();
933 for i in 0..mu {
934 let z = get_test_z(i + 3);
935 z_lcccs.push(z);
936 }
937 let mut z_cccs = Vec::new();
938 for i in 0..nu {
939 let z = get_test_z(i + 3);
940 z_cccs.push(z);
941 }
942
943 let ccs: CCS<Fr> = get_test_ccs();
944
945 let mut rng = test_rng();
946 let gamma: Fr = Fr::rand(&mut rng);
947 let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
948 let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
949
950 let (pedersen_params, _) =
951 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
952
953 // Create the LCCCS instances out of z_lcccs
954 let mut lcccs_instances = Vec::new();
955 for z_i in z_lcccs.iter() {
956 let (inst, _) = ccs
957 .to_lcccs::<_, _, Pedersen<Projective, true>, true>(&mut rng, &pedersen_params, z_i)
958 .unwrap();
959 lcccs_instances.push(inst);
960 }
961 // Create the CCCS instance out of z_cccs
962 let mut cccs_instances = Vec::new();
963 for z_i in z_cccs.iter() {
964 let (inst, _) = ccs
965 .to_cccs::<_, _, Pedersen<Projective>, false>(&mut rng, &pedersen_params, z_i)
966 .unwrap();
967 cccs_instances.push(inst);
968 }
969
970 let sigmas_thetas = compute_sigmas_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime).unwrap();
971
972 let expected_c = compute_c(
973 &ccs,
974 &sigmas_thetas,
975 gamma,
976 &beta,
977 &lcccs_instances
978 .iter()
979 .map(|lcccs| lcccs.r_x.clone())
980 .collect(),
981 &r_x_prime,
982 )
983 .unwrap();
984
985 let cs = ConstraintSystem::<Fr>::new_ref();
986 let mut vec_sigmas = Vec::new();
987 let mut vec_thetas = Vec::new();
988 for sigmas in sigmas_thetas.0 {
989 vec_sigmas
990 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap());
991 }
992 for thetas in sigmas_thetas.1 {
993 vec_thetas
994 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap());
995 }
996 let vec_r_x: Vec<Vec<FpVar<Fr>>> = lcccs_instances
997 .iter()
998 .map(|lcccs| {
999 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap()
1000 })
1001 .collect();
1002 let vec_r_x_prime =
1003 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap();
1004 let gamma_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(gamma)).unwrap();
1005 let beta_var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap();
1006
1007 let computed_c = compute_c_gadget(
1008 cs.clone(),
1009 &ccs,
1010 vec_sigmas,
1011 vec_thetas,
1012 gamma_var,
1013 beta_var,
1014 vec_r_x,
1015 vec_r_x_prime,
1016 )
1017 .unwrap();
1018
1019 assert_eq!(expected_c, computed_c.value().unwrap());
1020 }
1021
1022 /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step,
1023 /// to verify the folding in the NIMFSGadget circuit
1024 #[test]
1025 pub fn test_nimfs_gadget_verify() {
1026 let mut rng = test_rng();
1027
1028 // Create a basic CCS circuit
1029 let ccs = get_test_ccs::<Fr>();
1030 let (pedersen_params, _) =
1031 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1032
1033 let mu = 32;
1034 let nu = 42;
1035
1036 // Generate a mu LCCCS & nu CCCS satisfying witness
1037 let mut z_lcccs = Vec::new();
1038 for i in 0..mu {
1039 let z = get_test_z(i + 3);
1040 z_lcccs.push(z);
1041 }
1042 let mut z_cccs = Vec::new();
1043 for i in 0..nu {
1044 let z = get_test_z(nu + i + 3);
1045 z_cccs.push(z);
1046 }
1047
1048 // Create the LCCCS instances out of z_lcccs
1049 let mut lcccs_instances = Vec::new();
1050 let mut w_lcccs = Vec::new();
1051 for z_i in z_lcccs.iter() {
1052 let (running_instance, w) = ccs
1053 .to_lcccs::<_, _, Pedersen<Projective, false>, false>(
1054 &mut rng,
1055 &pedersen_params,
1056 z_i,
1057 )
1058 .unwrap();
1059 lcccs_instances.push(running_instance);
1060 w_lcccs.push(w);
1061 }
1062 // Create the CCCS instance out of z_cccs
1063 let mut cccs_instances = Vec::new();
1064 let mut w_cccs = Vec::new();
1065 for z_i in z_cccs.iter() {
1066 let (new_instance, w) = ccs
1067 .to_cccs::<_, _, Pedersen<Projective>, false>(&mut rng, &pedersen_params, z_i)
1068 .unwrap();
1069 cccs_instances.push(new_instance);
1070 w_cccs.push(w);
1071 }
1072
1073 // Prover's transcript
1074 let poseidon_config = poseidon_canonical_config::<Fr>();
1075 let mut transcript_p: PoseidonSponge<Fr> = PoseidonSponge::<Fr>::new(&poseidon_config);
1076
1077 // Run the prover side of the multifolding
1078 let (proof, folded_lcccs, folded_witness, _) =
1079 NIMFS::<Projective, PoseidonSponge<Fr>>::prove(
1080 &mut transcript_p,
1081 &ccs,
1082 &lcccs_instances,
1083 &cccs_instances,
1084 &w_lcccs,
1085 &w_cccs,
1086 )
1087 .unwrap();
1088
1089 // Verifier's transcript
1090 let mut transcript_v: PoseidonSponge<Fr> = PoseidonSponge::<Fr>::new(&poseidon_config);
1091
1092 // Run the verifier side of the multifolding
1093 let folded_lcccs_v = NIMFS::<Projective, PoseidonSponge<Fr>>::verify(
1094 &mut transcript_v,
1095 &ccs,
1096 &lcccs_instances,
1097 &cccs_instances,
1098 proof.clone(),
1099 )
1100 .unwrap();
1101 assert_eq!(folded_lcccs, folded_lcccs_v);
1102
1103 // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
1104 ccs.check_relation(&folded_witness, &folded_lcccs).unwrap();
1105
1106 // allocate circuit inputs
1107 let cs = ConstraintSystem::<Fr>::new_ref();
1108 let lcccs_instancesVar =
1109 Vec::<LCCCSVar<Projective>>::new_witness(cs.clone(), || Ok(lcccs_instances.clone()))
1110 .unwrap();
1111 let cccs_instancesVar =
1112 Vec::<CCCSVar<Projective>>::new_witness(cs.clone(), || Ok(cccs_instances.clone()))
1113 .unwrap();
1114 let proofVar =
1115 ProofVar::<Projective>::new_witness(cs.clone(), || Ok(proof.clone())).unwrap();
1116 let mut transcriptVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1117
1118 let enabled = Boolean::<Fr>::new_witness(cs.clone(), || Ok(true)).unwrap();
1119 let (folded_lcccsVar, _) = NIMFSGadget::<Projective>::verify(
1120 cs.clone(),
1121 &ccs,
1122 &mut transcriptVar,
1123 &lcccs_instancesVar,
1124 &cccs_instancesVar,
1125 proofVar,
1126 enabled,
1127 )
1128 .unwrap();
1129 assert!(cs.is_satisfied().unwrap());
1130 assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u);
1131 }
1132
1133 /// test that checks the native LCCCS.to_sponge_{bytes,field_elements} vs
1134 /// the R1CS constraints version
1135 #[test]
1136 pub fn test_lcccs_to_sponge_preimage() {
1137 let mut rng = test_rng();
1138
1139 let ccs = get_test_ccs();
1140 let z1 = get_test_z::<Fr>(3);
1141
1142 let (pedersen_params, _) =
1143 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1144
1145 let (lcccs, _) = ccs
1146 .to_lcccs::<_, _, Pedersen<Projective, true>, true>(&mut rng, &pedersen_params, &z1)
1147 .unwrap();
1148 let bytes = lcccs.to_sponge_bytes_as_vec();
1149 let field_elements = lcccs.to_sponge_field_elements_as_vec();
1150
1151 let cs = ConstraintSystem::<Fr>::new_ref();
1152
1153 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
1154 let bytes_var = lcccsVar.to_sponge_bytes().unwrap();
1155 let field_elements_var = lcccsVar.to_sponge_field_elements().unwrap();
1156
1157 assert!(cs.is_satisfied().unwrap());
1158
1159 // check that the natively computed and in-circuit computed hashes match
1160 assert_eq!(bytes_var.value().unwrap(), bytes);
1161 assert_eq!(field_elements_var.value().unwrap(), field_elements);
1162 }
1163
1164 /// test that checks the native LCCCS.hash vs the R1CS constraints version
1165 #[test]
1166 pub fn test_lcccs_hash() {
1167 let mut rng = test_rng();
1168 let poseidon_config = poseidon_canonical_config::<Fr>();
1169 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1170
1171 let ccs = get_test_ccs();
1172 let z1 = get_test_z::<Fr>(3);
1173
1174 let (pedersen_params, _) =
1175 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1176 let pp_hash = Fr::from(42u32); // only for test
1177
1178 let i = Fr::from(3_u32);
1179 let z_0 = vec![Fr::from(3_u32)];
1180 let z_i = vec![Fr::from(3_u32)];
1181 let (lcccs, _) = ccs
1182 .to_lcccs::<_, _, Pedersen<Projective, true>, true>(&mut rng, &pedersen_params, &z1)
1183 .unwrap();
1184 let h = lcccs.clone().hash(&sponge, pp_hash, i, &z_0, &z_i);
1185
1186 let cs = ConstraintSystem::<Fr>::new_ref();
1187
1188 let spongeVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1189 let pp_hashVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(pp_hash)).unwrap();
1190 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
1191 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
1192 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
1193 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
1194 let (hVar, _) = lcccsVar
1195 .clone()
1196 .hash(&spongeVar, &pp_hashVar, &iVar, &z_0Var, &z_iVar)
1197 .unwrap();
1198 assert!(cs.is_satisfied().unwrap());
1199
1200 // check that the natively computed and in-circuit computed hashes match
1201 assert_eq!(hVar.value().unwrap(), h);
1202 }
1203
1204 #[test]
1205 pub fn test_augmented_f_circuit() {
1206 let mut rng = test_rng();
1207 let poseidon_config = poseidon_canonical_config::<Fr>();
1208 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1209
1210 const MU: usize = 3;
1211 const NU: usize = 3;
1212
1213 let start = Instant::now();
1214 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
1215 let mut augmented_f_circuit =
1216 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>, MU, NU>::empty(
1217 &poseidon_config,
1218 F_circuit,
1219 None,
1220 )
1221 .unwrap();
1222 let ccs = augmented_f_circuit.ccs.clone();
1223 println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed());
1224 println!("CCS m x n: {} x {}", ccs.m, ccs.n);
1225
1226 // CycleFold circuit
1227 let cs2 = ConstraintSystem::<Fq>::new_ref();
1228 let cf_circuit = HyperNovaCycleFoldCircuit::<Projective, GVar, MU, NU>::empty();
1229 cf_circuit.generate_constraints(cs2.clone()).unwrap();
1230 cs2.finalize();
1231 let cs2 = cs2
1232 .into_inner()
1233 .ok_or(Error::NoInnerConstraintSystem)
1234 .unwrap();
1235 let cf_r1cs = extract_r1cs::<Fq>(&cs2);
1236 println!("CF m x n: {} x {}", cf_r1cs.A.n_rows, cf_r1cs.A.n_cols);
1237
1238 let (pedersen_params, _) =
1239 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1240 let (cf_pedersen_params, _) =
1241 Pedersen::<Projective2>::setup(&mut rng, cf_r1cs.A.n_cols - cf_r1cs.l - 1).unwrap();
1242
1243 // public params hash
1244 let pp_hash = Fr::from(42u32); // only for test
1245
1246 // first step
1247 let z_0 = vec![Fr::from(3_u32)];
1248 let mut z_i = z_0.clone();
1249
1250 // prepare the dummy instances
1251 let W_dummy = Witness::<Fr>::dummy(&ccs);
1252 let U_dummy = LCCCS::<Projective>::dummy(&ccs);
1253 let w_dummy = W_dummy.clone();
1254 let u_dummy = CCCS::<Projective>::dummy(&ccs);
1255 let (cf_W_dummy, cf_U_dummy): (
1256 CycleFoldWitness<Projective2>,
1257 CycleFoldCommittedInstance<Projective2>,
1258 ) = cf_r1cs.dummy_witness_instance();
1259
1260 // set the initial dummy instances
1261 let mut W_i = W_dummy.clone();
1262 let mut U_i = U_dummy.clone();
1263 let mut w_i = w_dummy.clone();
1264 let mut u_i = u_dummy.clone();
1265 let mut cf_W_i = cf_W_dummy.clone();
1266 let mut cf_U_i = cf_U_dummy.clone();
1267 u_i.x = vec![
1268 U_i.hash(&sponge, pp_hash, Fr::zero(), &z_0, &z_i),
1269 cf_U_i.hash_cyclefold(&sponge, pp_hash),
1270 ];
1271
1272 let n_steps: usize = 4;
1273 let mut iFr = Fr::zero();
1274 for i in 0..n_steps {
1275 let start = Instant::now();
1276
1277 // for this test, let Us & us be just an array of copies of the U_i & u_i respectively
1278 let Us = vec![U_i.clone(); MU - 1];
1279 let Ws = vec![W_i.clone(); MU - 1];
1280 let us = vec![u_i.clone(); NU - 1];
1281 let ws = vec![w_i.clone(); NU - 1];
1282 let all_Us = [vec![U_i.clone()], Us.clone()].concat();
1283 let all_us = [vec![u_i.clone()], us.clone()].concat();
1284 let all_Ws = [vec![W_i.clone()], Ws].concat();
1285 let all_ws = [vec![w_i.clone()], ws].concat();
1286
1287 let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap();
1288
1289 let (U_i1, W_i1);
1290
1291 if i == 0 {
1292 W_i1 = Witness::<Fr>::dummy(&ccs);
1293 U_i1 = LCCCS::dummy(&ccs);
1294
1295 let u_i1_x = U_i1.hash(&sponge, pp_hash, Fr::one(), &z_0, &z_i1);
1296
1297 // hash the initial (dummy) CycleFold instance, which is used as the 2nd public
1298 // input in the AugmentedFCircuit
1299 let cf_u_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1300
1301 augmented_f_circuit = AugmentedFCircuit::<
1302 Projective,
1303 Projective2,
1304 GVar2,
1305 CubicFCircuit<Fr>,
1306 MU,
1307 NU,
1308 > {
1309 _c2: PhantomData,
1310 _gc2: PhantomData,
1311 poseidon_config: poseidon_config.clone(),
1312 ccs: ccs.clone(),
1313 pp_hash: Some(pp_hash),
1314 i: Some(Fr::zero()),
1315 i_usize: Some(0),
1316 z_0: Some(z_0.clone()),
1317 z_i: Some(z_i.clone()),
1318 external_inputs: Some(vec![]),
1319 U_i: Some(U_i.clone()),
1320 Us: Some(Us.clone()),
1321 u_i_C: Some(u_i.C),
1322 us: Some(us.clone()),
1323 U_i1_C: Some(U_i1.C),
1324 F: F_circuit,
1325 x: Some(u_i1_x),
1326 nimfs_proof: None,
1327
1328 // cyclefold values
1329 cf_u_i_cmW: None,
1330 cf_U_i: None,
1331 cf_x: Some(cf_u_i1_x),
1332 cf_cmT: None,
1333 };
1334 } else {
1335 let mut transcript_p: PoseidonSponge<Fr> =
1336 PoseidonSponge::<Fr>::new(&poseidon_config.clone());
1337 transcript_p.absorb(&pp_hash);
1338 let (rho, nimfs_proof);
1339 (nimfs_proof, U_i1, W_i1, rho) = NIMFS::<Projective, PoseidonSponge<Fr>>::prove(
1340 &mut transcript_p,
1341 &ccs,
1342 &all_Us,
1343 &all_us,
1344 &all_Ws,
1345 &all_ws,
1346 )
1347 .unwrap();
1348
1349 // sanity check: check the folded instance relation
1350 ccs.check_relation(&W_i1, &U_i1).unwrap();
1351
1352 let u_i1_x = U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), &z_0, &z_i1);
1353
1354 let rho_bits = rho.into_bigint().to_bits_le()[..NOVA_N_BITS_RO].to_vec();
1355 let rho_Fq = Fq::from_bigint(BigInteger::from_bits_le(&rho_bits)).unwrap();
1356
1357 // CycleFold part:
1358 // get the vector used as public inputs 'x' in the CycleFold circuit
1359 let cf_u_i_x = [
1360 vec![rho_Fq],
1361 get_cm_coordinates(&U_i.C),
1362 Us.iter()
1363 .flat_map(|Us_i| get_cm_coordinates(&Us_i.C))
1364 .collect(),
1365 get_cm_coordinates(&u_i.C),
1366 us.iter()
1367 .flat_map(|us_i| get_cm_coordinates(&us_i.C))
1368 .collect(),
1369 get_cm_coordinates(&U_i1.C),
1370 ]
1371 .concat();
1372
1373 let cf_circuit = HyperNovaCycleFoldCircuit::<Projective, GVar, MU, NU> {
1374 _gc: PhantomData,
1375 r_bits: Some(rho_bits.clone()),
1376 points: Some(
1377 [
1378 vec![U_i.clone().C],
1379 Us.iter().map(|Us_i| Us_i.C).collect(),
1380 vec![u_i.clone().C],
1381 us.iter().map(|us_i| us_i.C).collect(),
1382 ]
1383 .concat(),
1384 ),
1385 x: Some(cf_u_i_x.clone()),
1386 };
1387
1388 // ensure that the CycleFoldCircuit is well defined
1389 assert_eq!(
1390 cf_circuit.points.clone().unwrap().len(),
1391 HyperNovaCycleFoldConfig::<Projective, MU, NU>::N_INPUT_POINTS
1392 );
1393
1394 let (_cf_w_i, cf_u_i, cf_W_i1, cf_U_i1, cf_cmT, _) = fold_cyclefold_circuit::<
1395 HyperNovaCycleFoldConfig<Projective, MU, NU>,
1396 Projective,
1397 GVar,
1398 Projective2,
1399 GVar2,
1400 Pedersen<Projective2>,
1401 false,
1402 >(
1403 &mut transcript_p,
1404 cf_r1cs.clone(),
1405 cf_pedersen_params.clone(),
1406 pp_hash,
1407 cf_W_i.clone(), // CycleFold running instance witness
1408 cf_U_i.clone(), // CycleFold running instance
1409 cf_u_i_x, // CycleFold incoming instance
1410 cf_circuit,
1411 &mut rng,
1412 )
1413 .unwrap();
1414
1415 // hash the CycleFold folded instance, which is used as the 2nd public input in the
1416 // AugmentedFCircuit
1417 let cf_u_i1_x = cf_U_i1.hash_cyclefold(&sponge, pp_hash);
1418
1419 augmented_f_circuit = AugmentedFCircuit::<
1420 Projective,
1421 Projective2,
1422 GVar2,
1423 CubicFCircuit<Fr>,
1424 MU,
1425 NU,
1426 > {
1427 _c2: PhantomData,
1428 _gc2: PhantomData,
1429 poseidon_config: poseidon_config.clone(),
1430 ccs: ccs.clone(),
1431 pp_hash: Some(pp_hash),
1432 i: Some(iFr),
1433 i_usize: Some(i),
1434 z_0: Some(z_0.clone()),
1435 z_i: Some(z_i.clone()),
1436 external_inputs: Some(vec![]),
1437 U_i: Some(U_i.clone()),
1438 Us: Some(Us.clone()),
1439 u_i_C: Some(u_i.C),
1440 us: Some(us.clone()),
1441 U_i1_C: Some(U_i1.C),
1442 F: F_circuit,
1443 x: Some(u_i1_x),
1444 nimfs_proof: Some(nimfs_proof),
1445
1446 // cyclefold values
1447 cf_u_i_cmW: Some(cf_u_i.cmW),
1448 cf_U_i: Some(cf_U_i),
1449 cf_x: Some(cf_u_i1_x),
1450 cf_cmT: Some(cf_cmT),
1451 };
1452
1453 // assign the next round instances
1454 cf_W_i = cf_W_i1;
1455 cf_U_i = cf_U_i1;
1456 }
1457
1458 let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap();
1459 assert!(cs.is_satisfied().unwrap());
1460
1461 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<Fr>(&cs); // includes 1 and public inputs
1462 assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap());
1463 let r1cs_z = [vec![Fr::one()], r1cs_x_i1.clone(), r1cs_w_i1.clone()].concat();
1464 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
1465 // assign them directly to w_i, u_i.
1466 (u_i, w_i) = ccs
1467 .to_cccs::<_, _, Pedersen<Projective>, false>(&mut rng, &pedersen_params, &r1cs_z)
1468 .unwrap();
1469 ccs.check_relation(&w_i, &u_i).unwrap();
1470
1471 // sanity checks
1472 assert_eq!(w_i.w, r1cs_w_i1);
1473 assert_eq!(u_i.x, r1cs_x_i1);
1474 assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap());
1475 assert_eq!(u_i.x[1], augmented_f_circuit.cf_x.unwrap());
1476 let expected_u_i1_x = U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), &z_0, &z_i1);
1477 let expected_cf_U_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1478 // u_i is already u_i1 at this point, check that has the expected value at x[0]
1479 assert_eq!(u_i.x[0], expected_u_i1_x);
1480 assert_eq!(u_i.x[1], expected_cf_U_i1_x);
1481
1482 // set values for next iteration
1483 iFr += Fr::one();
1484 // assign z_{i+1} into z_i
1485 z_i = z_i1.clone();
1486 U_i = U_i1.clone();
1487 W_i = W_i1.clone();
1488
1489 // check the new LCCCS instance relation
1490 ccs.check_relation(&W_i, &U_i).unwrap();
1491 // check the new CCCS instance relation
1492 ccs.check_relation(&w_i, &u_i).unwrap();
1493
1494 // check the CycleFold instance relation
1495 cf_r1cs.check_relation(&cf_W_i, &cf_U_i).unwrap();
1496
1497 println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
1498 }
1499 }
1500}