[영지식 증명] Circom 파헤치기

Introduction

안녕하세요, 지난 시간까지는 영지식 증명 방법 중 하나인 PLONK에 대하여 알아보았습니다. 지난 시간까지 조금 이론적인 내용을 다루었다면, 이번 시간에는 영지식 증명을 위한 회로를 짜는 방법에 대하여 알아보도록 하겠습니다. 

 

Alice가 영지식 증명을 통해 어떤 주장을 증명하고 싶어합니다. Alice는 앞서 배운 PLONK를 직접 구현할 수도 있겠지만, 이러한 과정은 시간이 굉장히 많이 소요됩니다. 다행히도, 개발자들이 이미 쉽게 영지식 증명을 위한 회로를 짤 수 있는 방법을 마련해 두었습니다. Circom, Halo2, Noir 등이 이러한 예시입니다. 이번 시간에는 Circom 을 사용하는 방법에 대하여 알아보도록 하겠습니다. 

Installing Circom

자세한 circom 설치 방법은 여기나와 있습니다. 하나하나 따라가면 circom 설치를 문제없이 완료하실 수 있습니다.

마지막으로 circom --help 명령어를 통해 circom 의 설치를 확인해줍시다.

 

Writing multiplication circuit template

우선 두 수 곱셈의 계산결과를 증명할 수 있는 circuit을 만들어 보겠습니다. (출처)

pragma circom 2.0.0;

/*This circuit template checks that c is the multiplication of a and b.*/  

template Multiply2 () {  

   // Declaration of signals.  
   signal input a;  
   signal input b;  
   signal output c;  

   // Constraints.  
   c <== a * b;  
}

우선 pragma circom 2.0.0; 은 사용할 circom 의 컴파일러 버전을 의미합니다.

그 다음 Multiply2 라는 template을 정의해줍니다. Circom에서의 template은, 큰 circuit을 만들기 위한 추상화된 단위조직입니다.

Template 내부의 signal 들은 사용할 변수들을 의미합니다. Circom에서는 기본적으로 signal 들을 private으로 간주하고, output은 항상 public 합니다. 마지막 c <== a*b 는 변수간 만족해야 하는 constraint를 의미합니다. circom에서는 덧셈과 곱셈에 대한 constraint를 사용할 수 있습니다.

Proving & verifying multiplication circuit

이렇게 만든 circuit을 실제로 증명에 사용하기 위해서는 우선 component를 만들어야 합니다. 정의한 template을 바탕으로 다음과 같이 component를 만들어 주겠습니다. 

component main = Multiply2();

완성된 코드를 multiply2.circom 으로 저장하겠습니다. 그 후에 아래 커맨드를 통해 circuit을 compile 해주도록 하겠습니다.

circom multiply2.circom --r1cs --wasm --sym

작업이 끝나면 multiply_js 폴더도 함께 만들어진 것을 확인할 수 있습니다.

 

이 다음으로 진행해야 할 작업은, prover가 실제로 자신이 가지고 있는 정보를 사용해 증명을 만들기 위한 값들 (witness) 을 생성해 내는 작업입니다. circom 에서는 이러한 witness를 json 파일 형태로 받게 됩니다. 저희의 경우도 {'a': 10, 'b': 17} 의 정보를 담은 input.json 파일을 생성해 주도록 하겠습니다. 그 후, 생성된 multiply_js 폴더로 들어가 아래 커맨드를 통해 witness 를 생성합니다.

node generate_witness.js multiply2.wasm ../input.json witness.wtns

 

마지막으로 증명을 생성하는 방법입니다. 해당 포스트에서는 Groth16 방법을 통해 증명을 생성하도록 하겠습니다. 우선 아래 커맨드를 통해 타원곡선에서의 trusted setup 에 참여하도록 하겠습니다. 

snarkjs powersoftau new bn128 12 pot12_0000.ptau -v
snarkjs powersoftau contribute pot12_0000.ptau pot12_0001.ptau --name="First contribution" -v

pot12_0000/1.ptau 파일이 생성된 것을 확인할 수 있습니다.

 

PLONK와 다르게, Groth16의 setup은 circuit-specific 합니다. 따라서 직접 제작한 circuit을 위한 setup을 진행해주겠습니다. 

snarkjs powersoftau prepare phase2 pot12_0001.ptau pot12_final.ptau -v
snarkjs groth16 setup multiply2.r1cs pot12_final.ptau multiply2_0000.zkey
snarkjs zkey contribute multiply2_0000.zkey multiply2_0001.zkey --name="your name" -v
snarkjs zkey export verificationkey multiply2_0001.zkey verification_key.json

 

이제 증명을 위한 모든 과정이 마무리 되었습니다. 아래 커맨드를 통해 증명을 생성합시다.

snarkjs groth16 prove multiply2_0001.zkey witness.wtns proof.json public.json

 

또한 아래 커맨드를 통해 만들어진 증명을 검증할 수 있습니다. 

snarkjs groth16 verify verification-key.json public.json proof.json

 

Proving matrix multiplication

이번에는 조금 더 어려운 예시를 들어보도록 하겠습니다. Prover가 임의의 input $A \in \mathbf{R}^{m \times n}$ (public) 과 행렬 $B \in \mathbf{R}^{n \times p}$ (private) 을 가지고 있다고 가정하겠습니다. Prover는 $AB = C$ 를 증명하고 싶어합니다. (C: public) 이 경우 어떻게 해당 행렬 곱셈을 증명할 수 있는 circuit을 나타낼 수 있는지 알아보도록 하겠습니다.

 

우선 첫번째로, matElemMul 이라는 템플릿을 정의해주겠습니다. matElemMul template은 인풋으로 두 개의 $\mathbf{R}^{m \times n}$ 행렬을 받게 됩니다. 또한 해당 template의 output 행렬은, 두 인풋 행렬의 hardamard product (element-wise product) 로 계산됩니다. 코드는 아래와 같습니다.

pragma circom 2.0.0;

// matrix multiplication by element
template matElemMul (m,n) {
    signal input a[m][n];
    signal input b[m][n];
    signal output out[m][n];
    
    for (var i=0; i < m; i++) {
        for (var j=0; j < n; j++) {
            out[i][j] <== a[i][j] * b[i][j];
        }
    }
}

 

실제 코드에서도 두 인풋 행렬의 각 entry 마다 element-wise하게 곱셈을 진행한 후, output 행렬에 넣어주는 것을 확인할 수 있습니다. 

 

그 다음으로는 matElemsum template을 정의해주겠습니다. 해당 template은 인풋 행렬을 하나 받아 해당 행렬내의 모든 원소의 합을 리턴합니다. 코드 상에서도 행렬 내의 각 원소를 traverse 하며 리턴 값을 증가시켜나가는 것을 확인할 수 있습니다. 

pragma circom 2.0.0;

// sum of all elements in a matrix
template matElemSum (m,n) {
    signal input a[m][n];
    signal output out;

    signal sum[m*n];
    sum[0] <== a[0][0];
    var idx = 0;
    
    for (var i=0; i < m; i++) {
        for (var j=0; j < n; j++) {
            if (idx > 0) {
                sum[idx] <== sum[idx-1] + a[i][j];
            }
            idx++;
        }
    }

    out <== sum[m*n-1];
}

 

이제 마지막으로 해당 두 템플릿을 사용하여 행렬간 곱셈을 증명하는 circom 코드를 작성해 보겠습니다.

pragma circom 2.0.0;

include "matElemMul.circom";
include "matElemSum.circom";

// matrix multiplication
template matMul (m,n,p) {
    signal input a[m][n];
    signal input b[n][p];
    signal output out[m][p];

    component matElemMulComp[m][p];
    component matElemSumComp[m][p];
    
    for (var i=0; i < m; i++) {
        for (var j=0; j < p; j++) {
            matElemMulComp[i][j] = matElemMul(1,n);
            matElemSumComp[i][j] = matElemSum(1,n);
            for (var k=0; k < n; k++) {      
                matElemMulComp[i][j].a[0][k] <== a[i][k];
                matElemMulComp[i][j].b[0][k] <== b[k][j];
            }
            for (var k=0; k < n; k++) {
                matElemSumComp[i][j].a[0][k] <== matElemMulComp[i][j].out[0][k];
            }
            out[i][j] <== matElemSumComp[i][j].out;
        }
    }
}

찬찬히 살펴보도록 하겠습니다. 두 개의 인풋 행렬 $a, b$ 가 존재하며, output 행렬 $out \in \mathbf{R}^{m \times p}$ 또한 존재하는 것을 확인할 수 있습니다. 이제 인덱스 $i, j$를 돌며 $out_{i,j}$ 를 넣어주게 됩니다. 각 $out_{i,j}$를 계산하기 위해서 matElemMulComp 와 matElemSumComp를 또한 정의하게 됩니다. 이 둘은 각각 $\mathbf{R}^{1 \times n}$ 의 row vector를 인풋으로 받습니다. 

 

우선 matElemMulComp에는 행렬 $a$의 ith row, 행렬 $b$의 jth column 을 넣어주게 됩니다. 이 결과물은 아까 말한 것처럼 두 벡터의 element-wise product 가 됩니다. 또한 이 결과물을 matElemSumComp에 넣어주게 되는데요, 아까 정의한 것처럼 해당 템플릿은 각 element-wise product를 전부 summation한 결과를 리턴해주게 됩니다. 이렇게 계산된 결과는 행렬곱에서 $out_{i,j}$이 가져야 하는 값과 동일합니다. 

 

 증명 과정 또한 동일합니다. $n, m, p = 2,3,4$ 인 경우, 저희 예시의 경우 행렬 $b$만 private이고 인풋 $a$는 public 이므로 아래와 같이 component를 정의해주겠습니다.

component main {public [a]} = matMul(2,3,4);

또한 input.json 파일도 행렬의 크기에 맞게 아래와 같이 정의해줍니다.

{"a": [1,2,3,1,2,3], "b": [1,2,3,4,1,2,3,4,1,2,3,4]}

이제 다시 한번 circuit-dependent 한 셋업을 진행한 후, 증명과정을 거치면 증명 및 검증이 이루어지는 것을 확인할 수 있습니다.

 

Conclusion

이번 시간에는 영지식 증명 회로를 만들 수 있는 도구인 circom의 기본적인 사용방법에 대하여 알아보았습니다. 언어의 문법이 직관적이라 빠르게 익힐 수 있다는 장점을 가진 언어인 것 같습니다. 궁금한 점이나 질문 있으시면 댓글로 남겨주세요.