%20and%20Code%20Analysis_%20(1).png)
When representing computations as circuits, there are often complex operations such as bitwise XOR and bitwise AND. For example, performing a bitwise XOR operation on two 32-bit bitstrings usually requires hundreds of addition and multiplication gates, significantly increasing circuit size. Introducing the Lookup argument protocol effectively reduces circuit complexity.
To prove that two 32-bit bitstrings and their corresponding outputs satisfy a bitwise XOR relationship, one can encode the inputs and outputs into a lookup table of size \(2^{32}\), then demonstrate that the inputs and outputs align with a specific row in the table. To reduce table size, smaller tables such as \(2^{16}\) or \(2^{8}\) can be used, along with constraints between bits to balance table size and proof speed.
The Lookup argument is used to verify whether elements of one set appear in another set without revealing additional information. In circuit design, Lookup arguments are frequently applied to verify complex constraints, especially in cases involving non-gate or non-scalar multiplication operations. They are mainly used in proving systems like Plonkish and Halo2. This method significantly reduces circuit constraints and enhances proof efficiency. The specific construction steps are as follows:
The Logup protocol originates from the CQ protocol, which uses logarithms and derivatives from higher mathematics to reduce set membership proofs to simpler problems. Its workflow, as shown in Figure 1, involves the following steps:
1. Construct Lookup Items and Table:
2. Formulate LHS and RHS Expressions:
3. Verify Logarithmic Equality: Convert the multiplicative forms into logarithmic sums:
\[\sum_{j=1}^{n}log(\beta+f_{j})=\sum_{i=1}^{N}m_{i}\cdot log(\beta+t_{i})\]
4. Check Fractional Equality: Validate the equality:
\[\sum_{j=1}^{n}\frac{1}{\beta+f_{j}}=\sum_{i=1}^{N}\frac{m_{i}}{\beta+r_{i}}\]
If the equation holds, the lookup values are confirmed to be in the table.
The Logup protocol extends the CQ protocol from univariate polynomials to multivariate polynomials, adapting to zkSNARK algorithms with hypercube implementations. The zkSNARK prover uses the univariate version.
The core of the Logup protocol’s Lookup argument relies on the following mathematical theorem:
Lemma (Set Inclusion): Let \(F\) be a field with characteristic \(p > N\), and suppose \(\{a_i\}_{i=1}^{N}\) and \(\{b_i\}_{i=1}^{N}\) are arbitrary sequences of elements from F. The set\(\{a_i\} \subseteq \{b_i\}\) (with duplicate values removed) if and only if there exists a sequence \(\{m_i\}_{i=1}^{N}\) from \(F_q \subseteq F\) such that:
\[\sum_{i=1}^{N}\frac{1}{X+a_{i}}=\sum_{i=1}^{N}\frac{m_{i}}{X+b_{i}}\]
in the function field \(F(X)\). Furthermore, \(\{a_i\} = \{b_i\}\) (as sets) if and only if \(m_i \neq 0\) for all \(t\).
The Logup protocol utilizes the sum-check protocol for verifying Lookup equations, including the following components:
Logup Workflow:
1. Compute Auxiliary Columns: Define auxiliary columns \(h_i(x)\) for batches of lookup items \(\{f_i(x)\}\) using a challenge value x:
\[h_i(x) = \frac{1}{x+f_{2i}} + \frac{1}{x+f_{2i+1}}\]
2. Construct Lookup Table Polynomial: For table entries \(t(x)\), define:
\[g(x) = \frac{1}{x+t(x)}\]
3. Define\(z(x)\) Polynomial Recursion: The definition of the polynomial \(z(x)\) is used to verify the relationship between lookup items and the lookup table. Its recursive relationship is as follows:
\[Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)\]
Where:
The recursive relationship of the \(z(x)\) polynomial ensures that the sum of the auxiliary columns across the entire lookup table range is zero. This property can help verify whether a lookup item is present in the lookup table.
The initial condition of the Z polynomial is:
\[Z(1) = 0\]
Finally, the Lookup argument computation is completed using the PIOP+PCS protocol.
The code corresponding to the Logup argument in the zkm prover implements the Lookup verification of the Logup protocol through the following steps:
Below is an explanation of the code structure:
Now, let’s go over each method corresponding to the Logup protocol.
The Lookup struct defines the basic information to be verified, including the columns, Lookup table, and frequency columns:
pub struct Lookup<F: Field> {
pub(crate) columns: Vec<Column<F>>, // Set of columns to be verified, representing the f_i(x) polynomial
pub(crate) table_column: Column<F>, // Lookup table column, representing the t(x) polynomial
pub(crate) frequencies_column: Column<F>, // Frequency column for each column, representing the m(x) polynomial
pub filter_columns: Vec<Option<Filter<F>>>, // Filtering columns, optionally verifying certain rows
}
The Lookup_helper_columns function is the core of the code, generating auxiliary columns \(h_i(x)\) and \(g(x)\), and computing the recursive verification polynomial \(Z(x)\).
Key Flow and Code Analysis
1. Initialization and Degree Constraint Check:
assert_eq!(constraint_degree, 3, "TODO: Allow other constraint degrees.");
The constraint degree constraint_degree is fixed at 3 to ensure the formula calculations conform to the predefined structure. Currently, the code supports only this degree.
2. Get the Number of Auxiliary Columns:
let num_helper_columns = Lookup.num_helper_columns(constraint_degree);
num_helper_columns calculates the number of auxiliary columns required, including \(h_i(x)\), 1 / (table + challenge), and \(Z(x)\).
3. Generate h_i(x) Auxiliary Columns:
let mut helper_columns = get_helper_cols(
trace_poly_values,
trace_poly_values[0].len(),
&columns_filters,
grand_challenge,
constraint_degree,
);
\(h_i(x)\) Calculation: The get_helper_cols function divides the columns into batches, with each batch containing constraint_degree - 1 elements. For each batch, an auxiliary column \(h_i(x)\) is generated:
\[h_i(x) = \frac{1}{x+f_{2i}} + \frac{1}{x+f_{2(i+1)}}\]
Purpose: \(h_i(x)\) helps verify, during recursion, whether column values are present in table_column.
4. Compute the Inverse of the Table Column 1/(table + challenge):
let mut table = Lookup.table_column.eval_all_rows(trace_poly_values);
for x in table.iter_mut() {
*x = challenge + *x;
}
let table_inverse: Vec<F> = F::batch_multiplicative_inverse(&table);
Table Column Inverse \(g(x)\): After adding the challenge value challenge to each \(t(x)\), the reciprocal is taken, forming the auxiliary column
\[g(x) = \frac{1}{x+t(x)}\]
Purpose: This auxiliary column ensures that \(t(x)\) participates in verification through its reciprocal.
5. Compute the Recursive Polynomial \(Z(x)\):
let frequencies = &Lookup.frequencies_column.eval_all_rows(trace_poly_values);
let mut z = Vec::with_capacity(frequencies.len());
z.push(F::ZERO);
for i in 0..frequencies.len() - 1 {
let x = helper_columns[..num_helper_columns - 1]
.iter()
.map(|col| col.values[i])
.sum::<F>()
- frequencies[i] * table_inverse[i];
z.push(z[i] + x);
}
helper_columns.push(z.into());
\(Z(x)\) Recursion Formula: The recursion formula for \(Z(x)\) is:
\[Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)\]
Where frequencies represent \(m(x)\), and table_inverse represents \(g(x)\).
Purpose: Through recursion, this formula verifies the consistency of the distributions of \(f_i(x)\) and \(t(x)\), ensuring that all columns satisfy the Lookup constraints.
The eval_packed_Lookups_generic function checks the correctness of the auxiliary columns and \(Z(x)\) using the recursive formula to validate whether column values are included in the table_column.
1. Verify the Correctness of Auxiliary Columns h_i(x):
eval_helper_columns(
&Lookup.filter_columns,
&Lookup_columns,
local_values,
next_values,
&Lookup_vars.local_values[start..start + num_helper_columns - 1],
degree,
&grand_challenge,
yield_constr,
);
Here, the eval_helper_columns function is called to check each row of h_i(x) and ensure that the auxiliary columns are correctly generated.
2. Verify the Recursion of \(Z(x)\):
let z = Lookup_vars.local_values[start + num_helper_columns - 1];
let next_z = Lookup_vars.next_values[start + num_helper_columns - 1];
let table_with_challenge = Lookup.table_column.eval(local_values) + challenge;
let y = Lookup_vars.local_values[start..start + num_helper_columns - 1]
.iter()
.fold(P::ZEROS, |acc, x| acc + *x)
* table_with_challenge
- Lookup.frequencies_column.eval(local_values);
yield_constr.constraint_first_row(z);
yield_constr.constraint((next_z - z) * table_with_challenge - y);
Check the Recursion of \(Z(x)\): Ensures that the initial value of \(Z(x)\) is 0 and that every row satisfies:
\[Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)\]
This function builds recursive constraints at the circuit level, ensuring that the Lookup process remains consistent within the recursive proof circuit. It verifies the auxiliary columns and \(Z(x)\) to support the recursive proof.
Subscribe to the ZKM Blog to stay updated with the latest research by ZKM. If you have any questions about the article, you can contact the ZKM team on discord: discord.com/zkm
When representing computations as circuits, there are often complex operations such as bitwise XOR and bitwise AND. For example, performing a bitwise XOR operation on two 32-bit bitstrings usually requires hundreds of addition and multiplication gates, significantly increasing circuit size. Introducing the Lookup argument protocol effectively reduces circuit complexity.
To prove that two 32-bit bitstrings and their corresponding outputs satisfy a bitwise XOR relationship, one can encode the inputs and outputs into a lookup table of size \(2^{32}\), then demonstrate that the inputs and outputs align with a specific row in the table. To reduce table size, smaller tables such as \(2^{16}\) or \(2^{8}\) can be used, along with constraints between bits to balance table size and proof speed.
The Lookup argument is used to verify whether elements of one set appear in another set without revealing additional information. In circuit design, Lookup arguments are frequently applied to verify complex constraints, especially in cases involving non-gate or non-scalar multiplication operations. They are mainly used in proving systems like Plonkish and Halo2. This method significantly reduces circuit constraints and enhances proof efficiency. The specific construction steps are as follows:
The Logup protocol originates from the CQ protocol, which uses logarithms and derivatives from higher mathematics to reduce set membership proofs to simpler problems. Its workflow, as shown in Figure 1, involves the following steps:
1. Construct Lookup Items and Table:
2. Formulate LHS and RHS Expressions:
3. Verify Logarithmic Equality: Convert the multiplicative forms into logarithmic sums:
\[\sum_{j=1}^{n}log(\beta+f_{j})=\sum_{i=1}^{N}m_{i}\cdot log(\beta+t_{i})\]
4. Check Fractional Equality: Validate the equality:
\[\sum_{j=1}^{n}\frac{1}{\beta+f_{j}}=\sum_{i=1}^{N}\frac{m_{i}}{\beta+r_{i}}\]
If the equation holds, the lookup values are confirmed to be in the table.
The Logup protocol extends the CQ protocol from univariate polynomials to multivariate polynomials, adapting to zkSNARK algorithms with hypercube implementations. The zkSNARK prover uses the univariate version.
The core of the Logup protocol’s Lookup argument relies on the following mathematical theorem:
Lemma (Set Inclusion): Let \(F\) be a field with characteristic \(p > N\), and suppose \(\{a_i\}_{i=1}^{N}\) and \(\{b_i\}_{i=1}^{N}\) are arbitrary sequences of elements from F. The set\(\{a_i\} \subseteq \{b_i\}\) (with duplicate values removed) if and only if there exists a sequence \(\{m_i\}_{i=1}^{N}\) from \(F_q \subseteq F\) such that:
\[\sum_{i=1}^{N}\frac{1}{X+a_{i}}=\sum_{i=1}^{N}\frac{m_{i}}{X+b_{i}}\]
in the function field \(F(X)\). Furthermore, \(\{a_i\} = \{b_i\}\) (as sets) if and only if \(m_i \neq 0\) for all \(t\).
The Logup protocol utilizes the sum-check protocol for verifying Lookup equations, including the following components:
Logup Workflow:
1. Compute Auxiliary Columns: Define auxiliary columns \(h_i(x)\) for batches of lookup items \(\{f_i(x)\}\) using a challenge value x:
\[h_i(x) = \frac{1}{x+f_{2i}} + \frac{1}{x+f_{2i+1}}\]
2. Construct Lookup Table Polynomial: For table entries \(t(x)\), define:
\[g(x) = \frac{1}{x+t(x)}\]
3. Define\(z(x)\) Polynomial Recursion: The definition of the polynomial \(z(x)\) is used to verify the relationship between lookup items and the lookup table. Its recursive relationship is as follows:
\[Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)\]
Where:
The recursive relationship of the \(z(x)\) polynomial ensures that the sum of the auxiliary columns across the entire lookup table range is zero. This property can help verify whether a lookup item is present in the lookup table.
The initial condition of the Z polynomial is:
\[Z(1) = 0\]
Finally, the Lookup argument computation is completed using the PIOP+PCS protocol.
The code corresponding to the Logup argument in the zkm prover implements the Lookup verification of the Logup protocol through the following steps:
Below is an explanation of the code structure:
Now, let’s go over each method corresponding to the Logup protocol.
The Lookup struct defines the basic information to be verified, including the columns, Lookup table, and frequency columns:
pub struct Lookup<F: Field> {
pub(crate) columns: Vec<Column<F>>, // Set of columns to be verified, representing the f_i(x) polynomial
pub(crate) table_column: Column<F>, // Lookup table column, representing the t(x) polynomial
pub(crate) frequencies_column: Column<F>, // Frequency column for each column, representing the m(x) polynomial
pub filter_columns: Vec<Option<Filter<F>>>, // Filtering columns, optionally verifying certain rows
}
The Lookup_helper_columns function is the core of the code, generating auxiliary columns \(h_i(x)\) and \(g(x)\), and computing the recursive verification polynomial \(Z(x)\).
Key Flow and Code Analysis
1. Initialization and Degree Constraint Check:
assert_eq!(constraint_degree, 3, "TODO: Allow other constraint degrees.");
The constraint degree constraint_degree is fixed at 3 to ensure the formula calculations conform to the predefined structure. Currently, the code supports only this degree.
2. Get the Number of Auxiliary Columns:
let num_helper_columns = Lookup.num_helper_columns(constraint_degree);
num_helper_columns calculates the number of auxiliary columns required, including \(h_i(x)\), 1 / (table + challenge), and \(Z(x)\).
3. Generate h_i(x) Auxiliary Columns:
let mut helper_columns = get_helper_cols(
trace_poly_values,
trace_poly_values[0].len(),
&columns_filters,
grand_challenge,
constraint_degree,
);
\(h_i(x)\) Calculation: The get_helper_cols function divides the columns into batches, with each batch containing constraint_degree - 1 elements. For each batch, an auxiliary column \(h_i(x)\) is generated:
\[h_i(x) = \frac{1}{x+f_{2i}} + \frac{1}{x+f_{2(i+1)}}\]
Purpose: \(h_i(x)\) helps verify, during recursion, whether column values are present in table_column.
4. Compute the Inverse of the Table Column 1/(table + challenge):
let mut table = Lookup.table_column.eval_all_rows(trace_poly_values);
for x in table.iter_mut() {
*x = challenge + *x;
}
let table_inverse: Vec<F> = F::batch_multiplicative_inverse(&table);
Table Column Inverse \(g(x)\): After adding the challenge value challenge to each \(t(x)\), the reciprocal is taken, forming the auxiliary column
\[g(x) = \frac{1}{x+t(x)}\]
Purpose: This auxiliary column ensures that \(t(x)\) participates in verification through its reciprocal.
5. Compute the Recursive Polynomial \(Z(x)\):
let frequencies = &Lookup.frequencies_column.eval_all_rows(trace_poly_values);
let mut z = Vec::with_capacity(frequencies.len());
z.push(F::ZERO);
for i in 0..frequencies.len() - 1 {
let x = helper_columns[..num_helper_columns - 1]
.iter()
.map(|col| col.values[i])
.sum::<F>()
- frequencies[i] * table_inverse[i];
z.push(z[i] + x);
}
helper_columns.push(z.into());
\(Z(x)\) Recursion Formula: The recursion formula for \(Z(x)\) is:
\[Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)\]
Where frequencies represent \(m(x)\), and table_inverse represents \(g(x)\).
Purpose: Through recursion, this formula verifies the consistency of the distributions of \(f_i(x)\) and \(t(x)\), ensuring that all columns satisfy the Lookup constraints.
The eval_packed_Lookups_generic function checks the correctness of the auxiliary columns and \(Z(x)\) using the recursive formula to validate whether column values are included in the table_column.
1. Verify the Correctness of Auxiliary Columns h_i(x):
eval_helper_columns(
&Lookup.filter_columns,
&Lookup_columns,
local_values,
next_values,
&Lookup_vars.local_values[start..start + num_helper_columns - 1],
degree,
&grand_challenge,
yield_constr,
);
Here, the eval_helper_columns function is called to check each row of h_i(x) and ensure that the auxiliary columns are correctly generated.
2. Verify the Recursion of \(Z(x)\):
let z = Lookup_vars.local_values[start + num_helper_columns - 1];
let next_z = Lookup_vars.next_values[start + num_helper_columns - 1];
let table_with_challenge = Lookup.table_column.eval(local_values) + challenge;
let y = Lookup_vars.local_values[start..start + num_helper_columns - 1]
.iter()
.fold(P::ZEROS, |acc, x| acc + *x)
* table_with_challenge
- Lookup.frequencies_column.eval(local_values);
yield_constr.constraint_first_row(z);
yield_constr.constraint((next_z - z) * table_with_challenge - y);
Check the Recursion of \(Z(x)\): Ensures that the initial value of \(Z(x)\) is 0 and that every row satisfies:
\[Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)\]
This function builds recursive constraints at the circuit level, ensuring that the Lookup process remains consistent within the recursive proof circuit. It verifies the auxiliary columns and \(Z(x)\) to support the recursive proof.
Subscribe to the ZKM Blog to stay updated with the latest research by ZKM. If you have any questions about the article, you can contact the ZKM team on discord: discord.com/zkm
