halo2_axiom/plonk/
lookup.rs

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

halo2_axiom/plonk/
lookup.rs
