안녕하세요, 이전 시간에는 영지식 회로 (zero-knowledge circuit)을 만들 수 있는 프로그래밍 언어 Circom 의 사용 방법에 대하여 알아보았습니다. 이번 시간에는 PLONK 기반의 영지식 회로를 만들 수 있는 Halo2 언어에 대하여 살펴보도록 하겠습니다. 체감상 Halo2는 Circom 보다 진입장벽이 더 높은 것 같습니다. 이번 블로그 글의 목표는 코드에 사용되는 모든 component의 동작을 이해하는 것보다는 high level 에서 동작을 이해하는 것을 목표로 하겠습니다. halo2는 Rust언어를 기반으로 작동하기 때문에, 해당 코드 작성 전 Rust 설치가 우선시되어야 합니다.
조금 더 구체적으로, 이번 시간에는 Halo2 를 통해 피보나치 수열의 계산을 증명하는 방법에 대하여 알아보도록 하겠습니다. 오늘 사용할 코드는 해당 링크를 참조했습니다.
Proving using Halo2
우선 필요한 라이브러리들을 불러오는 것으로 코드를 시작하겠습니다.
use halo2_proofs::circuit::{Value, Layouter, AssignedCell};
use halo2_proofs::poly::Rotation;
use halo2_proofs::{plonk::*};
use halo2_proofs::arithmetic::Field;
다음으로는 Config struct를 정의해주도록 하겠습니다. #[derive(Clone, Debug, Copy)]는, 정의하는 struct에 대하여 Clone, Debug, Copy trait 의 정의를 자동으로 생성해주도록 하는 Rust의 attribute입니다.
#[derive(Clone, Debug, Copy)]
struct Config {
elem_1: Column<Advice>,
elem_2: Column<Advice>,
elem_3: Column<Advice>,
q_fib: Selector,
}Halo2는 네가지 종류의 column이 존재합니다. 이 중 피보나치 수열의 증명을 위해 3 가지 advice column과 한가지 selector column을 정의해 주도록 하겠습니다.
그 다음으로는 정의한 Config struct에 메소드들을 정의해주도록 하겠습니다. 우선으로는 configure method를 정의해주도록 하겠습니다. configure 함수는 정의한 Config struct에 column들과 gate를 정의하는 역할을 수행합니다.
impl Config {
fn configure<F: Field>(
cs: &mut ConstraintSystem<F>
) -> Self {
let elem_1 = cs.advice_column();
cs.enable_equality(elem_1);
let elem_2 = cs.advice_column();
cs.enable_equality(elem_2);
let elem_3 = cs.advice_column();
cs.enable_equality(elem_3);
let q_fib = cs.selector();
cs.create_gate("fibonacci", |virtual_cells| {
let q_fib = virtual_cells.query_selector(q_fib);
let elem_1 = virtual_cells.query_advice(elem_1, Rotation::cur());
let elem_2 = virtual_cells.query_advice(elem_2, Rotation::cur());
let elem_3 = virtual_cells.query_advice(elem_3, Rotation::cur());
vec![
// q_fib * (elem_1 + elem_2 - elem_3) = 0
q_fib * (elem_1 + elem_2 - elem_3),
]
});
Self { elem_1, elem_2, elem_3, q_fib }
}elem1, 2, 3에 해당하는 advice column, 그리고 q_fib 에 해당하는 selector column을 정의해 줍니다. 또한 일전 PLONK 글에서 설명한 것처럼, gate 의 copy constraint 조건을 확인하기 위해서 이들은 permutation check 에 활용됩니다. Halo2에서 해당 column들을 permutation check 에 활용하기 위해서는 이들 column에 대하여 enable_equality 함수를 적용시켜주어야 합니다.
그 다음으로는 피보나치 수열에 해당하는 gate를 생성해주게 됩니다. 피보나치 수열의 식은 q_fib * (elem_1 + elem_2 - elem_3) = 0 으로 작성할 수 있습니다. 또한 해당 조건은 각 column의 동일한 row 에서 이루어지는 작업이므로 Rotation::cur() 을 사용해 이 작업이 모두 동일한 row 에서 일어나는 작업임을 증명하게 됩니다. 또한 q_fib 를 앞에 곱해줌으로, 해당 조건은 q_fib 라는 selector 가 켜졌을 때만 조건식을 확인하는 역할을 수행하게 됩니다. 마지막으로는 만들어진 Config 를 리턴해주게 됩니다.
그 다음으로는 assign 메소드를 정의해 주도록 하겠습니다.
fn assign<F: Field>(
&self,
mut layouter: impl Layouter<F>,
elem_2: AssignedCell<F, F>,
elem_3: AssignedCell<F, F>,
) -> Result<(
AssignedCell<F, F>, // elem_2
AssignedCell<F, F> // elem_3
), Error> {
layouter.assign_region(|| "steady-state Fibonacci", |mut region| {
let offset = 0;
// Enable q_fib
self.q_fib.enable(&mut region, offset)?;
// Copy elem_1 (which is the previous elem_2)
let elem_1 = elem_2.copy_advice(|| "copy elem_2 into current elem_1", &mut region, self.elem_1, offset)?;
// Copy elem_2 (which is the previous elem_3)
let elem_2 = elem_3.copy_advice(|| "copy elem_3 into current elem_2", &mut region, self.elem_2, offset)?;
let elem_3 = elem_1.value_field().evaluate() + elem_2.value_field().evaluate();
// Assign elem_3
let elem_3 = region.assign_advice(|| "elem_3", self.elem_3, offset, || elem_3)?;
Ok((
elem_2,
elem_3
))
})
}
}assign 블록의 역할은, 이전 row의 값들을 가져와 그 다음 row 에 정의하는 것입니다. elem_2 와 elem_3가 이전 row의 두번째, 세번째 column 값들입니다. layouter는 새로운 row를 만드는 역할이라고 이해하시면 됩니다. 우선 q_fib.enable(&mut region, offset)?; 을 통해 해당 row에서의 selector 값을 켜주도록 하겠습니다.
그 후, copy_advice 함수를 통해 이전 row 에서의 두번째, 세번째 column값을 현재 row 로 가져오겠습니다. 여기서 offset은 기준이 되는 row를 바탕으로의 offset을 나타내며, 저희의 경우 해당 row 에 이전 row의 값들을 정의할 것이기 때문에 offset은 0으로 설정해두면 됩니다. 마지막으로 현재 row의 세번째 column에 값을 지정해주게 됩니다. 이 경우 이전 row의 값들을 바탕으로 직접 값을 계산하여, 세번째 column에도 advice_column값을 넣어주도록 하겠습니다.
이제 만들어진 Circuit을 검증하는 방법에 대하여 알아보도록 하겠습니다. 우선 필요한 라이브러리들을 불러오도록 하겠습니다.
#[cfg(test)]
mod tests {
use halo2_proofs::{circuit::SimpleFloorPlanner, pasta::Fp, dev::MockProver};
use super::*;또한 우리가 증명할 Halo2 테이블은 아래와 같습니다.
/*
1, 1, 2, 3, 5, 8, 13, ...
| elem_1 | elem_2 | sum | q_fib
--------------------------------
| 1 | 1 | 2 | 1
| 1 | 2 | 3 | 1
*/
그 다음으로는 MyCircuit struct와, Circuit trait을 만들도록 하겠습니다.
#[derive(Default)]
struct MyCircuit<F: Field> {
elem_1: Value<F>, // 1
elem_2: Value<F>, // 1
}
impl<F: Field> Circuit<F> for MyCircuit<F> {
type Config = Config;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
Self::default()
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
Self::Config::configure(meta)
}
fn synthesize(&self, config: Self::Config, mut layouter: impl Layouter<F>) -> Result<(), Error> {
// elem_2 = 1, elem_3 = 2
let (elem_2, elem_3) = config.init(layouter.namespace(|| "init"), self.elem_1, self.elem_2)?;
// 1 + 2 = 3
config.assign(layouter.namespace(|| "first assign after init"), elem_2, elem_3)?;
Ok(())
}
}해당 코드에 보면, config.init을 통해 circuit 기본 값들을 initialize 해주고, assign 함수를 통해 이전 row의 element 를 받아 다음 row에 할당해주는 것을 확인할 수 있습니다. 또한 configure 함수에서도 이전에 정의한 Config의 configure 함수를 통해 column들을 만들어줍니다.
마지막으로 테스트 코드를 작성해 주겠습니다.
#[test]
fn test_fib() {
let a = Fp::from(1); // F[0]
let b = Fp::from(1); // F[1]
let circuit = MyCircuit {
elem_1: Value::known(Fp::one()),
elem_2: Value::known(Fp::one()),
};
let prover = MockProver::run(3, &circuit, vec![]).unwrap();
prover.assert_satisfied();
}
}피보나치 수열의 첫 값을 1, 1로 설정해준 뒤, MockProver를 통해 assign 된 값들이 우리가 앞서 만든 모든 조건을 만족하는 것을 확인할 수 있습니다. MockProver::run 의 파라미터로 들어가는 3이라는 숫자는 circuit 사이즈와 관련된 파라미터 입니다.
이번 예제에서는 따로 instance column을 사용하지 않아 public input, output을 따로 확인할 수는 없습니다. 다음번에 Halo2 글을 다루게 된다면 instance column을 활용하는 예제를 가져와 보겠습니다. 여기까지 모든 코드를 작성 후 cargo build 후 cargo test를 해주게 되면 테스트가 올바르게 통과하는 것을 확인할 수 있습니다.
Chiquito
지금까지 Halo2의 예제를 살펴보았습니다. Halo2는 바로 원하는 circuit을 구현하기에는 어려운 감이 있는 것 같다고 개인적으로 생각합니다. Chiquito 는 이러한 어려움을 조금 해소해 줍니다. Python으로 코드를 작성하면 이것을 Halo2 코드를 통해 증명을 생성해 주는데요, 개인적으로 Halo2 보다 훨씬 더 코드가 직관적이라고 생각합니다. 예를 들어, 앞서 작성한 피보나치 수열의 증명을 생성하고 싶다면, 아래와 같이 코드를 작성해주면 됩니다.
class FiboStep(StepType):
def setup(self: FiboStep):
self.c = self.internal("c")
self.constr(eq(self.circuit.a + self.circuit.b, self.c))
self.transition(eq(self.circuit.b, self.circuit.a.next()))
self.transition(eq(self.c, self.circuit.b.next()))
def wg(self: FiboStep, args: Tuple[int, int]):
a_value, b_value = args
self.assign(self.circuit.a, F(a_value))
self.assign(self.circuit.b, F(b_value))
self.assign(self.c, F(a_value + b_value))
class Fibonacci(Circuit):
def setup(self: Fibonacci):
self.a: Queriable = self.forward("a")
self.b: Queriable = self.forward("b")
self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
self.pragma_num_steps(11)
def trace(self: Fibonacci, args: Any):
self.add(self.fibo_step, (1, 1))
a = 1
b = 2
for i in range(1, 11):
self.add(self.fibo_step, (a, b))
prev_a = a
a = b
b += prev_a
fibo = Fibonacci()
fibo_witness = fibo.gen_witness(None)
fibo.halo2_mock_prover(fibo_witness)Halo2 코드와 비슷하면서도 훨씬 간단하고 직관적임을 볼 수 있습니다. 물론 굉장히 구체적인 Halo2 설정을 사용하고 싶다면 직접 코드를 작성해야겠지만, 그렇지 않다면 Chiquito 를 사용해 쉽게 zk circuit을 생성해낼 수 있습니다.
Conclusion
오늘은 Halo2 코드 예제를 작성해보고, Chiquito 에 대하여도 간단한 설명을 드렸습니다. Circom, Halo2, Chiquito를 잘 활용하셔서 원하는 영지식 회로를 잘 사용하셨으면 좋겠습니다.
'영지식증명' 카테고리의 다른 글
| [영지식증명] Sum-Check Protocol 응용: 행렬곱 증명 (1) | 2024.02.15 |
|---|---|
| [영지식증명] Sum-Check Protocol (2) | 2024.02.14 |
| [영지식 증명] Circom 파헤치기 (4) | 2024.01.21 |
| [영지식 증명] PLONK 파헤치기 2 - Permutation Check (2) | 2024.01.12 |
| [영지식 증명] PLONK 파헤치기 2 - Polynomial Commitment (2) | 2024.01.10 |