【zkMIPS系列】Lookup Argument (Logup)与代码分析

ZKM
更新于 2024-12-05 15:15
阅读 335

通过引入Lookup argument协议，可以有效减小电路的复杂度。

# 1. 引言

在将运算表示为电路的过程中，通常有较为复杂的操作，比如按位异或，按位与操作等。如果需要对两个32位长的比特串进行按位异或操作，则通常需要上百个加法和乘法门来表示该运算，这显然增加了电路的规模。通过引入Lookup argument协议，可以有效减小电路的复杂度。

为证明两个$32$位长的比特串及其对应输出满足按位异或的关系，可以将输入和输出编码为一张大小为$2^{32}$的查询表，随后证明输入和输出都在特定的一行中。如果需要降低表的大小，可以设置表为$2^{16}$, $2^8$，并加上位之间的约束，以达到优化表大小和证明速度的平衡。

Lookup argument用于证明一个集合中的元素是否出现在另一个集合中，且不泄露多余的信息。在电路设计中，Lookup argument 经常用于验证复杂的约束，尤其是包含非门或非标量乘法等操作的情况，主要用于Plonkish，Halo2等证明系统中。这种方法极大地减少了电路约束的复杂度，提高了证明效率，其具体的构造步骤如下：

- **构造查找表**：构造包含所有目标值的查找表 T，这可以是一个多项式表示的集合，其中包含了需要验证的所有合法值。
- **构造查找项**：证明者会将电路中的一些值通过哈希或其他方式映射为查找项（Lookup Items），并通过算法证明这些查找项是否包含在查找表 T中。
- **多项式映射**：证明者将查找表 T 和查找项转化为多项式，然后通过多项式相等性和插值验证二者是否一致。具体做法是用排列或插值多项式，确保查找表和查找项的值在某些位置上相等。
- **一致性检查**：为了验证查找项和查找表的正确性，Verifier 会用某种方式验证二者多项式的根是否一致。通常会引入一个随机标量来验证多项式的一致性。

# 2. Logup协议

## 2.1 cq协议

Logup协议的起源来源于cq协议，cq使用log及高等数学中的求导概念，将集合证明问题规约到更简单的问题，其原理图如图1所示，主要步骤如下：

1. **查找项和查找表的构建**：
    - 将需要验证的值构造成查找项集合（Values），每个项的形式为  $(\beta + f_i)$ ，其中  $ f_i $  是查找项的具体值。
    - 构造一个查找表集合（Table），每个项的形式为  $(\beta + t_i)$ ，其中  $ t_i $  是查找表的具体值。
2. **构造左右两侧表达式**：
    - **左侧（LHS）**：将所有查找项的值相乘，得到左侧的积形式表达式  $\prod_{i=1}^n (\beta + f_i)$ 。
    - **右侧（RHS）**：将查找表的项按照对应的频次相乘，得到右侧的积形式表达式  $\prod_{i=1}^N (\beta + t_i)^{m_i}$ ，其中  $ m_i $  是每个查找表项出现的次数。
3. **对数相等性验证**：
    通过对数运算，将两边的积形式转化为对数和的形式
    $$
    \sum_{j=1}^n \log(\beta + f_j) = \sum_{i=1}^N m_i \cdot \log(\beta + t_i)
    $$    
    以确保查找项和查找表项的一致性。
4. **验证分数相等性**：
    通过构造分数形式的等式验证，检查 
     $$
          \sum_{j=1}^n \frac{1}{\beta + f_j} = \sum_{i=1}^N \frac{m_i}{\beta + t_i}
     $$
     
    如果等式成立，说明查找项的值集合可以在查找表中找到。

![image.png](https://img.learnblockchain.cn/attachments/2024/12/6i6TXN4467514c16a0a86.png)
图1. cq lookup argument

## 2.2 Logup协议

Logup协议将cq协议中的一元多项式（unvariant polynomial) 扩展为多元多项式 (multivariant polynomial)，以适应于使用Hypercube的zkSNARK算法，在zkm prover中实现的是一元多项式的版本。

Logup协议的Lookup argument主要依赖于以下数学定理：

**引理（集合包含）**：设  $ F $  为一个特征为  $ p > N $  的域，假设  $ \{a_i\}*{i=1}^N $ 、 $ \{b_i\}*{i=1}^N $  是域元素的任意序列。那么，集合  $ \{a_i\} \subseteq \{b_i\} $  （作为集合，去掉了重复的值）当且仅当存在一个从  $ F_q \subseteq F $  中取出的域元素序列  $ \{m_i\}_{i=1}^N $ ，使得：
$$
\sum_{i=1}^N \frac{1}{X + a_i} = \sum_{i=1}^N \frac{m_i}{X + b_i}
$$

在函数域  $ F(X) $  中成立。此外，当且仅当对于每个  $ i = 1, \dots, N $  都有  $ m_i \neq 0 $  时，集合  $ \{a_i\} $  与  $ \{b_i\} $  相等，即  $ \{a_i\} = \{b_i\} $ 。

Logup的主要基于sumcheck protocol的来实现对于Lookup等式的检查，包括以下公式，

$h_i(x)$：通过每一批查找项的倒数和来构造辅助列。

- $ g(x) $：查找表列的倒数。
- Z多项式递归关系：确保查找项在查找表中的一致性，初始条件为0，类似于一个累加器，即$Z(1)=0$。

**Logup的主要流程如下：**

**(1). 计算辅助列**

辅助列  $ h_i(x) $  是用来帮助验证查找项是否在查找表中。对于一组查找列  $ \{f_i(x)\} $  和一个挑战值  $ x $ ，定义每个  $ h_i(x) $  为：
$$
h_i(x) = \frac{1}{x + f_{2i}} + \frac{1}{x + f_{2i+1}}
$$
每一批的查找项（即一组  $ f_i(x) $ ）都会生成一个  $ h_i(x) $ ，帮助验证查找项在查找表中的正确性。

**(2). Lookup table的多项式**

对于查找表的多项式  $ t(x) $ ，构造一个辅助列  $ g(x) $ ：
$$
g(x) = \frac{1}{x + t(x)}
$$
这个辅助列对应查找表中的每一行元素  $ t(x) $ ，并用来构造后续的 Z 多项式。

**(3). 使用定理写出递推公式Z(X)**

Z 多项式  $ Z(x) $  的定义用于验证查找项和查找表之间的关系，它的递归关系如下：
$$
Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)
$$
其中：
-  $ Z(x) $  是 Z 多项式在当前步的值。
-  $ Z(gx) $  是 Z 多项式在下一步的值。
-  $ \sum h_i(x) $  表示所有辅助列的和。
-  $ m(x) $  是频次列，表示查找项在查找表中的出现频率。

Z 多项式的递归关系确保了辅助列的和在整个查找表范围内的总和为零。这一性质可以帮助我们验证查找项是否包含在查找表中。

Z 多项式的初始条件为：
$$
Z(1) = 0.
$$

最后，使用PIOP+PCS协议完成Lookup argument的运算。

# 3. 代码解析

zkm prover对应的Logup argument的代码通过以下几步实现 `Logup` 协议的 Lookup 验证：

1. **定义 `Lookup` 结构体**：包括列、Lookup 表和频率列。
2. **生成辅助列 `h_i(x)` 和 `1 / (table + challenge)`**，用于递推验证。
3. **构建递推验证的 `Z(x)` 多项式**，以确保列值的分布一致性。
4. **验证辅助列和 `Z(x)` 的正确性**，通过 `eval_packed_Lookups_generic` 函数执行通用 packed Lookup 检查。

下面介绍一下代码结构：

1. **`Lookup` 结构体**：用于定义要验证的列、Lookup 表、频率列及其他过滤列。
2. **`Lookup_helper_columns` 函数**：生成 Lookup 操作所需的辅助列（如 `h_i` 和 `g`）以及递推验证的 `Z` 多项式。
3. **`eval_packed_Lookups_generic` 函数**：为 `Logup` 协议执行通用的 packed Lookup 检查，用于验证辅助列 `h_i` 和 `Z` 多项式的正确性。
4. **`eval_ext_Lookups_circuit` 函数**：在电路级别实现 Lookup 验证，以支持递归证明中的约束构建。

接下来，进入每个结构对应的方法，对Logup协议进行解析。

## 3.1 `Lookup` 结构体定义

`Lookup` 结构体定义了需要验证的列、Lookup 表和频率列等基础信息：

```rust
pub struct Lookup<F: Field> {
    pub(crate) columns: Vec<Column<F>>,          // 需要验证的列集合，表示 f_i(x) 多项式
    pub(crate) table_column: Column<F>,          // Lookup 表列，表示 t(x) 多项式
    pub(crate) frequencies_column: Column<F>,    // 每列出现的频率列，表示 m(x) 多项式
    pub filter_columns: Vec<Option<Filter<F>>>,  // 过滤列，可选择性地验证某些行
}
```

- **`columns`**：包含若干个需要验证的列，通过 Lookup 操作确保这些列的值包含在 `table_column` 中。
- **`table_column`**：Lookup 表列 `t(x)`，用于验证的基准数据。
- **`frequencies_column`**：表示各列在 Lookup 表中的频率，用于 `Z(x)` 多项式的计算。
- **`filter_columns`**：选择性过滤某些行，以便特定验证。

## 3.2 `Lookup_helper_columns` 函数

`Lookup_helper_columns` 是代码的核心部分，生成辅助列 `h_i(x)` 和 `g(x)`，并计算验证一致性的 `Z(x)` 多项式。

**关键流程和代码解析**

1. **初始化和校验约束度数**：
    
    ```rust
    assert_eq!(constraint_degree, 3, "TODO: Allow other constraint degrees.");    
    ```
    
    这里约束度数 `constraint_degree` 被固定为 3，以确保公式计算符合预设结构。代码实现中目前仅支持这一度数。
    
2. **获取辅助列的数量**：
    
    ```rust
    let num_helper_columns = Lookup.num_helper_columns(constraint_degree);    
    ```
    
    `num_helper_columns` 计算所需的辅助列数量，包括 `h_i(x)` 和 `1 / (table + challenge)` 及 `Z(x)`。
    
3. **生成 `h_i(x)` 辅助列**：
    
    ```rust
    let mut helper_columns = get_helper_cols(
        trace_poly_values,
        trace_poly_values[0].len(),
        &columns_filters,
        grand_challenge,
        constraint_degree,
    );       
      ```
    
**`h_i(x)`计算**：`get_helper_cols` 函数将 `columns` 中的列分成批次，每批次包含 `constraint_degree - 1` 个元素。每批次生成一个辅助列 `h_i(x)`：
$$
    h_i(x) = \frac{1}{x + f_{2i}} + \frac{1}{x + f_{2i+1}}
 $$
**作用**：`h_i(x)` 帮助在递推中验证列值是否在 `table_column` 中。
4. **计算表列的挑战逆 `1 / (table + challenge)`**：
    
   ```rust    
    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);        
   ```    
  
**表列逆值 `g(x)`**：每个 `t(x)` 加上挑战值 `challenge` 后取倒数，形成辅助列  
    $$ 
    g(x) = \frac{1}{x + t(x)} 
    $$
**作用**：这个辅助列确保了 `t(x)` 的值通过倒数操作参与验证。

5. **计算递推多项式 `Z(x)`**：
    
   ```rust
    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)` 递推公式**：`Z(x)` 多项式的递推公式为：
  $$
    Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)
  $$
其中 `frequencies` 表示  $ m(x) $  列，`table_inverse` 为  $ g(x) $ 。

**作用**：通过递推验证 `f_i(x)` 和 `t(x)` 的分布一致性，确保所有列满足 Lookup 约束。

## 3.3 `eval_packed_Lookups_generic` 函数

`eval_packed_Lookups_generic` 用于检查辅助列和 `Z(x)` 多项式的正确性，通过递推公式验证列值是否包含在 `table_column` 中。

1. **验证辅助列 `h_i(x)` 的正确性**：
    
    ```rust
    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,
    );    
    ```
    
这里调用 `eval_helper_columns` 函数逐行检查 `h_i(x)` 的值，以确保辅助列生成正确。
    
2. **验证 `Z(x)` 多项式的递推**：
    
    ```rust
    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);
    ```
    
**检查 `Z(x)` 的递推关系**：确保 `Z(x)` 的初始值为 0，并且每一行的 `Z(x)` 满足：
$$
    Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x)
$$

## 3.4 `eval_ext_Lookups_circuit` 函数

这个函数用于构建电路中的递归约束，确保 Lookup 过程在递归证明电路中保持一致性。它实现了对辅助列和 `Z(x)` 的验证，以便支持递归证明。

1. 引言

构造查找表：构造包含所有目标值的查找表 T，这可以是一个多项式表示的集合，其中包含了需要验证的所有合法值。
构造查找项：证明者会将电路中的一些值通过哈希或其他方式映射为查找项（Lookup Items），并通过算法证明这些查找项是否包含在查找表 T中。
多项式映射：证明者将查找表 T 和查找项转化为多项式，然后通过多项式相等性和插值验证二者是否一致。具体做法是用排列或插值多项式，确保查找表和查找项的值在某些位置上相等。
一致性检查：为了验证查找项和查找表的正确性，Verifier 会用某种方式验证二者多项式的根是否一致。通常会引入一个随机标量来验证多项式的一致性。

2. Logup协议

2.1 cq协议

Logup协议的起源来源于cq协议，cq使用log及高等数学中的求导概念，将集合证明问题规约到更简单的问题，其原理图如图1所示，主要步骤如下：

查找项和查找表的构建：
- 将需要验证的值构造成查找项集合（Values），每个项的形式为 $(\beta + f_i)$ ，其中 $ f_i $ 是查找项的具体值。
- 构造一个查找表集合（Table），每个项的形式为 $(\beta + t_i)$ ，其中 $ t_i $ 是查找表的具体值。
构造左右两侧表达式：
- 左侧（LHS）：将所有查找项的值相乘，得到左侧的积形式表达式 $\prod_{i=1}^n (\beta + f_i)$ 。
- 右侧（RHS）：将查找表的项按照对应的频次相乘，得到右侧的积形式表达式 $\prod_{i=1}^N (\beta + t_i)^{m_i}$ ，其中 $ m_i $ 是每个查找表项出现的次数。
对数相等性验证：通过对数运算，将两边的积形式转化为对数和的形式 $$ \sum_{j=1}^n \log(\beta + fj) = \sum{i=1}^N m_i \cdot \log(\beta + t_i) $$
以确保查找项和查找表项的一致性。
验证分数相等性：通过构造分数形式的等式验证，检查 $$ \sum_{j=1}^n \frac{1}{\beta + fj} = \sum{i=1}^N \frac{m_i}{\beta + t_i} $$

如果等式成立，说明查找项的值集合可以在查找表中找到。

图1. cq lookup argument

2.2 Logup协议

Logup协议的Lookup argument主要依赖于以下数学定理：

引理（集合包含）：设 $ F $ 为一个特征为 $ p > N $ 的域，假设 $ {a_i}{i=1}^N $ 、 $ {b_i}{i=1}^N $ 是域元素的任意序列。那么，集合 $ {a_i} \subseteq {b_i} $ （作为集合，去掉了重复的值）当且仅当存在一个从 $ F_q \subseteq F $ 中取出的域元素序列 $ {mi}{i=1}^N $ ，使得： $$ \sum_{i=1}^N \frac{1}{X + ai} = \sum{i=1}^N \frac{m_i}{X + b_i} $$

在函数域 $ F(X) $ 中成立。此外，当且仅当对于每个 $ i = 1, \dots, N $ 都有 $ m_i \neq 0 $ 时，集合 $ {a_i} $ 与 $ {b_i} $ 相等，即 $ {a_i} = {b_i} $ 。

Logup的主要基于sumcheck protocol的来实现对于Lookup等式的检查，包括以下公式，

$h_i(x)$：通过每一批查找项的倒数和来构造辅助列。

$ g(x) $：查找表列的倒数。
Z多项式递归关系：确保查找项在查找表中的一致性，初始条件为0，类似于一个累加器，即$Z(1)=0$。

Logup的主要流程如下：

(1). 计算辅助列

辅助列 $ h_i(x) $ 是用来帮助验证查找项是否在查找表中。对于一组查找列 $ {f_i(x)} $ 和一个挑战值 $ x $ ，定义每个 $ h_i(x) $ 为： $$ hi(x) = \frac{1}{x + f{2i}} + \frac{1}{x + f_{2i+1}} $$ 每一批的查找项（即一组 $ f_i(x) $ ）都会生成一个 $ h_i(x) $ ，帮助验证查找项在查找表中的正确性。

(2). Lookup table的多项式

对于查找表的多项式 $ t(x) $ ，构造一个辅助列 $ g(x) $ ： $$ g(x) = \frac{1}{x + t(x)} $$ 这个辅助列对应查找表中的每一行元素 $ t(x) $ ，并用来构造后续的 Z 多项式。

(3). 使用定理写出递推公式Z(X)

Z 多项式 $ Z(x) $ 的定义用于验证查找项和查找表之间的关系，它的递归关系如下： $$ Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x) $$ 其中：

$ Z(x) $ 是 Z 多项式在当前步的值。
$ Z(gx) $ 是 Z 多项式在下一步的值。
$ \sum h_i(x) $ 表示所有辅助列的和。
$ m(x) $ 是频次列，表示查找项在查找表中的出现频率。

Z 多项式的递归关系确保了辅助列的和在整个查找表范围内的总和为零。这一性质可以帮助我们验证查找项是否包含在查找表中。

Z 多项式的初始条件为： $$ Z(1) = 0. $$

最后，使用PIOP+PCS协议完成Lookup argument的运算。

3. 代码解析

zkm prover对应的Logup argument的代码通过以下几步实现 Logup 协议的 Lookup 验证：

定义 Lookup 结构体：包括列、Lookup 表和频率列。
生成辅助列 h_i(x) 和 1 / (table + challenge)，用于递推验证。
构建递推验证的 Z(x) 多项式，以确保列值的分布一致性。
验证辅助列和 Z(x) 的正确性，通过 eval_packed_Lookups_generic 函数执行通用 packed Lookup 检查。

下面介绍一下代码结构：

Lookup 结构体：用于定义要验证的列、Lookup 表、频率列及其他过滤列。
Lookup_helper_columns 函数：生成 Lookup 操作所需的辅助列（如 h_i 和 g）以及递推验证的 Z 多项式。
eval_packed_Lookups_generic 函数：为 Logup 协议执行通用的 packed Lookup 检查，用于验证辅助列 h_i 和 Z 多项式的正确性。
eval_ext_Lookups_circuit 函数：在电路级别实现 Lookup 验证，以支持递归证明中的约束构建。

接下来，进入每个结构对应的方法，对Logup协议进行解析。

3.1 `Lookup` 结构体定义

Lookup 结构体定义了需要验证的列、Lookup 表和频率列等基础信息：

pub struct Lookup&lt;F: Field> {
    pub(crate) columns: Vec&lt;Column&lt;F>>,          // 需要验证的列集合，表示 f_i(x) 多项式
    pub(crate) table_column: Column&lt;F>,          // Lookup 表列，表示 t(x) 多项式
    pub(crate) frequencies_column: Column&lt;F>,    // 每列出现的频率列，表示 m(x) 多项式
    pub filter_columns: Vec&lt;Option&lt;Filter&lt;F>>>,  // 过滤列，可选择性地验证某些行
}

columns：包含若干个需要验证的列，通过 Lookup 操作确保这些列的值包含在 table_column 中。
table_column：Lookup 表列 t(x)，用于验证的基准数据。
frequencies_column：表示各列在 Lookup 表中的频率，用于 Z(x) 多项式的计算。
filter_columns：选择性过滤某些行，以便特定验证。

3.2 `Lookup_helper_columns` 函数

Lookup_helper_columns 是代码的核心部分，生成辅助列 h_i(x) 和 g(x)，并计算验证一致性的 Z(x) 多项式。

关键流程和代码解析

初始化和校验约束度数：
```
assert_eq!(constraint_degree, 3, "TODO: Allow other constraint degrees.");    
```
这里约束度数 constraint_degree 被固定为 3，以确保公式计算符合预设结构。代码实现中目前仅支持这一度数。
获取辅助列的数量：
```
let num_helper_columns = Lookup.num_helper_columns(constraint_degree);    
```
num_helper_columns 计算所需的辅助列数量，包括 h_i(x) 和 1 / (table + challenge) 及 Z(x)。

生成 h_i(x) 辅助列：

let mut helper_columns = get_helper_cols(
    trace_poly_values,
    trace_poly_values[0].len(),
    &columns_filters,
    grand_challenge,
    constraint_degree,
);

h_i(x)计算：get_helper_cols 函数将 columns 中的列分成批次，每批次包含 constraint_degree - 1 个元素。每批次生成一个辅助列 h_i(x)： $$ hi(x) = \frac{1}{x + f{2i}} + \frac{1}{x + f_{2i+1}} $$ 作用：h_i(x) 帮助在递推中验证列值是否在 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&lt;F> = F::batch_multiplicative_inverse(&table);

表列逆值 g(x)：每个 t(x) 加上挑战值 challenge 后取倒数，形成辅助列
$$ g(x) = \frac{1}{x + t(x)} $$ 作用：这个辅助列确保了 t(x) 的值通过倒数操作参与验证。

计算递推多项式 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::&lt;F>()
        - frequencies[i] * table_inverse[i];
    z.push(z[i] + x);
}
helper_columns.push(z.into());

Z(x) 递推公式：Z(x) 多项式的递推公式为： $$ Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x) $$ 其中 frequencies 表示 $ m(x) $ 列，table_inverse 为 $ g(x) $ 。

作用：通过递推验证 f_i(x) 和 t(x) 的分布一致性，确保所有列满足 Lookup 约束。

3.3 `eval_packed_Lookups_generic` 函数

eval_packed_Lookups_generic 用于检查辅助列和 Z(x) 多项式的正确性，通过递推公式验证列值是否包含在 table_column 中。

验证辅助列 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,
);

这里调用 eval_helper_columns 函数逐行检查 h_i(x) 的值，以确保辅助列生成正确。

验证 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);

检查 Z(x) 的递推关系：确保 Z(x) 的初始值为 0，并且每一行的 Z(x) 满足： $$ Z(gx) = Z(x) + \sum h_i(x) - m(x) \cdot g(x) $$

3.4 `eval_ext_Lookups_circuit` 函数

这个函数用于构建电路中的递归约束，确保 Lookup 过程在递归证明电路中保持一致性。它实现了对辅助列和 Z(x) 的验证，以便支持递归证明。

原创
学分: 16
分类: Layer2
标签: zkVM zkMIPS

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

【zkMIPS系列】Lookup Argument (Logup)与代码分析

1. 引言

2. Logup协议

2.1 cq协议

2.2 Logup协议

3. 代码解析

3.1 `Lookup` 结构体定义

3.2 `Lookup_helper_columns` 函数

3.3 `eval_packed_Lookups_generic` 函数

3.4 `eval_ext_Lookups_circuit` 函数

0 条评论

专栏: zkMIPS解读

文章目录

【zkMIPS系列】Lookup Argument (Logup)与代码分析

1. 引言

2. Logup协议

2.1 cq协议

2.2 Logup协议

3. 代码解析

3.1 Lookup 结构体定义

3.2 Lookup_helper_columns 函数

3.3 eval_packed_Lookups_generic 函数

3.4 eval_ext_Lookups_circuit 函数

0 条评论

专栏: zkMIPS解读

文章目录

3.1 `Lookup` 结构体定义

3.2 `Lookup_helper_columns` 函数

3.3 `eval_packed_Lookups_generic` 函数

3.4 `eval_ext_Lookups_circuit` 函数