sonobe/folding-schemes/src/folding/hypernova/circuits.rs
folding-schemes/src/folding/hypernova/circuits.rsRaw
1/// Implementation of [HyperNova](https://eprint.iacr.org/2023/573.pdf) circuits
2use ark_crypto_primitives::sponge::{
3 constraints::CryptographicSpongeVar,
4 poseidon::{constraints::PoseidonSpongeVar, PoseidonSponge},
5 CryptographicSponge,
6};
7use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
8use ark_ec::{CurveGroup, Group};
9use ark_ff::PrimeField;
10use ark_r1cs_std::{
11 alloc::{AllocVar, AllocationMode},
12 boolean::Boolean,
13 eq::EqGadget,
14 fields::{fp::FpVar, FieldVar},
15 groups::GroupOpsBounds,
16 prelude::CurveVar,
17 R1CSVar, ToBitsGadget, ToConstraintFieldGadget,
18};
19use ark_relations::r1cs::{
20 ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, Namespace, SynthesisError,
21};
22use ark_std::{fmt::Debug, ops::Neg, One, Zero};
23use core::{borrow::Borrow, marker::PhantomData};
24
25use super::{
26 cccs::CCCS,
27 lcccs::LCCCS,
28 nimfs::{NIMFSProof, NIMFS},
29 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<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, together with the rho's powers vector so
321 // they can be used in other parts of the AugmentedFCircuit
322 Self::fold(
323 running_instances,
324 new_instances,
325 proof.sigmas_thetas,
326 r_x_prime,
327 rho,
328 )
329 }
330
331 /// Runs (in-circuit) the verifier side of the fold, computing the new folded LCCCS instance
332 #[allow(clippy::type_complexity)]
333 fn fold(
334 lcccs: &[LCCCSVar<C>],
335 cccs: &[CCCSVar<C>],
336 sigmas_thetas: (Vec<Vec<FpVar<CF1<C>>>>, Vec<Vec<FpVar<CF1<C>>>>),
337 r_x_prime: Vec<FpVar<CF1<C>>>,
338 rho: FpVar<CF1<C>>,
339 ) -> Result<(LCCCSVar<C>, Vec<Vec<Boolean<CF1<C>>>>), SynthesisError> {
340 let (sigmas, thetas) = (sigmas_thetas.0.clone(), sigmas_thetas.1.clone());
341 let mut u_folded: FpVar<CF1<C>> = FpVar::zero();
342 let mut x_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); lcccs[0].x.len()];
343 let mut v_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); sigmas[0].len()];
344
345 let mut rho_vec: Vec<Vec<Boolean<CF1<C>>>> =
346 vec![vec![Boolean::FALSE; NOVA_N_BITS_RO]; lcccs.len() + cccs.len() - 1];
347 let mut rho_i = FpVar::one();
348 for i in 0..(lcccs.len() + cccs.len()) {
349 let u: FpVar<CF1<C>>;
350 let x: Vec<FpVar<CF1<C>>>;
351 let v: Vec<FpVar<CF1<C>>>;
352 if i < lcccs.len() {
353 u = lcccs[i].u.clone();
354 x = lcccs[i].x.clone();
355 v = sigmas[i].clone();
356 } else {
357 u = FpVar::one();
358 x = cccs[i - lcccs.len()].x.clone();
359 v = thetas[i - lcccs.len()].clone();
360 }
361
362 u_folded += rho_i.clone() * u;
363 x_folded = x_folded
364 .iter()
365 .zip(
366 x.iter()
367 .map(|x_i| x_i * rho_i.clone())
368 .collect::<Vec<FpVar<CF1<C>>>>(),
369 )
370 .map(|(a_i, b_i)| a_i + b_i)
371 .collect();
372
373 v_folded = v_folded
374 .iter()
375 .zip(
376 v.iter()
377 .map(|x_i| x_i * rho_i.clone())
378 .collect::<Vec<FpVar<CF1<C>>>>(),
379 )
380 .map(|(a_i, b_i)| a_i + b_i)
381 .collect();
382
383 // compute the next power of rho
384 rho_i *= rho.clone();
385 // crop the size of rho_i to NOVA_N_BITS_RO
386 let rho_i_bits = rho_i.to_bits_le()?;
387 rho_i = Boolean::le_bits_to_fp_var(&rho_i_bits[..NOVA_N_BITS_RO])?;
388 if i < lcccs.len() + cccs.len() - 1 {
389 // store the cropped rho_i into the rho_vec
390 rho_vec[i] = rho_i_bits[..NOVA_N_BITS_RO].to_vec();
391 }
392 }
393
394 // return the folded instance, together with the rho's powers vector so they can be used in
395 // other parts of the AugmentedFCircuit
396 Ok((
397 LCCCSVar::<C> {
398 // C this is later overwritten by the U_{i+1}.C value checked by the cyclefold circuit
399 C: lcccs[0].C.clone(),
400 u: u_folded,
401 x: x_folded,
402 r_x: r_x_prime,
403 v: v_folded,
404 },
405 rho_vec,
406 ))
407 }
408}
409
410/// Computes c from the step 5 in section 5 of HyperNova, adapted to multiple LCCCS & CCCS
411/// instances:
412/// $$
413/// c = \sum_{i \in [\mu]} \left(\sum_{j \in [t]} \gamma^{i \cdot t + j} \cdot e_i \cdot \sigma_{i,j} \right)
414/// + \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}
415/// \theta_{k,j} \right)
416/// $$
417#[allow(clippy::too_many_arguments)]
418fn compute_c_gadget<F: PrimeField>(
419 cs: ConstraintSystemRef<F>,
420 ccs: &CCS<F>,
421 vec_sigmas: Vec<Vec<FpVar<F>>>,
422 vec_thetas: Vec<Vec<FpVar<F>>>,
423 gamma: FpVar<F>,
424 beta: Vec<FpVar<F>>,
425 vec_r_x: Vec<Vec<FpVar<F>>>,
426 vec_r_x_prime: Vec<FpVar<F>>,
427) -> Result<FpVar<F>, SynthesisError> {
428 let mut e_lcccs = Vec::new();
429 for r_x in vec_r_x.iter() {
430 e_lcccs.push(EqEvalGadget::eq_eval(r_x, &vec_r_x_prime)?);
431 }
432
433 let mut c = FpVar::<F>::zero();
434 let mut current_gamma = FpVar::<F>::one();
435 for i in 0..vec_sigmas.len() {
436 for j in 0..ccs.t {
437 c += current_gamma.clone() * e_lcccs[i].clone() * vec_sigmas[i][j].clone();
438 current_gamma *= gamma.clone();
439 }
440 }
441
442 let ccs_c = Vec::<FpVar<F>>::new_constant(cs.clone(), ccs.c.clone())?;
443 let e_k = EqEvalGadget::eq_eval(&beta, &vec_r_x_prime)?;
444 #[allow(clippy::needless_range_loop)]
445 for k in 0..vec_thetas.len() {
446 let mut sum = FpVar::<F>::zero();
447 for i in 0..ccs.q {
448 let mut prod = FpVar::<F>::one();
449 for j in ccs.S[i].clone() {
450 prod *= vec_thetas[k][j].clone();
451 }
452 sum += ccs_c[i].clone() * prod;
453 }
454 c += current_gamma.clone() * e_k.clone() * sum;
455 current_gamma *= gamma.clone();
456 }
457 Ok(c)
458}
459
460/// `AugmentedFCircuit` enhances the original step function `F`, so that it can
461/// be used in recursive arguments such as IVC.
462///
463/// The method for converting `F` to `AugmentedFCircuit` (`F'`) is defined in
464/// [Nova](https://eprint.iacr.org/2021/370.pdf), where `AugmentedFCircuit` not
465/// only invokes `F`, but also adds additional constraints for verifying the
466/// correct folding of primary instances (i.e., the instances over `C1`).
467/// In the paper, the primary instances are Nova's `CommittedInstance`, but we
468/// extend this method to support using HyperNova's `LCCCS` and `CCCS` instances
469/// as primary instances.
470///
471/// Furthermore, to reduce circuit size over `C2`, we implement the constraints
472/// defined in [CycleFold](https://eprint.iacr.org/2023/1192.pdf). These extra
473/// constraints verify the correct folding of CycleFold instances.
474///
475/// For multi-instance folding, one needs to specify the const generics below:
476/// * `MU` - the number of LCCCS instances to be folded
477/// * `NU` - the number of CCCS instances to be folded
478#[derive(Debug, Clone)]
479pub struct AugmentedFCircuit<
480 C1: CurveGroup,
481 C2: CurveGroup,
482 GC2: CurveVar<C2, CF2<C2>>,
483 FC: FCircuit<CF1<C1>>,
484 const MU: usize,
485 const NU: usize,
486> where
487 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
488{
489 pub _c2: PhantomData<C2>,
490 pub _gc2: PhantomData<GC2>,
491 pub poseidon_config: PoseidonConfig<CF1<C1>>,
492 pub ccs: CCS<C1::ScalarField>, // CCS of the AugmentedFCircuit
493 pub pp_hash: Option<CF1<C1>>,
494 pub i: Option<CF1<C1>>,
495 pub i_usize: Option<usize>,
496 pub z_0: Option<Vec<C1::ScalarField>>,
497 pub z_i: Option<Vec<C1::ScalarField>>,
498 pub external_inputs: Option<Vec<C1::ScalarField>>,
499 pub U_i: Option<LCCCS<C1>>,
500 pub Us: Option<Vec<LCCCS<C1>>>, // other U_i's to be folded that are not the main running instance
501 pub u_i_C: Option<C1>, // u_i.C
502 pub us: Option<Vec<CCCS<C1>>>, // other u_i's to be folded that are not the main incoming instance
503 pub U_i1_C: Option<C1>, // U_{i+1}.C
504 pub F: FC, // F circuit
505 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
506 pub nimfs_proof: Option<NIMFSProof<C1>>,
507
508 // cyclefold verifier on C1
509 pub cf_u_i_cmW: Option<C2>, // input, cf_u_i.cmW
510 pub cf_U_i: Option<CycleFoldCommittedInstance<C2>>, // input, RelaxedR1CS CycleFold instance
511 pub cf_x: Option<CF1<C1>>, // public input (cf_u_{i+1}.x[1])
512 pub cf_cmT: Option<C2>,
513}
514
515impl<C1, C2, GC2, FC, const MU: usize, const NU: usize> AugmentedFCircuit<C1, C2, GC2, FC, MU, NU>
516where
517 C1: CurveGroup,
518 C2: CurveGroup,
519 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
520 FC: FCircuit<CF1<C1>>,
521 <C1 as CurveGroup>::BaseField: PrimeField,
522 <C2 as CurveGroup>::BaseField: PrimeField,
523 <C1 as Group>::ScalarField: Absorb,
524 <C2 as Group>::ScalarField: Absorb,
525 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
526 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
527{
528 pub fn default(
529 poseidon_config: &PoseidonConfig<CF1<C1>>,
530 F_circuit: FC,
531 ccs: CCS<C1::ScalarField>,
532 ) -> Result<Self, Error> {
533 if MU < 1 || NU < 1 {
534 return Err(Error::CantBeZero("mu,nu".to_string()));
535 }
536 Ok(Self {
537 _c2: PhantomData,
538 _gc2: PhantomData,
539 poseidon_config: poseidon_config.clone(),
540 ccs,
541 pp_hash: None,
542 i: None,
543 i_usize: None,
544 z_0: None,
545 z_i: None,
546 external_inputs: None,
547 U_i: None,
548 Us: None,
549 u_i_C: None,
550 us: None,
551 U_i1_C: None,
552 F: F_circuit,
553 x: None,
554 nimfs_proof: None,
555 cf_u_i_cmW: None,
556 cf_U_i: None,
557 cf_x: None,
558 cf_cmT: None,
559 })
560 }
561
562 pub fn empty(
563 poseidon_config: &PoseidonConfig<CF1<C1>>,
564 F: FC, // FCircuit
565 ccs: Option<CCS<C1::ScalarField>>,
566 ) -> Result<Self, Error> {
567 let initial_ccs = CCS {
568 // m, n, s, s_prime and M will be overwritten by the `upper_bound_ccs' method
569 m: 0,
570 n: 0,
571 l: 2, // io_len
572 s: 1,
573 s_prime: 1,
574 t: 3, // note: this is only supports R1CS for the moment
575 q: 2,
576 d: 2,
577 S: vec![vec![0, 1], vec![2]],
578 c: vec![C1::ScalarField::one(), C1::ScalarField::one().neg()],
579 M: vec![],
580 };
581 let mut augmented_f_circuit = Self::default(poseidon_config, F, initial_ccs)?;
582 if ccs.is_some() {
583 augmented_f_circuit.ccs = ccs.unwrap();
584 } else {
585 augmented_f_circuit.ccs = augmented_f_circuit.upper_bound_ccs()?;
586 }
587 Ok(augmented_f_circuit)
588 }
589
590 /// This method computes the CCS parameters. This is used because there is a circular
591 /// dependency between the AugmentedFCircuit CCS and the CCS parameters m & n & s & s'.
592 /// For a stable FCircuit circuit, the CCS parameters can be computed in advance and can be
593 /// feed in as parameter for the AugmentedFCircuit::empty method to avoid computing them there.
594 pub fn upper_bound_ccs(&self) -> Result<CCS<C1::ScalarField>, Error> {
595 let r1cs = get_r1cs_from_cs::<CF1<C1>>(self.clone()).unwrap();
596 let mut ccs = CCS::from_r1cs(r1cs.clone());
597
598 let z_0 = vec![C1::ScalarField::zero(); self.F.state_len()];
599 let mut W_i = Witness::<C1::ScalarField>::dummy(&ccs);
600 let mut U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
601 let mut w_i = W_i.clone();
602 let mut u_i = CCCS::<C1>::dummy(ccs.l);
603
604 let n_iters = 2;
605 for _ in 0..n_iters {
606 let Us = vec![U_i.clone(); MU - 1];
607 let Ws = vec![W_i.clone(); MU - 1];
608 let us = vec![u_i.clone(); NU - 1];
609 let ws = vec![w_i.clone(); NU - 1];
610
611 let all_Us = [vec![U_i.clone()], Us.clone()].concat();
612 let all_us = [vec![u_i.clone()], us.clone()].concat();
613 let all_Ws = [vec![W_i.clone()], Ws].concat();
614 let all_ws = [vec![w_i.clone()], ws].concat();
615
616 let mut transcript_p: PoseidonSponge<C1::ScalarField> =
617 PoseidonSponge::<C1::ScalarField>::new(&self.poseidon_config.clone());
618 // since this is only for the number of constraints, no need to absorb the pp_hash here
619 let (nimfs_proof, U_i1, _, _) = NIMFS::<C1, PoseidonSponge<C1::ScalarField>>::prove(
620 &mut transcript_p,
621 &ccs,
622 &all_Us,
623 &all_us,
624 &all_Ws,
625 &all_ws,
626 )?;
627
628 let augmented_f_circuit = Self {
629 _c2: PhantomData,
630 _gc2: PhantomData,
631 poseidon_config: self.poseidon_config.clone(),
632 ccs: ccs.clone(),
633 pp_hash: Some(C1::ScalarField::zero()),
634 i: Some(C1::ScalarField::zero()),
635 i_usize: Some(0),
636 z_0: Some(z_0.clone()),
637 z_i: Some(z_0.clone()),
638 external_inputs: Some(vec![C1::ScalarField::zero(); self.F.external_inputs_len()]),
639 U_i: Some(U_i.clone()),
640 Us: Some(Us),
641 u_i_C: Some(u_i.C),
642 us: Some(us),
643 U_i1_C: Some(U_i1.C),
644 F: self.F.clone(),
645 x: Some(C1::ScalarField::zero()),
646 nimfs_proof: Some(nimfs_proof),
647 // cyclefold values
648 cf_u_i_cmW: None,
649 cf_U_i: None,
650 cf_x: None,
651 cf_cmT: None,
652 };
653
654 let cs: ConstraintSystem<C1::ScalarField>;
655 (cs, ccs) = augmented_f_circuit.compute_cs_ccs()?;
656 // prepare instances for next loop iteration
657 use crate::arith::r1cs::extract_w_x;
658 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<C1::ScalarField>(&cs);
659 u_i = CCCS::<C1> {
660 C: u_i.C,
661 x: r1cs_x_i1,
662 };
663 w_i = Witness::<C1::ScalarField> {
664 w: r1cs_w_i1.clone(),
665 r_w: C1::ScalarField::one(),
666 };
667 W_i = Witness::<C1::ScalarField>::dummy(&ccs);
668 U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
669 }
670 Ok(ccs)
671
672 // Ok(augmented_f_circuit.compute_cs_ccs()?.1)
673 }
674
675 /// Returns the cs (ConstraintSystem) and the CCS out of the AugmentedFCircuit
676 #[allow(clippy::type_complexity)]
677 pub fn compute_cs_ccs(
678 &self,
679 ) -> Result<(ConstraintSystem<C1::ScalarField>, CCS<C1::ScalarField>), Error> {
680 let cs = ConstraintSystem::<C1::ScalarField>::new_ref();
681 self.clone().generate_constraints(cs.clone())?;
682 cs.finalize();
683 let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?;
684 let r1cs = extract_r1cs::<C1::ScalarField>(&cs);
685 let ccs = CCS::from_r1cs(r1cs.clone());
686
687 Ok((cs, ccs))
688 }
689}
690
691impl<C1, C2, GC2, FC, const MU: usize, const NU: usize> ConstraintSynthesizer<CF1<C1>>
692 for AugmentedFCircuit<C1, C2, GC2, FC, MU, NU>
693where
694 C1: CurveGroup,
695 C2: CurveGroup,
696 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
697 FC: FCircuit<CF1<C1>>,
698 <C1 as CurveGroup>::BaseField: PrimeField,
699 <C2 as CurveGroup>::BaseField: PrimeField,
700 <C1 as Group>::ScalarField: Absorb,
701 <C2 as Group>::ScalarField: Absorb,
702 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
703 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
704{
705 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
706 let pp_hash = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
707 Ok(self.pp_hash.unwrap_or_else(CF1::<C1>::zero))
708 })?;
709 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
710 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
711 })?;
712 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
713 Ok(self
714 .z_0
715 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
716 })?;
717 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
718 Ok(self
719 .z_i
720 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
721 })?;
722 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
723 Ok(self
724 .external_inputs
725 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
726 })?;
727
728 let U_dummy = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
729 let u_dummy = CCCS::<C1>::dummy(self.ccs.l);
730
731 let U_i =
732 LCCCSVar::<C1>::new_witness(cs.clone(), || Ok(self.U_i.unwrap_or(U_dummy.clone())))?;
733 let Us = Vec::<LCCCSVar<C1>>::new_witness(cs.clone(), || {
734 Ok(self.Us.unwrap_or(vec![U_dummy.clone(); MU - 1]))
735 })?;
736 let us = Vec::<CCCSVar<C1>>::new_witness(cs.clone(), || {
737 Ok(self.us.unwrap_or(vec![u_dummy.clone(); MU - 1]))
738 })?;
739 let U_i1_C = NonNativeAffineVar::new_witness(cs.clone(), || {
740 Ok(self.U_i1_C.unwrap_or_else(C1::zero))
741 })?;
742 let nimfs_proof_dummy = NIMFSProof::<C1>::dummy(&self.ccs, MU, NU);
743 let nimfs_proof = ProofVar::<C1>::new_witness(cs.clone(), || {
744 Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy))
745 })?;
746
747 let cf_u_dummy =
748 CycleFoldCommittedInstance::dummy(HyperNovaCycleFoldConfig::<C1, MU, NU>::IO_LEN);
749 let cf_U_i = CycleFoldCommittedInstanceVar::<C2, GC2>::new_witness(cs.clone(), || {
750 Ok(self.cf_U_i.unwrap_or(cf_u_dummy.clone()))
751 })?;
752 let cf_cmT = GC2::new_witness(cs.clone(), || Ok(self.cf_cmT.unwrap_or_else(C2::zero)))?;
753
754 let sponge = PoseidonSpongeVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
755
756 // get z_{i+1} from the F circuit
757 let i_usize = self.i_usize.unwrap_or(0);
758 let z_i1 =
759 self.F
760 .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?;
761
762 let is_basecase = i.is_zero()?;
763 let is_not_basecase = is_basecase.not();
764
765 // Primary Part
766 // P.1. Compute u_i.x
767 // u_i.x[0] = H(i, z_0, z_i, U_i)
768 let (u_i_x, _) = U_i.clone().hash(
769 &sponge,
770 pp_hash.clone(),
771 i.clone(),
772 z_0.clone(),
773 z_i.clone(),
774 )?;
775 // u_i.x[1] = H(cf_U_i)
776 let (cf_u_i_x, cf_U_i_vec) = cf_U_i.clone().hash(&sponge, pp_hash.clone())?;
777
778 // P.2. Construct u_i
779 let u_i = CCCSVar::<C1> {
780 // u_i.C is provided by the prover as witness
781 C: NonNativeAffineVar::<C1>::new_witness(cs.clone(), || {
782 Ok(self.u_i_C.unwrap_or(C1::zero()))
783 })?,
784 // u_i.x is computed in step 1
785 x: vec![u_i_x, cf_u_i_x],
786 };
787
788 let all_Us = [vec![U_i.clone()], Us].concat();
789 let all_us = [vec![u_i.clone()], us].concat();
790
791 // P.3. NIMFS.verify, obtains U_{i+1} by folding [U_i] & [u_i].
792 // Notice that NIMFSGadget::fold_committed_instance does not fold C. We set `U_i1.C` to
793 // unconstrained witnesses `U_i1_C` respectively. Its correctness will be checked on the
794 // other curve.
795 let mut transcript = PoseidonSpongeVar::new(cs.clone(), &self.poseidon_config);
796 transcript.absorb(&pp_hash)?;
797 let (mut U_i1, rho_vec) = NIMFSGadget::<C1>::verify(
798 cs.clone(),
799 &self.ccs.clone(),
800 &mut transcript,
801 &all_Us,
802 &all_us,
803 nimfs_proof,
804 is_not_basecase.clone(),
805 )?;
806 U_i1.C = U_i1_C;
807
808 // P.4.a compute and check the first output of F'
809 let (u_i1_x, _) = U_i1.clone().hash(
810 &sponge,
811 pp_hash.clone(),
812 i + FpVar::<CF1<C1>>::one(),
813 z_0.clone(),
814 z_i1.clone(),
815 )?;
816 let (u_i1_x_base, _) = LCCCSVar::new_constant(cs.clone(), U_dummy)?.hash(
817 &sponge,
818 pp_hash.clone(),
819 FpVar::<CF1<C1>>::one(),
820 z_0.clone(),
821 z_i1.clone(),
822 )?;
823 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
824 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
825
826 // convert rho_bits of the rho_vec to a `NonNativeFieldVar`
827 let rho_vec_nonnat = rho_vec
828 .iter()
829 .map(|rho_i| {
830 let mut bits = rho_i.clone();
831 bits.resize(C1::BaseField::MODULUS_BIT_SIZE as usize, Boolean::FALSE);
832 NonNativeUintVar::from(&bits)
833 })
834 .collect();
835
836 // CycleFold part
837 // C.1. Compute cf1_u_i.x and cf2_u_i.x
838 let cf_x: Vec<NonNativeUintVar<CF2<C2>>> = [
839 rho_vec_nonnat,
840 all_Us
841 .iter()
842 .flat_map(|U| vec![U.C.x.clone(), U.C.y.clone()])
843 .collect(),
844 all_us
845 .iter()
846 .flat_map(|u| vec![u.C.x.clone(), u.C.y.clone()])
847 .collect(),
848 vec![U_i1.C.x, U_i1.C.y],
849 ]
850 .concat();
851
852 // ensure that cf_u has as public inputs the C from main instances U_i, u_i, U_i+1
853 // coordinates of the commitments.
854 // C.2. Construct `cf_u_i`
855 let cf_u_i = CycleFoldCommittedInstanceVar::<C2, GC2> {
856 // cf1_u_i.cmE = 0. Notice that we enforce cmE to be equal to 0 since it is allocated
857 // as 0.
858 cmE: GC2::zero(),
859 // cf1_u_i.u = 1
860 u: NonNativeUintVar::new_constant(cs.clone(), C1::BaseField::one())?,
861 // cf_u_i.cmW is provided by the prover as witness
862 cmW: GC2::new_witness(cs.clone(), || Ok(self.cf_u_i_cmW.unwrap_or(C2::zero())))?,
863 // cf_u_i.x is computed in step 1
864 x: cf_x,
865 };
866
867 // C.3. nifs.verify (fold_committed_instance), obtains cf_U_{i+1} by folding cf_u_i & cf_U_i.
868 // compute cf_r = H(cf_u_i, cf_U_i, cf_cmT)
869 // cf_r_bits is denoted by rho* in the paper.
870 let cf_r_bits = CycleFoldChallengeGadget::<C2, GC2>::get_challenge_gadget(
871 &mut transcript,
872 pp_hash.clone(),
873 cf_U_i_vec,
874 cf_u_i.clone(),
875 cf_cmT.clone(),
876 )?;
877 // Fold cf1_u_i & cf_U_i into cf1_U_{i+1}
878 let cf_U_i1 =
879 NIFSFullGadget::<C2, GC2>::fold_committed_instance(cf_r_bits, cf_cmT, cf_U_i, cf_u_i)?;
880
881 // Back to Primary Part
882 // P.4.b compute and check the second output of F'
883 // Base case: u_{i+1}.x[1] == H(cf_U_{\bot})
884 // Non-base case: u_{i+1}.x[1] == H(cf_U_{i+1})
885 let (cf_u_i1_x, _) = cf_U_i1.clone().hash(&sponge, pp_hash.clone())?;
886 let (cf_u_i1_x_base, _) =
887 CycleFoldCommittedInstanceVar::new_constant(cs.clone(), cf_u_dummy)?
888 .hash(&sponge, pp_hash)?;
889 let cf_x = FpVar::new_input(cs.clone(), || {
890 Ok(self.cf_x.unwrap_or(cf_u_i1_x_base.value()?))
891 })?;
892 cf_x.enforce_equal(&is_basecase.select(&cf_u_i1_x_base, &cf_u_i1_x)?)?;
893
894 Ok(())
895 }
896}
897
898#[cfg(test)]
899mod tests {
900 use ark_bn254::{constraints::GVar, Fq, Fr, G1Projective as Projective};
901 use ark_ff::BigInteger;
902 use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
903 use ark_std::{test_rng, UniformRand};
904 use std::time::Instant;
905
906 use super::*;
907 use crate::{
908 arith::{
909 ccs::tests::{get_test_ccs, get_test_z},
910 r1cs::extract_w_x,
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 nova::traits::NovaR1CS,
920 },
921 frontend::tests::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 folded_lcccs.check_relation(&ccs, &folded_witness).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.hash vs the R1CS constraints version
1134 #[test]
1135 pub fn test_lcccs_hash() {
1136 let mut rng = test_rng();
1137 let poseidon_config = poseidon_canonical_config::<Fr>();
1138 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1139
1140 let ccs = get_test_ccs();
1141 let z1 = get_test_z::<Fr>(3);
1142
1143 let (pedersen_params, _) =
1144 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1145 let pp_hash = Fr::from(42u32); // only for test
1146
1147 let i = Fr::from(3_u32);
1148 let z_0 = vec![Fr::from(3_u32)];
1149 let z_i = vec![Fr::from(3_u32)];
1150 let (lcccs, _) = ccs
1151 .to_lcccs::<_, _, Pedersen<Projective, true>, true>(&mut rng, &pedersen_params, &z1)
1152 .unwrap();
1153 let h = lcccs
1154 .clone()
1155 .hash(&sponge, pp_hash, i, z_0.clone(), z_i.clone());
1156
1157 let cs = ConstraintSystem::<Fr>::new_ref();
1158
1159 let spongeVar = PoseidonSpongeVar::<Fr>::new(cs.clone(), &poseidon_config);
1160 let pp_hashVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(pp_hash)).unwrap();
1161 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
1162 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
1163 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
1164 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
1165 let (hVar, _) = lcccsVar
1166 .clone()
1167 .hash(
1168 &spongeVar,
1169 pp_hashVar,
1170 iVar.clone(),
1171 z_0Var.clone(),
1172 z_iVar.clone(),
1173 )
1174 .unwrap();
1175 assert!(cs.is_satisfied().unwrap());
1176
1177 // check that the natively computed and in-circuit computed hashes match
1178 assert_eq!(hVar.value().unwrap(), h);
1179 }
1180
1181 #[test]
1182 pub fn test_augmented_f_circuit() {
1183 let mut rng = test_rng();
1184 let poseidon_config = poseidon_canonical_config::<Fr>();
1185 let sponge = PoseidonSponge::<Fr>::new(&poseidon_config);
1186
1187 const MU: usize = 3;
1188 const NU: usize = 3;
1189
1190 let start = Instant::now();
1191 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
1192 let mut augmented_f_circuit =
1193 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>, MU, NU>::empty(
1194 &poseidon_config,
1195 F_circuit,
1196 None,
1197 )
1198 .unwrap();
1199 let ccs = augmented_f_circuit.ccs.clone();
1200 println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed());
1201 println!("CCS m x n: {} x {}", ccs.m, ccs.n);
1202
1203 // CycleFold circuit
1204 let cs2 = ConstraintSystem::<Fq>::new_ref();
1205 let cf_circuit = HyperNovaCycleFoldCircuit::<Projective, GVar, MU, NU>::empty();
1206 cf_circuit.generate_constraints(cs2.clone()).unwrap();
1207 cs2.finalize();
1208 let cs2 = cs2
1209 .into_inner()
1210 .ok_or(Error::NoInnerConstraintSystem)
1211 .unwrap();
1212 let cf_r1cs = extract_r1cs::<Fq>(&cs2);
1213 println!("CF m x n: {} x {}", cf_r1cs.A.n_rows, cf_r1cs.A.n_cols);
1214
1215 let (pedersen_params, _) =
1216 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1217 let (cf_pedersen_params, _) =
1218 Pedersen::<Projective2>::setup(&mut rng, cf_r1cs.A.n_cols - cf_r1cs.l - 1).unwrap();
1219
1220 // public params hash
1221 let pp_hash = Fr::from(42u32); // only for test
1222
1223 // first step
1224 let z_0 = vec![Fr::from(3_u32)];
1225 let mut z_i = z_0.clone();
1226
1227 // prepare the dummy instances
1228 let W_dummy = Witness::<Fr>::dummy(&ccs);
1229 let U_dummy = LCCCS::<Projective>::dummy(ccs.l, ccs.t, ccs.s);
1230 let w_dummy = W_dummy.clone();
1231 let u_dummy = CCCS::<Projective>::dummy(ccs.l);
1232 let (cf_W_dummy, cf_U_dummy): (
1233 CycleFoldWitness<Projective2>,
1234 CycleFoldCommittedInstance<Projective2>,
1235 ) = cf_r1cs.dummy_instance();
1236
1237 // set the initial dummy instances
1238 let mut W_i = W_dummy.clone();
1239 let mut U_i = U_dummy.clone();
1240 let mut w_i = w_dummy.clone();
1241 let mut u_i = u_dummy.clone();
1242 let mut cf_W_i = cf_W_dummy.clone();
1243 let mut cf_U_i = cf_U_dummy.clone();
1244 u_i.x = vec![
1245 U_i.hash(&sponge, pp_hash, Fr::zero(), z_0.clone(), z_i.clone()),
1246 cf_U_i.hash_cyclefold(&sponge, pp_hash),
1247 ];
1248
1249 let n_steps: usize = 4;
1250 let mut iFr = Fr::zero();
1251 for i in 0..n_steps {
1252 let start = Instant::now();
1253
1254 // for this test, let Us & us be just an array of copies of the U_i & u_i respectively
1255 let Us = vec![U_i.clone(); MU - 1];
1256 let Ws = vec![W_i.clone(); MU - 1];
1257 let us = vec![u_i.clone(); NU - 1];
1258 let ws = vec![w_i.clone(); NU - 1];
1259 let all_Us = [vec![U_i.clone()], Us.clone()].concat();
1260 let all_us = [vec![u_i.clone()], us.clone()].concat();
1261 let all_Ws = [vec![W_i.clone()], Ws].concat();
1262 let all_ws = [vec![w_i.clone()], ws].concat();
1263
1264 let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap();
1265
1266 let (U_i1, W_i1);
1267
1268 if i == 0 {
1269 W_i1 = Witness::<Fr>::dummy(&ccs);
1270 U_i1 = LCCCS::dummy(ccs.l, ccs.t, ccs.s);
1271
1272 let u_i1_x = U_i1.hash(&sponge, pp_hash, Fr::one(), z_0.clone(), z_i1.clone());
1273
1274 // hash the initial (dummy) CycleFold instance, which is used as the 2nd public
1275 // input in the AugmentedFCircuit
1276 let cf_u_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1277
1278 augmented_f_circuit = AugmentedFCircuit::<
1279 Projective,
1280 Projective2,
1281 GVar2,
1282 CubicFCircuit<Fr>,
1283 MU,
1284 NU,
1285 > {
1286 _c2: PhantomData,
1287 _gc2: PhantomData,
1288 poseidon_config: poseidon_config.clone(),
1289 ccs: ccs.clone(),
1290 pp_hash: Some(pp_hash),
1291 i: Some(Fr::zero()),
1292 i_usize: Some(0),
1293 z_0: Some(z_0.clone()),
1294 z_i: Some(z_i.clone()),
1295 external_inputs: Some(vec![]),
1296 U_i: Some(U_i.clone()),
1297 Us: Some(Us.clone()),
1298 u_i_C: Some(u_i.C),
1299 us: Some(us.clone()),
1300 U_i1_C: Some(U_i1.C),
1301 F: F_circuit,
1302 x: Some(u_i1_x),
1303 nimfs_proof: None,
1304
1305 // cyclefold values
1306 cf_u_i_cmW: None,
1307 cf_U_i: None,
1308 cf_x: Some(cf_u_i1_x),
1309 cf_cmT: None,
1310 };
1311 } else {
1312 let mut transcript_p: PoseidonSponge<Fr> =
1313 PoseidonSponge::<Fr>::new(&poseidon_config.clone());
1314 transcript_p.absorb(&pp_hash);
1315 let (rho_powers, nimfs_proof);
1316 (nimfs_proof, U_i1, W_i1, rho_powers) =
1317 NIMFS::<Projective, PoseidonSponge<Fr>>::prove(
1318 &mut transcript_p,
1319 &ccs,
1320 &all_Us,
1321 &all_us,
1322 &all_Ws,
1323 &all_ws,
1324 )
1325 .unwrap();
1326
1327 // sanity check: check the folded instance relation
1328 U_i1.check_relation(&ccs, &W_i1).unwrap();
1329
1330 let u_i1_x =
1331 U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), z_0.clone(), z_i1.clone());
1332
1333 let rho_powers_Fq: Vec<Fq> = rho_powers
1334 .iter()
1335 .map(|rho_i| {
1336 Fq::from_bigint(BigInteger::from_bits_le(&rho_i.into_bigint().to_bits_le()))
1337 .unwrap()
1338 })
1339 .collect();
1340 let rho_powers_bits: Vec<Vec<bool>> = rho_powers
1341 .iter()
1342 .map(|rho_i| rho_i.into_bigint().to_bits_le()[..NOVA_N_BITS_RO].to_vec())
1343 .collect();
1344
1345 // CycleFold part:
1346 // get the vector used as public inputs 'x' in the CycleFold circuit
1347 let cf_u_i_x = [
1348 // all values for multiple instances
1349 rho_powers_Fq,
1350 get_cm_coordinates(&U_i.C),
1351 Us.iter()
1352 .flat_map(|Us_i| get_cm_coordinates(&Us_i.C))
1353 .collect(),
1354 get_cm_coordinates(&u_i.C),
1355 us.iter()
1356 .flat_map(|us_i| get_cm_coordinates(&us_i.C))
1357 .collect(),
1358 get_cm_coordinates(&U_i1.C),
1359 ]
1360 .concat();
1361
1362 let cf_circuit = HyperNovaCycleFoldCircuit::<Projective, GVar, MU, NU> {
1363 _gc: PhantomData,
1364 r_bits: Some(rho_powers_bits.clone()),
1365 points: Some(
1366 [
1367 vec![U_i.clone().C],
1368 Us.iter().map(|Us_i| Us_i.C).collect(),
1369 vec![u_i.clone().C],
1370 us.iter().map(|us_i| us_i.C).collect(),
1371 ]
1372 .concat(),
1373 ),
1374 x: Some(cf_u_i_x.clone()),
1375 };
1376
1377 // ensure that the CycleFoldCircuit is well defined
1378 assert_eq!(
1379 cf_circuit.r_bits.clone().unwrap().len(),
1380 HyperNovaCycleFoldConfig::<Projective, MU, NU>::N_INPUT_POINTS - 1
1381 );
1382 assert_eq!(
1383 cf_circuit.points.clone().unwrap().len(),
1384 HyperNovaCycleFoldConfig::<Projective, MU, NU>::N_INPUT_POINTS
1385 );
1386
1387 let (_cf_w_i, cf_u_i, cf_W_i1, cf_U_i1, cf_cmT, _) = fold_cyclefold_circuit::<
1388 HyperNovaCycleFoldConfig<Projective, MU, NU>,
1389 Projective,
1390 GVar,
1391 Projective2,
1392 GVar2,
1393 Pedersen<Projective2>,
1394 false,
1395 >(
1396 &mut transcript_p,
1397 cf_r1cs.clone(),
1398 cf_pedersen_params.clone(),
1399 pp_hash,
1400 cf_W_i.clone(), // CycleFold running instance witness
1401 cf_U_i.clone(), // CycleFold running instance
1402 cf_u_i_x, // CycleFold incoming instance
1403 cf_circuit,
1404 &mut rng,
1405 )
1406 .unwrap();
1407
1408 // hash the CycleFold folded instance, which is used as the 2nd public input in the
1409 // AugmentedFCircuit
1410 let cf_u_i1_x = cf_U_i1.hash_cyclefold(&sponge, pp_hash);
1411
1412 augmented_f_circuit = AugmentedFCircuit::<
1413 Projective,
1414 Projective2,
1415 GVar2,
1416 CubicFCircuit<Fr>,
1417 MU,
1418 NU,
1419 > {
1420 _c2: PhantomData,
1421 _gc2: PhantomData,
1422 poseidon_config: poseidon_config.clone(),
1423 ccs: ccs.clone(),
1424 pp_hash: Some(pp_hash),
1425 i: Some(iFr),
1426 i_usize: Some(i),
1427 z_0: Some(z_0.clone()),
1428 z_i: Some(z_i.clone()),
1429 external_inputs: Some(vec![]),
1430 U_i: Some(U_i.clone()),
1431 Us: Some(Us.clone()),
1432 u_i_C: Some(u_i.C),
1433 us: Some(us.clone()),
1434 U_i1_C: Some(U_i1.C),
1435 F: F_circuit,
1436 x: Some(u_i1_x),
1437 nimfs_proof: Some(nimfs_proof),
1438
1439 // cyclefold values
1440 cf_u_i_cmW: Some(cf_u_i.cmW),
1441 cf_U_i: Some(cf_U_i),
1442 cf_x: Some(cf_u_i1_x),
1443 cf_cmT: Some(cf_cmT),
1444 };
1445
1446 // assign the next round instances
1447 cf_W_i = cf_W_i1;
1448 cf_U_i = cf_U_i1;
1449 }
1450
1451 let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap();
1452 assert!(cs.is_satisfied().unwrap());
1453
1454 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<Fr>(&cs); // includes 1 and public inputs
1455 assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap());
1456 let r1cs_z = [vec![Fr::one()], r1cs_x_i1.clone(), r1cs_w_i1.clone()].concat();
1457 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
1458 // assign them directly to w_i, u_i.
1459 (u_i, w_i) = ccs
1460 .to_cccs::<_, _, Pedersen<Projective>, false>(&mut rng, &pedersen_params, &r1cs_z)
1461 .unwrap();
1462 u_i.check_relation(&ccs, &w_i).unwrap();
1463
1464 // sanity checks
1465 assert_eq!(w_i.w, r1cs_w_i1);
1466 assert_eq!(u_i.x, r1cs_x_i1);
1467 assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap());
1468 assert_eq!(u_i.x[1], augmented_f_circuit.cf_x.unwrap());
1469 let expected_u_i1_x =
1470 U_i1.hash(&sponge, pp_hash, iFr + Fr::one(), z_0.clone(), z_i1.clone());
1471 let expected_cf_U_i1_x = cf_U_i.hash_cyclefold(&sponge, pp_hash);
1472 // u_i is already u_i1 at this point, check that has the expected value at x[0]
1473 assert_eq!(u_i.x[0], expected_u_i1_x);
1474 assert_eq!(u_i.x[1], expected_cf_U_i1_x);
1475
1476 // set values for next iteration
1477 iFr += Fr::one();
1478 // assign z_{i+1} into z_i
1479 z_i = z_i1.clone();
1480 U_i = U_i1.clone();
1481 W_i = W_i1.clone();
1482
1483 // check the new LCCCS instance relation
1484 U_i.check_relation(&ccs, &W_i).unwrap();
1485 // check the new CCCS instance relation
1486 u_i.check_relation(&ccs, &w_i).unwrap();
1487
1488 // check the CycleFold instance relation
1489 cf_r1cs
1490 .check_relaxed_instance_relation(&cf_W_i, &cf_U_i)
1491 .unwrap();
1492
1493 println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
1494 }
1495 }
1496}