labrador/
verifier.rs

1//! Labrador Verifier
2//!
3//! This module implements the **verifier** side of the protocol in
4//! Fig. 2 (and the verification algorithm in Fig. 3) of the paper.  The prover
5//! proof `proof` is accepted **iff** every arithmetic check listed in Fig. 2
6//! and lines 8–20 of Fig. 3 succeeds.
7//!
8//! The verifier receives:
9//! * a public statement `st`;
10//! * the CRS containing the Ajtai commitment matrices \(\mathbf{A},\mathbf{B},\mathbf{C},\mathbf{D}\);
11//! * a proof `proof` comprising
12//!   \[(\mathbf{u}_1,\mathbf{u}_2,\,\vec p,\,b''^{(k)}\,\vec z,\tilde\mathbf t,\tilde\mathbf g,\tilde\mathbf h)\]  
13//!   exactly as dispatched by the prover.
14//!
15//! ## Outline of the nine verifier checks
16//! The implementation follows Fig. 3 literally:
17//!
18//! On failure the function returns [`VerifierError`] precisely identifying the
19//! violated condition.
20
21#![allow(clippy::result_large_err)]
22
23use crate::commitments::{
24    common_instances::AjtaiInstances,
25    outer_commitments::{self, DecompositionParameters},
26};
27use crate::core::aggregate::{FunctionsAggregation, ZeroConstantFunctionsAggregation};
28use crate::core::{inner_product, jl::Projection};
29use crate::relation::env_params;
30use crate::relation::{env_params::EnvironmentParameters, statement::Statement};
31use crate::ring::{rq::Rq, rq_matrix::RqMatrix, rq_vector::RqVector, zq::Zq, Norms};
32use crate::transcript::{LabradorTranscript, Sponge};
33use thiserror::Error;
34
35#[derive(Debug, Error)]
36pub enum VerifierError {
37    #[error("matrix not symmetric at ({i},{j}): expected {expected:?}, found {found:?}")]
38    NotSymmetric {
39        i: usize,
40        j: usize,
41        expected: Rq,
42        found: Rq,
43    },
44    #[error("B0 mismatch at index {index}: expected {expected}, computed {computed}")]
45    B0Mismatch {
46        index: usize,
47        expected: Zq,
48        computed: Zq,
49    },
50    #[error("Computed Norm: {norm} -- Maximum Bound {allowed}, Step: {step}")]
51    NormSumExceeded {
52        norm: u128,
53        allowed: u128,
54        step: String,
55    },
56    #[error("A·z check failed: expected {expected:?}, computed {computed:?}")]
57    AzError {
58        computed: RqVector,
59        expected: RqVector,
60    },
61    #[error("⟨z,z⟩ mismatch: expected {expected:?}, computed {computed:?}")]
62    ZInnerError { computed: Rq, expected: Rq },
63    #[error("φ(z) mismatch: expected {expected:?}, computed {computed:?}")]
64    PhiError { computed: Rq, expected: Rq },
65    #[error("relation check failed")]
66    RelationCheckFailed,
67    #[error("outer commitment mismatch: expected {expected:?}, computed {computed:?}")]
68    OuterCommitError {
69        computed: RqVector,
70        expected: RqVector,
71    },
72    #[error(transparent)]
73    DecompositionError(#[from] outer_commitments::DecompositionError),
74}
75
76/// Implements the algorithm executed by the verifier \(\mathcal{V}\) in the paper.
77pub struct LabradorVerifier<'a> {
78    /// System‑wide environment parameters like rank and multiplicity.
79    params: &'a EnvironmentParameters,
80    /// Common reference string (CRS) holding the commitment matrices
81    /// \(\mathbf{A},\mathbf{B},\mathbf{C},\mathbf{D}\).
82    crs: &'a AjtaiInstances,
83    /// Public relation statement.
84    st: &'a Statement,
85    /* --- aggregation instances ---------------------------------------------------------- */
86    constant_aggregator: ZeroConstantFunctionsAggregation<'a>,
87    funcs_aggregator: FunctionsAggregation<'a>,
88}
89
90impl<'a> LabradorVerifier<'a> {
91    /// Constructs a new verifier instance.
92    pub fn new(
93        params: &'a EnvironmentParameters,
94        crs: &'a AjtaiInstances,
95        st: &'a Statement,
96    ) -> Self {
97        Self {
98            params,
99            crs,
100            st,
101            constant_aggregator: ZeroConstantFunctionsAggregation::new(params),
102            funcs_aggregator: FunctionsAggregation::new(params),
103        }
104    }
105
106    /// Validate JL projection bound  (Fig. 2):
107    /// \[
108    ///   \|\vec p\|_2^2 = \sum_{j=1}^{2\lambda} p_j^2 \;\stackrel{?}{\le}\; 128\,\beta^2.
109    /// \]
110    fn check_vector_p_norm_bound<S: Sponge>(
111        &self,
112        proof: &LabradorTranscript<S>,
113        transcript: &mut LabradorTranscript<S>,
114    ) -> Result<Projection, VerifierError> {
115        transcript.absorb_u1(&proof.u1);
116
117        let projections = transcript.generate_projections(
118            env_params::SECURITY_PARAMETER,
119            self.params.rank,
120            self.params.multiplicity,
121        );
122        transcript.absorb_vector_p(&proof.vector_p);
123        if proof.vector_p.l2_norm_squared() > 128 * self.params.beta_sq {
124            return Err(VerifierError::NormSumExceeded {
125                norm: proof.vector_p.l2_norm_squared(),
126                allowed: 128 * self.params.beta_sq,
127                step: String::from("vector p norm check"),
128            });
129        }
130        Ok(projections)
131    }
132
133    /// Validate b'' constant term (Fig. 2):
134    /// For every `k`, verifies
135    /// \[
136    ///   b_{0}^{''(k)} \stackrel{?}{=} \sum_{l=1}^{L} \psi_{l}^{(k)}\,b_{0}^{'(l)}
137    ///                    + \langle\,\vec\omega^{(k)},\vec p\rangle .
138    /// \]
139    #[allow(clippy::type_complexity)]
140    fn check_b_double_prime_constant<S: Sponge>(
141        &self,
142        proof: &LabradorTranscript<S>,
143        transcript: &mut LabradorTranscript<S>,
144    ) -> Result<(Vec<Vec<Zq>>, Vec<Vec<Zq>>), VerifierError> {
145        let size_of_psi = usize::div_ceil(env_params::SECURITY_PARAMETER, self.params.log_q);
146        let size_of_omega = size_of_psi;
147        let psi = transcript.generate_vector_psi(size_of_psi, self.params.constraint_l);
148        let omega = transcript.generate_vector_omega(size_of_omega, env_params::SECURITY_PARAMETER);
149        transcript.absorb_vector_b_ct_aggr(&proof.b_ct_aggr);
150
151        for k in 0..self.params.kappa {
152            let b_0_poly = proof.b_ct_aggr.elements()[k].coeffs()[0];
153            let mut b_0: Zq = (0..self.params.constraint_l)
154                .map(|l| psi[k][l] * self.st.b_0_ct[l])
155                .sum();
156
157            let inner_omega_p =
158                inner_product::compute_linear_combination(&omega[k], &proof.vector_p);
159            b_0 += inner_omega_p;
160            if b_0 != b_0_poly {
161                return Err(VerifierError::B0Mismatch {
162                    index: k,
163                    expected: b_0_poly,
164                    computed: b_0,
165                });
166            }
167        }
168
169        Ok((psi, omega))
170    }
171
172    /// Validate consolidated norm bound  (Fig. 3 line 14):
173    /// \[
174    ///  \sum_{\ell=0}^{1}\|\mathbf z^{(\ell)}\|_2^2
175    ///   + \sum_{i=1}^r\sum_{k=0}^{t_1-1}\|\mathbf t_i^{(k)}\|_2^2
176    ///   + \sum_{1\le i\le j\le r}\sum_{k=0}^{t_2-1}\|\mathbf g_{ij}^{(k)}\|_2^2
177    ///   + \sum_{1\le i\le j\le r}\sum_{k=0}^{t_1-1}\|\mathbf h_{ij}^{(k)}\|_2^2
178    ///     \stackrel{?}{\le} (\beta')^2 .
179    ///     \]
180    fn check_final_norm_sum<S: Sponge>(
181        &self,
182        proof: &LabradorTranscript<S>,
183    ) -> Result<(), VerifierError> {
184        // decompose z into z = z^(0) + z^(1) * b, only two parts.
185        let z_ij = proof.z.decompose(self.params.b, 2);
186        let t_ij: Vec<Vec<RqVector>> = proof
187            .t
188            .elements()
189            .iter()
190            .map(|i| RqVector::decompose(i, self.params.b, self.params.t_1))
191            .collect();
192        let g_ij: Vec<Vec<RqVector>> = proof
193            .g
194            .elements()
195            .iter()
196            .map(|i| RqVector::decompose(i, self.params.b, self.params.t_2))
197            .collect();
198        let h_ij: Vec<Vec<RqVector>> = proof
199            .h
200            .elements()
201            .iter()
202            .map(|i| RqVector::decompose(i, self.params.b, self.params.t_1))
203            .collect();
204        let norm_z_ij = z_ij.iter().fold(0, |acc, p| acc + p.l2_norm_squared());
205        let norm_t_ij = Self::norm_squared(&t_ij);
206        let norm_g_ij = Self::norm_squared(&g_ij);
207        let norm_h_ij = Self::norm_squared(&h_ij);
208        let norm_sum = norm_z_ij + norm_t_ij + norm_g_ij + norm_h_ij;
209
210        if norm_sum > self.params.beta_prime_sq {
211            return Err(VerifierError::NormSumExceeded {
212                norm: norm_sum,
213                allowed: self.params.beta_prime_sq,
214                step: String::from("Step 14 in verification"),
215            });
216        }
217        Ok(())
218    }
219
220    /// Validate amortised Ajtai relation (Fig. 3 line 15):
221    /// \[
222    ///   \mathbf A\,\mathbf z \stackrel{?}{=} \sum_{i=1}^r c_i\,\tilde\mathbf t_i
223    /// \]
224    /// where the challenges `c_i` are re‑sampled locally from the sponge.
225    fn check_az_amortization_correctness<S: Sponge>(
226        &self,
227        proof: &LabradorTranscript<S>,
228        transcript: &mut LabradorTranscript<S>,
229    ) -> Result<RqVector, VerifierError> {
230        let challenges =
231            transcript.generate_challenges(env_params::OPERATOR_NORM, self.params.multiplicity);
232        let az = self.crs.commitment_scheme_a.matrix() * &proof.z;
233        let ct_sum =
234            inner_product::compute_linear_combination(proof.t.elements(), challenges.elements());
235        if az != ct_sum {
236            return Err(VerifierError::AzError {
237                computed: az,
238                expected: ct_sum,
239            });
240        }
241        Ok(challenges)
242    }
243
244    /// Validate the following (Fig. 3 line 16):
245    /// \[
246    ///   \langle\mathbf z,\mathbf z\rangle \stackrel{?}{=}
247    ///   \sum_{i,j} g_{ij}\,c_i\,c_j .
248    /// \]
249    fn check_g_correctness<S: Sponge>(
250        &self,
251        proof: &LabradorTranscript<S>,
252        challenges: &RqVector,
253    ) -> Result<(), VerifierError> {
254        let z_inner =
255            inner_product::compute_linear_combination(proof.z.elements(), proof.z.elements());
256        let sum_gij_cij = Self::calculate_gh_ci_cj(&proof.g, challenges, self.params.multiplicity);
257
258        if z_inner != sum_gij_cij {
259            return Err(VerifierError::ZInnerError {
260                computed: z_inner,
261                expected: sum_gij_cij,
262            });
263        }
264        Ok(())
265    }
266
267    /// Validate the following (Fig. 3 line 17):
268    /// \[
269    ///   2\,\sum_{i=1}^r \langle\varphi_i,\mathbf z\rangle c_i
270    ///   \stackrel{?}{=} \sum_{i,j} h_{ij}\,c_i\,c_j .
271    /// \]
272    fn check_h_correctness<S: Sponge>(
273        &self,
274        proof: &LabradorTranscript<S>,
275        challenges: &RqVector,
276    ) -> Result<(), VerifierError> {
277        let sum_phi_z_c =
278            Self::calculate_phi_z_c(self.funcs_aggregator.get_appr_phi(), challenges, &proof.z);
279        let sum_hij_cij = Self::calculate_gh_ci_cj(&proof.h, challenges, self.params.multiplicity);
280
281        // Left side multiple by 2 because of when we calculate h_ij, we didn't apply the division (divided by 2)
282        if &sum_phi_z_c * &Zq::TWO != sum_hij_cij {
283            return Err(VerifierError::PhiError {
284                computed: &sum_phi_z_c * &Zq::TWO,
285                expected: sum_hij_cij,
286            });
287        }
288        Ok(())
289    }
290
291    /// Validate the following (Fig. 3 line 18):
292    /// \[
293    ///   2\sum_{i,j} a_{ij} g_{ij} + \sum_i h_{ii}\;\stackrel{?}{=}\; 2b .
294    /// \]
295    fn check_aggregated_relation<S: Sponge>(
296        &self,
297        proof: &LabradorTranscript<S>,
298    ) -> Result<(), VerifierError> {
299        let r = self.funcs_aggregator.get_agg_a().elements().len();
300
301        let mut sum_a_primes_g = Rq::zero();
302        // walk only over the stored half: i ≤ j
303        for i in 0..r {
304            for j in 0..r {
305                sum_a_primes_g = &sum_a_primes_g
306                    + &(self.funcs_aggregator.get_agg_a().get_cell(i, j) * proof.g.get_cell(i, j));
307            }
308        }
309
310        let sum_h_ii = (0..r).fold(Rq::zero(), |acc, i| &acc + proof.h.get_cell(i, i));
311
312        let b_primes2 = self.funcs_aggregator.get_aggr_b() * &Zq::TWO;
313        let sum_a_primes_g2 = &sum_a_primes_g * &Zq::TWO;
314
315        if &sum_a_primes_g2 + &sum_h_ii != b_primes2 {
316            return Err(VerifierError::RelationCheckFailed);
317        }
318        Ok(())
319    }
320
321    /// Validate uter commitment u1 (Fig. 3 line 19):
322    /// \[
323    ///   \mathbf u_1^{\text{re}} = \sum_{i=1}^r\sum_{k=0}^{t_1-1}\mathbf B_{ik}\,\mathbf t_i^{(k)}
324    ///          + \sum_{1\le i\le j\le r}\sum_{k=0}^{t_2-1}\mathbf C_{ijk}\,\mathbf g_{ij}^{(k)}
325    /// \]
326    fn check_u1<S: Sponge>(&self, proof: &LabradorTranscript<S>) -> Result<(), VerifierError> {
327        let u_1 = &proof.u1;
328        let commitment_u1 = outer_commitments::compute_u1(
329            self.crs,
330            &proof.t,
331            DecompositionParameters::new(self.params.b, self.params.t_1)?,
332            &proof.g,
333            DecompositionParameters::new(self.params.b, self.params.t_2)?,
334        );
335
336        if proof.u1 != commitment_u1 {
337            return Err(VerifierError::OuterCommitError {
338                computed: u_1.clone(),
339                expected: commitment_u1,
340            });
341        }
342        Ok(())
343    }
344
345    /// Validate outer commitment u2 (Fig. 3 line 20):
346    /// \[
347    ///   \mathbf u_2^{\text{re}} = \sum_{1\le i\le j\le r}\sum_{k=0}^{t_1-1}
348    ///                              \mathbf D_{ijk}\,\mathbf h_{ij}^{(k)}
349    /// \]
350    /// and checks equality with the transcript.
351    fn check_u2<S: Sponge>(&self, proof: &LabradorTranscript<S>) -> Result<(), VerifierError> {
352        let commitment_u2 = outer_commitments::compute_u2(
353            self.crs,
354            &proof.h,
355            DecompositionParameters::new(self.params.b, self.params.t_1)?,
356        );
357
358        if proof.u2 != commitment_u2 {
359            return Err(VerifierError::OuterCommitError {
360                computed: commitment_u2,
361                expected: proof.u2.clone(),
362            });
363        }
364        Ok(())
365    }
366
367    /// calculate the right hand side of line 16 or line 17, \sum(g_ij * c_i * c_j) or \sum(h_ij * c_i * c_j)
368    fn calculate_gh_ci_cj(x_ij: &RqMatrix, random_c: &RqVector, r: usize) -> Rq {
369        (0..r)
370            .map(|i| {
371                (0..r)
372                    .map(|j| {
373                        &(x_ij.get_cell(i, j) * &random_c.elements()[i]) * &random_c.elements()[j]
374                    })
375                    .fold(Rq::zero(), |acc, x| &acc + &x)
376            })
377            .fold(Rq::zero(), |acc, x| &acc + &x)
378    }
379
380    /// calculate the left hand side of line 17, \sum(<\phi_z, z> * c_i)
381    fn calculate_phi_z_c(phi: &[RqVector], c: &RqVector, z: &RqVector) -> Rq {
382        phi.iter()
383            .zip(c.elements())
384            .map(|(phi_i, c_i)| {
385                &(inner_product::compute_linear_combination(phi_i.elements(), z.elements())) * c_i
386            })
387            .fold(Rq::zero(), |acc, x| &acc + &x)
388    }
389
390    fn norm_squared(polys: &[Vec<RqVector>]) -> u128 {
391        polys.iter().fold(0, |acc, poly| {
392            acc + poly.iter().fold(0, |acc, p| acc + p.l2_norm_squared())
393        })
394    }
395
396    /// Verifies a prover transcript.
397    /// Executes **all** verifier steps (Fig. 2 page 17, Fig. 3 page 18).
398    ///
399    /// Returns `Ok(true)` if *all* checks succeed, otherwise an explanatory
400    /// [`VerifierError`].  The sponge seeded inside this routine **must** be
401    /// identical to the prover’s so that the generated randomizers match.
402    pub fn verify<S: Sponge>(
403        &mut self,
404        proof: &LabradorTranscript<S>,
405    ) -> Result<bool, VerifierError> {
406        // fresh sponge — deterministic (Todo: Add domain separator)
407        let mut transcript = LabradorTranscript::new(S::default());
408
409        // --- Fig. 2: JL Projections Norm Check ------------------------------------------------------------------
410        let projections = self.check_vector_p_norm_bound(proof, &mut transcript)?;
411
412        // --- Fig. 2: Constant of Constant Functions Aggregation Check -------------------------------------------
413        let (psi, omega) = self.check_b_double_prime_constant(proof, &mut transcript)?;
414
415        // --- Fig. 3, Line 14: Check Prover's Last Message Norm --------------------------------------------------
416        self.check_final_norm_sum(proof)?;
417
418        // Generate Randomness for Next Steps
419        let vector_alpha = transcript.generate_rq_vector(self.params.constraint_k);
420        let vector_beta = transcript.generate_rq_vector(usize::div_ceil(
421            env_params::SECURITY_PARAMETER,
422            self.params.log_q,
423        ));
424        transcript.absorb_u2(&proof.u2);
425
426        // --- Fig. 3, Line 15: Check Correctness of Amortization --------------------------------------------------
427        let challenges = self.check_az_amortization_correctness(proof, &mut transcript)?;
428
429        // --- Fig. 3, Line 16: Check Relation of z, g, and challenges ---------------------------------------------
430        self.check_g_correctness(proof, &challenges)?;
431
432        // Generate Randomness for Next Steps
433        self.constant_aggregator.calculate_agg_phi_double_prime(
434            &self.st.phi_ct,
435            &projections.get_conjugated_projection_matrices(),
436            &psi,
437            &omega,
438        );
439        self.funcs_aggregator.calculate_aggr_phi(
440            &self.st.phi_constraint,
441            self.constant_aggregator.get_phi_double_prime(),
442            &vector_alpha,
443            &vector_beta,
444        );
445        // --- Fig. 3, Line 17: Check Relation of z, \varphi, h, and challenges -------------------------------------
446        self.check_h_correctness(proof, &challenges)?;
447
448        self.constant_aggregator
449            .calculate_agg_a_double_prime(&psi, &self.st.a_ct);
450        self.funcs_aggregator.calculate_agg_a(
451            &self.st.a_constraint,
452            self.constant_aggregator.get_alpha_double_prime(),
453            &vector_alpha,
454            &vector_beta,
455        );
456        self.funcs_aggregator.calculate_aggr_b(
457            &self.st.b_constraint,
458            &proof.b_ct_aggr,
459            &vector_alpha,
460            &vector_beta,
461        );
462        // --- Fig. 3, Line 18: Check Aggregated Elements Equal to 0 -----------------------------------------------
463        self.check_aggregated_relation(proof)?;
464
465        // --- Fig. 3, Line 19-20: Check Correntness of u1 and u2---------------------------------------------------
466        self.check_u1(proof)?;
467        self.check_u2(proof)?;
468
469        Ok(true)
470    }
471}
472
473#[cfg(test)]
474mod tests {
475    use super::*;
476    use crate::prover::LabradorProver;
477    use crate::relation::witness::Witness;
478    use crate::transcript::sponges::shake::ShakeSponge;
479
480    #[test]
481    fn test_verify() {
482        let ep_1 = EnvironmentParameters::default();
483        // generate a random witness based on ep above
484        let witness_1 = Witness::new(ep_1.rank, ep_1.multiplicity, ep_1.beta_sq);
485        // generate public statements based on witness_1
486        let st: Statement = Statement::new(&witness_1, &ep_1);
487        // generate the common reference string matrices
488        let crs = AjtaiInstances::new(&ep_1);
489
490        // create a new prover
491        let mut prover = LabradorProver::new(&ep_1, &crs, &witness_1, &st);
492        let proof: LabradorTranscript<ShakeSponge> = prover.prove().unwrap();
493
494        // create a new verifier
495        let mut verifier = LabradorVerifier::new(&ep_1, &crs, &st);
496        let result = verifier.verify(&proof);
497        assert!(result.unwrap());
498    }
499}
labrador/verifier.rs

labrador/
verifier.rs
