회로 설계

Halo2는 PLONK 알고리즘 기반의 제로지식 증명 프레임워크로, Rust 언어로 작성됩니다. 피보나치 수열을 증명하려면 (예: Fib(10)=55) 각 계산 단계(비밀 값)를 명시하고, 프로그램(회로)을 통해 검증하여 증명을 생성해야 합니다. PLONK 알고리즘에서는 표를 사용하여 계산 추적을 수행합니다. 예시는 다음과 같습니다:

회로 검증 조건은 다음과 같습니다:

• 다음 a = b, 다음 b = r (등치 제약)
• a + b - r = 0 (사용자 정의 게이트 제약)

입력/출력(목표 결과) 열과 선택자 열(제약 활성화 여부)을 추가해야 하므로 표는 다음과 같이 설계됩니다:

회로 검증 조건은 다음과 같습니다:

• selector * (a + b - c) = 0 (사용자 정의 게이트 제약)
• next_a = b, next_b = c (등치 제약)

최종 노출 결과는 마지막 줄의 c 값 55입니다.

회로가 수행해야 할 단계는 다음과 같습니다:

1. 첫 번째 줄에 a=1, b=1을 입력하고 현재 b 열과 c 열을 반환합니다.
2. 반복(7회), 다음 줄 작성:
3. 이전 줄의 b 열을 현재 a 열로 복사합니다.
4. 이전 줄의 c 열을 현재 b 열로 복사합니다.
5. 합을 계산하여 현재 c 열에 입력합니다.
6. 현재 b 열과 c 열을 반환합니다.
7. 마지막 줄의 c 열 값을 노출합니다(결과).

회로 메서드에서 값 입력 및 계산 함수는 일반적으로 AssignedCell 타입의 단위 셀을 파라미터와 반환 값으로 사용합니다.

FibChip 구조체를 사용하여 이러한 작업을 구현합니다 FibChip

• configure(): 회로 구성 및 사용자 정의 게이트 제약 설정
• initialize_first_row(): 첫 번째 줄의 값 a=1, b=1 입력, c 계산 후 할당된 셀 b와 c 반환
• generate_next_row(): 다음 줄 작성, 이전 줄의 b와 c를 현재 줄의 a와 b로 복사하고 c 계산 및 입력, 현재 셀 b와 c 반환
• expose_public(): 마지막 줄의 c를 최종 결과로 노출하여 검증

구현 방법

1. Cargo 프로젝트 생성

cargo new halo2_fib --bin

2. Cargo.toml에 halo2_proofs 패키지 의존성 추가

[package]
name = "halo2_fib"
version = "0.1.0"
edition = "2021"

[dependencies]
halo2_proofs = { git = "https://github.com/zcash/halo2.git" }

3. src/main.rs를 src/fib.rs로 변경하고 src/lib.rs 생성, 내용 추가

mod fib;

프로젝트 구조는 다음과 같습니다:

halo2_fib
├── src
|    ├── fib.rs
|    └── lib.rs
├── Cargo.lock
└── Cargo.toml

4. fib.rs 구현 회로 구성

#[derive(Clone, Debug, Copy)]
struct FibConfigurations {
    selector: Selector,
    a: Column<Advice>,
    b: Column<Advice>,
    c: Column<Advice>,
    target: Column<Instance>,
}

회로 및 기능 구현

struct FibCircuit {
    config: FibConfigurations
}
impl FibCircuit {
    // 구성 및 제약 조건 생성
    fn setup<F: Field>(meta: &mut ConstraintSystem<F>) -> FibConfigurations {
        let selector = meta.selector();
        let a = meta.advice_column();
        let b = meta.advice_column();
        let c = meta.advice_column();
        let target = meta.instance_column();

        meta.enable_equality(a);
        meta.enable_equality(b);
        meta.enable_equality(c);
        meta.enable_equality(target);
        // 사용자 정의 게이트 제약
        meta.create_gate("피보나치(합)", |meta| {
            let selector = meta.query_selector(selector);
            let num_a = meta.query_advice(a, Rotation::cur());
            let num_b = meta.query_advice(b, Rotation::cur());
            let num_c = meta.query_advice(c, Rotation::cur());
            vec![
                ("a + b = c", selector * (num_a + num_b - num_c)),
            ]
        });
        FibConfigurations { selector, a, b, c, target }
    }
    // 첫 번째 줄 입력 및 반환
    fn initialize_first_row<F: Field>(&self, mut layouter: impl Layouter<F>, a: Value<F>, b: Value<F>) -> Result<(AssignedCell<F, F>, AssignedCell<F, F>), Error> {
        layouter.assign_region(|| "첫 번째 줄 입력", |mut region| {
            self.config.selector.enable(&mut region, 0)?;
            region.assign_advice(|| "a 값 로드", self.config.a,  0, || a).expect("a 로드 실패");
            let cur_b = region.assign_advice(|| "b 값 로드", self.config.b,  0, || b).expect("b 로드 실패");
            let cur_c = region.assign_advice(|| "현재 c 계산", self.config.c,  0, || a+b).expect("c 입력 실패");
            Ok((cur_b, cur_c))  // 반환
        })
    }
    // 다음 줄 입력 및 반환
    fn generate_next_row<F: Field>(&self, mut layouter: impl Layouter<F>, pre_b: &AssignedCell<F,F>, pre_c: &AssignedCell<F, F>) -> Result<(AssignedCell<F, F>, AssignedCell<F, F>), Error> {
        layouter.assign_region(|| "다음 줄 입력", |mut region| {
            self.config.selector.enable(&mut region, 0)?;
            let cur_a = pre_b.copy_advice(|| "이전 b를 현재 a로 복사", &mut region, self.config.a, 0).expect("a 복사 실패");
            let cur_b = pre_c.copy_advice(|| "이전 c를 현재 b로 복사", &mut region, self.config.b, 0).expect("b 복사 실패");
            let value_c = cur_a.value_field().evaluate() + cur_b.value_field().evaluate();
            let cur_c = region.assign_advice(|| "현재 c 계산", self.config.c, 0, || value_c).expect("c 입력 실패");
            Ok((cur_b, cur_c))  // 반환
        })
    }
    // 특정 셀을 최종 결과로 노출
    fn expose_result<F:Field>( &self, mut layouter: impl Layouter<F>, cell: &AssignedCell<F,F>, row: usize ) -> Result<(), Error> {
        layouter.constrain_instance(cell.cell(), self.config.target, row)
    }
}

회로 구현

#[derive(Default)]
struct FibCircuit<F: Field> {
    a: Value<F>, // 초기 a=1
    b: Value<F>, // 초기 b=1
}

impl<F: Field> Circuit<F> for FibCircuit<F> {
    type Config = FibConfigurations;
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self { Self::default() }

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config { FibCircuit::setup(meta) }

    fn synthesize(&self, config: Self::Config, mut layouter: impl Layouter<F>) -> Result<(), Error> {
        let fib = FibCircuit { config };
        // 초기 첫 줄
        let (mut b, mut c) = fib.initialize_first_row(layouter.namespace(||"첫 줄 입력"), self.a, self.b).expect("첫 줄 실패");
        // 다음 줄 반복 입력(7회)
        for _i in 3..10 {
            let (next_b, next_c) = fib.generate_next_row(layouter.namespace(||"다음 줄 입력"), &b, &c).expect("다음 줄 실패");
            b = next_b;
            c = next_c;
        }
        // 결과 노출
        fib.expose_result(layouter, &c, 0)?;
        Ok(())
    }
}

회로 테스트

#[test]
fn test_fib() {
    let circuit = FibCircuit {a: Value::known(Fp::one()),b: Value::known(Fp::one())};
    let target = Fp::from(55);
    let public_input = vec![target];
    let prover = MockProver::run(4, &circuit, vec![public_input]).unwrap();  // 최대 2^4=16 줄
    prover.assert_satisfied();
}

5. 회로 레이아웃 생성

• Cargo.toml에 features/dev 추가, "halo2_proofs/dev-graph" 및 "plotters" 의존성 추가

[package]
name = "halo2_fib"
version = "0.1.0"
edition = "2021"

[features]
dev = ["halo2_proofs/dev-graph", "plotters"]

[dependencies]
halo2_proofs = { git = "https://github.com/zcash/halo2.git" }
plotters = { version = "0.3.5", optional = true }

• fib.rs에 레이아웃 생성 메서드 추가

#[cfg(feature = "dev")]
#[test]
fn print_fib() {
    use plotters::prelude::*;
    let root = BitMapBackend::new("fib-layout.png", (1024, 3096)).into_drawing_area();
    root.fill(&WHITE).unwrap();
    let root = root.titled("Fib Layout", ("sans-serif", 60)).unwrap();

    let circuit = FibCircuit {
        a: Value::known(Fp::one()),
        b: Value::known(Fp::one()),
    };
    halo2_proofs::dev::CircuitLayout::default()
        .render(5, &circuit, &root)
        .unwrap();

    let dot_string = halo2_proofs::dev::circuit_dot_graph(&circuit);
    print!("{}", dot_string);
}

3. features=dev로 테스트 실행

cargo test --features=dev

완전한 코드: https://github.com/hanzhichao/halo2-fib/blob/master/src/fib.rs

회로 레이아웃

v2- 두 개의 advice 열 사용

c 열을 사용하지 않아도 비용을 줄일 수 있지만, 사용하는 줄 수는 약간 증가합니다.

실행 단계:

1. configure() 회로 구성 및 제약 설정
2. initialize_first_row(): 첫 줄과 다음 줄 입력, b와 next_b 셀 반환
3. generate_next_row(): 7회 반복, 다음 줄 입력, b와 next_b 셀 반환
4. 마지막 b 값 노출

완전한 코드: https://github.com/hanzhichao/halo2-fib/blob/v2/src/fib.rs

회로 레이아웃

v3- 첫 줄과 다음 줄 로직 통합

v2의 첫 줄과 두 번째 줄 로직은 동일하므로, 동일한 함수를 사용할 수 있습니다. 이 경우, 입력에 두 개의 초기 셀이 필요합니다. 표는 다음과 같이 설계됩니다:

실행 단계:

1. configure() 회로 구성 및 제약 설정
2. load_private(): a=1을 a 열에 입력, 셀 a 반환
3. load_private(): b=1을 a 열에 입력, 셀 b 반환
4. generate_next_row(): 8회 반복, 다음 줄 입력, b와 next_b 셀 반환
5. 마지막 b 값 노출

완전한 코드: https://github.com/hanzhichao/halo2-fib/blob/v3/src/fib.rs

회로 레이아웃

참고

• https://github.com/rairyx/Halo2-Fibonacci/blob/main/src/fibonacci.rs
• https://github.com/dragan2234/fibosquared-halo2/blob/main/src/fibosquare.rs