p3_uni_stark/
verifier.rs

Help
1use alloc::vec;
2use alloc::vec::Vec;
3
4use itertools::Itertools;
5use p3_air::{Air, BaseAir};
6use p3_challenger::{CanObserve, CanSample, FieldChallenger};
7use p3_commit::{Pcs, PolynomialSpace};
8use p3_field::{Field, FieldAlgebra, FieldExtensionAlgebra};
9use p3_matrix::dense::RowMajorMatrixView;
10use p3_matrix::stack::VerticalPair;
11use p3_util::zip_eq::zip_eq;
12use tracing::instrument;
13
14use crate::symbolic_builder::{get_log_quotient_degree, SymbolicAirBuilder};
15use crate::{PcsError, Proof, StarkGenericConfig, Val, VerifierConstraintFolder};
16
17#[instrument(skip_all)]
18pub fn verify<SC, A>(
19    config: &SC,
20    air: &A,
21    challenger: &mut SC::Challenger,
22    proof: &Proof<SC>,
23    public_values: &Vec<Val<SC>>,
24) -> Result<(), VerificationError<PcsError<SC>>>
25where
26    SC: StarkGenericConfig,
27    A: Air<SymbolicAirBuilder<Val<SC>>> + for<'a> Air<VerifierConstraintFolder<'a, SC>>,
28{
29    let Proof {
30        commitments,
31        opened_values,
32        opening_proof,
33        degree_bits,
34    } = proof;
35
36    let degree = 1 << degree_bits;
37    let log_quotient_degree = get_log_quotient_degree::<Val<SC>, A>(air, 0, public_values.len());
38    let quotient_degree = 1 << log_quotient_degree;
39
40    let pcs = config.pcs();
41    let trace_domain = pcs.natural_domain_for_degree(degree);
42    let quotient_domain =
43        trace_domain.create_disjoint_domain(1 << (degree_bits + log_quotient_degree));
44    let quotient_chunks_domains = quotient_domain.split_domains(quotient_degree);
45
46    let air_width = <A as BaseAir<Val<SC>>>::width(air);
47    let valid_shape = opened_values.trace_local.len() == air_width
48        && opened_values.trace_next.len() == air_width
49        && opened_values.quotient_chunks.len() == quotient_degree
50        && opened_values
51            .quotient_chunks
52            .iter()
53            .all(|qc| qc.len() == <SC::Challenge as FieldExtensionAlgebra<Val<SC>>>::D);
54    if !valid_shape {
55        return Err(VerificationError::InvalidProofShape);
56    }
57
58    // Observe the instance.
59    challenger.observe(Val::<SC>::from_canonical_usize(proof.degree_bits));
60    // TODO: Might be best practice to include other instance data here in the transcript, like some
61    // encoding of the AIR. This protects against transcript collisions between distinct instances.
62    // Practically speaking though, the only related known attack is from failing to include public
63    // values. It's not clear if failing to include other instance data could enable a transcript
64    // collision, since most such changes would completely change the set of satisfying witnesses.
65
66    challenger.observe(commitments.trace.clone());
67    challenger.observe_slice(public_values);
68    let alpha: SC::Challenge = challenger.sample_ext_element();
69    challenger.observe(commitments.quotient_chunks.clone());
70
71    let zeta: SC::Challenge = challenger.sample();
72    let zeta_next = trace_domain.next_point(zeta).unwrap();
73
74    pcs.verify(
75        vec![
76            (
77                commitments.trace.clone(),
78                vec![(
79                    trace_domain,
80                    vec![
81                        (zeta, opened_values.trace_local.clone()),
82                        (zeta_next, opened_values.trace_next.clone()),
83                    ],
84                )],
85            ),
86            (
87                commitments.quotient_chunks.clone(),
88                zip_eq(
89                    quotient_chunks_domains.iter(),
90                    &opened_values.quotient_chunks,
91                    VerificationError::InvalidProofShape,
92                )?
93                .map(|(domain, values)| (*domain, vec![(zeta, values.clone())]))
94                .collect_vec(),
95            ),
96        ],
97        opening_proof,
98        challenger,
99    )
100    .map_err(VerificationError::InvalidOpeningArgument)?;
101
102    let zps = quotient_chunks_domains
103        .iter()
104        .enumerate()
105        .map(|(i, domain)| {
106            quotient_chunks_domains
107                .iter()
108                .enumerate()
109                .filter(|(j, _)| *j != i)
110                .map(|(_, other_domain)| {
111                    other_domain.zp_at_point(zeta)
112                        * other_domain.zp_at_point(domain.first_point()).inverse()
113                })
114                .product::<SC::Challenge>()
115        })
116        .collect_vec();
117
118    let quotient = opened_values
119        .quotient_chunks
120        .iter()
121        .enumerate()
122        .map(|(ch_i, ch)| {
123            zps[ch_i]
124                * ch.iter()
125                    .enumerate()
126                    .map(|(e_i, &c)| SC::Challenge::monomial(e_i) * c)
127                    .sum::<SC::Challenge>()
128        })
129        .sum::<SC::Challenge>();
130
131    let sels = trace_domain.selectors_at_point(zeta);
132
133    let main = VerticalPair::new(
134        RowMajorMatrixView::new_row(&opened_values.trace_local),
135        RowMajorMatrixView::new_row(&opened_values.trace_next),
136    );
137
138    let mut folder = VerifierConstraintFolder {
139        main,
140        public_values,
141        is_first_row: sels.is_first_row,
142        is_last_row: sels.is_last_row,
143        is_transition: sels.is_transition,
144        alpha,
145        accumulator: SC::Challenge::ZERO,
146    };
147    air.eval(&mut folder);
148    let folded_constraints = folder.accumulator;
149
150    // Finally, check that
151    //     folded_constraints(zeta) / Z_H(zeta) = quotient(zeta)
152    if folded_constraints * sels.inv_zeroifier != quotient {
153        return Err(VerificationError::OodEvaluationMismatch);
154    }
155
156    Ok(())
157}
158
159#[derive(Debug)]
160pub enum VerificationError<PcsErr> {
161    InvalidProofShape,
162    /// An error occurred while verifying the claimed openings.
163    InvalidOpeningArgument(PcsErr),
164    /// Out-of-domain evaluation mismatch, i.e. `constraints(zeta)` did not match
165    /// `quotient(zeta) Z_H(zeta)`.
166    OodEvaluationMismatch,
167}
p3_uni_stark/verifier.rs

p3_uni_stark/
verifier.rs
