openvm_stark_backend/verifier/
constraints.rs

Help
1use std::marker::PhantomData;
2
3use itertools::Itertools;
4use p3_commit::PolynomialSpace;
5use p3_field::{Field, FieldAlgebra, FieldExtensionAlgebra};
6use p3_matrix::{dense::RowMajorMatrixView, stack::VerticalPair};
7use tracing::instrument;
8
9use super::{
10    error::VerificationError,
11    folder::{GenericVerifierConstraintFolder, VerifierConstraintFolder},
12};
13use crate::{
14    air_builders::symbolic::SymbolicExpressionDag,
15    config::{Domain, StarkGenericConfig, Val},
16    proof::AdjacentOpenedValues,
17};
18
19#[allow(clippy::too_many_arguments)]
20#[instrument(skip_all, level = "trace")]
21pub fn verify_single_rap_constraints<SC>(
22    constraints: &SymbolicExpressionDag<Val<SC>>,
23    preprocessed_values: Option<&AdjacentOpenedValues<SC::Challenge>>,
24    partitioned_main_values: Vec<&AdjacentOpenedValues<SC::Challenge>>,
25    after_challenge_values: Vec<&AdjacentOpenedValues<SC::Challenge>>,
26    quotient_chunks: &[Vec<SC::Challenge>],
27    domain: Domain<SC>, // trace domain
28    qc_domains: &[Domain<SC>],
29    zeta: SC::Challenge,
30    alpha: SC::Challenge,
31    challenges: &[Vec<SC::Challenge>],
32    public_values: &[Val<SC>],
33    exposed_values_after_challenge: &[Vec<SC::Challenge>],
34) -> Result<(), VerificationError>
35where
36    SC: StarkGenericConfig,
37{
38    let zps = qc_domains
39        .iter()
40        .enumerate()
41        .map(|(i, domain)| {
42            qc_domains
43                .iter()
44                .enumerate()
45                .filter(|(j, _)| *j != i)
46                .map(|(_, other_domain)| {
47                    other_domain.zp_at_point(zeta)
48                        * other_domain.zp_at_point(domain.first_point()).inverse()
49                })
50                .product::<SC::Challenge>()
51        })
52        .collect_vec();
53
54    let quotient = quotient_chunks
55        .iter()
56        .enumerate()
57        .map(|(ch_i, ch)| {
58            ch.iter()
59                .enumerate()
60                .map(|(e_i, &c)| zps[ch_i] * SC::Challenge::monomial(e_i) * c)
61                .sum::<SC::Challenge>()
62        })
63        .sum::<SC::Challenge>();
64
65    let unflatten = |v: &[SC::Challenge]| {
66        v.chunks_exact(SC::Challenge::D)
67            .map(|chunk| {
68                chunk
69                    .iter()
70                    .enumerate()
71                    .map(|(e_i, &c)| SC::Challenge::monomial(e_i) * c)
72                    .sum()
73            })
74            .collect::<Vec<SC::Challenge>>()
75    };
76
77    let sels = domain.selectors_at_point(zeta);
78
79    let (preprocessed_local, preprocessed_next) = preprocessed_values
80        .as_ref()
81        .map(|values| (values.local.as_slice(), values.next.as_slice()))
82        .unwrap_or((&[], &[]));
83    let preprocessed = VerticalPair::new(
84        RowMajorMatrixView::new_row(preprocessed_local),
85        RowMajorMatrixView::new_row(preprocessed_next),
86    );
87
88    let partitioned_main: Vec<_> = partitioned_main_values
89        .into_iter()
90        .map(|values| {
91            VerticalPair::new(
92                RowMajorMatrixView::new_row(&values.local),
93                RowMajorMatrixView::new_row(&values.next),
94            )
95        })
96        .collect();
97
98    let after_challenge_ext_values: Vec<_> = after_challenge_values
99        .into_iter()
100        .map(|values| {
101            let [local, next] = [&values.local, &values.next]
102                .map(|flattened_ext_values| unflatten(flattened_ext_values));
103            (local, next)
104        })
105        .collect();
106    let after_challenge = after_challenge_ext_values
107        .iter()
108        .map(|(local, next)| {
109            VerticalPair::new(
110                RowMajorMatrixView::new_row(local),
111                RowMajorMatrixView::new_row(next),
112            )
113        })
114        .collect();
115
116    let mut folder: VerifierConstraintFolder<'_, SC> = GenericVerifierConstraintFolder {
117        preprocessed,
118        partitioned_main,
119        after_challenge,
120        is_first_row: sels.is_first_row,
121        is_last_row: sels.is_last_row,
122        is_transition: sels.is_transition,
123        alpha,
124        accumulator: SC::Challenge::ZERO,
125        challenges,
126        public_values,
127        exposed_values_after_challenge,
128        _marker: PhantomData,
129    };
130    folder.eval_constraints(constraints);
131
132    let folded_constraints = folder.accumulator;
133    // Finally, check that
134    //     folded_constraints(zeta) / Z_H(zeta) = quotient(zeta)
135    if folded_constraints * sels.inv_zeroifier != quotient {
136        return Err(VerificationError::OodEvaluationMismatch);
137    }
138
139    Ok(())
140}
openvm_stark_backend/verifier/constraints.rs

openvm_stark_backend/verifier/
constraints.rs
