大多数令人关注的计算通常是“有状态的”（stateful）——也就是说，它们需要经历一系列步骤才能产生最终结果。

有时候，我们不需要证明我们执行了计算，只需展示结果即可。例如，如果 A 是一个列表，我们可以通过证明 B 是 A 的排列（permutation）并且 B 中的所有元素都是有序的，来证明 B 是列表 A 的排序版本。我们不需要证明我们正确地执行了排序算法的每一个步骤。我们已经展示了如何证明列表中的元素是有序的，但高效地证明一个列表是另一个列表的排列却出乎意料地棘手，因此我们稍后会介绍这项技术。

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

由于哈希函数有点令人望而生畏，我们通过展示如何证明我们对一个列表正确地执行了选择排序（Selection Sort），来介绍有状态计算的概念。如上所述，这种方法有些“大材小用”，因为直接证明输出列表是输入列表的有序排列会更简单——使用什么算法对列表进行排序并不重要。

然而，我们仍然展示选择排序算法，因为我们认为它是对有状态计算的一个平缓的入门。

选择排序的工作原理如下：

• 遍历列表
• 在每个索引 i 处，将 i 处的值与包含 i 及其后面每一个项的子列表（包含 i..n-1）进行比较
• 将 i 处的项与子列表 i..n-1 中的最小值进行交换

下方的动画演示了选择排序的过程：

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

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

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

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

在本章中，我们将简单地把这些组件组合在一起。首先，我们构建一个 template，用于证明我们正确找出了子列表中最小值的索引：

Copy
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 处的项）。下面的代码用于将特定索引处的数字与其后面的最小项进行交换。

Copy
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++) {
    dxEqS[i] = IsEqual();
    dxEqS[i].in[0] <== i;
    dxEqS[i].in[1] <== s;

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

    / if IdxEqS[i].out + IdxEqT[i].out
    / equals 0, then it is not i ≠ s and i ≠ t
    dxNorST[i] = IsZero();
    dxNorST[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]
    ranchS[i] <== IdxEqS[i].out * qst.out;
    ranchT[i] <== IdxEqT[i].out * qss.out;
    ranchNorST[i] <== IdxNorST[i].out * in[i];
    
    / multiply branchS by zero if s equals t
    ut[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 索引之后的值：

Copy
// 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 + 1; i < n; i++) {
    if (in[i] < minv) {
      minv = in[i];
      idxv = i;
    }
  }
  min <-- minv;
  idx <-- idxv;

  // only compare to values start and later
  component lt[n];
  
  // CHANGES HERE: LOOP FROM START TO N-1
  for (var i = start ; i < n; i++) {
    lt[i] = LessEqThan(252);
    lt[i].in[0] <== min;
    lt[i].in[1] <== in[i];
    lt[i].out === 1;
  }

  // Quin Selector -- ensure that
  // 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;
}

最终算法

要证明我们正确执行了选择排序，我们只需将上面的 template 重复 n - 2 次即可。

Copy
include "circomlib/comparators.circom";

// ----QUIN SELECTOR ----
template CalculateTotal(n) {
  signal input in[n];
  signal output out;

  signal sums[n];

  sums[0] <== in[0];

  for (var i = 1; i < n; i++) {
    sums[i] <== sums[i-1] + in[i];
  }

  out <== sums[n-1];
}

// from https://github.com/darkforest-eth/circuits/blob/master/perlin/QuinSelector.circom
template QuinSelector(choices) {
  signal input in[choices];
  signal input index;
  signal output out;
  
  // Ensure that index < choices
  component lessThan = LessThan(4);
  lessThan.in[0] <== index;
  lessThan.in[1] <== choices;
  lessThan.out === 1;

  component calcTotal = CalculateTotal(choices);
  component eqs[choices];

  // For each item, check whether its index equals the input index.
  for (var i = 0; i < choices; i ++) {
    eqs[i] = IsEqual();
    eqs[i].in[0] <== i;
    eqs[i].in[1] <== index;

    // eqs[i].out is 1 if the index matches. As such, at most one input to
    // calcTotal is not 0.
    calcTotal.in[i] <== eqs[i].out * in[i];
  }

  // Returns 0 + 0 + 0 + item
  out <== calcTotal.out;
}

// Given array in[n]
// swap the items at index
// s and t
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];
  }
}

// Find the smallest element starting
// at index start
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 + 1; i < n; i++) {
    if (in[i] < minv) {
      minv = in[i];
      idxv = i;
    }
  }
  min <-- minv;
  idx <-- idxv;

  // only compare to values start and later
  component lt[n];
  
  // CHANGES HERE: LOOP FROM START TO N-1
  for (var i = start ; i < n; i++) {
    lt[i] = LessEqThan(252);
    lt[i].in[0] <== min;
    lt[i].in[1] <== in[i];
    lt[i].out === 1;
  }

  // Quin Selector -- ensure that
  // 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;
}

// Given an array in, swap
// start with the smallest element
// in front of it
template Select(n, start) {
  // unsorted list
  signal input in[n];
  
  // index 0 swapped with the min
  signal output out[n];

  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];
  }
}

// ---- CORE ALGORITHM ----
template SelectionSort(n) {
  assert(n > 0);

  signal input in[n];
  signal output out[n];

  signal intermediateStates[n][n];

  component SSort[n - 1];
  for (var i = 0; i < n; i++) {
    // copy the input to the first row of
    // intermediateStates. Note that we can do
    // if(i == 0) because i is not a signal
    // and i is known at compile time
    if (i == 0) {
      for (var j = 0; j < n; j++) {
        intermediateStates[0][j] <== in[j];
      }
    }

    else {
      // select sort n items starting at i - 1
      // for i = 1, we compare item at 0 to
      // the rest of the list
      SSort[i - 1] = Select(n, i - 1);
      
      // load in the intermediate state i -1
      for (var j = 0; j < n; j++) {
        SSort[i - 1].in[j] <== intermediateStates[i - 1][j];
      }
      // write the sorted result to row i
      for (var j = 0; j < n; j++) {
        SSort[i - 1].out[j] ==> intermediateStates[i][j];
      }
    }
  }

  // write the final state to the ouput
  for (var i = 0; i < n; i++) {
    intermediateStates[n-1][i] ==> out[i];
  }
}

component main = SelectionSort(9);

/* INPUT = {"in": [3,1,8,2,4,0,1,2,4]} */

结论

“中间状态”（intermediate state）的概念以及证明我们在中间状态之间进行了正确的转换，是实践中验证大多数 ZK 算法（特别是哈希函数和 ZK 虚拟机）的核心所在。本章介绍的选择排序算法为有状态计算提供了一个平缓的入门。