ACIR文档（草案）

摘要

本文档描述了ACIR的目的，它是什么以及如何使用ACIR程序由编译器和证明系统。它旨在成为ACIR的参考文档。

简介

ACIR的目的是在通用证明系统（如Aztec的Barretenberg）和前端（如Noir）之间建立联系，后者描述用户特定的计算。

更确切地说，Noir是一种零知识证明（ZKP）编程语言，允许用户使用接近Rust语法的高级语言以直观的方式编写程序。Noir能够生成Noir程序的执行证明，使用外部证明系统。然而，证明系统使用特定的低级基于约束的语言。同样，前端也有自己的内部表示来表示用户程序。

ACIR的目标是提供一个通用的开源中间表示，类似于证明系统“语言”，但与特定证明系统无关，既可以由证明系统使用，也可以作为前端的目标。因此，最终，ACIR程序只是程序的一种表示，专为证明系统设计。

抽象电路中间表示

ACIR代表抽象电路中间表示

• 抽象电路：电路是一个简单的计算模型，其中基本计算单元，称为门，通过电线连接。数据通过电线流动，门根据它们的输入计算输出电线。更正式地说，它们是带有顶点的有向无环图（DAG），其中顶点是门，边是电线。由于电线的不可变性质（其值在执行期间不会改变），它们非常适合描述ZKPs的计算。此外，当我们使用电路时，我们不会丢失任何表达性，因为众所周知，任何有界计算都可以转换为算术电路（即只有加法和乘法门的电路）。这里的“抽象”一词仅表示我们不是指实际的物理电路（如电子电路）。此外，我们不会完全使用电路模型，而将使用更适合ZKPs的另一个模型，即约束模型（见下文）。
• 中间表示：ACIR表示是中间表示，因为它位于前端和其证明系统之间。ACIR字节码将黑 Noir编译器的输出与证明系统后端输入之间的链接。

约束模型

生成特定程序已执行证明的第一步是执行此程序。由于证明系统将处理ACIR程序，因此我们实际上需要使用用户提供的输入执行ACIR程序。

在ACIR术语中，门称为操作码，电线称为部分见证。然而，我们不是通过电线连接操作码，而是创建约束：操作码约束一组电线。这种约束模型可以简单地取代电路模型。例如，加法门输出_wire = input_wire_1 + input_wire_2可以用以下算术约束表示：output_wire - (input_wire_1 + input_wire_2) = 0

求解

由于这些约束，执行ACIR程序被称为求解见证。从代表程序输入的见证中，其值由用户提供，我们可以通过按定义顺序逐个执行/求解约束来找出其他见证的值。

例如，如果input_wire_1和input_wire_2的值分别为3和8，则可以通过说output_wire是11来求解操作码output_wire - (input_wire_1 + input_wire_2) = 0。

总之，工作流程如下

1. 用户程序 -> (编译) ACIR，一组操作码，它们约束（部分）见证
2. 用户输入 + ACIR -> (执行/求解) 分配所有（部分）见证的值
3. 见证分配 + ACIR -> (证明系统) 证明

虽然从理论上讲，操作码的顺序无关紧要，因为方程组不依赖于其顺序，但在实践中，它对求解（即执行的性能）有很大影响。ACIR操作码必须按顺序排列，以便每个操作码都可以逐个解决。

见证的值位于证明系统的标量域中。我们将将其称为FieldElement或ACIR域。证明系统需要所有部分见证和所有约束的值才能生成证明。

备注：部分见证的值在整个程序执行过程中是唯一且固定的，尽管在某些罕见情况下，同一执行和见证可能有多个值（当有多个约束的有效解时）。见证可能有多个可能值可能表明电路不安全。

备注：为什么我们使用“部分见证”这个术语？这是因为证明系统可能创建其他约束和见证（特别是使用BlackBoxFuncCall，见下文）。证明是指完整的见证分配及其约束。ACIR操作码及其部分见证是获取完整约束和见证列表之前的中间表示。为了简单起见，我们现在将使用见证而不是部分见证。

ACIR参考

在此假设证明系统是Barretenberg。一些参数可能因其他证明系统而略有不同，特别是FieldElement的字节大小，对于Barretenberg来说是254。

某些操作码有输入和输出，这意味着输出被限制为从输入计算出的操作码的结果。求解器期望在解决此类操作码时所有输入都是已知的。

某些操作码不受限制，这意味着它们不会被证明系统使用，只由求解器使用。

最后，某些操作码将有一个谓词，其值为0或1。它的目的是当值为0时取消操作码，使其没有效果。请注意，删除操作码不是解决方案，因为这会修改电路（电路主要是操作码列表）。

备注：操作码作用于证据，但我们将看到某些操作码作用于证据的表达式。我们将一个表达式称为证据的线性组合和/或两个证据的乘积（以及一个常数项）。单个证据是一个（简单）表达式，反之，可以使用断言零操作码将表达式转换为单个证据（见下文）。所以基本上，使用证据或表达式是等效的，但后者在某些情况下可以避免创建证据。

断言零操作码

断言零操作码添加了约束P(w) = 0，其中w=(w_1,..w_n)是n个证据的元组，P是总次数不超过2的多项式。多项式的系数 ${q_M}_{i,j}, q_i,q_c$ 是定义操作码的已知值。断言零操作码的一般表达式如下：$\sum_{i,j} {q_M}_{i,j}w_iw_j + \sum_i q_iw_i +q_c = 0$

断言零操作码可以用于

• 表达证据的约束；例如，要表达证据 $w$ 是布尔值，可以添加操作码：$w*w-w=0$
• 或者，计算某些输入的算术运算的结果。例如，要乘以两个证据 $x$ 和 $y$，您将使用操作码 $z-x*y=0$，这将约束 $z$ 为 $x*y$。

求解器期望在执行操作码时最多只有一个证据是未知的。

黑盒函数调用操作码

这些操作码代表特定的计算。尽管任何计算都可以仅使用断言零操作码来完成，但这并不总是高效的。某些证明系统，特别是Aztec的证明系统，可以使用查找表等实现更高效的计算。黑盒函数调用操作码用于请求证明系统自行处理计算。所有黑盒函数都接受一个元组（证据，num_bits）作为输入，其中num_bits是一个表示输入证据字节大小的常数，并且它们有一个或多个证据作为输出。一些更高级的计算假设证明系统有一个'嵌入式曲线'。这是一个与证明系统的主曲线循环的曲线，即嵌入式曲线的标量场是主曲线的基域，反之亦然。证明系统使用的曲线取决于证明系统（及其/或其配置）。Aztec的Barretenberg使用BN254作为主曲线，Grumpkin作为嵌入式曲线。

ACIR支持的黑白盒函数

AES128Encrypt：使用CBC模式对提供的明文进行AES128加密，使用PKCS#7填充输入。

• 输入：字节数组 [u8; N]
• iv：初始化向量 [u8; 16]
• key：用户密钥 [u8; 16]
• 输出：长度为`input.len() + (16 - input.len() % 16)`的byte向量

AND：执行lhs和rhs的位与操作。bit_size必须对两个输入相同。

• lhs：（证据，bit_size）
• rhs：（证据，bit_size）
• 输出：一个值被限制为lhs AND rhs的见证，作为位宽为bit_size的位整数。

异或(XOR)：执行lhs和rhs的按位异或操作。bit_size必须对两个输入相同。

• lhs：（证据，bit_size）
• rhs：（证据，bit_size）
• 输出：一个值被限制为lhs XOR rhs的见证，作为位宽为bit_size的位整数。

范围(RANGE)：将输入限制为提供的位宽（witness, bit_size）

SHA256：计算输入的SHA256

• 输入是一个字节数组，即一个（FieldElement, 8）的向量。
• 输出是一个长度为32的字节数组，即一个包含32个（FieldElement, 8）的向量，被限制为输入的SHA256。

Blake2s：根据RFC7693计算输入的Blake2s哈希（https://tools.ietf.org/html/rfc7693）

• 输入是一个字节数组，即一个（FieldElement, 8）的向量。
• 输出是一个长度为32的字节数组，即一个包含32个（FieldElement, 8）的向量，被限制为输入的blake2s。

SchnorrVerify：在嵌入的曲线上验证Schnorr签名

• 输入包括
  • 公钥，作为2个（FieldElement, 254）
  • 签名，作为64字节向量（FieldElement, 8）
  • 消息，作为（FieldElement, 8）的向量
• 输出：表示签名验证结果的见证；失败为0，成功为1。

由于嵌入曲线的标量场不是ACIR场，因此（r,s）签名被表示为一个64字节的数组，用于两个域元素。另一方面，公钥坐标是ACIR场。证明系统决定消息的哈希方式。Barretenberg使用Blake2s。

PedersenCommitment：使用嵌入曲线的生成器计算输入的Pedersen承诺

• 输入：一个（FieldElement, 254）的向量
• 输出：表示结果Grumpkin点的x,y坐标的2个见证
• 域分隔符：一个常数公钥值（域元素），您可以将其用于使承诺也依赖于域分隔符。Noir使用0作为域分隔符。

后端应处理ACIR域元素和嵌入曲线的标量场之间的适当转换。在Aztec的Barretenberg中，后者比ACIR场大，因此很简单。Pedersen生成器由证明系统管理。

PedersenHash：使用嵌入曲线的生成器计算输入及其数量的Pedersen承诺

• 输入：一个（FieldElement, 254）的向量
• 输出：'prepended input'的Pedersen承诺的x坐标（见下文）
• 域分隔符：一个常数公钥值（域元素），您可以将其用于使哈希也依赖于域分隔符。Noir使用0作为域分隔符。

在Barretenberg中，PedersenHash执行与PedersenCommitment相同，但除了它将输入的前缀为它们的长度。

HashToField128Security：此操作码已弃用并将被删除。

EcdsaSecp256k1：在Secp256k1上验证ECDSA签名

• 输入
  • 公钥x坐标，32字节
  • 公钥y坐标，32字节
  • 签名，64字节数组
  • 消息的哈希，字节向量
• 输出：失败为0，成功为1

输入和输出类似于SchnorrVerify，除了我们使用不同的曲线（secp256k1），因此签名和公钥中涉及的域元素被定义为32字节的数组。另一个区别是，我们假设消息已经被哈希。

EcdsaSecp256r1：与EcdsaSecp256k1相同，但在另一个曲线上执行。

MultiScalarMul：对嵌入曲线的变量基/输入点（P）执行标量乘法

• 输入：点（FieldElement, N）输入点的x和y坐标的向量[x1, y1, x2, y2,...]。标量（FieldElement, N）输入标量的低和高部分[s1_low, s1_high, s2_low, s2_high, ...]。（FieldElement, N）对于Barretenberg，它们都必须小于128位。
• 输出：(FieldElement, N) 输出点的 x 和 y 坐标向量 [op1_x, op1_y, op2_x, op2_y, ...]。点按 $s_{low}P + s_{high}2^{128}*P$ 计算得出。

由于 Grumpkin 标量场大于 ACIR 场，我们提供 2 个 ACIR 场，分别代表 Grumpkin 标量 $a$ 的低和高部分：$a=low+high*2^{128}$，其中 $low, high < 2^{128}$。

Keccak256：计算输入的 Keccak-256（以太坊版本）。

• 输入：字节向量（FieldElement，8）
• 输出：32 字节向量（FieldElement，8）

Keccak256VariableLength：计算输入的 Keccak-256（以太坊版本），长度限制在给定值。

• 输入：字节向量（FieldElement，8）
• var_message_size：要哈希的输入数量；它必须小于（或等于）输入长度
• 输出：32 字节向量（FieldElement，8）

RecursiveAggregation：在电路中验证证明。**警告：此操作码可能发生变化。**

• verification_key：表示正在验证的电路验证密钥的（FieldElement，254）向量
• public_inputs：表示要验证的证明对应的公输入的（FieldElement，254）向量
• key_hash：一个（FieldElement，254）。它应该是验证密钥的哈希。Barretenberg 期望验证密钥的 Pedersen 哈希
• input_aggregation_object：一个可选的（FieldElement，254）向量。它是证明系统特有的数据块。
• output_aggregation_object：函数返回的一些证据，表示证明系统内部的一些数据。

此黑盒函数并不完全验证证明，它所做的是验证 key_hash 是否确实是验证密钥的哈希，使用户可以将验证密钥作为私输入，只将 key_hash 作为公输入，这更高效。它还做的一件事是准备证明的验证。为了完全验证证明，可能还需要进行一些操作，这最终由最终验证者完成。这就是为什么这个黑盒函数不说验证是否通过。如果您在一个 ACIR 程序中要验证多个证明，您将多次调用 RecursiveAggregation() 并将 output_aggregation_object 作为 input_aggregation_object 传递给下一个 RecursiveAggregation() 调用，除了第一次调用，此时没有 input_aggregation_object。如果您使用黑盒函数验证的某个证明没有验证，那么主 ACIR 程序的证明验证最终将失败。

Brillig

此操作码在执行（求解）电路时用作求解器的提示。操作码不生成任何约束，通常是未约束 noir 函数编译的结果。

• 输入：操作码的输入，作为 '算术表达式'。
• 输出：操作码输出，作为证据
• 字节码：表示在此操作码内执行的计算的汇编代码。Noir 汇编规范不包含在此文档中。
• 谓词：一个算术表达式，当它为空时禁用操作码。

让我们用一个欧几里得除法的例子来说明。计算 a/b 的正常方法，其中 a 和 b 是 8 位整数，是实现欧几里得算法，该算法循环（或递归）计算 'a mod b' 的余数。这个计算需要大量步骤在 ACIR 中正确实现，尤其是带条件的循环。然而，欧几里得除法可以用一个 assert-zero 操作码轻松约束：a = bq+r，假设 q 是 8 位，r < b。由于这些假设可以用几个范围操作码轻松写出，因此欧几里得除法实际上可以用少量操作码实现。

然而，为了编写这些操作码，我们需要除法的结果，即见证 q 和 r。但从约束 a=bq+r 来看，求解器如何仅用一条方程式求解 q 和 r 呢？这正是 brillig/unconstrained 函数发挥作用的地方。我们简单地定义一个函数，该函数执行常规的欧几里得算法，从 a 和 b 计算出 q 和 r。由于 Brillig 操作码不生成约束，因此它不会提供给证明系统，而是由求解器直接使用来计算 q 和 r 的值。

总之，求解 Brillig 操作码执行其字节码定义的计算，在提供的输入上操作，并将结果赋值给输出见证，而不添加任何约束。

指令

此操作码是 Brillig 操作码的特化。与 Brillig 中的通用汇编代码不同，指令有一个硬编码的名称，告诉求解器执行哪种计算：在 Brillig 中，计算是指未约束 Noir 函数的编译字节码，而在指令中，计算是硬编码在编译器中的。指令将来将被 Brillig 操作码所取代。

MemoryOp：ACIR 的内存抽象

ACIR 能够访问任何见证数组。每个数组都分配一个 ID（BlockId），并且需要通过 MemoryInit 操作码进行初始化。然后可以通过提供索引和读/写的值（算术表达式）来从/向数组读取和写入。注意，ACIR 数组都具有已知固定长度（如下面的 MemoryInit 操作码中给出）

• block_id：数组标识符
• op：描述要执行的内存操作
  • operation：值为 1 的常量表达式表示向内存写入，值为 0 表示读取
  • index：数组索引，它必须小于数组长度
  • value：当 operation 为 0 时，我们要读取的值；当 operation 为 1 时，我们要在指定索引处写入的值
• 谓词：一个算术表达式，当它为空时禁用操作码。

MemoryInit

从见证向量初始化 ACIR 数组。

• block_id：数组标识符
• init：指定数组初始值的见证向量

每个 block_id 只能有一个 MemoryInit，且 MemoryOp 操作码必须在 MemoryInit 之后。