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