排列论证 - The Permutation Argument

排列论证是一种证明两个列表拥有相同元素，但可能顺序不同的证明。例如，[2,3,1] 是 [1,2,3] 的一种排列，反之亦然。

排列论证对于证明一个列表是另一个列表的排序版本很有用。也就是说，如果列表 B 具有与列表 A 相同的元素，并且 B 的元素已排序，那么我们就知道证明者已正确排序 A。

要确定两个列表是否相同，我们通常对它们进行排序并逐个元素地进行比较。

但是，要知道一个列表是否已排序，我们需要检查 1) 元素是否按顺序排列，以及 2) 排序算法的输出是否包含与输入相同的元素。

这会产生一个循环依赖——要知道一个列表是另一个列表的排列，我们必须知道它们的排序版本是相同的。但是要知道排序算法是否正确执行，我们必须知道排序的输出是输入的排列。

这在常规代码中不是问题，但在 ZK 中，我们必须约束计算的每个步骤。

我们已经展示了如何证明一个列表已排序。本章重点介绍如何证明两个列表是彼此的排列。

选项 1：为排序算法编写约束

在前面的章节中，我们展示了如何为选择排序算法编写约束。选择排序算法在 O(n2) 时间内运行，因此它将具有 O(n2) 个约束。我们可以使用更高效的算法（如归并排序）在 O(nlog⁡n) 个约束中完成相同的操作，但正如我们将看到的，存在更好的解决方案。

选项 2：尝试直接约束一对一映射

可以尝试直接编写一个电路，当且仅当一个列表是另一个列表的排列时，该电路才满足。换句话说，一个列表中的每个元素在另一个列表中都有一个匹配的元素，反之亦然。

例如，为了证明 [a1, a2, a3] 是 [b1, b2, b3] 的排列，我们需要显示两者之间的映射，证明每个 a_i 映射到 b 列表中的某个元素，并且每个 b_i 映射到 a 列表中的某个元素就足够了。

为了创建一个电路来证明双重映射，我们创建一个由 s 信号组成的矩阵，定义如下：

               b1             b2             b3
    --------------------------------------------
a1 | s11 = (a1-b1)  s12 = (a1-b2)  s12 = (a1-b3)
a2 | s21 = (a2-b1)  s22 = (a2-b2)  s23 = (a2-b3)
a3 | s31 = (a3-b1)  s32 = (a3-b2)  s33 = (a3-b3)

请注意，如果 s 信号为 0，则相应的 a 元素和 b 元素相等。例如，如果 a3 == b1，则 s31 将为 0。

如果我们然后按行和按列将 s 信号相乘，并将它们的乘积约束为 o 信号，如下所示，那么如果至少有一个匹配的元素，o 信号将为零。

     b1      b2      b3
a1  s11  ×  s12  ×  s13   =  o_row1
     ×       ×       ×
a2  s21  ×  s22  ×  s23   =  o_row2
     ×       ×       ×
a3  s31  ×  s3...