# Cairo 基礎介紹

➡ 看完基礎介紹後如果你對 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:

%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` 檔，例如：

{
    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 語法範例

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

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 時候的值

func main():
    [ap] = 100; ap++
    # << Your code here >>

    ret
end

- 要求：在程序結束時，取值的結果必須在 `ap - 1` 這個 memory cell 裡
- 要求：你的代碼不需依賴於 `x` 的值

:::spoiler Answer:

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
這可以讓我們減少代碼數量：

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