2021-02-10 03:36:25 -08:00
|
|
|
|
use super::circuit::Expression;
|
|
|
|
|
use ff::Field;
|
2020-11-30 22:53:20 -08:00
|
|
|
|
|
2021-01-20 05:47:55 -08:00
|
|
|
|
pub(crate) mod prover;
|
|
|
|
|
pub(crate) mod verifier;
|
2020-11-30 22:53:20 -08:00
|
|
|
|
|
|
|
|
|
#[derive(Clone, Debug)]
|
2021-02-10 03:36:25 -08:00
|
|
|
|
pub(crate) struct Argument<F: Field> {
|
2021-02-11 18:24:55 -08:00
|
|
|
|
pub input_expressions: Vec<Expression<F>>,
|
|
|
|
|
pub table_expressions: Vec<Expression<F>>,
|
2020-11-30 22:53:20 -08:00
|
|
|
|
}
|
|
|
|
|
|
2021-02-10 03:36:25 -08:00
|
|
|
|
impl<F: Field> Argument<F> {
|
2021-05-26 16:37:32 -07:00
|
|
|
|
/// Constructs a new lookup argument.
|
|
|
|
|
///
|
|
|
|
|
/// `table_map` is a sequence of `(input, table)` tuples.
|
|
|
|
|
pub fn new(table_map: Vec<(Expression<F>, Expression<F>)>) -> Self {
|
|
|
|
|
let (input_expressions, table_expressions) = table_map.into_iter().unzip();
|
2020-11-30 22:53:20 -08:00
|
|
|
|
Argument {
|
2021-05-26 16:37:32 -07:00
|
|
|
|
input_expressions,
|
|
|
|
|
table_expressions,
|
2020-11-30 22:53:20 -08:00
|
|
|
|
}
|
|
|
|
|
}
|
2020-12-22 07:54:41 -08:00
|
|
|
|
|
|
|
|
|
pub(crate) fn required_degree(&self) -> usize {
|
2021-02-11 18:24:55 -08:00
|
|
|
|
assert_eq!(self.input_expressions.len(), self.table_expressions.len());
|
2020-12-22 07:54:41 -08:00
|
|
|
|
|
2021-07-08 11:46:38 -07:00
|
|
|
|
// The first value in the permutation poly should be one.
|
2020-12-22 07:54:41 -08:00
|
|
|
|
// degree 2:
|
2021-07-08 11:46:38 -07:00
|
|
|
|
// l_0(X) * (1 - z(X)) = 0
|
2020-12-22 07:54:41 -08:00
|
|
|
|
//
|
2021-07-09 08:14:52 -07:00
|
|
|
|
// The "last" value in the permutation poly should be a boolean, for
|
|
|
|
|
// completeness and soundness.
|
2021-07-08 11:46:38 -07:00
|
|
|
|
// degree 3:
|
|
|
|
|
// l_last(X) * (z(X)^2 - z(X)) = 0
|
2020-12-22 07:54:41 -08:00
|
|
|
|
//
|
2021-07-08 11:46:38 -07:00
|
|
|
|
// Enable the permutation argument for only the rows involved.
|
|
|
|
|
// degree (2 + input_degree + table_degree) or 4, whichever is larger:
|
2021-07-09 08:18:45 -07:00
|
|
|
|
// (1 - (l_last + l_blind)) * (
|
2021-07-08 11:46:38 -07:00
|
|
|
|
// z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
|
|
|
|
|
// - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
|
|
|
|
|
// ) = 0
|
|
|
|
|
//
|
|
|
|
|
// The first two values of a' and s' should be the same.
|
2020-12-22 07:54:41 -08:00
|
|
|
|
// degree 2:
|
|
|
|
|
// l_0(X) * (a'(X) - s'(X)) = 0
|
|
|
|
|
//
|
2021-07-08 11:46:38 -07:00
|
|
|
|
// Either the two values are the same, or the previous
|
|
|
|
|
// value of a' is the same as the current value.
|
|
|
|
|
// degree 3:
|
2021-07-09 11:44:27 -07:00
|
|
|
|
// (1 - (l_last + l_blind)) * (a′(X) − s′(X))⋅(a′(X) − a′(\omega^{-1} X)) = 0
|
2021-02-11 17:40:53 -08:00
|
|
|
|
let mut input_degree = 1;
|
2021-02-11 18:24:55 -08:00
|
|
|
|
for expr in self.input_expressions.iter() {
|
2021-02-11 17:40:53 -08:00
|
|
|
|
input_degree = std::cmp::max(input_degree, expr.degree());
|
|
|
|
|
}
|
|
|
|
|
let mut table_degree = 1;
|
2021-02-11 18:24:55 -08:00
|
|
|
|
for expr in self.table_expressions.iter() {
|
2021-02-11 17:40:53 -08:00
|
|
|
|
table_degree = std::cmp::max(table_degree, expr.degree());
|
|
|
|
|
}
|
|
|
|
|
|
2021-07-13 14:46:52 -07:00
|
|
|
|
// In practice because input_degree and table_degree are initialized to
|
|
|
|
|
// one, the latter half of this max() invocation is at least 4 always,
|
|
|
|
|
// rendering this call pointless except to be explicit in case we change
|
|
|
|
|
// the initialization of input_degree/table_degree in the future.
|
|
|
|
|
std::cmp::max(
|
|
|
|
|
// (1 - (l_last + l_blind)) z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
|
|
|
|
|
4,
|
|
|
|
|
// (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)
|
|
|
|
|
2 + input_degree + table_degree,
|
|
|
|
|
)
|
2020-12-22 07:54:41 -08:00
|
|
|
|
}
|
2020-11-30 22:53:20 -08:00
|
|
|
|
}
|