You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

358 lines
14 KiB

  1. \documentclass{article}
  2. \usepackage[utf8]{inputenc}
  3. \usepackage{amsfonts}
  4. \usepackage{amsthm}
  5. \usepackage{amsmath}
  6. \usepackage{mathtools}
  7. \usepackage{enumerate}
  8. \usepackage{hyperref}
  9. \usepackage{xcolor}
  10. \usepackage{centernot}
  11. \usepackage{algorithm}
  12. \usepackage{algpseudocode}
  13. \usepackage{pgf-umlsd} % diagrams
  14. % message between threads. From https://tex.stackexchange.com/a/174765
  15. % Example:
  16. % \bloodymess[delay]{sender}{message content}{receiver}{DIR}{start note}{end note}
  17. \newcommand{\bloodymess}[7][0]{
  18. \stepcounter{seqlevel}
  19. \path
  20. (#2)+(0,-\theseqlevel*\unitfactor-0.7*\unitfactor) node (mess from) {};
  21. \addtocounter{seqlevel}{#1}
  22. \path
  23. (#4)+(0,-\theseqlevel*\unitfactor-0.7*\unitfactor) node (mess to) {};
  24. \draw[->,>=angle 60] (mess from) -- (mess to) node[midway, above]
  25. {#3};
  26. \if R#5
  27. \node (\detokenize{#3} from) at (mess from) {\llap{#6~}};
  28. \node (\detokenize{#3} to) at (mess to) {\rlap{~#7}};
  29. \else\if L#5
  30. \node (\detokenize{#3} from) at (mess from) {\rlap{~#6}};
  31. \node (\detokenize{#3} to) at (mess to) {\llap{#7~}};
  32. \else
  33. \node (\detokenize{#3} from) at (mess from) {#6};
  34. \node (\detokenize{#3} to) at (mess to) {#7};
  35. \fi
  36. \fi
  37. }
  38. % prevent warnings of underfull \hbox:
  39. \usepackage{etoolbox}
  40. \apptocmd{\sloppy}{\hbadness 4000\relax}{}{}
  41. \theoremstyle{definition}
  42. \newtheorem{definition}{Def}[section]
  43. \newtheorem{theorem}[definition]{Thm}
  44. % custom lemma environment to set custom numbers
  45. \newtheorem{innerlemma}{Lemma}
  46. \newenvironment{lemma}[1]
  47. {\renewcommand\theinnerlemma{#1}\innerlemma}
  48. {\endinnerlemma}
  49. \title{Notes on HyperNova}
  50. \author{arnaucube}
  51. \date{May 2023}
  52. \begin{document}
  53. \maketitle
  54. \begin{abstract}
  55. Notes taken while reading about HyperNova \cite{cryptoeprint:2023/573} and CCS\cite{cryptoeprint:2023/552}.
  56. Usually while reading papers I take handwritten notes, this document contains some of them re-written to $LaTeX$.
  57. The notes are not complete, don't include all the steps neither all the proofs.
  58. Thanks to \href{https://twitter.com/asn_d6}{George Kadianakis} for clarifications, and the authors \href{https://twitter.com/srinathtv}{Srinath Setty} and \href{https://twitter.com/abhiramko}{Abhiram Kothapalli} for answers on chats and twitter.
  59. \end{abstract}
  60. \tableofcontents
  61. \section{CCS}
  62. \subsection{R1CS to CCS overview}
  63. \begin{description}
  64. \item[R1CS instance] $S_{R1CS} = (m, n, N, l, A, B, C)$\\
  65. where $m, n$ are such that $A \in \mathbb{F}^{m \times n}$, and $l$ such that the public inputs $x \in \mathbb{F}^l$. Also $z=(w, 1, x) \in \mathbb{F}^n$, thus $w \in \mathbb{F}^{n-l-1}$.
  66. \item[CCS instance] $S_{CCS} = (m, n, N, l, t, q, d, M, S, c)$\\
  67. where we have the same parameters than in $S_{R1CS}$, but additionally:\\
  68. $t=|M|$, $q = |c| = |S|$, $d$= max degree in each variable.
  69. \item[R1CS-to-CCS parameters] $n=n,~ m=m,~ N=N,~ l=l,~ t=3,~ q=2,~ d=2$, $M=\{A,B,C\}$, $S=\{\{0,~1\},~ \{2\}\}$, $c=\{1,-1\}$
  70. \end{description}
  71. The CCS relation check:
  72. $$\sum_{i=0}^{q-1} c_i \cdot \bigcirc_{j \in S_i} M_j \cdot z ==0$$
  73. where $z=(w, 1, x) \in \mathbb{F}^n$.
  74. In our R1CS-to-CCS parameters is equivalent to
  75. \begin{align*}
  76. &c_0 \cdot ( (M_0 z) \circ (M_1 z) ) + c_1 \cdot (M_2 z) ==0\\
  77. \Longrightarrow &1 \cdot ( (A z) \circ (B z) ) + (-1) \cdot (C z) ==0\\
  78. \Longrightarrow &( (A z) \circ (B z) ) - (C z) ==0
  79. \end{align*}
  80. which is equivalent to the R1CS relation: $Az \circ Bz == Cz$
  81. An example of the conversion from R1CS to CCS implemented in SageMath can be found at\\
  82. \href{https://github.com/arnaucube/math/blob/master/r1cs-ccs.sage}{https://github.com/arnaucube/math/blob/master/r1cs-ccs.sage}.
  83. Similar relations between Plonkish and AIR arithmetizations to CCS are shown in the CCS paper \cite{cryptoeprint:2023/552}, but for now with the R1CS we have enough to see the CCS generalization idea and to use it for the HyperNova scheme.
  84. \subsection{Committed CCS}
  85. $R_{CCCS}$ instance: $(C, \mathsf{x})$, where $C$ is a commitment to a multilinear polynomial in $s'-1$ variables.
  86. Sat if:
  87. \begin{enumerate}[i.]
  88. \item $\text{Commit}(pp, \widetilde{w}) = C$
  89. \item $\sum_{i=1}^q c_i \cdot \left( \prod_{j \in S_i} \left( \sum_{y \in \{0,1\}^{\log m}} \widetilde{M}_j(x, y) \cdot \widetilde{z}(y) \right) \right)$\\
  90. where $\widetilde{z}(y) = \widetilde{(w, 1, \mathsf{x})}(x) ~\forall x \in \{0, 1\}^{s'}$
  91. \end{enumerate}
  92. \subsection{Linearized Committed CCS}
  93. $R_{LCCCS}$ instance: $(C, u, \mathsf{x}, r, v_1, \ldots, v_t)$, where $C$ is a commitment to a multilinear polynomial in $s'-1$ variables, and $u \in \mathbb{F},~ \mathsf{x} \in \mathbb{F}^l,~ r \in \mathbb{F}^s,~ v_i \in \mathbb{F} ~\forall i \in [t]$.
  94. Sat if:
  95. \begin{enumerate}[i.]
  96. \item $\text{Commit}(pp, \widetilde{w}) = C$
  97. \item $\forall i \in [t],~ v_i = \sum_{y \in \{0,1\}^{s'}} \widetilde{M}_i(r, y) \cdot \widetilde{z}(y)$\\
  98. where $\widetilde{z}(y) = \widetilde{(w, u, \mathsf{x})}(x) ~\forall x \in \{0, 1\}^{s'}$
  99. \end{enumerate}
  100. \section{Multifolding Scheme for CCS}
  101. Recall sum-check protocol notation: \underline{$C \leftarrow \langle P, V(r) \rangle (g, l, d, T)$} means
  102. $$T=\sum_{x_1 \in \{0,1\}} \sum_{x_2 \in \{0,1\}} \cdots \sum_{x_l \in \{0,1\}} g(x_1, x_2, \ldots, x_l)$$
  103. where $g$ is a $l$-variate polynomial, with degree at most $d$ in each variable, and $T$ is the claimed value.
  104. \vspace{1cm}
  105. Let $s= \log m,~ s'= \log n$.
  106. \begin{enumerate}
  107. \item $V \rightarrow P: \gamma \in^R \mathbb{F},~ \beta \in^R \mathbb{F}^s$
  108. \item $V: r_x' \in^R \mathbb{F}^s$
  109. \item $V \leftrightarrow P$: sum-check protocol:
  110. $$c \leftarrow \langle P, V(r_x') \rangle (g, s, d+1, \underbrace{\sum_{j \in [t]} \gamma^j \cdot v_j}_\text{T})$$
  111. (in fact, $T=(\sum_{j \in [t]} \gamma^j \cdot v_j) \underbrace{+ \gamma^{t+1} \cdot Q(x)}_{=0}) = \sum_{j \in [t]} \gamma^j \cdot v_j$)\\
  112. where:
  113. \begin{align*}
  114. g(x) &:= \underbrace{\left( \sum_{j \in [t]} \gamma^j \cdot L_j(x) \right)}_\text{LCCCS check} + \underbrace{\gamma^{t+1} \cdot Q(x)}_\text{CCCS check}\\
  115. \text{for LCCCS:}~ L_j(x) &:= \widetilde{eq}(r_x, x) \cdot \left(
  116. \underbrace{\sum_{y \in \{0,1\}^{s'}} \widetilde{M}_j(x, y) \cdot \widetilde{z}_1(y)}_\text{this is the check from LCCCS}
  117. \right)\\
  118. \text{for CCCS:}~ Q(x) := &\widetilde{eq}(\beta, x) \cdot \left(
  119. \underbrace{ \sum_{i=1}^q c_i \cdot \prod_{j \in S_i} \left( \sum_{y \in \{0, 1\}^{s'}} \widetilde{M}_j(x, y) \cdot \widetilde{z}_2(y) \right) }_\text{this is the check from CCCS}
  120. \right)
  121. \end{align*}
  122. Notice that
  123. $$v_j= \sum_{y\in \{0,1\}^{s'}} \widetilde{M}_j(r, y) \cdot \widetilde{z}(y) = \sum_{x\in \{0,1\}^s} L_j(x)$$
  124. \item $P \rightarrow V$: $\left( (\sigma_1, \ldots, \sigma_t), (\theta_1, \ldots, \theta_t) \right)$, where $\forall j \in [t]$,
  125. $$\sigma_j = \sum_{y \in \{0,1\}^{s'}} \widetilde{M}_j(r_x', y) \cdot \widetilde{z}_1(y)$$
  126. $$\theta_j = \sum_{y \in \{0, 1\}^{s'}} \widetilde{M}_j(r_x', y) \cdot \widetilde{z}_2(y)$$
  127. where $\sigma_j,~\theta_j$ are the checks from LCCCS and CCCS respectively with $x=r_x'$.
  128. \item V: $e_1 \leftarrow \widetilde{eq}(r_x, r_x')$, $e_2 \leftarrow \widetilde{eq}(\beta, r_x')$\\
  129. check:
  130. $$c = \left( \sum_{j \in [t]} \gamma^j e_1 \sigma_j + \gamma^{t+1} e_2 \left( \sum_{i=1}^q c_i \cdot \prod_{j \in S_i} \sigma \right) \right)$$
  131. which should be equivalent to the $g(x)$ computed by $V,P$ in the sum-check protocol.
  132. \item $V \rightarrow P: \rho \in^R \mathbb{F}$
  133. \item $V, P$: output the folded LCCCS instance $(C', u', \mathsf{x}', r_x', v_1', \ldots, v_t')$, where $\forall i \in [t]$:
  134. \begin{align*}
  135. C' &\leftarrow C_1 + \rho \cdot C_2\\
  136. u' &\leftarrow u + \rho \cdot 1\\
  137. \mathsf{x}' &\leftarrow \mathsf{x}_1 + \rho \cdot \mathsf{x}_2\\
  138. v_i' &\leftarrow \sigma_i + \rho \cdot \theta_i
  139. \end{align*}
  140. \item $P$: output folded witness: $\widetilde{w}' \leftarrow \widetilde{w}_1 + \rho \cdot \widetilde{w}_2$.
  141. \end{enumerate}
  142. \vspace{1cm}
  143. Multifolding flow:
  144. \begin{center}
  145. \begin{sequencediagram}
  146. \newinst[1]{p}{Prover}
  147. \newinst[3]{v}{Verifier}
  148. \bloodymess[1]{v}{$\gamma,~\beta,~r_x'$}{p}{L}{
  149. \shortstack{
  150. $\gamma \in \mathbb{F},~ \beta \in \mathbb{F}^s$\\
  151. $r_x' \in \mathbb{F}^s$
  152. }
  153. }{}
  154. \bloodymess[1]{p}{$c,~ \pi_{SC}$}{v}{R}{sum-check prove}{sum-check verify}
  155. \bloodymess[1]{p}{$\{\sigma_j\},~\{\theta_j\}$}{v}{R}{compute $\{\sigma_j\}, \{\theta_j\}~ \forall j \in [t]$}{verify $c$ with $\{\sigma_j\}, \{\theta_j\}$ relation}
  156. \bloodymess[1]{v}{$\rho$}{p}{L}{$\rho \in^R \mathbb{F}$}{}
  157. \callself[0]{p}{fold LCCCS instance}{p}
  158. \prelevel
  159. \callself[0]{v}{fold LCCCS instance}{v}
  160. \callself[0]{p}{fold $\widetilde{w}$}{p}
  161. \end{sequencediagram}
  162. \end{center}
  163. \vspace{1cm}
  164. Now, to see the verifier check from step 5, observe that in LCCCS, since $\widetilde{w}$ satisfies,
  165. \begin{align*}
  166. v_j &= \sum_{y \in \{0,1\}^{s'}} \widetilde{M}_j(r_x, y) \cdot \widetilde{z}_1(y)\\
  167. &= \sum_{x \in \{0,1\}^s}
  168. \underbrace{
  169. \widetilde{eq}(r_x, x) \cdot \left( \sum_{y \in \{0,1\}^{s'}} \widetilde{M}_j(x, y) \cdot \widetilde{z}_1(y) \right)
  170. }_{L_j(x)}\\
  171. &= \sum_{x \in \{0,1\}^s} L_j(x)
  172. \end{align*}
  173. Observe also that in CCCS, since $\widetilde{w}$ satisfies,
  174. $$
  175. 0=\underbrace{\sum_{i=1}^q c_i \cdot \prod_{j \in S_i} \left( \sum_{y \in \{0, 1\}^{s'}} \widetilde{M}_j(x, y) \cdot \widetilde{z}_2(y) \right)}_{q(x)}
  176. $$
  177. we have that
  178. $$
  179. G(X) = \sum_{x \in \{0,1\}^s} eq(X, x) \cdot q(x)
  180. $$
  181. is multilinear, and can be seen as a Lagrange polynomial where coefficients are evaluations of $q(x)$ on the hypercube.
  182. For an honest prover, all these coefficients are zero, thus $G(X)$ must necessarily be the zero polynomial. Thus $G(\beta)=0$ for $\beta \in^R \mathbb{F}^s$.
  183. \begin{align*}
  184. % 0&=\sum_{i=1}^q c_i \cdot \prod_{j \in S_i} \left( \sum_{y \in \{0, 1\}^{s'}} \widetilde{M}_j(\beta, y) \cdot \widetilde{z}_2(y) \right)\\
  185. 0&=G(\beta) = \sum_{x \in \{0,1\}^s} eq(\beta, x) \cdot q(x)\\
  186. &= \sum_{x \in \{0,1\}^s}
  187. \underbrace{\widetilde{eq}(\beta , x) \cdot
  188. \overbrace{
  189. \sum_{i=1}^q c_i \cdot \prod_{j \in S_i} \left( \sum_{y \in \{0, 1\}^{s'}} \widetilde{M}_j(x, y) \cdot \widetilde{z}_2(y) \right)
  190. }^{q(x)}
  191. }_{Q(x)}\\
  192. &= \sum_{x \in \{0,1\}^s} Q(x)
  193. \end{align*}
  194. \framebox{\begin{minipage}{4.3 in}
  195. \begin{footnotesize}
  196. \textbf{Note}: notice that this past equation is related to Spartan paper \cite{cryptoeprint:2019/550}, lemmas 4.2 and 4.3, where instead of
  197. $$q(x) = \sum_{i=1}^q c_i \cdot \prod_{j \in S_i} \left( \sum_{y \in \{0, 1\}^{s'}} \widetilde{M}_j(x, y) \cdot \widetilde{z}_2(y) \right)$$
  198. for our R1CS example, we can restrict it to just $M_0,M_1,M_2$, which would be
  199. $$=\left( \sum_{y \in \{0,1\}^s} \widetilde{M_0}(x, y) \cdot \widetilde{z}(y) \right) \cdot \left( \sum_{y \in \{0,1\}^s} \widetilde{M_1}(x, y) \cdot \widetilde{z}(y) \right) - \sum_{y \in \{0,1\}^s} \widetilde{M_2}(x, y) \cdot \widetilde{z}(y)$$
  200. and we can see that $q(x)$ is the same equation $\widetilde{F}_{io}(x)$ that we had in Spartan:
  201. $$
  202. \widetilde{F}_{io}(x)=\left( \sum_{y \in \{0,1\}^s} \widetilde{A}(x, y) \cdot \widetilde{z}(y) \right) \cdot \left( \sum_{y \in \{0,1\}^s} \widetilde{B}(x, y) \cdot \widetilde{z}(y) \right) - \sum_{y \in \{0,1\}^s} \widetilde{C}(x, y) \cdot \widetilde{z}(y)
  203. $$
  204. where
  205. $$Q_{io}(t) = \sum_{x \in \{0,1\}^s} \widetilde{F}_{io}(x) \cdot \widetilde{eq}(t,x)=0$$
  206. and V checks $Q_{io}(\tau)=0$ for $\tau \in^R \mathbb{F}^s$, which in HyperNova is $G(\beta)=0$ for $\beta \in^R \mathbb{F}^s$.
  207. $Q_{io}(\cdot)$ is a zero-polynomial ($G(\cdot)$ in HyperNova), it evaluates to zero for all points in its domain iff $\widetilde{F}_{io}(\cdot)$ evaluates to zero at all points in the $s$-dimensional boolean hypercube.
  208. \begin{align*}
  209. \text{Spartan} &\longleftrightarrow \text{HyperNova}\\
  210. \tau &\longleftrightarrow \beta\\
  211. \widetilde{F}_{io}(x) &\longleftrightarrow q(x)\\
  212. Q_{io}(\tau) &\longleftrightarrow G(\beta)
  213. \end{align*}
  214. So, in HyperNova
  215. $$0 = \sum_{x \in \{0,1\}^s} Q(x) = \sum_{x \in \{0,1\}^s} \widetilde{eq}(\beta,x) \cdot q(x)$$
  216. \end{footnotesize}
  217. \end{minipage}}
  218. \vspace{1cm}
  219. Comming back to HyperNova equations, we can now see that
  220. \begin{align*}
  221. c &= g(r_x')\\
  222. &= \left( \sum_{j \in [t]} \gamma^j \cdot L_j(r_x') \right) + \gamma^{t+1} \cdot Q(r_x')\\
  223. &= \left( \sum_{j \in [t]} \gamma^j \cdot \overbrace{e_1 \cdot \sigma_j}^{L_j(r_x')} \right) + \gamma^{t+1} \cdot \overbrace{e_2 \cdot \sum_{i \in [q]} c_i \prod_{j \in S_i} \theta_j}^{Q(x)}
  224. \end{align*}
  225. where $e_1 = \widetilde{eq}(r_x, r_x')$ and $e_2=\widetilde{eq}(\beta, r_x')$.
  226. Which is the check that $V$ performs at step $5$.
  227. %%%%%% APPENDIX
  228. \appendix
  229. \section{Appendix: Some details}
  230. This appendix contains some notes on things that don't specifically appear in the paper, but that would be needed in a practical implementation of the scheme.
  231. \subsection{Matrix and Vector to Sparse Multilinear Extension}
  232. Let $M \in \mathbb{F}^{m \times n}$ be a matrix. We want to compute its MLE
  233. $$\widetilde{M}(x_1, \ldots, x_l) = \sum_{e \in \{0, 1 \}^l} M(e) \cdot \widetilde{eq}(x, e)$$
  234. We can view the matrix $M \in \mathbb{F}^{m \times n}$ as a function with the following signature:
  235. $$M(\cdot): \{0,1\}^s \times \{0,1\}^{s'} \rightarrow \mathbb{F}$$
  236. where $s = \lceil \log m \rceil,~ s' = \lceil \log n \rceil$.
  237. An entry in $M$ can be accessed with a $(s+s')$-bit identifier.
  238. eg.:
  239. $$
  240. M = \begin{pmatrix}
  241. 1 & 2 & 3\\
  242. 4 & 5 & 6\\
  243. \end{pmatrix}
  244. \in \mathbb{F}^{3 \times 2}
  245. $$
  246. $m = 3,~ n = 2,~~~ s = \lceil \log 3 \rceil = 2,~ s' = \lceil \log 2 \rceil = 1$
  247. So, $M(x, y) = x$, where $x \in \{0,1\}^s,~ y \in \{0,1\}^{s'},~ x \in \mathbb{F}$
  248. $$
  249. M = \begin{pmatrix}
  250. M(00,0) & M(01,0) & M(10,0)\\
  251. M(00,1) & M(01,1) & M(10,1)\\
  252. \end{pmatrix}
  253. \in \mathbb{F}^{3 \times 2}
  254. $$
  255. This logic can be defined as follows:
  256. \begin{algorithm}[H]
  257. \caption{Generating a Sparse Multilinear Polynomial from a matrix}
  258. \begin{algorithmic}
  259. \State set empty vector $v \in (\text{index:}~ \mathbb{Z}, x: \mathbb{F}^{s \times s'})$
  260. \For {$i$ to $m$}
  261. \For {$j$ to $n$}
  262. \If {$M_{i,j} \neq 0$}
  263. \State $v.\text{append}( \{ \text{index}: i \cdot n + j,~ x: M_{i,j} \} )$
  264. \EndIf
  265. \EndFor
  266. \EndFor
  267. \State return $v$ \Comment {$v$ represents the evaluations of the polynomial}
  268. \end{algorithmic}
  269. \end{algorithm}
  270. Once we have the polynomial, its MLE comes from
  271. $$\widetilde{M}(x_1, \ldots, x_{s+s'}) = \sum_{e \in \{0,1\}^{s+s'}} M(e) \cdot \widetilde{eq}(x, e)$$
  272. $$M(X) \in \mathbb{F}[X_1, \ldots, X_s]$$
  273. \paragraph{Multilinear extensions of vectors}
  274. Given a vector $u \in \mathbb{F}^m$, the polynomial $\widetilde{u}$ is the MLE of $u$, and is obtained by viewing $u$ as a function mapping ($s=\log m$)
  275. $$u(x): \{0,1\}^s \rightarrow \mathbb{F}$$
  276. $\widetilde{u}(x, e)$ is the multilinear extension of the function $u(x)$
  277. $$\widetilde{u}(x_1, \ldots, x_s) = \sum_{e \in \{0,1\}^s} u(e) \cdot \widetilde{eq}(x, e)$$
  278. \bibliography{paper-notes.bib}
  279. \bibliographystyle{unsrt}
  280. \end{document}