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::sponge::Absorb;
3use ark_ec::{CurveGroup, Group};
4use ark_ff::PrimeField;
5use ark_r1cs_std::{
6 alloc::{AllocVar, AllocationMode},
7 eq::EqGadget,
8 fields::{fp::FpVar, FieldVar},
9};
10use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError};
11use core::{borrow::Borrow, marker::PhantomData};
12
13use super::{cccs::CCCS, lcccs::LCCCS, nimfs::Proof};
14use crate::folding::circuits::{
15 nonnative::affine::NonNativeAffineVar,
16 sum_check::{IOPProofVar, SumCheckVerifierGadget, VPAuxInfoVar},
17 utils::EqEvalGadget,
18 CF1,
19};
20use crate::utils::virtual_polynomial::VPAuxInfo;
21use crate::{ccs::CCS, transcript::TranscriptVar};
22
23/// Committed CCS instance
24#[derive(Debug, Clone)]
25pub struct CCCSVar<C: CurveGroup>
26where
27 <C as CurveGroup>::BaseField: PrimeField,
28{
29 // Commitment to witness
30 pub C: NonNativeAffineVar<C>,
31 // Public input/output
32 pub x: Vec<FpVar<CF1<C>>>,
33}
34impl<C> AllocVar<CCCS<C>, CF1<C>> for CCCSVar<C>
35where
36 C: CurveGroup,
37 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
38{
39 fn new_variable<T: Borrow<CCCS<C>>>(
40 cs: impl Into<Namespace<CF1<C>>>,
41 f: impl FnOnce() -> Result<T, SynthesisError>,
42 mode: AllocationMode,
43 ) -> Result<Self, SynthesisError> {
44 f().and_then(|val| {
45 let cs = cs.into();
46
47 let C = NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?;
48 let x: Vec<FpVar<C::ScalarField>> =
49 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
50
51 Ok(Self { C, x })
52 })
53 }
54}
55
56/// Linearized Committed CCS instance
57#[derive(Debug, Clone)]
58pub struct LCCCSVar<C: CurveGroup>
59where
60 <C as CurveGroup>::BaseField: PrimeField,
61{
62 // Commitment to witness
63 pub C: NonNativeAffineVar<C>,
64 // Relaxation factor of z for folded LCCCS
65 pub u: FpVar<CF1<C>>,
66 // Public input/output
67 pub x: Vec<FpVar<CF1<C>>>,
68 // Random evaluation point for the v_i
69 pub r_x: Vec<FpVar<CF1<C>>>,
70 // Vector of v_i
71 pub v: Vec<FpVar<CF1<C>>>,
72}
73impl<C> AllocVar<LCCCS<C>, CF1<C>> for LCCCSVar<C>
74where
75 C: CurveGroup,
76 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
77{
78 fn new_variable<T: Borrow<LCCCS<C>>>(
79 cs: impl Into<Namespace<CF1<C>>>,
80 f: impl FnOnce() -> Result<T, SynthesisError>,
81 mode: AllocationMode,
82 ) -> Result<Self, SynthesisError> {
83 f().and_then(|val| {
84 let cs = cs.into();
85
86 let C = NonNativeAffineVar::<C>::new_variable(cs.clone(), || Ok(val.borrow().C), mode)?;
87 let u = FpVar::<C::ScalarField>::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?;
88 let x: Vec<FpVar<C::ScalarField>> =
89 Vec::new_variable(cs.clone(), || Ok(val.borrow().x.clone()), mode)?;
90 let r_x: Vec<FpVar<C::ScalarField>> =
91 Vec::new_variable(cs.clone(), || Ok(val.borrow().r_x.clone()), mode)?;
92 let v: Vec<FpVar<C::ScalarField>> =
93 Vec::new_variable(cs.clone(), || Ok(val.borrow().v.clone()), mode)?;
94
95 Ok(Self { C, u, x, r_x, v })
96 })
97 }
98}
99
100/// ProofVar defines a multifolding proof
101#[derive(Debug)]
102pub struct ProofVar<C: CurveGroup> {
103 pub sc_proof: IOPProofVar<C>,
104 #[allow(clippy::type_complexity)]
105 pub sigmas_thetas: (Vec<Vec<FpVar<CF1<C>>>>, Vec<Vec<FpVar<CF1<C>>>>),
106}
107impl<C> AllocVar<Proof<C>, CF1<C>> for ProofVar<C>
108where
109 C: CurveGroup,
110 <C as ark_ec::CurveGroup>::BaseField: PrimeField,
111 <C as Group>::ScalarField: Absorb,
112{
113 fn new_variable<T: Borrow<Proof<C>>>(
114 cs: impl Into<Namespace<CF1<C>>>,
115 f: impl FnOnce() -> Result<T, SynthesisError>,
116 mode: AllocationMode,
117 ) -> Result<Self, SynthesisError> {
118 f().and_then(|val| {
119 let cs = cs.into();
120
121 let sc_proof = IOPProofVar::<C>::new_variable(
122 cs.clone(),
123 || Ok(val.borrow().sc_proof.clone()),
124 mode,
125 )?;
126 let sigmas: Vec<Vec<FpVar<CF1<C>>>> = val
127 .borrow()
128 .sigmas_thetas
129 .0
130 .iter()
131 .map(|sigmas_i| Vec::new_variable(cs.clone(), || Ok(sigmas_i.clone()), mode))
132 .collect::<Result<Vec<Vec<FpVar<CF1<C>>>>, SynthesisError>>()?;
133 let thetas: Vec<Vec<FpVar<CF1<C>>>> = val
134 .borrow()
135 .sigmas_thetas
136 .1
137 .iter()
138 .map(|thetas_i| Vec::new_variable(cs.clone(), || Ok(thetas_i.clone()), mode))
139 .collect::<Result<Vec<Vec<FpVar<CF1<C>>>>, SynthesisError>>()?;
140
141 Ok(Self {
142 sc_proof,
143 sigmas_thetas: (sigmas.clone(), thetas.clone()),
144 })
145 })
146 }
147}
148
149pub struct NIMFSGadget<C: CurveGroup> {
150 _c: PhantomData<C>,
151}
152impl<C: CurveGroup> NIMFSGadget<C>
153where
154 <C as CurveGroup>::BaseField: PrimeField,
155{
156 pub fn verify(
157 cs: ConstraintSystemRef<CF1<C>>,
158 // only used the CCS params, not the matrices
159 ccs: &CCS<C::ScalarField>,
160 mut transcript: impl TranscriptVar<C::ScalarField>,
161
162 running_instances: &[LCCCSVar<C>],
163 new_instances: &[CCCSVar<C>],
164 proof: ProofVar<C>,
165 ) -> Result<LCCCSVar<C>, SynthesisError> {
166 // get the challenges
167 let gamma_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"gamma");
168 let gamma_scalar: FpVar<CF1<C>> =
169 FpVar::<CF1<C>>::new_constant(cs.clone(), gamma_scalar_raw)?;
170 transcript.absorb(gamma_scalar)?;
171 let gamma: FpVar<CF1<C>> = transcript.get_challenge()?;
172
173 let beta_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"beta");
174 let beta_scalar: FpVar<CF1<C>> =
175 FpVar::<CF1<C>>::new_constant(cs.clone(), beta_scalar_raw)?;
176 transcript.absorb(beta_scalar)?;
177 let beta: Vec<FpVar<CF1<C>>> = transcript.get_challenges(ccs.s)?;
178
179 let vp_aux_info_raw = VPAuxInfo::<C::ScalarField> {
180 max_degree: ccs.d + 1,
181 num_variables: ccs.s,
182 phantom: PhantomData::<C::ScalarField>,
183 };
184 let vp_aux_info = VPAuxInfoVar::<CF1<C>>::new_witness(cs.clone(), || Ok(vp_aux_info_raw))?;
185
186 // sumcheck
187 // first, compute the expected sumcheck sum: \sum gamma^j v_j
188 let mut sum_v_j_gamma = FpVar::<CF1<C>>::zero();
189 let mut gamma_j = FpVar::<C::ScalarField>::one();
190 for running_instance in running_instances.iter() {
191 for j in 0..running_instance.v.len() {
192 gamma_j *= gamma.clone();
193 sum_v_j_gamma += running_instance.v[j].clone() * gamma_j.clone();
194 }
195 }
196
197 // verify the interactive part of the sumcheck
198 let (e_vars, r_vars) =
199 SumCheckVerifierGadget::<C>::verify(&proof.sc_proof, &vp_aux_info, &mut transcript)?;
200
201 // extract the randomness from the sumcheck
202 let r_x_prime = r_vars.clone();
203
204 // verify the claim c
205 let computed_c = compute_c_gadget(
206 cs.clone(),
207 ccs,
208 proof.sigmas_thetas.0.clone(), // sigmas
209 proof.sigmas_thetas.1.clone(), // thetas
210 gamma,
211 beta,
212 running_instances
213 .iter()
214 .map(|lcccs| lcccs.r_x.clone())
215 .collect(),
216 r_x_prime.clone(),
217 )?;
218 computed_c.enforce_equal(&e_vars[e_vars.len() - 1])?;
219
220 // get the folding challenge
221 let rho_scalar_raw = C::ScalarField::from_le_bytes_mod_order(b"rho");
222 let rho_scalar: FpVar<CF1<C>> = FpVar::<CF1<C>>::new_constant(cs.clone(), rho_scalar_raw)?;
223 transcript.absorb(rho_scalar)?;
224 let rho: FpVar<CF1<C>> = transcript.get_challenge()?;
225
226 // return the folded instance
227 Self::fold(
228 running_instances,
229 new_instances,
230 proof.sigmas_thetas,
231 r_x_prime,
232 rho,
233 )
234 }
235
236 #[allow(clippy::type_complexity)]
237 fn fold(
238 lcccs: &[LCCCSVar<C>],
239 cccs: &[CCCSVar<C>],
240 sigmas_thetas: (Vec<Vec<FpVar<CF1<C>>>>, Vec<Vec<FpVar<CF1<C>>>>),
241 r_x_prime: Vec<FpVar<CF1<C>>>,
242 rho: FpVar<CF1<C>>,
243 ) -> Result<LCCCSVar<C>, SynthesisError> {
244 let (sigmas, thetas) = (sigmas_thetas.0.clone(), sigmas_thetas.1.clone());
245 let mut u_folded: FpVar<CF1<C>> = FpVar::zero();
246 let mut x_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); lcccs[0].x.len()];
247 let mut v_folded: Vec<FpVar<CF1<C>>> = vec![FpVar::zero(); sigmas[0].len()];
248
249 let mut rho_i = FpVar::one();
250 for i in 0..(lcccs.len() + cccs.len()) {
251 let u: FpVar<CF1<C>>;
252 let x: Vec<FpVar<CF1<C>>>;
253 let v: Vec<FpVar<CF1<C>>>;
254 if i < lcccs.len() {
255 u = lcccs[i].u.clone();
256 x = lcccs[i].x.clone();
257 v = sigmas[i].clone();
258 } else {
259 u = FpVar::one();
260 x = cccs[i - lcccs.len()].x.clone();
261 v = thetas[i - lcccs.len()].clone();
262 }
263
264 u_folded += rho_i.clone() * u;
265 x_folded = x_folded
266 .iter()
267 .zip(
268 x.iter()
269 .map(|x_i| x_i * rho_i.clone())
270 .collect::<Vec<FpVar<CF1<C>>>>(),
271 )
272 .map(|(a_i, b_i)| a_i + b_i)
273 .collect();
274
275 v_folded = v_folded
276 .iter()
277 .zip(
278 v.iter()
279 .map(|x_i| x_i * rho_i.clone())
280 .collect::<Vec<FpVar<CF1<C>>>>(),
281 )
282 .map(|(a_i, b_i)| a_i + b_i)
283 .collect();
284
285 rho_i *= rho.clone();
286 }
287
288 Ok(LCCCSVar::<C> {
289 C: lcccs[0].C.clone(), // WIP this will come from the cyclefold circuit
290 u: u_folded,
291 x: x_folded,
292 r_x: r_x_prime,
293 v: v_folded,
294 })
295 }
296}
297
298/// computes c from the step 5 in section 5 of HyperNova, adapted to multiple LCCCS & CCCS
299/// instances:
300/// $$
301/// c = \sum_{i \in [\mu]} \left(\sum_{j \in [t]} \gamma^{i \cdot t + j} \cdot e_i \cdot \sigma_{i,j} \right)
302/// + \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}
303/// \theta_{k,j} \right)
304/// $$
305#[allow(clippy::too_many_arguments)]
306fn compute_c_gadget<F: PrimeField>(
307 cs: ConstraintSystemRef<F>,
308 ccs: &CCS<F>,
309 vec_sigmas: Vec<Vec<FpVar<F>>>,
310 vec_thetas: Vec<Vec<FpVar<F>>>,
311 gamma: FpVar<F>,
312 beta: Vec<FpVar<F>>,
313 vec_r_x: Vec<Vec<FpVar<F>>>,
314 vec_r_x_prime: Vec<FpVar<F>>,
315) -> Result<FpVar<F>, SynthesisError> {
316 let mut e_lcccs = Vec::new();
317 for r_x in vec_r_x.iter() {
318 e_lcccs.push(EqEvalGadget::eq_eval(r_x, &vec_r_x_prime)?);
319 }
320
321 let mut c = FpVar::<F>::zero();
322 let mut current_gamma = FpVar::<F>::one();
323 for i in 0..vec_sigmas.len() {
324 for j in 0..ccs.t {
325 c += current_gamma.clone() * e_lcccs[i].clone() * vec_sigmas[i][j].clone();
326 current_gamma *= gamma.clone();
327 }
328 }
329
330 let ccs_c = Vec::<FpVar<F>>::new_constant(cs.clone(), ccs.c.clone())?;
331 let e_k = EqEvalGadget::eq_eval(&beta, &vec_r_x_prime)?;
332 #[allow(clippy::needless_range_loop)]
333 for k in 0..vec_thetas.len() {
334 let mut sum = FpVar::<F>::zero();
335 for i in 0..ccs.q {
336 let mut prod = FpVar::<F>::one();
337 for j in ccs.S[i].clone() {
338 prod *= vec_thetas[k][j].clone();
339 }
340 sum += ccs_c[i].clone() * prod;
341 }
342 c += current_gamma.clone() * e_k.clone() * sum;
343 current_gamma *= gamma.clone();
344 }
345 Ok(c)
346}
347
348#[cfg(test)]
349mod tests {
350 use ark_pallas::{Fr, Projective};
351 use ark_r1cs_std::{alloc::AllocVar, fields::fp::FpVar, R1CSVar};
352 use ark_relations::r1cs::ConstraintSystem;
353 use ark_std::{test_rng, UniformRand};
354
355 use super::*;
356 use crate::{
357 ccs::{
358 tests::{get_test_ccs, get_test_z},
359 CCS,
360 },
361 commitment::{pedersen::Pedersen, CommitmentScheme},
362 folding::hypernova::{
363 nimfs::NIMFS,
364 utils::{compute_c, compute_sigmas_thetas},
365 },
366 transcript::{
367 poseidon::{poseidon_canonical_config, PoseidonTranscript, PoseidonTranscriptVar},
368 Transcript,
369 },
370 };
371
372 #[test]
373 pub fn test_compute_c_gadget() {
374 // number of LCCCS & CCCS instances to fold in a single step
375 let mu = 32;
376 let nu = 42;
377
378 let mut z_lcccs = Vec::new();
379 for i in 0..mu {
380 let z = get_test_z(i + 3);
381 z_lcccs.push(z);
382 }
383 let mut z_cccs = Vec::new();
384 for i in 0..nu {
385 let z = get_test_z(i + 3);
386 z_cccs.push(z);
387 }
388
389 let ccs: CCS<Fr> = get_test_ccs();
390
391 let mut rng = test_rng();
392 let gamma: Fr = Fr::rand(&mut rng);
393 let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
394 let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
395
396 let (pedersen_params, _) =
397 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
398
399 // Create the LCCCS instances out of z_lcccs
400 let mut lcccs_instances = Vec::new();
401 for z_i in z_lcccs.iter() {
402 let (inst, _) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap();
403 lcccs_instances.push(inst);
404 }
405 // Create the CCCS instance out of z_cccs
406 let mut cccs_instances = Vec::new();
407 for z_i in z_cccs.iter() {
408 let (inst, _) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap();
409 cccs_instances.push(inst);
410 }
411
412 let sigmas_thetas = compute_sigmas_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime).unwrap();
413
414 let expected_c = compute_c(
415 &ccs,
416 &sigmas_thetas,
417 gamma,
418 &beta,
419 &lcccs_instances
420 .iter()
421 .map(|lcccs| lcccs.r_x.clone())
422 .collect(),
423 &r_x_prime,
424 )
425 .unwrap();
426
427 let cs = ConstraintSystem::<Fr>::new_ref();
428 let mut vec_sigmas = Vec::new();
429 let mut vec_thetas = Vec::new();
430 for sigmas in sigmas_thetas.0 {
431 vec_sigmas
432 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap());
433 }
434 for thetas in sigmas_thetas.1 {
435 vec_thetas
436 .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap());
437 }
438 let vec_r_x: Vec<Vec<FpVar<Fr>>> = lcccs_instances
439 .iter()
440 .map(|lcccs| {
441 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap()
442 })
443 .collect();
444 let vec_r_x_prime =
445 Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap();
446 let gamma_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(gamma)).unwrap();
447 let beta_var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap();
448
449 let computed_c = compute_c_gadget(
450 cs.clone(),
451 &ccs,
452 vec_sigmas,
453 vec_thetas,
454 gamma_var,
455 beta_var,
456 vec_r_x,
457 vec_r_x_prime,
458 )
459 .unwrap();
460
461 assert_eq!(expected_c, computed_c.value().unwrap());
462 }
463
464 /// Test that generates mu>1 and nu>1 instances, and folds them in a single multifolding step,
465 /// to verify the folding in the NIMFSGadget circuit
466 #[test]
467 pub fn test_nimfs_gadget_verify() {
468 let mut rng = test_rng();
469
470 // Create a basic CCS circuit
471 let ccs = get_test_ccs::<Fr>();
472 let (pedersen_params, _) =
473 Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
474
475 let mu = 32;
476 let nu = 42;
477
478 // Generate a mu LCCCS & nu CCCS satisfying witness
479 let mut z_lcccs = Vec::new();
480 for i in 0..mu {
481 let z = get_test_z(i + 3);
482 z_lcccs.push(z);
483 }
484 let mut z_cccs = Vec::new();
485 for i in 0..nu {
486 let z = get_test_z(nu + i + 3);
487 z_cccs.push(z);
488 }
489
490 // Create the LCCCS instances out of z_lcccs
491 let mut lcccs_instances = Vec::new();
492 let mut w_lcccs = Vec::new();
493 for z_i in z_lcccs.iter() {
494 let (running_instance, w) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap();
495 lcccs_instances.push(running_instance);
496 w_lcccs.push(w);
497 }
498 // Create the CCCS instance out of z_cccs
499 let mut cccs_instances = Vec::new();
500 let mut w_cccs = Vec::new();
501 for z_i in z_cccs.iter() {
502 let (new_instance, w) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap();
503 cccs_instances.push(new_instance);
504 w_cccs.push(w);
505 }
506
507 // Prover's transcript
508 let poseidon_config = poseidon_canonical_config::<Fr>();
509 let mut transcript_p: PoseidonTranscript<Projective> =
510 PoseidonTranscript::<Projective>::new(&poseidon_config);
511
512 // Run the prover side of the multifolding
513 let (proof, folded_lcccs, folded_witness) =
514 NIMFS::<Projective, PoseidonTranscript<Projective>>::prove(
515 &mut transcript_p,
516 &ccs,
517 &lcccs_instances,
518 &cccs_instances,
519 &w_lcccs,
520 &w_cccs,
521 )
522 .unwrap();
523
524 // Verifier's transcript
525 let mut transcript_v: PoseidonTranscript<Projective> =
526 PoseidonTranscript::<Projective>::new(&poseidon_config);
527
528 // Run the verifier side of the multifolding
529 let folded_lcccs_v = NIMFS::<Projective, PoseidonTranscript<Projective>>::verify(
530 &mut transcript_v,
531 &ccs,
532 &lcccs_instances,
533 &cccs_instances,
534 proof.clone(),
535 )
536 .unwrap();
537 assert_eq!(folded_lcccs, folded_lcccs_v);
538
539 // Check that the folded LCCCS instance is a valid instance with respect to the folded witness
540 folded_lcccs
541 .check_relation(&pedersen_params, &ccs, &folded_witness)
542 .unwrap();
543
544 // allocate circuit inputs
545 let cs = ConstraintSystem::<Fr>::new_ref();
546 let lcccs_instancesVar =
547 Vec::<LCCCSVar<Projective>>::new_witness(cs.clone(), || Ok(lcccs_instances.clone()))
548 .unwrap();
549 let cccs_instancesVar =
550 Vec::<CCCSVar<Projective>>::new_witness(cs.clone(), || Ok(cccs_instances.clone()))
551 .unwrap();
552 let proofVar =
553 ProofVar::<Projective>::new_witness(cs.clone(), || Ok(proof.clone())).unwrap();
554 let transcriptVar = PoseidonTranscriptVar::<Fr>::new(cs.clone(), &poseidon_config);
555
556 let folded_lcccsVar = NIMFSGadget::<Projective>::verify(
557 cs.clone(),
558 &ccs,
559 transcriptVar,
560 &lcccs_instancesVar,
561 &cccs_instancesVar,
562 proofVar,
563 )
564 .unwrap();
565 assert!(cs.is_satisfied().unwrap());
566 assert_eq!(folded_lcccsVar.u.value().unwrap(), folded_lcccs.u);
567 }
568}