深入了解Starknet编程语言Cairo 1.0：设计原理、存在问题及改进之处

Starknet Astro ｜2023-03-27 14:24

Cairo 是一个图灵完备的 ZK 友好高级语言，也是以太坊 L2-Starknet 的合约开发语言，它正在进行改版升级。

作者：Maxlion，Starknet Astro

译者导读

Cairo 是一个图灵完备的 ZK 友好高级语言，也是以太坊 L2-Starknet 的合约开发语言，它正在进行改版升级。本篇文章是分析 Cairo 1.0 系列文章的第一篇，作者 Mathieu 分析了 Sierra 作为 Cairo 高级语言到 Cairo 汇编的中间层的设计动机与实现原理。文中提到了大量 Cairo 0 存在问题、Cairo 1 改进之处，并附有丰富的代码细节，推荐 Cairo 开发者阅读全文以深入了解 Cairo 1.0。

原文链接

TL;DR

Sierra 在高级 Cairo 编程语言与更原始的编译目标（如 CASM）之间担任了重要的中间人角色，确保生成的 CASM 可在 Starknet 上安全运行。它的设计以安全为中心，使用一组函数来生成安全的 CASM 代码，结合强大的编译器和线性类型系统来防止运行时错误，以及内置 Gas 系统来防止无限循环。在接下来的部分，我们将专注于理解 Sierra 程序的结构，提供了阅读和理解 Sierra 程序所需的基本要求。

简介

我（Mathieu）最近参加了 Starkware Sessions 的两场会议，分别是 Shahar Papini 的“Enforcing Safety Using Typesystems”和 Ori Ziv 的“Not Stopping at the Halting Problem”。如果你想了解更多有关 Cairo 堆栈的信息，我强烈建议你观看这些视频。以下文章是一个系列的第一篇，我将深入了解 Sierra 以更好地理解 Cairo、其机制以及整个 Starknet。

Sierra（Safe Intermediate Representation 安全中间表示）是高级语言 Cairo 和诸如 Cairo Assembly（CASM）之类的编译目标之间的中间层。该语言旨在确保安全并防止运行时错误。它使用编译器检测可能在编译时失败的操作，以确保每个函数都返回并且没有无限循环。Sierra 使用简单但强大的类型系统来表达中间层代码，同时确保安全性。这使得可以有效地编译成 CASM。

动机

在 Cairo 0 中，开发人员会使用 Cairo 编写 Starknet 合约，将其编译为 CASM，并直接部署编译输出到 Starknet 上。用户可以通过调用智能合约函数、签署交易并将其发送给排序器来与 Starknet 合约交互。排序器将运行交易以获取用户的交易费用，证明者（SHARP）将为包括此交易的批次生成 ZK 证明，排序器将收取包括交易在内的交易费用。

深入了解Starknet编程语言Cairo 1.0：设计原理、存在问题及改进之处

然而，该 Cairo 0 流程会产生一些问题：

在 Cairo 中只有有效的语句才能被证明，所以无法证明失败的交易。无法证明无效的语句，例如 assert 0 = 1，因为它转换为无法满足的多项式约束。
交易执行可能会失败，导致交易未被包括在块中。在这种情况下，排序器会做无偿的工作。由于失败的交易没有有效的证明，它们不能被包括在内，也没有办法强制排序器收费。
排序器可能被 DDoS 攻击，攻击者使用无效交易使其白干一场，而排序器无法收取运行这些交易的任何费用。
无法区分审查制度 censorship（当排序器故意决定不包括某些交易）和无效交易，因为这两种类型的交易都不会被包括在块中。

在以太坊上，所有失败的交易都被标记为 reverted，但仍包括在块中，允许验证者在失败时收取交易费用。为了防止恶意用户用无效交易轰击网络并使排序器不堪重负，从而使合法交易无法处理，Starknet 需要一个类似的系统，允许排序器收取失败交易的费用。为了解决上述问题，Starknet 网络需要实现两个目标：完整性和有效性。完整性确保交易执行始终可以被证明，即使它预计会失败。有效性确保不会拒绝有效交易，从而防止审查制度。

Sierra 是构造正确的（Correct-by-constrction），让排序器为所有交易收费。我们可以部署分支代码（例如 if/else），而不是可能失败的代码（例如 asserts）。Cairo 1 的 asserts 被翻译成分支 Sierra 代码，允许错误传播回返回布尔值的原始入口点，表示交易成功或失败。如果入口点返回值为 true/false，则 Starknet 操作系统可以确定交易是否有效，并决定是否应用状态更新，如果交易成功。

Cairo 1 提供类似于 Rust 的语法，并通过抽象 Sierra 的安全构造来创建可证明的、开发人员友好的编程语言。它编译为 Sierra，这是 Cairo 代码的构造正确的中间表示，不包含任何失败语义。这确保了没有 Sierra 代码会失败，并且它最终编译为 CASM 的安全子集。开发人员可以专注于编写高效的智能合约，而不必担心编写非失败的代码，所有这些都具有改进的安全原语。

开发人员将会将他们的 Cairo 1 代码编译为 Sierra，并将 Sierra 程序部署到 Starknet 上，而不是将 CASM 代码部署到 Starknet 上。在声明交易时，排序器将负责将 Sierra 代码编译为 CASM，以确保不能在 Starknet 上部署失败的代码。

构造正确

为了设计一个不会失败的语言，我们必须首先确定 Cairo 0 中的不安全操作。包括：

非法的内存地址引用；尝试访问未分配的内存单元
断言（assertions），因为它们可能会失败而无法恢复
由于 Cairo 的一次性写入内存模型，导致对同一内存地址的多次写入
无限循环，这使得无法确定程序是否会退出

确保解引用不会失败

在 Cairo 0 中，开发人员可以编写以下代码，试图访问未分配的内存单元的内容。

let (ptr:felt*) = alloc();

tempvar x = [ptr];

Sierra 的类型系统通过强制执行严格的所有权规则并利用 Box 等智能指针来防止常见的指针相关错误，从而使得在编译时能够检测和防止无效指针解引用。Box 类型用作指向有效和已初始化指针实例的指针，并提供两个函数进行实例化和解引用：box_new() 和 box_deref()。通过使用类型系统在编译时捕获解引用错误，从而使得从 Sierra 编译的 CASM 避免了无效指针解引用。

确保不会重复写入任何内存单元

在 Cairo 0 中，用户将使用如下数组：

let (array:felt*) = alloc();

assert array[0] = 1;

assert array[1] = 2;

assert array[1] = 3; // fails

然而，尝试两次写入同一数组索引会导致运行时错误，因为内存单元只能被写入一次。为避免这个问题，Sierra 引入了一个 Array 类型以及一个 array_append(Array, value:T) -> Array 函数。该函数接受一个数组实例和一个要附加的值，并返回指向新的下一个空闲内存单元的更新的数组实例。因此，值会按顺序附加到数组的末尾，而不必担心由于已经写入的内存单元可能导致的冲突问题。

为确保已经附加的先前使用的数组实例不会被重复使用，Sierra 使用线性类型系统确保对象仅使用一次。因此，任何已经被附加的 Array 实例不能在另一个 array_append 调用中重复使用。

下面的代码显示了一个 Sierra 程序的片段，该程序创建了一个 felt 数组，并使用 array_append 库函数两次追加值 1。在代码中，第一个 array_append 调用使用 id [0] 的数组变量作为输入，并返回一个表示更新的数组的 id [2] 变量。然后将此变量用作下一个 array_append 调用的输入参数。重要的是要注意，一旦被库函数使用，id [0] 的变量就不能被重复使用，尝试使用 id [0] 作为输入参数调用 array_append 将导致编译错误。

array_new() -> ([0]);

felt_const<1>() -> ([1]);

store_temp([1]) -> ([1]);

array_append([0], [1]) -> ([2]);

felt_const<1>() -> ([4]);

store_temp([4]) -> ([4]);

array_append([2], [4]) -> ([5]);

对于可以多次重新使用的对象，比如 felts，Sierra 提供了 dup(T) -> (T,T) 函数，返回两个相同对象的实例，可以用于不同的操作。这个函数仅适用于安全可复制的类型，通常是不包含数组或字典的类型。

非故障断言

通常使用断言来评估代码中特定点布尔表达式的结果。如果评估结果不符，就会引发错误。与 Cairo 0 中不同，Cairo 1 断言指令的编译将生成分支 Sierra 代码。如果不满足断言，则该代码将提前终止当前函数执行，并继续执行下一条指令。

确保使用字典的程序的健全性

字典和数组一样存在多次添加值的问题，可以通过引入特殊的 Dict 类型和一组工具函数来实例化、检索和设置字典中的值来解决这个问题。然而，字典存在一个健全性问题。每个 Dict 都必须在程序结束时调用 dict_squash(Dict) -> () 函数来压缩，以验证键更新序列的一致性。未压缩的字典是危险的，因为恶意证明者可以证明不一致更新的正确性。

正如我们之前所见，线性类型系统强制对象只能使用一次。唯一使用“使用”Dict 的方法是调用 dict_squash 函数，该函数使用字典实例并不返回任何内容。这意味着在将 Sierra 代码编译为 CASM 时将检测到未压缩的字典，并在编译时引发错误。对于其他不需要一次性使用的类型，通常是不包含 Dict 的类型， Sierra 引入 drop(T)->() 函数，该函数使用对象的实例并不返回任何内容。

值得注意的是，drop 和 dup 都不会产生任何 CASM 代码。它们仅在 Sierra 层提供类型安全，确保变量仅使用一次。

防止死循环

确定程序最终会停止或永远运行是计算机科学中的一个基本问题，被称为停机问题，在一般情况下是无法解决的。在像 Starknet 这样的分布式环境中，用户可以部署和运行任意代码，因此防止用户运行无限循环代码是很重要的，例如以下 Cairo 代码。

fn foo() { foo() }

由于递归函数如果停止条件永远不满足就可能导致无限循环，因此 Cairo-to-Sierra 编译器将在递归函数开头注入withdraw_gas方法。由于该功能尚未实现，因此开发人员仍需要在递归函数中调用withdraw_gas并自行处理结果，尽管在未来版本中应该会包含在编译器中。

该withdraw_gas 函数将通过计算函数中每条指令的运行成本来从交易总可用 Gas 中扣除运行函数所需的 Gas 数量。成本是通过确定每个操作需要多少步来分析的，大多数操作的步在编译时是已知的。在 Cairo 程序执行期间，如果withdraw_gas 调用返回 null 或负值，则当前函数执行会停止，所有待处理的变量都将通过对未压缩字典调用dict_squash 和对其他变量调用drop 来消耗，并将被认为是执行失败。由于 Starknet 上的所有交易都有一个有限的可用 Gas 量来执行交易，因此避免了无限循环，并通过确保仍有足够的 Gas 可用来删除变量并停止执行，排序器将能够从事务失败中收取费用。

通过一组有限的指令实现安全的 CASM

Sierra 的主要目标是确保生成的 CASM 代码不会失败。为实现这一目标，Sierra 程序由调用 libfuncs 的语句组成。这些是一组内置库函数，为这些函数生成的 CASM 代码是保证安全的。例如，array_append 库函数生成的安全 CASM 代码可用于将值附加到数组中。

通过仅允许一组安全和可信赖的库函数来实现代码安全的这种方法类似于 Rust 编程语言的哲学。通过提供一组安全和可信赖的抽象，这两种语言都有助于避免常见的编程错误，并增加代码的安全性和可靠性。Cairo 1 使用了与 Rust 类似的所有权和借用系统，为开发人员提供了一种在编译时推理代码安全性的方式，这有助于防止错误并提高整体代码质量。

免责声明

本文旨在为读者提供通用信息和理解，不表示 Nethermind 支持任何特定资产、项目或团队，也不保证其安全性。Nethermind 没有明示或暗示地向本文中包含的信息或观点的准确性或完整性作出任何陈述或保证。任何第三方不得以任何方式依赖本文，包括但不限于金融、投资、税收、监管、法律或其他建议，或将本文解释为任何形式的建议。请注意，虽然 Nethermind 为 Starkware 提供服务，但本文不是这些服务的一部分。

关于我们

Nethermind 是一个由世界级建设者和研究者组成的团队。我们为全球企业和开发人员提供访问和构建去中心化 Web 的能力。我们的工作触及 Web3 生态系统的每个部分，从 Nethermind 节点到基础密码学研究和 Starknet 生态系统的基础设施。发现我们的 Starknet 工具套件：Solidity 转 Cairo 编译器 Warp、StarkNet 区块浏览器 Voyager、针对 StarkNet 智能合约的开源形式验证工具 Horus、StarkNet 客户端实现 Juno，以及 Cairo 智能合约安全审计服务。如果您有兴趣解决一些区块链中最困难的问题，请访问我们的求职信息！