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{pgf-umlsd} % diagrams
 11\usepackage{centernot}
 12\usepackage{algorithm}
 13\usepackage{algpseudocode}
 14
 15
 16% prevent warnings of underfull \hbox:
 17\usepackage{etoolbox}
 18\apptocmd{\sloppy}{\hbadness 4000\relax}{}{}
 19
 20\theoremstyle{definition}
 21\newtheorem{definition}{Def}[section]
 22\newtheorem{theorem}[definition]{Thm}
 23
 24% custom lemma environment to set custom numbers
 25\newtheorem{innerlemma}{Lemma}
 26\newenvironment{lemma}[1]
 27{\renewcommand\theinnerlemma{#1}\innerlemma}
 28{\endinnerlemma}
 29
 30
 31\title{Notes on HyperNova}
 32\author{arnaucube}
 33\date{May 2023}
 34
 35\begin{document}
 36
 37\maketitle
 38
 39\begin{abstract}
 40	Notes taken while reading about Spartan \cite{cryptoeprint:2023/573}, \cite{cryptoeprint:2023/552}.
 41
 42	Usually while reading papers I take handwritten notes, this document contains some of them re-written to $LaTeX$.
 43
 44	The notes are not complete, don't include all the steps neither all the proofs.
 45\end{abstract}
 46
 47\tableofcontents
 48
 49
 50\section{CCS}
 51\subsection{R1CS to CCS overview}
 52
 53\begin{description}
 54	\item[R1CS instance] $S_{R1CS} = (m, n, N, l, A, B, C)$\\
 55		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}$.
 56	\item[CCS instance] $S_{CCS} = (m, n, N, l, t, q, d, M, S, c)$\\
 57		where we have the same parameters than in $S_{R1CS}$, but additionally:\\
 58		$t=|M|$, $q = |c| = |S|$, $d$= max degree in each variable.
 59	\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\}$
 60\end{description}
 61
 62The CCS relation check:
 63$$\sum_{i=0}^{q-1} c_i \cdot \bigcirc_{j \in S_i} M_j \cdot z ==0$$
 64
 65where $z=(w, 1, x) \in \mathbb{F}^n$.
 66
 67In our R1CS-to-CCS parameters is equivalent to
 68
 69\begin{align*}
 70	&c_0 \cdot ( (M_0 z) \circ (M_1 z) ) + c_1 \cdot (M_2 z) ==0\\
 71	\Longrightarrow &1 \cdot ( (A z) \circ (B z) ) + (-1) \cdot (C z) ==0\\
 72	\Longrightarrow &( (A z) \circ (B z) ) - (C z) ==0
 73\end{align*}
 74
 75which is equivalent to the R1CS relation: $Az \circ Bz == Cz$
 76
 77An example of the conversion from R1CS to CCS implemented in SageMath can be found at\\
 78\href{https://github.com/arnaucube/math/blob/master/r1cs-ccs.sage}{https://github.com/arnaucube/math/blob/master/r1cs-ccs.sage}.
 79
 80\subsection{Committed CCS}
 81$R_{CCCS}$ instance: $(C, \mathsf{x})$, where $C$ is a commitment to a multilinear polynomial in $s'-1$ variables.
 82
 83Sat if:
 84\begin{enumerate}[i.]
 85	\item $\text{Commit}(pp, \widetilde{w}) = C$
 86	\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)$\\
 87		where $\widetilde{z}(y) = \widetilde{(w, 1, \mathsf{x})}(x) ~\forall x \in \{0, 1\}^{s'}$
 88\end{enumerate}
 89
 90
 91\subsection{Linearized Committed CCS}
 92$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]$.
 93
 94Sat 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
101
102\section{Multifolding Scheme for CCS}
103Recall sum-check protocol notation: \underline{$C \leftarrow \langle P, V(r) \rangle (g, l, d, T)$}:
104$$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)$$
105where $g$ is a $l$-variate polynomial, with degree at most $d$ in each variable, and $T$ is the claimed value.
106
107\vspace{1cm}
108
109Let $s= \log m,~ s'= \log n$.
110
111\begin{enumerate}
112	\item $V \rightarrow P: \gamma \in^R \mathbb{F},~ \beta \in^R \mathbb{F}^s$
113	\item $V: r_x' \in^R \mathbb{F}^s$
114	\item $V \leftrightarrow P$: sum-check protocol:
115		$$c \leftarrow \langle P, V(r_x') \rangle (g, s, d+1, \overbrace{\sum_{j \in [t]} \gamma^j \cdot v_j}^\text{T})$$
116		where:
117		\begin{align*}
118			g(x) &:= \left( \sum_{j \in [t]} \gamma^j \cdot L_j(x) \right) + \gamma^{t+1} \cdot Q(x)\\
119			\text{for LCCCS:}~ L_j(x) &:= \widetilde{eq}(r_x, x) \cdot \left(
120				\underbrace{\sum_{y \in \{0,1\}^{s'}} \widetilde{M}_j(x, y) \cdot \widetilde{z}_1(y)}_\text{this is the check from LCCCS}
121			\right)\\
122				\text{for CCCS:}~ Q(x) := &\widetilde{eq}(\beta, x) \cdot \left(
123				\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 CommittedCCS}
124			\right)
125		\end{align*}
126		Notice that $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)$.
127	\item $P \rightarrow V$: $\left( (\sigma_1, \ldots, \sigma_t), (\theta_1, \ldots, \theta_t) \right)$, where $\forall j \in [t]$,
128		$$\sigma_j = \sum_{y \in \{0,1\}^{s'}} \widetilde{M}_j(r_x', y) \cdot \widetilde{z}_1(y)$$
129		$$\theta_j = \sum_{y \in \{0, 1\}^{s'}} \widetilde{M}_j(r_x', y) \cdot \widetilde{z}_2(y)$$
130		where $\sigma_j,~\theta_j$ are the checks from LCCCS and CCCS respectively with $x=r_x'$.
131	\item V: $e_1 \leftarrow \widetilde{eq}(r_x, r_x')$, $e_2 \leftarrow \widetilde{eq}(\beta, r_x')$\\
132		check:
133		$$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)$$
134		which should be equivalent to the $g(x)$ computed by $V,P$ in the sum-check protocol.
135	\item $V \rightarrow P: \rho \in^R \mathbb{F}$
136	\item $V, P$: output the folded LCCCS instance $(C', u', \mathsf{x}', r_x', v_1', \ldots, v_t')$, where $\forall i \in [t]$:
137		\begin{align*}
138			C' &\leftarrow C_1 + \rho \cdot C_2\\
139			u' &\leftarrow u + \rho \cdot 1\\
140			\mathsf{x}' &\leftarrow \mathsf{x}_1 + \rho \cdot \mathsf{x}_2\\
141			v_i' &\leftarrow \sigma_i + \rho \cdot \theta_i
142		\end{align*}
143	\item $P$: output folded witness: $\widetilde{w}' \leftarrow \widetilde{w}_1 + \rho \cdot \widetilde{w}_2$.
144\end{enumerate}
145
146
147
148%%%%%% APPENDIX
149\appendix
150\section{Appendix: Some details}
151This 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.
152
153\subsection{Matrix and Vector to Sparse Multilinear Extension}
154
155Let $M \in \mathbb{F}^{m \times n}$ be a matrix. We want to compute its MLE
156$$\widetilde{M}(x_1, \ldots, x_l) = \sum_{e \in \{0, 1 \}^l} M(e) \cdot \widetilde{eq}(x, e)$$
157
158We can view the matrix $M \in \mathbb{F}^{m \times n}$ as a function with the following signature:
159$$M(\cdot): \{0,1\}^s \times \{0,1\}^{s'} \rightarrow \mathbb{F}$$
160where $s = \lceil \log m \rceil,~ s' = \lceil \log n \rceil$.
161
162An entry in $M$ can be accessed with a $(s+s')$-bit identifier.
163
164eg.:
165$$
166M = \begin{pmatrix}
1671 & 2 & 3\\
1684 & 5 & 6\\
169\end{pmatrix}
170\in \mathbb{F}^{3 \times 2}
171$$
172
173$m = 3,~ n = 2,~~~ s = \lceil \log 3 \rceil = 2,~ s' = \lceil \log 2 \rceil = 1$
174
175So, $M(s_0, s_1) = x$, where $s_0 \in \{0,1\}^s,~ s_1 \in \{0,1\}^{s'},~ x \in \mathbb{F}$
176
177$$
178M = \begin{pmatrix}
179M(00,0) & M(01,0) & M(10,0)\\
180M(00,1) & M(01,1) & M(10,1)\\
181\end{pmatrix}
182\in \mathbb{F}^{3 \times 2}
183$$
184
185This logic can be defined as follows:
186
187\begin{algorithm}[H]
188\caption{Generating a Sparse Multilinear Polynomial from a matrix}
189\begin{algorithmic}
190	\State set empty vector $v \in (\text{index:}~ \mathbb{Z}, x: \mathbb{F})^{s \times s'}$
191	\For {$i$ to $n$}
192	\For {$j$ to $m$}
193		\If {$M_{i,j} \neq 0$}
194			\State $v.\text{append}( \{ \text{index}: i \cdot m + j,~ x: M_{i,j} \} )$
195		\EndIf
196	\EndFor
197	\EndFor
198	\State return $v$    \Comment {$v$ represents the evaluations of the polynomial}
199\end{algorithmic}
200\end{algorithm}
201
202Once we have the polynomial, its MLE comes from
203$$\widetilde{M}(x_1, \ldots, x_{s+s'}) = \sum_{e \in \{0,1\}^{s+s'}} M(e) \cdot \widetilde{eq}(x, e)$$
204
205$$M(X) \in \mathbb{F}[X_1, \ldots, X_s]$$
206
207\paragraph{Multilinear extensions of vectors}
208Given 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$)
209$$u(x): \{0,1\}^s \rightarrow \mathbb{F}$$
210$\widetilde{u}(x, e)$ is the multilinear extension of the function $u(x)$
211$$\widetilde{u}(x_1, \ldots, x_s) = \sum_{e \in \{0,1\}^s} u(e) \cdot \widetilde{eq}(x, e)$$
212
213\bibliography{paper-notes.bib}
214\bibliographystyle{unsrt}
215
216\end{document}