openvm_stark_backend/verifier/
constraints.rs

1use std::marker::PhantomData;
2
3use itertools::Itertools;
4use p3_commit::PolynomialSpace;
5use p3_field::{BasedVectorSpace, Field, PrimeCharacteristicRing};
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.vanishing_poly_at_point(zeta)
48                        * other_domain
49                            .vanishing_poly_at_point(domain.first_point())
50                            .inverse()
51                })
52                .product::<SC::Challenge>()
53        })
54        .collect_vec();
55
56    let quotient = quotient_chunks
57        .iter()
58        .enumerate()
59        .map(|(ch_i, ch)| {
60            ch.iter()
61                .enumerate()
62                .map(|(e_i, &c)| {
63                    zps[ch_i]
64                        * SC::Challenge::ith_basis_element(e_i)
65                            .expect("basis element index out of bounds")
66                        * c
67                })
68                .sum::<SC::Challenge>()
69        })
70        .sum::<SC::Challenge>();
71
72    let unflatten = |v: &[SC::Challenge]| {
73        v.chunks_exact(SC::Challenge::DIMENSION)
74            .map(|chunk| {
75                chunk
76                    .iter()
77                    .enumerate()
78                    .map(|(e_i, &c)| {
79                        SC::Challenge::ith_basis_element(e_i)
80                            .expect("basis element index out of bounds")
81                            * c
82                    })
83                    .sum()
84            })
85            .collect::<Vec<SC::Challenge>>()
86    };
87
88    let sels = domain.selectors_at_point(zeta);
89
90    let (preprocessed_local, preprocessed_next) = preprocessed_values
91        .as_ref()
92        .map(|values| (values.local.as_slice(), values.next.as_slice()))
93        .unwrap_or((&[], &[]));
94    let preprocessed = VerticalPair::new(
95        RowMajorMatrixView::new_row(preprocessed_local),
96        RowMajorMatrixView::new_row(preprocessed_next),
97    );
98
99    let partitioned_main: Vec<_> = partitioned_main_values
100        .into_iter()
101        .map(|values| {
102            VerticalPair::new(
103                RowMajorMatrixView::new_row(&values.local),
104                RowMajorMatrixView::new_row(&values.next),
105            )
106        })
107        .collect();
108
109    let after_challenge_ext_values: Vec<_> = after_challenge_values
110        .into_iter()
111        .map(|values| {
112            let [local, next] = [&values.local, &values.next]
113                .map(|flattened_ext_values| unflatten(flattened_ext_values));
114            (local, next)
115        })
116        .collect();
117    let after_challenge = after_challenge_ext_values
118        .iter()
119        .map(|(local, next)| {
120            VerticalPair::new(
121                RowMajorMatrixView::new_row(local),
122                RowMajorMatrixView::new_row(next),
123            )
124        })
125        .collect();
126
127    let mut folder: VerifierConstraintFolder<'_, SC> = GenericVerifierConstraintFolder {
128        preprocessed,
129        partitioned_main,
130        after_challenge,
131        is_first_row: sels.is_first_row,
132        is_last_row: sels.is_last_row,
133        is_transition: sels.is_transition,
134        alpha,
135        accumulator: SC::Challenge::ZERO,
136        challenges,
137        public_values,
138        exposed_values_after_challenge,
139        _marker: PhantomData,
140    };
141    folder.eval_constraints(constraints);
142
143    let folded_constraints = folder.accumulator;
144    // Finally, check that
145    //     folded_constraints(zeta) / Z_H(zeta) = quotient(zeta)
146    if folded_constraints * sels.inv_vanishing != quotient {
147        return Err(VerificationError::OodEvaluationMismatch);
148    }
149
150    Ok(())
151}
openvm_stark_backend/verifier/constraints.rs

openvm_stark_backend/verifier/
constraints.rs
