p3_uni_stark/
verifier.rs

1//! See `prover.rs` for an overview of the protocol and a more detailed soundness analysis.
2
3use alloc::vec;
4use alloc::vec::Vec;
5
6use itertools::Itertools;
7use p3_air::{Air, BaseAir};
8use p3_challenger::{CanObserve, FieldChallenger};
9use p3_commit::{Pcs, PolynomialSpace};
10use p3_field::{BasedVectorSpace, Field, PrimeCharacteristicRing};
11use p3_matrix::dense::RowMajorMatrixView;
12use p3_matrix::stack::VerticalPair;
13use p3_util::zip_eq::zip_eq;
14use tracing::instrument;
15
16use crate::symbolic_builder::{SymbolicAirBuilder, get_log_quotient_degree};
17use crate::{PcsError, Proof, StarkGenericConfig, Val, VerifierConstraintFolder};
18
19#[instrument(skip_all)]
20pub fn verify<SC, A>(
21    config: &SC,
22    air: &A,
23    proof: &Proof<SC>,
24    public_values: &Vec<Val<SC>>,
25) -> Result<(), VerificationError<PcsError<SC>>>
26where
27    SC: StarkGenericConfig,
28    A: Air<SymbolicAirBuilder<Val<SC>>> + for<'a> Air<VerifierConstraintFolder<'a, SC>>,
29{
30    let Proof {
31        commitments,
32        opened_values,
33        opening_proof,
34        degree_bits,
35    } = proof;
36
37    let pcs = config.pcs();
38
39    let degree = 1 << degree_bits;
40    let log_quotient_degree =
41        get_log_quotient_degree::<Val<SC>, A>(air, 0, public_values.len(), config.is_zk());
42    let quotient_degree = 1 << (log_quotient_degree + config.is_zk());
43
44    let mut challenger = config.initialise_challenger();
45    let trace_domain = pcs.natural_domain_for_degree(degree);
46    let init_trace_domain = pcs.natural_domain_for_degree(degree >> (config.is_zk()));
47
48    let quotient_domain =
49        trace_domain.create_disjoint_domain(1 << (degree_bits + log_quotient_degree));
50    let quotient_chunks_domains = quotient_domain.split_domains(quotient_degree);
51
52    let randomized_quotient_chunks_domains = quotient_chunks_domains
53        .iter()
54        .map(|domain| pcs.natural_domain_for_degree(domain.size() << (config.is_zk())))
55        .collect_vec();
56
57    // Check that the random commitments are/are not present depending on the ZK setting.
58    if SC::Pcs::ZK {
59        // If ZK is enabled, the prover should have random commitments.
60        if opened_values.random.is_none() || commitments.random.is_none() {
61            return Err(VerificationError::RandomizationError);
62        }
63        // If ZK is not enabled, the prover should not have random commitments.
64    } else if opened_values.random.is_some() || commitments.random.is_some() {
65        return Err(VerificationError::RandomizationError);
66    }
67
68    let air_width = <A as BaseAir<Val<SC>>>::width(air);
69    let valid_shape = opened_values.trace_local.len() == air_width
70        && opened_values.trace_next.len() == air_width
71        && opened_values.quotient_chunks.len() == quotient_degree
72        && opened_values
73            .quotient_chunks
74            .iter()
75            .all(|qc| qc.len() == <SC::Challenge as BasedVectorSpace<Val<SC>>>::DIMENSION)
76        // We've already checked that opened_values.random is present if and only if ZK is enabled.
77        && if let Some(r_comm) = &opened_values.random {
78            r_comm.len() == SC::Challenge::DIMENSION
79        } else {
80            true
81        };
82    if !valid_shape {
83        return Err(VerificationError::InvalidProofShape);
84    }
85
86    // Observe the instance.
87    challenger.observe(Val::<SC>::from_usize(proof.degree_bits));
88    challenger.observe(Val::<SC>::from_usize(proof.degree_bits - config.is_zk()));
89    // TODO: Might be best practice to include other instance data here in the transcript, like some
90    // encoding of the AIR. This protects against transcript collisions between distinct instances.
91    // Practically speaking though, the only related known attack is from failing to include public
92    // values. It's not clear if failing to include other instance data could enable a transcript
93    // collision, since most such changes would completely change the set of satisfying witnesses.
94
95    challenger.observe(commitments.trace.clone());
96    challenger.observe_slice(public_values);
97
98    // Get the first Fiat Shamir challenge which will be used to combine all constraint polynomials
99    // into a single polynomial.
100    //
101    // Soundness Error: n/|EF| where n is the number of constraints.
102    let alpha: SC::Challenge = challenger.sample_algebra_element();
103    challenger.observe(commitments.quotient_chunks.clone());
104
105    // We've already checked that commitments.random is present if and only if ZK is enabled.
106    // Observe the random commitment if it is present.
107    if let Some(r_commit) = commitments.random.clone() {
108        challenger.observe(r_commit);
109    }
110
111    // Get an out-of-domain point to open our values at.
112    //
113    // Soundness Error: dN/|EF| where `N` is the trace length and our constraint polynomial has degree `d`.
114    let zeta: SC::Challenge = challenger.sample_algebra_element();
115    let zeta_next = init_trace_domain.next_point(zeta).unwrap();
116
117    // We've already checked that commitments.random and opened_values.random are present if and only if ZK is enabled.
118    let mut coms_to_verify = if let Some(random_commit) = &commitments.random {
119        let random_values = opened_values
120            .random
121            .as_ref()
122            .ok_or(VerificationError::RandomizationError)?;
123        vec![(
124            random_commit.clone(),
125            vec![(trace_domain, vec![(zeta, random_values.clone())])],
126        )]
127    } else {
128        vec![]
129    };
130    coms_to_verify.extend(vec![
131        (
132            commitments.trace.clone(),
133            vec![(
134                trace_domain,
135                vec![
136                    (zeta, opened_values.trace_local.clone()),
137                    (zeta_next, opened_values.trace_next.clone()),
138                ],
139            )],
140        ),
141        (
142            commitments.quotient_chunks.clone(),
143            // Check the commitment on the randomized domains.
144            zip_eq(
145                randomized_quotient_chunks_domains.iter(),
146                &opened_values.quotient_chunks,
147                VerificationError::InvalidProofShape,
148            )?
149            .map(|(domain, values)| (*domain, vec![(zeta, values.clone())]))
150            .collect_vec(),
151        ),
152    ]);
153
154    pcs.verify(coms_to_verify, opening_proof, &mut challenger)
155        .map_err(VerificationError::InvalidOpeningArgument)?;
156
157    let zps = quotient_chunks_domains
158        .iter()
159        .enumerate()
160        .map(|(i, domain)| {
161            quotient_chunks_domains
162                .iter()
163                .enumerate()
164                .filter(|(j, _)| *j != i)
165                .map(|(_, other_domain)| {
166                    other_domain.vanishing_poly_at_point(zeta)
167                        * other_domain
168                            .vanishing_poly_at_point(domain.first_point())
169                            .inverse()
170                })
171                .product::<SC::Challenge>()
172        })
173        .collect_vec();
174
175    let quotient = opened_values
176        .quotient_chunks
177        .iter()
178        .enumerate()
179        .map(|(ch_i, ch)| {
180            // We checked in valid_shape the length of "ch" is equal to
181            // <SC::Challenge as BasedVectorSpace<Val<SC>>>::DIMENSION. Hence
182            // the unwrap() will never panic.
183            zps[ch_i]
184                * ch.iter()
185                    .enumerate()
186                    .map(|(e_i, &c)| SC::Challenge::ith_basis_element(e_i).unwrap() * c)
187                    .sum::<SC::Challenge>()
188        })
189        .sum::<SC::Challenge>();
190
191    let sels = init_trace_domain.selectors_at_point(zeta);
192
193    let main = VerticalPair::new(
194        RowMajorMatrixView::new_row(&opened_values.trace_local),
195        RowMajorMatrixView::new_row(&opened_values.trace_next),
196    );
197
198    let mut folder = VerifierConstraintFolder {
199        main,
200        public_values,
201        is_first_row: sels.is_first_row,
202        is_last_row: sels.is_last_row,
203        is_transition: sels.is_transition,
204        alpha,
205        accumulator: SC::Challenge::ZERO,
206    };
207    air.eval(&mut folder);
208    let folded_constraints = folder.accumulator;
209
210    // Finally, check that
211    //     folded_constraints(zeta) / Z_H(zeta) = quotient(zeta)
212    if folded_constraints * sels.inv_vanishing != quotient {
213        return Err(VerificationError::OodEvaluationMismatch);
214    }
215
216    Ok(())
217}
218
219#[derive(Debug)]
220pub enum VerificationError<PcsErr> {
221    InvalidProofShape,
222    /// An error occurred while verifying the claimed openings.
223    InvalidOpeningArgument(PcsErr),
224    /// Out-of-domain evaluation mismatch, i.e. `constraints(zeta)` did not match
225    /// `quotient(zeta) Z_H(zeta)`.
226    OodEvaluationMismatch,
227    /// The FRI batch randomization does not correspond to the ZK setting.
228    RandomizationError,
229}
p3_uni_stark/verifier.rs

p3_uni_stark/
verifier.rs
