选择排序的零知识证明

感兴趣的大多数计算通常是“有状态的”——也就是说，它们需要经过一系列步骤才能产生最终结果。

有时，我们不需要展示我们执行了计算，而只需要展示结果。例如，如果 A 是一个列表，我们可以通过展示 B 是 A 的一个排列，并且 B 的所有元素都是有序的来证明 B 是列表 A 的排序版本。没有必要展示我们正确地执行了排序算法的每一步。我们已经展示了如何证明列表的元素是有序的，但是有效地证明一个列表是另一个列表的排列是非常棘手的，所以我们将在后面介绍这种技术。

一般来说，有许多实际的计算不允许简单地证明结果是正确的。值得注意的是，证明我们正确地执行了 sha256("RareSkills") 需要实际正确地执行哈希函数的每一步。

由于哈希函数有点吓人，我们通过展示如何正确地对列表执行选择排序来介绍有状态计算的概念。如上所述，这种方法是“过度杀伤”，因为证明输出列表是输入的已排序排列更简单——我们使用什么算法对列表进行排序并不重要。

然而，我们仍然展示选择排序算法，因为我们认为它是对有状态计算的一个温和的介绍。

选择排序的工作原理是：

• 迭代列表
• 在每个索引 i 处，将 i 处的值与包含 i 和前面每个项目的子列表（包括 i..n-1）进行比较
• 将 i 处的项目与子列表 i..n-1 的最小值交换

选择排序在下面的动画中进行了说明：

https://img.learnblockchain.cn/2025/04/16/SelectionSortC.mp4

由于信号在 ZK 电路中是不可变的，所以每次交换时，我们都需要创建一个新列表。例如，如果我们对 [5,2,3,4] 进行排序，状态转换的序列将是：

1. i = 0, [5,2,3,4] —> 交换 —> [2,5,3,4]
2. i = 1, [2,5,3,4] —> 交换 —> [2,3,5,4]
3. i = 2, [2,3,5,4] —> 交换 —> [2,3,4,5]

为了证明我们正确地执行了选择排序，我们需要证明在迭代 i 时，我们将 i 处的项目与子列表 i…n - 1 的最小值交换了。我们已经在前面的章节中构建了大部分所需的组件：

• 我们可以证明某个项目是列表的最小值，并且它位于某个索引处。
• 我们可以证明我们交换了列表中的两个项目。

在本章中，我们只是将这些组件组合在一起。首先，我们构建一个模板，该模板证明我们正确地识别了子列表中最小值的索引：

template GetMinAtIdx(n) {
  signal input in[n];

  // compute and constrain min and idx
  // to be the min value in the list
  // and the index of the minimum value
  signal output min;
  signal output idx;

  // compute the minimum and its index
  // outside of the constraints
  var minv = in[0];
  var idxv = 0;
  for (var i = 1; i < n; i++) {
    if (in[i] < minv) {
      minv = in[i];
      idxv = i;
    }
  }
  min <-- minv;
  idx <-- idxv;

  // constrain that min is ≤ all others
  component lte[n];
  for (var i = 0 ; i < n; i++) {
    lte[i] = LessEqThan(252);
    lte[i].in[0] <== min;
    lte[i].in[1] <== in[i];
    lte[i].out === 1;
  }

  // assert min is really at in[idx]
  component qs = QuinSelector(n);
  qs.index <== idx;
  for (var i = 0; i < n; i++) {
    qs.in[i] <== in[i];
  }
  qs.out === min;
}

排序算法的一次迭代

选择排序的第一步是将索引 0 处的项目与整个列表中的最小项目（可能是索引 0 处的项目）交换。以下是用于将特定索引处的数字与前面的最小项目交换的代码。

template Swap(n) {
  signal input in[n];
  signal input s;
  signal input t;
  signal output out[n];

  // NEW CODE to detect if s == t
  signal sEqT;
  sEqT <== IsEqual()([s, t]);

  // get the value at s
  component qss = QuinSelector(n);
  qss.index <== s;
  for (var i = 0; i < n; i++) {
    qss.in[i] <== in[i];
  }

  // get the value at t
  component qst = QuinSelector(n);
  qst.index <== t;
  for (var i = 0; i < n; i++) {
    qst.in[i] <== in[i];
  }

  component IdxEqS[n];
  component IdxEqT[n];
  component IdxNorST[n];
  signal branchS[n];
  signal branchT[n];
  signal branchNorST[n];
  for (var i = 0; i < n; i++) {
    IdxEqS[i] = IsEqual();
    IdxEqS[i].in[0] <== i;
    IdxEqS[i].in[1] <== s;

    IdxEqT[i] = IsEqual();
    IdxEqT[i].in[0] <== i;
    IdxEqT[i].in[1] <== t;

    // if IdxEqS[i].out + IdxEqT[i].out
    // equals 0, then it is not i ≠ s and i ≠ t
    IdxNorST[i] = IsZero();
    IdxNorST[i].in <== IdxEqS[i].out + IdxEqT[i].out;

    // if we are at index s, write in[t]
    // if we are at index t, write in[s]
    // else write in[i]
    branchS[i] <== IdxEqS[i].out * qst.out;
    branchT[i] <== IdxEqT[i].out * qss.out;
    branchNorST[i] <== IdxNorST[i].out * in[i];

    // multiply branchS by zero if s equals t
    out[i] <==  (1-sEqT) * (branchS[i]) + branchT[i] + branchNorST[i];
  }
}

template Select(n, start) {
  // unsorted list
  signal input in[n];

  // index start swapped with the min
  signal output out[n];

  // we will define GetMinAtIdxStartingAt in the next codeblock
  component minIdx0 = GetMinAtIdxStartingAt(n, start);
  for (var i = 0; i < n; i++) {
      minIdx0.in[i] <== in[i];
  }

  component Swap0 = Swap(n);
  Swap0.s <== start; // swap 0 with the min
  Swap0.t <== minIdx0.idx; // with the min (could be idx 0)
  for (var i = 0; i < n; i++) {
      Swap0.in[i] <== in[i];
  }

  // copy to out
  for (var i = 0; i < n; i++) {
      out[i] <== Swap0.out[i];
  }
}

当然，我们应该对这个进行参数化，因为我们将在索引 0…n - 2 中重复此过程。为此，我们将修改 GetMinAtIdx 以仅考虑 start 索引之后的值：

// formerly GetMinAtIdx
template GetMinAtIdxStartingAt(n, start) {
  signal input in[n];
  signal output min;
  signal output idx;

  // only look for values start and later
  var minv = in[start];
  var idxv = start;
  for (var i = start +...