Cairoの基本

有限体

多くの有限体上での割り算と同様に x / y の結果は常に式 (x / y) * y == x を満たす

値が偶数かどうかのチェック：

通常のCPUでは、ある値xに2をかけると、結果は常に偶数になる。これはCairoでは成り立たない。

前に見たように、(P+1)/2を取って2を掛けると1が得られるが、これは奇数である。実はこの性質は、CPUでは「たまたま」働いているのです。

x に 3 をかけても 3 で割り切れる数にはならないのです (次の c++ コードを実行してみてください: std::cout << 122979382473034411U * 3 << std::endl;)．

ほとんどの変数はfield elementに定義される臭い

非決定論的計算

Cairoプログラムの目的は、「ある計算が正しいこと」を証明することなので、時にはショートカットをすることもある。

たとえば、「x=961 の平方根 y が 0 ～ 100 の範囲にあることを証明すること」を考えれば、961から始めてその根を計算し、その根が必要な範囲にあることを確認する複雑なコードを書くことになる

しかし、もっと簡単な方法で、以下の二つの命題に分解してを示せばよい

31から始めてそれを2乗すれば961になること

31が範囲内にあること

つまり、入力(961)から始めるのではなく、解(31)から始める。このような証明方法を非決定論的計算と呼ぶ

非決定論的計算は以下のように分類できる

1. yの値を推測する

3. yが範囲内であることを確認する

メモリ

メモリは一度だけセルに値を書き込むことができるが、その後値を変更することはできない

つまり、各メモリセルの値は証明者が選択するが、Cairo プログラム実行中に)変更することはできない

「アドレス 0 のメモリセルから値を読んで、7 を得たことを確認する」または

「そのメモリセルに値 7 を書き込む」と解釈できる

連続メモリ

Cairoでは、プログラムがアクセスするメモリアドレスが連続している

例えば、アドレス7と9にアクセスした場合、プログラムの終了までに8にもアクセスしなければならない（アクセスの順番は関係ない）。

アドレス範囲に隙間がある場合、証明者は自動的にそのアドレスを任意の値で埋める

このような隙間があることは、メモリが使われずに消費されていることを意味し、非効率的

あまりに多くの隙間があると、証明生成コストが高くなりすぎてしまう

それでも健全性保証には違反しせず、偽証明を生成できないらしい。根拠は？

レジスタ

時間の経過とともに変化する可能性のある唯一の値は、指定されたレジスタ内に保持される

ap (アロケーションポインタ) - まだ使用されていないメモリセル

fp (フレームポインタ) - 現在の関数のフレーム。

関数のすべての引数とローカル変数のアドレスは、このレジスタの値からの相対的なもので、関数が開始されるとこの値はapと等しくなる。

しかし、apとは異なり、fpの値は関数のスコープ全体を通じて同じまま

pc (プログラムカウンタ) - 現在の命令

ap++ という接尾辞は、命令を実行した後で Cairo に ap を 1 つ増やすように指示します

ap++ はそれ自体で命令ではなく、セミコロンの前に現れる命令の一部分で、この構文はap++独自のものであり、2つの命令を分離するために使用することはできない

code:ex

次のリストは、Cairo にある有効なassert-equal 命令が何であるかを示しています。

code:example2

命令中に出現する可能性のある整数は2種類あります。