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