halo2_proofs/plonk/
lookup.rs

Help
1use super::circuit::Expression;
2use ff::Field;
3
4pub(crate) mod prover;
5pub(crate) mod verifier;
6
7#[derive(Clone, Debug)]
8pub(crate) struct Argument<F: Field> {
9    pub input_expressions: Vec<Expression<F>>,
10    pub table_expressions: Vec<Expression<F>>,
11}
12
13impl<F: Field> Argument<F> {
14    /// Constructs a new lookup argument.
15    ///
16    /// `table_map` is a sequence of `(input, table)` tuples.
17    pub fn new(table_map: Vec<(Expression<F>, Expression<F>)>) -> Self {
18        let (input_expressions, table_expressions) = table_map.into_iter().unzip();
19        Argument {
20            input_expressions,
21            table_expressions,
22        }
23    }
24
25    pub(crate) fn required_degree(&self) -> usize {
26        assert_eq!(self.input_expressions.len(), self.table_expressions.len());
27
28        // The first value in the permutation poly should be one.
29        // degree 2:
30        // l_0(X) * (1 - z(X)) = 0
31        //
32        // The "last" value in the permutation poly should be a boolean, for
33        // completeness and soundness.
34        // degree 3:
35        // l_last(X) * (z(X)^2 - z(X)) = 0
36        //
37        // Enable the permutation argument for only the rows involved.
38        // degree (2 + input_degree + table_degree) or 4, whichever is larger:
39        // (1 - (l_last(X) + l_blind(X))) * (
40        //   z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
41        //   - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
42        // ) = 0
43        //
44        // The first two values of a' and s' should be the same.
45        // degree 2:
46        // l_0(X) * (a'(X) - s'(X)) = 0
47        //
48        // Either the two values are the same, or the previous
49        // value of a' is the same as the current value.
50        // degree 3:
51        // (1 - (l_last(X) + l_blind(X))) * (a′(X) − s′(X))⋅(a′(X) − a′(\omega^{-1} X)) = 0
52        let mut input_degree = 1;
53        for expr in self.input_expressions.iter() {
54            input_degree = std::cmp::max(input_degree, expr.degree());
55        }
56        let mut table_degree = 1;
57        for expr in self.table_expressions.iter() {
58            table_degree = std::cmp::max(table_degree, expr.degree());
59        }
60
61        // In practice because input_degree and table_degree are initialized to
62        // one, the latter half of this max() invocation is at least 4 always,
63        // rendering this call pointless except to be explicit in case we change
64        // the initialization of input_degree/table_degree in the future.
65        std::cmp::max(
66            // (1 - (l_last + l_blind)) z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
67            4,
68            // (1 - (l_last + l_blind)) z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
69            2 + input_degree + table_degree,
70        )
71    }
72}
halo2_proofs/plonk/lookup.rs

halo2_proofs/plonk/
lookup.rs
