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.
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/.