概要
递归証明のメインネットへのリリースにより、StarkEx アプリケーションと StarkNet の拡張が証明によって可能になりました。
递归証明は拡張性を向上させ、コストと遅延を低減します(拡張性と遅延の両方を犠牲にすることなく)。
递归証明は L3 およびその他の応用に条件を提供します。
递归証明についてのブログ記事を見てみましょう、とてもクールですね?
倍増の拡張!
Cairo によってサポートされる递归証明が本番環境に投入されました。これにより、STARK の L2 拡張能力が大幅に向上しました。イーサリアムへの書き込みの単一の証明によるトランザクションの数は急速に倍増することができます。
これまで、STARK の証明は数万から数十万のトランザクションを「集約」してイーサリアムに書き込むことで拡張を実現してきました。递归を使用することで、多くのこのような証明を 1 つの単一の証明に「集約」することができます。
この手法は、Cairo ベースの多くのアプリケーションに適用されています:StarkWare の SaaS 拡張エンジンである StarkEx および許可なしの Rollup で実行される StarkNet 上で動作するアプリケーション。
開発の経緯
2020 年 3 月のメインネットリリース以来、STARK の証明はさまざまな開発段階を経てきました。
STARK の拡張
2020 年 6 月、最初の STARK 拡張ソリューションである StarkEx がイーサリアムメインネットに展開されました。StarkEx には、オフチェーンで大規模な計算を実行し、トランザクションの正確性を示す STARK 証明を生成するプルーバがあり、チェーン上で証明の正確性を検証するバリデータもあります。最初の展開は、StarkWare のエンジニアがゼロから手作業で行ったため、StarkEx の機能は非常に制限されていました。最終的に、一般的な計算をサポートするプログラミング言語が必要であると判断し、Cairo が生まれました。
Cairo プログラミング言語
2020 年夏、Cairo がイーサリアムメインネットに初めて登場しました。Cairo は、CPU 代数の中間コード(CPU Algebraic Intermediate Representation [AIR])であり、対応する「CPU」命令セットを検証するための単一の AIR を含んでいます。Cairo は、より複雑なビジネスロジックや任意の計算命題をエンコードして証明するための大きな扉を開き、より高速で安全です。Cairo プログラムは、対応するアプリケーションの実行ロジックを証明することができます。ただし、Cairo プログラムは複数のアプリケーションを組み合わせることもできます。これが SHARP です。
SHARP
SHARP は、複数の独立したアプリケーションのトランザクションを集約し、単一の STARK 証明で証明する共有プロバーです。アプリケーションは異なるバッチのトランザクションを組み合わせることができ、STARK 証明の容量をより速く埋めることができます。トランザクションの処理速度と遅延が向上します。递归証明は次世代の先進技術であり、ハードコーディングされたロジックだけでなく、一般的な計算にも適用されます。
递归証明のすべての利点を理解するには、SHARP がこれまでにどのように(非递归的に)証明を実行してきたかをさらに理解する必要があります。図 1 は典型的な非递归的なフローを示しています:
image
このフローでは、命題が段階的に到着します。容量(または時間)が一定の閾値に達すると、大規模な組み合わせ命題(Train)が生成されます。この組み合わせ命題を証明するには、すべての個別の命題が到着する必要があります。この証明には時間がかかります(個別の命題の証明に必要な時間の合計ほど)。
非常に大きな命題の証明は、メモリなどの利用可能な計算リソースに制約を受けます。递归の前では、これは実際には STARK 証明のスケーラビリティを制限する大きな障害でした。
递归証明とは何ですか?
STARK 証明により、命題の証明にかかる時間は命題の実行にかかる時間とほぼ線形の関係になります。さらに、命題の証明にかかる時間が T である場合、証明の検証にかかる時間はおおよそ log (T) であり、これは通常「対数圧縮」と呼ばれます。つまり、STARK を使用することで、ユーザーは命題の計算に比べて証明の検証にかかる時間を大幅に短縮することができます。
Cairo は一般的な計算命題を表現することができ、これらの命題は STARK 証明によって証明され、対応する STARK バリデータによって検証されます。
これが递归の機会です:数千ものトランザクションの正確性を証明するために Cairo プログラムを書くことができるだけでなく、複数の STARK 証明を検証するために Cairo プログラムを書くこともできます。複数の「上流」証明の有効性を証明するための証明を生成することができます。これが递归証明と呼ばれるものです。
対数圧縮と証明時間のほぼ線形の関係により、STARK 証明の証明にかかる時間は非常に短くなります(将来的には数分程度になる予定です)。
递归を実装する際、SHARP は命題を受け取るとすぐにそれを検証することができます。証明はさまざまなモードで繰り返し結合され、递归証明が生成され、最終的に生成された証明がチェーン上のバリデータスマートコントラクトに提出されます。図 2 は典型的な递归証明のモードを示しています:
image
この例では、4 つの命題が SHARP に送信されます(それぞれが異なるアプリケーションから来る可能性があります)。これらの命題はそれぞれ個別に証明されます。次に、各証明のペアが递归バリデータ命題(STARK 証明を検証する Cairo プログラム)によって検証され、証明が生成されます。この命題は 2 つの証明が検証されたことを証明します。次に、递归バリデータ命題によってこれら 2 つの証明が再度結合されます。これにより、すべての 4 つの元の命題が証明される証明が生成されます。この証明は最終的にチェーンに提出され、Solidity バリデータスマートコントラクトによって検証されます。
递归証明の直接的な利点
チェーン上のコストを削減
複数の証明を 1 つに「圧縮」することに成功したため、トランザクションごとのチェーン上の検証コストが大幅に低下します(各命題には多くのトランザクションが含まれる可能性があります)。
递归証明を使用することで、証明のサイズに制約を受けることなく、証明の容量をほぼ無限に拡張することができます。各トランザクションのコストは数桁以上低下することができます。
実際の操作では、コストの削減は受け入れ可能な遅延(およびトランザクションの到着速度)に依存します。また、通常、各証明には関連するチェーン上のデータ出力も伴いますので、チェーンに書き込まれるデータ量も制限されます。それにもかかわらず、コストを数桁削減し、パフォーマンスをさらに向上させることは容易です。
遅延の低減
递归証明モードは、大規模な組み合わせ命題の証明の遅延を低減することができます。2 つの要素が機能します:
受信した命題は並列に証明できます(巨大な組み合わせ命題を証明する必要はありません)。
Train の最後の命題が到着するのを待つ必要はありません。代わりに、新しい命題が到着するたびにいつでも証明と結合できます。つまり、Train の最後の命題の遅延は、最後の命題の証明にかかる時間に加えて、証明の递归バリデータ命題(この特定の Train に「参加」しているすべての命題を証明する)にかかる時間です。
私たちは証明の递归バリデータ命題の遅延問題に積極的に取り組んでおり、数ヶ月以内に証明の递归バリデータ命題が数分のオーダーに達すると予想しています。したがって、効率的な SHARP の遅延は数分から数時間に制御することができます。遅延の長さは、各トランザクションのチェーン上のコストに対するトレードオフに依存します。これは SHARP の遅延の大幅な改善です。
L3 アプリケーションの促進
Cairo で開発された递归バリデータ命題は、StarkNet に証明を提出する可能性を開くものです。これにより、StarkNet の L2 パブリックネットワーク上に L3 を展開することができます。
递归モードは、L2 上の単一の証明によって検証される L3 からの集約証明にも適用されます。したがって、L3 も大規模なスケーリングを実現することができます。
その他の応用
递归は、コストとパフォーマンスをさらに拡張したいプラットフォームやアプリケーションにさらなる機会を提供します。
各 STARK 証明は、特定の「公開入力」(または Cairo の用語で「プログラム出力」)に適用される命題の有効性を証明します。概念的には、STARK の再帰性により、2 つの入力を持つ 2 つの証明を 1 つの入力を持つ証明に圧縮することができます。つまり、証明の数は減少しますが、入力の数は変わりません。その後、入力は通常、アプリケーションによって L1 上の特定の状態を更新するために使用されます(たとえば、状態ルートの更新やチェーン上の引き出しの実行など)。
递归命題がアプリケーションレベルで認識できる場合、つまりアプリケーション自体の意味を理解できる場合、递归命題は 2 つの証明を 1 つに圧縮するだけでなく、2 つの入力を 1 つに組み合わせることもできます。最終的な命題の証明は、アプリケーションの意味に基づいた入力の組み合わせの有効性を証明します。これがアプリケーションの再帰(Applicative Recursion)です(図 3 の例を参照)。
image
命題 1 は A から B への状態更新を証明し、命題 2 は B から C へのさらなる更新を検証します。命題 1 と命題 2 の証明は、第三の命題に結合され、A から C への更新を直接証明します。同様の再帰的なロジックを適用することで、状態更新のコストを大幅に削減し、最終的な遅延要件を達成することができます。
アプリケーションの再帰のもう 1 つの重要な例は、複数の証明からの集約データの圧縮です。たとえば、StarkNet のような有効性証明ロールアップの場合、L2 の各ストレージ更新も L1 の転送データとして保存され、データの可用性が確保されます。ただし、同じストレージユニットに対して複数回の更新を送信する必要はありません。なぜなら、証明で検証されたトランザクションのみが最終的にデータの可用性を満たすからです。この最適化は、単一の StarkNet ブロックで実行されています。ただし、アプリケーションの再帰を適用することで、複数の L2 ブロックの集約データを圧縮することができます。これにより、コストを大幅に削減し、L2 のブロック生成時間を短縮することができますが、L1 の更新のスケーラビリティを損なうことはありません。
注意すべき点:アプリケーションの再帰は、前述のアプリケーションの一般的な再帰と組み合わせて使用することができます。ただし、これらの 2 つの最適化は関連していません。
バリデータの複雑さの低減
STARK バリデータの複雑さは、検証に使用される命題のタイプによって異なります。特に Cairo の命題については、バリデータの複雑さは Cairo 言語で許可される特定の要素、具体的にはサポートされるビルトインアイテム(Cairo を CPU に例えると、ビルトインアイテムは CPU のマイクロサーキットに相当します:計算が頻繁すぎるため、自身の計算を最適化する必要があります)に依存します。
Cairo 言語は進化し続け、ますます有用なビルトインアイテムを提供しています。一方、递归バリデータは一部のビルトインアイテムのみを使用する必要があります。したがって、递归 SHARP は、Cairo の任意の命題をサポートするために递归バリデータで完全な言語をサポートすることに成功しました。具体的には、L1 の Solidity バリデータは递归証明を検証するだけなので、バリデータはより安定したサブセットの Cairo 言語を検証するだけで十分です:L1 バリデータは最新で最も安定したビルトインアイテムの更新を必要としません。言い換えれば、命題は進化し続けますが、複雑な検証は L2 に任せ、L1 バリデータは単純で安定した命題を検証するだけです。
計算フットプリントの削減
递归の前では、複数の命題を 1 つの証明に集約することが制約されていました(証明が証明できる命題のサイズと生成に必要な時間によって制約されます)。
递归により、そのような大きな命題を証明する必要はありません。より小さくて安価な計算インスタンスが利用できるためです(ただし、大規模な単一のプルーバーを使用する場合よりも多くの計算インスタンスが必要になるかもしれません)。これにより、証明器インスタンスをより多くの物理的および仮想的な環境に展開することが可能になります。
まとめ
一般的な計算の递归証明は、StarkNet を含むイーサリアムメインネット上の複数の製品システムにすでに展開されています。
递归の利点は、改善が進むにつれて徐々に明らかになります。並列計算のポテンシャルが発揮されると、ガス料金が削減され、遅延が改善され、超高いスケーラビリティが実現されるでしょう。
递归はコストと遅延の面で非常に優れており、L3 およびアプリケーションの再帰などの新たな機会を生み出します。递归バリデータは引き続き最適化され、パフォーマンスとコスト効率も向上していくでしょう。