openvm_stark_backend/verifier/
fractional_sumcheck_gkr.rs

1use p3_field::PrimeCharacteristicRing;
2use thiserror::Error;
3use tracing::debug;
4
5use crate::{
6    poly_common::{eval_eq_mle, interpolate_cubic_at_0123, interpolate_linear_at_01},
7    proof::{GkrLayerClaims, GkrProof},
8    FiatShamirTranscript, StarkProtocolConfig,
9};
10
11#[derive(Debug, Error, PartialEq, Eq)]
12pub enum GkrVerificationError<EF: core::fmt::Debug + core::fmt::Display + PartialEq + Eq> {
13    #[error("Zero-round proof: q0_claim should be 1, got {actual}")]
14    InvalidZeroRoundValue { actual: EF },
15    #[error("Zero-check failed: numerator at root should be zero, got {actual}")]
16    ZeroCheckFailed { actual: EF },
17    #[error("Denominator consistency check failed at root: expected {expected}, got {actual}")]
18    RootConsistencyCheckFailed { expected: EF, actual: EF },
19    #[error("Layer consistency check failed at round {round}: expected {expected}, got {actual}")]
20    LayerConsistencyCheckFailed {
21        round: usize,
22        expected: EF,
23        actual: EF,
24    },
25    #[error("Expected {expected} layers, got {actual}")]
26    IncorrectLayerCount { expected: usize, actual: usize },
27    #[error("Expected {expected} sumcheck polynomial entries, got {actual}")]
28    IncorrectSumcheckPolyCount { expected: usize, actual: usize },
29    #[error("Round {round} expected {expected} sumcheck sub-rounds, got {actual}")]
30    IncorrectSubroundCount {
31        round: usize,
32        expected: usize,
33        actual: usize,
34    },
35}
36
37/// Verifies the GKR protocol for fractional sumcheck.
38///
39/// Reduces the fractional sum ∑_{y ∈ H_{ℓ+n_logup}} p̂(y)/q̂(y) = 0 to evaluation claims
40/// on the input layer polynomials p̂(ξ) and q̂(ξ) at a random point ξ.
41///
42/// The argument `total_rounds` must equal `ℓ+n_logup`.
43///
44/// # Returns
45/// `(p̂(ξ), q̂(ξ), ξ)` where ξ ∈ F_ext^{ℓ+n_logup} is the random evaluation point.
46#[allow(clippy::type_complexity)]
47pub fn verify_gkr<SC: StarkProtocolConfig, TS: FiatShamirTranscript<SC>>(
48    proof: &GkrProof<SC>,
49    transcript: &mut TS,
50    total_rounds: usize,
51) -> Result<(SC::EF, SC::EF, Vec<SC::EF>), GkrVerificationError<SC::EF>> {
52    assert!(total_rounds > 0);
53
54    // Note: this is already asserted by proof shape
55    if proof.claims_per_layer.len() != total_rounds {
56        return Err(GkrVerificationError::IncorrectLayerCount {
57            expected: total_rounds,
58            actual: proof.claims_per_layer.len(),
59        });
60    }
61
62    // Note: this is already asserted by proof shape
63    // Sumcheck polys: round j has j sub-rounds, so total = 0+1+2+...+(total_rounds-1)
64    let expected_sumcheck_entries = total_rounds.saturating_sub(1);
65    if proof.sumcheck_polys.len() != expected_sumcheck_entries {
66        return Err(GkrVerificationError::IncorrectSumcheckPolyCount {
67            expected: expected_sumcheck_entries,
68            actual: proof.sumcheck_polys.len(),
69        });
70    }
71
72    transcript.observe_ext(proof.q0_claim);
73
74    // Handle round 0 (no sumcheck, direct tree evaluation)
75    let layer_claims = &proof.claims_per_layer[0];
76    observe_layer_claims::<SC, TS>(transcript, layer_claims);
77
78    // Compute recursive relations for layer 1 → 0
79    let (p_cross_term, q_cross_term) = compute_recursive_relations::<SC>(layer_claims);
80
81    // Zero-check: p̂₀ must be zero
82    if p_cross_term != SC::EF::ZERO {
83        return Err(GkrVerificationError::ZeroCheckFailed {
84            actual: p_cross_term,
85        });
86    }
87
88    // Verify q0 consistency
89    if q_cross_term != proof.q0_claim {
90        return Err(GkrVerificationError::RootConsistencyCheckFailed {
91            expected: proof.q0_claim,
92            actual: q_cross_term,
93        });
94    }
95
96    // Sample μ₁ and reduce to single evaluation
97    let mu = transcript.sample_ext();
98    debug!(gkr_round = 0, %mu);
99    let (mut numer_claim, mut denom_claim) = reduce_to_single_evaluation::<SC>(layer_claims, mu);
100    debug!(%numer_claim, %denom_claim);
101    let mut gkr_r = vec![mu];
102
103    // Handle rounds 1..total_rounds with sumcheck
104    for round in 1..total_rounds {
105        // Sample batching challenge λⱼ
106        let lambda = transcript.sample_ext();
107        debug!(gkr_round = round, %lambda);
108        let claim = numer_claim + lambda * denom_claim;
109
110        // Run sumcheck protocol for this round (round j has j sub-rounds)
111        // Invariant: `gkr_r.len() == round_r.len() == round`
112        let (new_claim, round_r, eq_at_r_prime) =
113            verify_gkr_sumcheck::<SC, TS>(proof, transcript, round, claim, &gkr_r)?;
114        debug_assert_eq!(eq_at_r_prime, eval_eq_mle(&gkr_r, &round_r));
115
116        // Observe layer evaluation claims
117        let layer_claims = &proof.claims_per_layer[round];
118        observe_layer_claims::<SC, TS>(transcript, layer_claims);
119
120        // Compute recursive relations
121        let (p_cross_term, q_cross_term) = compute_recursive_relations::<SC>(layer_claims);
122
123        // Verify consistency
124        let expected_claim = (p_cross_term + lambda * q_cross_term) * eq_at_r_prime;
125        if expected_claim != new_claim {
126            return Err(GkrVerificationError::LayerConsistencyCheckFailed {
127                round,
128                expected: expected_claim,
129                actual: new_claim,
130            });
131        }
132
133        // Sample μⱼ and reduce to single evaluation
134        let mu = transcript.sample_ext();
135        debug!(gkr_round = round, %mu);
136        (numer_claim, denom_claim) = reduce_to_single_evaluation::<SC>(layer_claims, mu);
137        // Update evaluation point: ξ^{(j)} = (μⱼ, ρ^{(j-1)})
138        gkr_r = std::iter::once(mu).chain(round_r).collect();
139    }
140
141    Ok((numer_claim, denom_claim, gkr_r))
142}
143
144/// Verify sumcheck for a single GKR round.
145///
146/// Reduces evaluation of (p̂ⱼ₋₁ + λⱼ·q̂ⱼ₋₁)(ξ^{(j-1)}) to evaluations at the next layer.
147///
148/// # Returns
149/// `(claim, ρ^{(j-1)}, eq(ξ^{(j-1)}, ρ^{(j-1)}))` where ρ^{(j-1)} is randomly sampled from the
150/// sumcheck protocol.
151#[allow(clippy::type_complexity)]
152fn verify_gkr_sumcheck<SC: StarkProtocolConfig, TS: FiatShamirTranscript<SC>>(
153    proof: &GkrProof<SC>,
154    transcript: &mut TS,
155    round: usize,
156    mut claim: SC::EF,
157    gkr_r: &[SC::EF],
158) -> Result<(SC::EF, Vec<SC::EF>, SC::EF), GkrVerificationError<SC::EF>> {
159    debug_assert!(
160        round > 0,
161        "verify_gkr_sumcheck should not be called for round 0"
162    );
163    debug_assert_eq!(
164        gkr_r.len(),
165        round,
166        "gkr_r should have exactly round elements"
167    );
168
169    // For round j, there are j sumcheck sub-rounds
170    let expected_subrounds = round;
171    let polys = &proof.sumcheck_polys[round - 1];
172    // Note: this is already asserted by proof shape
173    if polys.len() != expected_subrounds {
174        return Err(GkrVerificationError::IncorrectSubroundCount {
175            round,
176            expected: expected_subrounds,
177            actual: polys.len(),
178        });
179    }
180    let mut gkr_r_prime = Vec::with_capacity(round);
181    let mut eq = SC::EF::ONE; // eq(ξ^{(j-1)}, ρ^{(j-1)}) computed incrementally
182
183    for (sumcheck_round, poly_evals) in polys.iter().enumerate() {
184        debug!(gkr_round = round, %sumcheck_round, sum_claim = %claim);
185        // Observe s(1), s(2), s(3) where s is the sumcheck polynomial
186        for &eval in poly_evals {
187            transcript.observe_ext(eval);
188        }
189
190        let ri = transcript.sample_ext();
191        gkr_r_prime.push(ri);
192        debug!(gkr_round = round, %sumcheck_round, r_round = %ri);
193
194        let ev0 = claim - poly_evals[0]; // s(0) = claim - s(1)
195        let evals = [ev0, poly_evals[0], poly_evals[1], poly_evals[2]];
196        claim = interpolate_cubic_at_0123(&evals, ri);
197
198        // Update eq incrementally: eq *= ξᵢ·rᵢ + (1-ξᵢ)·(1-rᵢ)
199        let xi = gkr_r[sumcheck_round];
200        eq *= xi * ri + (SC::EF::ONE - xi) * (SC::EF::ONE - ri);
201    }
202
203    Ok((claim, gkr_r_prime, eq))
204}
205
206/// Observes layer claims in the transcript.
207fn observe_layer_claims<SC: StarkProtocolConfig, TS: FiatShamirTranscript<SC>>(
208    transcript: &mut TS,
209    claims: &GkrLayerClaims<SC>,
210) {
211    transcript.observe_ext(claims.p_xi_0);
212    transcript.observe_ext(claims.q_xi_0);
213    transcript.observe_ext(claims.p_xi_1);
214    transcript.observe_ext(claims.q_xi_1);
215}
216
217/// Computes recursive relations from layer claims.
218fn compute_recursive_relations<SC: StarkProtocolConfig>(
219    claims: &GkrLayerClaims<SC>,
220) -> (SC::EF, SC::EF) {
221    let p_cross_term = claims.p_xi_0 * claims.q_xi_1 + claims.p_xi_1 * claims.q_xi_0;
222    let q_cross_term = claims.q_xi_0 * claims.q_xi_1;
223    (p_cross_term, q_cross_term)
224}
225
226/// Reduces claims to a single evaluation point using linear interpolation.
227fn reduce_to_single_evaluation<SC: StarkProtocolConfig>(
228    claims: &GkrLayerClaims<SC>,
229    mu: SC::EF,
230) -> (SC::EF, SC::EF) {
231    let numer = interpolate_linear_at_01(&[claims.p_xi_0, claims.p_xi_1], mu);
232    let denom = interpolate_linear_at_01(&[claims.q_xi_0, claims.q_xi_1], mu);
233    (numer, denom)
234}
openvm_stark_backend/verifier/fractional_sumcheck_gkr.rs

openvm_stark_backend/verifier/
fractional_sumcheck_gkr.rs
