Halo2

참고 :
https://erroldrummond.gitbook.io/halo2-tutorial/section-1/chips-fish-sold-separately

목적

증명 가능한 계산 시스템을 만들기 위해, 아래를 달성해야함 :

• 회로의 구조 정의
• 회로에 값을 넣음
• 회로가 조건을 만족하는지 확인
• 나중에 그 회로에 대해 proof를 생성하고 검증

전체 구조 흐름

Config 정의 → Chip 구조체로 감싸기 → Trait로 연산 게이트 정의 → Layouter로 값을 할당 → Circuit으로 synthesize → Prove

• Config : 어떤 열들(column)이 필요한지 정의
• Chip : 계산 단위의 회로 기능 묶음
• Trait : 실제 계산 정의(gate)
• Layouter : 회로의 실제 layout과 값 할당 방식 정의
• Circuit : 회로 전체를 synthesize로 연결하고 구성
• MockProver : 실제 증명 시뮬레이션 도구

1. Config : 회로의 '부품' 정의

• 전체 회로에서 어떤 열(Column)이 필요한지 정의
• 열의 타입에 따라 용도가 다름:

컴포넌트	목적
Column<Advice>	witness (private input, wire) (= 증명 과정 중 채워지는 값들)
Column<Fixed>	컴파일 타임에 고정된 상수 또는 selector (게이트 활성화 여부)
Column<Instance>	공개 입력값
Selector	Fixed의 특수 버전으로, 특정 행(row)에만 제약조건을 활성화

#[allow(non_snake_case, dead_code )]
#[derive(Debug, Clone)]

struct TutorialConfig {
	l: Column<Advice>,
	r: Column<Advice>,
	o: Column<Advice>,

	sl: Column<Fixed>,
	sr: Column<Fixed>,
	so: Column<Fixed>,
	sm: Column<Fixed>,
	sc: Column<Fixed>,
	PI: Column<Instance>,
}

🔗 왜 필요 한가?

• 증명 시스템은 각 행에 대해 어떤 열들이 어떤 조건을 만족하는지 계산해야 하므로, 형식을 정하고 열들을 구분해서 관리해야 함

2. Chip : 기능 단위의 회로 패키지

• 하나의 Config를 감싸는 구조체
• 타입 시스템을 위한 마커 PhantomData<F>를 포함

struct TutorialChip<F: FieldExt> {
	config: TutorialConfig,
	marker: PhantomData<F>,
}

🔗 왜 필요 한가?

• 여러 종류의 계산 기능을 모듈처럼 분리하고, 타입별로 맞게 구성하기 위함
• 이를 통해, 재사용성/확장성 높은 회로 구성 가능

3. Trait: 계산(게이트) 로직을 정의

• Chip에서 지원하는 연산들을 trait로 정의 (보통 하나의 함수 = 하나의 게이트)
• ex : l⋅sl + r⋅sr + l⋅r⋅sm − o⋅so + sc + PI = 0

pub trait TutorialComposer<F: FieldExt> {
	fn add_gate(...);
}

🔗 왜 필요 한가?

• 여러 게이트 종류들을 추상화된 인터페이스로 정의하여, 다양한 chip에서 공통적으로 적용 가능
• 특정 구조에 묶이지 않고, 다양한 기능의 회로 설계 가능

4. Layouter: 회로에 값 할당

• 실제로 열에 값을 집어넣는 역할
• 논리 구조 단위로 assign_region() 사용
• Region::assign_advice, assign_fixed, enable_selector 등으로 실제 물리적인 값 넣음

🔗 왜 필요 한가?

• 구조에 값을 집어 넣어야 제약이 만족되는지 검증 가능
• Layouter를 통하여 구조에 따른 실제 작동을 가능하게 함

5. Circuit: 전체 회로 조립

• 위 모든 내용 조립
• Circuit<F> Trait을 구현 -> configure(), synthesize() 필요

impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
	fn configure(cs: &mut ConstraintSystem<F>) -> Self::Config { ... }
	fn synthesize(&self, cs: &mut impl Layouter<F>) -> Result<(), Error> { ... }
}

🔗 왜 필요 한가?

• configure는 static한 회로 구조를 정의
• synthesize는 실제 증명 시 이 회로가 어떻게 작동할지를 정의

6. Proof & MockProver: 동작 확인 or 실제 증명

• MockProver → 로컬 테스트용으로 constraint 만족 여부 확인
• Prover → 실제 증명 생성

let prover = MockProver::run(k, &circuit, vec![...])?;
prover.assert_satisfied();

1. int k를 생성하고, 값을 할당.
   • k는 서킷의 사이즈 의미
   • columns안의 rows의 개수가 2^k보다 작다는 것을 의미
2. circuit struct안에 들어갈 값을 초기화.(= Circuit에 입력할 값 준비)
3. MockProver::run()으로 증명 실행
4. .assert_satisfied()로 constraint 충족 여부 확인

🔗 왜 필요한가?

• 우리가 정의한 회로 구조가 논리적으로 맞는지 확인

Halo2 vs 디지털 시스템 설계

단계	반도체 설계 (디지털 논리 회로)	Halo2 회로 설계	공통 개념 (설계 레벨)
1️⃣ 구조 정의	Gate-Level 설계: NAND, AND, XOR 조합으로 회로 구성 (Verilog module로 표현)	Config: Advice, Fixed, Instance 열 정의	Gate-level abstraction
2️⃣ 기능 모듈화	Module wrapping: 작은 기능 단위로 모듈화 (ex. ALU, MUX)	Chip: config를 감싸고 타입화	모듈 단위로 기능 분리
3️⃣ 기능 명세	always 블록/assign 문로 로직 명세	Trait: 각 게이트 함수 정의 (예: add_gate)	동작(연산) 명세
4️⃣ 레이아웃 생성	배선 및 시뮬레이션 준비: 파형 시뮬레이션 위한 testbench / value assignment	Layouter: 값 할당, selector 활성화	Netlist-level wiring & simulation
5️⃣ 전체 회로 생성	Top module + 하위 모듈 연결	Circuit 구조체: configure() + synthesize()	구조적 설계 / 회로 전체 연결
6️⃣ 검증	시뮬레이션 (ModelSim, Vivado) 또는 Formal Verification	MockProver로 constraint 만족 확인	기능적 검증
7️⃣ 구현	Synthesis (gate-level netlist 생성) → Place & Route → Netlist,GDSII 생성	Prover → Proof 생성 → On-chain 검증기(zkProof(verifiable output))	실제 실행 가능한 아티팩트 생성
8️⃣ 테스트 벡터	Testbench에서 다양한 입력 케이스 검증	MockProver input으로 다양한 케이스 테스트	테스트 벡터 생성 및 검증

반도체: verilog로 AND 게이트

module and_gate (
  input wire a, b,
  output wire y
);
  assign y = a & b;
endmodule

-> vivado로 컴파일하면, synthesis -> netlist -> place & route -> 검증 순으로 진행

Halo2: Add Gate 구성

trait TutorialComposer<F: FieldExt> {
	fn add_gate(...) {
	  // l⋅sl + r⋅sr − o⋅so = 0 형태의 제약 정의
	}
}

-> 이걸 기반으로 MockProver로 테스트, 실제 Prover로 proof 생성

Halo2를 하드웨어 적으로 상상하면?

• Advice column = 전선(wire)

• Row = 한 시점(time step) 또는 gate 인스턴스

• Fixed column = 전압을 항상 1로 고정한 신호선 (즉 selector 역할)

• Selector = AND 게이트의 enable 핀이라고 보면 됨

• assign_advice = 입력 값을 버퍼에 적재

• enable_selector = 이 row에서만 연산 작동하도록 하는 컨트롤 신호

• circuit 구조체 = Top module

cell

• 셀은 작성 중인 값 테이블의 단일 위치를 나타냄
• 값을 보유하는게 아니라 어느 행을 참조할지를 나타내는 포인터를 보유함

https://www.youtube.com/watch?v=60lkR8DZKUA

Building and Testing Circuits

• n(2^k) rows, m columns
• cell의 value는 finite field에 있음
• 각 컬럼 i에 대해 Lagrange polynomial $a_i(x)$생성
• 그리고 row j에서, w = nth root of unity인 cell $A_{(i,j)}= a_i(w^j)$가 된다

• 커스텀 게이트는 r1cs 와 다르게 linear x linear로 표현되지 않아도 된다.
• 그래서 selector 하나를 가지고 instance columns, advice columns등의 여러 열을 조합 가능함.
  -> 따라서 더 유연한 게이트 설계가 가능하다!

---

Circuit에서 import되는 라이브러리 정리

arithmetic::FieldExt

• finite field와 관련된 연산을 처리하는 타입

circuit::{Layouter, SimpleFloorPlanner, Value}

• Layouter : 회로의 레이아웃 정의, 각 단계에서 필요한 데이터를 어떤 방식으로 배열할 지 결정(회로 구조 계획)
• SimpleFloorPlanner : 레이아웃 간단하게 설정할 수 있게 함
• Value : 주어진 유한체의 값을 래핑할 수 있는 타입으로, 해당값이 known인지 unknown인지 나타낼 수 있다.(중간 값, 입력 값 저장)

plonk::{Circuit, ConstraintSystem, Error}

• Circuit : 회로의 구조를 정의하는 추상화, 회로가 어떤 방식으로 계산될지 정의
• ConstraintSystem : 회로의 제약 조건을 정의하는 구조, 입력 값과 중간 계산 결과에 대한 제약 설정. 제약 조건을 통해 각 입력이 올바르도록 보장

std::marker::PhantomData

• 제네릭 타입의 빈 데이터 타입을 선언하기 위한 것
• 메모리를 차지하지 않지만, 타입 시스템에서 타입 정보를 유지하는데 사용됨

To be countinued
1. 라이브러리 모아서 다른 편으로 연재
2. Circom vs Halo2 차이점 정리 후 연재(HDL vs zk 회로 언어)
3. 반도체와 Halo2 차이 정리 후 따로 연재
4. Halo2 + STARK 구조의 비교: STARK은 왜 HDL 스타일에 더 잘 맞는가?