概要
递归証明のメインネットへのリリースにより、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（SHARed ProSver）は、複数の独立したアプリケーションのトランザクションを集約し、単一の STARK 証明で証明することができる共有証明器です。アプリケーションは異なるバッチのトランザクションを組み合わせることができ、STARK 証明の容量をより迅速に埋めることができます。トランザクションの処理速度と遅延が向上します。递归証明は次世代の先進技術であり、ハードコーディングされたロジックだけでなく、一般的な計算にも適用されます。
递归証明のすべての利点を理解するには、これまでに（非递归的に）証明がどのように実行されてきたかを詳しく調べる必要があります。図 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 つに「圧縮」することに成功したため、トランザクションごとのチェーン上の検証コストが大幅に低下します（各命題には多くのトランザクションが含まれる可能性があります）。
递归証明を使用することで、証明のサイズに制約がある計算リソースの障害（メモリなど）がなくなります。各命題の容量は限られており、個別に証明することができます。したがって、递归を使用すると、递归的な組み合わせ命題（Train）の容量はほぼ無限になり、トランザクションごとのコストを数桁以上削減することができます。
実際の操作では、コストの削減は受け入れ可能な遅延（およびトランザクションの到着速度）に依存します。また、通常、各証明には関連するチェーン上のデータ出力も伴いますので、チェーンに書き込まれるデータ量も制限されます。それにもかかわらず、コストを数桁削減したり、パフォーマンスをさらに向上させたりすることは容易です。
遅延の低減
递归証明モードは、大規模な組み合わせ命題の証明の遅延を低減することができます。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 の証明は 1 つの証明に結合され、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 およびアプリケーションの递归など、新たな機会を生み出します。递归バリデーターは継続的に最適化され、パフォーマンスとコスト効率も向上していきます。