摘要
证明系统允许一方向另一方证明某一陈述是真实的。大多数现有的实际证明系统要求该陈述用有限域上的多项式方程来表示。这使得表示一个人希望证明或验证的陈述的过程相当复杂，因为这个过程需要为每个陈述提供一组新的方程。
已经提出了处理这个问题的各种方法，例如参见[1]。
我们推出 Cairo，一种实用高效、图灵完备、STARK 友好的 CPU 架构。我们描述了一组多项式方程来声明程序在此架构上的执行是有效的。给定一个想要证明的陈述，开罗允许编写一个描述该陈述的程序，而不是编写一组多项式方程。
1，介绍
1.1， 背景
Babai、Fortnow 和 Lund [8] 的开创性工作首次展示了交互式证明系统在可扩展性方面的应用。非正式地说，此类系统允许两方（称为证明者和验证者）参与协议，其中证明者使验证者相信某个陈述是正确的。该陈述的一般形式是：“我知道某个计算的输入会产生某个输出”，其中计算和输出对于证明者和验证者来说都是已知的。最简单的方法是证明者将输入发送给验证者并让验证者重复计算。这种方法有两个潜在的不良特征：
- （1）验证者学习输入（缺乏隐私），
- （2）验证者需要重新执行计算（效率低下）。
用于计算完整性的密码证明系统是可以通过以下方式解决这些问题的协议： - （1）引入零知识[17]以保护隐私；
- （2）启用简洁验证，这比重新执行效率高得多。
本文通过引入 Cairo 来解决表示经过验证的计算的挑战，Cairo 是一种允许以计算机程序的形式描述计算，然后生成该计算的完整性证明的架构。 Cairo 架构的设计目的是：（1）易于编写和阅读用作可证明语句的程序，以及（2）高效证明，例如基于 STARK [10] 证明系统。
在大多数现有的实用证明系统中，必须用有限域上的多项式方程来表示所证明的计算。这个过程称为“算术化”，首次在[19]中的交互式证明中使用。这种表示形式1的例子有算术电路、二次跨度程序[15]（又名R1CS）和代数中间表示形式[10，第14页]。 14]（空气）。
这种用多项式方程组来表示计算的要求使得在实际应用中使用这些证明系统变得非常复杂。此外，一些进行算术处理的方法会导致不必要的计算（请参阅下面的分支和循环示例）。
考虑一些这样的算术过程的示例。从断言 x ̸= y 的简单任务开始。请注意，多项式方程通常必须采用 p = 0（而不是 p ̸= 0）的形式，其中 p 是变量中的某个多项式。断言 x ̸= y 可以转换为 ∃a: (x − y) · a = 1（通过添加辅助变量 a）。稍微复杂一点的模 264 加法任务可以通过添加 64 个捕获总和的二进制表示的辅助变量来转换为多项式方程。
当必须处理计算中的分支（例如，如果 x = y 则做一件事，否则做另一件事）和循环（例如，重复做某事直到 x = y）时，任务会变得更加复杂。处理分支的一种方法是将两个分支都转换为多项式方程，并添加一个根据条件值“选择”结果的方程（例如，方程 z = (1−b)·x +b·y 强制 z=xifb=0 且 z=yifb=1)。循环可以通过将迭代次数限制为某个常数 B 并精确执行循环体 B 次来解决，如果在某个时刻满足条件，则下一次迭代将简单地传递结果，直到循环结束。请注意，最后两种情况需要额外的“不必要”计算：在第一种情况下执行两个分支并执行 B 次迭代，即使在第二种情况下循环提前结束。
应对计算表示挑战的一种方法是编写一个编译器——一种以代码作为输入并输出表示代码执行情况的多项式方程列表的计算机程序。遵循这种方法的系统示例包括 ZKPDL [20]、Pinocchio [22]、TinyRAM for SNARKs [11] 和 STARKs [10] 以及 xJsnark [18]。这可能会使过程更简单，但结果仍然存在一些缺点，例如前面提到的执行不必要代码的低效率，以及限制循环中迭代次数的必要性。
另一种方法的动机来自 CPU 和冯·诺依曼架构的发明：人们可以设计一个单一的通用多项式方程组，代表为某些固定指令集编写的任意计算机程序的执行。在预处理 SNARK 的背景下，这种方法被用在 vnTinyRAM 系统中 [13]。
1.2 我们的贡献
我们提出了 Cairo，一种高效实用的冯诺依曼架构，可以与 STARK 证明系统一起使用来生成计算完整性的证明。因此，它是第一个 STARK 冯诺依曼架构。开罗的主要优势是：
- 高效 选择 Cairo 指令集是为了使相应的 AIR 尽可能高效。例如，[13]的构建每个周期需要大约 1000 个变量。将此与开罗 AIR 所需的 51 个变量进行比较（参见第 9 节）。此外，我们提出了内置函数的想法（第 2.8 节和第 7 节），它使得执行预定义操作的开销可以忽略不计（例如，应用加密哈希函数）。
- 实用 Cairo 支持条件分支、内存、函数调用和递归。
- 成熟可靠 Cairo 是在以太坊区块链上运行的多个加密货币系统的支柱。 Cairo 程序的证明经常生成并通过链上合约进行验证。欲了解更多信息，请参阅[2]。
本文提出的以下概念对于实现 Cairo 的性能至关重要：
- Algebraic RISC2 Cairo 使用小而简单但相对富有表现力的指令集；其中所有指令都可以使用 15 个标志和三个整数进行编码。参见第 2.3.2 节和第 4.5 节。
- 非确定性连续只读随机存取存储器 Cairo 没有使用传统的读写存储器模型，而是使用
独特的内存模型（第 2.6 节），它受到更多限制 - 例如，所有内存单元的值均由证明者选择，并且在执行代码时不会更改。附加限制允许非常高效的 AIR 实现，每次内存访问仅需要 5 个跟踪单元（第 9.7 节）。这一点尤其重要，因为每条指令使用 4 次内存访问（一次用于获取指令，另外 3 次用于 3 个操作数）。事实上，大多数通常使用读写存储器完成的编程任务也可以使用这种新的存储器模型来完成（参见第 6 节和第 8 节）。 - 排列范围检查 排列范围检查，在第 9.9 节中介绍，允许仅使用 3 个跟踪单元（与所需的 16 个跟踪单元相比）来检查（在 AIR 中）某个值是否在 [0, 216 ）范围内。通过使用二进制表示的简单方法）。每条指令使用 3 个这样的范围检查值，因此这种效率至关重要。
- 内置 Cairo 架构支持直接以一组方程的形式实现预定义操作，而不是使用 Cairo 代码来实现它们。我们将此类预定义操作称为内置操作（第 2.8 节和第 7 节）。使用内置函数的优点是它们可以显着减少由于从手写 AIR 到 Cairo 代码的转换而增加的开销。这使得程序员可以从编写代码中受益，同时不会遭受显着的性能开销。
- 高效的公共内存 Cairo的内存实现还有另一个重要的特点——每个应该与验证者共享的内存单元（例如，程序的代码和输出），只增加了4次算术运算的验证成本（不包括Fiat-沙米尔哈希）。参见第 2.6.1 节和第 9.8 节。
- 非确定性冯·诺依曼的优点 例如，(1) 证明验证者只知道哈希值（而不是代码）的程序，以及 (2) 在一个证明中证明多个不同的程序以减少摊销验证成本。参见第 2.2 节。
Cairo 这个名字来自术语“CPU AIR”——实现 CPU 概念的 AIR（第 9 节）
1.3 概述
第 2 节介绍了开罗的主要特征，并解释了在架构设计中做出的许多决定。
第 3 节给出了开罗机的正式定义，并解释了它如何融入证明系统。
第 4 节描述了 Cairo 机的状态转换函数。本节非常技术性，因为它解释了构成指令的 15 个标志中的每一个如何影响状态转换。在实践中，215 种可能的组合中很少被使用。它的对应部分，第 5 节，提供了一组有用的指令，可以使用特定的标志配置来实现。这些指令构成了 Cairo 汇编语言（尽管确切的语法超出了本文的范围）。
第 6 节建议如何安排只读存储器以允许处理函数调用（包括递归）。换句话说，如何在 Cairo 中实现函数调用堆栈。
第 7 节解释了内置函数的概念，它是针对选定函数的优化执行单元。
第 8 节高度概述了如何处理常见的编程任务（例如，整数除法和模拟读写内存），考虑到 Cairo 的独特功能（例如，其独特的内存模型以及基本的内存模型）算术运算是在有限域上计算的，而不是更常见的 64 位整数算术）。
由于 Cairo 的主要目的是生成计算完整性证明，因此必须能够使用证明系统来证明 Cairo 程序的执行已成功完成。证明系统的自然候选者是 STARK [10]，因为它能够有效地处理统一计算。
第 9 节解释了如何将 Cairo 机实现为代数中间表示 (AIR) [10，第 10 页]。 14]，这是 STARK 协议中描述计算的方式。它包括强制开罗机器行为的多项式约束的详细描述。
1.4 符号
在整篇论文中，F 是一个大小为 |F| 的固定有限域。对于两个整数，b∈Z，我们使用记号[a,b):={x∈Z:a≤x<b} 和 [a, b] := {x ∈ Z : a ≤ x ≤ b}。
1.5 致谢
我们感谢 Eli Ben-Sasson 在 Cairo 开发和撰写本文期间提供的有益评论和讨论，感谢 StarkWare 的工程师在设计过程中提供了有用的建议并帮助实现了系统，感谢 Jeremy Avigad 和 Yoav Seginer 对此提供了有益的评论纸。
2 设计原则
Cairo 框架使人们能够证明任意计算的完整性。也就是说，让验证者相信某个程序成功运行并具有某些给定的输出。
Cairo 旨在提供直观的编程框架，以便使用 STARK 协议有效证明程序执行的有效性 [10]。尽管 STARK 协议可以单独使用（即没有 Cairo）来证明任意计算的完整性，但 Cairo 围绕 STARK 提供了一个抽象层，简化了计算的描述方式。
为了直接使用 STARK 证明系统，计算必须被构建为 AIR（代数中间表示）[10，第 17 页]。 14]，参见2.1节，这需要相当复杂的设计过程。 Cairo 框架引入了一种可以描述计算的汇编语言（以及在此基础上的完整编程语言——这超出了本文的范围）。这比设计 AIR 容易得多。
请注意，虽然 Cairo 被设计为与 STARK 协议一起使用，但它也可以与许多其他基于有限域的证明系统一起使用，例如 SNARKs [11]。
本节介绍 Cairo 背后的原则，并解释其设计过程中做出的一些选择。
2.1 代数中间表示 (AIR) 和带预处理的随机 AIR (RAP)
许多基于有限域的证明系统 [16,11,12,14] 使用算术电路或二次跨度程序 [15]（又名 R1CS）。考虑一个算术电路 - 具有加法门和乘法门的电路，其中所有值都来自某个固定的有限域。证明者得到这样一个算术电路，加上输入（见证人），使其返回 0，其中 0 是“真实”或“成功”的代数表示。然后，它生成一个证明，证明该特定算术电路的某些输入存在，使其返回 0。
STARK 证明系统基于 AIR（代数中间表示，参见[10，第 14 页]），而不是算术电路或 R1CS。 AIR 可以被认为是在称为“踪迹”（见证）的字段元素（某些有限字段 F）的（二维）表上运行的多项式约束（方程）列表。 STARK 证明证明存在满足约束的迹。
通常，表中的列数较少（大约 20），行数为 2 的幂。每个约束都分配有一个域，该域是约束所应用的行的周期性集合。例如，约束可以应用于所有行、每第四行或单个行。
正如我们将在第 9.6 节中看到的，Cairo AIR 实际上并不是真正的 AIR（根据 [10，第 14 页] 中的正式定义），它是带有预处理的随机 AIR（RAP，请参阅 [3]） ）。 RAP 是 AIR 一词的更广泛定义，它允许证明者和验证者之间进行额外的交互步骤。这意味着：
- 约束可能涉及变量 c0 , . 。 。 , cm ∈ F 不属于迹线单元的一部分。我们将它们称为交互变量。
- 跟踪列分为两组：交互步骤之前和之后。
- 我们不需要一个令人满意的赋值，而是要求 (c0,...,cm) 的大多数 5 个值存在满足赋值，其中第一组列与值 (c0,...,cm) 无关。
可以修改 STARK 协议来证明描述为 RAP 的语句（参见第 9.6 节）。
由于这个概念在 RAP 一词被创造之前就已在开罗使用，因此我们在本文中将继续使用术语“开罗 AIR”，而不是“开罗 RAP”。
2.2 冯·诺依曼架构
Cairo 框架涉及从描述为计算机程序的计算转向描述为 AIR 的计算。处理此翻译的两种主要方法是：
ASIC 方法：将程序编译为 AIR。在这种方法中，人们编写一个计算机程序（编译器），它将用某种语言编写的程序作为输入，并输出表示等效计算的 AIR（一组约束）。这类似于编译器，它接受程序并根据输入代码输出 ASIC 或 FPGA。
CPU 方法：设计一个行为类似于 CPU 的 AIR（独立于正在验证的计算）。该 AIR 代表单个计算 - 从内存中获取指令的循环，
执行该指令，并继续执行下一条指令。这类似于使用单个通用 CPU 芯片而不是专用芯片。
ASIC 方法的主要优点是效率。基于计算构建 AIR 没有解码指令和使用内存的开销。然而，由于使用内置函数（参见第 2.8 节和第 7 节）减少了这种开销，这使得 CPU 方法能够在许多计算中提供与手写 AIR 相似的性能。如果某个计算无法利用现有的内置函数，则需要进行权衡：您可以在（1）接受性能损失和（2）设计一个新的内置函数以提高计算性能之间进行选择7。
CPU 方法有许多优点，包括：
- 小约束集：由于约束集独立于被证明的计算，因此它具有固定的大小。 Cairo CPU 的 AIR 由 30-40 个约束组成8。这提高了验证成本。
- 单个AIR：虽然ASIC 方法需要输出AIR 约束的计算机程序，但CPU 方法具有可以运行任何程序的一组约束。因此，此 AIR 的验证程序只需实现一次（而不是每个应用程序）。特别是，这简化了证明系统的审核过程。一旦检查了约束，在考虑新应用程序时，唯一需要审核的是它的代码（比多项式方程更容易审核）。 AIR 独立于应用程序的另一个优点是，它简化了构建递归 STARK 证明的过程（参见第 2.2.4 节）。
2.2 节的其余部分描述了遵循冯诺依曼架构的 CPU 方法的优点。在冯·诺依曼架构中，程序的字节码和数据位于同一内存中。称为“程序计数器”(PC) 的寄存器指向内存地址。 CPU (1) 获取该存储单元的值，(2) 执行该值表示的指令（这可能会影响存储单元或通过向 PC 分配不同的值来更改程序流程），(3) 将 PC 移至下一条指令，并且 (4) 重复此过程。
2.2.1 引导加载：从哈希加载程序
一个程序可以将另一个程序的字节码写入内存，然后将PC设置为指向该内存段，从而开始执行另一个程序。
这个想法的一个具体用途是“从哈希引导加载”：一个称为“引导加载程序”的程序计算并输出另一个程序的字节码的哈希，然后开始如上所述执行它。 这样，验证者只需要知道正在执行的程序的哈希值，而不是其完整的字节码。
这提高了隐私性和可扩展性：
- 隐私：验证者可以在不知道计算结果的情况下验证程序的执行9。
- 可扩展性：假设验证者已知程序哈希，则验证时间并不线性依赖于程序大小，如果将程序（而不是其哈希）作为验证者的输入，则会出现这种情况。
2.2.2 在同一个证明中运行多个不同的程序
上述引导加载程序可以扩展为依次执行多个程序，输出每个程序的字节码哈希以及程序的输出。请注意，这些程序可以描述完全不同的计算。由于证明的大小和验证它的成本在计算大小上都是次线性的，因此可以使用这样的引导加载程序来获取多个程序并生成证明所有程序有效性的单个证明。验证费用将由这些计划分摊。
让我们举一个数值示例：在 STARK 所基于的理论结构 STIK10 中，证明验证与迹线长度 O(logT) 呈对数关系，请参见 [10，第 10 页]。 21]。 STARK 构造（使用 Merkle 树承诺）添加了另一个 O(logT) 乘法因子，导致验证时间复杂度为 O(log2 T)。为了简单起见，我们假设长度为 T 的执行轨迹的完整性证明的验证恰好是 log2(T)。分别验证两个程序各 100 万步的证明将花费 2log2(T) ≈ 794，而验证两个程序的一个证明将花费 log2(2T) ≈ 438。可以看到，随着更多程序添加到批次中，一批许多程序中的一个程序的摊余验证成本接近于零。
2.2.3 高级优化（即时编译和字节码生成）
一些高级优化可以通过在程序执行期间自动生成字节码来实现。例如，程序可以克隆函数的字节码并将一些值直接放置在需要它们的指令中，而不是从函数的内存中获取值。考虑指令“从内存读取 c 和 x 并计算 x + c”。一旦知道 c 的值（让我们用 C 表示），我们可以用可能更有效的指令“从内存读取 x 并计算 x + C”来替换指令，其中 C 是指令的立即值。
所有其他形式的字节码生成也是可能的：程序可以根据某些规则生成 Cairo 字节码，然后执行它。例如，假设我们需要计算多个 xi 的 xci，我们可以编写一个函数，获取 c 并返回使用长乘法序列计算 xc 的函数的字节码（而不是使用递归和条件跳转的简单实现，因此效率低得多）。
2.2.4 增量可验证计算（递归证明）
递归证明是证明另一个证明有效性的证明。例如，令 A0 表示某个语句。证明系统最简单的用途是证明者让验证者相信 A0 是正确的。现在，让我们将 A1 定义为“我验证了证明 A0 为真这一事实的证据”这一陈述。人们可以尝试生成 A1 的证明。然后我们可以继续语句 A2、A3 等等。这个想法被称为“增量可验证计算”，首先在[23]中定义和分析。
为了生成递归证明，必须将验证过程（验证者正在运行的算法）编码为被证明的语句。对于许多证明系统，特别是 ASIC 方法，这会产生循环依赖：验证者依赖于被证明的程序，而被证明的程序又依赖于验证者的代码。然而，使用 CPU 方法，验证器不依赖于程序，这简化了递归证明——因为循环依赖被打破。此外，使用从散列引导加载的思想（第 2.2.1 节），整个验证程序可以编码为一个散列（例如 256 位），这允许将程序作为参数传递给自身（这是一个生成递归证明的步骤）。
2.3 指令集
指令集是 Cairo CPU 可以在单个步骤中执行的操作集。本节介绍 Cairo 指令集的高级属性。
2.3.1 指标
为了为 Cairo 设计一个好的指令集，首先需要了解应该优化哪些指标。与在晶体管构建的物理芯片上执行的普通指令集不同，Cairo 在 AIR 中执行（参见第 2.1 节）12。普通指令集应尽量减少指令执行的延迟和所需晶体管的数量；同时最大化计算的吞吐量。高效 AIR 的指标是不同的：粗略地说，设计 AIR 时（以及因此设计将由 AIR 执行的指令集时）最重要的约束是最小化所使用的跟踪单元的数量13。这或多或少相当于多项式方程组中变量的数量。
为了设计一套有效的指令集，我们必须了解应该优化哪些属性。合理的衡量标准是平均程序（在所述指令集中最佳编写）使用的跟踪单元数量的预期。这是一种非正式的衡量标准，因为为了准确，它需要了解程序的分布，并要求每个程序都在所有比较的指令集中以最有效的方式编写。尽管如此，人们仍然可以使用这一定义作为整个设计中许多决策的指南。
以两个指令集 A 和 B 为例。指令集 A 有一条指令“as_bool”，用于计算表达式“如果 x ̸= 0，则为 1，否则为 0”。指令集 B 是相同的指令集，只是缺少“as_bool”。假设在 CPU 中基于指令集 A 执行单个步骤的成本（以跟踪单元为单位）为 a（为简单起见，我们假设所有指令消耗相同数量的跟踪单元），并且使用时单个步骤的成本为指令集 B 是 b（其中 a > b，因为添加附加指令的复杂性）。另一方面，如果使用指令集 A 编写某个程序，则可能需要 kA 步；如果使用指令集 B 编写，则可能需要 kB 步（此处 kB ≥ kA，因为每次程序需要使用“as_bool”时，可能需要多个来自指令集B)的指令。如果a·kA < b·kB，则指令集A更适合该程序，如果a·kA > b·kB，则指令集B更适合该程序。当决定是否包含指令时，应考虑每步的额外成本 (a/b) 与额外步骤 (kB/kA)，并且为了设计高效的指令集，必须了解应具有哪些属性进行优化。合理的衡量标准是平均程序（在所述指令集中最佳编写）使用的跟踪单元数量的预期。这是一种非正式的衡量标准，因为为了准确，它需要了解程序的分布，并要求每个程序都在所有比较的指令集中以最有效的方式编写。尽管如此，人们仍然可以使用这一定义作为整个设计中许多决策的指南。对“典型”程序执行此操作，并对“典型”程序的外观有所了解。