how the pyramids where built
Cairo VMについてzk summitのスライドからみていく
https://scrapbox.io/files/62667936fc21ae00233879f0.pnghttps://scrapbox.io/files/6266793c18e19000219d00e4.png
キムチは流石にダサいって..
kimchiはcircom的なフレームワークと理解
https://scrapbox.io/files/62667e065d00bf001d913908.png
レジスタ
Cairo VMは3 つのレジスタ (pc, ap, fp) で動作する "CPU" で構成されている決定論的ステートマシン
CPUは、pc、ap、fpの3つのレジスタを操作し、mという (読み出し専用の) メモリにアクセスできる。
pc: 現在実行中のCairo命令のメモリ上のアドレスが格納されている
ap: 慣習的に、これまでプログラムによって使用されていない最初のメモリセルを指している
多くの命令では、別のメモリセルが命令によって使われたことを示すために、この値を1つ増やすことがある
fp: 現在の関数のスタックフレームの先頭を指す。
fpの値によっては、スタックライクな動作が可能になる。
関数が戻ってきたとき,fpは以前の値に戻る.したがって、fpの値は、同じ関数の呼び出しのすべての命令で同じ
この性質により、fpは関数の引数やローカル変数のアドレスとして使用することができる
https://scrapbox.io/files/6266799158bc8b0021214f44.pnghttps://scrapbox.io/files/626679a618e19000219d0437.png
ここで、以下のように15番地に100を入れて、その次に1を加算すると15番地の値が101になる
https://scrapbox.io/files/626679e85e888c001d7460c3.pnghttps://scrapbox.io/files/626679ee7b416a001d093cd9.png
メモリの整合性はグローバルな要件なので、ローカルにチェックすることは複雑であり、15番地に何があるのか読み出せない
メモリアドレスと時系列で命令をソートする必要があり、フィールドでは些細なことではない
この辺のCairoの仕様はRustっぽい
つまり、メモリ書き込みは一度のみ許されるmutableなメモリを持っているので、毎度メモリの値を比較している
https://scrapbox.io/files/62667a9694ee88002383a550.pnghttps://scrapbox.io/files/62667aa78ad990001dd7fe98.png
そのほかのjumpやincrementsについては資料参照
メモリ
CPU は、非決定的な読み取り専用のランダムアクセスメモリにアクセスできる。
非決定論的とは、すべてのメモリセルの初期値、ひいては最終値を、証明者が選択することが許されているという意味
読み取り専用とは、Cairoコードの実行中にメモリセルの値が変化しないことを意味する
ここでは、アドレスaのメモリの値を表すために、m(a)とaという表記を使用しています。 https://scrapbox.io/files/62694d57c90435001e538333.png
各命令の最初のワードを形成する63ビットの構造。
ビットはリトルエンディアンに似たエンコーディングで並びます(最下位ビットが最初)
offdstは下位16ビット、dst_regは48ビット(最下位ビットから)
命令セット
cairo VMではプログラム(以降Pと呼ぶ)を構成する命令群のAIR(STARKベースのスキーム)を作成する
-> ini_pc | ini_ap | ini_fp を入力として P を実行すると、出力レジスタ fin_pc | fin_ap | fin_fp が得られることの証明を作成する
https://scrapbox.io/files/62667c73e2431b002036fd2f.pnghttps://scrapbox.io/files/62667c81c9fdf60020960496.png
各命令の意味によって、状態遷移の内容が決定される。
プログラムの命令は64ビットであり、以下のような構造になっている
table: 命令セット
0-15 0ff_dst
16-31 off_op0
32-47 0ff_op1
48-63 flags
https://scrapbox.io/files/62667d148ff67800234f4306.pnghttps://scrapbox.io/files/62667d20b14cd100234a0257.png
https://scrapbox.io/files/62667d2ed266d000231f5643.pnghttps://scrapbox.io/files/62667d3658bc8b0021216a6a.png
左辺(off_dst) =(flags) 右辺(off_op0)(off_op1)
オペコード単体で実行可能な命令もあるが、命令が操作する値や対象(メインメモリの番地など)を指定する必要がある場合もあり、これをoperandという。
オペコードとオペランドの組み合わせで一つの命令が構成される。オペランドの数は命令ごとに決まっている
flagsの中身
dst_regとop0_regは0=apもしくは1=fpをとる
https://scrapbox.io/files/6266a6767b416a001d0ad7d4.pnghttps://scrapbox.io/files/6266a67eacbc15001ddfc020.png
pcの2-4はop1_srcが保持しており、二つ目のoperandを指定する
5-6はres_logであり、右辺の計算処理を定義する
https://scrapbox.io/files/6266ae0dc9fdf6002098c18d.pnghttps://scrapbox.io/files/6266ae1394ee88002385b0d5.png
7-9はpc の更新またはインクリメントの種類を定義する
10-11はap の更新またはインクリメントの種類を定義する
https://scrapbox.io/files/6266aece494142001d6e7a81.pnghttps://scrapbox.io/files/6266aed7ed4a2c00232b3df2.png
12-14はopecodeなのでアセンブリ命令の種類を表す
https://scrapbox.io/files/6266aee9494142001d6e7c8d.png
具体的にdst,op0,op1,regは何をやってるんだい?
https://scrapbox.io/files/6266af29b90a1400237924e7.pnghttps://scrapbox.io/files/6266af2f5eb86f001d551790.png
https://scrapbox.io/files/6266af44ce365b001d462b1e.pnghttps://scrapbox.io/files/6266af4908e001001d606ec4.png
無駄にスライドつけてるだけな気がしてきたので一旦pending(2022/04/25)
状態遷移的な
https://scrapbox.io/files/6266b64218e19000219fb473.pnghttps://scrapbox.io/files/6266b64a2ec56a0023f0b951.png
https://scrapbox.io/files/6266b72e08e001001d60a7e2.pnghttps://scrapbox.io/files/6266b735e9731c001d6b2722.png
https://scrapbox.io/files/6266b766b14cd100234c32a9.pnghttps://scrapbox.io/files/6266b778494142001d6ed0c9.png
https://scrapbox.io/files/6266b780167bbb0023d4ba71.pnghttps://scrapbox.io/files/6266b7887b416a001d0b6bd2.png
https://scrapbox.io/files/6266b79258bc8b002123c04b.pnghttps://scrapbox.io/files/6266b799d266d0002322166e.png
https://scrapbox.io/files/6266b7a0acbc15001de074aa.pnghttps://scrapbox.io/files/6266b7a7503472001dfcd7e7.png
https://scrapbox.io/files/6266b7b4e5be01001d829a57.png
https://scrapbox.io/files/626946767a763d001de1e3a2.png
AIR for Cairo
このセクションでは、Cairo マシンの AIR (算術中間表現) を構築する方法を説明します
2.1節では、AIR をフィールド要素の表 (トレース) に対して作用する多項式制約の体系と定義しました。
Cairo VM用のAIRは、カイロマシンがacceptを出力する場合に限り、制約を満たすようなシステムである。
このようなAIRを使えば、証明者は検証者にマシンがacceptすることを納得させることができる。
なお、このセクションを理解することは、Cairo 言語やアーキテクチャを理解するために必要ではありません。
ただし、メモリ制約と並べ換え範囲チェック制約により、健全性、完全性ともに完全とは言えない。
メモリ制約の健全性誤差も並べ替え範囲チェックの健全性誤差も解析できるらしい
AIRを記述する簡単な方法は、トレースの各セルが何を意味するかを記述し、次に各制約を列挙して、それが何を強制するかを説明することである。
このセクションでは、制約のリストとトレースセルの拡張を交互に行う別の方法でAIRを紹介します。
我々の目的のために、表中の各セルの正確な位置は調べないことにします。
そのセルがいくつのインスタンスとして存在するかにのみ注目します。例えば、以下のような場合です。
N = T + 1のトレースセルがi∈0, Tのpciを表し、16Nのトレースセルは のトレースセルは、命令のフラグを表す15ビット(技術的な理由によ り。
技術的な理由により、セル数は2のべき乗でなければなりません)。
同じ役割を持つトレースセルの集合を仮想カラムと呼ぶ。必要な仮想カラムをすべて集めたら、2次元のテーブルの中にどのように配置するかを決めます。全ての仮想カラムは周期的に1つのカラムの中に配置される。例えば、トレース長(行数)がL=16Nであれば、pciを表す仮想カラムは16行ごとにテーブル内にセルを持つことになる。
サイズ間の比率が2のべき乗であることから、最適配置29の処理は容易であるが、本稿では扱わない。
また、仮想カラムを構成するセルの中から周期的な部分集合を取り出し、そのセルを仮想カラムとして扱う仮想サブカラムの概念も定義する。
例えば、サイズ4Nの仮想カラムを定義し、その上で全ての値が0, 216の範囲にあることを強制し、サイズNの3つのサブカラムをoffdst, offop0, offop1について定義することができる。 これにより、親カラムに対して1組の制約を記述することができます(例えば。
を記述し、offdst, offop0, offop1に対して、命令での使用方法に応じた3組の制約を記述します。
したがって、次のように進みます:仮想カラムのいくつかを記述します。
次に、それらに関連するいくつかの制約を記述し、さらに仮想カラムと制約を記述する可能性があります。
列を記述し、さらに制約を記述し、といった具合に進めていきます。