LogUp查找参数及其使用Lambdaworks对连续只读存储器的实现

介绍

在 之前的文章 中，我们解释了如何为连续只读存储器定义约束，并将其作为一个例子来理解约束的一般定义方式。这一次，我们将继续深入研究这个例子，介绍 LogUp 构造，使其适应于单变量多项式，并解释我们是如何实现它的。

在接下来的内容中，我们将假定你对约束、连续只读存储器的概念以及它们的实现方式有所了解。为了更深入地了解这些主题，我们建议阅读前面提到的文章，因为本文将是它的延续。

什么是 LogUp？

LogUp 是 Lookup Argument (查找参数) 的一个实例。但查找参数究竟是什么？它们是一种工具，使我们能够有效地证明特定的值 $v$ 属于一个值表 $T$，而无需暴露整个表。这个概念对于提高语句参数的效率非常有用，否则这些语句的算术化成本会非常高。

本质上，查找参数使证明者能够说服验证者，给定集合 $A$（通常表示为 trace table (跟踪表) 的一列）的每个元素都包含在另一个集合 $T$（查找表）中。通过这种方式，我们不必进行大量的算术约束来确保 $A$ 满足某些条件并以某种方式存在，而是预先计算 $A$ 可以拥有的所有有效值，将它们写入表 $T$，然后使用查找参数来证明 $A$ 的所有元素都属于 $T$（即，它们是有效元素）。换句话说，我们实现了验证数据之间的关系，同时保护隐私或优化计算。

在 上述文章 中可以找到一个 Lookup argument (查找参数) 的例子。让我们快速回顾一下我们当时的做法：给定两列，$a$（地址）和 $v$（值），我们需要创建它们对应的排序后的列 $a'$ 和 $v'$。我们使用了一种称为 Grand Product (大乘积) 的 Lookup argument (查找参数) 来证明它们是原始列的排列。

使用从 $F$ 的扩展中采样的两个随机元素 $z$ 和 $\alpha$，我们使用以下公式构造了一个辅助列 $p$：

$p_{i+1}=pi \cdot \frac{z-(a{i+1}+\alpha v{i+1})}{z-(a'{i+1}+\alpha v'_{i+1})},$

目标是验证此列的最后一个元素等于 1：

$p{n-1}=\prod{i=0}^{n-1} \frac{z-(a_i+\alpha v_i)}{z-(a'_i+\alpha v'_i)}=1.$

这保证了 $a'$ 和 $v'$ 是 $a$ 和 $v$ 的排列，从而确保了表的正确性。

LogUp 背后的思想是用它们的对数导数来替换这些乘积，或者更简单地说，将乘积转换为分数的和。 这种方法减少了证明者和验证者的计算量。该方法得名是因为对数导数将诸如 $\prod_{i=1}^{n} \frac{1}{X-y_i}$ 之类的乘积转换为和：

$\sum_{i=1}^{n} \frac{1}{X-y_i}.$

因此，假设我们有一个来自主跟踪的列 $a=(a_0,\dots,a_n)$，其中包含重复元素，以及一个来自查找表的列 $t=(t_0,\dots,t_m)$，其中没有重复项，并且我们想证明 $a$ 的所有元素都属于 $t$。 在这种情况下，证明等式就足够了：

$\sum_{i=0}^{n} \frac{1}{\alpha-ai}=\sum{i=0}^{m} \frac{m_i}{\alpha-t_i}$

其中 $\alpha$ 是一个随机元素，$m_i$ 是 $t_i$ 在 $a$ 中的 multiplicity (重数)，即 $t_i$ 在 $a$ 中出现的次数。

此时可能会出现一个很自然的问题：用和代替乘积是否仍然更有效，主要是因为这样做会引入分数？正如我们稍后将看到的，我们不会直接处理这些分数。相反，我们将等式的两边乘以公分母。

连续只读存储器示例

为了理解 LogUp 参数的约束是如何编写的，让我们回到我们的连续只读存储器的例子。为了理解这个例子，我们建议参考 Lambdaworks 中的相应实现。

主 Trace

首先，我们需要理解在想要使用 LogUp 参数的情况下，主 trace 的列是如何定义的。我们将以类似于第一篇文章中的方式进行。给定我们内存的地址列 $a$ 和值列 $v$，我们将向主 trace 添加三个附加列：$a'$、$v'$ 和 $m$。$a'$ 和 $v'$ 列将包含与 $a$ 和 $v$ 相同的值，但将按升序排序，不重复值。$m$ 列将表示这些值在原始列中的 multiplicity (重数)。由于这些列没有重复项，因此它们会更小。为了确保所有列具有相同的长度并适合单个表，我们将通过重复 $a'$ 和 $v'$ 的最后一个值来 padding (填充) 它们，并在 $m$ 列中为这些 padding (填充) 行分配 multiplicity (重数) $0$。

让我们看一个例子。如果我们的原始表是：

则主 trace 将变为：

请注意，原始表不代表有效的只读存储器（因为地址 2 有两个不同的值，20 和 40），我们仍然可以构建主 trace。 稍后，SingleValueConstraint 转换约束将确保此类表格无效。

在我们的实现中，函数 read_only_logup_trace() 处理主 trace 的构造。它返回一个 TraceTable，其中包含上面描述的五个主列和一个最初填充为零的辅助列，稍后将被替换为适当的值。

/// 返回一个 trace table，其中包含一个填充零的辅助列（稍后将由 air 替换为正确的值）和
/// 以下五个主要列：
/// 原始地址和值，没有重复项的排序后的地址和值，以及
/// 每个排序后的地址和值在原始地址和值中出现的 multiplicity (重数)（即，它们在原始地址和值列中出现的次数）。
pub fn read_only_logup_trace<
    F: IsPrimeField + IsFFTField + IsSubFieldOf<E> + Send + Sync,
    E: IsField + Send + Sync,
>(
    addresses: Vec<FieldElement<F>>,
    values: Vec<FieldElement<F>>,
) -> TraceTable<F, E> {
    // 我们对地址和值进行排序。
    let mut address_value_pairs: Vec<_> = addresses.iter().zip(values.iter()).collect();
    address_value_pairs.sort_by_key(|(addr, _)| addr.representative());

    //我们定义将添加到原始列的主要列
    let mut multiplicities = Vec::new();
    let mut sorted_addresses = Vec::new();
    let mut sorted_values = Vec::new();

    for (key, group) in &address_value_pairs.into_iter().group_by(|&(a, v)| (a, v)) {
        let group_vec: Vec<_> = group.collect();
        multiplicities.push(FieldElement::<F>::from(group_vec.len() as u64));
        sorted_addresses.push(key.0.clone());
        sorted_values.push(key.1.clone());
    }

    // 我们使用每个值的最后一个值调整排序后的地址和值的大小，以便它们与原始地址和值具有相同的
    // 行数。但是，它们的 multiplicity (重数) 应为零。
    sorted_addresses.resize(addresses.len(), sorted_addresses.last().unwrap().clone());
    sorted_values.resize(addresses.len(), sorted_values.last().unwrap().clone());
    multiplicities.resize(addresses.len(), FieldElement::<F>::zero());

    let main_columns = vec![
        addresses.clone(),
        values.clone(),
        sorted_addresses,
        sorted_values,
        multiplicities,
    ];

    // 我们创建一个与主列长度相同的向量，其中填充了来自 field extension (域扩展) 的零，并将其作为辅助列。
    let zero_vec = vec![FieldElement::<E>::zero(); main_columns[0].len()];
    TraceTable::from_columns(main_columns, vec![zero_vec], 1)
}

辅助 Trace

现在，让我们看看如何构造辅助列。辅助列，我们将其称为 $s$，应按如下方式累加主表中每一行对应的分数之和：

$s_0=\frac{m_0}{z-(a'_0+\alpha v'_0)}-\frac{1}{z-(a_0+\alpha v_0)},$ $s_1=s_0+\frac{m_1}{z-(a'_1+\alpha v'_1)}-\frac{1}{z-(a_1+\alpha v_1)}$

依此类推，得到：

$s_{i+1}=si+\frac{m{i+1}}{z-(a'{i+1}+\alpha v'{i+1})}-\frac{1}{z-(a{i+1}+\alpha v{i+1})}$ ，其中 $i \in {0,\dots,n-2}$。

例如，如果我们的主 trace 是：

那么，我们的辅助列 trace $s$ 如下所示：

观察到，如果主 trace 确实表示一个带有 multiplicity (重数) 的 permutation (排列)，那么 $s$ 的最后一个元素（即 $s{n-1}$）应该反映所有和的累加，相互抵消并导致 $0$（即 $s{n-1}=0$）。这类似于 Grand Product (大乘积) 中发生的情况，我们验证最终乘积是否抵消并得到 1（即 $p_{n-1}=1$）。让我们在上面表格中的示例的上下文中看看这一点：

$s_{n-1}=\frac{1}{z-(1+\alpha 10)}-\frac{1}{z-(3+\alpha 30)}+\frac{2}{z-(2+\alpha 20)}-\frac{1}{z-(1+\alpha 10)}+\frac{1}{z-(3+\alpha 30)}-\frac{1}{z-(2+\alpha 20)}+\frac{0}{z-(3+\alpha 30)}-\frac{1}{z-(2+\alpha 20)}=0$

现在，让我们看看这如何在我们的代码中实现的。在 Lambdaworks 中，辅助 trace 的构造在 AIR 实现中处理。具体来说，在 LogReadOnlyRAP 的实现中，你可以找到以下函数 build_auxiliary_trace()：

fn build_auxiliary_trace(
    &self,
    trace: &mut TraceTable<Self::Field, Self::FieldExtension>,
    challenges: &[FieldElement<E>],
) where
    Self::FieldExtension: IsFFTField,
{
    // 主表
    let main_segment_cols = trace.columns_main();
    let a = &main_segment_cols[0];
    let v = &main_segment_cols[1];
    let a_sorted = &main_segment_cols[2];
    let v_sorted = &main_segment_cols[3];
    let m = &main_segment_cols[4];

    // 挑战
    let z = &challenges[0];
    let alpha = &challenges[1];

    let trace_len = trace.num_rows();
    let mut aux_col = Vec::new();

    // s_0 = m_0/(z - (a'_0 + α * v'_0) - 1/(z - (a_0 + α * v_0)
    let unsorted_term = (-(&a[0] + &v[0] * alpha) + z).inv().unwrap();
    let sorted_term = (-(&a_sorted[0] + &v_sorted[0] * alpha) + z).inv().unwrap();
    aux_col.push(&m[0] * sorted_term - unsorted_term);

    // 将排列转换约束中给出的相同方程应用于 trace 的其余部分。
    // s_{i+1} = s_i + m_{i+1}/(z - (a'_{i+1} + α * v'_{i+1}) - 1/(z - (a_{i+1} + α * v_{i+1})
    for i in 0..trace_len - 1 {
        let unsorted_term = (-(&a[i + 1] + &v[i + 1] * alpha) + z).inv().unwrap();
        let sorted_term = (-(&a_sorted[i + 1] + &v_sorted[i + 1] * alpha) + z)
            .inv()
            .unwrap();
        aux_col.push(&aux_col[i] + &m[i + 1] * sorted_term - unsorted_term);
    }

    for (i, aux_elem) in aux_col.iter().enumerate().take(trace.num_rows()) {
        trace.set_aux(i, 0, aux_elem.clone())
    }
}

转换约束

现在，让我们看看如何使用 LogUp 为连续只读存储器定义转换约束。 前一篇文章中解释的前两个转换约束保持不变。 也就是说，我们不需要对 ContinuityConstraint 和 SingleValueConstraint 进行任何修改，因为使用 $a'$ 和 $v'$ 列验证内存是否为只读和连续的方法保持不变。

但是，修改第三个约束（称为 PermutationConstraint）至关重要。 此约束确保正确构造辅助列 $s$。 必须检查 $s_i$ 是否满足之前提到的方程：

$s_{i+1}=si+\frac{m{i+1}}{z-(a'{i+1}+\alpha v'{i+1})}-\frac{1}{z-(a{i+1}+\alpha v{i+1})}$ 其中 $i \in {0,\dots,n-2}$。

由于约束必须在没有除法的情况下表达，因此我们将等式的两边都乘以公分母。 这会将约束转换为以下形式：

$s{i+1} \cdot (z-(a'{i+1}+\alpha v'{i+1})) \cdot (z-(a{i+1}+\alpha v_{i+1})) == si \cdot (z-(a'{i+1}+\alpha v'{i+1})) \cdot (z-(a{i+1}+\alpha v{i+1})) + m{i+1} \cdot (z-(a{i+1}+\alpha v{i+1})) - (z-(a'{i+1}+\alpha v'{i+1}))$

此外，我们将等式的左侧移动到右侧，将其减去，以便可以将其解释为变量 $s$、$a$、$a'$、$v$ 和 $v'$ 中的多项式，该多项式等于零：

$0=si \cdot (z-(a'{i+1}+\alpha v'{i+1})) \cdot (z-(a{i+1}+\alpha v{i+1})) + m{i+1} \cdot (z-(a{i+1}+\alpha v{i+1})) - (z-(a'{i+1}+\alpha v'{i+1})) - s{i+1} \cdot (z-(a'{i+1}+\alpha v'{i+1})) \cdot (z-(a{i+1}+\alpha v_{i+1}))$

可以在 PermutationConstraint 实现中的 evaluate() 函数中找到此公式。 值得一提的是，证明者和验证者都必须以相同的方式评估多项式约束。 但是，由于每个人使用的 frames 类型都不同，因此我们被迫将此评估分为两种情况。

fn evaluate(
    &self,
    evaluation_context: &TransitionEvaluationContext<F, E>,
    transition_evaluations: &mut [FieldElement<E>],
) {
    // 在两个评估上下文中，Prover 和 Verfier 将以相同的方式评估转换多项式。
    // 唯一的区别是 Prover 的 Frame 具有基本域和域扩展元素，
    // 而 Verfier 的 Frame 仅具有域扩展元素。
    match evaluation_context {
        TransitionEvaluationContext::Prover {
            frame,
            periodic_values: _periodic_values,
            rap_challenges,
        } => {
            let first_step = frame.get_evaluation_step(0);
            let second_step = frame.get_evaluation_step(1);

            // 辅助 frame 元素
            let s0 = first_step.get_aux_evaluation_element(0, 0);
            let s1 = second_step.get_aux_evaluation_element(0, 0);

            // 挑战
            let z = &rap_challenges[0];
            let alpha = &rap_challenges[1];

            // 主 frame 元素
            let a1 = second_step.get_main_evaluation_element(0, 0);
            let v1 = second_step.get_main_evaluation_element(0, 1);
            let a_sorted_1 = second_step.get_main_evaluation_element(0, 2);
            let v_sorted_1 = second_step.get_main_evaluation_element(0, 3);
            let m = second_step.get_main_evaluation_element(0, 4);

            let unsorted_term = -(a1 + v1 * alpha) + z;
            let sorted_term = -(a_sorted_1 + v_sorted_1 * alpha) + z;

            // 我们正在使用以下 LogUp 方程：
            // s1 = s0 + m / sorted_term - 1/unsorted_term。
            // 由于约束必须在没有除法的情况下表达，因此我们将每个项乘以 sorted_term * unsorted_term：
            let res = s0 * &unsorted_term * &sorted_term + m * &unsorted_term
                - &sorted_term
                - s1 * unsorted_term * sorted_term;

            // eval 始终存在，除非约束 idx 定义不正确。
            if let Some(eval) = transition_evaluations.get_mut(self.constraint_idx()) {
                *eval = res;
            }
        }

        TransitionEvaluationContext::Verifier {
            frame,
            periodic_values: _periodic_values,
            rap_challenges,
        } => {
            let first_step = frame.get_evaluation_step(0);
            let second_step = frame.get_evaluation_step(1);

            // 辅助 frame 元素
            let s0 = first_step.get_aux_evaluation_element(0, 0);
            let s1 = second_step.get_aux_evaluation_element(0, 0);

            // 挑战
            let z = &rap_challenges[0];
            let alpha = &rap_challenges[1];

            // 主 frame 元素
            let a1 = second_step.get_main_evaluation_element(0, 0);
            let v1 = second_step.get_main_evaluation_element(0, 1);
            let a_sorted_1 = second_step.get_main_evaluation_element(0, 2);
            let v_sorted_1 = second_step.get_main_evaluation_element(0, 3);
            let m = second_step.get_main_evaluation_element(0, 4);

            let unsorted_term = z - (a1 + alpha * v1);
            let sorted_term = z - (a_sorted_1 + alpha * v_sorted_1);

            // 我们正在使用以下 LogUp 方程：
            // s1 = s0 + m / sorted_term - 1/unsorted_term。
            // 由于约束必须在没有除法的情况下表达，因此我们将每个项乘以 sorted_term * unsorted_term：
            let res = s0 * &unsorted_term * &sorted_term + m * &unsorted_term
                - &sorted_term
                - s1 * unsorted_term * sorted_term;

            // eval 始终存在，除非约束 idx 定义不正确。
            if let Some(eval) = transition_evaluations.get_mut(self.constraint_idx()) {
                *eval = res;
            }
        }
    }
}

另一个值得注意的改变是，与此约束关联的多项式现在是 3 次的。 如果我们观察到前面提到的零相等方程中，存在包含三个因子乘积的项，从而导致三个变量相乘，则这很容易理解。

值得强调的是，到目前为止，无论是在之前的文章中还是在其他两个转换约束中，我们都只处理了 2 次多项式。 此更改反映在代码中的两个位置。 首先，我们必须在定义转换约束时指定其 degree (阶数)：

impl<F, E> TransitionConstraint<F, E> for PermutationConstraint<F, E>
where
    F: IsSubFieldOf<E> + IsFFTField + Send + Sync,
    E: IsField + Send + Sync,
{
    fn degree(&self) -> usize {
        3
    }

    // ...
}

其次，在实现 AIR 时，我们必须指定 composition polynomial (组合多项式) 的 degree bound (次数界限)。 在以前的实现中，此数字设置为等于 trace 的长度。 但是，在这种情况下，将其扩大两倍非常重要。 这确保了当证明者定义组合多项式时，她可以将其分成两部分。 如果我们不这样做，证明者和验证者将处理整个组合多项式而不对其进行拆分，从而增加 FRI 轮数（优化）。

fn composition_poly_degree_bound(&self) -> usize {
    self.trace_length() * 2
}

边界约束

最后，让我们讨论如何定义 boundary constraints (边界约束)。 与主 trace 相关的所有 boundary constraints (边界约束) 将保持不变：我们需要确保 $a_0$、$a'_0$、$v_0$ 和 $v'_0$ 与 public inputs (公共输入) 中指定的值匹配。 此外，我们需要包含一个额外的约束来验证 $m_0$ 是否根据 public inputs (公共输入) 中描述的值正确定义。

现在，与 Grand Product (大乘积) 中使用的辅助 trace 的约束相比，辅助 trace 的约束将略有变化。 按照我们当时所做的相同逻辑，我们必须一方面确保辅助列 $s$ 的第一个元素被正确构造——也就是说，$s_0$ 满足前面 辅助 Trace 部分中描述的方程。 另一方面，我们需要检查最后一个元素 $s_{n-1}$ 是否等于零，以确保所有项都抵消并且验证 trace 是否对应于 permutation (排列)。

fn boundary_constraints(
    &self,
    rap_challenges: &[FieldElement<Self::FieldExtension>],
) -> BoundaryConstraints<Self::FieldExtension> {
    let a0 = &self.pub_inputs.a0;
    let v0 = &self.pub_inputs.v0;
    let a_sorted_0 = &self.pub_inputs.a_sorted_0;
    let v_sorted_0 = &self.pub_inputs.v_sorted_0;
    let m0 = &self.pub_inputs.m0;
    let z = &rap_challenges[0];
    let alpha = &rap_challenges[1];

    // 主要的 boundary constraints (边界约束)
    let c1 = BoundaryConstraint::new_main(0, 0, a0.clone().to_extension());
    let c2 = BoundaryConstraint::new_main(1, 0, v0.clone().to_extension());
    let c3 = BoundaryConstraint::new_main(2, 0, a_sorted_0.clone().to_extension());
    let c4 = BoundaryConstraint::new_main(3, 0, v_sorted_0.clone().to_extension());
    let c5 = BoundaryConstraint::new_main(4, 0, m0.clone().to_extension());

    // 辅助 boundary constraints (边界约束)
    let unsorted_term = (-(a0 + v0 * alpha) + z).inv().unwrap();
    let sorted_term = (-(a_sorted_0 + v_sorted_0 * alpha) + z).inv().unwrap();
    let p0_value = m0 * sorted_term - unsorted_term;

    let c_aux1 = BoundaryConstraint::new_aux(0, 0, p0_value);
    let c_aux2 = BoundaryConstraint::new_aux(
        0,
        self.trace_length - 1,
        FieldElement::<Self::FieldExtension>::zero(),
    );

    BoundaryConstraints::from_constraints(vec![c1, c2, c3, c4, c5, c_aux1, c_aux2])
}

总结

在这篇文章中，我们通过前一篇文章中解释的连续只读存储器的例子来探索查找参数方法 LogUp。 通过更改 trace 表的某些列的构造、permutation (排列) 转换约束以及其他一些小细节，我们使用这种新方法调整了我们已经为该示例所做的实现。

• 原文链接： blog.lambdaclass.com/log...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～