本文介绍了如何将计算问题转化为算术电路,从而利用zk-SNARKs进行高效验证。文章详细解释了算术电路和R1CS(Rank-One Constraint System)的概念,以及如何使用编译器将高级代码转换为算术电路。同时,讨论了非原生数据类型和操作在算术电路中的表示方法,以及SNARK友好的密码学原语的重要性。
高效的 zk-SNARKs(零知识简洁非交互式知识论证)的使用催生了许多新的和重要的应用。例如,我们可以将昂贵的计算委托给不受信任的服务器,并收到证明显示计算的完整性。这个证明很短,并且可以比重新执行整个计算的简单方法更快地验证。这怎么可能呢?关键的想法是,计算的完整性可以表示为非确定性多项式(NP)完全问题的解或可满足性。在我们解释 NP 完全意味着什么之前,让我们看一个例子。当你用高级语言编写代码时,编译器会将其转换为机器代码。然后在处理器中执行它,处理器具有用于执行必要操作的专用电路。我们可以用某种电路的形式表达任何复杂的计算。SNARK 的想法是,我们可以将代码转换为由整数的加法和乘法等运算组成的算术电路,并通过检查计算中涉及的值是否满足电路来证明执行的正确性。
一个 NP 完全问题是这样的:
NP 完全问题的例子包括电路可满足性、图着色问题和旅行商问题。
我们不想每次想编写代码时都写下对应于程序的电路。这样做就像用汇编语言或机器代码编写代码,而不是使用更高级的语言。为此,我们需要构建一个专用的编译器,它可以读取我们的代码并将其转换为算术电路。我们将看到一些运算导致了作为算术电路的直接表示(例如整数的加法或乘法)。相比之下,其他简单的函数,例如 XOR、AND 或相等性检查,具有更复杂的结构。
算术电路是一个有向无环图,涉及数字的乘法和加法。我们可以将其视为评估那些数字上的某些多项式。例如,以下电路表达了以下多项式的计算,$p(x) = x^3 + x^2 + 1$

我们也可以有采用不同值的电路,并表示一个多元多项式,例如 $p(x_1, x_2) = x_1x_2 + x_1 + x_2^2$。

算术电路也可以表示为 rank one constraint system,使得它们之间存在一一对应关系。
正如我们提到的,我们唯一的运算是加法和乘法;诸如除法之类的运算必须被模拟。例如,如果我们想执行
$a/b = c$
我们可以引入一个额外的变量($b$ 的乘法逆元,即 $b^{-1}$),
$x \times b = 1$
$a \times x = c$
第一个条件确保 $x$ 是 $b^{-1}$,第二个条件执行我们想要的计算。算术电路看起来像

我们也可以通过记住整数的乘法逆元(使用模运算)是 $b^{-1} = b^{p-2}$ 来解决这个问题。然而,这导致了一个更复杂的电路,因为我们通常必须评估一个大的 power,即使高效地完成($\log(p)$ 的数量级),也需要许多乘法门。因此,当尝试用算术电路表达非原生运算时,我们必须考虑最有效的方式。
(二次)秩 1 约束系统是以下形式的方程组:
$(a{01} + \sum a{k1}xk)(b{01} + \sum b_{k1}xk) = (c{01} + \sum c_{k1}xk)(a{01} + \sum a_{k1}xk)(b{01} + \sum b_{k1}xk) = (c{01} + \sum c_{k1}x_k)$
$(a{02} + \sum a{k2}xk)(b{02} + \sum b_{k2}xk) = (c{02} + \sum c_{k2}xk)(a{02} + \sum a_{k2}xk)(b{02} + \sum b_{k2}xk) = (c{02} + \sum c_{k2}x_k)$
$(a{0n} + \sum a{kn}xk)(b{0n} + \sum b_{kn}xk) = (c{0n} + \sum c_{kn}xk)(a{0n} + \sum a_{kn}xk)(b{0n} + \sum b_{kn}xk) = (c{0n} + \sum c_{kn}x_k)$
数字 $n$ 给出了系统中约束的总数。我们可以证明任何有界计算都可以表示为 R1CS。如果我们想执行像 $y^5$ 这样的计算,该怎么办?我们可以使用一种称为扁平化的简单方法。我们为中间计算引入新变量:
$y \times y = y_1 = y^2$
$y \times y_1 = y_2 = y^3$
$y_1 \times y_2 = y_3 = y^5$
对于这个简单的计算,向量 $x$ 仅仅是 $x = (y, y_1, y_2, y3)$。大多数元素 $a{ij}, b{ij}, c{ij}$ 都是零。非零元素是 $a{11}, b{11}, c{11}, a{12}, b{22}, c{32}, a{23}, b{33}, c_{34}$,它们都等于 1。我们也可以将 R1CS 表示为
$y \times y = y_1$
$y_1 \times y_1 = y_2$
$y \times y_2 = y_3$
两者表示相同的计算,但约束看起来有点不同。因此,对于给定的问题,可以有多种表示形式。
R1CS 跟踪计算中涉及的值以及变量之间的关系。我们有一个决定函数来检查变量 $x$ 的给定赋值是否满足 R1CS。我们必须将 $x$ 的值替换到方程组中,并查看左右两边是否相等。等效地,
$(a{01} + \sum a{k1}xk)(b{01} + \sum b_{k1}xk) - (c{01} + \sum c_{k1}x_k) = 0$
$(a{02} + \sum a{k2}xk)(b{02} + \sum b_{k2}xk) - (c{02} + \sum c_{k2}x_k) = 0$
$(a{0n} + \sum a{kn}xk)(b{0n} + \sum b_{kn}xk) - (c{0n} + \sum c_{kn}x_k) = 0$
R1CS 的一个优点是它的模块化。如果我们有两个约束系统,$CS_1, CS_2$,我们可以获得一个新的 $CS_3$,它必须满足这两个系统。
我们已经看到,电路和 R1CS 具有模块化属性,允许我们通过组合更简单的电路或方程组来推导出更复杂的电路或方程组。我们可以通过开发一个编译器来利用这一点,该编译器生成与每个数据类型和相关运算相关的电路/约束。
算术电路的本地元素是域元素,即 $0, 1, 2, 3, \dots, p$,我们也可以将其解释为 $-p/2 + 1, -p/2 + 2, \dots, 0, 1, 2, \dots, p/2$,以及运算 $+$ 和 $\times$。诸如 u8、u16、u64 和 i128 之类的数据类型不是,并且必须满足特定的属性。同样,我们必须用算术电路来表达它们的运算。例如,u16 是一个介于 0 和 65535 之间的整数值,远小于域元素的范围。如果我们想要这样的数据类型,我们必须执行范围检查以确保该值在 0 到 65535 之间。这个条件增加了开销,因为我们必须向与范围检查相关的电路添加约束。
布尔变量也面临类似的问题。在普通电路中,布尔值直接与一位相关联,并且位之间的运算已经过性能优化。如果我们想要表示一个布尔变量,它仅取值 0 和 1,我们必须添加约束来强制执行这些值。确保这一点的一个简单方法是让变量 $b$ 满足以下等式
$b(1 - b) = 0$
与此等式相关的算术电路如下所示,并显示了三个门:两个乘法和一个加法。

如果我们想要计算 $c = \neg b$,我们需要首先知道如何以电路形式表示 NOT。以下等式可以表示它
$c = 1 - b$
电路表示是,

如果我们对两个电路进行简单的粘贴,我们会得到

我们看到有很多重复的元素(例如 $1, -1, -b$。在后面的阶段,我们可以优化电路,使其不引入冗余元素或计算,因为这些只会增加证明时间。
假设我们想要用它的位表示(比如 u16)来表示一个整数 $k$。在这种情况下,我们有 16 位,$b_k$,每一位都有相同的电路(这意味着我们有 32 个乘法门和 16 个加法门),加上额外的检查,如下所示:
$k = \sum_{j=0}^{15} 2^j b_j$
一个简单的门不能代表按位运算,例如 AND、XOR 和 NOT。如果我们想以一种简单的方式执行 $a \oplus b$(在两个位串之间执行 XOR 运算,这通常会在流密码(例如 ChaCha20)中完成),我们需要表示以下内容:
我们可以使用两种解决方案来避免这个缺点。首先,我们可以创建显示输入和输出之间关系的表,并通过查看组合是否在表中来检查计算的有效性,而不是尝试通过字段运算的组合来表示每个非算术运算。例如,我们可以将 XOR 所有 8 位字符串的结果存储在表中,然后使用查找参数进行检查。这样,我们可以减少约束的数量,降低生成多项式的次数,并加快证明生成时间。
第二个解决方案是使用新的、对 SNARK 友好的加密函数。我们可以说,对 SNARK 友好的原语在算术电路中具有简单的表示形式(可以使用少量约束来表示它们);它们通常尝试使用该字段中的原生运算。SNARK 友好哈希函数的例子是 Poseidon 和 Rescue。
电路编译器分阶段工作。在第一阶段,编译器从主函数开始。它首先用它们对应的电路替换函数,并添加必要的变量以及与它们的数据类型相关的电路。在第二阶段,输入变量被替换为它们的实际值和所有中间结果,从而获得约束系统的解。
为了将代码转换为算术电路,我们可以实现 gadgets。这些仅仅是给出计算问题的一个构建块行为的元素。例如,我们可以实现一个 gadget 来测试两个整数的相等性,或者一个执行两个字符串连接的 gadget。给定模块化属性,我们可以将所有内容粘合在一起并获得大型电路。例如,Arkworks 提供了使用 gadgets 将代码转换为 R1CS 的工具。
给定计算的完整性可以表示为 NP 完全问题的可满足性或解,例如算术电路可满足性。为此,我们将整个计算转换为算术电路,其中本机元素是域元素(而不是位),并且域元素的加法和乘法是电路中的自然运算。我们可以等效地将电路表示为约束系统,例如 R1CS。鉴于电路和 R1CS 的模块化属性,我们可以将代码转换为电路的工作留给专用的编译器,该编译器获取每个数据类型及其运算,并将其转换为电路形式。所有非原生数据类型及其运算都必须根据原生元素和运算来定义,这使得某些运算(例如按位 AND、XOR、NOT)变得昂贵。反过来,这种转换使得对于 zk-SNARK 来说,完善的加密原语变得昂贵,因为每个函数都会添加许多约束。新的、对 SNARK 友好的原语和查找表的开发可以帮助降低电路表示的复杂性并加快证明的生成。
- 原文链接: blog.lambdaclass.com/how...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!