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 를 계산함으로써 증명이 맞는지 검증할 수 있다.
- 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 에서 증명 연산 결과와 함께 생성되는 증명키, 확인키에는 어떤 값으로 계산되는 것인지 궁금