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;
20pub mod folder;
22
23pub use error::*;
24pub use folder::GenericVerifierConstraintFolder;
25
26pub 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 #[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 let mvk = mvk.view(&proof.get_air_ids());
46 self.verify_raps(challenger, &mvk, proof)?;
47 Ok(())
48 }
49
50 #[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 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 {
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 let public_values = proof.get_public_values();
94 {
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 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 {
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; if proof.commitments.main_trace.len() != num_main_commits {
120 return Err(VerificationError::InvalidProofShape);
121 }
122 }
123 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 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 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 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 let rap_phase_seq_result =
180 rap_phase_seq_result.map_err(|_| VerificationError::ChallengePhaseError);
181
182 let alpha: SC::Challenge = challenger.sample_ext_element();
184 tracing::debug!("alpha: {alpha:?}");
185
186 challenger.observe(proof.commitments.quotient.clone());
188
189 let zeta: SC::Challenge = challenger.sample_ext_element();
191 tracing::debug!("zeta: {zeta:?}");
192
193 let pcs = self.config.pcs();
194 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 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 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 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 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 {
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 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 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, "ient_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; 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 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 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 rap_phase_seq_result
419 }
420}