Circom

(tag: fast step for zk Dapp developer, zk-snark, circuit)
해당 article은 circom 2 기준으로 작성되었습니다.

About Circom

(Background: modulo, finite field)

Circom은 영지식 증명을 생성하는 데 사용할 수 있는 산술 회로(arithmetic circuits)를 정의하기 위한 새로운 DSL(Domain-Specific Language)입니다.

Why defining arithmetic circuits?

zk-SNARK를 조금 알고 있으면 이해에 도움이 되겠지만, 대부분의 ZKP와 같이 zk-SNARK는 computational statements를 증명할 수 있습니다. 특히, zk-SNARK를 사용하려면 computational statements를 산술 회로로 모델링해야 합니다. 여기서 산술 회로는 주어진 소수 p값의 finite field상의 값을 가지는 와이어 세트로 구성된 회로입니다. 그리고 modulo p의 덧셈 및 곱셈 게이트에 연결합니다. Ethereum에서 zk-SNARK 증명을 생성하고 검증하려면 아래 주어진 소수 p값에 finite field에서 산술 회로를 만들어야 합니다.
p = 21888242871839275222246405745257275088548364400416034343698204186575808495617

How to deal with circuit in circom

zk-SNARK protocols를 사용하려면, signal간의 관계를 게이트와 변수를 연결하는 방정식으로 묘사해야 합니다. 회로를 묘사하는 방정식을 constraints라고 부를 것이며, 해당 회로의 signal이 충족해야 하는 조건으로 생각할 수 있습니다.(signal은 회로의 입력, 출력, 중간 신호를 의미)

circom을 사용하면, 자신만의 circuit과 constraint를 디자인하고 영지식 증명에 필요한 R1CS 표현을 컴파일러를 통해 출력할 수 있습니다. R1CS 표현은 영지식 증명에 필요한 표현이고 circom의 역할은 산술 회로를 구성하고 R1CS를 포함한 영지식 증명에 필요한 파일로 컴파일 하는 것입니다.

영지식을 통해 회로 만족도(circuit satisfiability)를 증명할 수 있습니다. 이것이 의미하는 바는 회로를 만족시키는 signal의 집합을 알고 있다는 것, 다시 말하자면 R1CS에 대한 솔루션을 알고있다는 것을 증명할 수 있다는 것입니다. 이 신호의 집합을 witness라고 합니다.

다시 한번 zk-SNARK 증명에 대해 이야기 하자면, witness라는 signals의 집합을 알고 있음을 증명할 수 있는 특정 유형의 영지식 증명입니다. 이는 공개 입력 및 출력을 제외한 어떠한 signals를 드러내지 않고 회로의 모든 constraint와 일치하는지 확인하는 과정을 가집니다.

이번 article에선 첫 단계 산술 회로를 컴파일하는 과정 즉, 영지식 증명에 필요한 R1CS 파일, witness 계산을 위해 필요한 wasm 파일 등을 출력할 수 있는 circuit compiler인 circom에 대해 다룹니다.

이해를 돕기 위해 witness는 "a set of all computation trace values"로 나타낼 수도 있다.

아래 오버뷰처럼 컴파일 이후는 일반적으로 snarkjs라는 툴을 사용해서 증명을 생성하고 검증하는 단계를 가집니다. 이는 snarkjs article에서 자세히 확인할 수 있습니다.

overview of zk-snark dapp using circom

요약하면, circom은 사용하기 쉬운 인터페이스를 통해 산술 회로를 구성하고 증명 메커니즘의 복잡성을 추상화하는 전체론적 프레임워크를 개발자에게 제공하는 것을 목표로 합니다.

---

Circom circuit

Signal

Circom을 사용하여 구축된 산술 회로는 signal에 대해 작동합니다. Signal은 식별자로 이름을 지정하거나, 배열에 저장, keyword signal을 사용하여 선언 가능합니다. Signal은 input, output으로 정의 가능하고 그렇지 않으면 intermediate signal 즉, 중간 신호로 여겨집니다.

Signal은 항상 private으로 여겨지며, 프로그래머가 public과 private signal을 구분 짓는 것은 main component를 정의할때만 입니다. circom에선, main component의 모든 output signal은 public(private 불가능)입니다.

Signal은 불변합니다. 즉, 값이 한번 할당되면 그 값은 바뀔 수 없습니다. 또한, 컴파일 시간에서 signal의 내용(상수가 할당 되었어도)은 항상 unknown으로 간주됩니다. 그 이유는 signal이 항상 상수 값을 가지고 있는지 여부를 감지하는 컴파일러의 힘에 의존하지 않고, 어떤 구성이 허용되고 허용되지 않는지에 대한 정확한 결정을 내릴 수 있는 정의를 제공하기 위함입니다.

Signal은 <--, <== 연산자를 사용해 할당 됩니다.(signal이 오른쪽에 있을 경우 -->, ==> 사용)
<==, ==> 연산자는 값을 할당하고 동시에 constraints를 생성하기 때문에 안전한 옵션입니다.
<--, --> 연산자는 할당된 표현식을 constraint에 포함시킬 수 없는 경우에만 사용해야 합니다.

Variables & Mutability

변수는 signal이 아닌 데이터를 보유하고 변경할 수 있는 식별자입니다. constraint를 작성하는데 사용되는 경우 필드의 숫자 값 또는 산술 표현식의 숫자 값을 보유합니다. 변수 식별자를 사용해 이름을 지정하거나 배열에 저장할 수 있습니다. 변수 할당은 = 로 할당하고, 할당은 명령문이며 값을 반환하지 않습니다. 표현식의 일부가 될 수 없으므로 잘못된 사용을 방지할 수 있습니다. 만약 표현식 내부에서 = 를 사용하면 컴파일 오류가 발생합니다.

Templates

Circom에서 일반적인 회로를 만드는 메커니즘은 template입니다. Circom의 하나의 중요 특징은 프로그래머가 template이라고 부르는 매개변수화 가능한 회로를 정의할 수 있는 모듈성입니다. 다른 회로에 결합되거나 더 큰 회로를 형성할 때 부분이 되기위해 인스턴스화 할 수 있습니다. template은 인스턴스화를 통해 회로를 정의하므로, 자체적인 input, output, 그 외 signal이 있습니다.

Template의 인스턴스화는 component 키워드와 필요한 매개변수를 제공해서 만들어집니다. 매개변수의 값은 컴파일 시간에서 알려진 상수여야 합니다.

Component

Component는 산술 회로를 정의하므로, N개의 input signal을 받아, M개의 output signal 그리고 K개의 intermediate signal을 생성합니다. 이는 constraint의 집합을 생성할 수 있습니다. component의 input 혹은 output signal을 접근하려면 dot notation을 사용하면 됩니다. 다른 signal은 component 밖에서 볼 수 없습니다.

Component 인스턴스화는 모든 input signal이 구체적인 값에 할당될 때까지 동작하지 않습니다. 그렇기에 인스턴스화가 지연될 수 있으므로 component 생성 명령은 component 객체의 실행을 의미하는 것이 아니라 모든 입력이 설정될 때 완료될 인스턴스화 프로세스의 생성을 의미합니다. Component는 signal과 같이 불변합니다. 추가적으로 이전에 주어진 크기에 대한 동일한 제한에 따라 component의 배열을 정의할 수 있습니다.

Function

함수는 숫자(또는 배열)값 혹은 표현식을 계산합니다. 또한, 함수는 재귀적일 수 있습니다. 하지만 함수 안에서 signal을 선언하거나 constraint를 생성할 수 없습니다. 필요한 경우 template을 사용해야 합니다. 주의해야할 점은 함수의 모든 실행 끝은 return문이 반환되어야 합니다.

Main Component

실행을 시작하기 위해서, 초기 component가 제공되어야 합니다. 기본적으로 그것이 main component입니다. 그러므로 main component는 일부 template으로 인스턴스화 해야 합니다. 이것은 회로를 생성하기 위해 필요한 틀별한 초기 component입니다. 그리고, 회로의 global input과 output signal을 정의합니다. Main component는 오직 하나만 정의할 수 있습니다.

Constraint Generation

Circom을 사용하면 프로그래머가 산술 회로를 정의하는 constraint를 정의할 수 있습니다. 모든 constraint는 2차 표현 형식 A$*$B + C = 0 이어야 합니다.(A, B, C는 신호의 1차 표현입니다.)
=== 연산자로 constraint가 부과됩니다. 구성 단계에서 변수는 곱셈, 덧셈 및 기타 변수 또는 signal 및 필드 값을 사용하여 착성된 산술 표현식을 포함할 수 있습니다. constraint는 2차 표현식만 포함될 수 있습니다. 2차 표현 이외의 다른 산술 표현식이나 나눗셈이나 거듭제곱과 같은 다른 산술 연산자를 사용하는 것은 constraint로 허용되지 않습니다. 앞에 Signal 부분에서도 말했지만 constraint가 추가되지 않는 <-- 연산자를 오용하면 안됩니다. 되도록이면 <== 연산자를 사용해서 할당과 constraint 추가를 수행하는 것이 좋습니다.

<-- 연산자 사용 예시)
y <== x / z (틀린 표현, 나눗셈이 허용되지 않음)>

y <-- x / z
x === y$*$z 로 나눠야함

추가 사항

Unknown

Constraint 생성중에 허용되는 최대 표현은 2차 표현식이므로, 컴파일 시 알수없는 값 사용에 대해 특정 검사와 constraint가 부과됩니다. Circom에서 상수 값과 template 매개변수는 항상 known으로 간주하고 signal은 항상 unknown으로 간주됩니다.

Pragma

.circom 확장자를 가진 모든 파일은 컴파일러 버전을 지정해야 합니다. 이는 회로가 명령어 뒤에 표시된 컴파일러 버전과 호환되는지 확인하기 위함입니다. 파일에 이 명령이 없으면 코드가 최신 컴파일러 버전과 호환되는 것으로 가정하고 경고가 발생합니다.

more details in circom language docs

---

short example

위 내용을 바탕으로 몇가지 예제를 살펴볼 수 있습니다.

1.NAND gate

pragma circom 2.0.0;

template NAND() {
	signal input s1;
	signal input s2;
	signal output s3;

	s3 <== 1 - s1*s2;
}

component main = NAND();

해당 회로는 기본적인 NAND게이트를 회로로 만든 것입니다. 앞서 말했듯이 컴파일러 버전을 명시해주는 것이 좋습니다. s1, s2는 별다른 명시가 없으므로 private input이고 s3는 public output입니다. 아래와 같이 해당 회로에서 input인 s1,s2의 바이너리 형식을 강제할 수 있는 constraint를 추가할 수도 있습니다.

pragma circom 2.0.0;

template NAND() {
	signal input s1;
	signal input s2;
	signal output s3;
	
	s3 <== 1 - s1*s2;
	s1*(s1-1) === 0;
	s2*(s2-1) === 0;
}

component main = NAND();

2. 혼합 회로

앞에서 구현한 NAND 게이트를 포함한 일반적인 gate들은 circomlib의 gates.circom에서도 확인할 수 있습니다. 아래 예시와 같이 해당 circom파일을 include하여 gate들을 조합한 혼합 회로를 만들어 볼 수 있습니다.

pragma circom 2.0.0;
include "circomlib/circuits/gates.circom"

template GateSample() {
	signal input s1;
	signal input s2;
	signal input s4;
	signal s3;
	signal output s5;

	component G1 = NAND();
	component G2 = AND();

	G1.a <== s1;
	G1.b <== s2;
	s3 <== G1.out;
	G2.a <== s3;
	G2.b <== s4;
	s5 <== G2.out;
}

component main = GateSample();

해당 회로는 앞서 설명한 NAND게이트를 통과한 후 NAND게이트 output과 새로운 input을 추가해 AND게이트를 통과하는 회로입니다. s3는 intermediate signal 즉 중간 신호이며 이번 회로에서는 간단하게 값을 할당만하기에 중간 신호 s3를 생략하여도 문제 없습니다.

//s3 <== G1.out;
//G2.a <== s3;
G2.a <== G1.out;

private input들 중 s1,s2를 public input으로 간주하고 싶으면 해당 로직을 따라하면 됩니다.

component main{public [s1,s2]} = GateSample();

3. 숫자 -> 이진수 변환

pragma circom 2.0.0;

template Num2Bits(n) {
    signal input in;
    signal output out[n];
    var lc1=0;

    for (var i = 0; i<n; i++) {
        out[i] <-- (in >> i) & 1;
        out[i] * (out[i] -1 ) === 0;
        lc1 += out[i] * 2**i;
    }

    lc1 === in;
}

component main{public [in]} = Num2Bits(8);

해당 회로는 숫자를 입력받을 매개변수를 가지고 있으며 10진수 숫자를 이진 표현으로 변환해주는 회로입니다. 회로의 output은 길이가 8인 이진 표현 배열입니다. Template 매개변수는 known으로 간주하기 때문에 output 배열에 대해 컴파일 오류가 발생하지 않습니다. 마지막으로는 변환이 잘 이루어졌는지 보증하기 위해 lc1 === in라는 constraint를 추가합니다.

기본적인 회로들로 circom을 직접 사용해 보았고 더 나아가 zk-SNARK dApp에 실제로 많이 사용되는 해시 함수(ex. poseidon 등)의 회로 표현을 살펴볼 수 있습니다. 이 article에서 다룬 내용은 산술 회로와 circom이며 zk-SNARK 증명을 생성하기위한 첫번째 단계입니다. zk-SNARK에 대해 더 알고싶거나 다음 단계로 넘어가고 싶다면 해당 article을 참고하면 됩니다.

---

Tools for circom

hardhat-circom - Hardhat plugin to integrate circom and snarkjs into build process.
zkrepl - Online play ground for zk circom circuits.
circomlib - Repository contains a library of circuit templates.