鸿途知科网【zkMIPS系列】ZKM Prover: Cross Table Lookup
1. 跨表lookup
1.1 多个表格的聚合
在零知识证明中的lookup中，我们可能有多个表格，每个表格可以包含不同的数据。这些表格之间可能存在一定的关联，需要聚合起来进行联合验证。这个过程的目的是将多个表格中的相关信息组合成一个查询（lookup）操作，然后将其验证。
例如，假设我们有两个表格 T1 和 T2，T1 存储了某些数据，而 T2 存储了与这些数据相关的查询条件或验证信息。跨表查找的目的是在 T2 中找到符合 T1 数据条件的行。
1.2 通过 lookup 操作进行查找
一旦多个表格聚合完成，就需要在一个 looked table 中进行查找。这个 looked table 是用来存储最终的验证结果，或者可以理解为最终的目标表格。查找过程使用 lookup 来验证某些数据是否存在于 looked table 中。
具体来说，通过 lookup 操作，系统会检查在给定的 looked table 中是否有某些值符合之前计算出来的查询条件（即来自多个表格的聚合）。如果存在符合条件的记录，则证明过程能够成功；否则，证明失败。
在这个过程中，通常会使用一个“过滤器”（filter）来确定哪些行是符合条件的。这个过滤器是通过列的线性组合来表达的，而线性组合的系数与各个表格中不同列的数据相关。
1.3 用 lookup 在 looked table 进行证明
在查找操作完成后，最终的目标是证明查询的正确性，而这个过程是通过在 looked table 中使用 lookup 来进行的。在这个过程中，零知识证明会生成一个证明，证明在某些给定的条件下，查找操作的结果是正确的，而证明者并不会泄露任何关于表格内容的具体信息。
在 STARK 中，lookup 操作通常会使用 Z(x) 多项式来构建证明，Z(x) 多项式是在多次线性组合与过滤器操作下生成的，用来表示查询结果的有效性和约束。
2. 跨表lookup流程
2.1 表列和过滤器的聚合
首先，我们需要聚合多个表格中的列和过滤器。每个表中的列可以通过线性组合形成新的列，而过滤器决定哪些行会被纳入计算。
- 线性组合：
$$ \sum_{i=1}^{n} f_i \cdot a_i $$
其中，$f_i$ 是与每个列相关联的系数。
- 过滤器： 过滤器是一个函数 $f(x)$，它在每行计算时返回0或1，表示是否选择该行。如果 $f(x) = 1$ ，则该行的列值会被纳入计算。
代码分析：
pub(crate) fn get_helper_cols<F: Field>(
trace: &[PolynomialValues<F>], // 传入的迹数据
degree: usize, // 迹的度数
columns_filters: &[ColumnFilter<F>], // 列和过滤器的元组
challenge: GrandProductChallenge<F>, // 用于组合列的挑战
constraint_degree: usize, // 约束度数
) -> Vec<PolynomialValues<F>> { // 返回多个辅助列
let num_helper_columns = ceil_div_usize(columns_filters.len(), constraint_degree - 1); // 计算需要的辅助列数量
let mut helper_columns = Vec::with_capacity(num_helper_columns); // 初始化辅助列存储向量
// 对每一批列和过滤器进行处理，按约束度数（例如：constraint_degree - 1）分批处理
for mut cols_filts in &columns_filters.iter().chunks(constraint_degree - 1) {
let (first_col, first_filter) = cols_filts.next().unwrap(); // 获取当前批次的第一个列和过滤器
let mut filter_col = Vec::with_capacity(degree); // 用于存储每行的过滤器值
// 对每个行进行处理，结合过滤器和列
let first_combined = (0..degree)
.map(|d| {
// 计算每行的过滤器值
let f = if let Some(filter) = first_filter {
let f = filter.eval_table(trace, d); // 使用过滤器计算当前行的值
filter_col.push(f); // 存储当前行的过滤器值
f
} else {
filter_col.push(F::ONE); // 如果没有过滤器，则返回1
F::ONE
};
// 如果过滤器值为1，则返回组合后的列值
if f.is_one() {
let evals = first_col
.iter()
.map(|c| c.eval_table(trace, d)) // 计算列的评估值
.collect::<Vec<F>>();
challenge.combine(evals.iter()) // 使用挑战来组合列
} else {
assert_eq!(f, F::ZERO, "Non-binary filter?"); // 如果过滤器值为0，抛出异常
F::ONE // 否则返回1
}
})
.collect::<Vec<F>>(); // 汇总当前批次所有行的结果
let mut acc = F::batch_multiplicative_inverse(&first_combined); // 对组合结果进行批量求逆
// 如果过滤器值为0，则当前行的值应为0
for d in 0..degree {
if filter_col[d].is_zero() {
acc[d] = F::ZERO;
}
}
// 对剩余列进行相同的处理
for (col, filt) in cols_filts {
let mut filter_col = Vec::with_capacity(degree); // 存储过滤器的值
let mut combined = (0..degree)
.map(|d| {
let f = if let Some(filter) = filt {
let f = filter.eval_table(trace, d); // 计算当前行的过滤器值
filter_col.push(f); // 存储过滤器值
f
} else {
filter_col.push(F::ONE); // 如果没有过滤器，则返回1
F::ONE
};
if f.is_one() {
let evals = col
.iter()
.map(|c| c.eval_table(trace, d)) // 计算列的评估值
.collect::<Vec<F>>();
challenge.combine(evals.iter()) // 使用挑战来组合列
} else {
assert_eq!(f, F::ZERO, "Non-binary filter?"); // 如果过滤器值为0，抛出异常
F::ONE // 否则返回1
}
})
.collect::<Vec<F>>(); // 汇总当前批次的列值
combined = F::batch_multiplicative_inverse(&combined); // 对组合列进行求逆
// 如果过滤器值为0，则当前行的值应为0
for d in 0..degree {
if filter_col[d].is_zero() {
combined[d] = F::ZERO;
}
}
batch_add_inplace(&mut acc, &combined); // 将当前列的结果加到累积结果中
}
helper_columns.push(acc.into()); // 将计算结果作为辅助列保存
}
assert_eq!(helper_columns.len(), num_helper_columns); // 确保辅助列的数量正确
helper_columns // 返回所有辅助列
}
get_helper_cols函数通过对每一列和过滤器的组合计算，得到辅助列。每个列与过滤器的组合结果经过求逆后，生成了辅助列。
2.2 辅助列的构造
辅助列通过计算每列的倒数，并对倒数进行求和来构造。每个列与过滤器结合，通过逆运算得到最终的辅助列。每批列会构造出一个新的辅助列。
- 辅助列的构造：
$$ hi(X)=\sum{i=1}^{N} \frac{1}{x + a_i} $$
2.3 Z多项式的计算
$Z(x)$ 多项式通过递归关系计算，保证了查找项在不同表之间的一致性。它的计算从初始条件 $Z(1)=0$ 开始，递归地将每个辅助列的值加到当前多项式中。
$$ Z(w)=Z(gw)+\sum h_i(X)-m(X)g(X) $$
其中，$h_i $ 是辅助列, $m(X)$ 代表了某个元素在lookup table中出现的次数。
fn partial_sums<F: Field>(
trace: &[PolynomialValues<F>], // 传入的迹数据
columns_filters: &[ColumnFilter<F>], // 列和过滤器的元组
challenge: GrandProductChallenge<F>, // 用于组合列的挑战
constraint_degree: usize, // 约束度数
) -> Vec<PolynomialValues<F>> { // 返回辅助列和Z多项式
let degree = trace[0].len(); // 获取迹的度数
let mut z = Vec::with_capacity(degree); // 用于存储Z多项式的向量
let mut helper_columns = get_helper_cols(trace, degree, columns_filters, challenge, constraint_degree); // 获取辅助列
// 计算Z多项式的最后一项
let x = helper_columns
.iter()
.map(|col| col.values[degree - 1]) // 获取每列的最后一项
.sum::<F>();
z.push(x); // 将最后一项加入Z多项式
// 递归计算Z多项式的每一项
for i in (0..degree - 1).rev() {
let x = helper_columns.iter().map(|col| col.values[i]).sum::<F>();
z.push(z[z.len() - 1] + x); // 将当前项加到Z多项式中
}
z.reverse(); // 反转Z多项式，使得Z(1) = 0
// 处理Z多项式并返回
if columns_filters.len() > 1 {
helper_columns.push(z.into());
} else {
helper_columns = vec![z.into()];
}
helper_columns // 返回计算后的辅助列
}
partial_sums函数计算 $Z(x)$ 多项式，并对辅助列进行累积，得到最终的Z多项式。
2.4 Logup进行查找验证
Logup的目的是验证多个查找表之间的项是否一致，确保跨表查找约束得到满足。在Logup过程中，验证是通过将辅助列和 $Z(x)$ 多项式进行比较来完成的。具体而言，Logup在验证每一行的查找项时，都会利用计算得到的辅助列和 $Z(x)$ 多项式。
公式：
-
查找项验证公式：
$$ \sum_{i=1}^{n} \frac{1}{x + a_i} = Z(x) $$
其中 ，是 $Z(x)$ 多项式， 是查找表中的项。
代码分析：
pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, S, const D: usize, const D2: usize>(
vars: &S::EvaluationFrame<FE, P, D2>, // 评估帧，包含当前和下一个状态的值
ctl_vars: &[CtlCheckVars<F, FE, P, D2>], // 跨表查找变量
consumer: &mut ConstraintConsumer<P>, // 用于消费约束的约束消费者
constraint_degree: usize, // 约束度数
) where
F: RichField + Extendable<D>, // 支持的字段类型
FE: FieldExtension<D2, BaseField = F>, // 字段扩展
P: PackedField<Scalar = FE>, // 打包字段类型
S: Stark<F, D>, // Stark配置类型
{
let local_values = vars.get_local_values(); // 获取当前状态的变量
let next_values = vars.get_next_values(); // 获取下一个状态的变量
// 遍历所有的跨表查找变量（`ctl_vars`）
for lookup_vars in ctl_vars {
let CtlCheckVars {
helper_columns, // 辅助列
local_z, // 当前Z值
next_z, // 下一个Z值
challenges, // 挑战值
columns, // 列的集合
filter, // 过滤器的集合
} = lookup_vars;
// 计算当前表的所有列的线性组合
let evals = columns
.iter()
.map(|col| {
col.iter()
.map(|c| c.eval_with_next(local_values, next_values)) // 对每列进行评估
.collect::<Vec<_>>()
})
.collect::<Vec<_>>();
// 使用辅助列进行约束验证
eval_helper_columns(
filter, // 过滤器
&evals, // 评估后的列
local_values, // 当前状态值
next_values, // 下一个状态值
helper_columns, // 辅助列
constraint_degree, // 约束度数
challenges, // 挑战值
consumer, // 约束消费者
);
// 如果有辅助列，验证Z多项式的值
if !helper_columns.is_empty() {
let h_sum = helper_columns.iter().fold(P::ZEROS, |acc, x| acc + *x); // 求辅助列的和
// 检查 `Z(g^(n-1))`
consumer.constraint_last_row(*local_z - h_sum);
// 检查 `Z(w) = Z(gw) + \sum h_i`
consumer.constraint_transition(*local_z - *next_z - h_sum);
} else if columns.len() > 1 {
// 如果只有两个列，则计算它们的组合值
let combin0 = challenges.combine(&evals[0]);
let combin1 = challenges.combine(&evals[1]);
let f0 = if let Some(filter0) = &filter[0] {
filter0.eval_filter(local_values, next_values) // 计算过滤器0的值
} else {
P::ONES
};
let f1 = if let Some(filter1) = &filter[1] {
filter1.eval_filter(local_values, next_values) // 计算过滤器1的值
} else {
P::ONES
};
// 约束最后一行
consumer.constraint_last_row(combin0 * combin1 * *local_z - f0 * combin1 - f1 * combin0);
// 约束过渡行
consumer.constraint_transition(
combin0 * combin1 * (*local_z - *next_z) - f0 * combin1 - f1 * combin0,
);
} else {
// 如果只有一列，则直接验证该列
let combin0 = challenges.combine(&evals[0]);
let f0 = if let Some(filter0) = &filter[0] {
filter0.eval_filter(local_values, next_values) // 计算过滤器的值
} else {
P::ONES
};
// 约束最后一行
consumer.constraint_last_row(combin0 * *local_z - f0);
// 约束过渡行
consumer.constraint_transition(combin0 * (*local_z - *next_z) - f0);
}
}
}
eval_cross_table_lookup_checks：在该函数中，我们首先计算每个列的评估结果，并使用辅助列进行检查。然后根据辅助列计算Z多项式的值并进行验证。最终通过约束消费者（consumer）来验证每个查找项是否符合预定的约束。
版权声明
本文仅代表作者观点，不代表区块链技术网立场。
本文系作者授权本站发表，未经许可，不得转载。
上一篇：区块链三大基石技术之二-哈希 下一篇：【预测】未来一年的加密货币
相关文章
作者文章
- 首尔的一笔交易如何击穿Hyperliquid最大的股票市场 2个月前 (08-29)
- Zcash的Ironwood升级强化隐私特性 2个月前 (08-29)
- 北极熊当选Glamsterdam升级吉祥物 - Magicians / Primordial Soup 2个月前 (08-29)
- 最佳实践：从Multi-Agent到Agent Team 2个月前 (08-29)
- ColdCard 硬件签名器安全警告（2026-07-30） 2个月前 (08-29)
发表评论:
◎欢迎参与讨论，请在这里发表您的看法、交流您的观点。