（现货合约量化机器人）Cairo 1.0 的内部机制：探索 Sierra

博森科技官网：www.bosenkejigz.com‍
量化机器人官网：www.qulianghua.com

译员前言Cairo 是一个图灵完备的 ZK 友善程序设计语言，都是以太币 L2-Starknet 的合同编程语言，它正在开展重做更新。本文是剖析 Cairo 1.0 系列文章的第一篇，创作者 Mathieu 阐述了 Sierra 做为 Cairo 程序设计语言到 Cairo 选编的内层设计动因与保持基本原理。原文中提及了很多 Cairo 0 存在的问题、Cairo 1 改善的地方，并附带丰富多样的代码小细节，强烈推荐 Cairo 开发人员阅读全文以全面了解 Cairo 1.0。

TL;DRSierra 在高端 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 证实，排序器将扣除包含交易等在内的交易花费。

Cairo 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种类作为偏向合理及已复位表针案例的表针，同时提供2个函数公式开展创建对象调解引入：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

但是，试着2次载入同一数组索引也会导致运行时错误，由于内存单元很容易被载入一次。为防止这种情况，Sierra 引进了一个 Array种类以及一个 array_append(Array,value:T)->Array函数公式。该函数公式接纳一个二维数组案例和一个要附带的值，并回到偏向一个新的下一个空余内存单元更新的二维数组案例。因而，会按序额外到二维数组的结尾，而不用担心因为早已载入的内存单元可能造成的冲突难题。

为保证早已附带的此前所使用的二维数组案例不被多次重复使用，Sierra 应用线形类型系统保证目标仅使用一次。因而，一切早已被附带的 Array 案例不可以在另一个 array_append 调用中多次重复使用。

下边的代码显示出了一个 Sierra 程序流程的桥段，该程序流程创建了一个 felt 二维数组，并用 array_append 库函数2次增加值 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)函数，回到2个同样对象案例，可用作不一样的操作。这一函数只适用于安全性可复制的种类，一般是不包括二维数组或字典的种类。

非常见故障肯定通常采用肯定来评价代码中特殊点布尔表达式得到的结果。假如评价结果不符合，就会引起不正确。与 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 主要用来删掉变量并停止执行，排列器将可以从事务管理逆境中收费。

根据一组有限的资源命令完成安全CASMSierra 的首要任务是保证产生的 CASM 代码不容易不成功。为推进这一目标，Sierra 程序流程由调用 libfuncs 的句子构成。这些都是一组内嵌库函数，给这些函数产生的 CASM 代码是确保安全的。比如，array_append 库函数产生的安全性 CASM 代码适合于将值额外到二维数组中。

根据仅容许一组安全与值得信赖的库函数来达到代码安全此方法类似 Rust 计算机语言的哲学。通过提供一组安全与值得信赖的抽象化，这两种语言都有助于防止比较常见的程序编写不正确，并提高代码的安全性稳定性。Cairo 1 采用了与 Rust 相近的使用权和使用系统软件，为开发者提供了一种在编译时逻辑推理代码产品安全性方法，这有利于避免不正确并提升整体代码品质。

免责协议文中致力于为阅读者给予通用性信息内容与理解，不表明 Nethermind 适用一切特殊财产、项目和精英团队，都不确保其安全性。Nethermind 并没有明确或暗示着地为本文中涉及到的信息或见解准确性或一致性做出一切阐述或确保。一切第三方不得以任何方法依靠文中，包含但是不限于金融业、项目投资、税款、管控、法律法规或其它提议，也将文中理解为任何方式的提议。一定要注意，尽管 Nethermind 为 Starkware 提供帮助，但文中并不是这些服务的一部分。