[Halo2-Dev] Poseidon Hash Circuit

1. 개요

이번에는 영지식 증명 프로토콜의 증명 대상인 circuit의 구현 방법에 대해 알아보자. 최근에 영지식 증명 프로토콜들을 구현하는 여러 프로젝트들이 있지만, 그 중에서도 lookup table 및 custom gate를 활용한 circuit의 작성이 가능한 halo2 라이브러리 설계방법을 알아보려한다. 이를 위한 첫번째 단계로, halo2의 custom gate를 잘 활용하고 있는 Scroll's poseidon hash circuit(scroll-dev-0723) 을 분석해보자. 특히, Poseidon 해시 함수의 가장 중요한 연산인 permutaion을 circuit으로 중점을 둘 것이다.

$\quad$

2. 파라미터 및 기본 설정

Recap

	r은 rate로 데이터 블록 길이에 해당하는 throughput, 데이터를 rate 단위로 나누어 연산
    c는 capacity로 안전성에 이 값이 클수록 더 높은 보안 수준을 의미, 처리 속도는 느려질 수 있음
    라운드 횟수: 스펀지 구조에서 permutation을 여러 라운드에 걸쳐 반복적으로 적용하는데, 이때 반복횟수
    state: permuation 과정에서 업데이트 되는 중간 계산 결과
    state의 길이는 N = r + c 으로 계산되며 라운드를 거치면서 값이 변경됨

$\quad$

Settings

다음에서 설정되는 파라미터 값들은 다양한 조합으로 설정 될 수 있다. 단, 값을 변경할 때에는 안전성을 고려해야 한다는 점에 유의해야한다.

• $S(x)=x^5$로 정의되는 s-box 사용

• RF = 8, RP = 57

• capacity = 1

• rate = 2

• width(t) = 3 elements (rate + capacity)

  	각 라운드 횟수: full 라운드 횟수(RF)는 총 8번, partial 라운드 횟수(RP)는 57번이며 full 라운드는 partial 라운드의 앞뒤로 배치한다. 
    즉, full 라운드 4번 - partial 라운드 57번 - full라운드 4번의 순서로 구성한다.

  $\quad$

Notation

다음의 표기에서 적고 있는 $k$ 인덱스는 width $t$ 에 대해 $0\leq k< t$ 범위에서 정의된다.

• $\vec{s}[k]$: state 들로 구성된 advice column

• $s_i[k]$: $i$ 번째 라운드에서 $k$번째 state

• ${\vec{rc}}_{a}[k],{\vec{rc}}_{b}[k]$: 라운드 상수들로 구성된 fixed column

• $rc_i[k]$ : $i$ 번째 라운드의 라운드 상수

• $M, N$: width $t$ 에 대해서 $t\times t$ 행렬로 정의되는 MDS 행렬과 그 역행렬

• $\vec{m_k} = (m_k[0], m_k[1],..., m_k[t-1])$: $t\times t$ MDS 행렬의 $k$ 번째 행벡터

• ${\vec{n}_k} = ({n}^{-1}_k[0], {n}^{-1}_k[1],..., {n}^{-1}_k[t-1])$: $t\times t$ MDS 역행렬의 $k$ 번째 행벡터

• ${\vec{s}}_{tmp}$: partial round 에서만 추가적으로 사용되는 advice column

• $\vec{s}_f, \vec{s}_{2p}, \vec{s}_{p}, \vec{s}_{paa}$: $0$ 과 $1$ 로 이루어진 selector column

  $\quad$
  $\quad$

3. Circuit 설계

Permutation 연산을 구성하는 gate

다음은 코드에서 정의하고 있는 gate들을 표로 나타내었다. 각 표에서 분홍색은 advice column, 하늘색은 fixed column에 해당하는 값을 구분하기 위하여 사용하였다. 아래 표에서 ${{\vec{s}[0], \vec{s}[1], \vec{s}[2]}}$는 width $= 3$ 인경우의 state들의 벡터이고, ${{\vec{rc_a}[0], \vec{rc_a}[1], \vec{rc_a}[2]}}$ 및 $\textcolor{#87AAB3}{{\vec{rc_b}[0], \vec{rc_b}[1], \vec{rc_b}[2]}}$는 라운드 상수들의 벡터이다. 초기 state는 $\textcolor{#DAA7AA}{{s_0[0], s_0[1], s_0[2]}}$로 정의되며, 초기 state에 더할 라운드 상수는 $\textcolor{#87AAB3}{{rc_0[0], rc_0[1], rc_0[2]}}$ 이다.
$\quad$

• full round
  permutation의 첫번째 라운드는 full 라운드로 시작한다. 아래 표는 selector $\vec{s}_f$의 상대적 위치로 정의되는 값들의 영역을 나타낸다.

  $\textcolor{#DAA7AA}{{\vec{s}[0]}}$	$\textcolor{#DAA7AA}{{\vec{s}[1]}}$	$\textcolor{#DAA7AA}{{\vec{s}[2]}}$	$\textcolor{#87AAB3}{{\vec{rc_a}[0]}}$	$\textcolor{#87AAB3}{{\vec{rc_a}[1]}}$	$\textcolor{#87AAB3}{{\vec{rc_a}[2]}}$	$\textcolor{#87AAB3}{{\vec{s}_f}}$
  $\textcolor{#DAA7AA}{{s_i[0]}}$	$\textcolor{#DAA7AA}{{s_i[1]}}$	$\textcolor{#DAA7AA}{{s_i[2]}}$	$\textcolor{#87AAB3}{{rc_i[0]}}$	$\textcolor{#87AAB3}{{rc_i[1]}}$	$\textcolor{#87AAB3}{{rc_i[2]}}$	$\textcolor{#87AAB3}{{v}}$
  $\textcolor{#DAA7AA}{{s_{i+1}[0]}}$	$\textcolor{#DAA7AA}{{s_{i+1}[1]}}$	$\textcolor{#DAA7AA}{{s_{i+1}[2]}}$

  full 라운드 에서의 $i$ 라운드의 state 에 적용할 연산을 표현하기 위해 표현식을 다음과 같이 정의하자.
  $\quad$

  $\begin{matrix} expr_k = \sum_{j=0..2}\{(s_i[j]+rc_i[j])^5*m_k[j]\} \end{matrix}$

  $\quad$
  그러면 $expr_k$ 는 $i+1$ 라운드의 state 구하기 위한 연산과 동일한 제약식을 표현한다. full 라운드의 제약식은 selector $\vec{s}_f$와 함께 정의되며, 위의 표에서와 같이 $\vec{s}_f$ 가 가지는 값을 $v$ 라고 하면, 최종적으로 얻는 full 라운드 gate가 만족해야 하는 식을 다음과 같이 정의하자.
  $\quad$

  $\begin{matrix} v*(expr_0-s_{i+1}[0])=0\\ \quad \\ v*(expr_1-s_{i+1}[1])=0\\ \quad \\ v*(expr_2-s_{i+1}[2])=0 \end{matrix}$

  $\quad$

  위의 식은 $v=1$ 일때, $k=0,1,2$ 에 대해서 $expr_k$ 와 $s_{i+1}[k]$ 가 같아야 함을 의미한다. 이 조건이 충족될 경우, $s_{i+1}[k]$ 에는 $s_i[k]$ 값에 full 라운드 연산이 올바르게 수행된 결과가 할당되어 있음을 확인할 수 있다.

  $\quad$

• partial round single
partial round single은 full round와 거의 동일한 연산을 수행하지만 $x^5$ 연산을 첫번째 state 에만 적용한다는 점이 다르다.

  $\textcolor{#DAA7AA}{{\vec{s}[0]}}$	$\textcolor{#DAA7AA}{{\vec{s}[1]}}$	$\textcolor{#DAA7AA}{{\vec{s}[2]}}$	$\textcolor{#87AAB3}{{\vec{rc}_a[0]}}$	$\textcolor{#87AAB3}{{\vec{rc}_a[1]}}$	$\textcolor{#87AAB3}{{\vec{rc}_a[2]}}$	$\textcolor{#87AAB3}{{\vec{s}_p}}$
  $\textcolor{#DAA7AA}{{s_i[0]}}$	$\textcolor{#DAA7AA}{{s_i[1]}}$	$\textcolor{#DAA7AA}{{s_i[2]}}$	$\textcolor{#87AAB3}{{a_i[0]}}$	$\textcolor{#87AAB3}{{a_i[1]}}$	$\textcolor{#87AAB3}{{a_i[2]}}$	$\textcolor{#87AAB3}{v}$
  $\textcolor{#DAA7AA}{{s_{i+1}[0]}}$	$\textcolor{#DAA7AA}{{s_{i+1}[1]}}$	$\textcolor{#DAA7AA}{{s_{i+1}[2]}}$

  partial round single의 gate는 selector $\vec{s}_p$ 와 함께 정의되며, 이때, 다음 라운드의 state 를 구하는 연산은 다음과 같다.
  $\quad$

  $\begin{matrix} expr_k =(s_i[0]+a_i[0])^5*m_k[0] + (s_i[1]+a_i[1])*m_k[1] +(s_i[2]+a_i[2])*m_k[2] \end{matrix}$

  $\quad$
  제약식은 selector $\vec{s}_p$와 함께 정의되며, 마찬가지로 $\vec{s}_p$ 가 가지는 값을 $v$ 라고 할때, gate의 제약식들은 다음과 같다.
  $\quad$

  $\begin{matrix} v*(expr_0-s_{i+1}[0])\\ \quad \\ v*(expr_1-s_{i+1}[1])\\ \quad \\ v*(expr_2-s_{i+1}[2]) \end{matrix}$

  $\quad$
  

• partial round
partial round로 정의되는 게이트에서는 partial 라운드 두번에 대한 제약조건들을 한번에 정의한다. 이를 위해서 추가로 advice column $\vec{s}_{tmp}$ 와 fixed column $\vec{rc}_b[k]$ 를 할당해서 제약을 준다. $\vec{rc}_a[k]$ 는 $i$ 라운드의 상수, $\vec{rc}_b[k]$ 는 $i+1$ 라운드의 상수를 할당할 위치이다.

  $\textcolor{#DAA7AA}{{\vec{s}[0]}}$	$\textcolor{#DAA7AA}{{\vec{s}[1]}}$	$\textcolor{#DAA7AA}{{\vec{s}[2]}}$	$\textcolor{#DAA7AA}{{\vec{s}_{tmp}}}$	$\textcolor{#87AAB3}{{\vec{rc}_a[0]}}$	$\textcolor{#87AAB3}{{\vec{rc}_a[1]}}$	$\textcolor{#87AAB3}{{\vec{rc}_a[2]}}$	$\textcolor{#87AAB3}{{\vec{rc}_b[0]}}$	$\textcolor{#87AAB3}{{\vec{rc}_b[1]}}$	$\textcolor{#87AAB3}{{\vec{rc}_b[2]}}$	$\textcolor{#87AAB3}{{\vec{s}_{2p}}}$
  $\textcolor{#DAA7AA}{{s_i[0]}}$	$\textcolor{#DAA7AA}{{s_i[1]}}$	$\textcolor{#DAA7AA}{{s_i[2]}}$	$\textcolor{#DAA7AA}{{t_i}}$	$\textcolor{#87AAB3}{{a_i[0]}}$	$\textcolor{#87AAB3}{{a_i[1]}}$	$\textcolor{#87AAB3}{{a_i[2]}}$	$\textcolor{#87AAB3}{{b_i[0]}}$	$\textcolor{#87AAB3}{{b_i[1]}}$	$\textcolor{#87AAB3}{{b_i[2]}}$	$\textcolor{#87AAB3}{v}$
  $\textcolor{#DAA7AA}{{s_{i+2}[0]}}$	$\textcolor{#DAA7AA}{{s_{i+2}[1]}}$	$\textcolor{#DAA7AA}{{s_{i+2}[2]}}$

  partial 라운드 gate는 selector $\vec{s}_{2p}$ 의 상대적 위치로 정의되는데, 라운드 두번에 대한 제약조건들을 하나의 행에서 정의하여 $i$ 라운드의 state를 입력으로 $i+2$ 라운드의 state를 포함하는 제약조건식들을 출력하도록 설계할 수 있다. 위 표에서 $i$ 라운드의 첫번째 state에 비선형 연산을 적용한 결과를 $t_i = (s_i[0] + a_i[0])^5$ 로 정의하고 partial 라운드의 gate를 정의하기 위해 필요한 중간 값들을 다음과 같이 정의하자.
  $\quad$

  $\begin{matrix}mid_k =t_i*m_k[0] + (s_i[1]+a_i[1])*m_k[1] +(s_i[2]+a_i[2])*m_k[2]\\ \quad \\ next_k=s_{i+2}[0]*n_k[0]+s_{i+2}[1]*n_k[1]+s_{i+2}[2]*n_k[2] \end{matrix}$

  $\quad$
  $mid_k$는 $s_{i+1}[k]$ 에 대응되는 값이며 $next_k$ 는 $s_{i+1}[k]$ 에 라운드 상수를 더하고 첫번째 성분에만 비선형 연산을 적용한 값으로 mds 행렬을 곱하기 전의 state 이므로 $s_{i+1}[k]$ 와의 관계를 다음과 같이 적을 수 있다.
  $\quad$

  $\begin{matrix} next_0 = (s_{i+1}[0]+b_{i}[0])^5 \\ \quad \\ next_1 = s_{i+1}[1]+b_i[1] \\ \quad \\ next_2 = s_{i+1}[2]+b_i[2] \end{matrix}$

  $\quad$
  partial 라운드의 selector $\vec{s}_{2p}$ 의 현재 행에서 값을 $v$ 라고 하고 gate의 제약식들을 다음과 같이 정의하자.
  $\quad$

  $\begin{matrix} v*(t_i - (s_i[0]+a_i[0])^5)=0\\ \quad \\ v*((mid_0+b_i[0])^5-next_0)=0\\ \quad \\ v*((mid_1+b_i[1])-next_1)=0\\ \quad \\ v*((mid_2+b_i[2])-next_2)=0 \end{matrix}$

  $\quad$
  그러면, $v=1$ 의 조건하에서 제약 조건을 circuit 에 추가할 수 있으며, 이 방법을 통해 partial round single gate만 활용하는 경우보다 행의 수가 거의 절반으로 감소하는 효과를 얻을 수 있다.
  $\quad$
  $\quad$

Combining all gateaints

각 gate의 호출 순서 및 횟수는 다음과 같다.
    1. [full round] * 4
    2. [partial round] * 28
    3. [partial round single] * 1
    4. [full round] * 4 

$\textsf{row}$	$\textcolor{#DAA7AA}{\vec{s}[0]}$	$\textcolor{#DAA7AA}{\vec{s}[1]}$	$\textcolor{#DAA7AA}{\vec{s}[2]}$	$\textcolor{#DAA7AA}{\vec{s}_{tmp}}$	$\textcolor{#87CEEB}{\vec{rc}_a[0]}$	$\textcolor{#87CEEB}{\vec{rc}_a[1]}$	$\textcolor{#87CEEB}{\vec{rc}_a[2]}$	$\textcolor{#87CEEB}{\vec{rc}_b[0]}$	$\textcolor{#87CEEB}{\vec{rc}_b[1]}$	$\textcolor{#87CEEB}{\vec{rc}_b[2]}$	$\textcolor{#87CEEB}{\vec{s}_{f}}$	$\textcolor{#87CEEB}{\vec{s}_{2p}}$	$\textcolor{#87CEEB}{\vec{s}_p}$
$0$	$\textcolor{#DAA7AA}{s_0[0]}$	$\textcolor{#DAA7AA}{s_0[1]}$	$\textcolor{#DAA7AA}{s_0[2]}$	$\textcolor{#DAA7AA}{-}$	$\textcolor{#87CEEB}{rc_0[0]}$	$\textcolor{#87CEEB}{rc_0[1]}$	$\textcolor{#87CEEB}{rc_0[2]}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{1}$	$\textcolor{#87CEEB}{0}$	$\textcolor{#87CEEB}{0}$
$1$	$\textcolor{#DAA7AA}{s_1[0]}$	$\textcolor{#DAA7AA}{s_1[1]}$	$\textcolor{#DAA7AA}{s_1[2]}$	$\textcolor{#DAA7AA}{{-}}$	$\textcolor{#87CEEB}{{rc_1[0]}}$	$\textcolor{#87CEEB}{{rc_1[1]}}$	$\textcolor{#87CEEB}{{rc_1[2]}}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{1}$	$\textcolor{#87CEEB}{0}$	$\textcolor{#87CEEB}{0}$
$2$	$\textcolor{#DAA7AA}{s_2[0]}$	$\textcolor{#DAA7AA}{s_2[1]}$	$\textcolor{#DAA7AA}{s_2[2]}$	$\textcolor{#DAA7AA}{{-}}$	$\textcolor{#87CEEB}{{rc_2[0]}}$	$\textcolor{#87CEEB}{{rc_2[1]}}$	$\textcolor{#87CEEB}{{rc_2[2]}}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{1}$	$\textcolor{#87CEEB}{0}$	$\textcolor{#87CEEB}{0}$
$3$	$\textcolor{#DAA7AA}{s_3[0]}$	$\textcolor{#DAA7AA}{s_3[1]}$	$\textcolor{#DAA7AA}{s_3[2]}$	$\textcolor{#DAA7AA}{{-}}$	$\textcolor{#87CEEB}{{rc_3[0]}}$	$\textcolor{#87CEEB}{{rc_3[1]}}$	$\textcolor{#87CEEB}{{rc_3[2]}}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{1}$	$\textcolor{#87CEEB}{0}$	$\textcolor{#87CEEB}{0}$
$4$	$\textcolor{#DAA7AA}{s_4[0]}$	$\textcolor{#DAA7AA}{s_4[1]}$	$\textcolor{#DAA7AA}{s_4[2]}$	$\textcolor{#DAA7AA}{{t_4}}$	$\textcolor{#87CEEB}{{rc_4[0]}}$	$\textcolor{#87CEEB}{{rc_4[1]}}$	$\textcolor{#87CEEB}{{rc_4[2]}}$	$\textcolor{#87CEEB}{{rc_5[0]}}$	$\textcolor{#87CEEB}{{rc_5[1]}}$	$\textcolor{#87CEEB}{{rc_5[2]}}$	$\textcolor{#87CEEB}{{0}}$	$\textcolor{#87CEEB}{{1}}$	$\textcolor{#87CEEB}{{0}}$
$5$	$\textcolor{#DAA7AA}{s_6[0]}$	$\textcolor{#DAA7AA}{s_6[1]}$	$\textcolor{#DAA7AA}{s_6[2]}$	$\textcolor{#DAA7AA}{{t_6}}$	$\textcolor{#87CEEB}{{rc_6[0]}}$	$\textcolor{#87CEEB}{{rc_6[1]}}$	$\textcolor{#87CEEB}{{rc_6[2]}}$	$\textcolor{#87CEEB}{{rc_7[0]}}$	$\textcolor{#87CEEB}{{rc_7[1]}}$	$\textcolor{#87CEEB}{{rc_7[2]}}$	$\textcolor{#87CEEB}{{0}}$	$\textcolor{#87CEEB}{{1}}$	$\textcolor{#87CEEB}{{0}}$
$...$	$\textcolor{#DAA7AA}{{...}}$	$\textcolor{#DAA7AA}{{...}}$	$\textcolor{#DAA7AA}{{...}}$	$\textcolor{#DAA7AA}{{...}}$	$\textcolor{#87CEEB}{{...}}$	$\textcolor{#87CEEB}{{...}}$	$\textcolor{#87CEEB}{{...}}$	$\textcolor{#87CEEB}{{...}}$	$\textcolor{#87CEEB}{{...}}$	$\textcolor{#87CEEB}{{...}}$	$\textcolor{#87CEEB}{{...}}$	$\textcolor{#87CEEB}{{...}}$	$\textcolor{#87CEEB}{{...}}$
$31$	$\textcolor{#DAA7AA}{s_{58}[0]}$	$\textcolor{#DAA7AA}{s_{58}[1]}$	$\textcolor{#DAA7AA}{s_{58}[2]}$	$\textcolor{#DAA7AA}{{t_{58}}}$	$\textcolor{#87CEEB}{{rc_{58}[0]}}$	$\textcolor{#87CEEB}{{rc_{58}[1]}}$	$\textcolor{#87CEEB}{{rc_{58}[2]}}$	$\textcolor{#87CEEB}{{rc_{59}[0]}}$	$\textcolor{#87CEEB}{{rc_{59}[1]}}$	$\textcolor{#87CEEB}{{rc_{59}[2]}}$	$\textcolor{#87CEEB}{{0}}$	$\textcolor{#87CEEB}{{1}}$	$\textcolor{#87CEEB}{{0}}$
$32$	$\textcolor{#DAA7AA}{s_{60}[0]}$	$\textcolor{#DAA7AA}{s_{60}[1]}$	$\textcolor{#DAA7AA}{s_{60}[2]}$	$\textcolor{#DAA7AA}{{-}}$	$\textcolor{#87CEEB}{{rc_{60}[0]}}$	$\textcolor{#87CEEB}{{rc_{60}[1]}}$	$\textcolor{#87CEEB}{{rc_{60}[2]}}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{{0}}$	$\textcolor{#87CEEB}{{0}}$	$\textcolor{#87CEEB}{{1}}$
$33$	$\textcolor{#DAA7AA}{s_{61}[0]}$	$\textcolor{#DAA7AA}{s_{61}[1]}$	$\textcolor{#DAA7AA}{s_{61}[2]}$	$\textcolor{#DAA7AA}{{-}}$	$\textcolor{#87CEEB}{{rc_{61}[0]}}$	$\textcolor{#87CEEB}{{rc_{61}[1]}}$	$\textcolor{#87CEEB}{{rc_{61}[2]}}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{{1}}$	$\textcolor{#87CEEB}{{0}}$	$\textcolor{#87CEEB}{{0}}$
$...$	$\textcolor{#DAA7AA}{...}$	$\textcolor{#DAA7AA}{...}$	$\textcolor{#DAA7AA}{...}$	$\textcolor{#DAA7AA}{...}$	$\textcolor{#87CEEB}{...}$	$\textcolor{#87CEEB}{...}$	$\textcolor{#87CEEB}{...}$	$\textcolor{#87CEEB}{...}$	$\textcolor{#87CEEB}{...}$	$\textcolor{#87CEEB}{...}$	$\textcolor{#87CEEB}{...}$	$\textcolor{#87CEEB}{..}$	$\textcolor{#87CEEB}{...}$
$36$	$\textcolor{#DAA7AA}{s_{64}[0]}$	$\textcolor{#DAA7AA}{s_{64}[1]}$	$\textcolor{#DAA7AA}{s_{64}[2]}$	$\textcolor{#DAA7AA}{{-}}$	$\textcolor{#87CEEB}{{rc_{64}[0]}}$	$\textcolor{#87CEEB}{{rc_{64}[1]}}$	$\textcolor{#87CEEB}{{rc_{64}[2]}}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{{1}}$	$\textcolor{#87CEEB}{{0}}$	$\textcolor{#87CEEB}{{0}}$
$37$	$\textcolor{#DAA7AA}{s_{65}[0]}$	$\textcolor{#DAA7AA}{s_{65}[1]}$	$\textcolor{#DAA7AA}{s_{65}[2]}$	$\textcolor{#DAA7AA}{{-}}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{-}$	$\textcolor{#87CEEB}{0}$	$\textcolor{#87CEEB}{{0}}$	$\textcolor{#87CEEB}{{0}}$

$\quad$
위 표는 permutation의 입출력 및 연산과정에서 발생하는 중간값들로 채워지며, ${s_i[k]}$와 ${rc_i[k]}$ 는 각각 라운드 $i$에서의 state와 라운드 상수를 의미한다. ${\vec{s}_{tmp}}$와 ${\vec{rc}_b[k]}$ 는 각각 partial round에서만 할당되는 advice column과 fixed column이다. 라운드의 진행에 따라 표의 값들이 채워지는 순서는 다음과 같다.

- 처음의 full 라운드는 0-3행을 채운다.
- partial 라운드는 4-32행을 채운다.
- 마지막 full 라운드는 33-36행을 채운다. 

$37$행의 ${s_{65}[0], s_{65}[1], s_{65}[2]}$는 permutation 연산의 출력이다. 출력 값의 행을 포함하여 최종적으로 얻게되는 표는 $38$개의 row, $4$개의 advice column과 $9$개의 fixed column 으로 구성된다.
$\quad$
$\quad$
$\quad$

4. 코드 분석

1) Spec

• Spec & Mds

  // T by T 정방행렬인 MDS와 그 역행렬의 타입
  pub(crate) type Mds<F, const T: usize> = [[F; T]; T];
  
  // poseidon permutation에 대한 파라미터를 정의
  pub trait Spec<F: FieldExt, const T: usize, const RATE: usize>: fmt::Debug {
  
      fn full_rounds() -> usize;
  
      fn partial_rounds() -> usize;
  
      fn sbox(val: F) -> F;
  
  	// constants()를 하드코딩하는 경우 정의하지 않아도 됨
      fn secure_mds() -> usize;
  
      // 정의된 파라미터에 따른 (round_constants, mds, mds^-1) 생성
  	// 하드코딩 할 수도 있음
      fn constants() -> (Vec<[F; T]>, Mds<F, T>, Mds<F, T>) {
          let r_f = Self::full_rounds();
          let r_p = Self::partial_rounds();
  
          let mut grain = grain::Grain::new(SboxType::Pow, T as u16, r_f as u16, r_p as u16);
  
          let round_constants = (0..(r_f + r_p))
              .map(|_| {
                  let mut rc_row = [F::zero(); T];
                  for (rc, value) in rc_row
                      .iter_mut()
                      .zip((0..T).map(|_| grain.next_field_element()))
                  {
                      *rc = value;
                  }
                  rc_row
              })
              .collect();
  
          let (mds, mds_inv) = mds::generate_mds::<F, T>(&mut grain, Self::secure_mds());
  
          (round_constants, mds, mds_inv)
      }
  }

  $\quad$
  specification의 약자로 permutation에 필요한 full/partial 라운드 횟수, s-box, MDS 행렬등을 정의하는 트레잇이다. constants()함수를 호출하면 (round_constants, mds, mds^-1)의 결과를 반환한다. 라운드 상수와 MDS 행렬, 그리고 그 역행렬은 Width에 해당하는 T값과 RF, RP에 따라 결정되는 값들이기 때문에 미리 계산해 두고 하드코딩된 값을 사용할 수 있다.
  $\quad$
  

2) Pow5Chip

  Pow5Chip`은 다음의 라운드들로 구성된 permutation circuit을 구현한다.
  	[0-3 rows]: 4 * full 라운드
    [4-31 rows]:  28 * (2 partial 라운드)
    [32 rows]: 1 partial 라운드
    [4-7 rows]: 4 * full 라운드

$\quad$

• Pow5Config

  pub struct Pow5Config<F: FieldExt, const WIDTH: usize, const RATE: usize> {
      pub(crate) state: [Column<Advice>; WIDTH],
      partial_sbox: Column<Advice>,
      rc_a: [Column<Fixed>; WIDTH],
      rc_b: [Column<Fixed>; WIDTH],
      s_full: Selector,
      s_partial: Selector,
      s_partial_single: Selector,
      s_pad_and_add: Selector,
  
      half_full_rounds: usize,
      half_partial_rounds: usize,
      alpha: [u64; 4],
      round_constants: Vec<[F; WIDTH]>,
      m_reg: Mds<F, WIDTH>,
      m_inv: Mds<F, WIDTH>,
  }

  Pow5Chip을 구성하는 값들은 위와 같다. Advice 및 Fixed 는 각 gate의 입출력 값이며, Seletor는 $0$ 과 $1$ 의 값으로 구성되어 gated의 제약조건을 확인하거나 하지않도록 조절하는 스위치의 역할을 한다. 그 이외의 값들은 Fixed 혹은 gate를 정의하기위해 사용된다.
  참고로 Scroll의 구현에는 s_pad_and_add selector 가 정의되어 있지만 입력의 패딩에 대한 제약조건을 주기 위한 것으로 이 글에서는 다루지 않는다.
  $\quad$

• full round

  meta.create_gate("full round", |meta| {
      let s_full = meta.query_selector(s_full);
  
      (0..WIDTH)
          .map(|next_idx| {
              let state_next = meta.query_advice(state[next_idx], Rotation::next());
              let expr = (0..WIDTH)
                  .map(|idx| {
                      let state_cur = meta.query_advice(state[idx], Rotation::cur());
                      let rc_a = meta.query_fixed(rc_a[idx], Rotation::cur());
                      pow_5(state_cur + rc_a) * m_reg[next_idx][idx]
                  })
                  .reduce(|acc, term| acc + term)
                  .expect("WIDTH > 0");
              s_full.clone() * (expr - state_next)
          })
          .collect::<Vec<_>>()
  });

  full round에 대한 create_gate 함수는 $3$장에서 설명한 full 라운드의 gate를 정의하고 있으며 s_full 는 full 라운드로 정의된 gate에 대한 selector 이다. state_cur와 state_next는 advice column을 참조하며, rc_a은 fixed column을 참조한다. m_reg는 입출력과는 독립적인 gate 내부 값이다.
  $\quad$

• partial round single

  meta.create_gate("partial round single", |meta| {
    let s_partial_single = meta.query_selector(s_partial_single);
  
    (0..WIDTH)
        .map(|next_idx| {
            let state_next = meta.query_advice(state[next_idx], Rotation::next());
            let cur_0 = meta.query_advice(state[0], Rotation::cur());
            let rc_a0 = meta.query_fixed(rc_a[0], Rotation::cur());
  
            let expr = pow_5(cur_0 + rc_a0) * m_reg[next_idx][0];
            let expr = expr
                + (1..WIDTH)
                    .map(|idx| {
                        let state_cur = meta.query_advice(state[idx], Rotation::cur());
                        let rc_a = meta.query_fixed(rc_a[idx], Rotation::cur());
                        (state_cur + rc_a) * m_reg[next_idx][idx]
                    })
                    .reduce(|acc, term| acc + term)
                    .expect("WIDTH > 0");
            s_partial_single.clone() * (expr - state_next)
        })
        .collect::<Vec<_>>()
  });

  s_partial_single 은 partial round single 로 정의된 gate에 대한 selector 이다. cur_0와 rc_a0는 각각 비선형 연산을 적용할 첫번째 state의 advice column 과 그에 대응되는 라운드 상수의 fixed column을 참조한다. 이전과 마찬가지로 m_reg는 gate 내부에서 사용되며, 결과적으로 $3$장에서 설명한 것과 동일한 제약조건식을 정의하고 있다.
  $\quad$
  

• partial round

  meta.create_gate("partial rounds", |meta| {
      let cur_0 = meta.query_advice(state[0], Rotation::cur());
      let mid_0 = meta.query_advice(partial_sbox, Rotation::cur());
  
      let rc_a0 = meta.query_fixed(rc_a[0], Rotation::cur());
      let rc_b0 = meta.query_fixed(rc_b[0], Rotation::cur());
  
      let s_partial = meta.query_selector(s_partial);
  
      use halo2_proofs::plonk::VirtualCells;
      let mid = |idx: usize, meta: &mut VirtualCells<F>| {
          let mid = mid_0.clone() * m_reg[idx][0];
          (1..WIDTH).fold(mid, |acc, cur_idx| {
              let cur = meta.query_advice(state[cur_idx], Rotation::cur());
              let rc_a = meta.query_fixed(rc_a[cur_idx], Rotation::cur());
              acc + (cur + rc_a) * m_reg[idx][cur_idx]
          })
      };
  
      let next = |idx: usize, meta: &mut VirtualCells<F>| {
          (0..WIDTH)
              .map(|next_idx| {
                  let next = meta.query_advice(state[next_idx], Rotation::next());
                  next * m_inv[idx][next_idx]
              })
              .reduce(|acc, next| acc + next)
              .expect("WIDTH > 0")
      };
  
      let partial_round_linear = |idx: usize, meta: &mut VirtualCells<F>| {
          let rc_b = meta.query_fixed(rc_b[idx], Rotation::cur());
          mid(idx, meta) + rc_b - next(idx, meta)
      };
  
      std::iter::empty()
          // state[0] round a
          .chain(Some(pow_5(cur_0 + rc_a0) - mid_0.clone()))
          // state[0] round b
          .chain(Some(pow_5(mid(0, meta) + rc_b0) - next(0, meta)))
          .chain((1..WIDTH).map(|idx| partial_round_linear(idx, meta)))
          .map(|exp| s_partial.clone() * exp)
          .collect::<Vec<_>>()
  });

  gate 정의의 마지막에서는 클로저로 정의된 변수들을 체인으로 연결하여 최종적인 제약조건 식들을 생성한다.

  • 첫번째 체인함수: mid_0 와 비선형 연산의 결과 pow_5(cur_0 + rc_a0) 의 차를 정의한다.

  • 두번째 체인함수: 클로저로 정의된 mid 와 next 의 첫번째 성분을 호출하고 있으며 각 클로저에서 정의되는 연산은 다음과 같다.

    • mid: 클로저 호출시, 앞서 비선형 연산으로 얻은 mid_0 값을 이용해서 partial 라운드 를 한번 수행한 결과의 state 를 리턴한다. 즉, 현재 $i$ 라운드의 다음 라운드인 $i+1$ 라운드의 state 를 리턴한다.
    • next: 클로저 호출시, Rotation::next() 인덱스에 대응되는 state 를 참조하여 mds 연산을 수행하기 이전의 값들을 리턴한다. 여기서, Rotation::next() 는 현재 행의 바로 다음에 있는 행을 의미한다.

    결과적으로 두번째 체인에서는 $i+1$ 라운드의 첫번째 state 에 다음번 partial 라운드의 결과를 얻기 위한 연산을 수행(단, mds 행렬곱 이전까지의 연산)한 값과 $i+2$ 라운드의 첫번째 state 에 mds 행렬의 역연산을 수행한 값의 차를 구한다.

  • 세번째 체인함수: partial_round_linear 에서 mid 와 next 의 첫번째 성분을 제외한 나머지 성분들을 호출하고 있다. mid 를 호출하여 $i+1$ 라운드의 state 들에 라운드 상수를 더한 값과 next 의 값의 차를 구한다.
    $\quad$

  또한, 마지막의 map 함수에서는 체인들로 연결된 각 연산들의 차에 s_partial 을 곱한 식을 최종 벡터로 정의한다.

$\quad$

5. 정리

Scroll 의 Poseidon hash 구현 코드를 기준으로 circuit 의 설계 방법을 정리해 보았다. 설계에서 주목할 점은 partial round single 과 partial round 를 구분해서 gate를 정의한 것이다. partial round 에서 하나의 행에 두개의 라운드에 대한 제약조건들을 표현한다. 이를 위해서 $i$ 라운드의 $ARC$, $s$-$box$, $MDS$ 연산을 $mid_k$로 저장하고, $i+2$ 라운드의 state벡터에는 $MDS$의 역연산 이용해서 각각 $i+1$ 라운드와의 연결고리를 만들어 제약 조건을 확인한다. 이를 위해서 추가로 하나의 advice column 과 세개의 fixed column 을 추가로 도입하면면서 최종적으로는 $4$ 개의 열이 증가하였지만, $26$ 개의 행을 감소시킬 수 있었다.
Halo2 를 사용했을때, 일반적으로 column 의 갯수는 증명의 크기와 비례하고 행의 갯수는 증명 생성시 다항식의 차수에 영향을 주어 proof 생성 시간에 비례하므로 partial round 의 도입은 proof size 의 증가와 proof 생성 시간의 감소를 가져올 것으로 예상할 수 있다. proof 생성 시간이 성능에 결정적인 영향을 주는 환경에서는 이러한 최적화 전략의 설계가 필수적이다. Scroll 의 Poseidon hash의 최적화 설계 버전에서는 이와 같은 방안을 고려하여 설계되었는데, 이에 대한 자세한 내용은 다음 포스트에서 다루도록 하겠다.