openvm_stark_backend/verifier/
mod.rs

1use std::iter::zip;
2
3use itertools::{izip, zip_eq, Itertools};
4use p3_challenger::{CanObserve, FieldChallenger};
5use p3_commit::{Pcs, PolynomialSpace};
6use p3_field::{FieldAlgebra, FieldExtensionAlgebra};
7use p3_util::log2_strict_usize;
8use tracing::instrument;
9
10use crate::{
11    config::{Com, Domain, StarkGenericConfig, Val},
12    interaction::RapPhaseSeq,
13    keygen::{types::MultiStarkVerifyingKey, view::MultiStarkVerifyingKeyView},
14    proof::{AdjacentOpenedValues, Proof},
15    verifier::constraints::verify_single_rap_constraints,
16};
17
18pub mod constraints;
19mod error;
20/// Constraint folder
21pub mod folder;
22
23pub use error::*;
24pub use folder::GenericVerifierConstraintFolder;
25
26/// Verifies a partitioned proof of multi-matrix AIRs.
27pub struct MultiTraceStarkVerifier<'c, SC: StarkGenericConfig> {
28    config: &'c SC,
29}
30
31impl<'c, SC: StarkGenericConfig> MultiTraceStarkVerifier<'c, SC> {
32    pub fn new(config: &'c SC) -> Self {
33        Self { config }
34    }
35    /// Verify collection of InteractiveAIRs and check the permutation
36    /// cumulative sum is equal to zero across all AIRs.
37    #[instrument(name = "MultiTraceStarkVerifier::verify", level = "debug", skip_all)]
38    pub fn verify(
39        &self,
40        challenger: &mut SC::Challenger,
41        mvk: &MultiStarkVerifyingKey<SC>,
42        proof: &Proof<SC>,
43    ) -> Result<(), VerificationError> {
44        // Note: construction of view panics if any air_id exceeds number of AIRs in provided `MultiStarkVerifyingKey`
45        let mvk = mvk.view(&proof.get_air_ids());
46        self.verify_raps(challenger, &mvk, proof)?;
47        Ok(())
48    }
49
50    /// Verify general RAPs without checking any relations (e.g., cumulative sum) between exposed values of different RAPs.
51    ///
52    /// Public values is a global list shared across all AIRs.
53    ///
54    /// - `num_challenges_to_sample[i]` is the number of challenges to sample in the trace challenge phase corresponding to `proof.commitments.after_challenge[i]`. This must have length equal
55    /// to `proof.commitments.after_challenge`.
56    #[instrument(level = "debug", skip_all)]
57    pub fn verify_raps(
58        &self,
59        challenger: &mut SC::Challenger,
60        mvk: &MultiStarkVerifyingKeyView<Val<SC>, Com<SC>>,
61        proof: &Proof<SC>,
62    ) -> Result<(), VerificationError> {
63        challenger.observe(mvk.pre_hash.clone());
64        let air_ids = proof.get_air_ids();
65        let num_airs = air_ids.len();
66        challenger.observe(Val::<SC>::from_canonical_usize(num_airs));
67        for &air_id in &air_ids {
68            challenger.observe(Val::<SC>::from_canonical_usize(air_id));
69        }
70        // Enforce trace height linear inequalities
71        for constraint in mvk.trace_height_constraints {
72            let sum = proof
73                .per_air
74                .iter()
75                .map(|ap| constraint.coefficients[ap.air_id] as u64 * ap.degree as u64)
76                .sum::<u64>();
77            if sum >= constraint.threshold as u64 {
78                return Err(VerificationError::InvalidProofShape);
79            }
80        }
81        // (T01a): Check that all `air_id`s are different and contained in `MultiStarkVerifyingKey`
82        {
83            let mut air_ids = air_ids;
84            air_ids.sort();
85            for ids in air_ids.windows(2) {
86                if ids[0] >= ids[1] {
87                    return Err(VerificationError::DuplicateAirs);
88                }
89            }
90        }
91        // Note: (T02) is implicit in use of BTreeMap in FRI PCS verify
92
93        let public_values = proof.get_public_values();
94        // (T03a): verify shape of public values
95        {
96            for (pvs_per_air, vk) in zip_eq(&public_values, &mvk.per_air) {
97                if pvs_per_air.len() != vk.params.num_public_values {
98                    return Err(VerificationError::InvalidProofShape);
99                }
100            }
101        }
102        // Challenger must observe public values
103        for pis in &public_values {
104            challenger.observe_slice(pis);
105        }
106
107        for preprocessed_commit in mvk.flattened_preprocessed_commits() {
108            challenger.observe(preprocessed_commit);
109        }
110
111        // (T04a): validate shapes of `main_trace_commits`:
112        {
113            let num_cached_mains = mvk
114                .per_air
115                .iter()
116                .map(|vk| vk.params.width.cached_mains.len())
117                .sum::<usize>();
118            let num_main_commits = num_cached_mains + 1; // always 1 common main
119            if proof.commitments.main_trace.len() != num_main_commits {
120                return Err(VerificationError::InvalidProofShape);
121            }
122        }
123        // Observe main trace commitments
124        challenger.observe_slice(&proof.commitments.main_trace);
125        challenger.observe_slice(
126            &proof
127                .per_air
128                .iter()
129                .map(|ap| Val::<SC>::from_canonical_usize(log2_strict_usize(ap.degree)))
130                .collect_vec(),
131        );
132
133        // Verification of challenge phase (except openings, which are done next).
134        let rap_phase = self.config.rap_phase_seq();
135        let exposed_values_per_air_per_phase = proof
136            .per_air
137            .iter()
138            .map(|proof| proof.exposed_values_after_challenge.clone())
139            .collect_vec();
140        let permutation_opened_values = proof
141            .opening
142            .values
143            .after_challenge
144            .iter()
145            .map(|after_challenge_per_matrix| {
146                after_challenge_per_matrix
147                    .iter()
148                    .map(|after_challenge| {
149                        vec![after_challenge.local.clone(), after_challenge.next.clone()]
150                    })
151                    .collect_vec()
152            })
153            .collect_vec();
154
155        // (T01b): `num_phases < 2`.
156        // Assumption: valid mvk has num_phases consistent between num_challenges_to_sample and exposed_values
157        let num_phases = mvk.num_phases();
158        if num_phases != proof.commitments.after_challenge.len() || num_phases > 1 {
159            return Err(VerificationError::InvalidProofShape);
160        }
161        // (T01c): validate shape of `exposed_values_after_challenge`
162        if !zip_eq(&exposed_values_per_air_per_phase, &mvk.per_air).all(|(ev_per_phase, vk)| {
163            ev_per_phase.len() == vk.params.num_exposed_values_after_challenge.len()
164                && zip_eq(ev_per_phase, &vk.params.num_exposed_values_after_challenge)
165                    .all(|(ev, &n)| ev.len() == n)
166        }) {
167            return Err(VerificationError::InvalidProofShape);
168        }
169
170        let (after_challenge_data, rap_phase_seq_result) = rap_phase.partially_verify(
171            challenger,
172            proof.rap_phase_seq_proof.as_ref(),
173            &exposed_values_per_air_per_phase,
174            &proof.commitments.after_challenge,
175            &permutation_opened_values,
176        );
177        // We don't want to bail on error yet; `OodEvaluationMismatch` should take precedence over
178        // `ChallengePhaseError`, but we won't know if the former happens until later.
179        let rap_phase_seq_result =
180            rap_phase_seq_result.map_err(|_| VerificationError::ChallengePhaseError);
181
182        // Draw `alpha` challenge
183        let alpha: SC::Challenge = challenger.sample_ext_element();
184        tracing::debug!("alpha: {alpha:?}");
185
186        // Observe quotient commitments
187        challenger.observe(proof.commitments.quotient.clone());
188
189        // Draw `zeta` challenge
190        let zeta: SC::Challenge = challenger.sample_ext_element();
191        tracing::debug!("zeta: {zeta:?}");
192
193        let pcs = self.config.pcs();
194        // Build domains
195        let (domains, quotient_chunks_domains): (Vec<_>, Vec<Vec<_>>) = mvk
196            .per_air
197            .iter()
198            .zip_eq(&proof.per_air)
199            .map(|(vk, air_proof)| {
200                let degree = air_proof.degree;
201                let quotient_degree = vk.quotient_degree;
202                let domain = pcs.natural_domain_for_degree(degree);
203                let quotient_domain =
204                    domain.create_disjoint_domain(degree * quotient_degree as usize);
205                let qc_domains = quotient_domain.split_domains(quotient_degree as usize);
206                (domain, qc_domains)
207            })
208            .unzip();
209        // Verify all opening proofs
210        let opened_values = &proof.opening.values;
211        let trace_domain_and_openings =
212            |domain: Domain<SC>,
213             zeta: SC::Challenge,
214             values: &AdjacentOpenedValues<SC::Challenge>| {
215                (
216                    domain,
217                    vec![
218                        (zeta, values.local.clone()),
219                        (domain.next_point(zeta).unwrap(), values.next.clone()),
220                    ],
221                )
222            };
223        // Build the opening rounds
224        // 1. First the preprocessed trace openings
225        // Assumption: each AIR with preprocessed trace has its own commitment and opening values
226        // T05a: validate `opened_values.preprocessed` shape
227        let preprocessed_widths: Vec<usize> = mvk
228            .per_air
229            .iter()
230            .filter_map(|vk| vk.params.width.preprocessed)
231            .collect();
232        if preprocessed_widths.len() != opened_values.preprocessed.len()
233            || zip_eq(preprocessed_widths, &opened_values.preprocessed)
234                .any(|(w, ov)| w != ov.local.len() || w != ov.next.len())
235        {
236            return Err(VerificationError::InvalidProofShape);
237        }
238        let mut rounds: Vec<_> = mvk
239            .preprocessed_commits()
240            .into_iter()
241            .zip_eq(&domains)
242            .flat_map(|(commit, domain)| commit.map(|commit| (commit, *domain)))
243            .zip_eq(&opened_values.preprocessed)
244            .map(|((commit, domain), values)| {
245                let domain_and_openings = trace_domain_and_openings(domain, zeta, values);
246                (commit, vec![domain_and_openings])
247            })
248            .collect();
249
250        // 2. Then the main trace openings
251        // T05b: validate `opened_values.main` shape inline below
252        let num_main_commits = opened_values.main.len();
253        if num_main_commits != proof.commitments.main_trace.len() {
254            return Err(VerificationError::InvalidProofShape);
255        }
256        let mut main_commit_idx = 0;
257        // All commits except the last one are cached main traces.
258        for (vk, domain) in zip_eq(&mvk.per_air, &domains) {
259            for &cached_main_width in &vk.params.width.cached_mains {
260                let commit = proof.commitments.main_trace[main_commit_idx].clone();
261                if opened_values.main[main_commit_idx].len() != 1 {
262                    return Err(VerificationError::InvalidProofShape);
263                }
264                let value = &opened_values.main[main_commit_idx][0];
265                if cached_main_width != value.local.len() || cached_main_width != value.next.len() {
266                    return Err(VerificationError::InvalidProofShape);
267                }
268                let domains_and_openings = vec![trace_domain_and_openings(*domain, zeta, value)];
269                rounds.push((commit.clone(), domains_and_openings));
270                main_commit_idx += 1;
271            }
272        }
273        // In the last commit, each matrix corresponds to an AIR with a common main trace.
274        {
275            let values_per_mat = &opened_values.main[main_commit_idx];
276            let commit = proof.commitments.main_trace[main_commit_idx].clone();
277            let domains_and_openings = zip(&mvk.per_air, &domains)
278                .filter(|(vk, _)| vk.has_common_main())
279                .zip(values_per_mat)
280                .map(|((vk, domain), values)| {
281                    let width = vk.params.width.common_main;
282                    if width != values.local.len() || width != values.next.len() {
283                        Err(VerificationError::InvalidProofShape)
284                    } else {
285                        Ok(trace_domain_and_openings(*domain, zeta, values))
286                    }
287                })
288                .collect::<Result<Vec<_>, _>>()?;
289            if domains_and_openings.len() != values_per_mat.len() {
290                return Err(VerificationError::InvalidProofShape);
291            }
292            rounds.push((commit.clone(), domains_and_openings));
293        }
294
295        let ext_degree = <SC::Challenge as FieldExtensionAlgebra<Val<SC>>>::D;
296        // 3. Then after_challenge trace openings, at most 1 phase for now.
297        // All AIRs with interactions should an after challenge trace.
298        let mut after_challenge_vk_domain_per_air = zip_eq(&mvk.per_air, &domains)
299            .filter(|(vk, _)| vk.has_interaction())
300            .peekable();
301        if after_challenge_vk_domain_per_air.peek().is_none() {
302            if !proof.commitments.after_challenge.is_empty()
303                || !opened_values.after_challenge.is_empty()
304            {
305                return Err(VerificationError::InvalidProofShape);
306            }
307            assert_eq!(num_phases, 0);
308        } else {
309            if num_phases != 1 || opened_values.after_challenge.len() != 1 {
310                return Err(VerificationError::InvalidProofShape);
311            }
312            let after_challenge_commit = proof.commitments.after_challenge[0].clone();
313            let domains_and_openings = zip(
314                after_challenge_vk_domain_per_air,
315                &opened_values.after_challenge[0],
316            )
317            .map(|((vk, domain), values)| {
318                let width = vk.params.width.after_challenge[0] * ext_degree;
319                if width != values.local.len() || width != values.next.len() {
320                    Err(VerificationError::InvalidProofShape)
321                } else {
322                    Ok(trace_domain_and_openings(*domain, zeta, values))
323                }
324            })
325            .collect::<Result<Vec<_>, _>>()?;
326            if domains_and_openings.len() != opened_values.after_challenge[0].len() {
327                return Err(VerificationError::InvalidProofShape);
328            }
329            rounds.push((after_challenge_commit, domains_and_openings));
330        }
331        if opened_values.quotient.len() != num_airs {
332            return Err(VerificationError::InvalidProofShape);
333        }
334        // All opened_values.quotient should have width D
335        if zip_eq(&opened_values.quotient, &mvk.per_air).any(|(per_air, vk)| {
336            per_air.len() != vk.quotient_degree as usize || {
337                per_air
338                    .iter()
339                    .any(|per_chunk| per_chunk.len() != ext_degree)
340            }
341        }) {
342            return Err(VerificationError::InvalidProofShape);
343        }
344        let quotient_domains_and_openings =
345            zip_eq(&opened_values.quotient, &quotient_chunks_domains)
346                .flat_map(|(chunk, quotient_chunks_domains_per_air)| {
347                    chunk
348                        .iter()
349                        .zip_eq(quotient_chunks_domains_per_air)
350                        .map(|(values, &domain)| (domain, vec![(zeta, values.clone())]))
351                })
352                .collect_vec();
353        rounds.push((
354            proof.commitments.quotient.clone(),
355            quotient_domains_and_openings,
356        ));
357
358        pcs.verify(rounds, &proof.opening.proof, challenger)
359            .map_err(|e| VerificationError::InvalidOpeningArgument(format!("{:?}", e)))?;
360
361        let mut preprocessed_idx = 0usize; // preprocessed commit idx
362        let mut after_challenge_idx = vec![0usize; num_phases];
363        let mut cached_main_commit_idx = 0;
364        let mut common_main_matrix_idx = 0;
365
366        // Verify each RAP's constraints
367        for (domain, qc_domains, quotient_chunks, vk, air_proof) in izip!(
368            domains,
369            quotient_chunks_domains,
370            &opened_values.quotient,
371            &mvk.per_air,
372            &proof.per_air
373        ) {
374            let preprocessed_values = vk.preprocessed_data.as_ref().map(|_| {
375                let values = &opened_values.preprocessed[preprocessed_idx];
376                preprocessed_idx += 1;
377                values
378            });
379            let mut partitioned_main_values = Vec::with_capacity(vk.num_cached_mains());
380            for _ in 0..vk.num_cached_mains() {
381                partitioned_main_values.push(&opened_values.main[cached_main_commit_idx][0]);
382                cached_main_commit_idx += 1;
383            }
384            if vk.has_common_main() {
385                partitioned_main_values
386                    .push(&opened_values.main.last().unwrap()[common_main_matrix_idx]);
387                common_main_matrix_idx += 1;
388            }
389            // loop through challenge phases of this single RAP
390            let after_challenge_values = if vk.has_interaction() {
391                (0..num_phases)
392                    .map(|phase_idx| {
393                        let matrix_idx = after_challenge_idx[phase_idx];
394                        after_challenge_idx[phase_idx] += 1;
395                        &opened_values.after_challenge[phase_idx][matrix_idx]
396                    })
397                    .collect_vec()
398            } else {
399                vec![]
400            };
401            verify_single_rap_constraints::<SC>(
402                &vk.symbolic_constraints.constraints,
403                preprocessed_values,
404                partitioned_main_values,
405                after_challenge_values,
406                quotient_chunks,
407                domain,
408                &qc_domains,
409                zeta,
410                alpha,
411                &after_challenge_data.challenges_per_phase,
412                &air_proof.public_values,
413                &air_proof.exposed_values_after_challenge,
414            )?;
415        }
416
417        // If we made it this far, use the `rap_phase_result` as the final result.
418        rap_phase_seq_result
419    }
420}