超市のレシートを例にして、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 個のポイントをランダムにサンプリングします（低次のテスト、1 つのポイントのエラーを検出する確率は 90% です）。証明は非対話型と多項式コミットメントを組み合わせて各ポイントの正当性を検証します（低次のテスト）。各ポイントの多項式コミットメントを取得し、状態ルートと組み合わせて証明を生成します。