23.04.28 [ZK] R1CS

zkSNARK 에 사용되는 R1CS 에 대해 이해한대로 정리해보았다. 

- what is zk-SNARK? 

zkSNARK 는 영지식증명 중에서도 비대화형으로 zcash 프로토콜에서 알고리즘으로 개발되어 사용되고 있다.

zk 가 나오게 된 배경, optimistic-rollup vs zk-rollup, zkVM vs zkEVM, zk-SNARK vs zk-STARK 등의 개념은 따로 정리해야겠다.

 

- what is R1CS?

영지식증명에서는 증명에 사용되는 복잡한 computational statements 를 산술 회로로 모델링하여 계산하는 과정이 필요하다.

따라서, 연산 과정을 최대한 단순화하여 모델링하기에 용이한 시스템으로 이해했다.

뒤에서 설명할 예시는 간단하지만 복잡한 시스템을 R1CS 로 모델링하기 위해서는

보통 circuit 으로 회로를 디자인하고 연산, 증명 및 결과 zkey 를 생성한다. 

iden3 에서 제공하는 SNARKjs 라이브러리가 있는데

이걸 사용하면 키 생성 및 연산 결과가 진짜 너무 간단하게 도출되어 생각보다 허무했다.

 

Rank 1 Constraint System

용어에 대해 살펴보자면, rank 1 행렬은 선형 독립 연산으로

행렬을 소거했을 때 만들어지는 피봇 행렬이 최대 1 인 행렬이며, 

constraint 는 회로 연산을 표현한 방정식이다. 

R1CS 에서는 3가지 연산 (덧셈, 곱셈, 뺄셈) 만 다루는데,

나눗셈, 모듈러 연산 같은 경우에는 덧셈, 곱셈으로 다시 나타낼 수 있기 때문이다. 

 

- example of R1CS

다음과 같은 임의의 해시 함수가 있다고 할 때,

증명자는 검증자에게 해당 해시 함수를 알고 있다는 사실을 증명하기 위해 4를 대입한 값인 72 를 output 으로 제출할 수 있다. 

이때, 검증자는 증명자가 4 라는 값을 사용하여 연산했다는 사실을 모르며, 

72 라는 output 과 연산에 사용된 중간값만 가지고도 증명자가 h(x) 에 대한 연산을 했다는 사실을 검증할 수 있다. 

 

계산 과정을 말로 풀어보자면

h(x) 함수의 변수 x 에 대한 차수를 2차로 내리기 위해 

먼저 곱셈 연산으로 이루어진 식 x * x 를 변수 sym1 으로 치환한다. 

그리고 2차로 내려진 식을 다시 1차로 내리기 위해 x * sym1 을 y 로 치환한다. 

그리고 치환한 y - x 를 sym2 로 치환하면 output 에 대한 연산은 치환한 변수를 사용하여

output = sym2 + 7 로 나타낼 수 있다.

 

위 식을 곱셈 연산 (c=a*b) 의 형태로 나타낼 수 있는데 (1, x, output, sym1, y, sym2 순으로)

먼저, sym1 = x * x 같은 경우에는  a = [0, 1, 0, 0, 0, 0] b = [0, 1, 0, 0, 0, 0] c=[0, 0, 0, 1, 0 , 0] 

y = x * sym1 은 a = [0, 1, 0, 0, 0, 0] b = [0, 0, 0, 1, 0 , 0] c = [0, 0, 0, 0, 1, 0]

sym2 = y - x 는 (y-x)*1 로 나타낼 수 있기 때문에 a = [0, -1, 0, 0, 1, 0] b =[1, 0, 0, 0, 0, 0] c = [0, 0, 0, 0, 0, 1]

output = sym2 + 7 도 (sym2 + 7)* 1로 나타낼 수 있기 때문에 a = [7, 0, 0, 0, 0, 1] b = [1, 0, 0, 0, 0, 0] c = [0, 0, 1, 0, 0, 0] 

 

그르면 이제 1차로 내린 행렬 a 들에 대한 행렬 A, b 들에 대한 행렬 B, c 들에 대한 행렬 C 를 만들 수 있다. 

그리고 c = a*b 즉, a*b-c = 0 이며 이를 A, B, C 행렬에 대한 스칼라곱 연산으로 변환할 수 있다. 

아래 수식에서 S 는 곱셈 연산으로 나타내기 위해 지정한 1, x, output, sym1, y, sym2 에 대한 basis 행렬이다. 

행렬 S 의 output 가 7 일 경우, 아래 식을 만족하는 행렬 S 를 계산함으로써 증명이 맞는지 검증할 수 있다. 

행렬 C 를 이항하는 이유는 R1CS 는 영벡터를 포함해야 하기 때문인가?

- circuit of zk-SNARK

위 연산을 Circom 의 circuit 으로 회로 게이트 연산을 작성 및 모듈화할 수 있다. 

 

// circuit.circom 

template BadHash() {
	signal private input x;
	signal x_squared;
	siganl x_cubed; 
	signal output out; 

	x_squared <== x * x; 
	x_cubed <== x_squared * xl 
	out <== x_cubed - x * 7;
}

component main = BadHash();

 

증명자가 계산하는데 사용한 중간 값에 대한 변수는 회로 연산에서 신호 signal 로 나타낼 수 있다. (circom 에서 다루는 변수 타입인 듯)

증명자가 사용한 값 x 인풋값은 검증자에게 알리면 안되므로 private 으로 정의한다. 

 

circom 에서 다루는 연산 기호에 대해 간단히 살펴보자면, 

<+ 는 signal 변수에 대한 초기값을 할당하는 역할을 한다. 

 js 의 = 대입 연산자랑 비슷한 역할을 하나? 생각했었는데

값 할당 외에도 추가적인 constraints 를 설정할 수 있는 역할이 있다고 한다. 

그때 이 연산자가 어떻게 작동하는지는 잘 모르겠다. 그리고 초기값으로 설정된 해당 신호의 R1CS 는 a = 3 이 아니라 a - 3 = 0 이다. 

a <+ 3;

그리고 <== 연산 같은 경우는 할당은 할당인데 조건부 할당이 가능한 연산자이다. 

x_squared <== x * x;

GPT 에 따르면, , a <== (b < c ? 1 : 0)은 b < c라는 조건이 참이면 a에 1을, 거짓이면 a에 0을 할당 한다고 한다. 

 

- 적고보니 드는 의문

1. 행렬 S 에서 output 값으로 인해 x 값이 도출되는 것은 증명자만 알고 있는 사실인가?

이것이 로컬(레이어2)에서 계산되어 레이어 1으로 올라가는건가?

2. SNARK js 에서 증명 연산 결과와 함께 생성되는 증명키, 확인키에는 어떤 값으로 계산되는 것인지 궁금