Cairo 1.0 的內部機制：探索 Sierra

译者導讀#

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 證明，排序器將收取包括交易在內的交易費用。

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<T> 類型用作指向有效和已初始化指針實例的指針，並提供兩個函數進行實例化和解引用：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<T> 類型以及一個 array_append<T>(Array<T>, value:T) -> Array<T> 函數。該函數接受一個數組實例和一個要附加的值，並返回指向新的下一個空閒內存單元的更新的數組實例。因此，值會按順序附加到數組的末尾，而不必擔心由於已經寫入的內存單元可能導致的衝突問題。

為確保已經附加的先前使用的數組實例不會被重複使用，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<felt>() -> ([0]);

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

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

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

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

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

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

對於可以多次重新使用的對象，比如 felts，Sierra 提供了 dup<T>(T) -> (T,T) 函數，返回兩個相同對象的實例，可以用於不同的操作。這個函數僅適用於安全可複製的類型，通常是不包含數組或字典的類型。

非故障斷言#

通常使用斷言來評估代碼中特定點布爾表達式的結果。如果評估結果不符，就會引發錯誤。與 Cairo 0 中不同，Cairo 1 斷言指令的編譯將生成分支 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 代碼。

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 智能合約安全審計服務。如果您有興趣解決一些區塊鏈中最困難的問題，請訪問我們的求職信息！