## 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. 메모리 또는 표준 출력에 데이터를 쓴다.


테이블이 여러 개이다. 프로세서, 메모리, 프로그램, 입력, 출력.
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}$$

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}}$$

# 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}$$

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


### 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