1use crate::{Curve, CurveFqSponge, CurveFrSponge, ScalarField, SRS_SIZE};
34use ark_ec::AffineRepr;
35use ark_ff::{Field, One, Zero};
36use ark_poly::{
37 univariate::DensePolynomial, EvaluationDomain, Evaluations, Polynomial,
38 Radix2EvaluationDomain as R2D,
39};
40use kimchi::{circuits::domains::EvaluationDomains, curve::KimchiCurve, plonk_sponge::FrSponge};
41use mina_poseidon::FqSponge;
42use poly_commitment::{
43 commitment::{combined_inner_product, BatchEvaluationProof, CommitmentCurve, Evaluation},
44 ipa::{OpeningProof, SRS},
45 utils::DensePolynomialOrEvaluations,
46 PolyComm, SRS as _,
47};
48use rand::{CryptoRng, RngCore};
49
50#[derive(PartialEq, Eq)]
51pub struct CoreInstance {
53 pub comm_d: Curve,
55 pub comm_q: Curve,
57 pub comm_a: Curve,
59}
60
61#[derive(PartialEq, Eq)]
62pub struct RelaxedInstance {
64 pub core: CoreInstance,
66 pub u: ScalarField,
68 pub comm_e: Curve,
70}
71
72impl CoreInstance {
73 pub fn relax(self) -> RelaxedInstance {
74 RelaxedInstance {
75 core: self,
76 u: ScalarField::one(),
77 comm_e: Curve::zero(),
78 }
79 }
80}
81
82#[derive(PartialEq, Eq)]
83pub struct CoreWitness {
86 pub d: Evaluations<ScalarField, R2D<ScalarField>>,
87 pub q: Evaluations<ScalarField, R2D<ScalarField>>,
88 pub a: Evaluations<ScalarField, R2D<ScalarField>>,
89}
90
91#[derive(PartialEq, Eq)]
92pub struct RelaxedWitness {
95 pub core: CoreWitness,
96 pub e: Evaluations<ScalarField, R2D<ScalarField>>,
97}
98
99impl CoreWitness {
100 pub fn relax(self, domain: R2D<ScalarField>) -> RelaxedWitness {
101 RelaxedWitness {
102 core: self,
103 e: Evaluations::from_vec_and_domain(vec![ScalarField::zero(); domain.size()], domain),
104 }
105 }
106}
107
108impl RelaxedInstance {
109 pub fn check_in_language(
113 &self,
114 srs: &SRS<Curve>,
115 domain: R2D<ScalarField>,
116 wit: &RelaxedWitness,
117 ) -> bool {
118 for i in 0..SRS_SIZE {
119 if self.u * wit.core.a[i] - wit.core.q[i] * wit.core.d[i] + wit.e[i]
121 != ScalarField::zero()
122 {
123 return false;
124 }
125 }
126 if self.core.comm_a
127 != srs
128 .commit_evaluations_non_hiding(domain, &wit.core.a)
129 .chunks[0]
130 {
131 return false;
132 }
133 if self.core.comm_d
134 != srs
135 .commit_evaluations_non_hiding(domain, &wit.core.d)
136 .chunks[0]
137 {
138 return false;
139 }
140 if self.core.comm_q
141 != srs
142 .commit_evaluations_non_hiding(domain, &wit.core.q)
143 .chunks[0]
144 {
145 return false;
146 }
147 if self.comm_e != srs.commit_evaluations_non_hiding(domain, &wit.e).chunks[0] {
148 return false;
149 }
150 true
151 }
152}
153
154pub fn folding_prover(
155 srs: &SRS<Curve>,
156 domain: R2D<ScalarField>,
157 inst1: &CoreInstance,
158 wit1: &CoreWitness,
159 inst2: &RelaxedInstance,
160 wit2: &RelaxedWitness,
161) -> (RelaxedInstance, RelaxedWitness, Curve) {
162 let mut fq_sponge = CurveFqSponge::new(Curve::other_curve_sponge_params());
163
164 let cross_term: Evaluations<ScalarField, R2D<ScalarField>> =
165 &(&(&wit2.core.a + &(&wit1.a * inst2.u)) - &(&wit2.core.q * &wit1.d))
166 - &(&wit1.q * &wit2.core.d);
167
168 let cross_term_comm: Curve = srs
169 .commit_evaluations_non_hiding(domain, &cross_term.clone())
170 .chunks[0];
171
172 fq_sponge.absorb_g(&[
173 inst1.comm_d,
174 inst1.comm_q,
175 inst1.comm_a,
176 inst2.core.comm_d,
177 inst2.core.comm_q,
178 inst2.core.comm_a,
179 inst2.comm_e,
180 cross_term_comm,
181 ]);
182
183 let recombination_chal = fq_sponge.challenge();
184
185 let a3 = &wit1.a + &(&wit2.core.a * recombination_chal);
186 let q3 = &wit1.q + &(&wit2.core.q * recombination_chal);
187 let d3 = &wit1.d + &(&wit2.core.d * recombination_chal);
188
189 let comm_a3 = inst1.comm_a + inst2.core.comm_a * recombination_chal;
190 let comm_q3 = inst1.comm_q + inst2.core.comm_q * recombination_chal;
191 let comm_d3 = inst1.comm_d + inst2.core.comm_d * recombination_chal;
192
193 let new_u = ScalarField::one() + recombination_chal * inst2.u;
194
195 let e3 = &(&wit2.e * (recombination_chal * recombination_chal))
196 - &(&cross_term * recombination_chal);
197 let comm_e3 = inst2.comm_e * (recombination_chal * recombination_chal)
198 - cross_term_comm * recombination_chal;
199
200 let new_inst = RelaxedInstance {
201 u: new_u,
202 comm_e: comm_e3.into(),
203 core: CoreInstance {
204 comm_d: comm_d3.into(),
205 comm_q: comm_q3.into(),
206 comm_a: comm_a3.into(),
207 },
208 };
209
210 let new_wit = RelaxedWitness {
211 e: e3,
212 core: CoreWitness {
213 d: d3,
214 q: q3,
215 a: a3,
216 },
217 };
218
219 (new_inst, new_wit, cross_term_comm)
220}
221
222pub fn folding_verifier(
223 inst1: &CoreInstance,
224 inst2: &RelaxedInstance,
225 cross_term_comm: Curve,
226) -> RelaxedInstance {
227 let mut fq_sponge = CurveFqSponge::new(Curve::other_curve_sponge_params());
228 fq_sponge.absorb_g(&[
229 inst1.comm_d,
230 inst1.comm_q,
231 inst1.comm_a,
232 inst2.core.comm_d,
233 inst2.core.comm_q,
234 inst2.core.comm_a,
235 inst2.comm_e,
236 cross_term_comm,
237 ]);
238
239 let recombination_chal = fq_sponge.challenge();
240
241 let comm_a3 = inst1.comm_a + inst2.core.comm_a * recombination_chal;
242 let comm_q3 = inst1.comm_q + inst2.core.comm_q * recombination_chal;
243 let comm_d3 = inst1.comm_d + inst2.core.comm_d * recombination_chal;
244
245 let new_u = ScalarField::one() + recombination_chal * inst2.u;
246
247 let comm_e3 = inst2.comm_e * (recombination_chal * recombination_chal)
248 - cross_term_comm * recombination_chal;
249
250 RelaxedInstance {
251 u: new_u,
252 comm_e: comm_e3.into(),
253 core: CoreInstance {
254 comm_d: comm_d3.into(),
255 comm_q: comm_q3.into(),
256 comm_a: comm_a3.into(),
257 },
258 }
259}
260
261#[derive(Debug, Clone)]
262pub struct ReadProof {
264 pub quotient_comm: Curve,
266
267 pub data_eval: ScalarField,
269 pub query_eval: ScalarField,
271 pub answer_eval: ScalarField,
273 pub error_eval: ScalarField,
275
276 pub opening_proof: OpeningProof<Curve>,
278}
279
280pub fn prove_relaxed<RNG>(
281 srs: &SRS<Curve>,
282 domain: EvaluationDomains<ScalarField>,
283 group_map: &<Curve as CommitmentCurve>::Map,
284 rng: &mut RNG,
285 inst: &RelaxedInstance,
286 wit: &RelaxedWitness,
287) -> ReadProof
288where
289 RNG: RngCore + CryptoRng,
290{
291 let mut fq_sponge = CurveFqSponge::new(Curve::other_curve_sponge_params());
292
293 let data_poly: DensePolynomial<ScalarField> = wit.core.d.interpolate_by_ref();
294 let query_poly: DensePolynomial<ScalarField> = wit.core.q.interpolate_by_ref();
295 let answer_poly: DensePolynomial<ScalarField> = wit.core.a.interpolate_by_ref();
296 let error_poly: DensePolynomial<ScalarField> = wit.e.interpolate_by_ref();
297
298 fq_sponge.absorb_g(&[
299 inst.core.comm_d,
300 inst.core.comm_q,
301 inst.core.comm_a,
302 inst.comm_e,
303 ]);
304
305 let quotient_poly: DensePolynomial<ScalarField> = {
307 let data_d2 = data_poly.evaluate_over_domain_by_ref(domain.d2);
308 let query_d2 = query_poly.evaluate_over_domain_by_ref(domain.d2);
309 let answer_d2 = answer_poly.evaluate_over_domain_by_ref(domain.d2);
310 let error_d2 = error_poly.evaluate_over_domain_by_ref(domain.d2);
311
312 let numerator_eval: Evaluations<ScalarField, R2D<ScalarField>> =
314 &(&(&answer_d2 * inst.u) - &(&data_d2 * &query_d2)) + &error_d2;
315
316 let numerator_eval_interpolated = numerator_eval.interpolate();
317
318 let fail_final_q_division = || panic!("Division by vanishing poly must not fail");
319 let (quotient, res) = numerator_eval_interpolated.divide_by_vanishing_poly(domain.d1);
322 if !res.is_zero() {
326 fail_final_q_division();
327 }
328
329 quotient
330 };
331
332 let quotient_comm = srs.commit_non_hiding("ient_poly, 1).chunks[0];
335 fq_sponge.absorb_g(&[quotient_comm]);
336
337 let evaluation_point = fq_sponge.challenge();
339
340 let mut fr_sponge = CurveFrSponge::new(Curve::sponge_params());
342 fr_sponge.absorb(&fq_sponge.clone().digest());
343
344 let data_eval = data_poly.evaluate(&evaluation_point);
345 let query_eval = query_poly.evaluate(&evaluation_point);
346 let answer_eval = answer_poly.evaluate(&evaluation_point);
347 let error_eval = error_poly.evaluate(&evaluation_point);
348 let quotient_eval = quotient_poly.evaluate(&evaluation_point);
349
350 for eval in [
351 data_eval,
352 query_eval,
353 answer_eval,
354 error_eval,
355 quotient_eval,
356 ]
357 .into_iter()
358 {
359 fr_sponge.absorb(&eval);
360 }
361
362 let (_, endo_r) = Curve::endos();
363 let polyscale = fr_sponge.challenge().to_field(endo_r);
365 let evalscale = fr_sponge.challenge().to_field(endo_r);
366
367 let opening_proof_inputs: Vec<_> = {
370 let coefficients_form =
371 DensePolynomialOrEvaluations::<_, R2D<ScalarField>>::DensePolynomial;
372 let non_hiding = |n_chunks| PolyComm {
373 chunks: vec![ScalarField::zero(); n_chunks],
374 };
375
376 vec![
377 (coefficients_form(&data_poly), non_hiding(1)),
378 (coefficients_form(&query_poly), non_hiding(1)),
379 (coefficients_form(&answer_poly), non_hiding(1)),
380 (coefficients_form(&error_poly), non_hiding(1)),
381 (coefficients_form("ient_poly), non_hiding(1)),
382 ]
383 };
384
385 let opening_proof = srs.open(
386 group_map,
387 opening_proof_inputs.as_slice(),
388 &[evaluation_point],
389 polyscale,
390 evalscale,
391 fq_sponge,
392 rng,
393 );
394
395 ReadProof {
396 quotient_comm,
397 data_eval,
398 query_eval,
399 answer_eval,
400 error_eval,
401 opening_proof,
402 }
403}
404
405pub fn verify_relaxed<RNG>(
406 srs: &SRS<Curve>,
407 domain: EvaluationDomains<ScalarField>,
408 group_map: &<Curve as CommitmentCurve>::Map,
409 rng: &mut RNG,
410 inst: &RelaxedInstance,
411 proof: &ReadProof,
412) -> bool
413where
414 RNG: RngCore + CryptoRng,
415{
416 let mut fq_sponge = CurveFqSponge::new(Curve::other_curve_sponge_params());
417 fq_sponge.absorb_g(&[
418 inst.core.comm_d,
419 inst.core.comm_q,
420 inst.core.comm_a,
421 inst.comm_e,
422 ]);
423 fq_sponge.absorb_g(&[proof.quotient_comm]);
424
425 let evaluation_point = fq_sponge.challenge();
426
427 let mut fr_sponge = CurveFrSponge::new(Curve::sponge_params());
428 fr_sponge.absorb(&fq_sponge.clone().digest());
429
430 let vanishing_poly_at_zeta = domain.d1.vanishing_polynomial().evaluate(&evaluation_point);
431 let quotient_eval = {
432 (inst.u * proof.answer_eval - proof.data_eval * proof.query_eval + proof.error_eval)
433 * vanishing_poly_at_zeta
434 .inverse()
435 .unwrap_or_else(|| panic!("Inverse fails only with negligible probability"))
436 };
437
438 for eval in [
439 proof.data_eval,
440 proof.query_eval,
441 proof.answer_eval,
442 proof.error_eval,
443 quotient_eval,
444 ]
445 .into_iter()
446 {
447 fr_sponge.absorb(&eval);
448 }
449
450 let (_, endo_r) = Curve::endos();
451 let polyscale = fr_sponge.challenge().to_field(endo_r);
453 let evalscale = fr_sponge.challenge().to_field(endo_r);
454
455 let coms_and_evaluations = vec![
456 Evaluation {
457 commitment: PolyComm {
458 chunks: vec![inst.core.comm_d],
459 },
460 evaluations: vec![vec![proof.data_eval]],
461 },
462 Evaluation {
463 commitment: PolyComm {
464 chunks: vec![inst.core.comm_q],
465 },
466 evaluations: vec![vec![proof.query_eval]],
467 },
468 Evaluation {
469 commitment: PolyComm {
470 chunks: vec![inst.core.comm_a],
471 },
472 evaluations: vec![vec![proof.answer_eval]],
473 },
474 Evaluation {
475 commitment: PolyComm {
476 chunks: vec![inst.comm_e],
477 },
478 evaluations: vec![vec![proof.error_eval]],
479 },
480 Evaluation {
481 commitment: PolyComm {
482 chunks: vec![proof.quotient_comm],
483 },
484 evaluations: vec![vec![quotient_eval]],
485 },
486 ];
487 let combined_inner_product = {
488 let evaluations: Vec<_> = coms_and_evaluations
489 .iter()
490 .map(|Evaluation { evaluations, .. }| evaluations.clone())
491 .collect();
492
493 combined_inner_product(&polyscale, &evalscale, evaluations.as_slice())
494 };
495
496 srs.verify(
497 group_map,
498 &mut [BatchEvaluationProof {
499 sponge: fq_sponge,
500 evaluation_points: vec![evaluation_point],
501 polyscale,
502 evalscale,
503 evaluations: coms_and_evaluations,
504 opening: &proof.opening_proof,
505 combined_inner_product,
506 }],
507 rng,
508 )
509}
510
511pub mod testing {
512 use super::*;
513 use crate::{Curve, ScalarField};
514 use ark_ff::UniformRand;
515 use ark_poly::Evaluations;
516 use mina_curves::pasta::{Fp, Vesta};
517 use poly_commitment::ipa::SRS;
518 use rand::Rng;
519
520 pub fn generate_random_inst_wit_core<RNG>(
522 srs: &SRS<Vesta>,
523 domain: R2D<ScalarField>,
524 rng: &mut RNG,
525 ) -> (CoreInstance, CoreWitness)
526 where
527 RNG: RngCore + CryptoRng,
528 {
529 let data: Vec<ScalarField> = {
530 let mut data = vec![];
531 (0..domain.size).for_each(|_| data.push(Fp::rand(rng)));
532 data
533 };
534
535 let data_comm: Curve = srs
536 .commit_evaluations_non_hiding(
537 domain,
538 &Evaluations::from_vec_and_domain(data.clone(), domain),
539 )
540 .chunks[0];
541
542 let query: Vec<ScalarField> = {
543 let mut query = vec![];
544 (0..domain.size)
545 .for_each(|_| query.push(Fp::from(rand::thread_rng().gen::<f64>() < 0.1)));
546 query
547 };
548
549 let answer: Vec<ScalarField> = data
550 .clone()
551 .iter()
552 .zip(query.iter())
553 .map(|(d, q)| *d * q)
554 .collect();
555
556 let comm_q = srs
557 .commit_evaluations_non_hiding(
558 domain,
559 &Evaluations::from_vec_and_domain(query.clone(), domain),
560 )
561 .chunks[0];
562
563 let comm_a = srs
564 .commit_evaluations_non_hiding(
565 domain,
566 &Evaluations::from_vec_and_domain(answer.clone(), domain),
567 )
568 .chunks[0];
569
570 let core_instance = CoreInstance {
571 comm_d: data_comm,
572 comm_q,
573 comm_a,
574 };
575
576 let core_witness = CoreWitness {
577 d: Evaluations::from_vec_and_domain(data, domain),
578 q: Evaluations::from_vec_and_domain(query, domain),
579 a: Evaluations::from_vec_and_domain(answer, domain),
580 };
581
582 (core_instance, core_witness)
583 }
584
585 pub fn generate_random_inst_wit_relaxed<RNG>(
589 srs: &SRS<Vesta>,
590 domain: R2D<ScalarField>,
591 rng: &mut RNG,
592 ) -> (RelaxedInstance, RelaxedWitness)
593 where
594 RNG: RngCore + CryptoRng,
595 {
596 let (inst, wit) = generate_random_inst_wit_core(srs, domain, rng);
597 let u = Fp::rand(rng);
598 let e = &(&wit.d * &wit.q) - &(&wit.a * u);
599 let comm_e = srs.commit_evaluations_non_hiding(domain, &e).chunks[0];
600
601 let relaxed_instance = RelaxedInstance {
602 core: inst,
603 u,
604 comm_e,
605 };
606
607 let relaxed_witness = RelaxedWitness { core: wit, e };
608
609 assert!(relaxed_instance.check_in_language(srs, domain, &relaxed_witness));
610
611 (relaxed_instance, relaxed_witness)
612 }
613}
614
615#[cfg(test)]
616mod tests {
617 use super::{testing::generate_random_inst_wit_core, *};
618 use crate::{Curve, ScalarField};
619 use ark_ec::AffineRepr;
620 use ark_ff::One;
621 use kimchi::{circuits::domains::EvaluationDomains, groupmap::GroupMap};
622 use mina_curves::pasta::Vesta;
623 use poly_commitment::commitment::CommitmentCurve;
624
625 #[test]
626 fn test_folding_read_proof_completeness_soundness() {
627 let mut rng = o1_utils::tests::make_test_rng(None);
628
629 let srs = poly_commitment::precomputed_srs::get_srs_test();
630 let domain: EvaluationDomains<ScalarField> =
631 EvaluationDomains::<ScalarField>::create(srs.size()).unwrap();
632
633 let group_map = <Vesta as CommitmentCurve>::Map::setup();
634
635 let (core_instance_1, core_witness_1) =
636 generate_random_inst_wit_core(&srs, domain.d1, &mut rng);
637 let (core_instance_2, core_witness_2) =
638 generate_random_inst_wit_core(&srs, domain.d1, &mut rng);
639 let relaxed_instance_2 = core_instance_2.relax();
640 let relaxed_witness_2 = core_witness_2.relax(domain.d1);
641
642 assert!(relaxed_instance_2.check_in_language(&srs, domain.d1, &relaxed_witness_2));
643
644 let (relaxed_instance_3, relaxed_witness_3, cross_term_1) = folding_prover(
645 &srs,
646 domain.d1,
647 &core_instance_1,
648 &core_witness_1,
649 &relaxed_instance_2,
650 &relaxed_witness_2,
651 );
652
653 assert!(relaxed_instance_3.check_in_language(&srs, domain.d1, &relaxed_witness_3));
654
655 assert!(
656 folding_verifier(&core_instance_1, &relaxed_instance_2, cross_term_1)
657 == relaxed_instance_3
658 );
659
660 let (core_instance_4, core_witness_4) =
661 generate_random_inst_wit_core(&srs, domain.d1, &mut rng);
662 let (relaxed_instance_5, relaxed_witness_5, cross_term_2) = folding_prover(
663 &srs,
664 domain.d1,
665 &core_instance_4,
666 &core_witness_4,
667 &relaxed_instance_3,
668 &relaxed_witness_3,
669 );
670
671 assert!(relaxed_instance_5.check_in_language(&srs, domain.d1, &relaxed_witness_5));
672
673 assert!(
674 folding_verifier(&core_instance_4, &relaxed_instance_3, cross_term_2)
675 == relaxed_instance_5
676 );
677
678 let proof = prove_relaxed(
679 &srs,
680 domain,
681 &group_map,
682 &mut rng,
683 &relaxed_instance_5,
684 &relaxed_witness_5,
685 );
686 let res = verify_relaxed(
687 &srs,
688 domain,
689 &group_map,
690 &mut rng,
691 &relaxed_instance_5,
692 &proof,
693 );
694
695 assert!(res, "Completeness: Proof must verify");
696
697 let proof_malformed_1 = ReadProof {
698 quotient_comm: Curve::zero(),
699 ..proof.clone()
700 };
701
702 let res_1 = verify_relaxed(
703 &srs,
704 domain,
705 &group_map,
706 &mut rng,
707 &relaxed_instance_5,
708 &proof_malformed_1,
709 );
710
711 assert!(!res_1, "Soundness: Malformed proof #1 must NOT verify");
712
713 let proof_malformed_2 = ReadProof {
714 query_eval: ScalarField::one(),
715 ..proof.clone()
716 };
717
718 let res_2 = verify_relaxed(
719 &srs,
720 domain,
721 &group_map,
722 &mut rng,
723 &relaxed_instance_5,
724 &proof_malformed_2,
725 );
726
727 assert!(!res_2, "Soundness: Malformed proof #2 must NOT verify");
728 }
729}