超市のレシートを例にして、stark の検証方法を説明します。
実際に行うことは、プログラム A に入力 x を与え、出力 y と時間制限 T を得ると、"A (x) が T の計算ステップ内で y を出力する" ことを証明するための証明文字列 Π を生成することです。y が 1 であれば、有効な証明です。
まず、再計算が不可能であることを検証する必要はありません。検証には実行トレースの一部をサンプリングするだけで十分であり、サンプリングが有効であるためには、エラーコードの機能を利用する必要があります。
また、実行トレースのデータが真実であり、変更されていないことを保証する必要があります。この場合、多項式コミットメントを利用する必要があります。検証には多項式コミットメントが必要であり、高速検証には低次テスト、高速冪算法、フェルマーの法則などを利用する必要があります。
上記の要素があれば、有効な検証が保証されます。また、透明性と非対話型検証を実現するために、ハッシュ関数を利用する必要があります。
手順のまとめ#
- 初期計算の実行トレース（スーパーマーケットのレシート）を取得します（encode (A,x,y,T)）。実行トレースをエンコードして T ステップの実行トレースを作成し、多項式を使用して𝚽を生成します。実行トレースを拡張するために、例えば 10 倍に拡張し、より大きな領域を選択します。実行トレースのデータは、領域の部分群（エラーコード、実行トレースは特定の領域上の多項式への割り当てとして見なされ、実行トレースを拡張するためにより大きな領域上のその多項式に割り当てられます）です。
- プログラム A をエンコードします。AIR を使用して、与えられたプログラムの制約を表す多項式の中間記述を行います。
- 上記の多項式を 1 つの多項式に統合し、FRI 多項式コミットメントを準備します。多項式コミットメントは、データが変更されないことを保証し、変更があれば検出されることを保証します（多項式コミットメントのサイズ、コミットメントの生成時間の複雑さは log (n) です。AIR の統合後の多項式と比較します）。
- 検証者はランダム性𝛔₀を送信し、これにより証明者と検証者はすべての多項式制約を A に "バンドル" することができます。
証明されたデータに基づいてハッシュを行い、いくつかのランダムな数値を生成します証明者は実行トレースと A に対する制約を組み合わせた多項式𝚵に基づいています。- 証明者は𝚵を検証者に送信します。検証者はローカルの整合性チェックを行い、𝚽と𝚵が適切に関連していることを確認します。
- 多項式コミットメントを行います。低次テストでは、log (𝚵の次数 n) 回の多項式分割の計算が必要であり、コミットメントのサイズの複雑さも log (n) です。コミットメントには𝚵のメルケル、分割後の𝚵のメルケル、ブランチパス（ブランチパスの選択は、以前の証明で生成されたデータのハッシュに基づいて各サンプルのインデックスまたは r 値をランダムに選択します）、最下層の葉のメルケルが含まれます。
- ハッシュに基づいて拡張された実行トレース（長い証明）の n 個のポイントをランダムにサンプリングします（低次テスト、ポイントごとのエラーの確率は 90% です）。証明は非対話型と多項式コミットメントを組み合わせて、各ポイントが正しいかどうかを検証します（低次テスト）。各ポイントの多項式コミットメントを取得し、状態ルートと組み合わせて証明を生成します。