kimchi/
prover.rs

1//! This module implements prover's zk-proof primitive.
2
3use crate::{
4    circuits::{
5        argument::{Argument, ArgumentType},
6        berkeley_columns::{BerkeleyChallenges, Environment, LookupEnvironment},
7        constraints::zk_rows_strict_lower_bound,
8        expr::{self, l0_1, Constants},
9        gate::GateType,
10        lookup::{self, runtime_tables::RuntimeTable, tables::combine_table_entry},
11        polynomials::{
12            complete_add::CompleteAdd,
13            endomul_scalar::EndomulScalar,
14            endosclmul::EndosclMul,
15            foreign_field_add::circuitgates::ForeignFieldAdd,
16            foreign_field_mul::{self, circuitgates::ForeignFieldMul},
17            generic, permutation,
18            poseidon::Poseidon,
19            range_check::circuitgates::{RangeCheck0, RangeCheck1},
20            rot::Rot64,
21            varbasemul::VarbaseMul,
22            xor::Xor16,
23        },
24        wires::{COLUMNS, PERMUTS},
25    },
26    curve::KimchiCurve,
27    error::ProverError,
28    lagrange_basis_evaluations::LagrangeBasisEvaluations,
29    plonk_sponge::FrSponge,
30    proof::{
31        LookupCommitments, PointEvaluations, ProofEvaluations, ProverCommitments, ProverProof,
32        RecursionChallenge,
33    },
34    prover_index::ProverIndex,
35    verifier_index::VerifierIndex,
36};
37use ark_ff::{FftField, Field, One, PrimeField, UniformRand, Zero};
38use ark_poly::{
39    univariate::DensePolynomial, DenseUVPolynomial, EvaluationDomain, Evaluations, Polynomial,
40    Radix2EvaluationDomain as D,
41};
42use core::array;
43use itertools::Itertools;
44use mina_poseidon::{sponge::ScalarChallenge, FqSponge};
45use o1_utils::ExtendedDensePolynomial as _;
46use poly_commitment::{
47    commitment::{
48        absorb_commitment, b_poly_coefficients, BlindedCommitment, CommitmentCurve, PolyComm,
49    },
50    utils::DensePolynomialOrEvaluations,
51    OpenProof, SRS as _,
52};
53use rand_core::{CryptoRng, RngCore};
54use rayon::prelude::*;
55use std::collections::HashMap;
56
57/// The result of a proof creation or verification.
58type Result<T> = core::result::Result<T, ProverError>;
59
60/// Helper to quickly test if a witness satisfies a constraint
61macro_rules! check_constraint {
62    ($index:expr, $evaluation:expr) => {{
63        check_constraint!($index, stringify!($evaluation), $evaluation);
64    }};
65    ($index:expr, $label:expr, $evaluation:expr) => {{
66        if cfg!(debug_assertions) {
67            let (_, res) = $evaluation
68                .interpolate_by_ref()
69                .divide_by_vanishing_poly($index.cs.domain.d1);
70            if !res.is_zero() {
71                panic!("couldn't divide by vanishing polynomial: {}", $label);
72            }
73        }
74    }};
75}
76
77/// Contains variables needed for lookup in the prover algorithm.
78#[derive(Default)]
79struct LookupContext<G, F>
80where
81    G: CommitmentCurve,
82    F: FftField,
83{
84    /// The joint combiner used to join the columns of lookup tables
85    joint_combiner: Option<F>,
86
87    /// The power of the joint_combiner that can be used to add a table_id column
88    /// to the concatenated lookup tables.
89    table_id_combiner: Option<F>,
90
91    /// The combined lookup entry that can be used as dummy value
92    dummy_lookup_value: Option<F>,
93
94    /// The combined lookup table
95    joint_lookup_table: Option<DensePolynomial<F>>,
96    joint_lookup_table_d8: Option<Evaluations<F, D<F>>>,
97
98    /// The sorted polynomials `s` in different forms
99    sorted: Option<Vec<Evaluations<F, D<F>>>>,
100    sorted_coeffs: Option<Vec<DensePolynomial<F>>>,
101    sorted_comms: Option<Vec<BlindedCommitment<G>>>,
102    sorted8: Option<Vec<Evaluations<F, D<F>>>>,
103
104    /// The aggregation polynomial in different forms
105    aggreg_coeffs: Option<DensePolynomial<F>>,
106    aggreg_comm: Option<BlindedCommitment<G>>,
107    aggreg8: Option<Evaluations<F, D<F>>>,
108
109    // lookup-related evaluations
110    /// evaluation of lookup aggregation polynomial
111    pub lookup_aggregation_eval: Option<PointEvaluations<Vec<F>>>,
112    /// evaluation of lookup table polynomial
113    pub lookup_table_eval: Option<PointEvaluations<Vec<F>>>,
114    /// evaluation of lookup sorted polynomials
115    pub lookup_sorted_eval: [Option<PointEvaluations<Vec<F>>>; 5],
116    /// evaluation of runtime lookup table polynomial
117    pub runtime_lookup_table_eval: Option<PointEvaluations<Vec<F>>>,
118
119    /// Runtime table
120    runtime_table: Option<DensePolynomial<F>>,
121    runtime_table_d8: Option<Evaluations<F, D<F>>>,
122    runtime_table_comm: Option<BlindedCommitment<G>>,
123    runtime_second_col_d8: Option<Evaluations<F, D<F>>>,
124}
125
126impl<G: KimchiCurve, OpeningProof: OpenProof<G>> ProverProof<G, OpeningProof>
127where
128    G::BaseField: PrimeField,
129{
130    /// This function constructs prover's zk-proof from the witness & the `ProverIndex` against SRS instance
131    ///
132    /// # Errors
133    ///
134    /// Will give error if `create_recursive` process fails.
135    pub fn create<
136        EFqSponge: Clone + FqSponge<G::BaseField, G, G::ScalarField>,
137        EFrSponge: FrSponge<G::ScalarField>,
138        RNG: RngCore + CryptoRng,
139    >(
140        groupmap: &G::Map,
141        witness: [Vec<G::ScalarField>; COLUMNS],
142        runtime_tables: &[RuntimeTable<G::ScalarField>],
143        index: &ProverIndex<G, OpeningProof>,
144        rng: &mut RNG,
145    ) -> Result<Self>
146    where
147        VerifierIndex<G, OpeningProof>: Clone,
148    {
149        Self::create_recursive::<EFqSponge, EFrSponge, RNG>(
150            groupmap,
151            witness,
152            runtime_tables,
153            index,
154            Vec::new(),
155            None,
156            rng,
157        )
158    }
159
160    /// This function constructs prover's recursive zk-proof from the witness &
161    /// the `ProverIndex` against SRS instance
162    ///
163    /// # Errors
164    ///
165    /// Will give error if inputs(like `lookup_context.joint_lookup_table_d8`)
166    /// are None.
167    ///
168    /// # Panics
169    ///
170    /// Will panic if `lookup_context.joint_lookup_table_d8` is None.
171    pub fn create_recursive<
172        EFqSponge: Clone + FqSponge<G::BaseField, G, G::ScalarField>,
173        EFrSponge: FrSponge<G::ScalarField>,
174        RNG: RngCore + CryptoRng,
175    >(
176        group_map: &G::Map,
177        mut witness: [Vec<G::ScalarField>; COLUMNS],
178        runtime_tables: &[RuntimeTable<G::ScalarField>],
179        index: &ProverIndex<G, OpeningProof>,
180        prev_challenges: Vec<RecursionChallenge<G>>,
181        blinders: Option<[Option<PolyComm<G::ScalarField>>; COLUMNS]>,
182        rng: &mut RNG,
183    ) -> Result<Self>
184    where
185        VerifierIndex<G, OpeningProof>: Clone,
186    {
187        internal_tracing::checkpoint!(internal_traces; create_recursive);
188        let d1_size = index.cs.domain.d1.size();
189
190        let (_, endo_r) = G::endos();
191
192        let num_chunks = if d1_size < index.max_poly_size {
193            1
194        } else {
195            d1_size / index.max_poly_size
196        };
197
198        // Verify the circuit satisfiability by the computed witness (baring plookup constraints)
199        // Catch mistakes before proof generation.
200        if cfg!(debug_assertions) && !index.cs.disable_gates_checks {
201            let public = witness[0][0..index.cs.public].to_vec();
202            index.verify(&witness, &public).expect("incorrect witness");
203        }
204
205        //~ 1. Ensure we have room in the witness for the zero-knowledge rows.
206        //~    We currently expect the witness not to be of the same length as the domain,
207        //~    but instead be of the length of the (smaller) circuit.
208        //~    If we cannot add `zk_rows` rows to the columns of the witness before reaching
209        //~    the size of the domain, abort.
210        let length_witness = witness[0].len();
211        let length_padding = d1_size
212            .checked_sub(length_witness)
213            .ok_or(ProverError::NoRoomForZkInWitness)?;
214
215        let zero_knowledge_limit = zk_rows_strict_lower_bound(num_chunks);
216        // Because the lower bound is strict, the result of the function above
217        // is not a sufficient number of zero knowledge rows, so the error must
218        // be raised anytime the number of zero knowledge rows is not greater
219        // than the strict lower bound.
220        // Example:
221        //   for 1 chunk, `zero_knowledge_limit` is 2, and we need at least 3,
222        //   thus the error should be raised and the message should say that the
223        //   expected number of zero knowledge rows is 3 (hence the + 1).
224        if (index.cs.zk_rows as usize) <= zero_knowledge_limit {
225            return Err(ProverError::NotZeroKnowledge(
226                zero_knowledge_limit + 1,
227                index.cs.zk_rows as usize,
228            ));
229        }
230
231        if length_padding < index.cs.zk_rows as usize {
232            return Err(ProverError::NoRoomForZkInWitness);
233        }
234
235        //~ 1. Pad the witness columns with Zero gates to make them the same length as the domain.
236        //~    Then, randomize the last `zk_rows` of each columns.
237        internal_tracing::checkpoint!(internal_traces; pad_witness);
238        for w in &mut witness {
239            if w.len() != length_witness {
240                return Err(ProverError::WitnessCsInconsistent);
241            }
242
243            // padding
244            w.extend(core::iter::repeat(G::ScalarField::zero()).take(length_padding));
245
246            // zk-rows
247            for row in w.iter_mut().rev().take(index.cs.zk_rows as usize) {
248                *row = <G::ScalarField as UniformRand>::rand(rng);
249            }
250        }
251
252        //~ 1. Setup the Fq-Sponge.
253        internal_tracing::checkpoint!(internal_traces; set_up_fq_sponge);
254        let mut fq_sponge = EFqSponge::new(G::other_curve_sponge_params());
255
256        //~ 1. Absorb the digest of the VerifierIndex.
257        let verifier_index_digest = index.verifier_index_digest::<EFqSponge>();
258        fq_sponge.absorb_fq(&[verifier_index_digest]);
259
260        //~ 1. Absorb the commitments of the previous challenges with the Fq-sponge.
261        for RecursionChallenge { comm, .. } in &prev_challenges {
262            absorb_commitment(&mut fq_sponge, comm)
263        }
264
265        //~ 1. Compute the negated public input polynomial as
266        //~    the polynomial that evaluates to $-p_i$ for the first `public_input_size` values of the domain,
267        //~    and $0$ for the rest.
268        let public = witness[0][0..index.cs.public].to_vec();
269        let public_poly = -Evaluations::<G::ScalarField, D<G::ScalarField>>::from_vec_and_domain(
270            public,
271            index.cs.domain.d1,
272        )
273        .interpolate();
274
275        //~ 1. Commit (non-hiding) to the negated public input polynomial.
276        let public_comm = index.srs.commit_non_hiding(&public_poly, num_chunks);
277        let public_comm = {
278            index
279                .srs
280                .mask_custom(
281                    public_comm.clone(),
282                    &public_comm.map(|_| G::ScalarField::one()),
283                )
284                .unwrap()
285                .commitment
286        };
287
288        //~ 1. Absorb the commitment to the public polynomial with the Fq-Sponge.
289        //~
290        //~    Note: unlike the original PLONK protocol,
291        //~    the prover also provides evaluations of the public polynomial to help the verifier circuit.
292        //~    This is why we need to absorb the commitment to the public polynomial at this point.
293        absorb_commitment(&mut fq_sponge, &public_comm);
294
295        //~ 1. Commit to the witness columns by creating `COLUMNS` hidding commitments.
296        //~
297        //~    Note: since the witness is in evaluation form,
298        //~    we can use the `commit_evaluation` optimization.
299        internal_tracing::checkpoint!(internal_traces; commit_to_witness_columns);
300        // generate blinders if not given externally
301        let blinders_final: Vec<PolyComm<G::ScalarField>> = match blinders {
302            None => (0..COLUMNS)
303                .map(|_| PolyComm::new(vec![UniformRand::rand(rng); num_chunks]))
304                .collect(),
305            Some(blinders_arr) => blinders_arr
306                .into_iter()
307                .map(|blinder_el| match blinder_el {
308                    None => PolyComm::new(vec![UniformRand::rand(rng); num_chunks]),
309                    Some(blinder_el_some) => blinder_el_some,
310                })
311                .collect(),
312        };
313        let w_comm_opt_res: Vec<Result<_>> = witness
314            .clone()
315            .into_par_iter()
316            .zip(blinders_final.into_par_iter())
317            .map(|(witness, blinder)| {
318                let witness_eval =
319                    Evaluations::<G::ScalarField, D<G::ScalarField>>::from_vec_and_domain(
320                        witness,
321                        index.cs.domain.d1,
322                    );
323
324                // TODO: make this a function rather no? mask_with_custom()
325                let witness_com = index
326                    .srs
327                    .commit_evaluations_non_hiding(index.cs.domain.d1, &witness_eval);
328                let com = index
329                    .srs
330                    .mask_custom(witness_com, &blinder)
331                    .map_err(ProverError::WrongBlinders)?;
332
333                Ok(com)
334            })
335            .collect();
336
337        let w_comm_res: Result<Vec<BlindedCommitment<G>>> = w_comm_opt_res.into_iter().collect();
338
339        let w_comm = w_comm_res?;
340
341        let w_comm: [BlindedCommitment<G>; COLUMNS] = w_comm
342            .try_into()
343            .expect("previous loop is of the correct length");
344
345        //~ 1. Absorb the witness commitments with the Fq-Sponge.
346        w_comm
347            .iter()
348            .for_each(|c| absorb_commitment(&mut fq_sponge, &c.commitment));
349
350        //~ 1. Compute the witness polynomials by interpolating each `COLUMNS` of the witness.
351        //~    As mentioned above, we commit using the evaluations form rather than the coefficients
352        //~    form so we can take advantage of the sparsity of the evaluations (i.e., there are many
353        //~    0 entries and entries that have less-than-full-size field elemnts.)
354        let witness_poly: [DensePolynomial<G::ScalarField>; COLUMNS] = (0..COLUMNS)
355            .into_par_iter()
356            .map(|i| {
357                Evaluations::<G::ScalarField, D<G::ScalarField>>::from_vec_and_domain(
358                    witness[i].clone(),
359                    index.cs.domain.d1,
360                )
361                .interpolate()
362            })
363            .collect::<Vec<_>>()
364            .try_into()
365            .unwrap();
366
367        let mut lookup_context = LookupContext::default();
368
369        //~ 1. If using lookup:
370        let lookup_constraint_system = index
371            .cs
372            .lookup_constraint_system
373            .try_get_or_err()
374            .map_err(ProverError::from)?;
375        if let Some(lcs) = lookup_constraint_system {
376            internal_tracing::checkpoint!(internal_traces; use_lookup, {
377                "uses_lookup": true,
378                "uses_runtime_tables": lcs.runtime_tables.is_some(),
379            });
380            //~~ * if using runtime table:
381            if let Some(cfg_runtime_tables) = &lcs.runtime_tables {
382                //~~~ * check that all the provided runtime tables have length and IDs that match the runtime table configuration of the index
383                //~~~   we expect the given runtime tables to be sorted as configured, this makes it easier afterwards
384                let expected_runtime: Vec<_> = cfg_runtime_tables
385                    .iter()
386                    .map(|rt| (rt.id, rt.len))
387                    .collect();
388                let runtime: Vec<_> = runtime_tables
389                    .iter()
390                    .map(|rt| (rt.id, rt.data.len()))
391                    .collect();
392                if expected_runtime != runtime {
393                    return Err(ProverError::RuntimeTablesInconsistent);
394                }
395
396                //~~~ * calculate the contribution to the second column of the lookup table
397                //~~~   (the runtime vector)
398                let (runtime_table_contribution, runtime_table_contribution_d8) = {
399                    let mut offset = lcs
400                        .runtime_table_offset
401                        .expect("runtime configuration missing offset");
402
403                    let mut evals = vec![G::ScalarField::zero(); d1_size];
404                    for rt in runtime_tables {
405                        let range = offset..(offset + rt.data.len());
406                        evals[range].copy_from_slice(&rt.data);
407                        offset += rt.data.len();
408                    }
409
410                    // zero-knowledge
411                    for e in evals.iter_mut().rev().take(index.cs.zk_rows as usize) {
412                        *e = <G::ScalarField as UniformRand>::rand(rng);
413                    }
414
415                    // get coeff and evaluation form
416                    let runtime_table_contribution =
417                        Evaluations::from_vec_and_domain(evals, index.cs.domain.d1).interpolate();
418
419                    let runtime_table_contribution_d8 =
420                        runtime_table_contribution.evaluate_over_domain_by_ref(index.cs.domain.d8);
421
422                    (runtime_table_contribution, runtime_table_contribution_d8)
423                };
424
425                // commit the runtime polynomial
426                // (and save it to the proof)
427                let runtime_table_comm =
428                    index
429                        .srs
430                        .commit(&runtime_table_contribution, num_chunks, rng);
431
432                // absorb the commitment
433                absorb_commitment(&mut fq_sponge, &runtime_table_comm.commitment);
434
435                // pre-compute the updated second column of the lookup table
436                let mut second_column_d8 = runtime_table_contribution_d8.clone();
437                second_column_d8
438                    .evals
439                    .par_iter_mut()
440                    .enumerate()
441                    .for_each(|(row, e)| {
442                        *e += lcs.lookup_table8[1][row];
443                    });
444
445                lookup_context.runtime_table = Some(runtime_table_contribution);
446                lookup_context.runtime_table_d8 = Some(runtime_table_contribution_d8);
447                lookup_context.runtime_table_comm = Some(runtime_table_comm);
448                lookup_context.runtime_second_col_d8 = Some(second_column_d8);
449            }
450
451            //~~ * If queries involve a lookup table with multiple columns
452            //~~   then squeeze the Fq-Sponge to obtain the joint combiner challenge $j'$,
453            //~~   otherwise set the joint combiner challenge $j'$ to $0$.
454            let joint_combiner = if lcs.configuration.lookup_info.features.joint_lookup_used {
455                fq_sponge.challenge()
456            } else {
457                G::ScalarField::zero()
458            };
459
460            //~~ * Derive the scalar joint combiner $j$ from $j'$ using the endomorphism (TODO: specify)
461            let joint_combiner: G::ScalarField = ScalarChallenge(joint_combiner).to_field(endo_r);
462
463            //~~ * If multiple lookup tables are involved,
464            //~~   set the `table_id_combiner` as the $j^i$ with $i$ the maximum width of any used table.
465            //~~   Essentially, this is to add a last column of table ids to the concatenated lookup tables.
466            let table_id_combiner: G::ScalarField = if lcs.table_ids8.as_ref().is_some() {
467                joint_combiner.pow([lcs.configuration.lookup_info.max_joint_size as u64])
468            } else {
469                // TODO: just set this to None in case multiple tables are not used
470                G::ScalarField::zero()
471            };
472            lookup_context.table_id_combiner = Some(table_id_combiner);
473
474            //~~ * Compute the dummy lookup value as the combination of the last entry of the XOR table (so `(0, 0, 0)`).
475            //~~   Warning: This assumes that we always use the XOR table when using lookups.
476            let dummy_lookup_value = lcs
477                .configuration
478                .dummy_lookup
479                .evaluate(&joint_combiner, &table_id_combiner);
480            lookup_context.dummy_lookup_value = Some(dummy_lookup_value);
481
482            //~~ * Compute the lookup table values as the combination of the lookup table entries.
483            let joint_lookup_table_d8 = {
484                let mut evals = Vec::with_capacity(d1_size);
485
486                for idx in 0..(d1_size * 8) {
487                    let table_id = match lcs.table_ids8.as_ref() {
488                        Some(table_ids8) => table_ids8.evals[idx],
489                        None =>
490                        // If there is no `table_ids8` in the constraint system,
491                        // every table ID is identically 0.
492                        {
493                            G::ScalarField::zero()
494                        }
495                    };
496
497                    let combined_entry =
498                        if !lcs.configuration.lookup_info.features.uses_runtime_tables {
499                            let table_row = lcs.lookup_table8.iter().map(|e| &e.evals[idx]);
500
501                            combine_table_entry(
502                                &joint_combiner,
503                                &table_id_combiner,
504                                table_row,
505                                &table_id,
506                            )
507                        } else {
508                            // if runtime table are used, the second row is modified
509                            let second_col = lookup_context.runtime_second_col_d8.as_ref().unwrap();
510
511                            let table_row = lcs.lookup_table8.iter().enumerate().map(|(col, e)| {
512                                if col == 1 {
513                                    &second_col.evals[idx]
514                                } else {
515                                    &e.evals[idx]
516                                }
517                            });
518
519                            combine_table_entry(
520                                &joint_combiner,
521                                &table_id_combiner,
522                                table_row,
523                                &table_id,
524                            )
525                        };
526                    evals.push(combined_entry);
527                }
528
529                Evaluations::from_vec_and_domain(evals, index.cs.domain.d8)
530            };
531
532            // TODO: This interpolation is avoidable.
533            let joint_lookup_table = joint_lookup_table_d8.interpolate_by_ref();
534
535            //~~ * Compute the sorted evaluations.
536            // TODO: Once we switch to committing using lagrange commitments,
537            // `witness` will be consumed when we interpolate, so interpolation will
538            // have to moved below this.
539            let sorted: Vec<_> = lookup::constraints::sorted(
540                dummy_lookup_value,
541                &joint_lookup_table_d8,
542                index.cs.domain.d1,
543                &index.cs.gates,
544                &witness,
545                joint_combiner,
546                table_id_combiner,
547                &lcs.configuration.lookup_info,
548                index.cs.zk_rows as usize,
549            )?;
550
551            //~~ * Randomize the last `EVALS` rows in each of the sorted polynomials
552            //~~   in order to add zero-knowledge to the protocol.
553            let sorted: Vec<_> = sorted
554                .into_iter()
555                .map(|chunk| {
556                    lookup::constraints::zk_patch(
557                        chunk,
558                        index.cs.domain.d1,
559                        index.cs.zk_rows as usize,
560                        rng,
561                    )
562                })
563                .collect();
564
565            //~~ * Commit each of the sorted polynomials.
566            let sorted_comms: Vec<_> = sorted
567                .iter()
568                .map(|v| index.srs.commit_evaluations(index.cs.domain.d1, v, rng))
569                .collect();
570
571            //~~ * Absorb each commitments to the sorted polynomials.
572            sorted_comms
573                .iter()
574                .for_each(|c| absorb_commitment(&mut fq_sponge, &c.commitment));
575
576            // precompute different forms of the sorted polynomials for later
577            // TODO: We can avoid storing these coefficients.
578            let sorted_coeffs: Vec<_> = sorted.iter().map(|e| e.clone().interpolate()).collect();
579            let sorted8: Vec<_> = sorted_coeffs
580                .iter()
581                .map(|v| v.evaluate_over_domain_by_ref(index.cs.domain.d8))
582                .collect();
583
584            lookup_context.joint_combiner = Some(joint_combiner);
585            lookup_context.sorted = Some(sorted);
586            lookup_context.sorted_coeffs = Some(sorted_coeffs);
587            lookup_context.sorted_comms = Some(sorted_comms);
588            lookup_context.sorted8 = Some(sorted8);
589            lookup_context.joint_lookup_table_d8 = Some(joint_lookup_table_d8);
590            lookup_context.joint_lookup_table = Some(joint_lookup_table);
591        }
592
593        //~ 1. Sample $\beta$ with the Fq-Sponge.
594        let beta = fq_sponge.challenge();
595
596        //~ 1. Sample $\gamma$ with the Fq-Sponge.
597        let gamma = fq_sponge.challenge();
598
599        //~ 1. If using lookup:
600        if let Some(lcs) = lookup_constraint_system {
601            //~~ * Compute the lookup aggregation polynomial.
602            let joint_lookup_table_d8 = lookup_context.joint_lookup_table_d8.as_ref().unwrap();
603
604            let aggreg = lookup::constraints::aggregation::<_, G::ScalarField>(
605                lookup_context.dummy_lookup_value.unwrap(),
606                joint_lookup_table_d8,
607                index.cs.domain.d1,
608                &index.cs.gates,
609                &witness,
610                &lookup_context.joint_combiner.unwrap(),
611                &lookup_context.table_id_combiner.unwrap(),
612                beta,
613                gamma,
614                lookup_context.sorted.as_ref().unwrap(),
615                rng,
616                &lcs.configuration.lookup_info,
617                index.cs.zk_rows as usize,
618            )?;
619
620            //~~ * Commit to the aggregation polynomial.
621            let aggreg_comm = index
622                .srs
623                .commit_evaluations(index.cs.domain.d1, &aggreg, rng);
624
625            //~~ * Absorb the commitment to the aggregation polynomial with the Fq-Sponge.
626            absorb_commitment(&mut fq_sponge, &aggreg_comm.commitment);
627
628            // precompute different forms of the aggregation polynomial for later
629            let aggreg_coeffs = aggreg.interpolate();
630            // TODO: There's probably a clever way to expand the domain without
631            // interpolating
632            let aggreg8 = aggreg_coeffs.evaluate_over_domain_by_ref(index.cs.domain.d8);
633
634            lookup_context.aggreg_comm = Some(aggreg_comm);
635            lookup_context.aggreg_coeffs = Some(aggreg_coeffs);
636            lookup_context.aggreg8 = Some(aggreg8);
637        }
638
639        let column_evaluations = index.column_evaluations.get();
640
641        //~ 1. Compute the permutation aggregation polynomial $z$.
642        internal_tracing::checkpoint!(internal_traces; z_permutation_aggregation_polynomial);
643        let z_poly = index.perm_aggreg(&witness, &beta, &gamma, rng)?;
644
645        //~ 1. Commit (hidding) to the permutation aggregation polynomial $z$.
646        let z_comm = index.srs.commit(&z_poly, num_chunks, rng);
647
648        //~ 1. Absorb the permutation aggregation polynomial $z$ with the Fq-Sponge.
649        absorb_commitment(&mut fq_sponge, &z_comm.commitment);
650
651        //~ 1. Sample $\alpha'$ with the Fq-Sponge.
652        let alpha_chal = ScalarChallenge(fq_sponge.challenge());
653
654        //~ 1. Derive $\alpha$ from $\alpha'$ using the endomorphism (TODO: details)
655        let alpha: G::ScalarField = alpha_chal.to_field(endo_r);
656
657        //~ 1. TODO: instantiate alpha?
658        let mut all_alphas = index.powers_of_alpha.clone();
659        all_alphas.instantiate(alpha);
660
661        //~ 1. Compute the quotient polynomial (the $t$ in $f = Z_H \cdot t$).
662        //~    The quotient polynomial is computed by adding all these polynomials together:
663        //~~ * the combined constraints for all the gates
664        //~~ * the combined constraints for the permutation
665        //~~ * TODO: lookup
666        //~~ * the negated public polynomial
667        //~    and by then dividing the resulting polynomial with the vanishing polynomial $Z_H$.
668        //~    TODO: specify the split of the permutation polynomial into perm and bnd?
669        let lookup_env = if let Some(lcs) = lookup_constraint_system {
670            let joint_lookup_table_d8 = lookup_context.joint_lookup_table_d8.as_ref().unwrap();
671
672            Some(LookupEnvironment {
673                aggreg: lookup_context.aggreg8.as_ref().unwrap(),
674                sorted: lookup_context.sorted8.as_ref().unwrap(),
675                selectors: &lcs.lookup_selectors,
676                table: joint_lookup_table_d8,
677                runtime_selector: lcs.runtime_selector.as_ref(),
678                runtime_table: lookup_context.runtime_table_d8.as_ref(),
679            })
680        } else {
681            None
682        };
683
684        internal_tracing::checkpoint!(internal_traces; eval_witness_polynomials_over_domains);
685        let lagrange = index.cs.evaluate(&witness_poly, &z_poly);
686        internal_tracing::checkpoint!(internal_traces; compute_index_evals);
687        let env = {
688            let mut index_evals = HashMap::new();
689            use GateType::*;
690            index_evals.insert(Generic, &column_evaluations.generic_selector4);
691            index_evals.insert(Poseidon, &column_evaluations.poseidon_selector8);
692            index_evals.insert(CompleteAdd, &column_evaluations.complete_add_selector4);
693            index_evals.insert(VarBaseMul, &column_evaluations.mul_selector8);
694            index_evals.insert(EndoMul, &column_evaluations.emul_selector8);
695            index_evals.insert(EndoMulScalar, &column_evaluations.endomul_scalar_selector8);
696
697            if let Some(selector) = &column_evaluations.range_check0_selector8 {
698                index_evals.insert(GateType::RangeCheck0, selector);
699            }
700
701            if let Some(selector) = &column_evaluations.range_check1_selector8 {
702                index_evals.insert(GateType::RangeCheck1, selector);
703            }
704
705            if let Some(selector) = &column_evaluations.foreign_field_add_selector8 {
706                index_evals.insert(GateType::ForeignFieldAdd, selector);
707            }
708
709            if let Some(selector) = &column_evaluations.foreign_field_mul_selector8 {
710                index_evals.extend(
711                    foreign_field_mul::gadget::circuit_gates()
712                        .iter()
713                        .map(|gate_type| (*gate_type, selector)),
714                );
715            }
716
717            if let Some(selector) = &column_evaluations.xor_selector8 {
718                index_evals.insert(GateType::Xor16, selector);
719            }
720
721            if let Some(selector) = &column_evaluations.rot_selector8 {
722                index_evals.insert(GateType::Rot64, selector);
723            }
724
725            let mds = &G::sponge_params().mds;
726            Environment {
727                constants: Constants {
728                    endo_coefficient: index.cs.endo,
729                    mds,
730                    zk_rows: index.cs.zk_rows,
731                },
732                challenges: BerkeleyChallenges {
733                    alpha,
734                    beta,
735                    gamma,
736                    joint_combiner: lookup_context
737                        .joint_combiner
738                        .unwrap_or(G::ScalarField::zero()),
739                },
740                witness: &lagrange.d8.this.w,
741                coefficient: &column_evaluations.coefficients8,
742                vanishes_on_zero_knowledge_and_previous_rows: &index
743                    .cs
744                    .precomputations()
745                    .vanishes_on_zero_knowledge_and_previous_rows,
746                z: &lagrange.d8.this.z,
747                l0_1: l0_1(index.cs.domain.d1),
748                domain: index.cs.domain,
749                index: index_evals,
750                lookup: lookup_env,
751            }
752        };
753
754        let mut cache = expr::Cache::default();
755
756        internal_tracing::checkpoint!(internal_traces; compute_quotient_poly);
757
758        let quotient_poly = {
759            // generic
760            let mut t4 = {
761                let generic_constraint =
762                    generic::Generic::combined_constraints(&all_alphas, &mut cache);
763                let generic4 = generic_constraint.evaluations(&env);
764
765                if cfg!(debug_assertions) {
766                    let p4 = public_poly.evaluate_over_domain_by_ref(index.cs.domain.d4);
767                    let gen_minus_pub = &generic4 + &p4;
768
769                    check_constraint!(index, gen_minus_pub);
770                }
771
772                generic4
773            };
774
775            // permutation
776            let (mut t8, bnd) = {
777                let alphas =
778                    all_alphas.get_alphas(ArgumentType::Permutation, permutation::CONSTRAINTS);
779                let (perm, bnd) = index.perm_quot(&lagrange, beta, gamma, &z_poly, alphas)?;
780
781                check_constraint!(index, perm);
782
783                (perm, bnd)
784            };
785
786            {
787                use crate::circuits::argument::DynArgument;
788
789                let range_check0_enabled = column_evaluations.range_check0_selector8.is_some();
790                let range_check1_enabled = column_evaluations.range_check1_selector8.is_some();
791                let foreign_field_addition_enabled =
792                    column_evaluations.foreign_field_add_selector8.is_some();
793                let foreign_field_multiplication_enabled =
794                    column_evaluations.foreign_field_mul_selector8.is_some();
795                let xor_enabled = column_evaluations.xor_selector8.is_some();
796                let rot_enabled = column_evaluations.rot_selector8.is_some();
797
798                for gate in [
799                    (
800                        (&CompleteAdd::default() as &dyn DynArgument<G::ScalarField>),
801                        true,
802                    ),
803                    (&VarbaseMul::default(), true),
804                    (&EndosclMul::default(), true),
805                    (&EndomulScalar::default(), true),
806                    (&Poseidon::default(), true),
807                    // Range check gates
808                    (&RangeCheck0::default(), range_check0_enabled),
809                    (&RangeCheck1::default(), range_check1_enabled),
810                    // Foreign field addition gate
811                    (&ForeignFieldAdd::default(), foreign_field_addition_enabled),
812                    // Foreign field multiplication gate
813                    (
814                        &ForeignFieldMul::default(),
815                        foreign_field_multiplication_enabled,
816                    ),
817                    // Xor gate
818                    (&Xor16::default(), xor_enabled),
819                    // Rot gate
820                    (&Rot64::default(), rot_enabled),
821                ]
822                .into_iter()
823                .filter_map(|(gate, is_enabled)| if is_enabled { Some(gate) } else { None })
824                {
825                    let constraint = gate.combined_constraints(&all_alphas, &mut cache);
826                    let eval = constraint.evaluations(&env);
827                    if eval.domain().size == t4.domain().size {
828                        t4 += &eval;
829                    } else if eval.domain().size == t8.domain().size {
830                        t8 += &eval;
831                    } else {
832                        panic!("Bad evaluation")
833                    }
834                    check_constraint!(index, format!("{:?}", gate.argument_type()), eval);
835                }
836            };
837
838            // lookup
839            {
840                if let Some(lcs) = lookup_constraint_system {
841                    let constraints = lookup::constraints::constraints(&lcs.configuration, false);
842                    let constraints_len = u32::try_from(constraints.len())
843                        .expect("not expecting a large amount of constraints");
844                    let lookup_alphas =
845                        all_alphas.get_alphas(ArgumentType::Lookup, constraints_len);
846
847                    // as lookup constraints are computed with the expression framework,
848                    // each of them can result in Evaluations of different domains
849                    for (ii, (constraint, alpha_pow)) in
850                        constraints.into_iter().zip_eq(lookup_alphas).enumerate()
851                    {
852                        let mut eval = constraint.evaluations(&env);
853                        eval.evals.par_iter_mut().for_each(|x| *x *= alpha_pow);
854
855                        if eval.domain().size == t4.domain().size {
856                            t4 += &eval;
857                        } else if eval.domain().size == t8.domain().size {
858                            t8 += &eval;
859                        } else if eval.evals.iter().all(|x| x.is_zero()) {
860                            // Skip any 0-valued evaluations
861                        } else {
862                            panic!("Bad evaluation")
863                        }
864
865                        check_constraint!(index, format!("lookup constraint #{ii}"), eval);
866                    }
867                }
868            }
869
870            // public polynomial
871            let mut f = t4.interpolate() + t8.interpolate();
872            f += &public_poly;
873
874            // divide contributions with vanishing polynomial
875            let (mut quotient, res) = f.divide_by_vanishing_poly(index.cs.domain.d1);
876            if !res.is_zero() {
877                return Err(ProverError::Prover(
878                    "rest of division by vanishing polynomial",
879                ));
880            }
881
882            quotient += &bnd; // already divided by Z_H
883            quotient
884        };
885
886        //~ 1. commit (hiding) to the quotient polynomial $t$
887        let t_comm = { index.srs.commit(&quotient_poly, 7 * num_chunks, rng) };
888
889        //~ 1. Absorb the commitment of the quotient polynomial with the Fq-Sponge.
890        absorb_commitment(&mut fq_sponge, &t_comm.commitment);
891
892        //~ 1. Sample $\zeta'$ with the Fq-Sponge.
893        let zeta_chal = ScalarChallenge(fq_sponge.challenge());
894
895        //~ 1. Derive $\zeta$ from $\zeta'$ using the endomorphism (TODO: specify)
896        let zeta = zeta_chal.to_field(endo_r);
897
898        let omega = index.cs.domain.d1.group_gen;
899        let zeta_omega = zeta * omega;
900
901        //~ 1. If lookup is used, evaluate the following polynomials at $\zeta$ and $\zeta \omega$:
902        if lookup_constraint_system.is_some() {
903            //~~ * the aggregation polynomial
904            let aggreg = lookup_context
905                .aggreg_coeffs
906                .as_ref()
907                .unwrap()
908                .to_chunked_polynomial(num_chunks, index.max_poly_size);
909
910            //~~ * the sorted polynomials
911            let sorted = lookup_context
912                .sorted_coeffs
913                .as_ref()
914                .unwrap()
915                .iter()
916                .map(|c| c.to_chunked_polynomial(num_chunks, index.max_poly_size))
917                .collect::<Vec<_>>();
918
919            //~~ * the table polynonial
920            let joint_table = lookup_context.joint_lookup_table.as_ref().unwrap();
921            let joint_table = joint_table.to_chunked_polynomial(num_chunks, index.max_poly_size);
922
923            lookup_context.lookup_aggregation_eval = Some(PointEvaluations {
924                zeta: aggreg.evaluate_chunks(zeta),
925                zeta_omega: aggreg.evaluate_chunks(zeta_omega),
926            });
927            lookup_context.lookup_table_eval = Some(PointEvaluations {
928                zeta: joint_table.evaluate_chunks(zeta),
929                zeta_omega: joint_table.evaluate_chunks(zeta_omega),
930            });
931            lookup_context.lookup_sorted_eval = array::from_fn(|i| {
932                if i < sorted.len() {
933                    let sorted = &sorted[i];
934                    Some(PointEvaluations {
935                        zeta: sorted.evaluate_chunks(zeta),
936                        zeta_omega: sorted.evaluate_chunks(zeta_omega),
937                    })
938                } else {
939                    None
940                }
941            });
942            lookup_context.runtime_lookup_table_eval =
943                lookup_context.runtime_table.as_ref().map(|runtime_table| {
944                    let runtime_table =
945                        runtime_table.to_chunked_polynomial(num_chunks, index.max_poly_size);
946                    PointEvaluations {
947                        zeta: runtime_table.evaluate_chunks(zeta),
948                        zeta_omega: runtime_table.evaluate_chunks(zeta_omega),
949                    }
950                });
951        }
952
953        //~ 1. Chunk evaluate the following polynomials at both $\zeta$ and $\zeta \omega$:
954        //~~ * $s_i$
955        //~~ * $w_i$
956        //~~ * $z$
957        //~~ * lookup (TODO, see [this issue](https://github.com/MinaProtocol/mina/issues/13886))
958        //~~ * generic selector
959        //~~ * poseidon selector
960        //~
961        //~    By "chunk evaluate" we mean that the evaluation of each polynomial can potentially be a vector of values.
962        //~    This is because the index's `max_poly_size` parameter dictates the maximum size of a polynomial in the protocol.
963        //~    If a polynomial $f$ exceeds this size, it must be split into several polynomials like so:
964        //~    $$f(x) = f_0(x) + x^n f_1(x) + x^{2n} f_2(x) + \cdots$$
965        //~
966        //~    And the evaluation of such a polynomial is the following list for $x \in {\zeta, \zeta\omega}$:
967        //~
968        //~    $$(f_0(x), f_1(x), f_2(x), \ldots)$$
969        //~
970        //~    TODO: do we want to specify more on that? It seems unnecessary except for the t polynomial (or if for some reason someone sets that to a low value)
971
972        internal_tracing::checkpoint!(internal_traces; lagrange_basis_eval_zeta_poly);
973        let zeta_evals =
974            LagrangeBasisEvaluations::new(index.max_poly_size, index.cs.domain.d1, zeta);
975        internal_tracing::checkpoint!(internal_traces; lagrange_basis_eval_zeta_omega_poly);
976        let zeta_omega_evals =
977            LagrangeBasisEvaluations::new(index.max_poly_size, index.cs.domain.d1, zeta_omega);
978
979        let chunked_evals_for_selector =
980            |p: &Evaluations<G::ScalarField, D<G::ScalarField>>| PointEvaluations {
981                zeta: zeta_evals.evaluate_boolean(p),
982                zeta_omega: zeta_omega_evals.evaluate_boolean(p),
983            };
984
985        let chunked_evals_for_evaluations =
986            |p: &Evaluations<G::ScalarField, D<G::ScalarField>>| PointEvaluations {
987                zeta: zeta_evals.evaluate(p),
988                zeta_omega: zeta_omega_evals.evaluate(p),
989            };
990
991        internal_tracing::checkpoint!(internal_traces; chunk_eval_zeta_omega_poly);
992        let chunked_evals = ProofEvaluations::<PointEvaluations<Vec<G::ScalarField>>> {
993            public: {
994                let chunked = public_poly.to_chunked_polynomial(num_chunks, index.max_poly_size);
995                Some(PointEvaluations {
996                    zeta: chunked.evaluate_chunks(zeta),
997                    zeta_omega: chunked.evaluate_chunks(zeta_omega),
998                })
999            },
1000            s: array::from_fn(|i| {
1001                chunked_evals_for_evaluations(&column_evaluations.permutation_coefficients8[i])
1002            }),
1003            coefficients: array::from_fn(|i| {
1004                chunked_evals_for_evaluations(&column_evaluations.coefficients8[i])
1005            }),
1006            w: array::from_fn(|i| {
1007                let chunked =
1008                    witness_poly[i].to_chunked_polynomial(num_chunks, index.max_poly_size);
1009                PointEvaluations {
1010                    zeta: chunked.evaluate_chunks(zeta),
1011                    zeta_omega: chunked.evaluate_chunks(zeta_omega),
1012                }
1013            }),
1014
1015            z: {
1016                let chunked = z_poly.to_chunked_polynomial(num_chunks, index.max_poly_size);
1017                PointEvaluations {
1018                    zeta: chunked.evaluate_chunks(zeta),
1019                    zeta_omega: chunked.evaluate_chunks(zeta_omega),
1020                }
1021            },
1022
1023            lookup_aggregation: lookup_context.lookup_aggregation_eval.take(),
1024            lookup_table: lookup_context.lookup_table_eval.take(),
1025            lookup_sorted: array::from_fn(|i| lookup_context.lookup_sorted_eval[i].take()),
1026            runtime_lookup_table: lookup_context.runtime_lookup_table_eval.take(),
1027            generic_selector: chunked_evals_for_selector(&column_evaluations.generic_selector4),
1028            poseidon_selector: chunked_evals_for_selector(&column_evaluations.poseidon_selector8),
1029            complete_add_selector: chunked_evals_for_selector(
1030                &column_evaluations.complete_add_selector4,
1031            ),
1032            mul_selector: chunked_evals_for_selector(&column_evaluations.mul_selector8),
1033            emul_selector: chunked_evals_for_selector(&column_evaluations.emul_selector8),
1034            endomul_scalar_selector: chunked_evals_for_selector(
1035                &column_evaluations.endomul_scalar_selector8,
1036            ),
1037
1038            range_check0_selector: column_evaluations
1039                .range_check0_selector8
1040                .as_ref()
1041                .map(chunked_evals_for_selector),
1042            range_check1_selector: column_evaluations
1043                .range_check1_selector8
1044                .as_ref()
1045                .map(chunked_evals_for_selector),
1046            foreign_field_add_selector: column_evaluations
1047                .foreign_field_add_selector8
1048                .as_ref()
1049                .map(chunked_evals_for_selector),
1050            foreign_field_mul_selector: column_evaluations
1051                .foreign_field_mul_selector8
1052                .as_ref()
1053                .map(chunked_evals_for_selector),
1054            xor_selector: column_evaluations
1055                .xor_selector8
1056                .as_ref()
1057                .map(chunked_evals_for_selector),
1058            rot_selector: column_evaluations
1059                .rot_selector8
1060                .as_ref()
1061                .map(chunked_evals_for_selector),
1062
1063            runtime_lookup_table_selector: lookup_constraint_system.as_ref().and_then(|lcs| {
1064                lcs.runtime_selector
1065                    .as_ref()
1066                    .map(chunked_evals_for_selector)
1067            }),
1068            xor_lookup_selector: lookup_constraint_system.as_ref().and_then(|lcs| {
1069                lcs.lookup_selectors
1070                    .xor
1071                    .as_ref()
1072                    .map(chunked_evals_for_selector)
1073            }),
1074            lookup_gate_lookup_selector: lookup_constraint_system.as_ref().and_then(|lcs| {
1075                lcs.lookup_selectors
1076                    .lookup
1077                    .as_ref()
1078                    .map(chunked_evals_for_selector)
1079            }),
1080            range_check_lookup_selector: lookup_constraint_system.as_ref().and_then(|lcs| {
1081                lcs.lookup_selectors
1082                    .range_check
1083                    .as_ref()
1084                    .map(chunked_evals_for_selector)
1085            }),
1086            foreign_field_mul_lookup_selector: lookup_constraint_system.as_ref().and_then(|lcs| {
1087                lcs.lookup_selectors
1088                    .ffmul
1089                    .as_ref()
1090                    .map(chunked_evals_for_selector)
1091            }),
1092        };
1093
1094        let zeta_to_srs_len = zeta.pow([index.max_poly_size as u64]);
1095        let zeta_omega_to_srs_len = zeta_omega.pow([index.max_poly_size as u64]);
1096        let zeta_to_domain_size = zeta.pow([d1_size as u64]);
1097
1098        //~ 1. Evaluate the same polynomials without chunking them
1099        //~    (so that each polynomial should correspond to a single value this time).
1100        let evals: ProofEvaluations<PointEvaluations<G::ScalarField>> = {
1101            let powers_of_eval_points_for_chunks = PointEvaluations {
1102                zeta: zeta_to_srs_len,
1103                zeta_omega: zeta_omega_to_srs_len,
1104            };
1105            chunked_evals.combine(&powers_of_eval_points_for_chunks)
1106        };
1107
1108        //~ 1. Compute the ft polynomial.
1109        //~    This is to implement [Maller's optimization](https://o1-labs.github.io/proof-systems/kimchi/maller_15.html).
1110        internal_tracing::checkpoint!(internal_traces; compute_ft_poly);
1111        let ft: DensePolynomial<G::ScalarField> = {
1112            let f_chunked = {
1113                // TODO: compute the linearization polynomial in evaluation form so
1114                // that we can drop the coefficient forms of the index polynomials from
1115                // the constraint system struct
1116
1117                // permutation (not part of linearization yet)
1118                let alphas =
1119                    all_alphas.get_alphas(ArgumentType::Permutation, permutation::CONSTRAINTS);
1120                let f = index.perm_lnrz(&evals, zeta, beta, gamma, alphas);
1121
1122                // the circuit polynomial
1123                let f = {
1124                    let (_lin_constant, mut lin) =
1125                        index.linearization.to_polynomial(&env, zeta, &evals);
1126                    lin += &f;
1127                    lin.interpolate()
1128                };
1129
1130                drop(env);
1131
1132                // see https://o1-labs.github.io/proof-systems/kimchi/maller_15.html#the-prover-side
1133                f.to_chunked_polynomial(num_chunks, index.max_poly_size)
1134                    .linearize(zeta_to_srs_len)
1135            };
1136
1137            let t_chunked = quotient_poly
1138                .to_chunked_polynomial(7 * num_chunks, index.max_poly_size)
1139                .linearize(zeta_to_srs_len);
1140
1141            &f_chunked - &t_chunked.scale(zeta_to_domain_size - G::ScalarField::one())
1142        };
1143
1144        //~ 1. construct the blinding part of the ft polynomial commitment
1145        //~    [see this section](https://o1-labs.github.io/proof-systems/kimchi/maller_15.html#evaluation-proof-and-blinding-factors)
1146        let blinding_ft = {
1147            let blinding_t = t_comm.blinders.chunk_blinding(zeta_to_srs_len);
1148            let blinding_f = G::ScalarField::zero();
1149
1150            PolyComm {
1151                // blinding_f - Z_H(zeta) * blinding_t
1152                chunks: vec![
1153                    blinding_f - (zeta_to_domain_size - G::ScalarField::one()) * blinding_t,
1154                ],
1155            }
1156        };
1157
1158        //~ 1. Evaluate the ft polynomial at $\zeta\omega$ only.
1159        internal_tracing::checkpoint!(internal_traces; ft_eval_zeta_omega);
1160        let ft_eval1 = ft.evaluate(&zeta_omega);
1161
1162        //~ 1. Setup the Fr-Sponge
1163        let fq_sponge_before_evaluations = fq_sponge.clone();
1164        let mut fr_sponge = EFrSponge::new(G::sponge_params());
1165
1166        //~ 1. Squeeze the Fq-sponge and absorb the result with the Fr-Sponge.
1167        fr_sponge.absorb(&fq_sponge.digest());
1168
1169        //~ 1. Absorb the previous recursion challenges.
1170        let prev_challenge_digest = {
1171            // Note: we absorb in a new sponge here to limit the scope in which we need the
1172            // more-expensive 'optional sponge'.
1173            let mut fr_sponge = EFrSponge::new(G::sponge_params());
1174            for RecursionChallenge { chals, .. } in &prev_challenges {
1175                fr_sponge.absorb_multiple(chals);
1176            }
1177            fr_sponge.digest()
1178        };
1179        fr_sponge.absorb(&prev_challenge_digest);
1180
1181        //~ 1. Compute evaluations for the previous recursion challenges.
1182        internal_tracing::checkpoint!(internal_traces; build_polynomials);
1183        let polys = prev_challenges
1184            .iter()
1185            .map(|RecursionChallenge { chals, comm }| {
1186                (
1187                    DensePolynomial::from_coefficients_vec(b_poly_coefficients(chals)),
1188                    comm.len(),
1189                )
1190            })
1191            .collect::<Vec<_>>();
1192
1193        //~ 1. Absorb the unique evaluation of ft: $ft(\zeta\omega)$.
1194        fr_sponge.absorb(&ft_eval1);
1195
1196        //~ 1. Absorb all the polynomial evaluations in $\zeta$ and $\zeta\omega$:
1197        //~~ * the public polynomial
1198        //~~ * z
1199        //~~ * generic selector
1200        //~~ * poseidon selector
1201        //~~ * the 15 register/witness
1202        //~~ * 6 sigmas evaluations (the last one is not evaluated)
1203        fr_sponge.absorb_multiple(&chunked_evals.public.as_ref().unwrap().zeta);
1204        fr_sponge.absorb_multiple(&chunked_evals.public.as_ref().unwrap().zeta_omega);
1205        fr_sponge.absorb_evaluations(&chunked_evals);
1206
1207        //~ 1. Sample $v'$ with the Fr-Sponge
1208        let v_chal = fr_sponge.challenge();
1209
1210        //~ 1. Derive $v$ from $v'$ using the endomorphism (TODO: specify)
1211        let v = v_chal.to_field(endo_r);
1212
1213        //~ 1. Sample $u'$ with the Fr-Sponge
1214        let u_chal = fr_sponge.challenge();
1215
1216        //~ 1. Derive $u$ from $u'$ using the endomorphism (TODO: specify)
1217        let u = u_chal.to_field(endo_r);
1218
1219        //~ 1. Create a list of all polynomials that will require evaluations
1220        //~    (and evaluation proofs) in the protocol.
1221        //~    First, include the previous challenges, in case we are in a recursive prover.
1222        let non_hiding = |n_chunks: usize| PolyComm {
1223            chunks: vec![G::ScalarField::zero(); n_chunks],
1224        };
1225
1226        let fixed_hiding = |n_chunks: usize| PolyComm {
1227            chunks: vec![G::ScalarField::one(); n_chunks],
1228        };
1229
1230        let coefficients_form = DensePolynomialOrEvaluations::DensePolynomial;
1231        let evaluations_form = |e| DensePolynomialOrEvaluations::Evaluations(e, index.cs.domain.d1);
1232
1233        let mut polynomials = polys
1234            .iter()
1235            .map(|(p, n_chunks)| (coefficients_form(p), non_hiding(*n_chunks)))
1236            .collect::<Vec<_>>();
1237
1238        //~ 1. Then, include:
1239        //~~ * the negated public polynomial
1240        //~~ * the ft polynomial
1241        //~~ * the permutation aggregation polynomial z polynomial
1242        //~~ * the generic selector
1243        //~~ * the poseidon selector
1244        //~~ * the 15 registers/witness columns
1245        //~~ * the 6 sigmas
1246        polynomials.push((coefficients_form(&public_poly), fixed_hiding(num_chunks)));
1247        polynomials.push((coefficients_form(&ft), blinding_ft));
1248        polynomials.push((coefficients_form(&z_poly), z_comm.blinders));
1249        polynomials.push((
1250            evaluations_form(&column_evaluations.generic_selector4),
1251            fixed_hiding(num_chunks),
1252        ));
1253        polynomials.push((
1254            evaluations_form(&column_evaluations.poseidon_selector8),
1255            fixed_hiding(num_chunks),
1256        ));
1257        polynomials.push((
1258            evaluations_form(&column_evaluations.complete_add_selector4),
1259            fixed_hiding(num_chunks),
1260        ));
1261        polynomials.push((
1262            evaluations_form(&column_evaluations.mul_selector8),
1263            fixed_hiding(num_chunks),
1264        ));
1265        polynomials.push((
1266            evaluations_form(&column_evaluations.emul_selector8),
1267            fixed_hiding(num_chunks),
1268        ));
1269        polynomials.push((
1270            evaluations_form(&column_evaluations.endomul_scalar_selector8),
1271            fixed_hiding(num_chunks),
1272        ));
1273        polynomials.extend(
1274            witness_poly
1275                .iter()
1276                .zip(w_comm.iter())
1277                .map(|(w, c)| (coefficients_form(w), c.blinders.clone()))
1278                .collect::<Vec<_>>(),
1279        );
1280        polynomials.extend(
1281            column_evaluations
1282                .coefficients8
1283                .iter()
1284                .map(|coefficientm| (evaluations_form(coefficientm), non_hiding(num_chunks)))
1285                .collect::<Vec<_>>(),
1286        );
1287        polynomials.extend(
1288            column_evaluations.permutation_coefficients8[0..PERMUTS - 1]
1289                .iter()
1290                .map(|w| (evaluations_form(w), non_hiding(num_chunks)))
1291                .collect::<Vec<_>>(),
1292        );
1293
1294        //~~ * the optional gates
1295        if let Some(range_check0_selector8) = &column_evaluations.range_check0_selector8 {
1296            polynomials.push((
1297                evaluations_form(range_check0_selector8),
1298                non_hiding(num_chunks),
1299            ));
1300        }
1301        if let Some(range_check1_selector8) = &column_evaluations.range_check1_selector8 {
1302            polynomials.push((
1303                evaluations_form(range_check1_selector8),
1304                non_hiding(num_chunks),
1305            ));
1306        }
1307        if let Some(foreign_field_add_selector8) = &column_evaluations.foreign_field_add_selector8 {
1308            polynomials.push((
1309                evaluations_form(foreign_field_add_selector8),
1310                non_hiding(num_chunks),
1311            ));
1312        }
1313        if let Some(foreign_field_mul_selector8) = &column_evaluations.foreign_field_mul_selector8 {
1314            polynomials.push((
1315                evaluations_form(foreign_field_mul_selector8),
1316                non_hiding(num_chunks),
1317            ));
1318        }
1319        if let Some(xor_selector8) = &column_evaluations.xor_selector8 {
1320            polynomials.push((evaluations_form(xor_selector8), non_hiding(num_chunks)));
1321        }
1322        if let Some(rot_selector8) = &column_evaluations.rot_selector8 {
1323            polynomials.push((evaluations_form(rot_selector8), non_hiding(num_chunks)));
1324        }
1325
1326        //~~ * optionally, the runtime table
1327        //~ 1. if using lookup:
1328        if let Some(lcs) = lookup_constraint_system {
1329            //~~ * add the lookup sorted polynomials
1330            let sorted_poly = lookup_context.sorted_coeffs.as_ref().unwrap();
1331            let sorted_comms = lookup_context.sorted_comms.as_ref().unwrap();
1332
1333            for (poly, comm) in sorted_poly.iter().zip(sorted_comms) {
1334                polynomials.push((coefficients_form(poly), comm.blinders.clone()));
1335            }
1336
1337            //~~ * add the lookup aggreg polynomial
1338            let aggreg_poly = lookup_context.aggreg_coeffs.as_ref().unwrap();
1339            let aggreg_comm = lookup_context.aggreg_comm.as_ref().unwrap();
1340            polynomials.push((coefficients_form(aggreg_poly), aggreg_comm.blinders.clone()));
1341
1342            //~~ * add the combined table polynomial
1343            let table_blinding = {
1344                let joint_combiner = lookup_context.joint_combiner.as_ref().unwrap();
1345                let table_id_combiner = lookup_context.table_id_combiner.as_ref().unwrap();
1346                let max_fixed_lookup_table_size = {
1347                    // CAUTION: This is not `lcs.configuration.lookup_info.max_joint_size` because
1348                    // the lookup table may be strictly narrower, and as such will not contribute
1349                    // the associated blinders.
1350                    // For example, using a runtime table with the lookup gate (width 2), but only
1351                    // width-1 fixed tables (e.g. range check), it would be incorrect to use the
1352                    // wider width (2) because there are no such contributing commitments!
1353                    // Note that lookup_table8 is a list of polynomials
1354                    lcs.lookup_table8.len()
1355                };
1356                let base_blinding = {
1357                    let fixed_table_blinding = if max_fixed_lookup_table_size == 0 {
1358                        G::ScalarField::zero()
1359                    } else {
1360                        (1..max_fixed_lookup_table_size).fold(G::ScalarField::one(), |acc, _| {
1361                            G::ScalarField::one() + *joint_combiner * acc
1362                        })
1363                    };
1364                    fixed_table_blinding + *table_id_combiner
1365                };
1366                if lcs.runtime_selector.is_some() {
1367                    let runtime_comm = lookup_context.runtime_table_comm.as_ref().unwrap();
1368
1369                    let chunks = runtime_comm
1370                        .blinders
1371                        .into_iter()
1372                        .map(|blinding| *joint_combiner * *blinding + base_blinding)
1373                        .collect();
1374
1375                    PolyComm::new(chunks)
1376                } else {
1377                    let chunks = vec![base_blinding; num_chunks];
1378                    PolyComm::new(chunks)
1379                }
1380            };
1381
1382            let joint_lookup_table = lookup_context.joint_lookup_table.as_ref().unwrap();
1383
1384            polynomials.push((coefficients_form(joint_lookup_table), table_blinding));
1385
1386            //~~ * if present, add the runtime table polynomial
1387            if lcs.runtime_selector.is_some() {
1388                let runtime_table_comm = lookup_context.runtime_table_comm.as_ref().unwrap();
1389                let runtime_table = lookup_context.runtime_table.as_ref().unwrap();
1390
1391                polynomials.push((
1392                    coefficients_form(runtime_table),
1393                    runtime_table_comm.blinders.clone(),
1394                ));
1395            }
1396
1397            //~~ * the lookup selectors
1398
1399            if let Some(runtime_lookup_table_selector) = &lcs.runtime_selector {
1400                polynomials.push((
1401                    evaluations_form(runtime_lookup_table_selector),
1402                    non_hiding(1),
1403                ))
1404            }
1405            if let Some(xor_lookup_selector) = &lcs.lookup_selectors.xor {
1406                polynomials.push((evaluations_form(xor_lookup_selector), non_hiding(1)))
1407            }
1408            if let Some(lookup_gate_selector) = &lcs.lookup_selectors.lookup {
1409                polynomials.push((evaluations_form(lookup_gate_selector), non_hiding(1)))
1410            }
1411            if let Some(range_check_lookup_selector) = &lcs.lookup_selectors.range_check {
1412                polynomials.push((evaluations_form(range_check_lookup_selector), non_hiding(1)))
1413            }
1414            if let Some(foreign_field_mul_lookup_selector) = &lcs.lookup_selectors.ffmul {
1415                polynomials.push((
1416                    evaluations_form(foreign_field_mul_lookup_selector),
1417                    non_hiding(1),
1418                ))
1419            }
1420        }
1421
1422        //~ 1. Create an aggregated evaluation proof for all of these polynomials at $\zeta$ and $\zeta\omega$ using $u$ and $v$.
1423        internal_tracing::checkpoint!(internal_traces; create_aggregated_ipa);
1424        let proof = OpenProof::open(
1425            &*index.srs,
1426            group_map,
1427            &polynomials,
1428            &[zeta, zeta_omega],
1429            v,
1430            u,
1431            fq_sponge_before_evaluations,
1432            rng,
1433        );
1434
1435        let lookup = lookup_context
1436            .aggreg_comm
1437            .zip(lookup_context.sorted_comms)
1438            .map(|(a, s)| LookupCommitments {
1439                aggreg: a.commitment,
1440                sorted: s.iter().map(|c| c.commitment.clone()).collect(),
1441                runtime: lookup_context.runtime_table_comm.map(|x| x.commitment),
1442            });
1443
1444        let proof = Self {
1445            commitments: ProverCommitments {
1446                w_comm: array::from_fn(|i| w_comm[i].commitment.clone()),
1447                z_comm: z_comm.commitment,
1448                t_comm: t_comm.commitment,
1449                lookup,
1450            },
1451            proof,
1452            evals: chunked_evals,
1453            ft_eval1,
1454            prev_challenges,
1455        };
1456
1457        internal_tracing::checkpoint!(internal_traces; create_recursive_done);
1458
1459        Ok(proof)
1460    }
1461}
1462
1463internal_tracing::decl_traces!(internal_traces;
1464    pasta_fp_plonk_proof_create,
1465    pasta_fq_plonk_proof_create,
1466    create_recursive,
1467    pad_witness,
1468    set_up_fq_sponge,
1469    commit_to_witness_columns,
1470    use_lookup,
1471    z_permutation_aggregation_polynomial,
1472    eval_witness_polynomials_over_domains,
1473    compute_index_evals,
1474    compute_quotient_poly,
1475    lagrange_basis_eval_zeta_poly,
1476    lagrange_basis_eval_zeta_omega_poly,
1477    chunk_eval_zeta_omega_poly,
1478    compute_ft_poly,
1479    ft_eval_zeta_omega,
1480    build_polynomials,
1481    create_aggregated_ipa,
1482    create_recursive_done);
1483
1484#[cfg(feature = "ocaml_types")]
1485pub mod caml {
1486    use super::*;
1487    use crate::proof::caml::{CamlProofEvaluations, CamlRecursionChallenge};
1488    use ark_ec::AffineRepr;
1489    use poly_commitment::{
1490        commitment::caml::CamlPolyComm,
1491        ipa::{caml::CamlOpeningProof, OpeningProof},
1492    };
1493
1494    #[cfg(feature = "internal_tracing")]
1495    pub use internal_traces::caml::CamlTraces as CamlProverTraces;
1496
1497    #[derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)]
1498    pub struct CamlProofWithPublic<CamlG, CamlF> {
1499        pub public_evals: Option<PointEvaluations<Vec<CamlF>>>,
1500        pub proof: CamlProverProof<CamlG, CamlF>,
1501    }
1502
1503    //
1504    // CamlProverProof<CamlG, CamlF>
1505    //
1506
1507    #[derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)]
1508    pub struct CamlProverProof<CamlG, CamlF> {
1509        pub commitments: CamlProverCommitments<CamlG>,
1510        pub proof: CamlOpeningProof<CamlG, CamlF>,
1511        // OCaml doesn't have sized arrays, so we have to convert to a tuple..
1512        pub evals: CamlProofEvaluations<CamlF>,
1513        pub ft_eval1: CamlF,
1514        pub public: Vec<CamlF>,
1515        //Vec<(Vec<CamlF>, CamlPolyComm<CamlG>)>,
1516        pub prev_challenges: Vec<CamlRecursionChallenge<CamlG, CamlF>>,
1517    }
1518
1519    //
1520    // CamlProverCommitments<CamlG>
1521    //
1522
1523    #[derive(Clone, ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)]
1524    pub struct CamlLookupCommitments<CamlG> {
1525        pub sorted: Vec<CamlPolyComm<CamlG>>,
1526        pub aggreg: CamlPolyComm<CamlG>,
1527        pub runtime: Option<CamlPolyComm<CamlG>>,
1528    }
1529
1530    #[allow(clippy::type_complexity)]
1531    #[derive(Clone, ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)]
1532    pub struct CamlProverCommitments<CamlG> {
1533        // polynomial commitments
1534        pub w_comm: (
1535            CamlPolyComm<CamlG>,
1536            CamlPolyComm<CamlG>,
1537            CamlPolyComm<CamlG>,
1538            CamlPolyComm<CamlG>,
1539            CamlPolyComm<CamlG>,
1540            CamlPolyComm<CamlG>,
1541            CamlPolyComm<CamlG>,
1542            CamlPolyComm<CamlG>,
1543            CamlPolyComm<CamlG>,
1544            CamlPolyComm<CamlG>,
1545            CamlPolyComm<CamlG>,
1546            CamlPolyComm<CamlG>,
1547            CamlPolyComm<CamlG>,
1548            CamlPolyComm<CamlG>,
1549            CamlPolyComm<CamlG>,
1550        ),
1551        pub z_comm: CamlPolyComm<CamlG>,
1552        pub t_comm: CamlPolyComm<CamlG>,
1553        pub lookup: Option<CamlLookupCommitments<CamlG>>,
1554    }
1555
1556    // These implementations are handy for conversions such as:
1557    // InternalType <-> Ocaml::Value
1558    //
1559    // It does this by hiding the required middle conversion step:
1560    // InternalType <-> CamlInternalType <-> Ocaml::Value
1561    //
1562    // Note that some conversions are not always possible to shorten,
1563    // because we don't always know how to convert the types.
1564    // For example, to implement the conversion
1565    // ProverCommitments<G> -> CamlProverCommitments<CamlG>
1566    // we need to know how to convert G to CamlG.
1567    // we don't know that information, unless we implemented some trait (e.g. ToCaml)
1568    // we can do that, but instead we implemented the From trait for the reverse
1569    // operations (From<G> for CamlG).
1570    // it reduces the complexity, but forces us to do the conversion in two
1571    // phases instead of one.
1572
1573    //
1574    // CamlLookupCommitments<CamlG> <-> LookupCommitments<G>
1575    //
1576
1577    impl<G, CamlG> From<LookupCommitments<G>> for CamlLookupCommitments<CamlG>
1578    where
1579        G: AffineRepr,
1580        CamlPolyComm<CamlG>: From<PolyComm<G>>,
1581    {
1582        fn from(
1583            LookupCommitments {
1584                aggreg,
1585                sorted,
1586                runtime,
1587            }: LookupCommitments<G>,
1588        ) -> Self {
1589            Self {
1590                aggreg: aggreg.into(),
1591                sorted: sorted.into_iter().map(Into::into).collect(),
1592                runtime: runtime.map(Into::into),
1593            }
1594        }
1595    }
1596
1597    impl<G, CamlG> From<CamlLookupCommitments<CamlG>> for LookupCommitments<G>
1598    where
1599        G: AffineRepr,
1600        PolyComm<G>: From<CamlPolyComm<CamlG>>,
1601    {
1602        fn from(
1603            CamlLookupCommitments {
1604                aggreg,
1605                sorted,
1606                runtime,
1607            }: CamlLookupCommitments<CamlG>,
1608        ) -> LookupCommitments<G> {
1609            LookupCommitments {
1610                aggreg: aggreg.into(),
1611                sorted: sorted.into_iter().map(Into::into).collect(),
1612                runtime: runtime.map(Into::into),
1613            }
1614        }
1615    }
1616
1617    //
1618    // CamlProverCommitments<CamlG> <-> ProverCommitments<G>
1619    //
1620
1621    impl<G, CamlG> From<ProverCommitments<G>> for CamlProverCommitments<CamlG>
1622    where
1623        G: AffineRepr,
1624        CamlPolyComm<CamlG>: From<PolyComm<G>>,
1625    {
1626        fn from(prover_comm: ProverCommitments<G>) -> Self {
1627            let [w_comm0, w_comm1, w_comm2, w_comm3, w_comm4, w_comm5, w_comm6, w_comm7, w_comm8, w_comm9, w_comm10, w_comm11, w_comm12, w_comm13, w_comm14] =
1628                prover_comm.w_comm;
1629            Self {
1630                w_comm: (
1631                    w_comm0.into(),
1632                    w_comm1.into(),
1633                    w_comm2.into(),
1634                    w_comm3.into(),
1635                    w_comm4.into(),
1636                    w_comm5.into(),
1637                    w_comm6.into(),
1638                    w_comm7.into(),
1639                    w_comm8.into(),
1640                    w_comm9.into(),
1641                    w_comm10.into(),
1642                    w_comm11.into(),
1643                    w_comm12.into(),
1644                    w_comm13.into(),
1645                    w_comm14.into(),
1646                ),
1647                z_comm: prover_comm.z_comm.into(),
1648                t_comm: prover_comm.t_comm.into(),
1649                lookup: prover_comm.lookup.map(Into::into),
1650            }
1651        }
1652    }
1653
1654    impl<G, CamlG> From<CamlProverCommitments<CamlG>> for ProverCommitments<G>
1655    where
1656        G: AffineRepr,
1657        PolyComm<G>: From<CamlPolyComm<CamlG>>,
1658    {
1659        fn from(caml_prover_comm: CamlProverCommitments<CamlG>) -> ProverCommitments<G> {
1660            let (
1661                w_comm0,
1662                w_comm1,
1663                w_comm2,
1664                w_comm3,
1665                w_comm4,
1666                w_comm5,
1667                w_comm6,
1668                w_comm7,
1669                w_comm8,
1670                w_comm9,
1671                w_comm10,
1672                w_comm11,
1673                w_comm12,
1674                w_comm13,
1675                w_comm14,
1676            ) = caml_prover_comm.w_comm;
1677            ProverCommitments {
1678                w_comm: [
1679                    w_comm0.into(),
1680                    w_comm1.into(),
1681                    w_comm2.into(),
1682                    w_comm3.into(),
1683                    w_comm4.into(),
1684                    w_comm5.into(),
1685                    w_comm6.into(),
1686                    w_comm7.into(),
1687                    w_comm8.into(),
1688                    w_comm9.into(),
1689                    w_comm10.into(),
1690                    w_comm11.into(),
1691                    w_comm12.into(),
1692                    w_comm13.into(),
1693                    w_comm14.into(),
1694                ],
1695                z_comm: caml_prover_comm.z_comm.into(),
1696                t_comm: caml_prover_comm.t_comm.into(),
1697                lookup: caml_prover_comm.lookup.map(Into::into),
1698            }
1699        }
1700    }
1701
1702    //
1703    // ProverProof<G> <-> CamlProofWithPublic<CamlG, CamlF>
1704    //
1705
1706    impl<G, CamlG, CamlF> From<(ProverProof<G, OpeningProof<G>>, Vec<G::ScalarField>)>
1707        for CamlProofWithPublic<CamlG, CamlF>
1708    where
1709        G: AffineRepr,
1710        CamlG: From<G>,
1711        CamlF: From<G::ScalarField>,
1712    {
1713        fn from(pp: (ProverProof<G, OpeningProof<G>>, Vec<G::ScalarField>)) -> Self {
1714            let (public_evals, evals) = pp.0.evals.into();
1715            CamlProofWithPublic {
1716                public_evals,
1717                proof: CamlProverProof {
1718                    commitments: pp.0.commitments.into(),
1719                    proof: pp.0.proof.into(),
1720                    evals,
1721                    ft_eval1: pp.0.ft_eval1.into(),
1722                    public: pp.1.into_iter().map(Into::into).collect(),
1723                    prev_challenges: pp.0.prev_challenges.into_iter().map(Into::into).collect(),
1724                },
1725            }
1726        }
1727    }
1728
1729    impl<G, CamlG, CamlF> From<CamlProofWithPublic<CamlG, CamlF>>
1730        for (ProverProof<G, OpeningProof<G>>, Vec<G::ScalarField>)
1731    where
1732        CamlF: Clone,
1733        G: AffineRepr + From<CamlG>,
1734        G::ScalarField: From<CamlF>,
1735    {
1736        fn from(
1737            caml_pp: CamlProofWithPublic<CamlG, CamlF>,
1738        ) -> (ProverProof<G, OpeningProof<G>>, Vec<G::ScalarField>) {
1739            let CamlProofWithPublic {
1740                public_evals,
1741                proof: caml_pp,
1742            } = caml_pp;
1743            let proof = ProverProof {
1744                commitments: caml_pp.commitments.into(),
1745                proof: caml_pp.proof.into(),
1746                evals: (public_evals, caml_pp.evals).into(),
1747                ft_eval1: caml_pp.ft_eval1.into(),
1748                prev_challenges: caml_pp
1749                    .prev_challenges
1750                    .into_iter()
1751                    .map(Into::into)
1752                    .collect(),
1753            };
1754
1755            (proof, caml_pp.public.into_iter().map(Into::into).collect())
1756        }
1757    }
1758}