Chaper 1: Endless Spreadsheet

Configuration

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let q_enable = meta.complex_selector();
        let advice = meta.advice_column();

• advice : an "advice" column which the prover can assign values to freely
• q_enable : a "selector" column, used turns gates on and off. it contains constants.

This can be visualized as a spreadsheet with two columns with infinite number of rows

advice	q_enable
...	...

the circuit is defined by fixing certain cells in this spreadsheet and the prover gets to fill in the rest of the spread sheet. At this point, we have spreadsheet where:

• the first column is completely unconstrained.
• the second column is a column of constant zeros.

이것을 좀 더 useful하게 만드려면, Gate를 define 해야함.

Gate : Halo2에서는 spreadsheet 내부 cell에서의 constraints으로, cell들의 관계를 만들어주는 역할

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let q_enable = meta.complex_selector();
        let advice = meta.advice_column();

        // define a new gate:
        // next = curr + 1 if q_enable is 1
        meta.create_gate("step", |meta| {
            let curr = meta.query_advice(advice, Rotation::cur());
            let next = meta.query_advice(advice, Rotation::next());
            let q_enable = meta.query_selector(q_enable);
            vec![q_enable * (curr - next + Expression::Constant(F::ONE))]
        });

이 gate는 global constraint을 강제함. 즉 모든 행에 적용됨

• advice cell in the current row : meta.query_advice(advice, Rotation::cur())
• 빼기 다음 행의 advice cell : meta.query_advice(advice, Rotation::next())
• 더하기 1 : Expression::constant(F::ONE)
• 곱하기 q_enable "selector": meta.query_selector(q_enable)

즉 :

• q_enable = 1이면, next = curr + 1
• q_enable = 0이면, next는 어떤 것이든 될 수 있음

-> gate를 켜고 끄기 위해 selector가 필요함,
- selector가 없었다면 항상 on 되어있는 상태이고, prover는 모든 행의 모든 게이트를 만족시켜야 한다.
- selector를 통해 우리는 어떤 행의 어떤 게이트를 enforce할지 프로그래밍 할 수 있음
- 이것이 synthesize step이다.

Configuration : spreadsheet와 그 안의 gate를 정의 하는 것
Synthesis : spreadsheet을 채우는 것

Synthesize

Creating Regions

Region : 연속된 rows의 집합

Region이 작동하는 방식은 아래와 같음 :

• 사용자가 Halo2에게 region을 생성하라고 함
• 그런 다음 시작을 기준으로 해당 영역의 셀을 참조할 수 있음

region을 생성하고, cell을 할당하는 것은 synthesize 스텝이다.
가장 작은 region은 single row이고, 가장 큰 region은 전체 spreadsheet이다.

    fn synthesize(
        &self,
        config: Self::Config, //
        mut layouter: impl Layouter<F>,
    ) -> Result<(), Error> {
        layouter.assign_region(
            || "steps",
            |mut region| {

위의 경우에는 single region을 사용

• Region의 존재 이유
  - usability를 위해. 그냥 큰 region하나를 가지고 있을 수 있지만, 이렇게 되면 참조하고자하는 cell의 절대 위치를 알아야 하고, indexing 또한 유저가 알아서 해아해서 조각으로 나누어서 관리하는 것
• Halo2는 region이 spreadsheet의 어디있는지 어떻게 아나?
  - Halo2가 그것을 직접 결정하고, spreadsheet의 사용 가능한 다음 행부터 영역 배치

Assigning Cells in a Region

Prover가 advice column에 채우는 value는 어디서 오는가? 즉 witness는 어디서 오는가?

• circuit struct에 멤버를 추가하여, synthesize에 witness를 채운다.

struct TestCircuit<F: Field> {
    _ph: PhantomData<F>,
    values: Value<Vec<F>>,
}

Value<T>는 Option<T>와 같음
이것은 prover만 아는 value를 채우기 위해서 존재

• verifier에게 Value는 Value::unknown()
• Prover에게는 Value::known(some_witness)

Proof를 생성할때, 사용자는 Value를 witness로 채우고, synthesis를 한다.
그럼 synthesis는 value를 spreadsheet에 assign한다.

region.assign_advice(
	|| "assign advice", // 1. 작업에 대한 설명 (디버깅용)
	config.advice, // 2. 할당할 열 (Advice 열)
	1, // 3. 할당할 행 (1번째 행)
	|| Value::known(self.values.as_ref().unwrap()[1]), // 4. 할당할 값 (self.values의 1번째 값)
)?;

Rust 문법

|| "assign advice"

• 역할: 이 부분은 클로저(closure)로, 작업에 대한 설명 문자열 "assign advice"를 반환합니다.
• 의미: 이 문자열은 디버깅이나 로깅 목적으로 사용되며, 이 작업이 무엇을 하는지 설명합니다. 예를 들어, 디버깅 시 "assign advice"라는 메시지가 출력될 수 있습니다.

|| Value::known(self.values.as_ref().unwrap()[1])

• 역할: 할당할 값을 반환하는 클로저입니다.
• 의미:
  • self.values.as_ref().unwrap()[1]: self.values에서 1번째 값을 가져옵니다.
  • Value::known(...): 가져온 값을 Halo2의 [Value]타입으로 래핑합니다. 이는 회로에서 사용할 수 있는 값으로 변환하는 작업입니다.

||의 역할

||는 클로저(closure)를 정의하는 문법입니다. 클로저는 익명 함수로, 코드 블록을 함수처럼 실행할 수 있습니다.

클로저의 형태

|| { ... }

• ||: 클로저의 매개변수를 정의합니다. 이 경우 매개변수가 없으므로 빈 ||를 사용합니다.
• { ... }: 클로저의 본문(body)입니다. 이 안에 실행할 코드를 작성합니다.

클로저의 사용 이유

Halo2에서는 assign_advice와 같은 함수가 클로저를 사용하여 값을 동적으로 계산하거나 반환하도록 요구합니다. 클로저를 사용하면 값이 필요할 때만 계산되므로 효율적입니다.