---
# System prepended metadata

title: STARK VM Tutorial

---

## STARK VM
### STARK
> Scalable Transparent ARgument of Knowledge, which applies to any SNARK (or even interactive SARK) that has at most a polylogarithmic prover overhead and no trusted setup.
 
정의가 넓은데 그 중 특히 AET, AIR, FRI 를 사용하는 STARK를 다룬다.

### AIR and AET
#### Arithmetic Intermediate Representation (AIR) constraints
- Boundary constraints: $\mathbb{F}^{\mathsf{w}} \rightarrow \mathbb{F}$
	- 함수 반환은 0 이면 만족, 아니면 불만족.
- Transition constraints: $\mathbb{F}^{2\mathsf{w}} \rightarrow \mathbb{F}$
	- (지금 상태, 다음 상태) 를 인자로 받기 때문에 2w 개의 인자
	- 상태는 레지스터, 메모리 등
#### Algebraic Execution Trace (AET)
T개의 명령으로 구성된 프로그램이라고 하면 T+1 개의 행의 AET가 나온다.
1. 초기 상태
2. 1개의 명령을 실행할 때마다 1개의 행 추가.

The AET is _integral_ if all Arithmetic Intermediate Representation (AIR) constraints are satisfied.

### Commitment
p = 2^64 - 2^32 + 1. prime
전체 Field generator $g = 1753635133440165772$
$g ^{2^{32}} = 1$
Trace domain의 generator $\omicron = g^{order/height}$
Fri domain은 $c \cdot o^i$

BaseField. 
$\mathbb{F}_{p^3} \cong \frac{\mathbb{F}[X]}{\langle X^3 -X + 1\rangle}$
64비트가 작기 때문에 Extension column 부터는 Extension Field의 원소들을 채운다.

하나의 제약당 두 개의 random 이 필요.
아래의 Nonlinear combination 다항식이 FRI의 입력이 된다.
$$\sum_{i=0} \alpha_i \cdot q_i(X) + \beta_i \cdot X^{\mathsf{d} - b_i} \cdot q_i(X) \enspace$$

$\alpha_i$ 가 필요한 이유에 대한 설명
https://aszepieniec.github.io/stark-anatomy/fri#compiling-a-polynomial-iop

### FRI
Quotient polynomial이 low-degree polynomial 임을 증명하는 방법.
- "low-degree"란  $\rho |D|$ 이하의 차수를 의미.
- FRI에서 folding을 수행해도 각 단계의 `(Hamming distance)/전체 길이` 비율은 유지되거나 증가한다. 마지막 단계에서 얻어진 상수항(Field element)이 예상값과 같으면 원래 다항식을 낮은 차수로, 다르면 높은 차수로 판정한다. 이 과정에서 $\rho$ 확률로 잘못된 판정을 할 수 있다. 보안 수준을 높이기 위해 여러 인덱스에 대해 이 과정을 반복하며, i번 반복하면 전체 오류 확률은 $\rho^i$ 로 감소하여 security bits를 증가시킨다.

### 폰 노이만 구조
1. 메모리에서 다음 명령을 읽는다.
2. 메모리 또는 표준 입력에서 데이터를 읽는다.
3. 명령에 따라 레지스터를 업데이트한다.
4. 메모리 또는 표준 출력에 데이터를 쓴다.

![von-neumann.svg](https://aszepieniec.github.io/stark-brainfuck/graphics/von-neumann.svg)

테이블이 여러 개이다. 프로세서, 메모리, 프로그램, 입력, 출력.
1. 개별 테이블 제약.
2. 테이블간의 관계에 대한 제약.

### Permutation Arguments
주장: 두 열은 순서만 다르다. 즉, 중복을 허용하는 집합으로서 같다.
$\lbrace c_ i \rbrace_ i = \lbrace k_ i\rbrace_ i$ 
예: $\lbrace 1, 3, 1, 2 \rbrace = \lbrace 1, 1, 2, 3 \rbrace$ 

**The transition constraint**
$\prod_i(\alpha - c_i) = \prod_i(\alpha - k_i)$
$\alpha$ 를 이용해 `2 * 3 = 1 * 6` 이렇게 다른 집합의 곱이 같아지는 것을 막는다.

예시

| $c_i$ | $e$                                                |
| ----- | -------------------------------------------------- |
| $w$   | $\alpha - w$                                       |
| $x$   | $(\alpha - w)(\alpha - x)$                         |
| $y$   | $(\alpha - w)(\alpha - x)(\alpha - y)$             |
| $z$   | $(\alpha - w)(\alpha - x)(\alpha - y)(\alpha - z)$ |

| $k_i$ | $e$                                                |
| ----- | -------------------------------------------------- |
| $x$   | $\alpha - x$                                       |
| $y$   | $(\alpha - x)(\alpha - y)$                         |
| $w$   | $(\alpha - x)(\alpha - y)(\alpha - w)$             |
| $z$   | $(\alpha - x)(\alpha - y)(\alpha - w)(\alpha - z)$ |

증명 개요
- Schwartz-zippel lemma로 $\alpha$에 방정식의 해가 나올 확률은 $height/|F|$.

Reference: [stark-brainfuck/docs/engine.md at master · aszepieniec/stark-brainfuck · GitHub](https://github.com/aszepieniec/stark-brainfuck/blob/master/docs/engine.md#permutation-arguments)

### Evaluation Arguments
주장: 한 테이블의 행들은 다른 테이블 행들의 서브리스트이다. 순서 보존.
$(c_i)_{i \vert j_{i}= 1}  = (k_j)_j$
- $j_i = 1$인 항들만 짧은 테이블의 칼럼에 포함됨.
- 순서까지 같음을 보이기 위해 먼저 나온 항일수록 $\alpha$ 의 차수가 높다. 

**The transition constraint**
큰 테이블
$\forall i > 0 : e_ {i} = \jmath_ {i} \cdot (\alpha e_ {i-1} + c_ i) + (1 - \jmath_ {i}) \cdot e_ {i-1}$
- $\jmath_i = 1$ 일 때만 기존 $e_{i-1}$ 에 $\alpha$ 를 곱하고 이번 행의 $c_i$ 를 더해준다.

작은 테이블
$\forall j > 0 : e_j = \alpha e_{j-1} + k_j$
- 모든 행에서 기존 $e_{i-1}$ 에 $\alpha$ 를 곱하고 이번 행의 $c_i$ 를 더해준다.

예시
큰 테이블

| $\jmath_ i$ | $c_ i$ | $e_ i$                      |
| ----------- | ------ | --------------------------- |
| 0           | $u$    | 0                           |
| 1           | $x$    | $x$                         |
| 0           | $v$    | $x$                         |
| 1           | $y$    | $\alpha x + y$              |
| 0           | $w$    | $\alpha x + y$              |
| 1           | $z$    | $\alpha^2 x + \alpha y + z$ |

작은 테이블

| $c_ j$ | $e_ j$                      |
| ------ | --------------------------- |
| $x$    | $x$                         |
| $y$    | $\alpha x + y$              |
| $z$    | $\alpha^2 x + \alpha y + z$ |

### Table Relations with Zero-Knowledge
문제: Permutation argument, Evaluation argument 는 Terminal 값으로 정보를 누출한다.
해결: Prover는 초기값을 1이 아닌 임의의 수로 두고 Verifier에게 보내지 않는다.
$k \cdot a \cdot \cdot b = k \cdot b \cdot a$ 이므로 초기값 k는 임의의 수여도 Permutation argument 는 성립한다. 대신 두 칼럼의 초기값은 같아야 한다. 이에 대한 제약은 아래의 **Difference Constraints** 에서 설명한다.

### STARK Engine 작동 순서
1. Execution trace의 데이터로 테이블의 base column들을 채운다. 테이블의 길이가 모두 $2^n$ 으로 같게 padding row도 넣는다.
2. 최대 차수의 randomizer polynomial를 랜덤하게 뽑는다. 이를 FRI domain에서 계산해서 _randomizer codeword_ 를 얻는다.
3. 테이블의 base 칼럼들을 보간(interpolate)한 뒤, 이를 FRI domain에서 계산해서 _base codewords_ 를 얻는다.
	1. 이 때 interpolation의 x좌표로 $2^n$ 개의 Trace domain의 원소들과 추가되는 randomizer 행들이 쓰인다.
	2. Trace domain은 $w^{2^n} = 1$ 을 만족하는 원소들이다.
	3. FRI domain은 위와 교집합이 없도록 $o w^i$ 를 만족하는 원소들이다.
4. Zip the randomizer and base codewords 후 머클 트리를 구한다.
	1. zip: 여러 원소들을 비트 단위로 이어붙임을 의미.
5. 머클 트리 루트를 Verifier에게 보내고 랜덤 상수 $a,b,c, \alpha, ...$ 등의 challenge를 얻는다.
6. challenge를 이용해 테이블의 extension columns를 채운다.
7. 테이블의 extension 칼럼들을 보간(interpolate)한 뒤, 이를 FRI domain에서 계산해서 _extension codewords_ 를 얻는다.
8. 모든 AIR 제약에 대한 _Quotient codewords_ 를 계산한다.
	1. Quotient codewords는 Quotient polynomial을 FRI domain에서 평가한 값들을 NTT(Number Theoretic Fourier Transform) 를 통해 계산함을 의미한다.
	2. Quotient polynomial 은 아래에서 자세히 알아보자.
9. Zip the extension codewords 후 두번째 머클 트리를 구한다.
10. Verifier에게 머클 루트를 보내고 1 + 2b + 2e + 2q 개의 랜덤 상수, _weights_ 를 받는다. b는 base codewords의 개수, e는 extension codewords의 개수, q는 quotient codewords의 개수를 말한다.
11. A nonlinear combination 을 계산한다. 
	1. 각 codeword는  $g(X) = \sum_{i=0}^{n-1} \alpha_i \cdot f_i(X) + \beta_i \cdot X^{2^k-d_i-1} \cdot f_i(X) \enspace$ 식으로 전부 더한다.
	2. randomizer는 하나의 weight만 사용해서 위에 더해준다.
12. 이 nonlinear combination codeword 의 머클 트리를 계산한다.
13. Verifier에게 머클 루트를 보내고 correct combination인지 체크할 t 개의 인덱스를 받는다.
14. 해당 인덱스들을 3개의 트리에서 open한다. weights와 codewords를 내적한 값과 nonlinear combination 중 해당 인덱스의 leaf node가 같은지 검증한다. 
15. The nonlinear combination codeword 에 대해서 FRI를 실행해서 각각의 열이 low-degree polynomial임을 보인다.

### Quotient polynomials
i번째 열에 대한 다항식을 c_i(x) 라 하자. 

**Boundary constraint**
첫번째 행에 대해서만 성립하는 제약
$$\frac{f(c_0(x)), ... , c_n(x))}{x - 1}$$
```python
for point, table in zip(points, self.tables):
                # boundary
                for constraint, bound in zip(table.boundary_constraints_ext(challenges), table.boundary_quotient_degree_bounds(challenges)):
                    eval = constraint.evaluate(point)
                    quotient = eval / \
                        (self.xfield.lift(self.fri.domain(index)) - self.xfield.one())
```

**Transition constraint**
transition constraint에는 point $X$, next_point $X_{next}$ 다 들어와야 evaluate 가능
- N: Table height
- $\omicron^{-1}$ 은 맨 마지막 행에 대한 Trace domain의 원소. 다음 행이 없기 때문에 Transition constraint가 만족하지 않으므로 분모에서 제외한다.
$$
\frac{f(c_0(x)), ... , c_n(x), c_0(\omicron x), ..., c_n(\omicron x))(X - \omicron^{-1})}{x^N - 1}
$$

**Terminal constraint**
마지막 행에 대해서만 성립하는 제약.
$$\frac{f(c_0(x)), ... , c_n(x)) - T}{x - \omicron^{-1}}$$
```python
# terminal
                for constraint, bound in zip(table.terminal_constraints_ext(challenges, terminals), table.terminal_quotient_degree_bounds(challenges, terminals)):
                    eval = constraint.evaluate(point)
                    quotient = eval / \
                        (self.xfield.lift(self.fri.domain(index)) -
                         self.xfield.lift(table.omicron.inverse()))
```

**Difference constraint**
서로 다른 두 칼럼이 첫번째 행에 대해서 같다는 제약.
$$\frac{f(c_0(x)), ... , c_n(x)) - g(c_0(x)), ... , c_n(x))}{x - 1}$$
```python
for arg in self.permutation_arguments:
                quotient = arg.evaluate_difference(
                    points) / (self.xfield.lift(self.fri.domain(index)) - self.xfield.one())
```

**Fiat-shamir**
1. base_tree.root()
	1. -> extension column의 random linear combination을 위한 challenges 샘플링
2. extension_tree.root()
3. terminals
	1. self.processor_table.instruction_permutation_terminal
	2. self.processor_table.memory_permutation_terminal
	3. self.processor_table.input_evaluation_terminal
	4. self.processor_table.output_evaluation_terminal
	5. self.instruction_table.evaluation_terminal
	6. -> weight_seed 샘플링
4. combination_tree.root()
	1. -> indices_seed 샘플링: FRI 검사할 인덱스를 뽑기 위한 랜덤 시드

### Table

**def interpolate_columns**
- randomizers: 다항식을 통해 노출되는 정보가 없게 하기 위한 랜덤 행
	- domain이 $\omicron$과 겹치지 않게 주의
	- x축은 $x = \omega^{2i+1}$ 로  잡아서 $\omega$ 의 짝수 제곱인 $\omicron$ 과 겹치지 않게 함.

**def extend**
기존 테이블에 extension column을 추가한다.

## The Programming Language: Brainfuck

Turing-complete. 명령어는 총 8개이다.
- `[` 는 현재 메모리 셀이 0 이면 대응하는 `]` 으로 점프. mv가 0이 아니면 `ip = ip + 2`.
- `]` 는 현재 메모리 셀이 0이 아니면 대응하는 `]` 으로 점프.
- `+` 현재 메모리 셀에 1을 더한다.
- `-` 현재 메모리 셀에서 1을 뺀다. 
- `<` 현재 메모리 포인터에서 1을 뺀다.
- `>`현재 메모리 포인터에서 1을 더한다.
- `.` 현재 메모리 셀의 값을 출력한다.
- `,` 현재 메모리 셀에 유저 입력을 저장한다.

**Prime Field Brainfuck**
기존 Brainfuck은 modulo 256을 사용하는데 여기서는 modulo $p = 2^{64} - 2^{32} + 1$를 사용한다. 따라서 p는 최대 메모리 셀의 개수, 최대 프로그램 명령의 개수이고 메모리에 저장되는 값은 $F_p$ 의 원소이다. 

**Brainfuck ISA**
Brainfuck은 그 자체로는 instruction set architecture(ISA)가 아니다.
왜냐하면 `[` 와 `]` 명령이 서로의 위치에 의존적이다. 따라서 `[` 와 `]` 다음에 jump 할 주소를 넣어주도록 컴파일해주자.

### Compiling Brianfuck Programs

**Pushdown automaton**
스택을 활용한 컴파일.
https://en.wikipedia.org/wiki/Pushdown_automaton

`c` 를 지금까지 출력에 쓴 기호의 총 개수라고 하자.
1. `[` 를 만나면
	1. `c`를 스택에 푸시한다. 
	2. `[` 와 placeholder `*` 를 출력한다.
2. `]` 를 만나면
	1. 스택에서 한 번 pop한다. 이 값을 `i`라고 하자.
	2. `i+1`에 있는 `*`를 `c+2`로 덮어쓴다.
	3. `]` 와 `i+2` 를 출력한다.
3. 다른 기호들은 출력에 그대로 쓴다.

예시
```
++>,<[>+.<-]
```

컴파일 과정 중 `[`, `]` 만 보자.
1. `]` 를 만났을 때
	1. 지금까지 5개를 출력했으므로 5를 스택에 푸시
	2. 인덱스 5에 `[`, 6에 `*` 를 출력
2. `]` 를 만났을 때
	1. 스택에서 5를 pop.
	2. 인덱스 11까지 썼으므로 현재 c = 12. 따라서 6에 있는 `*`를 14로 덮어쓴다. 
	3. `]` 와 `7` 을 출력한다.

컴파일 결과

| 0   | 1   | 2   | 3   | 4   | 5   | 6   | 7   | 8   | 9   | 10  | 11  | 12  | 13  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| +   | +   | >   | ,   | <   | [   | 14  | >   | +   | .   | <   | -   | ]   | 7   |

## Brainfuck VM

VM의 상태는 두 개의 레지스터와 메모리로 이뤄진다.
- ip: instruction pointer
- mp: memory pointer

VM은 전이 함수(state transition function)를 정의한다.
- `program[ip] == '['` 이면
	- `data[mp] == 0` 이면 점프. 즉 `ip = program[ip + 1]`
		- `program[ip + 1]` 의 의미: `[` 의 다음에는 목적 주소가 적혀있다.
	- 아니면, 목적 주소를 건너뛰어라. 즉 `ip = ip + 2`
- `program[ip] == ']'` 이면
	- `data[mp] != 0` 이면 점프. 즉 `ip = program[ip + 1]`
	- 아니면, 목적 주소를 건너뛰어라. 즉 `ip = ip + 2`
- `program[ip] == '<'` 이면 mp = mp - 1 and ip = ip + 1
- `program[ip] == '>'` 이면 mp = mp + 1 and ip = ip + 1
- `program[ip] == '+'` 이면 `data[mp] = data[mp] + 1` and ip = ip + 1
- `program[ip] == '-'` 이면 `data[mp] = data[mp] - 1` and ip = ip + 1
- `program[ip] == '.'` 이면 `data[mp]`를 출력 and ip = ip + 1
- `program[ip] == ','` 이면 `data[mp]`에 입력값을 저장 and ip = ip + 1

NOTE 
- binary operation이 없음. 예를 들어, `+` 에 operand가 없음

## Arithmetization of Brainfuck VM

**Registers**
- `clk` - clock. 현재까지 실행된 명령 수.
- `ip` - instruction pointer. `ci` 에 로드할 프로그램 주소.
- `ci` - 현재 명령. `ip` 위치의 프로그램 값
- `ni` - 다음 명령. `ip+1` 위치의 프로그램 값, `ip`가 마지막이라면 0.
- `mp` - memory pointer. `mv`에 로드할 메모리 주소
- `mv` - memory value. `mp` 에 위치한 메모리 값
- `inv` - inverse. `mv` 가 0이면 0, 아니면 `mv`의 곱셈 역원. 

**Tables**
- Memory Table 프로세서는 메모리를 읽고 쓴다.
- Instruction Table
- Input Table
- Output Table

![table-relations.svg](https://aszepieniec.github.io/stark-brainfuck/graphics/table-relations.svg)

### Processor Table
**구성**
- 7 base columns: 7 registers
- 4 extension columns: 다른 네 테이블과의 관계
	- `ipa`: Instruction Permutation
	- `mpa`: Memory Permutation
	- `iea`: Input Evaluation
	- `oea`: Output Evaluation
- $a, b, c, \alpha$: Instruction permutation의 random scalar
- $d, e, f, \beta$: Memory permutation의 random scalar
- $\gamma$: Input evaluation의 random scalar
- $\delta$: Output evaluation의 random scalar

제약을 만족하면 각 제약식은 0이 된다.

**Boundary constraints**
Base columns 
- `ci` 와 `ni` 를 제외한 레지스터들은 전부 0으로 초기화한다.
	- `clk - 0`, `ip - 0`, `mp - 0`, `mv - 0`, `inv - 0`
Extension columns
- `Instruction permuation`, `Memory permutation` 은 random initial이므로 제약 없음.
- `iea`, `oea`은 0으로 초기화.
	- `iea - 0`
	- `oea - 0`

**Transition constraints**
Disjunctive normal form: OR-of-ANDs
- OR은 제약 다항식의 곱셈, AND는 random coefficient를 이용한 일차 결합으로 표현 후 (제약 = 0)이 성립하도록 만든다.
- $A \rightarrow B$ 를 집합 기호로 표현하면 $\neg A \lor B$

**명령별 제약**
instruction deselector을 곱해서 제약이 특정 명령어에 대해서만 유효하게 만든다. 
$\mathsf{ci} = \varphi$ 인 경우에만 적용되게 할 때, 아래 식을 사용한다.
$$
\varsigma_\varphi(\mathsf{ci}) = \mathsf{ci} \prod_ {\phi \in \Phi \backslash \varphi} (\mathsf{ci} - \phi) \enspace
$$

ci = `[`
- 메모리 값이 0이면 점프, 0이 아니면 명령 포인터(ip) 2 증가: `(ip' - ip - 2) * mv + (ip' - ni) * iszero`
	- `iszero` 는 $1 - \mathsf{mv} \cdot \mathsf{inv}$ 식으로 `mv` 가 0일 때 1이 된다.
	- `ni` 는 다음 명령어고 컴파일할 때 점프할 위치를 넣어뒀다. 
- 메모리 포인터 유지: `mp' - mp`
- 메모리 값 유지: `mv' - mv`

ci = `]`
- 메모리 값이 0이 아니면 점프, 0이면 명령 포인터(ip) 2 증가: `(ip' - ip - 2) * iszero + (ip' - ni) * mv`
- 메모리 포인터 유지 `mp' - mp`
- 메모리 값 유지: `mv' - mv`

ci = `<`
- 명령 포인터(ip) 1 증가: `ip' - ip - 1`
- 메모리 포인터 1 감소: `mp' - mp + 1`
- 메모리 값은 제약 없음.

ci = `>`
- 명령 포인터(ip) 1 증가: `ip' - ip - 1`
- 메모리 포인터 1 증가: `mp' - mp - 1`
- 메모리 값은 제약 없음.

ci = `+`
- 명령 포인터(ip) 1 증가: `ip' - ip - 1`
- 메모리 포인터 유지 `mp' - mp`
- 메모리 값 1 증가: `mv' - mv - 1`

ci = `-`
- 명령 포인터(ip) 1 증가: `ip' - ip - 1`
- 메모리 포인터 유지 `mp' - mp`
- 메모리 값 1 감소: `mv' - mv + 1`

ci = `,`
- 명령 포인터(ip) 1 증가: `ip' - ip - 1`
- 메모리 포인터 유지 `mp' - mp`
- 메모리 값은 입력에서 가져오므로 제약 없음.

ci = `.`
- 명령 포인터(ip) 1 증가: `ip' - ip - 1`
- 메모리 포인터 유지 `mp' - mp`
- 메모리 값 유지 `mv' - mv`

instruction에 무관한 제약들
- clock이 1씩 증가:  `clk' - clk - 1`
- `inv * (1 - inv * mv)`
- `mv * (1 - inv * mv)`
	- 둘 다 필요한 이유: inv = 0 일 때 mv= 0 을 강제하기 위함

The transition constraints for the extension columns
1. The instruction permutation argument
	- $\mathsf{ci} \cdot ( \mathsf{ipa} \cdot (a \cdot \mathsf{ip} + b \cdot \mathsf{ci} + c \cdot \mathsf{ni} - \alpha) - \mathsf{ipa}^\star) + (\mathsf{ipa}^\star - \mathsf{ipa}) \cdot \prod_{\varphi \in \Phi} (\mathsf{ci} - \varphi)$
	- $\mathsf{ci} \in \Phi$ 일 때의 ip, ci, ni 칼럼은 instruction table과 순서만 다르다. 
2. The memory permutation argument
	- clk, mp, mv 칼럼이 memory table과 순서만 다르다.
	- $\mathsf{mpa} \cdot (d \cdot \mathsf{clk} + e \cdot \mathsf{mp} + f \cdot \mathsf{mv} - \beta) - \mathsf{mpa}^\star$
3. The input evaluation argument
	- evaluation argument 이므로 $\gamma$ 를 계속 곱하며 차수를 늘려간다.
	- $\varsigma_{‘,’}(\mathsf{ni}) \cdot (\mathsf{iea} \cdot \gamma + \mathsf{mv}) + (\mathsf{ni} - ',') \cdot \mathsf{iea} - \mathsf{iea}^\star$
		- instruction deselector $\varsigma$ 가 사용됨. ni가 `,`이면 더한다.
		- Q. 마지막 항이 $(iea - iea^*)$ 이렇게 괄호로 묶어야 하는 거 아닌가?
		- A. 아니다. $\mathsf{iea}^\star$ 를 우변에 넘기고 좌변이 $\mathsf{iea}^\star$ 와 같아야 한다는 제약으로 보면 더 잘 보인다.
1. The output evaluation argument
	- $\varsigma_{‘.’}(\mathsf{ni}) \cdot (\mathsf{oea} \cdot \delta + \mathsf{mv}) + (\mathsf{ni} - '.') \cdot \mathsf{oea} - \mathsf{oea}^\star$

**Terminal constraints**
1. $\mathsf{ipa} \cdot (a \cdot \mathsf{ip} + b \cdot \mathsf{ci} + c \cdot \mathsf{ni} - \alpha) - T_{\mathsf{ipa}}$
2. $\mathsf{mpa} \cdot (d \cdot \mathsf{clk} + e \cdot \mathsf{mp} + f \cdot \mathsf{mv} - \beta) - T_{\mathsf{mpa}}$
3. $\mathsf{iea} - T_{\mathsf{iea}}$
4. $\mathsf{oea} - T_{\mathsf{oea}}$

참고: Constraints는 구현 별로 조금씩 다름.
- https://github.com/aszepieniec/stark-brainfuck/blob/master/code/processor_table.py#L304
- https://github.com/andrewmilson/ministark/blob/main/examples/brainfuck/constraints.rs#L136

**Example: Processor Table**
가정
- $\beta = 3, d = e = f = 1$
- permutation argument init = 7

계산
- $prp_n = init \cdot \prod_{i=0}^n{(\beta - d \cdot \mathsf{clk} - e \cdot \mathsf{mp} - f \cdot \mathsf{mv})}$
- 2번째 행: $7 \cdot (3 - 1 - 0 -1)= 7$
- 3번째 행: $7 \cdot (3 - 2 - 0 - 2) = -7 = -7 +(2^{64} - 2^{32} + 1)$

| clk | ip  | ci  | ni  | mp  | mv  | mvi   | prp                  |
| --- | --- | --- | --- | --- | --- | ----- | -------------------- |
| 0   | 0   | a+  | a+  | 0   | 0   | 0     | 7                    |
| 1   |  1  | a+  | a>  |  0  |  1  | 1     | 7                    |
| 2   | 2   | a>  | a,  | 0   | 2   |  2⁻¹  | 18446744069414584314 |
| 3   | 3   | a,  | a<  | 1   | 0   | 0     | 18446744069414584342 |
| 4   | 4   | a<  | a[  | 1   | 97  | 97⁻¹  | 18446744069414584258 |
| 5   | 5   | a[  | 13  | 0   | 2   | 2⁻¹   | 18446744069414590684 |
| 6   | 7   | a>  | a+  | 0   | 2   | 2⁻¹   | 18446744069414546143 |
| 7   | 8   | a+  | a.  | 1   | 97  | 97⁻¹  | 18446744069414851567 |
| 8   | 9   | a.  | a<  | 1   | 98  | 98⁻¹  | 18446744069414851567 |
| 9   | 10  | a<  | a-  | 1   | 98  | 98⁻¹  | 18446744072360704225 |
| 10  | 11  | a-  | a]  | 0   | 2   | 2⁻¹   | 18446743754179754593 |
| 11  | 12  | a]  |  7  | 0   |  1  | 1     |  3467583127008       |
| 12  | 7   | a>  | a+  |  0  | 1   | 1     | 18446705926000187233 |
| 13  | 8   | a+  | a.  |  1  | 98  | 98⁻¹  |  4577209727650056    |
| 14  | 9   | a.  | a<  | 1   | 99  | 99⁻¹  |  1839593704143766310 |
| 15  | 10  | a<  | a-  |  1  | 99  | 99⁻¹  |  5741194161392097408 |
| 16  | 11  | a-  | a]  | 0   | 1   | 1     | 9586652100225931044  |
| 17  | 12  | a]  | 7   |  0  |  0  | 0     | 12634263021116362185 |
| 18  | 14  |  0  | 0   | 0   | 0   |  0    |  7659764256986325571 |
|     |     |     |     |     |     |       |  5425144832537830614 |

### Instruction Table
**구성**
- 3 bases columns: `ip`, `ci`, `ni`
- 2 extension columns
	- `ppa` processor permutation argument
	- `pea` program evaluation argument.
- a, b, c: permutation argument에서 base columns의 weight.
- $\alpha$: permutation argument의 random scalar.
- $\eta$: evaluation argument에서의 random scalar.

만드는 방법
1. program을 순회하며 (ip, ci, ni)를 채운다.
3. Processor Table의 패딩이 아닌 행들의 (ip, ci, ni) 를 한 번 복사해서 아래에 연결한다. 
4. `ip` 오름차순으로 정렬한다.

m을 해당 명령이 실행된 횟수라고 할 때, Instruction Table 내에서 각 명령은 m + 1번 반복된다.

제약의 의미
1. Processor가 program 에 적힌 (ip, ci, ni) 대로 실행한다.
2. 프로그램이 실행 도중 바뀌지 않는다.

**Boundary constraints**
- `ip` 는 0부터 시작한다.
	- `ip - 0`

**Transition constraints**
base column 제약
- `ip` 는 0 또는 1 증가
	- `(ip' - ip)(ip' - ip - 1)`
- `ip` 가 1 증가하면 이번 행의 `ni` 는 다음 행의 `ci'` 와 같다.
	- `(ip' - ip)(ni - ci')`
- `ip` 가 그대로 이면 `ci`도 그대로다.
	- `(ip' - ip - 1)(ci' - ci)`
- `ip` 가 그대로 이면 `ni` 도 그대로다.
	- `(ip' - ip - 1)(ni' - ni)`

extension column 제약
- 패딩 행은 ci = 0. 

The permutation argument
- $\mathsf{ci} \cdot (\mathsf{ip} + 1 - \mathsf{ip}^\star) \cdot (\mathsf{ppa}^\star - \mathsf{ppa} \cdot (a \cdot \mathsf{ip}^\star + b \cdot \mathsf{ci}^\star + c \cdot \mathsf{ni}^\star - \alpha))$
	- 패딩 행이 아니고 ip가 1 증가하지 않으면 permutation argument 누적
- $\left( \prod_{\varphi \in \Phi} \mathsf{ci} - \varphi \right) \cdot (\mathsf{ppa}^\star - \mathsf{ppa})$
	- $\Phi$ 는 instructions set
	- ci 가 instructions set의 원소가 아니라면 ppa는 그대로.
- $(\mathsf{ip} - \mathsf{ip}^\star) \cdot (\mathsf{ppa}^\star - \mathsf{ppa})$
	- ip가 변화하면 paa는 그대로.

The evaluation argument
다음 행에서 ip 가 바뀔 때만 evaluation argument
- $(\mathsf{ip}^\star - \mathsf{ip} - 1) \cdot (\mathsf{pea}^\star - \mathsf{pea} )$
- $(\mathsf{ip}^\star - \mathsf{ip}) \cdot (\mathsf{pea}^\star - \mathsf{pea} \cdot \eta - (a \cdot \mathsf{ip}^\star + b \cdot \mathsf{ci}^\star + c \cdot \mathsf{ni}^\star))$

**Terminal constraints**
- $ppa - T_{ppa}$
	- $T_{ipa} = T_{ppa}$ 이므로 prover에게 받은 $T_{ppa}$ 를 여기에도 사용
- $pea - T_{pea}$
	- $T_{pea}$ 는 Verifier가 직접 계산한다.

**Example: Instruction Table**

| ip  | ci  | ni  |
| --- | --- | --- |
| 0   | a+  | a+  |
| 0   | a+  | a+  |
| 1   | a+  | a>  |
| 1   | a+  | a>  |
| 2   | a>  | a,  |
| 2   | a>  | a,  |
| 3   | a,  | a<  |
| 3   | a,  | a<  |
| 4   | a<  | a[  |
| 4   | a<  | a[  |
| 5   | a[  | 13  |
| 5   | a[  | 13  |
| 7   | a>  | a+  |
| 7   | a>  | a+  |
| 7   | a>  | a+  |
| 8   | a+  | a.  |
| 8   | a+  | a.  |
| 8   | a+  | a.  |
| 9   | a.  | a<  |
| 9   | a.  | a<  |
| 9   | a.  | a<  |
| 10  | a<  | a-  |
| 10  | a<  | a-  |
| 10  | a<  | a-  |
| 11  | a-  | a]  |
| 11  | a-  | a]  |
| 11  | a-  | a]  |
| 12  | a]  | 7   |
| 12  | a]  | 7   |
| 12  | a]  | 7   |

### Memory Table

**구성**
- 3 base columns: `clk`, `mp`, `mv`
- 1 extension column: `ppa`
	- the permutation argument: Memory Table 과 Processor Table을 연결. 

**Boundary constraints**
- `clk = mp = mv = 0`
	- Processor Table 에서 동일한 제약이 있으므로 생략.
- `ppa` 에 대한 제약은 없음. Prover가 random 초기값을 하나 뽑기 때문.

**Transition constraints**
The base columns
- 메모리 포인터는 0 또는 1 증가
	- `(mp + 1 - mp')(mp - mp')`
- 메모리 포인터가 1 증가하면 새 메모리 값은 0
	- `(mp - mp')mv'`
- 메모리 포인터가 변하지 않고 사이클 카운트가 1 증가하면 메모리 값은 변할 수 있다.
	- `(mp - mp')(mv' - mv)`
		- 메모리 포인터가 변하면 메모리 값은 변하지 않는다.
	- `(clk - 1 - clk')(mv' - mv)`
		- 사이클 카운트가 1 증가하지 않으면 메모리 값은 변하지 않는다.    

The extension column
- `ppa`: a product argument
	- `ppa * (d * clk + e * mp + f * mv - beta) - ppa'`
	- d, e, f 는 각 칼럼에 대한 random weight.

**Terminal constraints**
The table has one terminal, $T_{ppa}$ sent by the prover.
Processor Table에서 $T_{mpa}$ 와 비슷한 기능.
마지막 행을 제외하고 모든 행의 `(d * clk + e * mp + f * mv - beta)` 를 곱한 값이 마지막 행의 ppa에 위치. 따라서 Terminal constraints 는 아래처럼 마지막 행을 곱해서 확인.
$\mathsf{ppa} \cdot (d \cdot \mathsf{clk} + e \cdot \mathsf{mp} + f \cdot \mathsf{mv} - \beta) - T_{\mathsf{ppa}}$

**Example: Memory Table**

| `clk` | `mp` | `mv` |
| ----- | ---- | ---- |
| 0     | 0    | 0    |
| 1     | 0    | 1    |
| 2     | 0    | 2    |
| 5     | 0    |  2   |
| 6     |  0   | 2    |
| 10    | 0    | 2    |
| 11    | 0    | 1    |
| 12    | 0    | 1    |
| 16    | 0    |  1   |
| 17    | 0    |  0   |
| 18    | 0    | 0    |
| 3     | 1    | 0    |
| 4     | 1    | 97   |
| 7     | 1    | 97   |
| 8     |  1   | 98   |
| 9     | 1    | 98   |
| 13    | 1    | 98   |
| 14    | 1    | 99   |
| 15    | 1    |  99  |

### Input and Output Table

구성
- Base column: `c`
- Extension column: `ea`

**Boundary constraints**
`ea - c`
해설: 첫 행에서 `ea`와 `c` 두 칼럼은 같다.

**Transition constraints**
$$\zeta \cdot ea + c' - ea'$$
해설
- Evaluation argument에 사용되는 challenge $\zeta$ 는 Input table에서의 $\gamma$, Output table에서의 $\delta$ 를 의미.
- 이번 행의 `ea` 에 $\zeta$ 를 곱하고 다음 행의 base column 에 있는 $c'$ 를 더하면 다음 행의 extension column $ea'$ 와 같다.

**Terminal constraint**
$T_{ea} - ea$
Terminal value는 prover가 보내지 않고 verifier가 계산한다. 

**Example: Input Table**
- ea: Evaluation Argument

| `input value` | `ea` |
| ------------- | ---- |
| 97            | 97   |

**Example: Output Table**
$\delta = 2$ 가정.

| `output value` | `ea`                     |
| -------------- | ------------------------ |
| 98             | 98                       |
| 99             | $98 \cdot 2 + 99 = 295$  |

### Difference Constraints

두 칼럼이 같은 값에서 시작함을 증명.
영지식성을 위해 Prover가 permutation argument에 쓰일 extension column의 초기값은 랜덤하게 잡는다. 그럼 비교하는 두 열의 초기값은 서로 같아야 3 * 2 * 4 = 6 * 4 * 1 처럼 두 열의 곱이 같다고 서로가 치환이라고 잘못 판단하지 않는다.

예를 들어, Processor Table의 `ipa` 칼럼과 Instruction Table 의 `ppa` 칼럼은 permutation argument 이다. 각 칼럼의 보간 다항식 $f_{ipa}(X), f_{ppa}(X)$ 는 첫번재 행에서 같다. $f_{ipa}(X) - f_{ppa}(X)$ 는 $X = o^{0} = 1$ 에서 0이어야 한다. 따라서 $X - 1$ 로 나누어 떨어진다.
즉, 몫 다항식은 $max(deg(f_{ipa}(X)), deg(f_{ppa}(X))) - 1$ 이하의 차수를 가짐을 증명해야 한다.

Processor Table 의 `mpa` 칼럼과 Memory Table의 `ppa` 칼럼도 마찬가지다.
$\frac{f_{\mathsf{mpa}}(X) - f_{\mathsf{ppa}}(X)}{X-1}$ 는 $\max(\deg(f_{\mathsf{mpa}}(X)), \deg(f_{\mathsf{ppa}}(X))) - 1$ 의 차수를 가짐을 보여야 한다.

## Attack 예시

내가 작성한 서킷의 soundness 체크
예시 공격
Memory value를 다른 값으로 바꾼다는 것은 balance를 바꿀 수도 있다는 것

프로그램
`+><.-><+` 

**Processor Table**
여기서 잘못된 것을 찾아보자.

| `clk` | `ip` | `ci` | `ni` | `mp` | `mv`  | `inv`         |
| ----- | ---- | ---- | ---- | ---- | ----- | ------------- |
| 0     | 0    | `+`  | `>`  | 0    | 0     | 0             |
| 1     | 1    | `>`  | `<`  | 0    | 1     | 1             |
| 2     | 2    | `<`  | `.`  | 1    | 0     | 0             |
| 3     | 3    | `.`  | `-`  | 0    | **2** | **2** $^{-1}$ |
| 4     | 4    | `-`  | `>`  | 0    | 2     | 2 $^{-1}$     |
| 5     | 5    | `>`  | `<`  | 0    | 1     | 1             |
| 6     | 6    | `<`  | `+`  | 1    | 0     | 0             |
| 7     | 7    | `+`  | 0    | 0    | 1     | 1             |
| 8     | 8    | 0    | 0    | 0    | 2     | 2 $^{-1}$     |


**Memory Table**

| `clk` | `mp` | `mv` |
| ----- | ---- | ---- |
| 0     | 0    | 0    |
| 1     | 0    | 1    |
| 5     | 0    | 1    |
| 7     | 0    | 1    |
| 8     | 0    | 2    |
| 3     | 0    | 2    |
| 4     | 0    | 2    |
| 2     | 1    | 0    |
| 6     | 1    | 0    |

**AIR constraints**
1. 첫번째 줄은 `ci`, `ni` 를 제외하면 전부 0이다.
2. 메모리 포인터 `mp` 는 0 또는 1 증가한다.
3. 메모리 포인터가 그대로라면 `clk` 는 점프하고 메모리 값 `mv` 는 그대로 유지되어야 한다.
	1. 1 -> 2 이렇게 clock cycle이 늘어나는 게 아니라  1 -> 5 이렇게 2이상 증가하는 경우에는 과거 `mp` 로 돌아가서 `mv` 도 같이 돌아오는 상황. 따라서 `mv` 가 직전 행의 값에서 변하면 안 된다.

문제는 clock cycle `clk`가 8에서 3으로 거꾸로 갔기 때문에 3번 제약을 지키더라도 미래의 `mv` 값을 과거의 `mv`에 넣을 수 있다.

### 정렬이 필요한 이유

Memory Table이 정렬되어 있다면 다음 두 가지 성질을 만족한다.
1. 같은 메모리 포인터에 대한 행들은 contiguous
2. 같은 메모리 포인터에 대한 행들은 clock cycle 오름차순으로 정렬되어 있다.

Memory Table 의 AIR constraints
- Boundary constraint
	- 첫번째 행은 전부 0이다.
- Transition constraints
	- `mv` 는 `clk`가 1 넘게 증가하는 행에서 변하지 않는다. 
	- `mp`가 변하면 다음 행의 `mv` 는 0이다.
- Transition constraints of the Processor Table
	- `mp` 가 그대로이고 $ci \notin \{+, - \}$ 이라면 `mv`는 변하지 않는다.

### Solution

The transition constraints for the base table
- 메모리 포인터 칼럼은 0 또는 1 증가한다.
	- `(mp' - mp) * (mp' - mp - 1)`
- 메모리 포인터가 같은 contiguous region에서, 클락 사이클 카운터는 1씩 증가한다.
	- 더미 row로 가능해짐.
	- `(mp' - mp - 1) * (clk' - clk - 1)`
- 메모리 포인터가 1 증가한다면 다음 메모리 값은 0이다.
	- 해석: 새로운 메모리 포인터로 바뀔 때 mv는 최초에 0.
	- `(mp' - mp) * mv'`
- The dummy next 는 0 또는 1이다.
	- `d' * (d' - 1)`
- 더미 row이면 메모리 값은 변하지 않는다.
	- `d * (mv' - mv)`
- 더미 row이면 메모리 포인터는 변하지 않는다.
	- `d * (mp' - mp)`

The transition constraints for the extension column: 
$$\mathsf{d} \cdot \mathsf{ppa} + (1 - \mathsf{d}) \cdot \mathsf{ppa} \cdot (d \cdot \mathsf{clk} + e \cdot \mathsf{mp} + f \cdot \mathsf{mv} - \beta) - \mathsf{ppa}^\star$$
해설
dummy row가 아닐 때만 permutation argument column에 곱해진다.
- d = 0 이면 $\mathsf{ppa} \cdot (d \cdot \mathsf{clk} + e \cdot \mathsf{mp} + f \cdot \mathsf{mv} - \beta) = \mathsf{ppa}^\star$
- d = 1 이면 $\mathsf{ppa} = \mathsf{ppa}^\star$

The terminal constraint
위의 transition constraint와 거의 같고 `ppa'` 만 $T_{ppa}$ 로 대체된다.
$$\mathsf{d} \cdot \mathsf{ppa} + (1 - \mathsf{d}) \cdot \mathsf{ppa} \cdot (d \cdot \mathsf{clk} + e \cdot \mathsf{mp} + f \cdot \mathsf{mv} - \beta) - T_{ppa}$$

## 참고
- [RISC Zero Developer Docs](https://dev.risczero.com/proof-system/stark-by-hand)
- [BrainSTARK, Part 0: Introduction | BrainSTARK](https://aszepieniec.github.io/stark-brainfuck/)
- 테이블 예시: [Brainfuck STARK Tutorial — Neptune](https://neptune.cash/learn/brainfuck-tutorial/)
- https://github.com/andrewmilson/ministark
- https://github.com/aszepieniec/stark-brainfuck