ROL:Cairo 1.0 的内部机制：探索 Sierra_ALP

译者导读

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

TL;DR

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

简介

我最近参加了StarkwareSessions的两场会议，分别是ShaharPapini的“EnforcingSafetyUsingTypesystems”和OriZiv的“NotStoppingattheHaltingProblem”。如果你想了解更多有关Cairo堆栈的信息，我强烈建议你观看这些视频。以下文章是一个系列的第一篇，我将深入了解Sierra以更好地理解Cairo、其机制以及整个Starknet。

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

动机

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

Cairo0交易流程

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

在Cairo中只有有效的语句才能被证明，所以无法证明失败的交易。无法证明无效的语句，例如?assert0=1，因为它转换为无法满足的多项式约束。交易执行可能会失败，导致交易未被包括在块中。在这种情况下，排序器会做无偿的工作。由于失败的交易没有有效的证明，它们不能被包括在内，也没有办法强制排序器收费。排序器可能被DDoS攻击，攻击者使用无效交易使其白干一场，而排序器无法收取运行这些交易的任何费用。无法区分审查制度censorship和无效交易，因为这两种类型的交易都不会被包括在块中。在以太坊上，所有失败的交易都被标记为?reverted，但仍包括在块中，允许验证者在失败时收取交易费用。为了防止恶意用户用无效交易轰击网络并使排序器不堪重负，从而使合法交易无法处理，Starknet需要一个类似的系统，允许排序器收取失败交易的费用。为了解决上述问题，Starknet网络需要实现两个目标：完整性和有效性。完整性确保交易执行始终可以被证明，即使它预计会失败。有效性确保不会拒绝有效交易，从而防止审查制度。

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

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

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

构造正确

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

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

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

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

tempvarx=;

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

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

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

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

assertarray=1;

assertarray=2;

assertarray=3;//fails

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

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

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

array_new<felt>()->();

felt_const<1>()->();

store_temp<felt>()->();

array_append<felt>(,)->();

felt_const<1>()->();

store_temp<felt>()->();

array_append<felt>(,)->();

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

非故障断言

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

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

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

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

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

防止死循环

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

fnfoo(){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编程语言的哲学。通过提供一组安全和可信赖的抽象，这两种语言都有助于避免常见的编程错误，并增加代码的安全性和可靠性。Cairo1使用了与Rust类似的所有权和借用系统，为开发人员提供了一种在编译时推理代码安全性的方式，这有助于防止错误并提高整体代码质量。

免责声明

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

标签：ROLALPHAPHAALPROLC$ALPHA币PHAE币Save Ralph

ICP热门资讯