Arithmetization — R1CS, AIR, and PLONKish TODO
Concept
Arithmetization is the step that turns the claim "this program executed correctly" into a polynomial constraint-satisfaction problem over a finite field — it's the first gate every ZK proof system passes through. R1CS expresses a computation as a set of constraints of the form A·z ∘ B·z = C·z, where z is a vector holding the public inputs and the witness, and each constraint corresponds to one multiplication gate; the representation is simple, but the constraint count grows in proportion to the number of multiplications. AIR views the computation as an execution trace table and expresses it through transition constraints — what must hold between two adjacent rows — plus boundary constraints; this fits VM execution, where the same operation repeats, especially well, making the constraint description very compact. PLONKish is an arithmetization built on a table of columns and rows, layered with arbitrary-degree custom gates, copy constraints (a permutation argument) that force different cells to be equal, and lookup arguments — its big advantage is that expensive operations like bit manipulation can be replaced with lookups into a precomputed table. The three approaches have comparable expressive power, but differ in circuit size, proving time, and setup requirements, so the real-world choice depends on the shape of the target computation.
In a ZK system, proving cost is mostly determined by how large the circuit grows at the arithmetization stage, so the same logic can be practical or not depending on which arithmetization it's compiled into.
Code & Formula
# 산술화 — R1CS·AIR·PLONKish
# y = x^3 + x + 5 (x=3 -> y=35) 를 R1CS 제약 A·z ∘ B·z = C·z 로 평탄화해 검증한다.
# witness 벡터 z = [1, out, x, sym1, y] (0=상수, 1=공개출력, 2=입력, 3~4=중간값)
IDX = {"one": 0, "out": 1, "x": 2, "sym1": 3, "y": 4}
N = len(IDX)
def row(**coeffs):
r = [0] * N
for name, c in coeffs.items():
r[IDX[name]] = c
return r
# 제약 1: x * x = sym1
# 제약 2: sym1 * x = y
# 제약 3: (y + x + 5*one) * one = out
A = [row(x=1), row(sym1=1), row(y=1, x=1, one=5)]
B = [row(x=1), row(x=1), row(one=1)]
C = [row(sym1=1), row(y=1), row(out=1)]
def dot(r, z):
return sum(a * b for a, b in zip(r, z))
def check_r1cs(z):
for a, b, c in zip(A, B, C):
if dot(a, z) * dot(b, z) != dot(c, z):
return False
return True
x = 3
sym1 = x * x
y = sym1 * x
out = y + x + 5
z = [1, out, x, sym1, y]
print("witness z =", z)
print("R1CS 제약 3개 모두 만족:", check_r1cs(z))
bad_z = z.copy()
bad_z[IDX["out"]] += 1 # 결과를 조작하면
print("조작된 out 은 거부됨:", not check_r1cs(bad_z))
docs/code/algorithms/algorithms-91.py
Exercise
Take a small expression like x^3 + x + 5 = 35 and flatten it into R1CS constraints by hand — write out the A, B, C matrices and the witness vector yourself — then express the same computation as transition constraints between two rows (AIR).
Practical Connection
When evaluating a design where order matching or settlement in a prediction market is computed off-chain and only the result is posted on-chain as a proof, you need to know how expensive operations like comparisons and division are inside a circuit to judge the break-even point against doing the computation on-chain.
Where it lands in Jayverse
- Verex: name the arithmetization before scoping any off-chain settlement PoC. PLONKish with lookups suits bit-manipulation-heavy order matching, AIR suits repeated per-order transition logic — write down which one and why before estimating constraint counts.
- Devnet: run the break-even check with real constraint counts. Compare proving k orders in one batch against posting them on-chain directly, using actual R1CS/AIR constraint counts from a devnet PoC, not an estimate.
- Auditor: treat a lookup table as an audited artifact. PLONKish lookups move correctness risk from constraint count to precomputed-table correctness, so any settlement circuit using lookups needs its table reviewed as its own item.
Key expressions
| Expression | 뜻 · 쓰이는 자리 |
|---|---|
| passes through | ~을 통과하다 · 모든 시스템이 거쳐야 하는 관문을 말할 때. "the first gate every ZK proof system passes through" |
| grow in proportion to | ~에 비례하여 늘어나다 · 크기가 다른 값에 정비례해서 증가할 때. "the constraint count grows in proportion to" |
| fit ... well | ~에 잘 들어맞다 · 특정 구조가 특정 상황에 적합할 때. "this fits VM execution, where the same operation repeats" |
| layered with | ~이 겹겹이 쌓인, ~으로 층을 이룬 · 여러 기능이 위에 덧붙여질 때. "layered with arbitrary-degree custom gates" |
| break-even point | 손익분기점 · 어느 지점부터 이득이 되는지를 가리킬 때. "judge the break-even point against doing the computation on-chain" |
| flatten (into) | ~로 풀어 헤치다, 단순화하여 펼치다 · 복잡한 식을 기본 제약식으로 분해할 때. "flatten it into R1CS constraints by hand" |
| comparable (expressive power) | 비슷한 수준의 표현력 · 서로 대등하게 견줄 만할 때. "The three approaches have comparable expressive power" |
| R1CS | 순위-1 제약 시스템(Rank-1 Constraint System) · A·z∘B·z=C·z 형태로 계산을 표현하는 ZK 산술화 방식. "R1CS expresses a computation as a set of constraints" |
| AIR | 대수적 중간 표현(Algebraic Intermediate Representation) · 실행 트레이스 테이블로 계산을 표현, VM 실행에 특히 적합. "AIR views the computation as an execution trace table" |
| PLONKish | PLONK 계열 산술화(테이블 기반 커스텀 게이트·룩업 지원 방식) · 비트 연산 등을 룩업 테이블로 대체 가능. "PLONKish is an arithmetization built on a table" |
If you study this on a given day, add a note link and a ✅ to this line in the source curriculum (docs/knowledge/dev-100-curriculum.md) and this spot will lead straight to the note body. You can also write directly on this page — but regenerating overwrites it, so it's safer to keep anything you want to save as markdown under docs/algorithms/.