Cairo 1.0 の内部メカニズム：Sierra を探る

翻訳者の導入#

Cairo は、チューリング完全な ZK フレンドリーな高級言語であり、Ethereum の L2-Starknet の契約開発言語でもあり、現在改版アップグレードが進行中です。本記事は Cairo 1.0 シリーズ記事の第一篇であり、著者Mathieuが、Cairo 高級言語から Cairo アセンブリへの中間層としての Sierra の設計動機と実装原理を分析しています。文中では、Cairo 0 に存在する多くの問題、Cairo 1 の改善点が言及されており、豊富なコードの詳細が添付されています。Cairo 開発者には、Cairo 1.0 を深く理解するために、全文を読むことをお勧めします。

原文リンク

TL;DR#

Sierra は、高級 Cairo プログラミング言語と、より原始的なコンパイルターゲット（例えば CASM）との間で重要な中間者の役割を果たし、生成された CASM が Starknet 上で安全に実行できることを保証します。その設計は安全性を中心にしており、安全な CASM コードを生成するために一連の関数を使用し、強力なコンパイラと線形型システムを組み合わせて実行時エラーを防ぎ、無限ループを防ぐために内蔵の Gas システムを使用しています。次の部分では、Sierra プログラムの構造を理解することに焦点を当て、Sierra プログラムを読むために必要な基本要件を提供します。

はじめに#

私（Mathieu）は最近、Starkware Sessions の 2 つの会議に参加しました。Shahar Papini の「Enforcing Safety Using Typesystems」と Ori Ziv の「Not Stopping at the Halting Problem」です。Cairo スタックに関する詳細を知りたい場合は、これらのビデオを視聴することを強くお勧めします。以下の記事はシリーズの第一篇であり、Cairo、メカニズム、そして Starknet 全体をよりよく理解するために Sierra を深く掘り下げます。

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 攻撃を受ける可能性があり、攻撃者は無効なトランザクションを使用して無駄な作業をさせ、オーダラーはこれらのトランザクションを実行するための料金を請求できません。
検閲制度（オーダラーが意図的に特定のトランザクションを含めないことを決定する場合）と無効なトランザクションを区別することができません。なぜなら、これらの 2 種類のトランザクションはどちらもブロックに含まれないからです。

Ethereum では、すべての失敗したトランザクションはrevertedとしてマークされますが、それでもブロックに含まれ、検証者は失敗時にトランザクション手数料を請求できます。悪意のあるユーザーが無効なトランザクションでネットワークを攻撃し、オーダラーを圧倒し、合法的なトランザクションが処理できなくなるのを防ぐために、Starknet はオーダラーが失敗したトランザクションの料金を請求できるようにする類似のシステムが必要です。上記の問題を解決するために、Starknet ネットワークは 2 つの目標を達成する必要があります：完全性と有効性。完全性は、トランザクションの実行が常に証明可能であることを保証し、たとえそれが失敗することが予想される場合でもです。有効性は、有効なトランザクションが拒否されないことを保証し、検閲制度を防ぎます。

Sierra は、正しく構築された（Correct-by-construction）ものであり、オーダラーがすべてのトランザクションに対して料金を請求できるようにします。私たちは、失敗する可能性のあるコード（例えば asserts）ではなく、分岐コード（例えば if/else）をデプロイできます。Cairo 1 の asserts は、分岐 Sierra コードに翻訳され、エラーが元のエントリポイントに戻ることを許可し、トランザクションが成功したか失敗したかを示すブール値を返します。エントリポイントが true/false を返す場合、Starknet オペレーティングシステムはトランザクションが有効かどうかを判断し、状態更新を適用するかどうかを決定できます。

Cairo 1 は Rust に似た構文を提供し、Sierra の安全な構造を抽象化することで、証明可能で開発者に優しいプログラミング言語を作成します。これは、Cairo コードの正しく構築された中間表現である Sierra にコンパイルされ、失敗の意味を含まないことを保証します。これにより、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>型は、有効で初期化されたポインタインスタンスを指すポインタとして使用され、インスタンス化と解参照のための 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

しかし、同じ配列インデックスに二度書き込もうとすると、メモリ単位は一度しか書き込むことができないため、実行時エラーが発生します。この問題を回避するために、Sierra はArray<T>型とarray_append<T>(Array<T>, value:T) -> Array<T>関数を導入しました。この関数は、配列インスタンスと追加する値を受け取り、次の空いているメモリ単位を指す更新された配列インスタンスを返します。したがって、値は順番に配列の末尾に追加され、すでに書き込まれたメモリ単位による競合の問題を心配する必要はありません。

すでに追加された以前に使用された配列インスタンスが再利用されないことを保証するために、Sierra は線形型システムを使用して、オブジェクトが一度だけ使用されることを保証します。したがって、すでに追加された Array インスタンスは、別のarray_append呼び出しで再利用することはできません。

以下のコードは、felt 配列を作成し、array_appendライブラリ関数を使用して値1を 2 回追加する Sierra プログラムの断片を示しています。コード内では、最初の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)関数を提供し、異なる操作に使用できる同じオブジェクトの 2 つのインスタンスを返します。この関数は、安全にコピー可能な型にのみ適用され、通常は配列や辞書を含まない型です。

非故障アサーション#

通常、アサーションはコードの特定のポイントでブール式の結果を評価するために使用されます。評価結果が一致しない場合、エラーが発生します。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 プログラミング言語の哲学に似ています。安全で信頼できる抽象のセットを提供することで、これらの 2 つの言語は一般的なプログラミングエラーを回避し、コードの安全性と信頼性を高めるのに役立ちます。Cairo 1 は、Rust に似た所有権と借用システムを使用しており、開発者にコンパイル時にコードの安全性を推論する方法を提供し、エラーを防ぎ、全体的なコード品質を向上させるのに役立ちます。

免責事項#

この記事は、読者に一般的な情報と理解を提供することを目的としており、Nethermind が特定の資産、プロジェクト、またはチームを支持することを示すものではなく、その安全性を保証するものでもありません。Nethermind は、この記事に含まれる情報や意見の正確性または完全性について、明示的または暗示的にいかなる表明または保証も行いません。第三者は、この記事に依存することはできず、金融、投資、税金、規制、法律、またはその他のアドバイスを含むがこれに限定されない方法で、またはこの記事を何らかの形でアドバイスとして解釈することはできません。なお、Nethermind は Starkware にサービスを提供していますが、この記事はこれらのサービスの一部ではありません。

私たちについて#

Nethermind は、世界クラスのビルダーと研究者からなるチームです。私たちは、世界中の企業や開発者に分散型 Web へのアクセスと構築の能力を提供しています。私たちの仕事は、Nethermind ノードから基礎的な暗号学研究、Starknet エコシステムのインフラストラクチャに至るまで、Web3 エコシステムのすべての部分に触れています。私たちの Starknet ツールキットを発見してください：Solidity から Cairo へのコンパイラ Warp、StarkNet ブロックエクスプローラー Voyager、StarkNet スマートコントラクト向けのオープンソース形式検証ツール Horus、StarkNet クライアント実装 Juno、およびCairo スマートコントラクトのセキュリティ監査サービス。もし、ブロックチェーンの最も困難な問題のいくつかを解決することに興味があるなら、私たちの求人情報をご覧ください！