# Cairo 基礎介紹
###### tags: `Cairo` `StarkNet`
---
:::warning
（Last edited on 2022.10.14）很抱歉，Cairo 迭代速度太快，這份文件的內容已經過期。請參考官方網站：
- https://www.cairo-lang.org/docs/hello_starknet/index.html#
:::
---
➡ 看完基礎介紹後如果你對 Cairo 還想再跟深入學習的話，你可以透過文中連結的 Hello Cairo 官方教學文件或是我整理出來的一些[重點](https://hackmd.io/2xdTRB1jT62gbHDOG_i5Qg)
**警告：深入學習的水深和這篇基礎介紹的水深差很多**
___
[TOC]
___
## Introduction
STARK 所使用的編程語言
- **"圖靈完備"**
- 近似於低階語言的用法
- 比使用 Solidity 這種高階語言複雜許多
- 甚至比其他 SNARK 的編程語言像是 `circom` 或是 `ZoKrates` 還麻煩
- **"高效率"**
- 能使用的功能和套件庫還很少
- pedersen, ecdsa
- 使用 Cairo 打造的項目: DeversiFi, dydx and immutableX
- 都是基於 Starkware 打造的 StarEx
- 針對 Solidity contracts 有經過多方審計
- 但還沒有看到針對 Cairo 代碼的審計
- STARK Prover 目前是使用 Polaris License 授權
- 可用於非商業使用, 或是
- 使用於商業用途但是產生的 proof 必須要送到 Polaris Verifier 去驗證
- 這是一組由 Starkware 官方維護的 Verifier 的名單
- [SHARP](https://www.cairo-lang.org/docs/sharp.html)(Shared Prover) service
- 目前唯一產生 STARK proof 的方式，Start Prover 還未開源
- 由 Starkware 維護
- 搜集多方執行 Cairo 程序後的結果，合併產生一個 proof
- 平攤、共享 proof 的成本
### Documentations and codes
- 開發者文件
- [Hello Cairo](https://www.cairo-lang.org/docs/hello_cairo/index.html): 用範例來介紹 Cairo
- [How Cairo works](https://www.cairo-lang.org/docs/how_cairo_works/index.html): 深入 Cairo 細節
建議從 Hello Cairo 開始
### Playground
- [Cairo playground](https://cairo-lang.org/playground/)
- 像是 Remix，你可以在上面編寫、編譯 Cairo 程式，甚至產生 proof
- 上面也有一系列的範例和練習題
### Playground <-> local env
你也可以在本地安裝 Cairo 開發環境(下方 [Setting up environment](#Setting-up-environment) 會介紹)
在本地端開發有幾項相比於 playground 的優勢:
- 你可以為程序提供 [input](https://hackmd.io/aqZ708enRfq4mK1YixYhQA#program-input)
- 在 playground 裡，你只能寫死你的程序 input
- 在編譯和執行你的程式時，有更多選擇:
- 在執行程式（`cairo-run`）時，你可以透過設置 `--step` 及 `--no-end` 參數來指定程序從執行到停止的步數
- 這可以幫你檢視程序執行到一半的狀態、找出程序可能在哪一步驟出錯
- 另外你也可以設置 `--tracer` 參數
- 它會在 `localhost:8100` 跑起一個後台，在頁面上還原執行的過程
- playground 也有一樣的功能
___
## Setting up environment
https://www.cairo-lang.org/docs/quickstart.html
### 1. Python
- 官方文件使用 python3.7 及 python virtual env
### 2. Install preliminary packages
- Ubuntu: `sudo apt install -y libgmp3-dev`
- Mac: `brew install gmp`
- python packages: `pip3 install ecdsa fastecdsa sympy`
- 如果是使用 python3.6: `pip3 install contextvars`
### 3. Install Cairo
**撰文當前最新版是 0.2.0 版**
- [download cairo@0.2.0](https://github.com/starkware-libs/cairo-lang/releases/tag/v0.2.0)
- install: `pip3 install cairo-lang-0.2.0.zip`
### 4. Quick example
假設我想要寫一個小程式，證明我知道某個 hash 值的 pre-image:
```python=
%builtins output pedersen
from starkware.cairo.common.cairo_builtins import HashBuiltin
from starkware.cairo.common.hash import hash2
# Implicit arguments: addresses of the output and pedersen
# builtins.
func main{output_ptr, pedersen_ptr : HashBuiltin*}():
alloc_locals
local preimage
%{ ids.preimage = program_input['preimage'] %}
let (digest) = hash2{hash_ptr=pedersen_ptr}(preimage, 0)
assert [output_ptr] = digest
let output_ptr = output_ptr + 1
return ()
end
```
將這個檔案存為 `test.cairo`
並將只有你知道的 pre-image 值存到 `input.json` 檔，例如：
```json=
{
preimage: 33
}
```
### 5. Compile and run
- 編譯
- `cairo-compile test.cairo --output test_compiled.json`
- 執行
- `cairo-run --program=test_compiled.json --program_input=input.json --print_output --layout=small --tracer`
- 可以到 [http://localhost:8100/](http://localhost:8100/) 去檢視程序執行過程
- `--program_input` 指定 input 檔
- `--print_output` 會印出程序的輸出
- `--layout=small` 會指定要使用哪一組預設功能（但目前也沒有太多預設功能可以選擇
你會看到程式輸出
```
Program output:
10895499158002645496215369097676997787459265175555863332772759280702396009108
```
108 開頭這個數字即是 33 這個值經過 pedersen hash function 得到的輸出
**注意： program output 不只是方便你 debug 用的，它還會影響你程式執行所產生的 proof。怎麼影響？後面會講**
### 6. prove
- 接著產生 proof 的部分就要使用 SHARP 了
- 在本地端和 playground 都可以送請求給 SHARP
- 本地端執行 `cairo-sharp submit --source test.cairo`
- 它會編譯和執行程式，並把程序的 metadata 及 execution trace 傳送給 SHARP
- 你會得到一個 **Job key** 和一個 **Fact**
- **Job key** 用於 SHARP，你可以透過它向 SHARP 查詢 proof 的處理狀態
- **Fact** 就像是你 proof 的 id（像是以太交易的 tx hash）
- 所以如果你的程式代碼一樣，執行時的 program input 也是一樣的話，那你就會**拿到一樣的 Fact**
- SHARP 把 proof 送到鏈上合約並驗證後，合約會在 fact registry 合約去註冊你程序的 Fact
- 這時候你就可以透過[合約](https://ropsten.etherscan.io/address/0x4Cd99A1FC780d874a34008fdC6da2961d540fE64#readProxyContract)去查詢你的 Fact
- `isValid(FACT_OF_YOUR_PROOF)`
___
## 接下來先介紹一些 Cairo 的架構和語法基礎
### ❥ numbers are field elements and they operate in prime field
- `p = 3618502788666131213697322783095070105623107215331596699973092056135872020481`
- `x = 100 (% p)`, `y = 3 (% p)`, `x + y = 100 + 3 (% p)`
- `felt` 表示 field element
- 在執行 **division** 或是 **checking even number** 時要小心
- division
- `x / y = 1206167596222043737899107594365023368541035738443865566657697352045290673527`
- 你可以看到結果不是你平常預期的 `100 / 3 = 33.33...` 或是 `33`
- 它只確保 `1206167596222043737899107594365023368541035738443865566657697352045290673527 * y = x`
- 建議不要直接使用除法運算符號，而是使用提供的數學運算套件
- `from starkware.cairo.common.math import ...`
### ❥ basic components
1. memory cells
- 下圖中每一個 row 都是一個 memory cell
- 第二行由上往下 1, 2, 3, ... 就是 memory cell 的編號（或說地址）
- 第三行是該 memory cell 的內容
- memory cells 是 **read only**, 也就是說如果你對同一個 memory cell 去賦值，會失敗
2. instructions(紅圈處)
- memory cell 開頭會寫入該程式的所有指令（也就是 memory cell 的開頭會保留給你的程式代碼，後面才是留給你程式執行過程中會寫入的值）
3. pointers(藍圈及黃色底線處)有三種
- 在程序執行的過程中，這些 pointer 的值會一直改變
- program counter(**pc**, 黃色底線處)
- 指向當前的 instruction
- application pointer(**ap**)
- 指向一個未使用的 memory cell
- ap 的值會隨著執行一直改變
- frame pointer(**fp**)
- 指向當前的 function frame
- 不同於 ap，在同一個函式執行的期間，fp 的值是固定的
#### Cairo 語法範例
```python=
ap = 123 # NO, YOU CAN NOT DO THIS
[ap] = 123 # YES, YOU CAN DO THIS
# And it assigns 123 to the memory cell ap points to
[ap] = [ap - 1] * [fp]; ap++ # See (a ) below.
[fp - 1] = [ap - 2] + [fp + 4]
[ap - 1] = [fp + 10] * [ap]; ap++
[ap - 1] = [fp + 10] + 12345; ap++ # See (b ) below.
[fp + 2] = [ap + 5]
[fp + 2] = 12345
[ap + 2] = [[ap + 5]] # See (c ) below.
[ap] = [fp - 3] - [ap + 4] # See (d ) below.
[ap] = [fp - 3] / [ap + 4] # See (d ) below.
```
:::spoiler (a )
這個 instruction 聲明等號右邊的兩個 memory cell (`[ap - 1]` and `[fp]`) 的乘積必須等於下一個 un-used memory cell (也就是等號左邊的 `[ap]`).
我們把這看作是：把這兩個值的乘積寫進 `[ap]` 裡。最後面的 `ap++` 指示 cairo 在前面的動作執行完後，把 `ap` 的值加一（也就是指到下一個 un-used memroy cell）
要更改 `ap` 值的方法，除了 `ap++`，就是使用 `ap += ...`
注意：`ap++` **不是一個獨立的指令** - 它和 `;` 符號是一起使用的。`;` 在這不可以當作分開 instruction 的功能 (不像 C++ 等語言的用法)
:::
:::spoiler (b )
在一個 instruction 裡，會出現兩種整數值
1. immediates:
- 像是 `[fp + 2] = 12345` 或是 `[ap - 1] = [fp + 10] + 12345` 裡的 `12345`
2. offsets:
- 像是 `[fp - 1] = [ap - 2] + [fp + 4]` 裡的 `-1`, `-2` 和 `4`
- offsets 的值需在一個範圍內： [-2^15^, 2^15^]
:::
:::spoiler (c )
這是一個 double dereference 的 instruction，取得 `[ap + 5]` 的值並再把它當作某個 memory cell 的地址，再一次去取值
:::
:::spoiler (d )
這些是語法糖 instruction – 它們會被編譯器分別用 `[fp - 3] = [ap] + [ap + 4]` 及 `[fp - 3] = [ap] * [ap + 4]` 取代
:::
### ❥ immutable memory
```python=
func main():
[ap] = 100
[ap] = 101
ret
end
```
你會看到以下 error，因為 memory 只能寫一次，再一次對同一個 `ap` 寫入會噴錯
:::danger
An ASSERT_EQ instruction failed: 100 != 101
:::
#### ⭐️exercise: 算出 𝑥^3^+23𝑥^2^+45𝑥+67 這個多項式在 x=100 時候的值
```python=
func main():
[ap] = 100; ap++
# << Your code here >>
ret
end
```
- 要求：在程序結束時，取值的結果必須在 `ap - 1` 這個 memory cell 裡
- 要求：你的代碼不需依賴於 `x` 的值
:::spoiler Answer:
```python=
func main():
[ap] = 100; ap++ # x
[ap] = [ap - 1] * [ap - 1]; ap++ # x^2
[ap] = [ap - 1] * [ap - 2]; ap++ # x^3
[ap] = [ap - 3] * 45; ap++ # 45x
[ap] = [ap - 3] * 23; ap++ # 23x^2
[ap] = [ap - 3] + [ap - 1]; ap++ # x^3 + 23x^2
[ap] = [ap - 3] + [ap - 1]; ap++ # x^3 + 23x^2 + 45x
[ap] = [ap - 1] + 67; ap++ # x^3 + 23x^2 + 45x + 67
ret
end
```
**你可以看到，要紀錄 ap 的變化是很困難的**
另一方面我們知道 x^3^+23x^2^+45x+67 可以寫成 x(x(x + 23) + 45) + 67
這可以讓我們減少代碼數量：
```python=
func main():
[ap] = 100; ap++ # x
[ap] = [ap - 1] + 23; ap++ # x + 23
[ap] = [ap - 1] * [ap - 2]; ap++ # x(x + 23)
[ap] = [ap - 1] + 45; ap++ # x(x + 23) + 45
[ap] = [ap - 1] * [ap - 4]; ap++ # x(x(x + 23) + 45)
[ap] = [ap - 1] + 67; ap++ # x(x(x + 23) + 45) + 67
ret
end
```
:::
___
## Wrap up
到這邊，你對最基本的 Cairo 架構及語法已經有一些了解了：
- memory cell 只能寫一次，寫完要改變 `ap` pointer 的值，讓它指向下一個沒被寫過的 memory cell
- 要紀錄這些 pointer 很困難，但別擔心，會有工具減輕這個負擔（例如 Reference 的使用），但在這不會去介紹 Reference
然後你也看過證明你知道 pre-image 的簡短例子了，知道怎麼 compile 和產生 proof。這邊要 highlight 的是例子中出現的兩段程式碼：
1.
```
%{ ids.preimage = program_input['preimage'] %}
```
2.
```
assert [output_ptr] = digest
```
第一段程式碼在做的事情是從 `input.json` 裡讀進只有你知道的 `preimage` 值
- `program_input` 是 Cairo 特殊用法，功能是讀進你在 `cairo-run` 透過參數 `program_input=...` 指定的 input json 檔
- `%{` 和 `%}` 這兩個符號組合中間的值是一個叫 hint 的 Cairo 功能，它是給 Prover 的工具（例如讀進 program input），對 Verifier 或其他沒有執行這個 Cairo 程式的人來說，hint 裡的代碼是無意義的
- 在這也不會去更詳細地介紹 hint
第二段代碼在做的是把 `digest` 的值，輸出到 program output。如同上面所說，program output 不只是給你 debug 用的，它還會影響你程式執行所產生的 proof！記得上面提到的 fact 嗎？這個 fact 是你 proof 的 id，它被註冊進 fact registry 代表你的 proof 成功被驗證
- fact 是由程式本身代碼的 hash 值再加上程式所輸出的 program output，組合起來再拿去 hash 所得到的值。
- 大概像這樣：`fact = hash(hash(program) | program outputs...)`
- 所以只要你 program input 不變（或甚至你的程式連 program input 都沒有），program output 就會一樣，而 program ouput 一樣，fact 就會一樣。
- 就像是你 pre-image 給 33，那 program output 一定會是 180 開頭那個數字
- 如果你 pre-image 給 34，那就會得到不一樣的 program output，也就會得到不一樣的 fact
- 那 dapp 要怎麼使用 fact ？
- 首先你要等到 SHARP 把 proof 送到鏈上去驗證，並註冊了你的 fact
- 再來你要去戳 dapp，告訴它你的 program output，讓它用 program output 加上 program 的 hash 值算出 fact，然後去問 fact registry
- 如果它確認這個 fact 真的存在 fact registry，那他就能確認你真的知道 pre-image
- 你可能會疑問它怎麼知道 program 的 hash 值？這裡假設 dapp 已經透過某種方式註冊這個 program 的 hash 值，所以你拿你自己寫的作弊 Cairo program 想要去騙 dapp 是沒辦法的，因為你的 program hash 和 dapp 裡註冊的 program hash 不一樣
- 我知道這個 Cairo program 例子很廢，但我只是想要藉由這個例子讓你知道 dapp 要怎麼整合 Cairo program
- 它和你可能習以為常的 dapp 使用方式很不一樣：
- 用 hint 讀取 program input
- 還要把你要證明的值 output 出來
- 然後你要等 SHARP 上傳 proof、fact 被註冊後，才能戳 dapp
- 最後你要提供 program output，讓 dapp 算出 fact
Sign in with Wallet
Connect another wallet