mina_tree/proofs/
verification.rs

1use std::rc::Rc;
2
3use ark_poly::{EvaluationDomain, Radix2EvaluationDomain};
4use ark_serialize::Write;
5use itertools::Itertools;
6use mina_p2p_messages::bigint::InvalidBigInt;
7use poly_commitment::ipa::SRS;
8
9use crate::{
10    proofs::{
11        accumulator_check,
12        step::{expand_deferred, StatementProofState},
13        unfinalized::AllEvals,
14        verifiers::make_zkapp_verifier_index,
15        wrap::Domain,
16        BACKEND_TICK_ROUNDS_N,
17    },
18    scan_state::{
19        protocol_state::MinaHash,
20        scan_state::transaction_snark::{SokDigest, Statement},
21        transaction_logic::{local_state::LazyValue, zkapp_statement::ZkappStatement},
22    },
23    VerificationKey,
24};
25
26use super::{
27    block::ProtocolState,
28    field::FieldWitness,
29    public_input::plonk_checks::make_shifts,
30    step::{step_verifier::PlonkDomain, ExpandDeferredParams},
31    to_field_elements::ToFieldElements,
32    transaction::{InnerCurve, PlonkVerificationKeyEvals},
33    util::{extract_bulletproof, extract_polynomial_commitment, two_u64_to_field},
34    wrap::expand_feature_flags,
35    ProverProof, VerifierIndex,
36};
37use kimchi::{
38    circuits::{expr::RowOffset, wires::PERMUTS},
39    error::VerifyError,
40    mina_curves::pasta::Pallas,
41    proof::{PointEvaluations, ProofEvaluations},
42};
43use mina_curves::pasta::{Fp, Fq, Vesta};
44use mina_p2p_messages::{
45    bigint::BigInt,
46    binprot::BinProtWrite,
47    v2::{
48        self, CompositionTypesDigestConstantStableV1, MinaBlockHeaderStableV2,
49        PicklesProofProofsVerified2ReprStableV2,
50        PicklesProofProofsVerified2ReprStableV2MessagesForNextStepProof,
51        PicklesProofProofsVerified2ReprStableV2MessagesForNextWrapProof,
52        PicklesProofProofsVerified2ReprStableV2PrevEvalsEvalsEvals,
53        PicklesProofProofsVerified2ReprStableV2StatementProofStateDeferredValuesPlonkFeatureFlags,
54        TransactionSnarkProofStableV2,
55    },
56};
57use mina_poseidon::pasta::FULL_ROUNDS;
58
59use super::prover::make_padded_proof_from_p2p;
60
61use super::public_input::{
62    messages::{MessagesForNextStepProof, MessagesForNextWrapProof},
63    plonk_checks::{PlonkMinimal, ScalarsEnv},
64    prepared_statement::{DeferredValues, PreparedStatement, ProofState},
65};
66
67#[cfg(target_family = "wasm")]
68#[cfg(test)]
69mod wasm {
70    use wasm_bindgen_test::*;
71    wasm_bindgen_test_configure!(run_in_browser);
72}
73
74fn validate_feature_flags(
75    feature_flags: &PicklesProofProofsVerified2ReprStableV2StatementProofStateDeferredValuesPlonkFeatureFlags,
76    evals: &PicklesProofProofsVerified2ReprStableV2PrevEvalsEvalsEvals,
77) -> bool {
78    let PicklesProofProofsVerified2ReprStableV2PrevEvalsEvalsEvals {
79        w: _,
80        coefficients: _,
81        z: _,
82        s: _,
83        generic_selector: _,
84        poseidon_selector: _,
85        complete_add_selector: _,
86        mul_selector: _,
87        emul_selector: _,
88        endomul_scalar_selector: _,
89        range_check0_selector,
90        range_check1_selector,
91        foreign_field_add_selector,
92        foreign_field_mul_selector,
93        xor_selector,
94        rot_selector,
95        lookup_aggregation,
96        lookup_table,
97        lookup_sorted,
98        runtime_lookup_table,
99        runtime_lookup_table_selector,
100        xor_lookup_selector,
101        lookup_gate_lookup_selector,
102        range_check_lookup_selector,
103        foreign_field_mul_lookup_selector,
104    } = evals;
105
106    fn enable_if<T>(x: &Option<T>, flag: bool) -> bool {
107        x.is_some() == flag
108    }
109
110    let f = feature_flags;
111    let range_check_lookup = f.range_check0 || f.range_check1 || f.rot;
112    let lookups_per_row_4 = f.xor || range_check_lookup || f.foreign_field_mul;
113    let lookups_per_row_3 = lookups_per_row_4 || f.lookup;
114    let lookups_per_row_2 = lookups_per_row_3;
115
116    [
117        enable_if(range_check0_selector, f.range_check0),
118        enable_if(range_check1_selector, f.range_check1),
119        enable_if(foreign_field_add_selector, f.foreign_field_add),
120        enable_if(foreign_field_mul_selector, f.foreign_field_mul),
121        enable_if(xor_selector, f.xor),
122        enable_if(rot_selector, f.rot),
123        enable_if(lookup_aggregation, lookups_per_row_2),
124        enable_if(lookup_table, lookups_per_row_2),
125        lookup_sorted.iter().enumerate().fold(true, |acc, (i, x)| {
126            let flag = match i {
127                0..=2 => lookups_per_row_2,
128                3 => lookups_per_row_3,
129                4 => lookups_per_row_4,
130                _ => panic!(),
131            };
132            acc && enable_if(x, flag)
133        }),
134        enable_if(runtime_lookup_table, f.runtime_tables),
135        enable_if(runtime_lookup_table_selector, f.runtime_tables),
136        enable_if(xor_lookup_selector, f.xor),
137        enable_if(lookup_gate_lookup_selector, f.lookup),
138        enable_if(range_check_lookup_selector, range_check_lookup),
139        enable_if(foreign_field_mul_lookup_selector, f.foreign_field_mul),
140    ]
141    .iter()
142    .all(|b| *b)
143}
144
145pub fn prev_evals_from_p2p<F: FieldWitness>(
146    evals: &PicklesProofProofsVerified2ReprStableV2PrevEvalsEvalsEvals,
147) -> Result<ProofEvaluations<PointEvaluations<Vec<F>>>, InvalidBigInt> {
148    let PicklesProofProofsVerified2ReprStableV2PrevEvalsEvalsEvals {
149        w,
150        coefficients,
151        z,
152        s,
153        generic_selector,
154        poseidon_selector,
155        complete_add_selector,
156        mul_selector,
157        emul_selector,
158        endomul_scalar_selector,
159        range_check0_selector,
160        range_check1_selector,
161        foreign_field_add_selector,
162        foreign_field_mul_selector,
163        xor_selector,
164        rot_selector,
165        lookup_aggregation,
166        lookup_table,
167        lookup_sorted,
168        runtime_lookup_table,
169        runtime_lookup_table_selector,
170        xor_lookup_selector,
171        lookup_gate_lookup_selector,
172        range_check_lookup_selector,
173        foreign_field_mul_lookup_selector,
174    } = evals;
175
176    fn of<'a, F: FieldWitness, I: IntoIterator<Item = &'a BigInt>>(
177        zeta: I,
178        zeta_omega: I,
179    ) -> Result<PointEvaluations<Vec<F>>, InvalidBigInt> {
180        Ok(PointEvaluations {
181            zeta: zeta
182                .into_iter()
183                .map(BigInt::to_field)
184                .collect::<Result<_, _>>()?,
185            zeta_omega: zeta_omega
186                .into_iter()
187                .map(BigInt::to_field)
188                .collect::<Result<_, _>>()?,
189        })
190    }
191
192    let of = |(zeta, zeta_omega): &(_, _)| -> Result<PointEvaluations<Vec<F>>, _> {
193        of(zeta, zeta_omega)
194    };
195    let of_opt = |v: &Option<(_, _)>| match v.as_ref() {
196        Some(v) => Ok(Some(of(v)?)),
197        None => Ok(None),
198    };
199
200    Ok(ProofEvaluations {
201        public: None,
202        w: crate::try_array_into_with(w, of)?,
203        z: of(z)?,
204        s: crate::try_array_into_with(s, of)?,
205        coefficients: crate::try_array_into_with(coefficients, of)?,
206        generic_selector: of(generic_selector)?,
207        poseidon_selector: of(poseidon_selector)?,
208        complete_add_selector: of(complete_add_selector)?,
209        mul_selector: of(mul_selector)?,
210        emul_selector: of(emul_selector)?,
211        endomul_scalar_selector: of(endomul_scalar_selector)?,
212        range_check0_selector: of_opt(range_check0_selector)?,
213        range_check1_selector: of_opt(range_check1_selector)?,
214        foreign_field_add_selector: of_opt(foreign_field_add_selector)?,
215        foreign_field_mul_selector: of_opt(foreign_field_mul_selector)?,
216        xor_selector: of_opt(xor_selector)?,
217        rot_selector: of_opt(rot_selector)?,
218        lookup_aggregation: of_opt(lookup_aggregation)?,
219        lookup_table: of_opt(lookup_table)?,
220        lookup_sorted: crate::try_array_into_with(lookup_sorted, of_opt)?,
221        runtime_lookup_table: of_opt(runtime_lookup_table)?,
222        runtime_lookup_table_selector: of_opt(runtime_lookup_table_selector)?,
223        xor_lookup_selector: of_opt(xor_lookup_selector)?,
224        lookup_gate_lookup_selector: of_opt(lookup_gate_lookup_selector)?,
225        range_check_lookup_selector: of_opt(range_check_lookup_selector)?,
226        foreign_field_mul_lookup_selector: of_opt(foreign_field_mul_lookup_selector)?,
227    })
228}
229
230pub fn prev_evals_to_p2p(
231    evals: &ProofEvaluations<PointEvaluations<Vec<Fp>>>,
232) -> PicklesProofProofsVerified2ReprStableV2PrevEvalsEvalsEvals {
233    let ProofEvaluations {
234        public: _,
235        w,
236        coefficients,
237        z,
238        s,
239        generic_selector,
240        poseidon_selector,
241        complete_add_selector,
242        mul_selector,
243        emul_selector,
244        endomul_scalar_selector,
245        range_check0_selector,
246        range_check1_selector,
247        foreign_field_add_selector,
248        foreign_field_mul_selector,
249        xor_selector,
250        rot_selector,
251        lookup_aggregation,
252        lookup_table,
253        lookup_sorted,
254        runtime_lookup_table,
255        runtime_lookup_table_selector,
256        xor_lookup_selector,
257        lookup_gate_lookup_selector,
258        range_check_lookup_selector,
259        foreign_field_mul_lookup_selector,
260    } = evals;
261
262    use mina_p2p_messages::pseq::PaddedSeq;
263
264    let of = |PointEvaluations { zeta, zeta_omega }: &PointEvaluations<Vec<Fp>>| {
265        (
266            zeta.iter().map(Into::into).collect(),
267            zeta_omega.iter().map(Into::into).collect(),
268        )
269    };
270
271    let of_opt = |v: &Option<PointEvaluations<Vec<Fp>>>| v.as_ref().map(of);
272
273    PicklesProofProofsVerified2ReprStableV2PrevEvalsEvalsEvals {
274        w: PaddedSeq(w.each_ref().map(of)),
275        z: of(z),
276        s: PaddedSeq(s.each_ref().map(of)),
277        coefficients: PaddedSeq(coefficients.each_ref().map(of)),
278        generic_selector: of(generic_selector),
279        poseidon_selector: of(poseidon_selector),
280        complete_add_selector: of(complete_add_selector),
281        mul_selector: of(mul_selector),
282        emul_selector: of(emul_selector),
283        endomul_scalar_selector: of(endomul_scalar_selector),
284        range_check0_selector: of_opt(range_check0_selector),
285        range_check1_selector: of_opt(range_check1_selector),
286        foreign_field_add_selector: of_opt(foreign_field_add_selector),
287        foreign_field_mul_selector: of_opt(foreign_field_mul_selector),
288        xor_selector: of_opt(xor_selector),
289        rot_selector: of_opt(rot_selector),
290        lookup_aggregation: of_opt(lookup_aggregation),
291        lookup_table: of_opt(lookup_table),
292        lookup_sorted: PaddedSeq(lookup_sorted.each_ref().map(of_opt)),
293        runtime_lookup_table: of_opt(runtime_lookup_table),
294        runtime_lookup_table_selector: of_opt(runtime_lookup_table_selector),
295        xor_lookup_selector: of_opt(xor_lookup_selector),
296        lookup_gate_lookup_selector: of_opt(lookup_gate_lookup_selector),
297        range_check_lookup_selector: of_opt(range_check_lookup_selector),
298        foreign_field_mul_lookup_selector: of_opt(foreign_field_mul_lookup_selector),
299    }
300}
301
302struct LimitedDomain<F: FieldWitness> {
303    domain: Radix2EvaluationDomain<F>,
304    shifts: kimchi::circuits::polynomials::permutation::Shifts<F>,
305}
306
307impl<F: FieldWitness> PlonkDomain<F> for LimitedDomain<F> {
308    fn vanishing_polynomial(&self, _x: F, _w: &mut super::witness::Witness<F>) -> F {
309        unimplemented!() // Unused during proof verification
310    }
311    fn generator(&self) -> F {
312        self.domain.group_gen
313    }
314    fn shifts(&self) -> &[F; PERMUTS] {
315        self.shifts.shifts()
316    }
317    fn log2_size(&self) -> u64 {
318        unimplemented!() // Unused during proof verification
319    }
320}
321
322// TODO: `domain_log2` and `srs_length_log2` might be the same here ? Remove one or the other
323pub fn make_scalars_env<F: FieldWitness, const NLIMB: usize>(
324    minimal: &PlonkMinimal<F, NLIMB>,
325    domain_log2: u8,
326    srs_length_log2: u64,
327    zk_rows: u64,
328) -> ScalarsEnv<F> {
329    let domain: Radix2EvaluationDomain<F> =
330        Radix2EvaluationDomain::new(1 << domain_log2 as u64).unwrap();
331
332    let zeta_to_n_minus_1 = domain.evaluate_vanishing_polynomial(minimal.zeta);
333
334    let (
335        omega_to_zk_minus_1,
336        omega_to_zk,
337        omega_to_intermediate_powers,
338        omega_to_zk_plus_1,
339        omega_to_minus_1,
340    ) = {
341        let gen = domain.group_gen;
342        let omega_to_minus_1 = F::one() / gen;
343        let omega_to_minus_2 = omega_to_minus_1.square();
344        let (omega_to_intermediate_powers, omega_to_zk_plus_1) = {
345            let mut next_term = omega_to_minus_2;
346            let omega_to_intermediate_powers = (0..(zk_rows.checked_sub(3).unwrap()))
347                .map(|_| {
348                    let term = next_term;
349                    next_term = term * omega_to_minus_1;
350                    term
351                })
352                .collect::<Vec<_>>();
353            (omega_to_intermediate_powers, next_term)
354        };
355        let omega_to_zk = omega_to_zk_plus_1 * omega_to_minus_1;
356        let omega_to_zk_minus_1 = move || omega_to_zk * omega_to_minus_1;
357
358        (
359            omega_to_zk_minus_1,
360            omega_to_zk,
361            omega_to_intermediate_powers,
362            omega_to_zk_plus_1,
363            omega_to_minus_1,
364        )
365    };
366
367    let zk_polynomial = (minimal.zeta - omega_to_minus_1)
368        * (minimal.zeta - omega_to_zk_plus_1)
369        * (minimal.zeta - omega_to_zk);
370
371    let shifts = make_shifts(&domain);
372    let domain = Rc::new(LimitedDomain { domain, shifts });
373
374    let vanishes_on_zero_knowledge_and_previous_rows = match minimal.joint_combiner {
375        None => F::one(),
376        Some(_) => omega_to_intermediate_powers.iter().fold(
377            // init
378            zk_polynomial * (minimal.zeta - omega_to_zk_minus_1()),
379            // f
380            |acc, omega_pow| acc * (minimal.zeta - omega_pow),
381        ),
382    };
383
384    let zeta_clone = minimal.zeta;
385    let zeta_to_srs_length =
386        LazyValue::make(move |_| (0..srs_length_log2).fold(zeta_clone, |acc, _| acc * acc));
387
388    let feature_flags = minimal
389        .joint_combiner
390        .map(|_| expand_feature_flags::<F>(&minimal.feature_flags.to_boolean()));
391
392    let unnormalized_lagrange_basis = match minimal.joint_combiner {
393        None => None,
394        Some(_) => {
395            use crate::proofs::witness::Witness;
396
397            let zeta = minimal.zeta;
398            let generator = domain.generator();
399            let omega_to_zk_minus_1_clone = omega_to_zk_minus_1();
400            let fun: Box<dyn Fn(RowOffset, &mut Witness<F>) -> F> =
401                Box::new(move |i: RowOffset, w: &mut Witness<F>| {
402                    let w_to_i = match (i.zk_rows, i.offset) {
403                        (false, 0) => F::one(),
404                        (false, 1) => generator,
405                        (false, -1) => omega_to_minus_1,
406                        (false, -2) => omega_to_zk_plus_1,
407                        (false, -3) | (true, 0) => omega_to_zk,
408                        (true, -1) => omega_to_zk_minus_1_clone,
409                        _ => todo!(),
410                    };
411                    crate::proofs::field::field::div_by_inv(zeta_to_n_minus_1, zeta - w_to_i, w)
412                });
413            Some(fun)
414        }
415    };
416
417    ScalarsEnv {
418        zk_polynomial,
419        zeta_to_n_minus_1,
420        srs_length_log2,
421        domain,
422        omega_to_minus_zk_rows: omega_to_zk,
423        feature_flags,
424        unnormalized_lagrange_basis,
425        vanishes_on_zero_knowledge_and_previous_rows,
426        zeta_to_srs_length,
427    }
428}
429
430fn get_message_for_next_step_proof<'a, AppState>(
431    messages_for_next_step_proof: &PicklesProofProofsVerified2ReprStableV2MessagesForNextStepProof,
432    commitments: &'a PlonkVerificationKeyEvals<Fp>,
433    app_state: &'a AppState,
434) -> Result<MessagesForNextStepProof<'a, AppState>, InvalidBigInt>
435where
436    AppState: ToFieldElements<Fp>,
437{
438    let PicklesProofProofsVerified2ReprStableV2MessagesForNextStepProof {
439        app_state: _, // unused
440        challenge_polynomial_commitments,
441        old_bulletproof_challenges,
442    } = messages_for_next_step_proof;
443
444    let challenge_polynomial_commitments: Vec<InnerCurve<Fp>> =
445        extract_polynomial_commitment(challenge_polynomial_commitments)?;
446    let old_bulletproof_challenges: Vec<[Fp; 16]> = extract_bulletproof(old_bulletproof_challenges);
447    let dlog_plonk_index = commitments;
448
449    Ok(MessagesForNextStepProof {
450        app_state,
451        dlog_plonk_index,
452        challenge_polynomial_commitments,
453        old_bulletproof_challenges,
454    })
455}
456
457fn get_message_for_next_wrap_proof(
458    PicklesProofProofsVerified2ReprStableV2MessagesForNextWrapProof {
459        challenge_polynomial_commitment,
460        old_bulletproof_challenges,
461    }: &PicklesProofProofsVerified2ReprStableV2MessagesForNextWrapProof,
462) -> Result<MessagesForNextWrapProof, InvalidBigInt> {
463    let challenge_polynomial_commitments: Vec<InnerCurve<Fq>> =
464        extract_polynomial_commitment(std::slice::from_ref(challenge_polynomial_commitment))?;
465
466    let old_bulletproof_challenges: Vec<[Fq; 15]> = extract_bulletproof(&[
467        old_bulletproof_challenges[0].0.clone(),
468        old_bulletproof_challenges[1].0.clone(),
469    ]);
470
471    Ok(MessagesForNextWrapProof {
472        challenge_polynomial_commitment: challenge_polynomial_commitments[0].clone(),
473        old_bulletproof_challenges,
474    })
475}
476
477fn get_prepared_statement<AppState>(
478    message_for_next_step_proof: &MessagesForNextStepProof<AppState>,
479    message_for_next_wrap_proof: &MessagesForNextWrapProof,
480    deferred_values: DeferredValues<Fp>,
481    sponge_digest_before_evaluations: &CompositionTypesDigestConstantStableV1,
482) -> PreparedStatement
483where
484    AppState: ToFieldElements<Fp>,
485{
486    let digest = sponge_digest_before_evaluations;
487    let sponge_digest_before_evaluations: [u64; 4] = digest.each_ref().map(|v| v.as_u64());
488
489    PreparedStatement {
490        proof_state: ProofState {
491            deferred_values,
492            sponge_digest_before_evaluations,
493            messages_for_next_wrap_proof: message_for_next_wrap_proof.hash(),
494        },
495        messages_for_next_step_proof: message_for_next_step_proof.hash(),
496    }
497}
498
499fn verify_with(
500    verifier_index: &VerifierIndex<Fq>,
501    proof: &ProverProof<Fq>,
502    public_input: &[Fq],
503) -> Result<(), VerifyError> {
504    use kimchi::{groupmap::GroupMap, mina_curves::pasta::PallasParameters};
505    use mina_poseidon::sponge::{DefaultFqSponge, DefaultFrSponge};
506    use poly_commitment::ipa::OpeningProof;
507
508    type SpongeParams = mina_poseidon::constants::PlonkSpongeConstantsKimchi;
509    type EFqSponge = DefaultFqSponge<PallasParameters, SpongeParams, FULL_ROUNDS>;
510    type EFrSponge = DefaultFrSponge<Fq, SpongeParams, FULL_ROUNDS>;
511
512    let group_map = GroupMap::<Fp>::setup();
513
514    kimchi::verifier::verify::<
515        FULL_ROUNDS,
516        Pallas,
517        EFqSponge,
518        EFrSponge,
519        OpeningProof<Pallas, FULL_ROUNDS>,
520    >(&group_map, verifier_index, proof, public_input)
521}
522
523pub struct VerificationContext<'a> {
524    pub verifier_index: &'a VerifierIndex<Fq>,
525    pub proof: &'a ProverProof<Fq>,
526    pub public_input: &'a [Fq],
527}
528
529fn batch_verify(proofs: &[VerificationContext]) -> Result<(), VerifyError> {
530    use kimchi::{groupmap::GroupMap, mina_curves::pasta::PallasParameters, verifier::Context};
531    use mina_poseidon::sponge::{DefaultFqSponge, DefaultFrSponge};
532    use poly_commitment::ipa::OpeningProof;
533
534    type SpongeParams = mina_poseidon::constants::PlonkSpongeConstantsKimchi;
535    type EFqSponge = DefaultFqSponge<PallasParameters, SpongeParams, FULL_ROUNDS>;
536    type EFrSponge = DefaultFrSponge<Fq, SpongeParams, FULL_ROUNDS>;
537
538    let group_map = GroupMap::<Fp>::setup();
539    let proofs = proofs
540        .iter()
541        .map(|p| Context {
542            verifier_index: p.verifier_index,
543            proof: p.proof,
544            public_input: p.public_input,
545        })
546        .collect_vec();
547
548    kimchi::verifier::batch_verify::<
549        FULL_ROUNDS,
550        Pallas,
551        EFqSponge,
552        EFrSponge,
553        OpeningProof<Pallas, FULL_ROUNDS>,
554    >(&group_map, &proofs)
555}
556
557fn run_checks(
558    proof: &PicklesProofProofsVerified2ReprStableV2,
559    verifier_index: &VerifierIndex<Fq>,
560) -> bool {
561    let mut errors: Vec<String> = vec![];
562    let mut checks = |condition: bool, s: &str| {
563        if !condition {
564            errors.push(s.to_string())
565        }
566    };
567
568    let non_chunking = {
569        let PicklesProofProofsVerified2ReprStableV2PrevEvalsEvalsEvals {
570            w,
571            coefficients,
572            z,
573            s,
574            generic_selector,
575            poseidon_selector,
576            complete_add_selector,
577            mul_selector,
578            emul_selector,
579            endomul_scalar_selector,
580            range_check0_selector,
581            range_check1_selector,
582            foreign_field_add_selector,
583            foreign_field_mul_selector,
584            xor_selector,
585            rot_selector,
586            lookup_aggregation,
587            lookup_table,
588            lookup_sorted,
589            runtime_lookup_table,
590            runtime_lookup_table_selector,
591            xor_lookup_selector,
592            lookup_gate_lookup_selector,
593            range_check_lookup_selector,
594            foreign_field_mul_lookup_selector,
595        } = &proof.prev_evals.evals.evals;
596
597        let mut iter = w
598            .iter()
599            .chain(coefficients.iter())
600            .chain([z])
601            .chain(s.iter())
602            .chain([
603                generic_selector,
604                poseidon_selector,
605                complete_add_selector,
606                mul_selector,
607                emul_selector,
608                endomul_scalar_selector,
609            ])
610            .chain(range_check0_selector.iter())
611            .chain(range_check1_selector.iter())
612            .chain(foreign_field_add_selector.iter())
613            .chain(foreign_field_mul_selector.iter())
614            .chain(xor_selector.iter())
615            .chain(rot_selector.iter())
616            .chain(lookup_aggregation.iter())
617            .chain(lookup_table.iter())
618            .chain(lookup_sorted.iter().flatten())
619            .chain(runtime_lookup_table.iter())
620            .chain(runtime_lookup_table_selector.iter())
621            .chain(xor_lookup_selector.iter())
622            .chain(lookup_gate_lookup_selector.iter())
623            .chain(range_check_lookup_selector.iter())
624            .chain(foreign_field_mul_lookup_selector.iter());
625
626        iter.all(|(a, b)| a.len() <= 1 && b.len() <= 1)
627    };
628
629    checks(non_chunking, "only uses single chunks");
630
631    checks(
632        validate_feature_flags(
633            &proof
634                .statement
635                .proof_state
636                .deferred_values
637                .plonk
638                .feature_flags,
639            &proof.prev_evals.evals.evals,
640        ),
641        "feature flags are consistent with evaluations",
642    );
643
644    let branch_data = &proof.statement.proof_state.deferred_values.branch_data;
645    let step_domain: u8 = branch_data.domain_log2.as_u8();
646    let step_domain = Domain::Pow2RootsOfUnity(step_domain as u64);
647
648    checks(
649        step_domain.log2_size() as usize <= BACKEND_TICK_ROUNDS_N,
650        "domain size is small enough",
651    );
652
653    {
654        // TODO: Don't use hardcoded values
655        let all_possible_domains = [13, 14, 15];
656        let [greatest_wrap_domain, _, least_wrap_domain] = all_possible_domains;
657
658        let actual_wrap_domain = verifier_index.domain.log_size_of_group;
659        checks(
660            actual_wrap_domain <= least_wrap_domain,
661            "invalid actual_wrap_domain (least_wrap_domain)",
662        );
663        checks(
664            actual_wrap_domain >= greatest_wrap_domain,
665            "invalid actual_wrap_domain (greatest_wrap_domain)",
666        );
667    }
668
669    for e in &errors {
670        eprintln!("{:?}", e);
671    }
672
673    errors.is_empty()
674}
675
676fn compute_deferred_values(
677    proof: &PicklesProofProofsVerified2ReprStableV2,
678) -> anyhow::Result<DeferredValues<Fp>> {
679    let bulletproof_challenges: Vec<Fp> = proof
680        .statement
681        .proof_state
682        .deferred_values
683        .bulletproof_challenges
684        .iter()
685        .map(|chal| {
686            let prechallenge = &chal.prechallenge.inner;
687            let prechallenge: [u64; 2] = prechallenge.each_ref().map(|v| v.as_u64());
688            two_u64_to_field(&prechallenge)
689        })
690        .collect();
691
692    let deferred_values = {
693        let old_bulletproof_challenges: Vec<[Fp; 16]> = proof
694            .statement
695            .messages_for_next_step_proof
696            .old_bulletproof_challenges
697            .iter()
698            .map(|v| {
699                v.0.clone()
700                    .map(|v| two_u64_to_field(&v.prechallenge.inner.0.map(|v| v.as_u64())))
701            })
702            .collect();
703        let proof_state: StatementProofState = (&proof.statement.proof_state).try_into()?;
704        let evals: AllEvals<Fp> = (&proof.prev_evals).try_into()?;
705
706        let zk_rows = 3;
707        expand_deferred(ExpandDeferredParams {
708            evals: &evals,
709            old_bulletproof_challenges: &old_bulletproof_challenges,
710            proof_state: &proof_state,
711            zk_rows,
712        })?
713    };
714
715    Ok(DeferredValues {
716        bulletproof_challenges,
717        ..deferred_values
718    })
719}
720
721/// <https://github.com/MinaProtocol/mina/blob/4e0b324912017c3ff576704ee397ade3d9bda412/src/lib/pickles/verification_key.mli#L30>
722pub struct VK<'a> {
723    pub commitments: PlonkVerificationKeyEvals<Fp>,
724    pub index: &'a VerifierIndex<Fq>,
725    pub data: (), // Unused in proof verification
726}
727
728/// Verifies a block's SNARK proof using the Kimchi proof system.
729///
730/// This function validates that a block header contains a valid zero-knowledge proof
731/// by performing two checks:
732/// 1. **Accumulator check**: Validates the polynomial commitment opening proofs
733/// 2. **Proof verification**: Verifies the blockchain SNARK proof against the protocol state hash.
734///    The blockchain SNARK proves the validity of the protocol state transaction (consensus). Defined
735///    in the OCaml codebase at
736///    <https://github.com/MinaProtocol/mina/tree/compatible/src/lib/blockchain_snark>.  This function
737///    verifies proofs generated by this circuit.
738///
739/// On verification failure, the block data is dumped to a file for debugging purposes.
740///
741/// # Arguments
742///
743/// * `header` - The block header containing the protocol state and its proof
744/// * `verifier_index` - Pre-computed verification key derived from the Blockchain SNARK
745/// * `srs` - Structured Reference String (SRS) for the polynomial commitment scheme
746///
747/// # Returns
748///
749/// `true` if both the accumulator check and proof verification succeed, `false` otherwise.
750pub fn verify_block(
751    header: &MinaBlockHeaderStableV2,
752    verifier_index: &VerifierIndex<Fq>,
753    srs: &SRS<Vesta>,
754) -> bool {
755    let MinaBlockHeaderStableV2 {
756        protocol_state,
757        protocol_state_proof,
758        ..
759    } = &header;
760
761    let vk = VK {
762        commitments: PlonkVerificationKeyEvals::from(verifier_index),
763        index: verifier_index,
764        data: (),
765    };
766
767    let Ok(protocol_state) = ProtocolState::try_from(protocol_state) else {
768        mina_core::warn!(message = format!("verify_block: Protocol state contains invalid field"));
769        return false; // invalid bigint
770    };
771    let protocol_state_hash = MinaHash::hash(&protocol_state);
772
773    let accum_check =
774        accumulator_check::accumulator_check(srs, &[protocol_state_proof]).unwrap_or(false);
775    let verified = verify_impl(&protocol_state_hash, protocol_state_proof, &vk).unwrap_or(false);
776    let ok = accum_check && verified;
777
778    mina_core::info!(message = format!("verify_block OK={ok:?}"));
779
780    if !ok {
781        on_fail::dump_block_verification(header);
782    }
783
784    ok
785}
786
787pub fn verify_transaction<'a>(
788    proofs: impl IntoIterator<Item = (&'a Statement<SokDigest>, &'a TransactionSnarkProofStableV2)>,
789    verifier_index: &VerifierIndex<Fq>,
790    srs: &SRS<Vesta>,
791) -> bool {
792    let vk = VK {
793        commitments: PlonkVerificationKeyEvals::from(verifier_index),
794        index: verifier_index,
795        data: (),
796    };
797
798    let mut inputs: Vec<(
799        &Statement<SokDigest>,
800        &PicklesProofProofsVerified2ReprStableV2,
801        &VK,
802    )> = Vec::with_capacity(128);
803
804    let mut accum_check_proofs: Vec<&PicklesProofProofsVerified2ReprStableV2> =
805        Vec::with_capacity(128);
806
807    proofs
808        .into_iter()
809        .for_each(|(statement, transaction_proof)| {
810            accum_check_proofs.push(transaction_proof);
811            inputs.push((statement, transaction_proof, &vk));
812        });
813
814    let accum_check =
815        accumulator_check::accumulator_check(srs, &accum_check_proofs).unwrap_or(false);
816    let verified = batch_verify_impl(inputs.as_slice()).unwrap_or(false);
817    let ok = accum_check && verified;
818
819    mina_core::info!(message = format!("verify_transactions OK={ok:?}"));
820
821    if !ok {
822        on_fail::dump_tx_verification(&inputs);
823    }
824
825    ok
826}
827
828/// <https://github.com/MinaProtocol/mina/blob/bfd1009abdbee78979ff0343cc73a3480e862f58/src/lib/crypto/kimchi_bindings/stubs/src/pasta_fq_plonk_proof.rs#L116>
829pub fn verify_zkapp(
830    verification_key: &VerificationKey,
831    zkapp_statement: &ZkappStatement,
832    sideloaded_proof: &PicklesProofProofsVerified2ReprStableV2,
833    srs: &SRS<Vesta>,
834) -> bool {
835    let verifier_index = make_zkapp_verifier_index(verification_key);
836    // <https://github.com/MinaProtocol/mina/blob/4e0b324912017c3ff576704ee397ade3d9bda412/src/lib/pickles/pickles.ml#LL260C1-L274C18>
837    let vk = VK {
838        commitments: *verification_key.wrap_index.clone(),
839        index: &verifier_index,
840        data: (),
841    };
842
843    let accum_check =
844        accumulator_check::accumulator_check(srs, &[sideloaded_proof]).unwrap_or(false);
845    let verified = verify_impl(&zkapp_statement, sideloaded_proof, &vk).unwrap_or(false);
846
847    let ok = accum_check && verified;
848
849    mina_core::info!(message = format!("verify_zkapp OK={ok:?}"));
850
851    if !ok {
852        on_fail::dump_zkapp_verification(verification_key, zkapp_statement, sideloaded_proof);
853    }
854
855    ok
856}
857
858fn verify_impl<AppState>(
859    app_state: &AppState,
860    proof: &PicklesProofProofsVerified2ReprStableV2,
861    vk: &VK,
862) -> anyhow::Result<bool>
863where
864    AppState: ToFieldElements<Fp>,
865{
866    let deferred_values = compute_deferred_values(proof)?;
867    let checks = run_checks(proof, vk.index);
868
869    let message_for_next_step_proof = get_message_for_next_step_proof(
870        &proof.statement.messages_for_next_step_proof,
871        &vk.commitments,
872        app_state,
873    )?;
874
875    let message_for_next_wrap_proof =
876        get_message_for_next_wrap_proof(&proof.statement.proof_state.messages_for_next_wrap_proof)?;
877
878    let prepared_statement = get_prepared_statement(
879        &message_for_next_step_proof,
880        &message_for_next_wrap_proof,
881        deferred_values,
882        &proof.statement.proof_state.sponge_digest_before_evaluations,
883    );
884
885    let npublic_input = vk.index.public;
886    let public_inputs = prepared_statement.to_public_input(npublic_input)?;
887    let proof = make_padded_proof_from_p2p(proof)?;
888
889    let result = verify_with(vk.index, &proof, &public_inputs);
890
891    if let Err(e) = result {
892        eprintln!("verify error={:?}", e);
893    };
894
895    Ok(result.is_ok() && checks)
896}
897
898fn batch_verify_impl<AppState>(
899    proofs: &[(&AppState, &PicklesProofProofsVerified2ReprStableV2, &VK)],
900) -> anyhow::Result<bool>
901where
902    AppState: ToFieldElements<Fp>,
903{
904    let mut verification_contexts = Vec::with_capacity(proofs.len());
905    let mut checks = true;
906
907    for (app_state, proof, vk) in proofs {
908        let deferred_values = compute_deferred_values(proof)?;
909        checks = checks && run_checks(proof, vk.index);
910
911        let message_for_next_step_proof = get_message_for_next_step_proof(
912            &proof.statement.messages_for_next_step_proof,
913            &vk.commitments,
914            app_state,
915        )?;
916
917        let message_for_next_wrap_proof = get_message_for_next_wrap_proof(
918            &proof.statement.proof_state.messages_for_next_wrap_proof,
919        )?;
920
921        let prepared_statement = get_prepared_statement(
922            &message_for_next_step_proof,
923            &message_for_next_wrap_proof,
924            deferred_values,
925            &proof.statement.proof_state.sponge_digest_before_evaluations,
926        );
927
928        let npublic_input = vk.index.public;
929        let public_inputs = prepared_statement.to_public_input(npublic_input)?;
930        let proof_padded = make_padded_proof_from_p2p(proof)?;
931
932        verification_contexts.push((vk.index, proof_padded, public_inputs));
933    }
934
935    let proofs: Vec<VerificationContext> = verification_contexts
936        .iter()
937        .map(|(vk, proof, public_input)| VerificationContext {
938            verifier_index: vk,
939            proof,
940            public_input,
941        })
942        .collect();
943
944    let result = batch_verify(&proofs);
945
946    Ok(result.is_ok() && checks)
947}
948
949/// Dump data when it fails, to reproduce and compare in OCaml
950mod on_fail {
951    use super::*;
952
953    pub(super) fn dump_zkapp_verification(
954        verification_key: &VerificationKey,
955        zkapp_statement: &ZkappStatement,
956        sideloaded_proof: &PicklesProofProofsVerified2ReprStableV2,
957    ) {
958        use mina_p2p_messages::{
959            binprot,
960            binprot::macros::{BinProtRead, BinProtWrite},
961        };
962
963        #[derive(Clone, Debug, PartialEq, BinProtRead, BinProtWrite)]
964        struct VerifyZkapp {
965            vk: v2::MinaBaseVerificationKeyWireStableV1,
966            zkapp_statement: v2::MinaBaseZkappStatementStableV2,
967            proof: v2::PicklesProofProofsVerified2ReprStableV2,
968        }
969
970        let data = VerifyZkapp {
971            vk: verification_key.into(),
972            zkapp_statement: zkapp_statement.into(),
973            proof: sideloaded_proof.clone(),
974        };
975
976        dump_to_file(&data, "verify_zkapp")
977    }
978
979    pub(super) fn dump_block_verification(header: &MinaBlockHeaderStableV2) {
980        dump_to_file(header, "verify_block")
981    }
982
983    pub(super) fn dump_tx_verification(
984        txs: &[(
985            &Statement<SokDigest>,
986            &PicklesProofProofsVerified2ReprStableV2,
987            &VK,
988        )],
989    ) {
990        let data = txs
991            .iter()
992            .map(|(statement, proof, _vk)| {
993                let statement: v2::MinaStateSnarkedLedgerStateWithSokStableV2 = (*statement).into();
994                (statement, (*proof).clone())
995            })
996            .collect::<Vec<_>>();
997
998        dump_to_file(&data, "verify_txs")
999    }
1000
1001    #[allow(unreachable_code)]
1002    fn dump_to_file<D: BinProtWrite>(data: &D, filename: &str) {
1003        #[cfg(any(test, feature = "fuzzing"))]
1004        {
1005            let (_, _) = (data, filename); // avoid unused vars
1006            return;
1007        }
1008
1009        if let Err(e) = dump_to_file_impl(data, filename) {
1010            mina_core::error!(
1011                message = "Failed to dump proof verification data",
1012                error = format!("{e:?}")
1013            );
1014        }
1015    }
1016
1017    fn dump_to_file_impl<D: BinProtWrite>(data: &D, filename: &str) -> std::io::Result<()> {
1018        let bin = {
1019            let mut vec = Vec::with_capacity(128 * 1024);
1020            data.binprot_write(&mut vec)?;
1021            vec
1022        };
1023
1024        let debug_dir = mina_core::get_debug_dir();
1025        let filename = debug_dir
1026            .join(generate_new_filename(filename, "binprot", &bin)?)
1027            .to_string_lossy()
1028            .to_string();
1029        std::fs::create_dir_all(&debug_dir)?;
1030
1031        let mut file = std::fs::File::create(&filename)?;
1032        file.write_all(&bin)?;
1033        file.sync_all()?;
1034
1035        mina_core::error!(
1036            message = format!("proof verication failed, dumped data to {:?}", &filename)
1037        );
1038
1039        Ok(())
1040    }
1041
1042    fn generate_new_filename(name: &str, extension: &str, data: &[u8]) -> std::io::Result<String> {
1043        use crate::proofs::util::sha256_sum;
1044
1045        let sum = sha256_sum(data);
1046        for index in 0..100_000 {
1047            let name = format!("{}_{}_{}.{}", name, sum, index, extension);
1048            let path = std::path::Path::new(&name);
1049            if !path.try_exists().unwrap_or(true) {
1050                return Ok(name);
1051            }
1052        }
1053        Err(std::io::Error::other("no filename available"))
1054    }
1055}
mina_tree/proofs/verification.rs

mina_tree/proofs/
verification.rs
