sp1_hypercube/logup_gkr/
verifier.rs

1use crate::prover::Record;
2use crate::record::MachineRecord;
3use crate::VerifierPublicValuesConstraintFolder;
4use crate::GKR_GRINDING_BITS;
5use crate::{air::MachineAir, Chip, ShardContext};
6use itertools::Itertools;
7use slop_air::BaseAir;
8use slop_algebra::AbstractField;
9use slop_challenger::GrindingChallenger;
10use slop_challenger::{CanObserve, FieldChallenger, IopCtx, VariableLengthChallenger};
11use slop_multilinear::{
12    full_geq, partial_lagrange_blocking, Mle, MleEval, MultilinearPcsChallenger, Point,
13};
14use slop_sumcheck::{partially_verify_sumcheck_proof, SumcheckError};
15use std::cmp::max;
16use std::{
17    collections::{BTreeMap, BTreeSet},
18    marker::PhantomData,
19};
20use thiserror::Error;
21
22use super::{ChipEvaluation, LogUpEvaluations, LogUpGkrOutput, LogupGkrProof};
23
24/// An error type for `LogUp` GKR.
25#[derive(Debug, Error)]
26pub enum LogupGkrVerificationError<EF> {
27    /// The sumcheck claim is not consistent with the calculated one from the prover messages.
28    #[error("inconsistent sumcheck claim at round {0}")]
29    InconsistentSumcheckClaim(usize),
30    /// Inconsistency between the calculated evaluation and the sumcheck evaluation.
31    #[error("inconsistent evaluation at round {0}")]
32    InconsistentEvaluation(usize),
33    /// Error when verifying sumcheck proof.
34    #[error("sumcheck error: {0}")]
35    SumcheckError(#[from] SumcheckError),
36    /// The proof shape does not match the expected one for the given number of interactions.
37    #[error("invalid shape")]
38    InvalidShape,
39    /// The size of the first layer does not match the expected one.
40    #[error("invalid first layer dimension: {0} != {1}")]
41    InvalidFirstLayerDimension(u32, u32),
42    /// The dimension of the last layer does not match the expected one.
43    #[error("invalid last layer dimension: {0} != {1}")]
44    InvalidLastLayerDimension(usize, usize),
45    /// The trace point does not match the claimed opening point.
46    #[error("trace point mismatch")]
47    TracePointMismatch,
48    /// The cumulative sum does not match the claimed one.
49    #[error("cumulative sum mismatch: {0} != {1}")]
50    CumulativeSumMismatch(EF, EF),
51    /// The numerator evaluation does not match the expected one.
52    #[error("numerator evaluation mismatch: {0} != {1}")]
53    NumeratorEvaluationMismatch(EF, EF),
54    /// The denominator evaluation does not match the expected one.
55    #[error("denominator evaluation mismatch: {0} != {1}")]
56    DenominatorEvaluationMismatch(EF, EF),
57    /// The denominator guts had zero in it.
58    #[error("denominator evaluation has zero value")]
59    ZeroDenominator,
60    /// Invalid grinding witness.
61    #[error("Invalid proof of work witness")]
62    Pow,
63    /// The public values verification failed.
64    #[error("public values verification failed")]
65    InvalidPublicValues,
66}
67
68/// Verifier for `LogUp` GKR.
69#[derive(Clone, Debug, Copy, Default, PartialEq, Eq, Hash)]
70pub struct LogUpGkrVerifier<GC, SC>(PhantomData<(GC, SC)>);
71
72impl<GC: IopCtx, SC: ShardContext<GC>> LogUpGkrVerifier<GC, SC> {
73    /// Verify the public values satisfy the required constraints, and return the cumulative sum.
74    pub fn verify_public_values(
75        challenge: GC::EF,
76        alpha: &GC::EF,
77        beta_seed: &Point<GC::EF>,
78        public_values: &[GC::F],
79    ) -> Result<GC::EF, LogupGkrVerificationError<GC::EF>> {
80        let betas = slop_multilinear::partial_lagrange_blocking(beta_seed).into_buffer().into_vec();
81        let mut folder = VerifierPublicValuesConstraintFolder::<GC> {
82            perm_challenges: (alpha, &betas),
83            alpha: challenge,
84            accumulator: GC::EF::zero(),
85            local_interaction_digest: GC::EF::zero(),
86            public_values,
87            _marker: PhantomData,
88        };
89        Record::<_, SC>::eval_public_values(&mut folder);
90        if folder.accumulator == GC::EF::zero() {
91            Ok(folder.local_interaction_digest)
92        } else {
93            Err(LogupGkrVerificationError::InvalidPublicValues)
94        }
95    }
96
97    /// Verify the `LogUp` GKR proof.
98    ///
99    /// # Errors
100    #[allow(clippy::too_many_arguments)]
101    #[allow(clippy::too_many_lines)]
102    pub fn verify_logup_gkr(
103        shard_chips: &BTreeSet<Chip<GC::F, SC::Air>>,
104        degrees: &BTreeMap<String, Point<GC::F>>,
105        max_log_row_count: usize,
106        proof: &LogupGkrProof<<GC::Challenger as GrindingChallenger>::Witness, GC::EF>,
107        public_values: &[GC::F],
108        challenger: &mut GC::Challenger,
109    ) -> Result<(), LogupGkrVerificationError<GC::EF>> {
110        let LogupGkrProof { circuit_output, round_proofs, logup_evaluations, witness } = proof;
111
112        let LogUpGkrOutput { numerator, denominator } = circuit_output;
113        if shard_chips.iter().all(|chip| chip.sends().is_empty() && chip.receives().is_empty()) {
114            return Err(LogupGkrVerificationError::InvalidShape);
115        }
116        let max_interaction_arity = shard_chips
117            .iter()
118            .flat_map(|c| c.sends().iter().chain(c.receives().iter()))
119            .map(|i| i.values.len() + 1)
120            .max()
121            .unwrap();
122
123        let max_interaction_kinds_values = Record::<_, SC>::interactions_in_public_values()
124            .iter()
125            .map(|kind| kind.num_values() + 1)
126            .max()
127            .unwrap_or(1);
128        let beta_seed_dim =
129            max(max_interaction_arity, max_interaction_kinds_values).next_power_of_two().ilog2();
130
131        // Check proof of work (grinding to find a number that hashes to have
132        // `GKR_GRINDING_BITS` zeroes at the beginning).
133        if !challenger.check_witness(GKR_GRINDING_BITS, *witness) {
134            return Err(LogupGkrVerificationError::Pow);
135        }
136
137        let alpha = challenger.sample_ext_element::<GC::EF>();
138        let beta_seed = (0..beta_seed_dim)
139            .map(|_| challenger.sample_ext_element::<GC::EF>())
140            .collect::<Point<_>>();
141        let pv_challenge = challenger.sample_ext_element::<GC::EF>();
142        let cumulative_sum = -LogUpGkrVerifier::<GC, SC>::verify_public_values(
143            pv_challenge,
144            &alpha,
145            &beta_seed,
146            public_values,
147        )?;
148
149        // Calculate the interaction number.
150        let num_of_interactions =
151            shard_chips.iter().map(|c| c.sends().len() + c.receives().len()).sum::<usize>();
152        let number_of_interaction_variables = num_of_interactions.next_power_of_two().ilog2();
153
154        let expected_size = 1 << (number_of_interaction_variables + 1);
155
156        if !numerator.guts().has_valid_shape()
157            || !denominator.guts().has_valid_shape()
158            || numerator.guts().dimensions.sizes() != [expected_size, 1]
159            || denominator.guts().dimensions.sizes() != [expected_size, 1]
160        {
161            return Err(LogupGkrVerificationError::InvalidShape);
162        }
163
164        // Observe the output claims.
165        challenger.observe_variable_length_extension_slice(numerator.guts().as_slice());
166        challenger.observe_variable_length_extension_slice(denominator.guts().as_slice());
167
168        if denominator.guts().as_slice().iter().any(slop_algebra::Field::is_zero) {
169            return Err(LogupGkrVerificationError::ZeroDenominator);
170        }
171
172        // Verify that the cumulative sum matches the claimed one.
173        let output_cumulative_sum = numerator
174            .guts()
175            .as_slice()
176            .iter()
177            .zip_eq(denominator.guts().as_slice().iter())
178            .map(|(n, d)| *n / *d)
179            .sum::<GC::EF>();
180        if output_cumulative_sum != cumulative_sum {
181            return Err(LogupGkrVerificationError::CumulativeSumMismatch(
182                output_cumulative_sum,
183                cumulative_sum,
184            ));
185        }
186
187        // Assert that the size of the first layer matches the expected one.
188        let initial_number_of_variables = numerator.num_variables();
189        if initial_number_of_variables != number_of_interaction_variables + 1 {
190            return Err(LogupGkrVerificationError::InvalidFirstLayerDimension(
191                initial_number_of_variables,
192                number_of_interaction_variables + 1,
193            ));
194        }
195        // Sample the first evaluation point.
196        let first_eval_point = challenger.sample_point::<GC::EF>(initial_number_of_variables);
197
198        // Follow the GKR protocol layer by layer.
199        let mut numerator_eval = numerator.blocking_eval_at(&first_eval_point)[0];
200        let mut denominator_eval = denominator.blocking_eval_at(&first_eval_point)[0];
201        let mut eval_point = first_eval_point;
202
203        if round_proofs.len() + 1 != max_log_row_count {
204            return Err(LogupGkrVerificationError::InvalidShape);
205        }
206
207        for (i, round_proof) in round_proofs.iter().enumerate() {
208            // Get the batching challenge for combining the claims.
209            let lambda = challenger.sample_ext_element::<GC::EF>();
210            // Check that the claimed sum is consistent with the previous round values.
211            let expected_claim = numerator_eval * lambda + denominator_eval;
212            if round_proof.sumcheck_proof.claimed_sum != expected_claim {
213                return Err(LogupGkrVerificationError::InconsistentSumcheckClaim(i));
214            }
215            // Verify the sumcheck proof.
216            partially_verify_sumcheck_proof(
217                &round_proof.sumcheck_proof,
218                challenger,
219                i + number_of_interaction_variables as usize + 1,
220                3,
221            )?;
222            // Verify that the evaluation claim is consistent with the prover messages.
223            let (point, final_eval) = round_proof.sumcheck_proof.point_and_eval.clone();
224            let eq_eval = Mle::full_lagrange_eval(&point, &eval_point);
225            let numerator_sumcheck_eval = round_proof.numerator_0 * round_proof.denominator_1
226                + round_proof.numerator_1 * round_proof.denominator_0;
227            let denominator_sumcheck_eval = round_proof.denominator_0 * round_proof.denominator_1;
228            let expected_final_eval =
229                eq_eval * (numerator_sumcheck_eval * lambda + denominator_sumcheck_eval);
230            if final_eval != expected_final_eval {
231                return Err(LogupGkrVerificationError::InconsistentEvaluation(i));
232            }
233
234            // Observe the prover message.
235            challenger.observe_ext_element(round_proof.numerator_0);
236            challenger.observe_ext_element(round_proof.numerator_1);
237            challenger.observe_ext_element(round_proof.denominator_0);
238            challenger.observe_ext_element(round_proof.denominator_1);
239
240            // Get the evaluation point for the claims of the next round.
241            eval_point = round_proof.sumcheck_proof.point_and_eval.0.clone();
242            // Sample the last coordinate and add to the point.
243            let last_coordinate = challenger.sample_ext_element::<GC::EF>();
244            eval_point.add_dimension_back(last_coordinate);
245            // Update the evaluation of the numerator and denominator at the last coordinate.
246            numerator_eval = round_proof.numerator_0
247                + (round_proof.numerator_1 - round_proof.numerator_0) * last_coordinate;
248            denominator_eval = round_proof.denominator_0
249                + (round_proof.denominator_1 - round_proof.denominator_0) * last_coordinate;
250        }
251
252        // Verify that the last layer evaluations are consistent with the evaluations of the traces.
253        let (interaction_point, trace_point) =
254            eval_point.split_at(number_of_interaction_variables as usize);
255        // Assert that the number of trace variables matches the expected one.
256        let trace_variables = trace_point.dimension();
257        if trace_variables != max_log_row_count {
258            return Err(LogupGkrVerificationError::InvalidLastLayerDimension(
259                trace_variables,
260                max_log_row_count,
261            ));
262        }
263
264        // Assert that the trace point is the same as the claimed opening point
265        let LogUpEvaluations { point, chip_openings } = logup_evaluations;
266        if point != &trace_point {
267            return Err(LogupGkrVerificationError::TracePointMismatch);
268        }
269
270        if shard_chips.len() != chip_openings.len()
271            || shard_chips.len() != degrees.len()
272            || shard_chips.iter().map(MachineAir::name).ne(chip_openings.keys().map(String::as_str))
273            || shard_chips.iter().map(MachineAir::name).ne(degrees.keys().map(String::as_str))
274        {
275            return Err(LogupGkrVerificationError::InvalidShape);
276        }
277
278        let betas = partial_lagrange_blocking(&beta_seed);
279
280        // Compute the expected opening of the last layer numerator and denominator values from the
281        // trace openings.
282        let mut numerator_values = Vec::with_capacity(num_of_interactions);
283        let mut denominator_values = Vec::with_capacity(num_of_interactions);
284        let mut point_extended = point.clone();
285        point_extended.add_dimension(GC::EF::zero());
286        let len = shard_chips.len();
287        challenger.observe(GC::F::from_canonical_usize(len));
288        for ((chip, openings), threshold) in
289            shard_chips.iter().zip_eq(chip_openings.values()).zip_eq(degrees.values())
290        {
291            // Observe the opening
292            if let Some(prep_eval) = openings.preprocessed_trace_evaluations.as_ref() {
293                challenger.observe_variable_length_extension_slice(prep_eval);
294                if !prep_eval.evaluations().has_valid_shape()
295                    || prep_eval.evaluations().sizes() != [chip.air.preprocessed_width()]
296                {
297                    return Err(LogupGkrVerificationError::InvalidShape);
298                }
299            } else if chip.air.preprocessed_width() != 0 {
300                return Err(LogupGkrVerificationError::InvalidShape);
301            }
302            challenger.observe_variable_length_extension_slice(&openings.main_trace_evaluations);
303            if !openings.main_trace_evaluations.evaluations().has_valid_shape()
304                || openings.main_trace_evaluations.evaluations().sizes() != [chip.air.width()]
305            {
306                return Err(LogupGkrVerificationError::InvalidShape);
307            }
308
309            if threshold.dimension() != point_extended.dimension() {
310                return Err(LogupGkrVerificationError::InvalidShape);
311            }
312
313            let geq_eval = full_geq(threshold, &point_extended);
314            let ChipEvaluation { main_trace_evaluations, preprocessed_trace_evaluations } =
315                openings;
316            for (interaction, is_send) in chip
317                .sends()
318                .iter()
319                .map(|s| (s, true))
320                .chain(chip.receives().iter().map(|r| (r, false)))
321            {
322                let (real_numerator, real_denominator) = interaction.eval(
323                    preprocessed_trace_evaluations.as_ref(),
324                    main_trace_evaluations,
325                    alpha,
326                    betas.as_slice(),
327                );
328                let padding_trace_opening =
329                    MleEval::from(vec![GC::EF::zero(); main_trace_evaluations.num_evaluations()]);
330                let padding_preprocessed_opening = preprocessed_trace_evaluations
331                    .as_ref()
332                    .map(|eval| MleEval::from(vec![GC::EF::zero(); eval.num_evaluations()]));
333                let (padding_numerator, padding_denominator) = interaction.eval(
334                    padding_preprocessed_opening.as_ref(),
335                    &padding_trace_opening,
336                    alpha,
337                    betas.as_slice(),
338                );
339
340                let numerator_eval = real_numerator - padding_numerator * geq_eval;
341                let denominator_eval =
342                    real_denominator + (GC::EF::one() - padding_denominator) * geq_eval;
343                let numerator_eval = if is_send { numerator_eval } else { -numerator_eval };
344                numerator_values.push(numerator_eval);
345                denominator_values.push(denominator_eval);
346            }
347        }
348        // Convert the values to a multilinear polynomials.
349        // Pad the numerator values with zeros.
350        numerator_values.resize(1 << interaction_point.dimension(), GC::EF::zero());
351        let numerator = Mle::from(numerator_values);
352        // Pad the denominator values with ones.
353        denominator_values.resize(1 << interaction_point.dimension(), GC::EF::one());
354        let denominator = Mle::from(denominator_values);
355
356        let expected_numerator_eval = numerator.blocking_eval_at(&interaction_point)[0];
357        let expected_denominator_eval = denominator.blocking_eval_at(&interaction_point)[0];
358        if numerator_eval != expected_numerator_eval {
359            return Err(LogupGkrVerificationError::NumeratorEvaluationMismatch(
360                numerator_eval,
361                expected_numerator_eval,
362            ));
363        }
364        if denominator_eval != expected_denominator_eval {
365            return Err(LogupGkrVerificationError::DenominatorEvaluationMismatch(
366                denominator_eval,
367                expected_denominator_eval,
368            ));
369        }
370        Ok(())
371    }
372}
sp1_hypercube/logup_gkr/verifier.rs

sp1_hypercube/logup_gkr/
verifier.rs
