math/slides_hypernova-part1-introduction.tex
slides_hypernova-part1-introduction.texRaw
1\documentclass{beamer}
2\usefonttheme[onlymath]{serif}
3
4\mode<presentation>
5{
6 \usetheme{Frankfurt}
7 \usecolortheme{dove} %% grey scale
8 \useinnertheme{circles}
9 % \setbeamercovered{transparent}
10}
11
12\hypersetup{
13 colorlinks,
14 citecolor=black,
15 filecolor=black,
16 linkcolor=black,
17 urlcolor=blue
18}
19\usepackage{graphicx}
20\usepackage{listings} % embed code
21
22\setbeamertemplate{itemize}{$\circ$}
23\setbeamertemplate{itemize items}{$\circ$}
24
25\beamertemplatenavigationsymbolsempty %% no navigation bar
26
27\setbeamertemplate{footline}{\hspace*{.1cm}\scriptsize{
28\hspace*{50pt} \hfill\insertframenumber/\inserttotalframenumber\hspace*{.1cm}\vspace*{.1cm}}}
29
30\setbeamertemplate{caption}[numbered]
31\setbeamerfont{caption}{size=\tiny}
32
33
34
35
36\title{HyperNova introduction}
37\author{}
38\date{\scriptsize{2023-07-25\\\href{https://0xparc.org}{0xPARC}, London}}
39
40\begin{document}
41
42\frame{\titlepage}
43
44
45% NOTE: This talk provides an overview, if people is interested we can do another session going more into the technical details of the schemes.
46
47
48\section[Preliminaries]{Preliminaries}
49
50\begin{frame}{IVC}
51
52For a function $F$, with initial input $z_0$, an IVC scheme allows a prover to produce a proof $\pi_i$ for the statement $z_i = F^{(i)}(z_0)$, given a proof $\pi_{i-1}$ for the statement $z_{i-1} = F^{(i-1)}(z_0)$
53
54TODO add draw
55TODO add reference to Valiant paper (2008)
56
57\end{frame}
58
59\begin{frame}{Recursion before folding schemes}
60We used to use recursive SNARKs to achieve IVC.
61
62 \begin{itemize}
63 \item Prove verification in circuit: inside a circuit, verify another proof
64 \begin{itemize}
65 \item eg. verifying a Groth16 proof inside a Groth16 circuit.
66 \end{itemize}
67 \item Amortized accumulation
68 \begin{itemize}
69 \item eg. Halo
70 \end{itemize}
71 \end{itemize}
72\end{frame}
73
74\begin{frame}{R1CS refresher}
75
76 R1CS instance: $(\{A, B, C\} \in \mathbb{F}^{m \times n},~ io,~ m,~ n,~ l)$, such that for $z=(io \in \mathbb{F}^l, 1, w \in \mathbb{F}^{m-l-1}) \in \mathbb{F}^m$,
77
78$$Az \circ Bz = Cz$$
79
80Typically we use some scheme to prove that the previous equation is fulfilled by some private $w$ (eg. Groth16, Marlin, Spartan, etc).
81
82\end{frame}
83
84% \begin{frame}{R1CS refresher}
85% TODO add A, B, C example from Vitalik article
86% \end{frame}
87
88\begin{frame}{Random linear combination}
89
90Combine 2 instances together through a random linear comibnation, and the outputted instance will still satisfy the relation.
91
92\begin{itemize}
93 \item Have 2 values $x_1, x_2$.
94 \item Set $r \in^R \mathbb{F}$
95 \item Compute $x_3 = x_1 + r \cdot x_2$.
96\end{itemize}
97
98\pause
99
100Combined with homomorphic commitments
101\begin{itemize}
102 \item We can do random linear combinations with the commitments and their witnesses, and the output can still be opened
103\end{itemize}
104
105% TODO check on internet if there is some more standard definition / examples.
106
107\end{frame}
108
109
110\section[Nova]{Nova}
111
112\begin{frame}{Folding schemes}
113We're not verifying the entire proof
114\begin{itemize}
115 \item Take n instances and 'batch' them together
116 \begin{itemize}
117 \item Folds $k$ (eg. 2) instances (eg. R1CS instances) and their respective witnesses into a single one
118 \end{itemize}
119 \item At the end of the chain of folds, we just prove that the last fold is correct through a SNARK
120 \begin{itemize}
121 \item Which implies that all the previous folds were correct
122 \end{itemize}
123\end{itemize}
124
125\pause
126
127In Nova: folding without a SNARK, we just reduce the satisfiability of the 2 inputted instances to the satisfiability of the single outputted one.
128
129[TODO image of multiple folding iterations]
130
131\end{frame}
132
133
134\begin{frame}{Relaxed R1CS}
135 We work with \emph{relaxed R1CS}
136
137$$Az \circ Bz = u \cdot Cz + E$$
138
139\begin{scriptsize} % TODO use the other simpler font syntax
140(= R1CS when $u=1,~ E=0$)
141\end{scriptsize}
142
143\begin{itemize}
144 \item main idea: allows us to fold, but accumulates \emph{cross terms}
145 \pause
146 \item when we do the \emph{relaxed} of higher degree equations (eg. plonkish), the cross terms grow (eg. Sangria with higher degree gates)
147\end{itemize}
148
149\end{frame}
150
151\begin{frame}{NIFS - setup}
152V and P: \emph{committed relaxed R1CS} instances
153\begin{align*}
154 \varphi_1&=(\overline{E}_1, u_1, \overline{w}_1, x_1)\\
155 \varphi_2&=(\overline{E}_2, u_2, \overline{w}_2, x_2)
156\end{align*}
157
158P: witnesses
159\begin{align*}
160 (E_1, r_{E_1}, w_1, r_{w_1})\\
161 (E_2, r_{E_2}, w_2, r_{w_2})
162\end{align*}
163
164Let $z_1 = (w_1, x_1, u_1)$ and $z_2 = (w_2, x_2, u_2)$.
165
166\end{frame}
167
168\begin{frame}{NIFS}
169\begin{footnotesize}
170% While Prover works with $w, E$, Verifier works with commitments to them (\emph{Committed Relaxed R1CS}).\\
171% To keep the relations working with the random linear combinations, we use homomorphic commitments.
172
173\begin{itemize}
174 \item V, P: folded instance $\varphi = (\overline{E}, u, \overline{w}, x)$
175 \begin{align*}
176 &\overline{E}=\overline{E}_1 + r \overline{T} + r^2 \overline{E}_2\\
177 &u = u_1 + r u_2\\
178 &\overline{w} = \overline{w}_1 + r \overline{w}_2\\
179 &x = x_1 + r x_2
180 \end{align*}
181 \item P: folded witness $(E, r_E, w, r_W)$
182 \begin{align*}
183 &E = E_1 + r T + r^2 E_2\\
184 &r_E = r_{E_1} + r \cdot r_T + r^2 r_{E_2}\\
185 &w=w_1 + r w_2\\
186 &r_W = r_{w_1} + r \cdot r_{w_2}
187 \end{align*}
188\end{itemize}
189\end{footnotesize}
190\pause
191\begin{scriptsize}
192Note: $T$ are the cross-terms coming from combining the two R1CS instances from
193\begin{align*}
194 Az \circ Bz &=A(z_1 + r \cdot z_2) \circ B(z_1 + r z_2)\\
195 &=A z_1 \circ B z_1 + r(A z_1 \circ B z_2 + A z_2 \circ B z_1) + r^2 (A z_2 \circ B z_2) = \ldots
196\end{align*}
197\end{scriptsize}
198
199\end{frame}
200
201\begin{frame}{NIFS}
202
203\begin{small}
204$$E=E_1 + r \underbrace{ (A z_1 \circ B z_2 + A z_2 \circ B z_1 - u_1 C z_2 - u_2 C z_1) }_\text{cross-terms} + r^2 E_2$$
205\end{small}
206
207$Az \circ Bz = uCz + E$ will hold for valid $z$ (which comes from valid $z_1,~ z_2$).
208
209[TODO add image of function F' with F inside with extra checks]
210
211\end{frame}
212
213
214
215\begin{frame}{NIFS}
216
217Each fold: $2~EC_{Add} + 1~EC_{Mul} + 1~hash$
218
21920k R1CS constraints (using curve cycles)
220
221{\footnotesize
222(so folding makes sense when we have a circuit with more than $2 \cdot 20k$ constraints)
223}
224
225\pause
226After all the folding iterations, Nova generates a SNARK proving the last folding instance.
227
228In Nova implementation, they use Spartan.
229\end{frame}
230
231\begin{frame}{Benchmarks}
232
233% TODO: review names, and add links to profiles.
234Benchmarks that Oskar, Carlos, et al did during the Vietnam residency in April
235\href{https://hackmd.io/u3qM9s_YR1emHZSg3jteQA?view}{https://hackmd.io/u3qM9s\_YR1emHZSg3jteQA}
236
237\begin{center}
238\begin{tabular}{ |c|c|c| }
239 \hline
240 Size & Constraints & Time\\
241 \hline
242 2KB & 883k & 320ms\\
243 4KB & 1.7m & 521ms\\
244 8KB & 3.4m & 1s\\
245 16KB & 6.8m & 1.9s\\
246 32KB & 13.7m & 4.1s \\
247 \hline
248\end{tabular}\\
249{\footnotesize eg. for 8kb, x100 Halo2 and Plonky2}
250\end{center}
251
252(this is for the folding, without the last snark)
253
254\end{frame}
255
256\begin{frame}{SuperNova}
257\begin{itemize}
258 \item iteration on Nova, combining \emph{different circuits} in a single one with \emph{selectors}
259 \item so we can work with a big circuit with \emph{subcircuits} without paying the whole size cost on each iteration
260 \item in IVC terms: fold multiple $F_i$ in a single $F'$ (in Nova was a single $F$ in $F'$)
261\end{itemize}
262
263This is useful for example for a VM, doing one $F_i$ for each opcode
264
265\end{frame}
266
267\section[HyperNova]{HyperNova}
268
269% \begin{frame}{CCS}
270% \begin{itemize}
271% \item kind of a generalization of constraint systems
272% \item can translate R1CS,Plonk,AIR to CCS
273% \end{itemize}
274% $$\sum_{i=0}^{q-1} c_i \cdot \bigcirc_{j \in S_i} M_j \cdot z ==0$$
275% \end{frame}
276
277\begin{frame}{R1CS to CCS example}
278
279\begin{scriptsize}
280\begin{itemize}
281 \item Kind of a generalization of constraint systems
282 \item Can translate R1CS,Plonk,AIR to CCS
283\end{itemize}
284\pause
285\begin{description}
286 \item[CCS instance] $S_{CCS} = (m, n, N, l, t, q, d, M, S, c)$\\
287 where we have the same parameters than in $S_{R1CS}$, but additionally:\\
288 $t=|M|$, $q = |c| = |S|$, $d$= max degree in each variable.
289 \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\}$
290\end{description}
291\pause
292
293The CCS relation check:
294\end{scriptsize}
295
296$$\sum_{i=0}^{q-1} c_i \cdot \bigcirc_{j \in S_i} M_j \cdot z ==0$$
297
298\begin{scriptsize}
299In our R1CS-to-CCS parameters is equivalent to
300\begin{align*}
301 &c_0 \cdot ( (M_0 z) \circ (M_1 z) ) + c_1 \cdot (M_2 z) ==0\\
302 \Longrightarrow &1 \cdot ( (A z) \circ (B z) ) + (-1) \cdot (C z) ==0\\
303 \Longrightarrow &( (A z) \circ (B z) ) - (C z) ==0
304\end{align*}
305\end{scriptsize}
306
307\end{frame}
308
309
310\begin{frame}{Multifolding}
311\begin{itemize}
312 \item Nova: 2-to-1 folding
313 \item HyperNova: multifolding, k-to-1 folding
314 \item We fold while through a SumCheck proving the correctness of the fold
315\end{itemize}
316
317SumCheck's polynomial work is trivial, most of the cost comes from Poseidon hash in the transcript
318
319[TODO WIP section]
320
321\end{frame}
322
323\begin{frame}{Multifolding - Overview}
324
325 \begin{tiny}
326 \begin{enumerate}
327 \item[1.] $V \rightarrow P: \gamma \in^R \mathbb{F},~ \beta \in^R \mathbb{F}^s$
328 \item[2.] $V: r_x' \in^R \mathbb{F}^s$
329 \item[3.] $V \leftrightarrow P$: sum-check protocol:
330 $c \leftarrow \langle P, V(r_x') \rangle (g, s, d+1, \underbrace{\sum_{j \in [t]} \gamma^j \cdot v_j}_\text{T})$, where:
331 \begin{align*}
332 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}\\
333 L_j(x) &:= \widetilde{eq}(r_x, x) \cdot \left(
334 \underbrace{\sum_{y \in \{0,1\}^{s'}} \widetilde{M}_j(x, y) \cdot \widetilde{z}_1(y)}_\text{LCCCS check}
335 \right)\\
336 Q(x) := &\widetilde{eq}(\beta, x) \cdot \left(
337 \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{CCCS check}
338 \right)
339 \end{align*}
340 \end{enumerate}
341 \end{tiny}
342
343\end{frame}
344
345\begin{frame}{Multifolding - Overview}
346
347 \begin{tiny}
348 \begin{enumerate}
349 \item[4.] $P \rightarrow V$: $\left( (\sigma_1, \ldots, \sigma_t), (\theta_1, \ldots, \theta_t) \right)$, where $\forall j \in [t]$,
350 $$\sigma_j = \sum_{y \in \{0,1\}^{s'}} \widetilde{M}_j(r_x', y) \cdot \widetilde{z}_1(y)$$
351 $$\theta_j = \sum_{y \in \{0, 1\}^{s'}} \widetilde{M}_j(r_x', y) \cdot \widetilde{z}_2(y)$$
352 \item[5.] V: $e_1 \leftarrow \widetilde{eq}(r_x, r_x')$, $e_2 \leftarrow \widetilde{eq}(\beta, r_x')$\\
353 check:
354 $$c = \left(\sum_{j \in [t]} \gamma^j \cdot e_1 \cdot \sigma_j \right) + \gamma^{t+1} \cdot e_2 \cdot \left( \sum_{i=1}^q c_i \cdot \prod_{j \in S_i} \theta_j \right)$$
355 \item[6.] $V \rightarrow P: \rho \in^R \mathbb{F}$
356 \item[7.] $V, P$: output the folded LCCCS instance $(C', u', \mathsf{x}', r_x', v_1', \ldots, v_t')$, where $\forall i \in [t]$:
357 \begin{align*}
358 C' &\leftarrow C_1 + \rho \cdot C_2\\
359 u' &\leftarrow u + \rho \cdot 1\\
360 \mathsf{x}' &\leftarrow \mathsf{x}_1 + \rho \cdot \mathsf{x}_2\\
361 v_i' &\leftarrow \sigma_i + \rho \cdot \theta_i
362 \end{align*}
363 \item[8.] $P$: output folded witness and the folded $r_w'$:
364 \begin{align*}
365 \widetilde{w}' &\leftarrow \widetilde{w}_1 + \rho \cdot \widetilde{w}_2\\
366 r_w' &\leftarrow r_{w_1} + \rho \cdot r_{w_2}
367 \end{align*}
368 \end{enumerate}
369 \end{tiny}
370
371\end{frame}
372
373\section[Wrappup]{Wrappup}
374
375\begin{frame}{Mysteries \& unsolved things}
376\begin{itemize}
377 \item how HyperNova compares to Protostar
378 \item prover knows the full witness [TODO update/rm this]
379\end{itemize}
380
381[TODO WIP section]
382\end{frame}
383
384
385\begin{frame}
386\frametitle{Wrappup}
387\begin{itemize}
388 \item HyperNova: \href{https://eprint.iacr.org/2023/573}{https://eprint.iacr.org/2023/573}
389 \item multifolding PoC on arkworks: \href{https://github.com/privacy-scaling-explorations/multifolding-poc}{github.com/privacy-scaling-explorations/multifolding-poc}
390 \item PSE hypernova WIP \href{https://github.com/privacy-scaling-explorations/Nova}{github.com/privacy-scaling-explorations/Nova}
391\end{itemize}
392
393\vspace{2cm}
394\tiny{
395 $$\text{2023-07-25}$$
396 $$\text{\href{https://0xparc.org}{0xPARC}}$$
397}
398\end{frame}
399
400
401% from Michael
402% - Why Nova?
403% - Nova's limitations
404% - Why Hypernova
405% - Hypernova concepts explained to General Technologist (minimal ZK understanding)
406% - Final output
407
408
409
410%%%%%
411% - We used recursive SNARKs to achieve IVC
412% - get a proof and prove that it's verification passes, inside another proof
413% - Folding: we're not verifying the entire proof
414% - we take n proofs and 'batch' them together
415% - at the end of the chain of folds, we just prove that the last fold is correct
416% - which implies that all the previous folds were correct
417% - Random Linear Combination: combine 2 instances together through a random linear comibnation, and the outputted instance will still satisfy the relation
418% - Multifolding SumCheck: SumCheck's polynomial work is trivial, most of the cost comes from Poseidon hash in the transcript
419
420\end{document}