What's Stark?

ZK 증명 시스템 구조 (공통된 큰 틀)
┌────────────────────────────────────┐
│   Arithmeticization                │ → 문제를 다항식으로 바꿈
├────────────────────────────────────┤
│   Commitment Scheme                │ → 다항식 or 증거를 커밋
├────────────────────────────────────┤
│   Low-Degree Testing / Constraints │ → 다항식이 "좋은 것"인지 확인
├────────────────────────────────────┤
│   Proof + Verification             │ → 증명 생성하고 검증
└────────────────────────────────────┘

단계	SNARK (ex. PLONK, Groth16)	STARK
표현	R1CS, Arithmetic circuits	Trace table → 다항식
커밋	KZG commitment, Merkle Tree	Merkle tree (RS-encoded)
LDT	Algebraic Consistency (PLONK), QAP	FRI (Reed-Solomon 기반)
증명	Groth16, PLONK proof 등	STARK proof (FRI 포함)

STARK란?

• Scalable Transparent ARgument of Knowledge
• SNARK와 비슷한 ZK proof이지만, trusted setup 없음 + 양자 내성

핵심 구조 :
1. 계산을 trace로 만든다.
2. trace -> 다항식으로 변환한다.
3. 이 다항식이 저차수라는 것을 증명한다 (FRI)
4. Merkle root로 다항식에 커밋하고, 일부 점만 검사한다.

계산 trace

Step	x	y
0	1	1
1	1	2
2	2	3
3	3	5
...

계산 과정을 위 처럼 정리하고, 이런 테이블을 각 컬럼마다 하나의 다항식으로 변환

• $f_1(x)$, $f_2(x)$, $\dots$
  즉 trace로 여러 다항식을 만든다.

저차수 다항식을 만드는 이유는

• 위의 다항식이 진짜 계산과정을 잘 담고 있는지 파악하려면, 너무 복잡하지 않은 다항식이 아니어야 함(검증 비용 때문)
• 그래서 이 다항식이 low-degree 다항식이라는 것을 증명해야함

여기서 아래 세가지 등장

• FRI : 다항식이 저차수인지 증명하는 프로토콜
• Reed-Solomon: 다항식을 오류 정정 가능한 코드로 만들기 위한 이론
• Split-and-Fold: FRI 효율 최적화 기법

FRI (Fast Reed-Solomon IOP of Proximity)

FRI는 STARK에서 다항식이 low-degree인지 증명하기 위한 핵심 프로토콜

역할 :

• 프로버가 "이건 degree ≤ d 짜리 다항식이야!" 라고 주장할 때,
• 검증자는 실제로 그렇다는 걸 소수의 점 샘플만으로 확인함.

어떻게 가능한가:

• 다항식을 Reed-Solomon 코드처럼 RS-encoding 하고,
• 그 다항식을 Merkle Tree로 커밋,
• 그 다음 여러번 차수를 줄이는 반복 과정 수행

이 반복 과정을 Split-and-Fold로 최적화

Split-and-Fold 기법

"여러 개의 constraint 다항식을 하나로 합쳐서 검증하자."

• 원래는 여러 개의 다항식:
  $f1(x),f2(x),f3(x),…,fk(x)$
  
• 이걸 하나의 folded polynomial로 만든다:
  $folded(x)=α1f1(x)+α2f2(x)+…+αkfk(x)$
  
• 각 $alpha_i$​는 난수 (verifier가 선택함)
  → 그러면 $f_{\text{folded}}$​이 low-degree라면, 각각도 low-degree일 확률이 높음 (Schwartz-Zippel)

Split 단계

1. 각 constraint는 서로 다른 도메인, degree, 조건일 수 있음
2. 예를 들어, 하나는 main trace 위에서, 하나는 shifted trace 위에서 동작함
3. 이걸 각각 비슷한 도메인 구조로 normalize
   • → 동일한 coset으로 mapping
   • → 동일한 evaluation domain

Fold 단계

모든 다항식을 하나의 다항식으로 합친다 :

Folded_P(x) = α₁·P₁(x) + α₂·P₂(x) + ... + α_k·P_k(x)

• 여기서 각 alpha_i 가 랜덤하게 고른 challenge
• 이 구조는 interactive proof에서 효율적으로 검증 가능

1. f(x) -> 짝수/홀수 계수로 나눔 (Split)
2. $f_{even}(x^2)$ + $x * f_{odd}(x^2)$ -> 새로운 낮은 차수의 다항식 (Fold)
3. 이걸 반복하면서 점점 다항식 줄임

Redd-Solomon과 Split-and-Fold가 전부 FRI에 포함되는 최적화 기법임

STARK 프로토콜 전체 흐름
├── Trace 생성
├── AIR Constraint → Quotient Polynomial들
│   ├── Quotient_1(x), Quotient_2(x), ...
│   └── 👉 Split-and-Fold 적용
├── 하나의 Folded Polynomial → Low-degree 증명 (FRI)

AIR

AIR = "알고리즘을 다항식으로 바꾸는 중간 표현"
STARK에서의 R1CS 또는 PLONK의 Gate system에 해당

AIR 구성
├── Trace Table (계산 상태)
├── Transition Constraints (시간 흐름 규칙)
├── Boundary Constraints (초기/최종 조건)
└── Public Inputs/Outputs

동작 방식
1. 프로그램 실행 결과 → Trace로 구성
2. 규칙(Constraints) 정의 → 다항식화
3. 전체 다항식이 low-degree → FRI로 증명

Trace Table

• 상태 변화의 시간에 따른 스냅샷
• 각 열(Column) = 하나의 변수 (ex. 레지스터, 스택, 메모리)
• 각 행(Row) = 시간 단위 (timestep)

예: 피보나치 계산 (x[n+2] = x[n+1] + x[n])

| t | reg0 | reg1 |
|---|------|------|
| 0 |   1  |   1  |
| 1 |   1  |   2  |
| 2 |   2  |   3  |
| 3 |   3  |   5  |
| 4 |   5  |   8  |

Transition Constraints

• 시간 t에서 t+1로 갈 때 지켜야 하는 관계식
• 이걸 다항식 형태로 정의함

reg0[t+1] = reg1[t]
reg1[t+1] = reg0[t] + reg1[t]
↓
(transition constraint 다항식 형태):
    f₀(x⋅g) - f₁(x) = 0
    f₁(x⋅g) - f₀(x) - f₁(x) = 0

여기서 x는 시점이고, g는 도메인 상의 primitive root (시간 이동)

Boundary Constraints

• 특정 시간에 값이 고정되어야 할 조건(입출력 조건)

예: reg0[0] = 1, reg1[0] = 1
    reg0[0] - 1 = 0
    reg1[0] - 1 = 0

Public Inputs & Outputs

• 외부로부터 주어진 값들, 증명자가 증명할 대상
• boundary constraint와 유사하게 처리됨

Constraint 다항식 정의 방식

AIR의 핵심은:

"trace가 주어진 규칙을 만족하는지"를
다항식들이 low-degree인지 확인함으로써 증명하는 것

이때 각 constraint를 다음과 같이 표현함:

코드 복사

P(x) = transition_constraint(x) * mask(x)

• mask(x)는 특정 점에서만 0이 아닌 다항식
• 전체 합쳐서 하나의 큰 다항식 P(x) 만듦

→ 이 P(x)가 실제로 low-degree인지 FRI로 증명하면 끝

예시: 피보나치 AIR

Trace

• 2개의 레지스터: x[n], x[n+1]

Transition Constraints

f₀(x⋅g) = f₁(x) f₁(x⋅g) = f₀(x) + f₁(x)`

(이 두 식이 전체 domain에서 만족되면 OK)

Boundary Constraints

f₀(1) = 1 f₁(1) = 1`