本文档介绍了使用排列参数证明两个列表包含相同的元素,但顺序可能不同的证明。
排列论证是一种证明两个列表拥有相同元素,但可能顺序不同的证明。例如,[2,3,1]
是 [1,2,3]
的一种排列,反之亦然。
排列论证对于证明一个列表是另一个列表的排序版本很有用。也就是说,如果列表 B 具有与列表 A 相同的元素,并且 B 的元素已排序,那么我们就知道证明者已正确排序 A。
要确定两个列表是否相同,我们通常对它们进行排序并逐个元素地进行比较。
但是,要知道一个列表是否已排序,我们需要检查 1) 元素是否按顺序排列,以及 2) 排序算法的输出是否包含与输入相同的元素。
这会产生一个循环依赖——要知道一个列表是另一个列表的排列,我们必须知道它们的排序版本是相同的。但是要知道排序算法是否正确执行,我们必须知道排序的输出是输入的排列。
这在常规代码中不是问题,但在 ZK 中,我们必须约束计算的每个步骤。
我们已经展示了如何证明一个列表已排序。本章重点介绍如何证明两个列表是彼此的排列。
在前面的章节中,我们展示了如何为选择排序算法编写约束。选择排序算法在 O(n2) 时间内运行,因此它将具有 O(n2) 个约束。我们可以使用更高效的算法(如归并排序)在 O(nlogn) 个约束中完成相同的操作,但正如我们将看到的,存在更好的解决方案。
可以尝试直接编写一个电路,当且仅当一个列表是另一个列表的排列时,该电路才满足。换句话说,一个列表中的每个元素在另一个列表中都有一个匹配的元素,反之亦然。
例如,为了证明 [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...
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!