o1vm/pickles/
verifier.rs

1use ark_ec::AffineRepr;
2use ark_ff::{Field, One, PrimeField, Zero};
3use rand::thread_rng;
4
5use kimchi::{
6    circuits::{
7        berkeley_columns::BerkeleyChallenges,
8        domains::EvaluationDomains,
9        expr::{ColumnEvaluations, Constants, Expr, ExprError, PolishToken},
10        gate::CurrOrNext,
11    },
12    curve::KimchiCurve,
13    groupmap::GroupMap,
14    plonk_sponge::FrSponge,
15    proof::PointEvaluations,
16};
17use mina_poseidon::{sponge::ScalarChallenge, FqSponge};
18use poly_commitment::{
19    commitment::{
20        absorb_commitment, combined_inner_product, BatchEvaluationProof, Evaluation, PolyComm,
21    },
22    ipa::OpeningProof,
23    OpenProof,
24};
25
26use super::{
27    column_env::{get_all_columns, RelationColumnType},
28    proof::{Proof, WitnessColumns},
29};
30use crate::{interpreters::mips::column::N_MIPS_SEL_COLS, E};
31use kimchi_msm::columns::Column;
32
33type CommitmentColumns<G> = WitnessColumns<PolyComm<G>, [PolyComm<G>; N_MIPS_SEL_COLS]>;
34type EvaluationColumns<F> = WitnessColumns<F, [F; N_MIPS_SEL_COLS]>;
35
36struct ColumnEval<'a, G: AffineRepr> {
37    commitment: &'a CommitmentColumns<G>,
38    zeta_eval: &'a EvaluationColumns<G::ScalarField>,
39    zeta_omega_eval: &'a EvaluationColumns<G::ScalarField>,
40}
41
42impl<G: AffineRepr> ColumnEvaluations<G::ScalarField> for ColumnEval<'_, G> {
43    type Column = Column<RelationColumnType>;
44    fn evaluate(
45        &self,
46        col: Self::Column,
47    ) -> Result<PointEvaluations<G::ScalarField>, ExprError<Self::Column>> {
48        let ColumnEval {
49            commitment: _,
50            zeta_eval,
51            zeta_omega_eval,
52        } = self;
53        if let Some(&zeta) = zeta_eval.get_column(&col) {
54            if let Some(&zeta_omega) = zeta_omega_eval.get_column(&col) {
55                Ok(PointEvaluations { zeta, zeta_omega })
56            } else {
57                Err(ExprError::MissingEvaluation(col, CurrOrNext::Next))
58            }
59        } else {
60            Err(ExprError::MissingEvaluation(col, CurrOrNext::Curr))
61        }
62    }
63}
64
65pub fn verify<
66    G: KimchiCurve,
67    EFqSponge: Clone + FqSponge<G::BaseField, G, G::ScalarField>,
68    EFrSponge: FrSponge<G::ScalarField>,
69>(
70    domain: EvaluationDomains<G::ScalarField>,
71    srs: &<OpeningProof<G> as OpenProof<G>>::SRS,
72    constraints: &[E<G::ScalarField>],
73    proof: &Proof<G>,
74) -> bool
75where
76    <G as AffineRepr>::BaseField: PrimeField,
77{
78    let Proof {
79        commitments,
80        zeta_evaluations,
81        zeta_omega_evaluations,
82        quotient_commitment,
83        quotient_evaluations,
84        opening_proof,
85    } = proof;
86
87    ////////////////////////////////////////////////////////////////////////////
88    // TODO :  public inputs
89    ////////////////////////////////////////////////////////////////////////////
90
91    ////////////////////////////////////////////////////////////////////////////
92    // Absorbing all the commitments to the columns
93    ////////////////////////////////////////////////////////////////////////////
94
95    let mut fq_sponge = EFqSponge::new(G::other_curve_sponge_params());
96    for comm in commitments.scratch.iter() {
97        absorb_commitment(&mut fq_sponge, comm)
98    }
99    for comm in commitments.scratch_inverse.iter() {
100        absorb_commitment(&mut fq_sponge, comm)
101    }
102    for comm in commitments.lookup_state.iter() {
103        absorb_commitment(&mut fq_sponge, comm)
104    }
105    absorb_commitment(&mut fq_sponge, &commitments.instruction_counter);
106    absorb_commitment(&mut fq_sponge, &commitments.error);
107    for comm in commitments.selector.iter() {
108        absorb_commitment(&mut fq_sponge, comm)
109    }
110
111    // Sample α with the Fq-Sponge.
112    let alpha = fq_sponge.challenge();
113
114    ////////////////////////////////////////////////////////////////////////////
115    // Quotient polynomial
116    ////////////////////////////////////////////////////////////////////////////
117
118    absorb_commitment(&mut fq_sponge, quotient_commitment);
119
120    // -- Preparing for opening proof verification
121    let zeta_chal = ScalarChallenge(fq_sponge.challenge());
122    let (_, endo_r) = G::endos();
123    let zeta = zeta_chal.to_field(endo_r);
124    let omega = domain.d1.group_gen;
125    let zeta_omega = zeta * omega;
126
127    let column_eval = ColumnEval {
128        commitment: commitments,
129        zeta_eval: zeta_evaluations,
130        zeta_omega_eval: zeta_omega_evaluations,
131    };
132
133    // -- Absorb all commitments_and_evaluations
134    let fq_sponge_before_commitments_and_evaluations = fq_sponge.clone();
135    let mut fr_sponge = EFrSponge::new(G::sponge_params());
136    fr_sponge.absorb(&fq_sponge.digest());
137
138    for (zeta_eval, zeta_omega_eval) in zeta_evaluations
139        .scratch
140        .iter()
141        .zip(zeta_omega_evaluations.scratch.iter())
142    {
143        fr_sponge.absorb(zeta_eval);
144        fr_sponge.absorb(zeta_omega_eval);
145    }
146    for (zeta_eval, zeta_omega_eval) in zeta_evaluations
147        .scratch_inverse
148        .iter()
149        .zip(zeta_omega_evaluations.scratch_inverse.iter())
150    {
151        fr_sponge.absorb(zeta_eval);
152        fr_sponge.absorb(zeta_omega_eval);
153    }
154    for (zeta_eval, zeta_omega_eval) in zeta_evaluations
155        .lookup_state
156        .iter()
157        .zip(zeta_omega_evaluations.lookup_state.iter())
158    {
159        fr_sponge.absorb(zeta_eval);
160        fr_sponge.absorb(zeta_omega_eval);
161    }
162    fr_sponge.absorb(&zeta_evaluations.instruction_counter);
163    fr_sponge.absorb(&zeta_omega_evaluations.instruction_counter);
164    fr_sponge.absorb(&zeta_evaluations.error);
165    fr_sponge.absorb(&zeta_omega_evaluations.error);
166    for (zeta_eval, zeta_omega_eval) in zeta_evaluations
167        .selector
168        .iter()
169        .zip(zeta_omega_evaluations.selector.iter())
170    {
171        fr_sponge.absorb(zeta_eval);
172        fr_sponge.absorb(zeta_omega_eval);
173    }
174    for (quotient_zeta_eval, quotient_zeta_omega_eval) in quotient_evaluations
175        .zeta
176        .iter()
177        .zip(quotient_evaluations.zeta_omega.iter())
178    {
179        fr_sponge.absorb(quotient_zeta_eval);
180        fr_sponge.absorb(quotient_zeta_omega_eval);
181    }
182
183    // FIXME: use a proper Challenge structure
184    let challenges = BerkeleyChallenges {
185        alpha,
186        // No permutation argument for the moment
187        beta: G::ScalarField::zero(),
188        gamma: G::ScalarField::zero(),
189        // No lookup for the moment
190        joint_combiner: G::ScalarField::zero(),
191    };
192    let (_, endo_r) = G::endos();
193
194    let constants = Constants {
195        endo_coefficient: *endo_r,
196        mds: &G::sponge_params().mds,
197        zk_rows: 0,
198    };
199
200    let combined_expr =
201        Expr::combine_constraints(0..(constraints.len() as u32), constraints.to_vec());
202
203    let numerator_zeta = PolishToken::evaluate(
204        combined_expr.to_polish().as_slice(),
205        domain.d1,
206        zeta,
207        &column_eval,
208        &constants,
209        &challenges,
210    )
211    .unwrap_or_else(|_| panic!("Could not evaluate quotient polynomial at zeta"));
212
213    let v_chal = fr_sponge.challenge();
214    let v = v_chal.to_field(endo_r);
215    let u_chal = fr_sponge.challenge();
216    let u = u_chal.to_field(endo_r);
217
218    let mut evaluations: Vec<_> = get_all_columns(column_eval.commitment.lookup_state.len())
219        .into_iter()
220        .map(|column| {
221            let commitment = column_eval
222                .commitment
223                .get_column(&column)
224                .unwrap_or_else(|| panic!("Could not get `commitment` for `Evaluation`"))
225                .clone();
226
227            let evaluations = column_eval
228                .evaluate(column)
229                .unwrap_or_else(|_| panic!("Could not get `evaluations` for `Evaluation`"));
230
231            Evaluation {
232                commitment,
233                evaluations: vec![vec![evaluations.zeta], vec![evaluations.zeta_omega]],
234            }
235        })
236        .collect();
237
238    evaluations.push(Evaluation {
239        commitment: proof.quotient_commitment.clone(),
240        evaluations: vec![
241            quotient_evaluations.zeta.clone(),
242            quotient_evaluations.zeta_omega.clone(),
243        ],
244    });
245
246    let combined_inner_product = {
247        let es: Vec<_> = evaluations
248            .iter()
249            .map(|Evaluation { evaluations, .. }| evaluations.clone())
250            .collect();
251
252        combined_inner_product(&v, &u, es.as_slice())
253    };
254
255    let batch = BatchEvaluationProof {
256        sponge: fq_sponge_before_commitments_and_evaluations,
257        evaluations,
258        evaluation_points: vec![zeta, zeta_omega],
259        polyscale: v,
260        evalscale: u,
261        opening: opening_proof,
262        combined_inner_product,
263    };
264
265    let group_map = G::Map::setup();
266
267    // Check the actual quotient works.
268    let (quotient_zeta, _) = quotient_evaluations.zeta.iter().fold(
269        (G::ScalarField::zero(), G::ScalarField::one()),
270        |(res, zeta_i_n), chunk| {
271            let res = res + zeta_i_n * chunk;
272            let zeta_i_n = zeta_i_n * zeta.pow([domain.d1.size]);
273            (res, zeta_i_n)
274        },
275    );
276    (quotient_zeta == numerator_zeta / (zeta.pow([domain.d1.size]) - G::ScalarField::one()))
277        && OpeningProof::verify(srs, &group_map, &mut [batch], &mut thread_rng())
278}
o1vm/pickles/verifier.rs

o1vm/pickles/
verifier.rs
