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）来验证每个查找项是否符合预定的约束。