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) NIMFS verifier circuit
2use ark_crypto_primitives::crh::{
3 poseidon::constraints::{CRHGadget, CRHParametersVar},
4 CRHSchemeGadget,
5};
6use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
7use ark_ec::{CurveGroup, Group};
8use ark_ff::PrimeField;
9use ark_r1cs_std::{
10 alloc::{AllocVar, AllocationMode},
11 boolean::Boolean,
12 eq::EqGadget,
13 fields::{fp::FpVar, FieldVar},
14 groups::GroupOpsBounds,
15 prelude::CurveVar,
16 R1CSVar, ToConstraintFieldGadget,
17};
18use ark_relations::r1cs::{
19 ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, Namespace, SynthesisError,
20};
21use ark_std::{fmt::Debug, ops::Neg, One, Zero};
22use core::{borrow::Borrow, marker::PhantomData};
23
24use super::{
25 cccs::CCCS,
26 lcccs::LCCCS,
27 nimfs::{NIMFSProof, NIMFS},
28 Witness,
29};
30use crate::folding::circuits::{
31 nonnative::affine::NonNativeAffineVar,
32 sum_check::{IOPProofVar, SumCheckVerifierGadget, VPAuxInfoVar},
33 utils::EqEvalGadget,
34 CF1, CF2,
35};
36use crate::folding::nova::get_r1cs_from_cs;
37use crate::frontend::FCircuit;
38use crate::utils::virtual_polynomial::VPAuxInfo;
39use crate::Error;
40use crate::{
41 ccs::{
42 r1cs::{extract_r1cs, extract_w_x},
43 CCS,
44 },
45 transcript::{
46 poseidon::{PoseidonTranscript, PoseidonTranscriptVar},
47 Transcript, TranscriptVar,
48 },
49};
50
51/// Committed CCS instance
52#[derive(Debug, Clone)]
53pub struct CCCSVar<C: CurveGroup>
54where
55 <C as CurveGroup>::BaseField: PrimeField,
56{
57 // Commitment to witness
58 pub C: NonNativeAffineVar<C>,
59 // Public input/output
60 pub x: Vec<FpVar<CF1<C>>>,
61}
62impl<C> AllocVar<CCCS<C>, CF1<C>> for CCCSVar<C>
63where
64 C: CurveGroup,
65 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
66{
67 fn new_variable<T: Borrow<CCCS<C>>>(
68 cs: impl Into<Namespace<CF1<C>>>,
69 f: impl FnOnce() -> Result<T, SynthesisError>,
70 mode: AllocationMode,
71 ) -> Result<Self, SynthesisError> {
72 f().and_then(|val| {
73 let cs = cs.into();
74
75 let C = NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?;
76 let x: Vec<FpVar<C::ScalarField>> =
77 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
78
79 Ok(Self { C, x })
80 })
81 }
82}
83
84/// Linearized Committed CCS instance
85#[derive(Debug, Clone)]
86pub struct LCCCSVar<C: CurveGroup>
87where
88 <C as CurveGroup>::BaseField: PrimeField,
89{
90 // Commitment to witness
91 pub C: NonNativeAffineVar<C>,
92 // Relaxation factor of z for folded LCCCS
93 pub u: FpVar<CF1<C>>,
94 // Public input/output
95 pub x: Vec<FpVar<CF1<C>>>,
96 // Random evaluation point for the v_i
97 pub r_x: Vec<FpVar<CF1<C>>>,
98 // Vector of v_i
99 pub v: Vec<FpVar<CF1<C>>>,
100}
101impl<C> AllocVar<LCCCS<C>, CF1<C>> for LCCCSVar<C>
102where
103 C: CurveGroup,
104 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
105{
106 fn new_variable<T: Borrow<LCCCS<C>>>(
107 cs: impl Into<Namespace<CF1<C>>>,
108 f: impl FnOnce() -> Result<T, SynthesisError>,
109 mode: AllocationMode,
110 ) -> Result<Self, SynthesisError> {
111 f().and_then(|val| {
112 let cs = cs.into();
113
114 let C = NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?;
115 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
116 let x: Vec<FpVar<C::ScalarField>> =
117 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
118 let r_x: Vec<FpVar<C::ScalarField>> =
119 Vec::new_variable(cs.clone(), || Ok(val.borrow().r_x.clone()), mode)?;
120 let v: Vec<FpVar<C::ScalarField>> =
121 Vec::new_variable(cs.clone(), || Ok(val.borrow().v.clone()), mode)?;
122
123 Ok(Self { C, u, x, r_x, v })
124 })
125 }
126}
127
128impl<C> LCCCSVar<C>
129where
130 C: CurveGroup,
131 <C as Group>::ScalarField: Absorb,
132 <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
133{
134 /// [`LCCCSVar`].hash implements the LCCCS instance hash compatible with the native
135 /// implementation from LCCCS.hash.
136 /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U` is the LCCCS.
137 /// Additionally it returns the vector of the field elements from the self parameters, so they
138 /// can be reused in other gadgets avoiding recalculating (reconstraining) them.
139 #[allow(clippy::type_complexity)]
140 pub fn hash(
141 self,
142 crh_params: &CRHParametersVar<CF1<C>>,
143 i: FpVar<CF1<C>>,
144 z_0: Vec<FpVar<CF1<C>>>,
145 z_i: Vec<FpVar<CF1<C>>>,
146 ) -> Result<(FpVar<CF1<C>>, Vec<FpVar<CF1<C>>>), SynthesisError> {
147 let U_vec = [
148 self.C.to_constraint_field()?,
149 vec![self.u],
150 self.x,
151 self.r_x,
152 self.v,
153 ]
154 .concat();
155 let input = [vec![i], z_0, z_i, U_vec.clone()].concat();
156 Ok((
157 CRHGadget::<C::ScalarField>::evaluate(crh_params, &input)?,
158 U_vec,
159 ))
160 }
161}
162
163/// ProofVar defines a multifolding proof
164#[derive(Debug)]
165pub struct ProofVar<C: CurveGroup> {
166 pub sc_proof: IOPProofVar<C>,
167 #[allow(clippy::type_complexity)]
168 pub sigmas_thetas: (Vec<Vec<FpVar<CF1<C>>>>, Vec<Vec<FpVar<CF1<C>>>>),
169}
170impl<C> AllocVar<NIMFSProof<C>, CF1<C>> for ProofVar<C>
171where
172 C: CurveGroup,
173 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
174 <C as Group>::ScalarField: Absorb,
175{
176 fn new_variable<T: Borrow<NIMFSProof<C>>>(
177 cs: impl Into<Namespace<CF1<C>>>,
178 f: impl FnOnce() -> Result<T, SynthesisError>,
179 mode: AllocationMode,
180 ) -> Result<Self, SynthesisError> {
181 f().and_then(|val| {
182 let cs = cs.into();
183
184 let sc_proof = IOPProofVar::<C>::new_variable(
185 cs.clone(),
186 || Ok(val.borrow().sc_proof.clone()),
187 mode,
188 )?;
189 let sigmas: Vec<Vec<FpVar<CF1<C>>>> = val
190 .borrow()
191 .sigmas_thetas
192 .0
193 .iter()
194 .map(|sigmas_i| Vec::new_variable(cs.clone(), || Ok(sigmas_i.clone()), mode))
195 .collect::<Result<Vec<Vec<FpVar<CF1<C>>>>, SynthesisError>>()?;
196 let thetas: Vec<Vec<FpVar<CF1<C>>>> = val
197 .borrow()
198 .sigmas_thetas
199 .1
200 .iter()
201 .map(|thetas_i| Vec::new_variable(cs.clone(), || Ok(thetas_i.clone()), mode))
202 .collect::<Result<Vec<Vec<FpVar<CF1<C>>>>, SynthesisError>>()?;
203
204 Ok(Self {
205 sc_proof,
206 sigmas_thetas: (sigmas.clone(), thetas.clone()),
207 })
208 })
209 }
210}
211
212pub struct NIMFSGadget<C: CurveGroup> {
213 _c: PhantomData<C>,
214}
215impl<C: CurveGroup> NIMFSGadget<C>
216where
217 <C as CurveGroup>::BaseField: PrimeField,
218{
219 pub fn verify(
220 cs: ConstraintSystemRef<CF1<C>>,
221 // only used the CCS params, not the matrices
222 ccs: &CCS<C::ScalarField>,
223 mut transcript: impl TranscriptVar<C::ScalarField>,
224
225 running_instances: &[LCCCSVar<C>],
226 new_instances: &[CCCSVar<C>],
227 proof: ProofVar<C>,
228 enabled: Boolean<C::ScalarField>,
229 ) -> Result<LCCCSVar<C>, SynthesisError> {
230 // absorb instances to transcript
231 for U_i in running_instances {
232 let v = [
233 U_i.C.to_constraint_field()?,
234 vec![U_i.u.clone()],
235 U_i.x.clone(),
236 U_i.r_x.clone(),
237 U_i.v.clone(),
238 ]
239 .concat();
240 transcript.absorb_vec(&v)?;
241 }
242 for u_i in new_instances {
243 let v = [u_i.C.to_constraint_field()?, u_i.x.clone()].concat();
244 transcript.absorb_vec(&v)?;
245 }
246
247 // get the challenges
248 let gamma_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"gamma");
249 let gamma_scalar: FpVar<CF1<C>> =
250 FpVar::<CF1<C>>::new_constant(cs.clone(), gamma_scalar_raw)?;
251 transcript.absorb(gamma_scalar)?;
252 let gamma: FpVar<CF1<C>> = transcript.get_challenge()?;
253
254 let beta_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"beta");
255 let beta_scalar: FpVar<CF1<C>> =
256 FpVar::<CF1<C>>::new_constant(cs.clone(), beta_scalar_raw)?;
257 transcript.absorb(beta_scalar)?;
258 let beta: Vec<FpVar<CF1<C>>> = transcript.get_challenges(ccs.s)?;
259
260 let vp_aux_info_raw = VPAuxInfo::<C::ScalarField> {
261 max_degree: ccs.d + 1,
262 num_variables: ccs.s,
263 phantom: PhantomData::<C::ScalarField>,
264 };
265 let vp_aux_info = VPAuxInfoVar::<CF1<C>>::new_witness(cs.clone(), || Ok(vp_aux_info_raw))?;
266
267 // sumcheck
268 // first, compute the expected sumcheck sum: \sum gamma^j v_j
269 let mut sum_v_j_gamma = FpVar::<CF1<C>>::zero();
270 let mut gamma_j = FpVar::<C::ScalarField>::one();
271 for running_instance in running_instances.iter() {
272 for j in 0..running_instance.v.len() {
273 gamma_j *= gamma.clone();
274 sum_v_j_gamma += running_instance.v[j].clone() * gamma_j.clone();
275 }
276 }
277
278 // verify the interactive part of the sumcheck
279 let (e_vars, r_vars) = SumCheckVerifierGadget::<C>::verify(
280 &proof.sc_proof,
281 &vp_aux_info,
282 &mut transcript,
283 enabled.clone(),
284 )?;
285
286 // extract the randomness from the sumcheck
287 let r_x_prime = r_vars.clone();
288
289 // verify the claim c
290 let computed_c = compute_c_gadget(
291 cs.clone(),
292 ccs,
293 proof.sigmas_thetas.0.clone(), // sigmas
294 proof.sigmas_thetas.1.clone(), // thetas
295 gamma,
296 beta,
297 running_instances
298 .iter()
299 .map(|lcccs| lcccs.r_x.clone())
300 .collect(),
301 r_x_prime.clone(),
302 )?;
303 computed_c.conditional_enforce_equal(&e_vars[e_vars.len() - 1], &enabled)?;
304
305 // get the folding challenge
306 let rho_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"rho");
307 let rho_scalar: FpVar<CF1<C>> = FpVar::<CF1<C>>::new_constant(cs.clone(), rho_scalar_raw)?;
308 transcript.absorb(rho_scalar)?;
309 let rho: FpVar<CF1<C>> = transcript.get_challenge()?;
310
311 // return the folded instance
312 Self::fold(
313 running_instances,
314 new_instances,
315 proof.sigmas_thetas,
316 r_x_prime,
317 rho,
318 )
319 }
320
321 #[allow(clippy::type_complexity)]
322 fn fold(
323 lcccs: &[LCCCSVar<C>],
324 cccs: &[CCCSVar<C>],
325 sigmas_thetas: (Vec<Vec<FpVar<CF1<C>>>>, Vec<Vec<FpVar<CF1<C>>>>),
326 r_x_prime: Vec<FpVar<CF1<C>>>,
327 rho: FpVar<CF1<C>>,
328 ) -> Result<LCCCSVar<C>, SynthesisError> {
329 let (sigmas, thetas) = (sigmas_thetas.0.clone(), sigmas_thetas.1.clone());
330 let mut u_folded: FpVar<CF1<C>> = FpVar::zero();
331 let mut x_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); lcccs[0].x.len()];
332 let mut v_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); sigmas[0].len()];
333
334 let mut rho_i = FpVar::one();
335 for i in 0..(lcccs.len() + cccs.len()) {
336 let u: FpVar<CF1<C>>;
337 let x: Vec<FpVar<CF1<C>>>;
338 let v: Vec<FpVar<CF1<C>>>;
339 if i < lcccs.len() {
340 u = lcccs[i].u.clone();
341 x = lcccs[i].x.clone();
342 v = sigmas[i].clone();
343 } else {
344 u = FpVar::one();
345 x = cccs[i - lcccs.len()].x.clone();
346 v = thetas[i - lcccs.len()].clone();
347 }
348
349 u_folded += rho_i.clone() * u;
350 x_folded = x_folded
351 .iter()
352 .zip(
353 x.iter()
354 .map(|x_i| x_i * rho_i.clone())
355 .collect::<Vec<FpVar<CF1<C>>>>(),
356 )
357 .map(|(a_i, b_i)| a_i + b_i)
358 .collect();
359
360 v_folded = v_folded
361 .iter()
362 .zip(
363 v.iter()
364 .map(|x_i| x_i * rho_i.clone())
365 .collect::<Vec<FpVar<CF1<C>>>>(),
366 )
367 .map(|(a_i, b_i)| a_i + b_i)
368 .collect();
369
370 rho_i *= rho.clone();
371 }
372
373 Ok(LCCCSVar::<C> {
374 C: lcccs[0].C.clone(), // WIP this will come from the cyclefold circuit
375 u: u_folded,
376 x: x_folded,
377 r_x: r_x_prime,
378 v: v_folded,
379 })
380 }
381}
382
383/// computes c from the step 5 in section 5 of HyperNova, adapted to multiple LCCCS & CCCS
384/// instances:
385/// $$
386/// c = \sum_{i \in [\mu]} \left(\sum_{j \in [t]} \gamma^{i \cdot t + j} \cdot e_i \cdot \sigma_{i,j} \right)
387/// + \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}
388/// \theta_{k,j} \right)
389/// $$
390#[allow(clippy::too_many_arguments)]
391fn compute_c_gadget<F: PrimeField>(
392 cs: ConstraintSystemRef<F>,
393 ccs: &CCS<F>,
394 vec_sigmas: Vec<Vec<FpVar<F>>>,
395 vec_thetas: Vec<Vec<FpVar<F>>>,
396 gamma: FpVar<F>,
397 beta: Vec<FpVar<F>>,
398 vec_r_x: Vec<Vec<FpVar<F>>>,
399 vec_r_x_prime: Vec<FpVar<F>>,
400) -> Result<FpVar<F>, SynthesisError> {
401 let mut e_lcccs = Vec::new();
402 for r_x in vec_r_x.iter() {
403 e_lcccs.push(EqEvalGadget::eq_eval(r_x, &vec_r_x_prime)?);
404 }
405
406 let mut c = FpVar::<F>::zero();
407 let mut current_gamma = FpVar::<F>::one();
408 for i in 0..vec_sigmas.len() {
409 for j in 0..ccs.t {
410 c += current_gamma.clone() * e_lcccs[i].clone() * vec_sigmas[i][j].clone();
411 current_gamma *= gamma.clone();
412 }
413 }
414
415 let ccs_c = Vec::<FpVar<F>>::new_constant(cs.clone(), ccs.c.clone())?;
416 let e_k = EqEvalGadget::eq_eval(&beta, &vec_r_x_prime)?;
417 #[allow(clippy::needless_range_loop)]
418 for k in 0..vec_thetas.len() {
419 let mut sum = FpVar::<F>::zero();
420 for i in 0..ccs.q {
421 let mut prod = FpVar::<F>::one();
422 for j in ccs.S[i].clone() {
423 prod *= vec_thetas[k][j].clone();
424 }
425 sum += ccs_c[i].clone() * prod;
426 }
427 c += current_gamma.clone() * e_k.clone() * sum;
428 current_gamma *= gamma.clone();
429 }
430 Ok(c)
431}
432
433#[derive(Debug, Clone)]
434pub struct AugmentedFCircuit<
435 C1: CurveGroup,
436 C2: CurveGroup,
437 GC2: CurveVar<C2, CF2<C2>>,
438 FC: FCircuit<CF1<C1>>,
439> where
440 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
441{
442 pub _c2: PhantomData<C2>,
443 pub _gc2: PhantomData<GC2>,
444 pub poseidon_config: PoseidonConfig<CF1<C1>>,
445 pub ccs: CCS<C1::ScalarField>, // CCS of the AugmentedFCircuit
446 pub i: Option<CF1<C1>>,
447 pub i_usize: Option<usize>,
448 pub z_0: Option<Vec<C1::ScalarField>>,
449 pub z_i: Option<Vec<C1::ScalarField>>,
450 pub external_inputs: Option<Vec<C1::ScalarField>>,
451 pub u_i_C: Option<C1>, // u_i.C
452 pub U_i: Option<LCCCS<C1>>,
453 pub U_i1_C: Option<C1>, // U_{i+1}.C
454 pub F: FC, // F circuit
455 pub x: Option<CF1<C1>>, // public input (u_{i+1}.x[0])
456 pub nimfs_proof: Option<NIMFSProof<C1>>,
457}
458
459impl<C1, C2, GC2, FC> AugmentedFCircuit<C1, C2, GC2, FC>
460where
461 C1: CurveGroup,
462 C2: CurveGroup,
463 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
464 FC: FCircuit<CF1<C1>>,
465 <C1 as CurveGroup>::BaseField: PrimeField,
466 <C2 as CurveGroup>::BaseField: PrimeField,
467 <C1 as Group>::ScalarField: Absorb,
468 <C2 as Group>::ScalarField: Absorb,
469 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
470 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
471{
472 pub fn default(
473 poseidon_config: &PoseidonConfig<CF1<C1>>,
474 F_circuit: FC,
475 ccs: CCS<C1::ScalarField>,
476 ) -> Self {
477 Self {
478 _c2: PhantomData,
479 _gc2: PhantomData,
480 poseidon_config: poseidon_config.clone(),
481 ccs,
482 i: None,
483 i_usize: None,
484 z_0: None,
485 z_i: None,
486 external_inputs: None,
487 u_i_C: None,
488 U_i: None,
489 U_i1_C: None,
490 F: F_circuit,
491 x: None,
492 nimfs_proof: None,
493 }
494 }
495
496 pub fn empty(
497 poseidon_config: &PoseidonConfig<CF1<C1>>,
498 F_circuit: FC,
499 ccs: Option<CCS<C1::ScalarField>>,
500 ) -> Result<Self, Error> {
501 let initial_ccs = CCS {
502 // m, n, s, s_prime and M will be overwritten by the `upper_bound_ccs' method
503 m: 0,
504 n: 0,
505 l: 2, // io_len
506 s: 1,
507 s_prime: 1,
508 t: 3, // note: this is only supports R1CS for the moment
509 q: 2,
510 d: 2,
511 S: vec![vec![0, 1], vec![2]],
512 c: vec![C1::ScalarField::one(), C1::ScalarField::one().neg()],
513 M: vec![],
514 };
515 let mut augmented_f_circuit = Self::default(poseidon_config, F_circuit, initial_ccs);
516 if ccs.is_some() {
517 augmented_f_circuit.ccs = ccs.unwrap();
518 } else {
519 augmented_f_circuit.ccs = augmented_f_circuit.upper_bound_ccs()?;
520 }
521 Ok(augmented_f_circuit)
522 }
523
524 /// This method computes the CCS parameters. This is used because there is a circular
525 /// dependency between the AugmentedFCircuit CCS and the CCS parameters m & n & s & s'.
526 /// For a stable FCircuit circuit, the CCS parameters can be computed in advance and can be
527 /// feed in as parameter for the AugmentedFCircuit::empty method to avoid computing them there.
528 pub fn upper_bound_ccs(&self) -> Result<CCS<C1::ScalarField>, Error> {
529 let r1cs = get_r1cs_from_cs::<CF1<C1>>(self.clone()).unwrap();
530 let mut ccs = CCS::from_r1cs(r1cs.clone());
531
532 let z_0 = vec![C1::ScalarField::zero(); self.F.state_len()];
533 let mut W_i =
534 Witness::<C1::ScalarField>::new(vec![C1::ScalarField::zero(); ccs.n - ccs.l - 1]);
535 let mut U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
536 let mut w_i = W_i.clone();
537 let mut u_i = CCCS::<C1>::dummy(ccs.l);
538
539 let n_iters = 3;
540
541 for _ in 0..n_iters {
542 let mut transcript_p: PoseidonTranscript<C1> =
543 PoseidonTranscript::<C1>::new(&self.poseidon_config.clone());
544 let (nimfs_proof, U_i1, _) = NIMFS::<C1, PoseidonTranscript<C1>>::prove(
545 &mut transcript_p,
546 &ccs,
547 &[U_i.clone()],
548 &[u_i.clone()],
549 &[W_i.clone()],
550 &[w_i.clone()],
551 )
552 .unwrap();
553
554 let augmented_f_circuit = Self {
555 _c2: PhantomData,
556 _gc2: PhantomData,
557 poseidon_config: self.poseidon_config.clone(),
558 ccs: ccs.clone(),
559 i: Some(C1::ScalarField::zero()),
560 i_usize: Some(0),
561 z_0: Some(z_0.clone()),
562 z_i: Some(z_0.clone()),
563 external_inputs: Some(vec![]),
564 u_i_C: Some(u_i.C),
565 U_i: Some(U_i.clone()),
566 U_i1_C: Some(U_i1.C),
567 F: self.F.clone(),
568 x: Some(C1::ScalarField::zero()),
569 nimfs_proof: Some(nimfs_proof),
570 };
571
572 let cs: ConstraintSystem<C1::ScalarField>;
573 (cs, ccs) = augmented_f_circuit.compute_cs_ccs()?;
574
575 // prepare instances for next loop iteration
576 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<C1::ScalarField>(&cs); // includes 1 and public inputs
577 u_i = CCCS::<C1> {
578 C: u_i.C,
579 x: r1cs_x_i1,
580 };
581 w_i = Witness::<C1::ScalarField> {
582 w: r1cs_w_i1.clone(),
583 r_w: C1::ScalarField::one(),
584 };
585 W_i = Witness::<C1::ScalarField>::dummy(&ccs);
586 U_i = LCCCS::<C1>::dummy(ccs.l, ccs.t, ccs.s);
587 }
588 Ok(ccs)
589 }
590
591 /// returns the cs (ConstraintSystem) and the CCS out of the AugmentedFCircuit
592 #[allow(clippy::type_complexity)]
593 fn compute_cs_ccs(
594 &self,
595 ) -> Result<(ConstraintSystem<C1::ScalarField>, CCS<C1::ScalarField>), Error> {
596 let cs = ConstraintSystem::<C1::ScalarField>::new_ref();
597 self.clone().generate_constraints(cs.clone())?;
598 cs.finalize();
599 let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?;
600 let r1cs = extract_r1cs::<C1::ScalarField>(&cs);
601 let ccs = CCS::from_r1cs(r1cs.clone());
602
603 Ok((cs, ccs))
604 }
605}
606
607impl<C1, C2, GC2, FC> ConstraintSynthesizer<CF1<C1>> for AugmentedFCircuit<C1, C2, GC2, FC>
608where
609 C1: CurveGroup,
610 C2: CurveGroup,
611 GC2: CurveVar<C2, CF2<C2>> + ToConstraintFieldGadget<CF2<C2>>,
612 FC: FCircuit<CF1<C1>>,
613 <C1 as CurveGroup>::BaseField: PrimeField,
614 <C2 as CurveGroup>::BaseField: PrimeField,
615 <C1 as Group>::ScalarField: Absorb,
616 <C2 as Group>::ScalarField: Absorb,
617 C1: CurveGroup<BaseField = C2::ScalarField, ScalarField = C2::BaseField>,
618 for<'a> &'a GC2: GroupOpsBounds<'a, C2, GC2>,
619{
620 fn generate_constraints(self, cs: ConstraintSystemRef<CF1<C1>>) -> Result<(), SynthesisError> {
621 let i = FpVar::<CF1<C1>>::new_witness(cs.clone(), || {
622 Ok(self.i.unwrap_or_else(CF1::<C1>::zero))
623 })?;
624 let z_0 = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
625 Ok(self
626 .z_0
627 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
628 })?;
629 let z_i = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
630 Ok(self
631 .z_i
632 .unwrap_or(vec![CF1::<C1>::zero(); self.F.state_len()]))
633 })?;
634 let external_inputs = Vec::<FpVar<CF1<C1>>>::new_witness(cs.clone(), || {
635 Ok(self
636 .external_inputs
637 .unwrap_or(vec![CF1::<C1>::zero(); self.F.external_inputs_len()]))
638 })?;
639
640 let U_dummy = LCCCS::<C1>::dummy(self.ccs.l, self.ccs.t, self.ccs.s);
641
642 let U_i =
643 LCCCSVar::<C1>::new_witness(cs.clone(), || Ok(self.U_i.unwrap_or(U_dummy.clone())))?;
644 let U_i1_C = NonNativeAffineVar::new_witness(cs.clone(), || {
645 Ok(self.U_i1_C.unwrap_or_else(C1::zero))
646 })?;
647 let mu = 1; // Note: at this commit, only 2-to-1 instance fold is supported
648 let nu = 1;
649 let nimfs_proof_dummy = NIMFSProof::<C1>::dummy(&self.ccs, mu, nu);
650 let nimfs_proof = ProofVar::<C1>::new_witness(cs.clone(), || {
651 Ok(self.nimfs_proof.unwrap_or(nimfs_proof_dummy))
652 })?;
653
654 let crh_params = CRHParametersVar::<C1::ScalarField>::new_constant(
655 cs.clone(),
656 self.poseidon_config.clone(),
657 )?;
658
659 // get z_{i+1} from the F circuit
660 let i_usize = self.i_usize.unwrap_or(0);
661 let z_i1 =
662 self.F
663 .generate_step_constraints(cs.clone(), i_usize, z_i.clone(), external_inputs)?;
664
665 let is_basecase = i.is_zero()?;
666 let is_not_basecase = is_basecase.not();
667
668 // Primary Part
669 // P.1. Compute u_i.x
670 // u_i.x[0] = H(i, z_0, z_i, U_i)
671 let (u_i_x, _) = U_i
672 .clone()
673 .hash(&crh_params, i.clone(), z_0.clone(), z_i.clone())?;
674
675 // P.2. Construct u_i
676 let u_i = CCCSVar::<C1> {
677 // u_i.C is provided by the prover as witness
678 C: NonNativeAffineVar::<C1>::new_witness(cs.clone(), || {
679 Ok(self.u_i_C.unwrap_or(C1::zero()))
680 })?,
681 // u_i.x is computed in step 1
682 x: vec![u_i_x],
683 };
684
685 // P.3. NIMFS.verify, obtains U_{i+1} by folding [U_i] & [u_i].
686 // Notice that NIMFSGadget::fold_committed_instance does not fold C. We set `U_i1.C` to
687 // unconstrained witnesses `U_i1_C` respectively. Its correctness will be checked on the
688 // other curve.
689 let transcript =
690 PoseidonTranscriptVar::<C1::ScalarField>::new(cs.clone(), &self.poseidon_config);
691 let mut U_i1 = NIMFSGadget::<C1>::verify(
692 cs.clone(),
693 &self.ccs.clone(),
694 transcript,
695 &[U_i.clone()],
696 &[u_i.clone()],
697 nimfs_proof,
698 is_not_basecase.clone(),
699 )?;
700 U_i1.C = U_i1_C;
701
702 // P.4.a compute and check the first output of F'
703 // Base case: u_{i+1}.x[0] == H((1, z_0, z_{i+1}, U_{i+1})
704 // Non-base case: u_{i+1}.x[0] == H((i+1, z_0, z_{i+1}, U_{i+1})
705 let (u_i1_x, _) = U_i1.clone().hash(
706 &crh_params,
707 i + FpVar::<CF1<C1>>::one(),
708 z_0.clone(),
709 z_i1.clone(),
710 )?;
711 let (u_i1_x_base, _) = U_i1.hash(
712 &crh_params,
713 FpVar::<CF1<C1>>::one(),
714 z_0.clone(),
715 z_i1.clone(),
716 )?;
717
718 let x = FpVar::new_input(cs.clone(), || Ok(self.x.unwrap_or(u_i1_x_base.value()?)))?;
719 x.enforce_equal(&is_basecase.select(&u_i1_x_base, &u_i1_x)?)?;
720
721 Ok(())
722 }
723}
724
725#[cfg(test)]
726mod tests {
727 use ark_bn254::{Fr, G1Projective as Projective};
728 use ark_grumpkin::{constraints::GVar as GVar2, Projective as Projective2};
729 use ark_r1cs_std::{alloc::AllocVar, fields::fp::FpVar, R1CSVar};
730 use ark_std::{test_rng, UniformRand};
731 use std::time::Instant;
732
733 use super::*;
734 use crate::{
735 ccs::{
736 r1cs::extract_w_x,
737 tests::{get_test_ccs, get_test_z},
738 CCS,
739 },
740 commitment::{pedersen::Pedersen, CommitmentScheme},
741 folding::hypernova::{
742 nimfs::NIMFS,
743 utils::{compute_c, compute_sigmas_thetas},
744 Witness,
745 },
746 frontend::tests::CubicFCircuit,
747 transcript::{
748 poseidon::{poseidon_canonical_config, PoseidonTranscript, PoseidonTranscriptVar},
749 Transcript,
750 },
751 };
752
753 #[test]
754 pub fn test_compute_c_gadget() {
755 // number of LCCCS & CCCS instances to fold in a single step
756 let mu = 32;
757 let nu = 42;
758
759 let mut z_lcccs = Vec::new();
760 for i in 0..mu {
761 let z = get_test_z(i + 3);
762 z_lcccs.push(z);
763 }
764 let mut z_cccs = Vec::new();
765 for i in 0..nu {
766 let z = get_test_z(i + 3);
767 z_cccs.push(z);
768 }
769
770 let ccs: CCS<Fr> = get_test_ccs();
771
772 let mut rng = test_rng();
773 let gamma: Fr = Fr::rand(&mut rng);
774 let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
775 let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
776
777 let (pedersen_params, _) =
778 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
779
780 // Create the LCCCS instances out of z_lcccs
781 let mut lcccs_instances = Vec::new();
782 for z_i in z_lcccs.iter() {
783 let (inst, _) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap();
784 lcccs_instances.push(inst);
785 }
786 // Create the CCCS instance out of z_cccs
787 let mut cccs_instances = Vec::new();
788 for z_i in z_cccs.iter() {
789 let (inst, _) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap();
790 cccs_instances.push(inst);
791 }
792
793 let sigmas_thetas = compute_sigmas_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime).unwrap();
794
795 let expected_c = compute_c(
796 &ccs,
797 &sigmas_thetas,
798 gamma,
799 &beta,
800 &lcccs_instances
801 .iter()
802 .map(|lcccs| lcccs.r_x.clone())
803 .collect(),
804 &r_x_prime,
805 )
806 .unwrap();
807
808 let cs = ConstraintSystem::<Fr>::new_ref();
809 let mut vec_sigmas = Vec::new();
810 let mut vec_thetas = Vec::new();
811 for sigmas in sigmas_thetas.0 {
812 vec_sigmas
813 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap());
814 }
815 for thetas in sigmas_thetas.1 {
816 vec_thetas
817 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap());
818 }
819 let vec_r_x: Vec<Vec<FpVar<Fr>>> = lcccs_instances
820 .iter()
821 .map(|lcccs| {
822 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap()
823 })
824 .collect();
825 let vec_r_x_prime =
826 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap();
827 let gamma_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(gamma)).unwrap();
828 let beta_var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap();
829
830 let computed_c = compute_c_gadget(
831 cs.clone(),
832 &ccs,
833 vec_sigmas,
834 vec_thetas,
835 gamma_var,
836 beta_var,
837 vec_r_x,
838 vec_r_x_prime,
839 )
840 .unwrap();
841
842 assert_eq!(expected_c, computed_c.value().unwrap());
843 }
844
845 /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step,
846 /// to verify the folding in the NIMFSGadget circuit
847 #[test]
848 pub fn test_nimfs_gadget_verify() {
849 let mut rng = test_rng();
850
851 // Create a basic CCS circuit
852 let ccs = get_test_ccs::<Fr>();
853 let (pedersen_params, _) =
854 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
855
856 let mu = 32;
857 let nu = 42;
858
859 // Generate a mu LCCCS & nu CCCS satisfying witness
860 let mut z_lcccs = Vec::new();
861 for i in 0..mu {
862 let z = get_test_z(i + 3);
863 z_lcccs.push(z);
864 }
865 let mut z_cccs = Vec::new();
866 for i in 0..nu {
867 let z = get_test_z(nu + i + 3);
868 z_cccs.push(z);
869 }
870
871 // Create the LCCCS instances out of z_lcccs
872 let mut lcccs_instances = Vec::new();
873 let mut w_lcccs = Vec::new();
874 for z_i in z_lcccs.iter() {
875 let (running_instance, w) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap();
876 lcccs_instances.push(running_instance);
877 w_lcccs.push(w);
878 }
879 // Create the CCCS instance out of z_cccs
880 let mut cccs_instances = Vec::new();
881 let mut w_cccs = Vec::new();
882 for z_i in z_cccs.iter() {
883 let (new_instance, w) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap();
884 cccs_instances.push(new_instance);
885 w_cccs.push(w);
886 }
887
888 // Prover's transcript
889 let poseidon_config = poseidon_canonical_config::<Fr>();
890 let mut transcript_p: PoseidonTranscript<Projective> =
891 PoseidonTranscript::<Projective>::new(&poseidon_config);
892
893 // Run the prover side of the multifolding
894 let (proof, folded_lcccs, folded_witness) =
895 NIMFS::<Projective, PoseidonTranscript<Projective>>::prove(
896 &mut transcript_p,
897 &ccs,
898 &lcccs_instances,
899 &cccs_instances,
900 &w_lcccs,
901 &w_cccs,
902 )
903 .unwrap();
904
905 // Verifier's transcript
906 let mut transcript_v: PoseidonTranscript<Projective> =
907 PoseidonTranscript::<Projective>::new(&poseidon_config);
908
909 // Run the verifier side of the multifolding
910 let folded_lcccs_v = NIMFS::<Projective, PoseidonTranscript<Projective>>::verify(
911 &mut transcript_v,
912 &ccs,
913 &lcccs_instances,
914 &cccs_instances,
915 proof.clone(),
916 )
917 .unwrap();
918 assert_eq!(folded_lcccs, folded_lcccs_v);
919
920 // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
921 folded_lcccs
922 .check_relation(&pedersen_params, &ccs, &folded_witness)
923 .unwrap();
924
925 // allocate circuit inputs
926 let cs = ConstraintSystem::<Fr>::new_ref();
927 let lcccs_instancesVar =
928 Vec::<LCCCSVar<Projective>>::new_witness(cs.clone(), || Ok(lcccs_instances.clone()))
929 .unwrap();
930 let cccs_instancesVar =
931 Vec::<CCCSVar<Projective>>::new_witness(cs.clone(), || Ok(cccs_instances.clone()))
932 .unwrap();
933 let proofVar =
934 ProofVar::<Projective>::new_witness(cs.clone(), || Ok(proof.clone())).unwrap();
935 let transcriptVar = PoseidonTranscriptVar::<Fr>::new(cs.clone(), &poseidon_config);
936
937 let enabled = Boolean::<Fr>::new_witness(cs.clone(), || Ok(true)).unwrap();
938 let folded_lcccsVar = NIMFSGadget::<Projective>::verify(
939 cs.clone(),
940 &ccs,
941 transcriptVar,
942 &lcccs_instancesVar,
943 &cccs_instancesVar,
944 proofVar,
945 enabled,
946 )
947 .unwrap();
948 assert!(cs.is_satisfied().unwrap());
949 assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u);
950 }
951
952 /// test that checks the native LCCCS.hash vs the R1CS constraints version
953 #[test]
954 pub fn test_lcccs_hash() {
955 let mut rng = test_rng();
956 let poseidon_config = poseidon_canonical_config::<Fr>();
957
958 let ccs = get_test_ccs();
959 let z1 = get_test_z::<Fr>(3);
960
961 let (pedersen_params, _) =
962 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
963
964 let i = Fr::from(3_u32);
965 let z_0 = vec![Fr::from(3_u32)];
966 let z_i = vec![Fr::from(3_u32)];
967 let (lcccs, _) = ccs.to_lcccs(&mut rng, &pedersen_params, &z1).unwrap();
968 let h = lcccs
969 .clone()
970 .hash(&poseidon_config, i, z_0.clone(), z_i.clone())
971 .unwrap();
972
973 let cs = ConstraintSystem::<Fr>::new_ref();
974
975 let crh_params = CRHParametersVar::<Fr>::new_constant(cs.clone(), poseidon_config).unwrap();
976 let iVar = FpVar::<Fr>::new_witness(cs.clone(), || Ok(i)).unwrap();
977 let z_0Var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_0.clone())).unwrap();
978 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i.clone())).unwrap();
979 let lcccsVar = LCCCSVar::<Projective>::new_witness(cs.clone(), || Ok(lcccs)).unwrap();
980 let (hVar, _) = lcccsVar
981 .clone()
982 .hash(&crh_params, iVar.clone(), z_0Var.clone(), z_iVar.clone())
983 .unwrap();
984 assert!(cs.is_satisfied().unwrap());
985
986 // check that the natively computed and in-circuit computed hashes match
987 assert_eq!(hVar.value().unwrap(), h);
988 }
989
990 #[test]
991 pub fn test_augmented_f_circuit() {
992 let mut rng = test_rng();
993 let poseidon_config = poseidon_canonical_config::<Fr>();
994
995 let start = Instant::now();
996 let F_circuit = CubicFCircuit::<Fr>::new(()).unwrap();
997 let mut augmented_f_circuit = AugmentedFCircuit::<
998 Projective,
999 Projective2,
1000 GVar2,
1001 CubicFCircuit<Fr>,
1002 >::empty(&poseidon_config, F_circuit, None)
1003 .unwrap();
1004 let ccs = augmented_f_circuit.ccs.clone();
1005 println!("AugmentedFCircuit & CCS generation: {:?}", start.elapsed());
1006 println!("CCS m x n: {} x {}", ccs.m, ccs.n);
1007
1008 let (pedersen_params, _) =
1009 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
1010
1011 // first step
1012 let z_0 = vec![Fr::from(3_u32)];
1013 let mut z_i = z_0.clone();
1014
1015 let W_dummy = Witness::<Fr>::new(vec![Fr::zero(); ccs.n - ccs.l - 1]);
1016 let U_dummy = LCCCS::<Projective>::dummy(ccs.l, ccs.t, ccs.s);
1017 let w_dummy = W_dummy.clone();
1018 let u_dummy = CCCS::<Projective>::dummy(ccs.l);
1019
1020 // set the initial dummy instances
1021 let mut W_i = W_dummy.clone();
1022 let mut U_i = U_dummy.clone();
1023 let mut w_i = w_dummy.clone();
1024 let mut u_i = u_dummy.clone();
1025 u_i.x = vec![U_i
1026 .hash(&poseidon_config, Fr::zero(), z_0.clone(), z_i.clone())
1027 .unwrap()];
1028
1029 let n_steps: usize = 4;
1030 let mut iFr = Fr::zero();
1031 for i in 0..n_steps {
1032 let start = Instant::now();
1033 let mut transcript_p: PoseidonTranscript<Projective> =
1034 PoseidonTranscript::<Projective>::new(&poseidon_config.clone());
1035 let (nimfs_proof, U_i1, W_i1) =
1036 NIMFS::<Projective, PoseidonTranscript<Projective>>::prove(
1037 &mut transcript_p,
1038 &ccs,
1039 &[U_i.clone()],
1040 &[u_i.clone()],
1041 &[W_i.clone()],
1042 &[w_i.clone()],
1043 )
1044 .unwrap();
1045
1046 // sanity check: check the folded instance relation
1047 U_i1.check_relation(&pedersen_params, &ccs, &W_i1).unwrap();
1048
1049 let z_i1 = F_circuit.step_native(i, z_i.clone(), vec![]).unwrap();
1050 let u_i1_x = U_i1
1051 .hash(&poseidon_config, iFr + Fr::one(), z_0.clone(), z_i1.clone())
1052 .unwrap();
1053
1054 augmented_f_circuit =
1055 AugmentedFCircuit::<Projective, Projective2, GVar2, CubicFCircuit<Fr>> {
1056 _c2: PhantomData,
1057 _gc2: PhantomData,
1058 poseidon_config: poseidon_config.clone(),
1059 ccs: ccs.clone(),
1060 i: Some(iFr),
1061 i_usize: Some(i),
1062 z_0: Some(z_0.clone()),
1063 z_i: Some(z_i.clone()),
1064 external_inputs: Some(vec![]),
1065 u_i_C: Some(u_i.C),
1066 U_i: Some(U_i.clone()),
1067 U_i1_C: Some(U_i1.C),
1068 F: F_circuit,
1069 x: Some(u_i1_x),
1070 nimfs_proof: Some(nimfs_proof),
1071 };
1072
1073 let (cs, _) = augmented_f_circuit.compute_cs_ccs().unwrap();
1074 assert!(cs.is_satisfied().unwrap());
1075
1076 let (r1cs_w_i1, r1cs_x_i1) = extract_w_x::<Fr>(&cs); // includes 1 and public inputs
1077 assert_eq!(r1cs_x_i1[0], augmented_f_circuit.x.unwrap());
1078 let r1cs_z = [vec![Fr::one()], r1cs_x_i1, r1cs_w_i1].concat();
1079 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
1080 // assign them directly to w_i, u_i.
1081 (u_i, w_i) = ccs.to_cccs(&mut rng, &pedersen_params, &r1cs_z).unwrap();
1082 u_i.check_relation(&pedersen_params, &ccs, &w_i).unwrap();
1083
1084 // sanity check
1085 assert_eq!(u_i.x[0], augmented_f_circuit.x.unwrap());
1086 let expected_u_i1_x = U_i1
1087 .hash(&poseidon_config, iFr + Fr::one(), z_0.clone(), z_i1.clone())
1088 .unwrap();
1089 // u_i is already u_i1 at this point, check that has the expected value at x[0]
1090 assert_eq!(u_i.x[0], expected_u_i1_x);
1091
1092 // set values for next iteration
1093 iFr += Fr::one();
1094 // assign z_{i+1} into z_i
1095 z_i = z_i1.clone();
1096 U_i = U_i1.clone();
1097 W_i = W_i1.clone();
1098
1099 // check the new LCCCS instance relation
1100 U_i.check_relation(&pedersen_params, &ccs, &W_i).unwrap();
1101 // check the new CCCS instance relation
1102 u_i.check_relation(&pedersen_params, &ccs, &w_i).unwrap();
1103
1104 println!("augmented_f_circuit step {}: {:?}", i, start.elapsed());
1105 }
1106 }
1107}