halo2_proofs/plonk/lookup/
verifier.rs

1use std::iter;
2
3use super::super::{
4    circuit::Expression, ChallengeBeta, ChallengeGamma, ChallengeTheta, ChallengeX,
5};
6use super::Argument;
7use crate::{
8    arithmetic::{CurveAffine, FieldExt},
9    plonk::{Error, VerifyingKey},
10    poly::{multiopen::VerifierQuery, Rotation},
11    transcript::{EncodedChallenge, TranscriptRead},
12};
13use ff::Field;
14
15pub struct PermutationCommitments<C: CurveAffine> {
16    permuted_input_commitment: C,
17    permuted_table_commitment: C,
18}
19
20pub struct Committed<C: CurveAffine> {
21    permuted: PermutationCommitments<C>,
22    product_commitment: C,
23}
24
25pub struct Evaluated<C: CurveAffine> {
26    committed: Committed<C>,
27    product_eval: C::Scalar,
28    product_next_eval: C::Scalar,
29    permuted_input_eval: C::Scalar,
30    permuted_input_inv_eval: C::Scalar,
31    permuted_table_eval: C::Scalar,
32}
33
34impl<F: FieldExt> Argument<F> {
35    pub(in crate::plonk) fn read_permuted_commitments<
36        C: CurveAffine,
37        E: EncodedChallenge<C>,
38        T: TranscriptRead<C, E>,
39    >(
40        &self,
41        transcript: &mut T,
42    ) -> Result<PermutationCommitments<C>, Error> {
43        let permuted_input_commitment = transcript.read_point()?;
44        let permuted_table_commitment = transcript.read_point()?;
45
46        Ok(PermutationCommitments {
47            permuted_input_commitment,
48            permuted_table_commitment,
49        })
50    }
51}
52
53impl<C: CurveAffine> PermutationCommitments<C> {
54    pub(in crate::plonk) fn read_product_commitment<
55        E: EncodedChallenge<C>,
56        T: TranscriptRead<C, E>,
57    >(
58        self,
59        transcript: &mut T,
60    ) -> Result<Committed<C>, Error> {
61        let product_commitment = transcript.read_point()?;
62
63        Ok(Committed {
64            permuted: self,
65            product_commitment,
66        })
67    }
68}
69
70impl<C: CurveAffine> Committed<C> {
71    pub(crate) fn evaluate<E: EncodedChallenge<C>, T: TranscriptRead<C, E>>(
72        self,
73        transcript: &mut T,
74    ) -> Result<Evaluated<C>, Error> {
75        let product_eval = transcript.read_scalar()?;
76        let product_next_eval = transcript.read_scalar()?;
77        let permuted_input_eval = transcript.read_scalar()?;
78        let permuted_input_inv_eval = transcript.read_scalar()?;
79        let permuted_table_eval = transcript.read_scalar()?;
80
81        Ok(Evaluated {
82            committed: self,
83            product_eval,
84            product_next_eval,
85            permuted_input_eval,
86            permuted_input_inv_eval,
87            permuted_table_eval,
88        })
89    }
90}
91
92impl<C: CurveAffine> Evaluated<C> {
93    pub(in crate::plonk) fn expressions<'a>(
94        &'a self,
95        l_0: C::Scalar,
96        l_last: C::Scalar,
97        l_blind: C::Scalar,
98        argument: &'a Argument<C::Scalar>,
99        theta: ChallengeTheta<C>,
100        beta: ChallengeBeta<C>,
101        gamma: ChallengeGamma<C>,
102        advice_evals: &[C::Scalar],
103        fixed_evals: &[C::Scalar],
104        instance_evals: &[C::Scalar],
105    ) -> impl Iterator<Item = C::Scalar> + 'a {
106        let active_rows = C::Scalar::one() - (l_last + l_blind);
107
108        let product_expression = || {
109            // z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
110            // - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
111            let left = self.product_next_eval
112                * &(self.permuted_input_eval + &*beta)
113                * &(self.permuted_table_eval + &*gamma);
114
115            let compress_expressions = |expressions: &[Expression<C::Scalar>]| {
116                expressions
117                    .iter()
118                    .map(|expression| {
119                        expression.evaluate(
120                            &|scalar| scalar,
121                            &|_| panic!("virtual selectors are removed during optimization"),
122                            &|index, _, _| fixed_evals[index],
123                            &|index, _, _| advice_evals[index],
124                            &|index, _, _| instance_evals[index],
125                            &|a| -a,
126                            &|a, b| a + &b,
127                            &|a, b| a * &b,
128                            &|a, scalar| a * &scalar,
129                        )
130                    })
131                    .fold(C::Scalar::zero(), |acc, eval| acc * &*theta + &eval)
132            };
133            let right = self.product_eval
134                * &(compress_expressions(&argument.input_expressions) + &*beta)
135                * &(compress_expressions(&argument.table_expressions) + &*gamma);
136
137            (left - &right) * &active_rows
138        };
139
140        std::iter::empty()
141            .chain(
142                // l_0(X) * (1 - z'(X)) = 0
143                Some(l_0 * &(C::Scalar::one() - &self.product_eval)),
144            )
145            .chain(
146                // l_last(X) * (z(X)^2 - z(X)) = 0
147                Some(l_last * &(self.product_eval.square() - &self.product_eval)),
148            )
149            .chain(
150                // (1 - (l_last(X) + l_blind(X))) * (
151                //   z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
152                //   - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
153                // ) = 0
154                Some(product_expression()),
155            )
156            .chain(Some(
157                // l_0(X) * (a'(X) - s'(X)) = 0
158                l_0 * &(self.permuted_input_eval - &self.permuted_table_eval),
159            ))
160            .chain(Some(
161                // (1 - (l_last(X) + l_blind(X))) * (a′(X) − s′(X))⋅(a′(X) − a′(\omega^{-1} X)) = 0
162                (self.permuted_input_eval - &self.permuted_table_eval)
163                    * &(self.permuted_input_eval - &self.permuted_input_inv_eval)
164                    * &active_rows,
165            ))
166    }
167
168    pub(in crate::plonk) fn queries<'r, 'params: 'r>(
169        &'r self,
170        vk: &'r VerifyingKey<C>,
171        x: ChallengeX<C>,
172    ) -> impl Iterator<Item = VerifierQuery<'r, 'params, C>> + Clone {
173        let x_inv = vk.domain.rotate_omega(*x, Rotation::prev());
174        let x_next = vk.domain.rotate_omega(*x, Rotation::next());
175
176        iter::empty()
177            // Open lookup product commitment at x
178            .chain(Some(VerifierQuery::new_commitment(
179                &self.committed.product_commitment,
180                *x,
181                self.product_eval,
182            )))
183            // Open lookup input commitments at x
184            .chain(Some(VerifierQuery::new_commitment(
185                &self.committed.permuted.permuted_input_commitment,
186                *x,
187                self.permuted_input_eval,
188            )))
189            // Open lookup table commitments at x
190            .chain(Some(VerifierQuery::new_commitment(
191                &self.committed.permuted.permuted_table_commitment,
192                *x,
193                self.permuted_table_eval,
194            )))
195            // Open lookup input commitments at \omega^{-1} x
196            .chain(Some(VerifierQuery::new_commitment(
197                &self.committed.permuted.permuted_input_commitment,
198                x_inv,
199                self.permuted_input_inv_eval,
200            )))
201            // Open lookup product commitment at \omega x
202            .chain(Some(VerifierQuery::new_commitment(
203                &self.committed.product_commitment,
204                x_next,
205                self.product_next_eval,
206            )))
207    }
208}