Halo2 <> ZK DSL <> HDL

jaewon·2025년 6월 30일

“Synthesis” in zk-Proof = 메타포로서의 “컴파일”

디지털 회로에서의 Synthesis

행위: HDL(예: Verilog/VHDL)로 작성한 추상적인 동작(behavioral description)을 논리 게이트 수준으로 내려서 물리적으로 실현 가능한 회로로 바꿈.
결과: 논리 게이트, 플립플롭 등의 게이트 레벨 넷리스트(netlist)가 생성됨.
의미: 고수준 설계를 저수준 하드웨어로 ‘구현’ 가능한 형태로 내림.

zk 시스템에서의 Synthesis

행위: 추상적인 제약 조건 정의(logic + constraints)를 실제 열(column)과 셀(cell) 기반의 회로에 매핑하고, 해당 회로가 어떤 witness를 요구하는지 지정함.
결과: 증명자가 어떤 값(witness)을 채워야 하는지, 제약이 어떻게 적용되는지 결정됨 → proving system에 입력될 수 있는 형태의 회로 “구현”됨.
의미: 제약 조건 = “논리 회로”, witness = “입력값”, 회로 전체 = “ZK용 정적 시스템”.
즉, ZK에서의 synthesis는 "logic → constraints → assign → proof 가능한 회로"로의 컴파일 단계라고 볼 수 있음. Circom이나 Halo2나 Noir 등 DSL들도 이 논리 흐름을 공유함.

ZK DSLs vs Halo2: HDL vs Constraint-Oriented

항목	HDL (예: Verilog)	ZK DSL (Circom, Noir 등)	Halo2
기본 설계 단위	신호(signal), 모듈(module)	회로(circuit), signal	trait, config, chip
회로 표현 방식	타이밍 기반 (클럭, 상태)	연산과 제약 기반	PLONK 제약 시스템 기반
추상화 수준	low-level (RTL)	중간 수준 DSL	low-level + Rust 기반 embedded DSL
Synthesis 대상	실제 하드웨어 회로	증명 가능한 회로 구조	Column/Cell 구조의 증명 회로
유저 난이도	전기전자 지식 필요	쉬움 (Noir), 중간(Circom)	매우 높음 (Rust ownership, PLONK 구조까지 이해 필요)
실제 proof 시스템 연동	FPGA/ASIC 설계	STARK/PLONK 시스템과 연동	PLONK/Halo2 백엔드 연동

핵심 차이

Circom, Noir → DSL을 통한 추상화된 설계
Halo2 → 회로 생성 + proving까지 다뤄야 하며 매우 low-level
Noir, Circom → 일반 개발자 친화적. HDL에 가까움.
Halo2 → Verilog보다 하드코어한 메커니즘 기반, “회로를 구성하는 언어”가 아니라 “증명 시스템 최적화 관점의 도구”

Halo2 vs STARK 시스템 (Cairo, zkWasm 등): 왜 STARK이 HDL 스타일과 더 맞는가?

항목	Halo2 (PLONK 기반)	STARK (Cairo, zkWasm 등)
회로 모델	고정 열 기반 수학적 제약 모델	실행 추적(trace table) 기반
설계 방식	명시적으로 열(column)을 지정하고 gate를 정의	프로시저/상태 기반으로 “코드를 실행하고 trace를 생성”
적합한 패러다임	수학적 추상화 → ZK 전문가용	VM-like 추상화 → 범용 프로그래머 친화적
구조 유연성	낮음 (열 기반 설계이므로 구조 바꾸기 어렵다)	높음 (프로그램 = 상태 변화, loop 등 자유로움)
HDL 유사도	낮음 (Verilog보다 수학적으로 복잡함)	높음 (Cairo는 Verilog처럼 상태 기반, execution trace 생성이 핵심)

핵심

STARK system은 “실행 → 기록 → 증명” 구조라서 HDL에서의 “시간에 따른 상태 변화”와 유사함
```
	- 상태기계 + 메모리 추적 → HDL과 매우 유사 (Cairo ≈ Verilog)
```
반면, Halo2는 수학적으로 gate 구성, column layout, selector 활용 등... HDL의 “구조”보다 “수학적 동치”에 초점.

HDL (Verilog/VHDL)
└── 설계 → Synthesis → 넷리스트 → 회로 제작

ZK 회로 설계
├── Circom/Noir (HDL 유사 DSL)
│   └── logic → constraints → compile → proving
├── Halo2 (PLONK 기반)
│   └── column 정의 → trait로 gate 정의 → layout → synthesize
└── STARK 계열 (Cairo, zkWasm)
    └── 실행 흐름 기록(trace) → AIR/FRI → proof

ZK에서의 Synthesis ≈ DSL을 증명 가능한 회로로 “컴파일”

왜 수학적 동치는 Halo2의 핵심인가?

ZK-SNARK 회로의 최종 목표
- ZK 회로는 결국 수학적 제약을 만족하는 입력(witness)이 존재한다는 것을 증명해야 함.

	-이 말은 회로가 수행하는 모든 연산, 상태 변화, 조건 등이 수학적 다항식(polynomial constraints) 형태로 정리되어야 한다는 뜻임.

즉, 회로 설계는 아래처럼 바뀜:
기존에는:
if (a > b) then x = 1 else x = 0 (논리적 표현)

Halo2에서는:
x ⋅ (a - b) ⋅ s = 0 같은 수학적 제약으로 바뀜
(여기서 s는 selector, 특정 위치에서만 제약이 적용됨)

그래서 Halo2에서 가장 중요한 건 연산을 정확히, 누락 없이 수학적 제약으로 매핑하는 것임. 이게 “수학적 동치”가 중요한 이유.

Halo2는 어떤 구조 때문에 수학에 집중할 수밖에 없을까?

Fixed-Column-Based Design (PLONK-style constraint system)
회로를 구성하는 기본 단위가 “행렬”이야. 예:

advice column: 증명자가 채우는 입력
fixed column: 미리 정해진 상수
selector column: 어떤 제약을 활성화할지 결정

이 column 기반 구조는 단순한 구조처럼 보이지만, 실제로는 복잡한 수학 연산을 column의 행(row)들 간 관계로 표현하는 게 핵심.

Custom Gate, Permutation, Lookup Table 지원
Halo2는 다음을 지원해서 회로를 수학적으로 효율화함:

custom gate: 복잡한 연산을 하나의 제약으로 압축
lookup table: 비선형 연산이나 조건 분기를 수학적으로 간단하게 표현
permutation: copy constraints를 다항식으로 바꿔주는 수학적 기법

📌 이 모든 것들이 “추상적인 동작”보단 “수학적으로 동치인 제약”을 어떻게 효율적으로 만들지를 고민하게 함.

왜 Verilog 같은 HDL 방식 대신 이걸 택했을까?

HDL 기반 접근의 한계:
시간 기반 상태 변화 (e.g. posedge clk)는 실제 하드웨어에서는 유효하지만, ZK 회로에서는 각 시간 상태가 수학적으로 검증 가능해야 함.
예를 들어 if-else는 ZK 회로에서는 직접 사용할 수 없음. 모든 분기마다 “모든 경우의 수”가 회로에 포함되어야 함.
Halo2처럼 수학 중심으로 짜면:
모든 연산, 상태 변화, 조건 분기 등이 한꺼번에 다항식으로 포착됨.

→ 증명 생성 시 GPU나 수학적 연산 최적화가 쉬워짐.

→ 증명 크기 작고 빠름, 보안성 검증 용이.

Permutation Argument (copy constraint를 다항식으로 바꾸는 방법)

Permutation argument는 “이 셀의 값은 저 셀의 값과 같아야 한다”는 copy constraint를 다항식 제약식으로 바꾸는 기술.
즉, 값이 서로 동일하다는 걸 "값들의 순열 관계가 같다"는 관점으로 재구성 하는 것.

왜 필요할까?
zk 회로에서는 값을 직접 복사할 수 없음.
대신 “A 위치의 값 = B 위치의 값”을 수학적으로 증명해야 함.

어떻게 증명하냐?

각 advice column의 셀 위치와 값을 (index, value) 쌍으로 정렬.

특정 "copy" 관계가 있다면, 그 두 셀의 쌍이 서로 순열 관계(permutation)에 포함되어 있어야 함.

이를 위해 permutation polynomial을 만들고, 실제 값들의 순열과 비교함.

디지털 회로와 비교

디지털 회로에서는 wire1 = wire2처럼 단순히 연결하면 되지만,

Halo2에서는 이게 보안적으로 중요해서, 직접 연결하는 대신 값 복사를 “수학적으로 증명”해야 함.

Lookup Argument (조건 분기나 비선형 연산을 다항식으로 단순화)

개념 요약
Lookup argument는 "어떤 값이 미리 정의된 테이블 안에 존재함"을 증명하는 방식.
이게 수학적으로도 간단하고, 비선형 또는 분기 로직을 매우 깔끔하게 다룰 수 있음.
왜 유용한가?
zk 회로는 비선형 연산, 조건 분기에 약함. (이걸 다항식으로 표현하기가 어려움)
```
예: if x == 3 then y = 7 else y = 9 → 분기!
```

이걸 lookup table로 바꾸면 단순한 "값 포함 여부" 체크로 바뀜.

어떻게 작동하냐?
테이블 (예: { (3, 7), (4, 9), ... })을 정의

회로 내에서 (x, y) 값이 테이블 안에 존재함을 증명

이 증명도 다항식으로 처리 가능함

수학적으로 보면?
“값이 테이블에 있다”는 것은 일종의 집합 포함 관계

이를 permutation argument와 유사한 방식으로 정리해서 polynomial identity로 바꿔줌

디지털 회로와 비교
디지털 회로에서는 LUT(Lookup Table)으로 조건 분기를 처리하지?

예: ROM 같은 형태로 “입력 → 출력” 매핑
Halo2에서도 비슷한 원리지만, 실제 메모리를 쓰는 대신 "테이블 내 포함 여부를 수학적으로 증명".

구분	Permutation Argument	Lookup Argument
목적	값 동일성 증명	값 포함성 증명
대상	Copy constraints	조건 분기, 비선형 연산
표현 방식	순열 (permutation)	테이블 안에 포함 여부
디지털 회로 대응	wire 연결	LUT (ROM)